fix misc issues around #4661 introduced when adding lazy push/pop to …

…selected theories

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

src/smt/smt_theory.cpp

@@ -40,27 +40,23 @@ namespace smt {
     }
 
     bool theory::lazy_push() {
-        if (m_is_lazy) {
+        if (m_lazy)
             ++m_lazy_scopes;
-        }
-        return m_is_lazy;
+        return m_lazy;
     }
 
-    bool theory::lazy_pop(unsigned num_scopes) {
-        if (m_is_lazy) {
-            SASSERT(m_lazy_scopes >= num_scopes);
-            m_lazy_scopes -= num_scopes;
-        }
-        return m_is_lazy;
+    bool theory::lazy_pop(unsigned& num_scopes) {
+        unsigned n = std::min(num_scopes, m_lazy_scopes);
+        num_scopes -= n;
+        m_lazy_scopes -= n;
+        return num_scopes == 0;
     }
 
     void theory::force_push() {
-        if (m_is_lazy) {       
-            m_is_lazy = false;
-            for (unsigned i = m_lazy_scopes; i-- > 0; ) {
-                push_scope_eh();
-            }
-        } 
+        flet<bool> _lazy(m_lazy, false);
+        for (; m_lazy_scopes > 0; --m_lazy_scopes) {
+            push_scope_eh();
+        }
     }
 
     void theory::display_var2enode(std::ostream & out) const {
@@ -175,8 +171,8 @@ namespace smt {
         m_id(fid),
         ctx(ctx),
         m(ctx.get_manager()),
-        m_is_lazy(true),
-        m_lazy_scopes(0) {
+        m_lazy_scopes(0),
+        m_lazy(true) {
     }
 
     theory::~theory() {

src/smt/smt_theory.h

@@ -35,8 +35,8 @@ namespace smt {
         ast_manager &   m;
         enode_vector    m_var2enode;
         unsigned_vector m_var2enode_lim;
-        bool            m_is_lazy;
         unsigned        m_lazy_scopes;
+        bool            m_lazy;
 
         friend class context;
         friend class arith_value;
@@ -75,7 +75,7 @@ namespace smt {
         }
 
         bool lazy_push();
-        bool lazy_pop(unsigned num_scopes);
+        bool lazy_pop(unsigned& num_scopes);
         void force_push();
 
     public:

src/smt/theory_datatype.cpp

@@ -369,6 +369,7 @@ namespace smt {
     }
 
     void theory_datatype::apply_sort_cnstr(enode * n, sort * s) {
+        force_push();
         // Remark: If s is an infinite sort, then it is not necessary to create
         // a theory variable. 
         // 
@@ -397,6 +398,7 @@ namespace smt {
     }
 
     void theory_datatype::new_eq_eh(theory_var v1, theory_var v2) {
+        force_push();
         m_find.merge(v1, v2);
     }
 
@@ -409,6 +411,7 @@ namespace smt {
     }
 
     void theory_datatype::assign_eh(bool_var v, bool is_true) {
+        force_push();
         enode * n     = ctx.bool_var2enode(v);
         if (!is_recognizer(n))
             return;
@@ -441,6 +444,7 @@ namespace smt {
     }
 
     void theory_datatype::relevant_eh(app * n) {
+        force_push();
         TRACE("datatype", tout << "relevant_eh: " << mk_pp(n, m) << "\n";);
         SASSERT(ctx.relevancy());
         if (is_recognizer(n)) {
@@ -472,6 +476,7 @@ namespace smt {
     }
 
     final_check_status theory_datatype::final_check_eh() {
+        force_push();
         int num_vars = get_num_vars();
         final_check_status r = FC_DONE;
         final_check_st _guard(this); 

src/smt/theory_lra.cpp

@@ -4080,9 +4080,11 @@ bool theory_lra::internalize_term(app * term) {
     return m_imp->internalize_term(term);
 }
 void theory_lra::internalize_eq_eh(app * atom, bool_var v) {
+    force_push();
     m_imp->internalize_eq_eh(atom, v);
 }
 void theory_lra::assign_eh(bool_var v, bool is_true) {
+    force_push();
     m_imp->assign_eh(v, is_true);
 }
 lbool theory_lra::get_phase(bool_var v) {
@@ -4095,9 +4097,11 @@ bool theory_lra::use_diseqs() const {
     return m_imp->use_diseqs();
 }
 void theory_lra::new_diseq_eh(theory_var v1, theory_var v2) {
+    force_push();
     m_imp->new_diseq_eh(v1, v2);
 }
 void theory_lra::apply_sort_cnstr(enode* n, sort* s) {
+    force_push();
     m_imp->apply_sort_cnstr(n, s);
 }
 void theory_lra::push_scope_eh() {
@@ -4122,6 +4126,7 @@ void theory_lra::init_search_eh() {
     m_imp->init_search_eh();
 }
 final_check_status theory_lra::final_check_eh() {
+    force_push();
     return m_imp->final_check_eh();
 }
 bool theory_lra::is_shared(theory_var v) const {
@@ -4131,6 +4136,7 @@ bool theory_lra::can_propagate() {
     return m_imp->can_propagate();
 }
 void theory_lra::propagate() {
+    force_push();
     m_imp->propagate();
 }
 justification * theory_lra::why_is_diseq(theory_var v1, theory_var v2) {

src/smt/theory_seq.cpp

@@ -318,6 +318,7 @@ struct scoped_enable_trace {
 };
 
 final_check_status theory_seq::final_check_eh() {
+    force_push();
     if (!m_has_seq) {
         return FC_DONE;
     }
@@ -1620,6 +1621,7 @@ bool theory_seq::check_int_string(expr* e) {
 
 
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
+    force_push();
     mk_var(n);
 }
 
@@ -3146,6 +3148,7 @@ void theory_seq::restart_eh() {
 }
 
 void theory_seq::relevant_eh(app* n) {
+    force_push();
     if (m_util.str.is_index(n)   ||
         m_util.str.is_replace(n) ||
         m_util.str.is_extract(n) ||