Fixed next_split call in pop (#6966)

* Give users ability to see if propagation failed

* Skip propagations in the new core if they are already satisfied

* Fix registration in final

* Don't make it too complicated...

* Fixed next_split when called in pop
Made delay_units available even without quantifiers

* Missing push calls before "decide"-callback

src/smt/smt_context.cpp

@@ -4122,7 +4122,6 @@ namespace smt {
             // Moreover, I backtrack only one level.
             bool delay_forced_restart =
                 m_fparams.m_delay_units &&
-                internalized_quantifiers() &&
                 num_lits == 1 &&
                 conflict_lvl > m_search_lvl + 1 &&
                 !m.proofs_enabled() &&

src/smt/theory_user_propagator.cpp

@@ -62,12 +62,12 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
     if (is_attached_to_var(n))
         return;
-    
+
     theory_var v = mk_var(n);
     m_var2expr.reserve(v + 1);
     m_var2expr[v] = term;
     m_expr2var.setx(term->get_id(), v, null_theory_var);
-    
+
     if (m.is_bool(e) && !ctx.b_internalized(e)) {
         bool_var bv = ctx.mk_bool_var(e);
         ctx.set_var_theory(bv, get_id());
@@ -79,7 +79,6 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     literal_vector explain;
     if (ctx.is_fixed(n, r, explain))
         m_prop.push_back(prop_info(explain, v, r));
-    
 }
 
 bool theory_user_propagator::propagate_cb(
@@ -109,14 +108,19 @@ void theory_user_propagator::register_cb(expr* e) {
 
 bool theory_user_propagator::next_split_cb(expr* e, unsigned idx, lbool phase) {
     if (e == nullptr) { // clear
-        m_next_split_var = null_bool_var;
+        m_next_split_var = nullptr;
+        return true;
+    }
+    if (!ctx.e_internalized(e)) {
+        // We may not eagerly internalize it (might crash when done in pop) => delay
+        m_next_split_var = e;
         return true;
     }
-    ensure_enode(e);
     bool_var b = enode_to_bool(ctx.get_enode(e), idx);
     if (b == null_bool_var || ctx.get_assignment(b) != l_undef)
         return false;
-    m_next_split_var = b;
+    m_next_split_var = e;
+    m_next_split_idx = idx;
     m_next_split_phase = phase;
     return true;
 }
@@ -150,7 +154,7 @@ final_check_status theory_user_propagator::final_check_eh() {
         m_final_eh(m_user_context, this);
     }
     catch (...) {
-      throw default_exception("Exception thrown in \"final\"-callback");
+        throw default_exception("Exception thrown in \"final\"-callback");
     }
     CTRACE("user_propagate", can_propagate(), tout << "can propagate\n");
     propagate();
@@ -170,11 +174,11 @@ void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned nu
     ctx.push_trail(insert_map<uint_set, unsigned>(m_fixed, v));
     m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector());
     try {
-         m_fixed_eh(m_user_context, this, var2expr(v), value);
-     }
-     catch (...) {
+        m_fixed_eh(m_user_context, this, var2expr(v), value);
+    }
+    catch (...) {
         throw default_exception("Exception thrown in \"fixed\"-callback");
-     }
+    }
 }
 
 bool_var theory_user_propagator::enode_to_bool(enode* n, unsigned idx) {
@@ -191,18 +195,18 @@ bool_var theory_user_propagator::enode_to_bool(enode* n, unsigned idx) {
 void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
     if (!m_decide_eh)
         return;
-    
+
     const bool_var_data& d = ctx.get_bdata(var);
-    
-    if (!d.is_enode() && !d.is_theory_atom()) 
+
+    if (!d.is_enode() && !d.is_theory_atom())
         return;
-    
-    enode* original_enode = nullptr; 
+
+    enode* original_enode = nullptr;
     unsigned original_bit = 0;
     bv_util bv(m);
     theory* th = nullptr;
     theory_var v = null_theory_var;
-    
+
     // get the associated theory
     if (!d.is_enode()) {
         // it might be a value that does not have an enode
@@ -216,7 +220,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
             th = ctx.get_theory(d.get_theory());
         }
     }
-    
+
     if (v == null_theory_var && !th)
         return;
 
@@ -225,7 +229,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
 
     if (v == null_theory_var) {
         // it is not a registered boolean value but it is a bitvector
-        auto registered_bv = ((theory_bv *) th)->get_bv_with_theory(var, get_family_id());
+        auto registered_bv = ((theory_bv*) th)->get_bv_with_theory(var, get_family_id());
         if (!registered_bv.first)
             // there is no registered bv associated with the bit
             return;
@@ -237,6 +241,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
     // call the registered callback
     unsigned new_bit = original_bit;
 
+    force_push();
     expr *e = var2expr(v);
     m_decide_eh(m_user_context, this, e, new_bit, is_pos);
 
@@ -252,12 +257,16 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
 }
 
 bool theory_user_propagator::get_case_split(bool_var& var, bool& is_pos) {
-    if (m_next_split_var == null_bool_var)
+    if (m_next_split_var == nullptr)
         return false;
-
-    var = m_next_split_var;
+    ensure_enode(m_next_split_var);
+    bool_var b = enode_to_bool(ctx.get_enode(m_next_split_var), m_next_split_idx);
+    if (b == null_bool_var || ctx.get_assignment(b) != l_undef)
+        return false;
+    var = b;
     is_pos = ctx.guess(var, m_next_split_phase);
-    m_next_split_var = null_bool_var;
+    m_next_split_var = nullptr;
+    m_next_split_idx = 0;
     m_next_split_phase = l_undef;
     return true;
 }
@@ -289,11 +298,11 @@ bool theory_user_propagator::can_propagate() {
 
 void theory_user_propagator::propagate_consequence(prop_info const& prop) {
     justification* js;
-    m_lits.reset();   
+    m_lits.reset();
     m_eqs.reset();
-    for (expr* id : prop.m_ids)
+    for (expr* id: prop.m_ids)
         m_lits.append(m_id2justification[expr2var(id)]);
-    for (auto const& [a,b] : prop.m_eqs)
+    for (auto const& [a, b]: prop.m_eqs)
         if (a != b)
             m_eqs.push_back(enode_pair(get_enode(expr2var(a)), get_enode(expr2var(b))));
     DEBUG_CODE(for (auto const& [a, b] : m_eqs) VERIFY(a->get_root() == b->get_root()););
@@ -328,7 +337,7 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
             lit = mk_literal(fn);
         }
         else 
-            lit = mk_literal(prop.m_conseq);            
+            lit = mk_literal(prop.m_conseq);
         ctx.mark_as_relevant(lit);
 
 #if 0
@@ -339,8 +348,8 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
 
         ctx.assign(lit, js);
 #endif
-        
-#if 1           
+
+#if 1
         m_lits.push_back(lit);
         ctx.mk_th_lemma(get_id(), m_lits);
 #endif
@@ -358,7 +367,7 @@ void theory_user_propagator::propagate() {
         return;
     TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n");
     force_push();
-    
+
     unsigned qhead = m_to_add_qhead;
     if (qhead < m_to_add.size()) {
         for (; qhead < m_to_add.size(); ++qhead)

src/smt/theory_user_propagator.h

@@ -83,7 +83,8 @@ namespace smt {
         expr_ref_vector        m_to_add;
         unsigned_vector        m_to_add_lim;
         unsigned               m_to_add_qhead = 0;
-        bool_var               m_next_split_var = null_bool_var;
+        expr*                  m_next_split_var = nullptr;
+        unsigned               m_next_split_idx = 0;
         lbool                  m_next_split_phase = l_undef;
 
         expr* var2expr(theory_var v) { return m_var2expr.get(v); }