fixes to consequence generation and cancellation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_context.cpp

@@ -70,22 +70,6 @@ namespace api {
     //
     // ------------------------
 
-    context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
-        m_ctx(ctx) {
-        #pragma omp critical (set_interruptable) 
-        {
-            SASSERT(m_ctx.m_interruptable == 0);
-            m_ctx.m_interruptable = &i;
-        }
-    }
-
-    context::set_interruptable::~set_interruptable() {
-        #pragma omp critical (set_interruptable) 
-        {
-            m_ctx.m_interruptable = 0;
-        }
-    }
-
     context::context(context_params * p, bool user_ref_count):
         m_params(p != 0 ? *p : context_params()),
         m_user_ref_count(user_ref_count),
@@ -105,11 +89,10 @@ namespace api {
         m_print_mode = Z3_PRINT_SMTLIB_FULL;
         m_searching  = false;
         
-        m_interruptable = 0;
-
         m_smtlib_parser           = 0;
         m_smtlib_parser_has_decls = false;
-                
+
+        m_interruptable = 0;                
         m_error_handler = &default_error_handler;
 
         m_basic_fid = m().get_basic_family_id();
@@ -139,6 +122,22 @@ namespace api {
         }
     }
 
+    context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
+        m_ctx(ctx) {
+        #pragma omp critical (set_interruptable) 
+        {
+            SASSERT(m_ctx.m_interruptable == 0);
+            m_ctx.m_interruptable = &i;
+        }
+    }
+
+    context::set_interruptable::~set_interruptable() {
+        #pragma omp critical (set_interruptable) 
+        {
+            m_ctx.m_interruptable = 0;
+        }
+    }
+
     void context::interrupt() {
         #pragma omp critical (set_interruptable)
         {

src/api/api_context.h

@@ -94,7 +94,7 @@ namespace api {
 
         event_handler *            m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt
 
-    public:
+     public:
         // Scoped obj for setting m_interruptable
         class set_interruptable {
             context & m_ctx;

src/api/z3_replayer.cpp

@@ -515,7 +515,7 @@ struct z3_replayer::imp {
                 if (idx >= m_cmds.size())
                     throw z3_replayer_exception("invalid command");
                 try {
-                    TRACE("z3_replayer_cmd", tout << m_cmds_names[idx] << "\n";);
+                    TRACE("z3_replayer_cmd", tout << idx << ":" << m_cmds_names[idx] << "\n";);
                     m_cmds[idx](m_owner);
                 }
                 catch (z3_error & ex) {

src/smt/asserted_formulas.cpp

@@ -543,8 +543,12 @@ void asserted_formulas::infer_patterns() {
 }
 
 void asserted_formulas::commit() {
-    m_macro_manager.mark_forbidden(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead);
+    commit(m_asserted_formulas.size());
-    m_asserted_qhead = m_asserted_formulas.size();
+}
+
+void asserted_formulas::commit(unsigned new_qhead) {
+    m_macro_manager.mark_forbidden(new_qhead - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead);
+    m_asserted_qhead = new_qhead;
 }
 
 void asserted_formulas::eliminate_term_ite() {

src/smt/asserted_formulas.h

@@ -113,6 +113,7 @@ public:
     unsigned get_formulas_last_level() const;
     unsigned get_qhead() const { return m_asserted_qhead; }
     void commit(); 
+    void commit(unsigned new_qhead); 
     expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
     proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
     expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }

src/smt/smt_consequences.cpp

@@ -174,6 +174,9 @@ namespace smt {
             else if (e_internalized(k) && m.are_distinct(v, get_enode(k)->get_root()->get_owner())) {
                 to_delete.push_back(k);
             }
+            else if (get_assignment(mk_diseq(k, v)) == l_true) {
+                to_delete.push_back(k);
+            }
         }
         for (unsigned i = 0; i < to_delete.size(); ++i) {
             var2val.remove(to_delete[i]);
@@ -215,9 +218,7 @@ namespace smt {
                 for (unsigned i = 0; i < literals.size(); ++i) {
                     literals[i].neg();
                 }
-                eq = mk_eq_atom(k, v);
+                literal lit = mk_diseq(k, v);
-                internalize_formula(eq, false);
-                literal lit(get_bool_var(eq), false);
                 literals.push_back(lit);
                 mk_clause(literals.size(), literals.c_ptr(), 0);
                 TRACE("context", display_literals_verbose(tout, literals.size(), literals.c_ptr()););
@@ -229,6 +230,18 @@ namespace smt {
         return to_delete.size();
     }
 
+    literal context::mk_diseq(expr* e, expr* val) {
+        ast_manager& m = m_manager;
+        if (m.is_bool(e)) {
+            return literal(get_bool_var(e), m.is_true(val));
+        }
+        else {
+            expr_ref eq(mk_eq_atom(e, val), m);
+            internalize_formula(eq, false);
+            return literal(get_bool_var(eq), true);
+        }
+    }
+
     lbool context::get_consequences(expr_ref_vector const& assumptions, 
                                     expr_ref_vector const& vars, 
                                     expr_ref_vector& conseq, 
@@ -288,18 +301,7 @@ namespace smt {
             // the opposite value of the current reference model.
             // If the variable is a non-Boolean, it means adding a disequality.
             //
-            literal lit;
+            literal lit = mk_diseq(e, val);
-            if (m.is_bool(e)) {
-                lit = literal(get_bool_var(e), m.is_true(val));
-            }
-            else {
-                eq = mk_eq_atom(e, val);
-                internalize_formula(eq, false);
-                lit = literal(get_bool_var(eq), true);
-                TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";
-                      display_literal_verbose(tout, lit); tout << "\n"; 
-                      tout << "Equal: " << are_equal(e, val) << "\n";);
-            }
             mark_as_relevant(lit);
             push_scope();
             assign(lit, b_justification::mk_axiom(), true);
@@ -434,6 +436,7 @@ namespace smt {
         pop_to_base_lvl();
         lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
         if (is_sat != l_true) {
+            TRACE("context", tout << is_sat << "\n";);
             return is_sat;
         }
         obj_map<expr, expr*> var2val;
@@ -475,20 +478,12 @@ namespace smt {
             obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
             unsigned num_vars = 0;
             for (; it != end && num_vars < chunk_size; ++it) {
+                if (get_cancel_flag()) {
+                    return l_undef;
+                }
                 expr* e = it->m_key;
                 expr* val = it->m_value;
-                literal lit;
+                literal lit = mk_diseq(e, val);
-                if (m.is_bool(e)) {
-                    lit = literal(get_bool_var(e), m.is_true(val));
-                }
-                else {
-                    eq = mk_eq_atom(e, val);
-                    internalize_formula(eq, false);
-                    lit = literal(get_bool_var(eq), true);
-                    TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";
-                          display_literal_verbose(tout, lit); tout << "\n"; 
-                          tout << "Equal: " << are_equal(e, val) << "\n";);
-                }
                 mark_as_relevant(lit);
                 if (get_assignment(lit) != l_undef) {
                     continue;
@@ -504,9 +499,6 @@ namespace smt {
                         m_not_l = null_literal;
                         SASSERT(m_search_lvl == get_search_level());
                     }
-                    if (get_cancel_flag()) {
-                        return l_undef;
-                    }
                 }
             }
             SASSERT(!inconsistent());

src/smt/smt_context.cpp

@@ -1833,7 +1833,7 @@ namespace smt {
         m_stats.m_num_decisions++;
         
         push_scope();
-        TRACE("context", tout << "splitting, lvl: " << m_scope_lvl << "\n";);
+        TRACE("decide", tout << "splitting, lvl: " << m_scope_lvl << "\n";);
 
         TRACE("decide_detail", tout << mk_pp(bool_var2expr(var), m_manager) << "\n";);
 
@@ -2949,7 +2949,11 @@ namespace smt {
         if (!m_asserted_formulas.inconsistent()) {
             unsigned sz    = m_asserted_formulas.get_num_formulas();
             unsigned qhead = m_asserted_formulas.get_qhead();
-            while (qhead < sz && !m_manager.canceled()) {
+            while (qhead < sz) {
+                if (get_cancel_flag()) {
+                    m_asserted_formulas.commit(qhead);
+                    return;
+                }
                 expr * f   = m_asserted_formulas.get_formula(qhead);
                 proof * pr = m_asserted_formulas.get_formula_proof(qhead);
                 internalize_assertion(f, pr, 0);

src/smt/smt_context.h

@@ -1356,6 +1356,8 @@ namespace smt {
 
         expr_ref antecedent2fml(uint_set const& ante);
 
+        literal mk_diseq(expr* v, expr* val);
+
         void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
                                    expr_ref_vector const& conseq, expr_ref_vector const& unfixed);
 

src/util/rlimit.cpp

@@ -36,7 +36,7 @@ bool reslimit::inc() {
 
 bool reslimit::inc(unsigned offset) {
     m_count += offset;
-    return !m_cancel && (m_limit == 0 || m_count <= m_limit);
+    return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
 }
 
 void reslimit::push(unsigned delta_limit) {