use lazy scopes to avoid push/pop overhead

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

src/smt/asserted_formulas.cpp

@@ -58,7 +58,8 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re
     m_propagate_values(*this),
     m_nnf_cnf(*this),
     m_apply_quasi_macros(*this),
-    m_flatten_clauses(*this) {
+    m_flatten_clauses(*this),
+    m_lazy_scopes(0) {
 
     m_macro_finder = alloc(macro_finder, m, m_macro_manager);
 
@@ -146,6 +147,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
 
 
 void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
+    force_push();
     proof_ref  in_pr(_in_pr, m), pr(_in_pr, m);
     expr_ref   r(e, m);
 
@@ -180,6 +182,10 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
 }
 
 void asserted_formulas::push_scope() {
+    ++m_lazy_scopes;
+}
+
+void asserted_formulas::push_scope_core() {
     reduce();
     commit();
     SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
@@ -198,7 +204,19 @@ void asserted_formulas::push_scope() {
     TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";);
 }
 
+void asserted_formulas::force_push() {
+    for (; m_lazy_scopes > 0; --m_lazy_scopes)
+        push_scope_core();
+}
+
 void asserted_formulas::pop_scope(unsigned num_scopes) {
+    if (m_lazy_scopes > 0) {
+        unsigned n = std::min(num_scopes, m_lazy_scopes);
+        m_lazy_scopes -= n;
+        num_scopes -= n;
+        if (num_scopes == 0)
+            return;
+    }
     TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
     m_bv_sharing.pop_scope(num_scopes);
     m_macro_manager.pop_scope(num_scopes);

src/smt/asserted_formulas.h

@@ -207,6 +207,10 @@ class asserted_formulas {
     nnf_cnf_fn                  m_nnf_cnf;
     apply_quasi_macros_fn       m_apply_quasi_macros;
     flatten_clauses_fn          m_flatten_clauses;
+    unsigned                    m_lazy_scopes;
+
+    void force_push();
+    void push_scope_core();
 
     bool invoke(simplify_fmls& s);
     void swap_asserted_formulas(vector<justified_expr>& new_fmls);
@@ -274,8 +278,8 @@ public:
     func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_macro_manager.get_macro_interpretation(i, interp); }
     quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); }
     // auxiliary function used to create a logic context based on a model.
-    void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); }
-    void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency* dep) { m_macro_manager.insert(f, m, pr, dep); }
+    void insert_macro(func_decl * f, quantifier * m, proof * pr) { force_push(); m_macro_manager.insert(f, m, pr); }
+    void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency* dep) { force_push(); m_macro_manager.insert(f, m, pr, dep); }
 
 };
 

src/smt/smt_quantifier.cpp

@@ -426,6 +426,8 @@ namespace smt {
     quantifier_manager::quantifier_manager(context & ctx, smt_params & fp, params_ref const & p) {
         m_imp = alloc(imp, *this, ctx, fp, mk_default_plugin());
         m_imp->m_plugin->set_manager(*this);
+        m_lazy_scopes = 0;
+        m_lazy = true;
         
     }
 
@@ -438,6 +440,10 @@ namespace smt {
     }
 
     void quantifier_manager::add(quantifier * q, unsigned generation) {
+        if (m_lazy) {
+            while (m_lazy_scopes-- > 0) m_imp->push();
+            m_lazy = false;
+        }
         m_imp->add(q, generation);
     }
 
@@ -529,12 +535,18 @@ namespace smt {
         return m_imp->check_model(m, root2value);
     }
 
-    void quantifier_manager::push() {
-        m_imp->push();
+    void quantifier_manager::push() {        
+        if (m_lazy) 
+            ++m_lazy_scopes;
+        else 
+            m_imp->push();
     }
 
     void quantifier_manager::pop(unsigned num_scopes) {
-        m_imp->pop(num_scopes);
+        if (m_lazy)
+            m_lazy_scopes -= num_scopes;
+        else
+            m_imp->pop(num_scopes);
     }
 
     void quantifier_manager::reset() {
@@ -711,7 +723,7 @@ namespace smt {
         }
 
         bool can_propagate() const override {
-            return m_mam->has_work();
+            return m_active && m_mam->has_work();
         }
 
         void restart_eh() override {
@@ -733,6 +745,8 @@ namespace smt {
         }
 
         void propagate() override {
+            if (!m_active)
+                return;
             m_mam->match();
             if (!m_context->relevancy() && use_ematching()) {
                 ptr_vector<enode>::const_iterator it  = m_context->begin_enodes();

src/smt/smt_quantifier.h

@@ -34,6 +34,9 @@ namespace smt {
     class quantifier_manager {
         struct imp;
         imp *                       m_imp;
+        unsigned                    m_lazy_scopes;
+        bool                        m_lazy;
+        void flush();
     public:
         quantifier_manager(context & ctx, smt_params & fp, params_ref const & p);
         ~quantifier_manager();

src/util/rlimit.cpp

@@ -35,7 +35,7 @@ reslimit::reslimit():
     m_cancel(0),
     m_suspend(false),
     m_count(0),
-    m_limit(0) {
+    m_limit(std::numeric_limits<uint64_t>::max()) {
 }
 
 uint64_t reslimit::count() const {
@@ -55,15 +55,15 @@ bool reslimit::inc(unsigned offset) {
 void reslimit::push(unsigned delta_limit) {
     uint64_t new_limit = delta_limit + m_count;
     if (new_limit <= m_count) {
-        new_limit = 0;
+        new_limit = std::numeric_limits<uint64_t>::max();
     }
     m_limits.push_back(m_limit);
-    m_limit = m_limit==0 ? new_limit : std::min(new_limit, m_limit);
+    m_limit = std::min(new_limit, m_limit);
     m_cancel = 0;
 }
 
 void reslimit::pop() {
-    if (m_count > m_limit && m_limit > 0) {
+    if (m_count > m_limit) {
         m_count = m_limit;
     }
     m_limit = m_limits.back();

src/util/rlimit.h

@@ -50,7 +50,7 @@ public:
     uint64_t count() const;
 
     bool suspended() const { return m_suspend;  }
-    inline bool not_canceled() const { return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; }
+    inline bool not_canceled() const { return (m_cancel == 0 && m_count <= m_limit) || m_suspend; }
     inline bool is_canceled() const { return !not_canceled(); }
     char const* get_cancel_msg() const;
     void cancel();