enable on-clause with dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jul 18, 2023 · 3d8f75b · 3d8f75b
1 parent 9db636c
commit 3d8f75b
Show file tree

Hide file tree

Showing 9 changed files with 46 additions and 18 deletions.
diff --git a/scripts/update_api.py b/scripts/update_api.py
@@ -1919,7 +1919,7 @@ def _to_pystr(s):
 _lib.Z3_set_error_handler.restype  = None
 _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
 
-Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
+Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.POINTER(ctypes.c_uint), ctypes.c_void_p)
 Z3_push_eh  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
 Z3_pop_eh   = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
 Z3_fresh_eh = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
@@ -984,14 +984,14 @@ extern "C" {
         Z3_TRY;
         RESET_ERROR_CODE();
         init_solver(c, s);     
-        user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned n, expr* const* _literals) {
+        user_propagator::on_clause_eh_t _on_clause = [=](void* user_ctx, expr* proof, unsigned nd, unsigned const* deps, unsigned n, expr* const* _literals) {
             Z3_ast_vector_ref * literals = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
             mk_c(c)->save_object(literals);
             expr_ref pr(proof, mk_c(c)->m());
             scoped_ast_vector _sc(literals);
             for (unsigned i = 0; i < n; ++i)
                 literals->m_ast_vector.push_back(_literals[i]);
-            on_clause_eh(user_ctx, of_expr(pr.get()), of_ast_vector(literals));
+            on_clause_eh(user_ctx, of_expr(pr.get()), nd, deps, of_ast_vector(literals));
         };
         to_solver_ref(s)->register_on_clause(user_context, _on_clause);
         auto& solver = *to_solver(s);

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
@@ -11438,11 +11438,12 @@ def to_AstVectorObj(ptr,):
 # for UserPropagator we use a global dictionary, which isn't great code.
 
 _my_hacky_class = None
-def on_clause_eh(ctx, p, clause):
+def on_clause_eh(ctx, p, n, dep, clause):
     onc = _my_hacky_class
     p = _to_expr_ref(to_Ast(p), onc.ctx)
     clause = AstVector(to_AstVectorObj(clause), onc.ctx)
-    onc.on_clause(p, clause)
+    deps = [dep[i] for i in range(n)]
+    onc.on_clause(p, deps, clause)
 
 _on_clause_eh = Z3_on_clause_eh(on_clause_eh)
 

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
@@ -1437,7 +1437,7 @@ Z3_DECLARE_CLOSURE(Z3_eq_eh,      void, (void* ctx, Z3_solver_callback cb, Z3_as
 Z3_DECLARE_CLOSURE(Z3_final_eh,   void, (void* ctx, Z3_solver_callback cb));
 Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
 Z3_DECLARE_CLOSURE(Z3_decide_eh,  void, (void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase));
-Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, Z3_ast_vector literals));
+Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals));
 
 
 /**

diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp
@@ -126,7 +126,7 @@ class proof_trim {
         if (m_empty)
             return;
 
-        if (hint && !is_rup(hint) && m_checker.check(hint)) {
+        if (hint && !is_rup(hint)) {
             auto clause1 = m_checker.clause(hint);
             if (clause1.size() != clause.size()) {
                 mk_clause(clause1);
@@ -239,8 +239,10 @@ class proof_saver {
 class proof_cmds_imp : public proof_cmds {
     cmd_context&    ctx;
     ast_manager&    m;
+    arith_util      m_arith;
     expr_ref_vector m_lits;
     app_ref         m_proof_hint;
+    unsigned_vector m_deps;
     bool            m_check  = true;
     bool            m_save   = false;
     bool            m_trim   = false;
@@ -266,11 +268,24 @@ class proof_cmds_imp : public proof_cmds {
             m_del = m.mk_app(symbol("del"), 0, nullptr, m.mk_proof_sort());
         return m_del;
     }
+
+    bool is_dep(expr* e) {
+        return m.is_proof(e) && symbol("deps") == to_app(e)->get_name();
+    }
+
+    void get_deps(expr* e) {
+        rational n;
+        bool is_int = false;
+        for (expr* arg : *to_app(e)) 
+            if (m_arith.is_numeral(arg, n, is_int) && n.is_unsigned())
+                m_deps.push_back(n.get_unsigned());
+    }
 
 public:
     proof_cmds_imp(cmd_context& ctx): 
         ctx(ctx), 
-        m(ctx.m()), 
+        m(ctx.m()),
+        m_arith(m),
         m_lits(m), 
         m_proof_hint(m), 
         m_assumption(m), 
@@ -280,7 +295,9 @@ class proof_cmds_imp : public proof_cmds {
 
     void add_literal(expr* e) override {
         if (m.is_proof(e)) {
-            if (!m_proof_hint)
+            if (is_dep(e))
+                get_deps(e);
+            else if (!m_proof_hint)
                 m_proof_hint = to_app(e);
         }
         else if (!m.is_bool(e))
@@ -297,9 +314,10 @@ class proof_cmds_imp : public proof_cmds {
         if (m_trim)
             trim().assume(m_lits);
         if (m_on_clause_eh)
-            m_on_clause_eh(m_on_clause_ctx, assumption(), m_lits.size(), m_lits.data());
+            m_on_clause_eh(m_on_clause_ctx, assumption(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data());
         m_lits.reset();
         m_proof_hint.reset();
+        m_deps.reset();
     }
 
     void end_infer() override {
@@ -310,9 +328,10 @@ class proof_cmds_imp : public proof_cmds {
         if (m_trim)
             trim().infer(m_lits, m_proof_hint);
         if (m_on_clause_eh)
-            m_on_clause_eh(m_on_clause_ctx, m_proof_hint, m_lits.size(), m_lits.data());
+            m_on_clause_eh(m_on_clause_ctx, m_proof_hint, m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data());
         m_lits.reset();
         m_proof_hint.reset();
+        m_deps.reset();
     }
 
     void end_deleted() override {
@@ -323,9 +342,10 @@ class proof_cmds_imp : public proof_cmds {
         if (m_trim)
             trim().del(m_lits);
         if (m_on_clause_eh)
-            m_on_clause_eh(m_on_clause_ctx, del(), m_lits.size(), m_lits.data());
+            m_on_clause_eh(m_on_clause_ctx, del(), m_deps.size(), m_deps.data(), m_lits.size(), m_lits.data());
         m_lits.reset();
         m_proof_hint.reset();
+        m_deps.reset();
     }
 
     void updt_params(params_ref const& p) override {

diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp
@@ -266,7 +266,8 @@ namespace sat {
         m_clause.reset();
         switch (j.get_kind()) {
         case justification::NONE:
-            m_clause.push_back(l);
+            if (l != null_literal)
+                m_clause.push_back(l);
             break;                
         case justification::BINARY:
             m_clause.push_back(l);
@@ -282,7 +283,7 @@ namespace sat {
             break;
         }
         std::sort(m_clause.begin(), m_clause.end());
-        IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n");
+        IF_VERBOSE(3, verbose_stream() << "add core {" << m_clause << "}\n");
         auto& [clauses, id, in_core] = m_clauses.find(m_clause);
         in_core = true;
         insert_dep(id);
@@ -337,7 +338,13 @@ namespace sat {
     }
 
     void proof_trim::assume(unsigned id, bool is_initial) {
-        std::sort(m_clause.begin(), m_clause.end());                
+        std::sort(m_clause.begin(), m_clause.end()); 
+        unsigned j = 0;
+        sat::literal prev = null_literal;
+        for (unsigned i = 0; i < m_clause.size(); ++i) 
+            if (m_clause[i] != prev)
+               prev = m_clause[j++] = m_clause[i];        
+        m_clause.shrink(j);
         if (unit_or_binary_occurs())
             return;        
         if (!m_conflict.empty() && m_clause.empty()) {

diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
@@ -312,7 +312,7 @@ namespace euf {
         for (unsigned i = 0; i < n; ++i) 
             m_clause.push_back(literal2expr(lits[i]));
         auto hint = status2proof_hint(st);
-        m_on_clause(m_on_clause_ctx, hint, m_clause.size(), m_clause.data());
+        m_on_clause(m_on_clause_ctx, hint, 0, nullptr, m_clause.size(), m_clause.data());
     }
 
     void solver::on_proof(unsigned n, literal const* lits, sat::status st) {

diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
@@ -190,7 +190,7 @@ namespace smt {
         if (ctx.get_fparams().m_clause_proof)
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) 
-            m_on_clause_eh(m_on_clause_ctx, p, v.size(), v.data());        
+            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());        
         if (m_has_log) {
             init_pp_out();
             auto& out = *m_pp_out;

diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
@@ -27,7 +27,7 @@ namespace user_propagator {
     typedef std::function<void(void*, callback*, unsigned)>                  pop_eh_t;
     typedef std::function<void(void*, callback*, expr*)>                     created_eh_t;
     typedef std::function<void(void*, callback*, expr*, unsigned, bool)>     decide_eh_t;
-    typedef std::function<void(void*, expr*, unsigned, expr* const*)>        on_clause_eh_t;
+    typedef std::function<void(void*, expr*, unsigned, unsigned const*, unsigned, expr* const*)>        on_clause_eh_t;
 
     class plugin : public decl_plugin {
     public: