move qhead to attribute on the state instead of the simplifier,

- add sat.smt option to enable the new incremental core (it is not ready for mainstream consumption as cloning and other features are not implemented and it hasn't been tested in any detail yet).
- move "name" into attribute on simplifier so it can be reused for diagnostics by the seq-simplifier.

src/ast/simplifiers/bit_blaster.cpp

@@ -37,7 +37,7 @@ void bit_blaster::reduce() {
     expr_ref   new_curr(m);
     proof_ref  new_pr(m);
     bool change = false;
-    for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) {
+    for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size(); idx++) {
         if (m_fmls.inconsistent())
             break;
         auto [curr, d] = m_fmls[idx]();
@@ -60,8 +60,6 @@ void bit_blaster::reduce() {
             m_fmls.model_trail().push(f, v, nullptr, {});
     }
     m_rewriter.cleanup();
-
-    advance_qhead();
 }
 
 

src/ast/simplifiers/bit_blaster.h

@@ -33,7 +33,7 @@ class bit_blaster : public dependent_expr_simplifier {
         m_rewriter(m, p) {
         updt_params(p);
     }
-
+    char const* name() const override { return "bit-blaster"; }
     void updt_params(params_ref const & p) override;
     void collect_param_descrs(param_descrs & r) override;
     void reduce() override;

src/ast/simplifiers/bv_slice.cpp

@@ -24,11 +24,10 @@ namespace bv {
     void slice::reduce() {
         process_eqs();
         apply_subst();
-        advance_qhead();
     }
 
     void slice::process_eqs() {
-        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+        for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) {
             auto const [f, d] = m_fmls[i]();
             process_eq(f);
         }  
@@ -137,7 +136,7 @@ namespace bv {
         expr_ref_vector cache(m), pin(m);
         ptr_vector<expr> todo, args;
         expr* c;
-        for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+        for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) {
             auto const [f, d] = m_fmls[i]();
             todo.push_back(f);
             pin.push_back(f);

src/ast/simplifiers/bv_slice.h

@@ -47,7 +47,7 @@ namespace bv {
     public:
 
         slice(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_bv(m), m_rewriter(m) {}
-
+        char const* name() const override { return "bv-slice"; }
         void push() override { dependent_expr_simplifier::push(); }
         void pop(unsigned n) override { dependent_expr_simplifier::pop(n); }
         void reduce() override;

src/ast/simplifiers/card2bv.cpp

@@ -29,7 +29,7 @@ void card2bv::reduce() {
 
     expr_ref new_f1(m), new_f2(m);
     proof_ref new_pr(m);
-    for (unsigned idx = m_qhead; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) {
+    for (unsigned idx = m_fmls.qhead(); !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) {
         auto [f, d] = m_fmls[idx]();
         rw1(f, new_f1);        
         rw2(false, new_f1, new_f2, new_pr);        
@@ -48,8 +48,6 @@ void card2bv::reduce() {
     func_decl_ref_vector const& fns = rw2.fresh_constants();
     for (func_decl* f : fns)
         m_fmls.model_trail().hide(f);    
-
-     advance_qhead();
 }
 
 void card2bv::collect_statistics(statistics& st) const {

src/ast/simplifiers/card2bv.h

@@ -34,6 +34,7 @@ class card2bv : public dependent_expr_simplifier {
 
 public:
     card2bv(ast_manager& m, params_ref const& p, dependent_expr_state& fmls);
+    char const* name() const override { return "card2bv"; }
     void reduce() override;
     void collect_statistics(statistics& st) const override;
     void reset_statistics() override { m_stats.reset(); }

src/ast/simplifiers/dependent_expr_state.h

@@ -41,6 +41,7 @@ Module Name:
    abstract interface to state updated by simplifiers.
  */
 class dependent_expr_state {
+    unsigned m_qhead = 0;
 public:
     virtual ~dependent_expr_state() {}
     virtual unsigned size() const = 0;
@@ -53,8 +54,15 @@ class dependent_expr_state {
     trail_stack    m_trail;
     void push() { m_trail.push_scope(); }
     void pop(unsigned n) { m_trail.pop_scope(n); }
-
-
+    unsigned qhead() const { return m_qhead; }
+    void advance_qhead() { m_qhead = size(); }
+    unsigned num_exprs() {
+        expr_fast_mark1 visited;
+        unsigned r = 0;
+        for (unsigned i = 0; i < size(); i++) 
+            r += get_num_exprs((*this)[i].fml(), visited);
+        return r;
+    }
 };
 
 /**
@@ -65,22 +73,22 @@ class dependent_expr_simplifier {
     ast_manager& m;
     dependent_expr_state& m_fmls;
     trail_stack& m_trail;
-    unsigned              m_qhead = 0;          // pointer into last processed formula in m_fmls
 
     unsigned num_scopes() const { return m_trail.get_num_scopes(); }
 
-    void advance_qhead() { if (num_scopes() > 0) m_trail.push(value_trail(m_qhead)); m_qhead = m_fmls.size(); }
 public:
     dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s), m_trail(s.m_trail) {}
     virtual ~dependent_expr_simplifier() {}
+    virtual char const* name() const = 0;
     virtual void push() { }
     virtual void pop(unsigned n) { }
     virtual void reduce() = 0;
     virtual void collect_statistics(statistics& st) const {}
     virtual void reset_statistics() {}
     virtual void updt_params(params_ref const& p) {}
     virtual void collect_param_descrs(param_descrs& r) {}
-    unsigned qhead() const { return m_qhead; }
+    ast_manager& get_manager() { return m; }
+    dependent_expr_state& get_fmls() { return m_fmls; }
 };
 
 /**

src/ast/simplifiers/elim_unconstrained.cpp

@@ -138,7 +138,7 @@ void elim_unconstrained::init_nodes() {
 
     // freeze subterms before the already processed head
     terms.reset();
-    for (unsigned i = 0; i < m_qhead; ++i)
+    for (unsigned i = 0; i < m_fmls.qhead(); ++i)
         terms.push_back(m_fmls[i].fml());
     for (expr* e : subterms::all(terms))
         m_frozen.mark(e, true);    
@@ -216,7 +216,7 @@ void elim_unconstrained::gc(expr* t) {
  */
 void elim_unconstrained::reconstruct_terms() {
     expr_ref_vector terms(m);
-    for (unsigned i = m_qhead; i < m_fmls.size(); ++i)
+    for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i)
         terms.push_back(m_fmls[i].fml());    
 
     for (expr* e : subterms_postorder::all(terms)) {
@@ -250,7 +250,7 @@ void elim_unconstrained::reconstruct_terms() {
 void elim_unconstrained::assert_normalized(vector<dependent_expr>& old_fmls) {
 
     unsigned sz = m_fmls.size();
-    for (unsigned i = m_qhead; i < sz; ++i) {
+    for (unsigned i = m_fmls.qhead(); i < sz; ++i) {
         auto [f, d] = m_fmls[i]();
         node& n = get_node(f);
         expr* g = n.m_term;
@@ -302,5 +302,4 @@ void elim_unconstrained::reduce() {
     vector<dependent_expr> old_fmls;
     assert_normalized(old_fmls);
     update_model_trail(*mc, old_fmls);
-    advance_qhead();
 }

src/ast/simplifiers/elim_unconstrained.h

@@ -71,6 +71,8 @@ class elim_unconstrained : public dependent_expr_simplifier {
 
     elim_unconstrained(ast_manager& m, dependent_expr_state& fmls);
 
+    char const* name() const override { return "elim-unconstrained"; }
+
     void reduce() override;
 
     void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); }

src/ast/simplifiers/eliminate_predicates.cpp

@@ -501,7 +501,7 @@ void eliminate_predicates::reduce_definitions() {
     for (auto const& [k, v] : m_macros) 
         macro_expander.insert(v->m_head, v->m_def, v->m_dep);
 
-    for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+    for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) {
         auto [f, d] = m_fmls[i]();
         expr_ref fml(f, m), new_fml(m);
         expr_dependency_ref dep(m);
@@ -779,7 +779,7 @@ eliminate_predicates::clause* eliminate_predicates::init_clause(expr* f, expr_de
 * eliminations.
 */
 void eliminate_predicates::init_clauses() {
-    for (unsigned i = 0; i < m_qhead; ++i)
+    for (unsigned i = 0; i < m_fmls.qhead(); ++i)
         m_to_exclude.push_back(m_fmls[i].fml());
     recfun::util rec(m);
     if (rec.has_rec_defs()) 
@@ -788,7 +788,7 @@ void eliminate_predicates::init_clauses() {
 
     process_to_exclude(m_disable_macro);
 
-    for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+    for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) {
         clause* cl = init_clause(i);
         add_use_list(*cl);
         m_clauses.push_back(cl);

src/ast/simplifiers/eliminate_predicates.h

@@ -129,6 +129,8 @@ class eliminate_predicates : public dependent_expr_simplifier {
     eliminate_predicates(ast_manager& m, dependent_expr_state& fmls);
 
     ~eliminate_predicates() override { reset(); }
+
+    char const* name() const override { return "elim-predicates"; }
 
     void reduce() override;
 

src/ast/simplifiers/euf_completion.cpp

@@ -80,7 +80,7 @@ namespace euf {
                 m_nodes_to_canonize.push_back(ch);
         };
 
-        for (unsigned i = m_qhead; i < sz; ++i) {
+        for (unsigned i = m_fmls.qhead(); i < sz; ++i) {
             expr* x, * y;
             auto [f, d] = m_fmls[i]();
             if (m.is_eq(f, x, y)) {
@@ -114,7 +114,7 @@ namespace euf {
         }
 
         unsigned sz = m_fmls.size();
-        for (unsigned i = m_qhead; i < sz; ++i) {
+        for (unsigned i = m_fmls.qhead(); i < sz; ++i) {
             auto [f, d] = m_fmls[i]();
 
             expr_dependency_ref dep(d, m);
@@ -127,8 +127,6 @@ namespace euf {
             }
             CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
         }
-        if (!m_has_new_eq)
-            advance_qhead();
     }
 
     bool completion::is_new_eq(expr* a, expr* b) {

src/ast/simplifiers/euf_completion.h

@@ -58,6 +58,7 @@ namespace euf {
         expr_dependency* explain_conflict();
     public:
         completion(ast_manager& m, dependent_expr_state& fmls);
+        char const* name() const override { return "euf-reduce"; }
         void push() override { m_egraph.push(); dependent_expr_simplifier::push(); }
         void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); }
         void reduce() override;

src/ast/simplifiers/max_bv_sharing.cpp

@@ -250,18 +250,19 @@ class max_bv_sharing : public dependent_expr_simplifier {
                  "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
     }
 
+    char const* name() const override { return "max-bv-sharing"; }
+
     void reduce() override {
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
-        for (unsigned idx = m_qhead; idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) {
+        for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) {
             auto [curr, d] = m_fmls[idx]();
             m_rw(curr, new_curr, new_pr);
             // Proof reconstruction: new_pr = m.mk_modus_ponens(old_pr, new_pr);
             m_num_steps += m_rw.get_num_steps();            
             m_fmls.update(idx, dependent_expr(m, new_curr, d));            
         }
         m_rw.cfg().cleanup();
-        advance_qhead();
     }        
 };
 

src/ast/simplifiers/propagate_values.cpp

@@ -78,26 +78,25 @@ void propagate_values::reduce() {
         subst.reset();
         m_rewriter.reset();
         m_rewriter.set_substitution(&subst);
-        for (unsigned i = 0; i < m_qhead; ++i)
+        for (unsigned i = 0; i < m_fmls.qhead(); ++i)
             add_sub(m_fmls[i]);
     };
 
     unsigned rw = m_stats.m_num_rewrites + 1;
     for (unsigned r = 0; r < m_max_rounds && rw != m_stats.m_num_rewrites; ++r) {            
         rw = m_stats.m_num_rewrites;
         init_sub();
-        for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i)
+        for (unsigned i = m_fmls.qhead(); i < m_fmls.size() && !m_fmls.inconsistent(); ++i)
             process_fml(i);
         init_sub();
-        for (unsigned i = m_fmls.size(); i-- > m_qhead && !m_fmls.inconsistent();)
+        for (unsigned i = m_fmls.size(); i-- > m_fmls.qhead() && !m_fmls.inconsistent();)
             process_fml(i);
         if (subst.empty())
             break;
     }
 
     m_rewriter.set_substitution(nullptr);        
     m_rewriter.reset();
-    advance_qhead();
 }
 
 void propagate_values::collect_statistics(statistics& st) const {

src/ast/simplifiers/propagate_values.h

@@ -37,6 +37,7 @@ class propagate_values : public dependent_expr_simplifier {
 
 public:
     propagate_values(ast_manager& m, params_ref const& p, dependent_expr_state& fmls);
+    char const* name() const override { return "propagate-values2"; }
     void reduce() override;
     void collect_statistics(statistics& st) const override;
     void reset_statistics() override { m_stats.reset(); }

src/ast/simplifiers/rewriter_simplifier.h

@@ -33,20 +33,21 @@ class rewriter_simplifier : public dependent_expr_simplifier {
         m_rewriter(m) {
         updt_params(p);
     }
+
+    char const* name() const override { return "simplifier"; }
 
     void reduce() override {
         m_num_steps = 0;
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
-        for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) {
+        for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size(); idx++) {
             if (m_fmls.inconsistent())
                 break;
             auto d = m_fmls[idx];
             m_rewriter(d.fml(), new_curr, new_pr);
             m_num_steps += m_rewriter.get_num_steps();
             m_fmls.update(idx, dependent_expr(m, new_curr, d.dep()));            
         }
-        advance_qhead();
     }
     void collect_statistics(statistics& st) const override { st.update("simplifier", m_num_steps); }
     void reset_statistics() override { m_num_steps = 0; }

src/ast/simplifiers/seq_simplifier.h

@@ -17,16 +17,46 @@ Module Name:
 
 #pragma once
 
+#include "util/stopwatch.h"
 #include "ast/simplifiers/dependent_expr_state.h"
 
 
 class seq_simplifier : public dependent_expr_simplifier {
     scoped_ptr_vector<dependent_expr_simplifier> m_simplifiers;
 
+    struct collect_stats {
+        stopwatch       m_watch;
+        double          m_start_memory = 0;
+        dependent_expr_simplifier& s;
+        collect_stats(dependent_expr_simplifier& s) : 
+            m_start_memory(static_cast<double>(memory::get_allocation_size()) / static_cast<double>(1024 * 1024)), 
+            s(s) {
+            m_watch.start();
+        }
+        ~collect_stats() {
+            m_watch.stop();
+            double end_memory = static_cast<double>(memory::get_allocation_size()) / static_cast<double>(1024 * 1024);
+            IF_VERBOSE(10,
+                statistics st;
+                verbose_stream() << "(" << s.name()
+                << " :num-exprs " << s.get_fmls().num_exprs()
+                << " :num-asts " << s.get_manager().get_num_asts()
+                << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
+                << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
+                << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
+                << ")" << "\n";
+            s.collect_statistics(st);
+            verbose_stream() << st);
+        }
+    };
+
 public:
+
     seq_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
         dependent_expr_simplifier(m, fmls) {
     }
+
+    char const* name() const override { return "and-then"; }
 
     void add_simplifier(dependent_expr_simplifier* s) {
         m_simplifiers.push_back(s);
@@ -36,9 +66,11 @@ class seq_simplifier : public dependent_expr_simplifier {
         for (auto* s : m_simplifiers) {
             if (m_fmls.inconsistent())
                 break;
+            if (!m.inc())
+                break;
+            collect_stats _cs(*s);
             s->reduce();
-        }
-        advance_qhead();        
+        }      
     }
 
     void collect_statistics(statistics& st) const override {