build fixes, add lazy push/pop state to avoid overhead on unused theories

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

src/smt/smt_context.h

@@ -893,7 +893,7 @@ namespace smt {
 
         void mk_clause(literal l1, literal l2, literal l3, justification * j);
 
-        void context::mk_th_clause(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params, clause_kind k);
+        void mk_th_clause(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params, clause_kind k);
 
         void mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) {
             mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_AXIOM);

src/smt/smt_theory.cpp

@@ -39,6 +39,30 @@ namespace smt {
         m_var2enode_lim.shrink(new_lvl);
     }
 
+    bool theory::lazy_push() {
+        if (m_is_lazy) {
+            ++m_lazy_scopes;
+        }
+        return m_is_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;
+    }
+
+    void theory::force_push() {
+        if (m_is_lazy) {       
+            m_is_lazy = false;
+            for (unsigned i = m_lazy_scopes; i-- > 0; ) {
+                push_scope_eh();
+            }
+        } 
+    }
+
     void theory::display_var2enode(std::ostream & out) const {
         unsigned sz = m_var2enode.size();
         for (unsigned v = 0; v < sz; v++) {
@@ -138,7 +162,9 @@ namespace smt {
     theory::theory(context& ctx, family_id fid):
         m_id(fid),
         ctx(ctx),
-        m(ctx.get_manager()) {
+        m(ctx.get_manager()),
+        m_is_lazy(true),
+        m_lazy_scopes(0) {
     }
 
     theory::~theory() {

src/smt/smt_theory.h

@@ -35,6 +35,8 @@ namespace smt {
         ast_manager &   m;
         enode_vector    m_var2enode;
         unsigned_vector m_var2enode_lim;
+        bool            m_is_lazy;
+        unsigned        m_lazy_scopes;
 
         friend class context;
         friend class arith_value;
@@ -72,6 +74,9 @@ namespace smt {
             return n->get_th_var(get_id());
         }
 
+        bool lazy_push();
+        bool lazy_pop(unsigned num_scopes);
+        void force_push();
         
     public:
         /**

src/smt/theory_datatype.cpp

@@ -293,6 +293,7 @@ namespace smt {
     }
 
     bool theory_datatype::internalize_term(app * term) {
+        force_push();
         TRACE("datatype", tout << "internalizing term:\n" << mk_pp(term, m) << "\n";);
         unsigned num_args = term->get_num_args();
         for (unsigned i = 0; i < num_args; i++)
@@ -452,11 +453,15 @@ namespace smt {
     }
 
     void theory_datatype::push_scope_eh() {
+        if (lazy_push())
+            return;
         theory::push_scope_eh();
         m_trail_stack.push_scope();
     }
 
     void theory_datatype::pop_scope_eh(unsigned num_scopes) {
+        if (lazy_pop(num_scopes))
+            return;
         m_trail_stack.pop_scope(num_scopes);
         unsigned num_old_vars = get_old_num_vars(num_scopes);
         std::for_each(m_var_data.begin() + num_old_vars, m_var_data.end(), delete_proc<var_data>());

src/smt/theory_fpa.cpp

@@ -409,6 +409,7 @@ namespace smt {
     }
 
     bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
+        force_push();
         TRACE("t_fpa_internalize", tout << "internalizing atom: " << mk_ismt2_pp(atom, m) << std::endl;);
         SASSERT(atom->get_family_id() == get_family_id());
 
@@ -430,6 +431,7 @@ namespace smt {
     }
 
     bool theory_fpa::internalize_term(app * term) {
+        force_push();
         TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, m) << "\n";);
         SASSERT(term->get_family_id() == get_family_id());
         SASSERT(!ctx.e_internalized(term));
@@ -584,11 +586,15 @@ namespace smt {
     }
 
     void theory_fpa::push_scope_eh() {
+        if (lazy_push())
+            return;
         theory::push_scope_eh();
         m_trail_stack.push_scope();
     }
 
     void theory_fpa::pop_scope_eh(unsigned num_scopes) {
+        if (lazy_pop(num_scopes))
+            return;
         m_trail_stack.pop_scope(num_scopes);
         TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";);
         theory::pop_scope_eh(num_scopes);

src/smt/theory_lra.cpp

@@ -4072,9 +4072,11 @@ void theory_lra::init() {
     m_imp->init();
 }    
 bool theory_lra::internalize_atom(app * atom, bool gate_ctx) {
+    force_push();
     return m_imp->internalize_atom(atom, gate_ctx);
 }
 bool theory_lra::internalize_term(app * term) {
+    force_push();
     return m_imp->internalize_term(term);
 }
 void theory_lra::internalize_eq_eh(app * atom, bool_var v) {
@@ -4099,10 +4101,14 @@ void theory_lra::apply_sort_cnstr(enode* n, sort* s) {
     m_imp->apply_sort_cnstr(n, s);
 }
 void theory_lra::push_scope_eh() {
+    if (lazy_push())
+        return;
     theory::push_scope_eh();
     m_imp->push_scope_eh();
 }
 void theory_lra::pop_scope_eh(unsigned num_scopes) {
+    if (lazy_pop(num_scopes))
+        return;
     m_imp->pop_scope_eh(num_scopes);
     theory::pop_scope_eh(num_scopes);
 }

src/smt/theory_recfun.cpp

@@ -54,6 +54,7 @@ namespace smt {
     }
 
     bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
+        force_push();
         TRACEFN(mk_pp(atom, m));
         if (!u().has_defs()) {
             return false;
@@ -75,6 +76,7 @@ namespace smt {
     }
 
     bool theory_recfun::internalize_term(app * term) {
+        force_push();
         if (!u().has_defs()) {
             return false;
         }
@@ -131,11 +133,15 @@ namespace smt {
     }
 
     void theory_recfun::push_scope_eh() {
+        if (lazy_push())
+            return;
         theory::push_scope_eh();
         m_preds_lim.push_back(m_preds.size());
     }
 
     void theory_recfun::pop_scope_eh(unsigned num_scopes) {
+        if (lazy_pop(num_scopes))
+            return;
         theory::pop_scope_eh(num_scopes);
         reset_queues();
         

src/smt/theory_seq.cpp

@@ -1492,6 +1492,7 @@ bool theory_seq::internalize_atom(app* a, bool) {
 }
 
 bool theory_seq::internalize_term(app* term) {
+    force_push();
     m_has_seq = true;
     if (ctx.e_internalized(term)) {
         enode* e = ctx.get_enode(term);
@@ -3109,6 +3110,8 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
 }
 
 void theory_seq::push_scope_eh() {
+    if (lazy_push()) 
+        return;
     theory::push_scope_eh();
     m_rep.push_scope();
     m_exclude.push_scope();
@@ -3123,6 +3126,8 @@ void theory_seq::push_scope_eh() {
 }
 
 void theory_seq::pop_scope_eh(unsigned num_scopes) {
+    if (lazy_pop(num_scopes))
+        return;
     m_trail_stack.pop_scope(num_scopes);
     theory::pop_scope_eh(num_scopes);
     m_dm.pop_scope(num_scopes);