roll back extra argument to on_clause

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/api/api_solver.cpp

@@ -1031,14 +1031,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 nd, unsigned const* deps, unsigned n, expr* const* _literals, unsigned const status) {
+        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()), nd, deps, of_ast_vector(literals), status);
+            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);

src/api/z3_api.h

@@ -1441,7 +1441,7 @@ 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_binding_eh, bool, (void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst));
-Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals, unsigned const status));
+Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals));
 
 
 /**

src/cmd_context/extra_cmds/proof_cmds.cpp

@@ -314,7 +314,7 @@ 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_deps.size(), m_deps.data(), m_lits.size(), m_lits.data(), 0u);
+            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();
@@ -328,7 +328,7 @@ 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_deps.size(), m_deps.data(), m_lits.size(), m_lits.data(), 0u);
+            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();
@@ -342,7 +342,7 @@ 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_deps.size(), m_deps.data(), m_lits.size(), m_lits.data(), 0u);
+            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();

src/sat/smt/euf_proof.cpp

@@ -382,7 +382,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, 0, nullptr, m_clause.size(), m_clause.data(), 0u);
+        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) {

src/smt/smt_clause_proof.cpp

@@ -194,16 +194,7 @@ namespace smt {
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) {
             // Encode status as an integer flag for simplicity.
-            unsigned st_code = 0;
-            switch (st) {
-                case status::assumption:    st_code = 1; break;
-                case status::lemma:         st_code = 2; break;
-                case status::th_lemma:      st_code = 3; break;
-                case status::th_assumption: st_code = 4; break;
-                case status::deleted:       st_code = 5; break;
-                default:                    st_code = 0; break;
-            }
-            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data(), st_code);
+            m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
         }
 
         if (m_has_log) {

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, unsigned const*, unsigned, expr* const*, unsigned const)>        on_clause_eh_t;
+    typedef std::function<void(void*, expr*, unsigned, unsigned const*, unsigned, expr* const*)>        on_clause_eh_t;
     typedef std::function<bool(void*, callback*, expr*, expr*)>              binding_eh_t;
 
     class plugin : public decl_plugin {