wip - dependent expr simpliifer

- simplify iterator over current indices
- add more simplifiers used by asserted_formulas
- improve diagnostics printing

src/ast/rewriter/macro_replacer.cpp

@@ -125,9 +125,28 @@ void macro_replacer::insert(app* head, expr* def, expr_dependency* dep) {
     m_map.insert(f, std::tuple(head, def, dep));
 }
 
-void macro_replacer::operator()(expr* t, expr_ref& result, expr_dependency_ref& dep) {
+void macro_replacer::operator()(expr* t, expr_dependency* dep_in, expr_ref& result, expr_dependency_ref& dep_out) {
-    macro_replacer_rw exp(m, *this, dep);
+    expr_dependency_ref _dep_in(dep_in, m);
+    macro_replacer_rw exp(m, *this, dep_out);
     exp(t, result);
+    if (!dep_in)
+        return;
+    // update dependencies if needed
+    m_dep_exprs.reset();
+    m.linearize(dep_in, m_dep_exprs);
+    unsigned sz = m_trail.size();
+    for (expr*& d : m_dep_exprs) {
+        exp(d, result);
+        if (result != d) {
+            d = result.get();
+            m_trail.push_back(result);
+        }
+    }
+    if (sz != m_trail.size()) {
+        dep_in = m.mk_join(m_dep_exprs.size(), m_dep_exprs.data());
+        m_trail.shrink(sz);
+    }
+    dep_out = m.mk_join(dep_in, dep_out);
 }
 
 bool macro_replacer::has_macro(func_decl* f, app_ref& head, expr_ref& def, expr_dependency_ref& dep) {

src/ast/rewriter/macro_replacer.h

@@ -26,6 +26,7 @@ class macro_replacer {
     ast_manager& m;
     ast_ref_vector m_trail;
     expr_dependency_ref_vector m_deps;
+    ptr_vector<expr> m_dep_exprs;
     obj_map<func_decl, std::tuple<app*, expr*, expr_dependency*>> m_map;
     struct macro_replacer_cfg;
     struct macro_replacer_rw;
@@ -35,8 +36,8 @@ public:
     macro_replacer(ast_manager& m): m(m), m_trail(m), m_deps(m) {}
 
     void insert(app* head, expr* def, expr_dependency* dep);
-    void operator()(expr* t, expr_ref& result, expr_dependency_ref& dep);
+    void operator()(expr* t, expr_dependency* d, expr_ref& result, expr_dependency_ref& dep);
-    void operator()(expr* t, expr_ref & result) { expr_dependency_ref dep(m); (*this)(t, result, dep); }
+    void operator()(expr* t, expr_ref & result) { expr_dependency_ref dep(m); (*this)(t, nullptr, result, dep); }
     void operator()(expr_ref & t) { expr_ref s(t, m); (*this)(s, t); }
 
     bool has_macro(func_decl* f, app_ref& head, expr_ref& def, expr_dependency_ref& d);

src/ast/simplifiers/CMakeLists.txt

@@ -17,4 +17,5 @@ z3_add_component(simplifiers
     euf
     rewriter
     bit_blaster
+    normal_forms
 )

src/ast/simplifiers/bit2int.h

@@ -0,0 +1,44 @@
+
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bit2int.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/bit2int.h"
+
+
+class bit2int_simplifier : public dependent_expr_simplifier {
+    bit2int m_rewriter;
+    
+public:
+    bit2int_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls),
+        m_rewriter(m) {
+    }
+
+    char const* name() const override { return "bit2int"; }
+        
+    void reduce() override {
+        expr_ref r(m);
+        proof_ref pr(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            if (!has_quantifiers(d.fml()))
+                continue;
+            m_rewriter(d.fml(), r, pr);
+            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+        }
+    }
+};
+

src/ast/simplifiers/bv_elim.h

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    bv_elim.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/bv_elim.h"
+
+
+namespace bv {
+class elim_simplifier : public dependent_expr_simplifier {
+    bv_elim_rw m_rewriter;
+    
+public:
+    elim_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls),
+        m_rewriter(m) {
+    }
+
+    char const* name() const override { return "bv-elim"; }
+        
+    void reduce() override {
+        expr_ref r(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            if (!has_quantifiers(d.fml()))
+                continue;
+            m_rewriter(d.fml(), r);
+            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+        }
+    }
+};
+}

src/ast/simplifiers/dependent_expr.h

@@ -18,6 +18,7 @@ Author:
 #pragma once
 
 #include "ast/ast.h"
+#include "ast/ast_pp.h"
 #include "ast/ast_translation.h"
 
 class dependent_expr {
@@ -88,4 +89,20 @@ public:
     std::tuple<expr*, expr_dependency*> operator()() const { 
         return { m_fml, m_dep }; 
     }
+
+    std::ostream& display(std::ostream& out) const {
+        return out << mk_pp(m_fml, m);
+        if (m_dep) {
+            out << "\n <- ";
+            ptr_vector<expr> deps;            
+            m.linearize(m_dep, deps);
+            for (expr* arg : deps)
+                out << mk_pp(arg, m) << " ";
+        }
+        return out;
+    }
 };
+
+inline std::ostream& operator<<(std::ostream& out, dependent_expr const& d) {
+    return d.display(out);
+}

src/ast/simplifiers/dependent_expr_state.cpp

@@ -24,7 +24,7 @@ unsigned dependent_expr_state::num_exprs() {
 }
 
 void dependent_expr_state::freeze(func_decl* f) {
-    if (m_frozen.is_marked(f))
+    if (m_frozen.is_marked(f) || !is_uninterp(f))
         return;
     m_frozen_trail.push_back(f);
     m_frozen.mark(f, true);
@@ -107,3 +107,13 @@ void dependent_expr_state::freeze_suffix() {
         freeze_terms(d.fml(), true, visited);
     }
 }
+
+bool dependent_expr_state::has_quantifiers() {
+    if (m_has_quantifiers != l_undef)
+        return m_has_quantifiers == l_true;
+    bool found = false;
+    for (unsigned i = qhead(); i < qtail(); ++i) 
+        found |= ::has_quantifiers((*this)[i].fml());
+    m_has_quantifiers = found ? l_true : l_false;
+    return m_has_quantifiers == l_true;
+}

src/ast/simplifiers/dependent_expr_state.h

@@ -44,6 +44,7 @@ class dependent_expr_state {
     unsigned m_qhead = 0;
     bool     m_suffix_frozen = false;
     bool     m_recfun_frozen = false;
+    lbool    m_has_quantifiers = l_undef;
     ast_mark m_frozen;
     func_decl_ref_vector m_frozen_trail;
     void freeze_prefix();
@@ -81,7 +82,7 @@ public:
     }
     void pop(unsigned n) { m_trail.pop_scope(n);  }
     
-    void advance_qhead() { freeze_prefix(); m_suffix_frozen = false; m_qhead = qtail(); }
+    void advance_qhead() { freeze_prefix(); m_suffix_frozen = false; m_has_quantifiers = l_undef;  m_qhead = qtail(); }
     unsigned num_exprs();
 
     /**
@@ -90,8 +91,16 @@ public:
     bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
     bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); }
     void freeze_suffix();
+
+    virtual std::ostream& display(std::ostream& out) const { return out; }
+
+    bool has_quantifiers();
 };
 
+inline std::ostream& operator<<(std::ostream& out, dependent_expr_state& st) {
+    return st.display(out);
+}
+
 /**
    Shared interface of simplifiers. 
  */
@@ -105,6 +114,26 @@ protected:
 
     unsigned qhead() const { return m_fmls.qhead(); }
     unsigned qtail() const { return m_fmls.qtail(); }
+    struct iterator {
+        dependent_expr_simplifier& s;
+        unsigned m_index = 0;
+        bool at_end = false;
+        unsigned index() const { return at_end ? s.qtail() : m_index; }
+        iterator(dependent_expr_simplifier& s, unsigned i) : s(s), m_index(i), at_end(i == s.qtail()) {}
+        bool operator==(iterator const& other) const { return index() == other.index(); }
+        bool operator!=(iterator const& other) const { return !(*this == other); }
+        iterator& operator++() { if (!s.m.inc() || s.m_fmls.inconsistent()) at_end = true; else ++m_index; return *this; }
+        unsigned operator*() const { return m_index; }
+    };
+
+    struct index_set {
+        dependent_expr_simplifier& s;
+        iterator begin() { return iterator(s, s.qhead()); }
+        iterator end() { return iterator(s, s.qtail()); }
+        index_set(dependent_expr_simplifier& s) : s(s) {}
+    };
+
+    index_set indices() { return index_set(*this); }
 
 public:
     dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s), m_trail(s.m_trail) {}

src/ast/simplifiers/distribute_forall.h

@@ -0,0 +1,45 @@
+
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    distribute_forall.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/distribute_forall.h"
+
+
+class distribute_forall_simplifier : public dependent_expr_simplifier {
+    distribute_forall m_dist;
+    
+public:
+    distribute_forall_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls),
+        m_dist(m) {
+    }
+
+    char const* name() const override { return "distribute-forall"; }
+        
+    void reduce() override {
+        if (!m_fmls.has_quantifiers())
+            return;
+        expr_ref r(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            if (!has_quantifiers(d.fml()))
+                continue;
+            m_dist(d.fml(), r);
+            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+        }
+    }
+};
+

src/ast/simplifiers/elim_bounds.h

@@ -0,0 +1,45 @@
+
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    elim_bounds.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/elim_bounds.h"
+
+
+class elim_bounds_simplifier : public dependent_expr_simplifier {
+    elim_bounds_rw m_rewriter;
+    
+public:
+    elim_bounds_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls),
+        m_rewriter(m) {
+    }
+
+    char const* name() const override { return "cheap-fourier-motzkin"; }
+        
+    void reduce() override {
+        if (!m_fmls.has_quantifiers())
+            return;
+        expr_ref r(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            if (!has_quantifiers(d.fml()))
+                continue;
+            m_rewriter(d.fml(), r);
+            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+        }
+    }
+};
+

src/ast/simplifiers/eliminate_predicates.cpp

@@ -129,6 +129,38 @@ bool eliminate_predicates::can_be_macro_head(expr* _head, unsigned num_bound) {
     return true;
 }
 
+/**
+ * a quasi macro head is of the form 
+ * f(x,x)   where x is the only bound variable
+ * f(x,y,x+y+3,1) where x, y are the only bound variables
+ */
+
+bool eliminate_predicates::can_be_quasi_macro_head(expr* head, unsigned num_bound) {
+    if (!is_app(_head))
+        return false;
+    app* head = to_app(_head);
+    func_decl* f = head->get_decl();
+    if (m_fmls.frozen(f))
+        return false;
+    if (m_is_macro.is_marked(f))
+        return false;
+    if (f->is_associative())
+        return false;
+    uint_set indices;
+    for (expr* arg : *head) {
+        if (!is_var(arg))
+            return continue;
+        unsigned idx = to_var(arg)->get_idx();
+        if (indices.contains(idx))
+            return continue;
+        if (idx >= num_bound)
+            return false;
+        indices.insert(idx);
+    }
+    return indices.size() == num_bound;
+}
+
+
 expr_ref eliminate_predicates::bind_free_variables_in_def(clause& cl, app* head, expr* def) {
     unsigned num_bound = cl.m_bound.size();
     if (head->get_num_args() == num_bound)
@@ -365,7 +397,6 @@ void eliminate_predicates::try_find_macro(clause& cl) {
     // (= (+ (f x) s) t) 
     // becomes (= (f x) (- t s))
     //
-    // TBD:
     // (= (+ (* -1 (f x)) x) t)
     // becomes (= (f x) (- (- t s)))
 
@@ -473,10 +504,13 @@ void eliminate_predicates::try_find_macro(clause& cl) {
     // becomes (= (f x) (- t s (k x))
     // add (>= (k x) 0)
     // why is this a real improvement?
-    // 
+    //
+    
+    //
     // To review: quasi-macros
-    // (= (f x y (+ x y)) s), where x y are all bound variables.
+    // (= (f x y (+ x y)) s), where x y are all bound variables.    
-    // then ...?
+    // then replace (f x y z) by (if (= z (+ x y)) s (f' x y))
+    //
 }
 
 
@@ -501,21 +535,18 @@ 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 = qhead(); i < qtail(); ++i) {
+    for (unsigned i : indices()) {
         auto [f, d] = m_fmls[i]();
         expr_ref fml(f, m), new_fml(m);
-        expr_dependency_ref dep(m);
+        expr_dependency_ref dep(d, m);
         while (true) {
-            macro_expander(fml, new_fml, dep);
+            macro_expander(fml, dep, new_fml, dep);
             if (new_fml == fml)
                 break;
             rewrite(new_fml);
             fml = new_fml;
         }
-        if (fml != f) {
+        m_fmls.update(i, dependent_expr(m, fml, dep));
-            dep = m.mk_join(d, dep);
-            m_fmls.update(i, dependent_expr(m, fml, dep));
-        }
     }
     reset();
     init_clauses();
@@ -772,7 +803,7 @@ void eliminate_predicates::init_clauses() {
 
     m_fmls.freeze_suffix();
 
-    for (unsigned i = qhead(); i < qtail(); ++i) {
+    for (unsigned i : indices()) {
         clause* cl = init_clause(i);
         add_use_list(*cl);
         m_clauses.push_back(cl);
@@ -816,6 +847,8 @@ void eliminate_predicates::reset() {
 
 
 void eliminate_predicates::reduce() {
+    if (!m_fmls.has_quantifiers())
+        return;
     reset();
     init_clauses();
     find_definitions();

src/ast/simplifiers/eliminate_predicates.h

@@ -109,6 +109,7 @@ private:
     void insert_macro(app* head, expr* def, expr_dependency* dep);
     expr_ref bind_free_variables_in_def(clause& cl, app* head, expr* def);
     bool can_be_macro_head(expr* head, unsigned num_bound);
+    bool can_be_quasi_macro_head(expr* head, unsigned num_bound);
     bool is_macro_safe(expr* e);
     void try_find_macro(clause& cl);
 
@@ -145,4 +146,4 @@ public:
 
 inline std::ostream& operator<<(std::ostream& out, eliminate_predicates::clause const& c) {
     return c.display(out);
-}
+}

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -68,8 +68,9 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
                 auto [f, dep1] = st[i]();
                 expr_ref g(m);
                 expr_dependency_ref dep2(m);
-                mrp(f, g, dep2);
+                mrp(f, dep1, g, dep2);
-                st.update(i, dependent_expr(m, g, m.mk_join(dep1, dep2)));
+                CTRACE("simplifier", f != g, tout << "updated " << mk_pp(g, m) << "\n");
+                st.update(i, dependent_expr(m, g, dep2));
             }
             continue;
         }
@@ -77,10 +78,28 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
         rp->set_substitution(t->m_subst.get());
         // rigid entries:
         // apply substitution to added in case of rigid model convertions
+        ptr_vector<expr> dep_exprs;
+        expr_ref_vector trail(m);
         for (unsigned i = qhead; i < st.qtail(); ++i) {
             auto [f, dep1] = st[i]();
             auto [g, dep2] = rp->replace_with_dep(f);
+            if (dep1) {
+                dep_exprs.reset();
+                trail.reset();
+                m.linearize(dep1, dep_exprs);                
+                for (auto*& d : dep_exprs) {
+                    auto [h, dep3] = rp->replace_with_dep(d);
+                    if (h != d) {
+                        trail.push_back(h);
+                        d = h;
+                        dep2 = m.mk_join(dep2, dep3);
+                    }
+                }
+                if (!trail.empty()) 
+                    dep1 = m.mk_join(dep_exprs.size(), dep_exprs.data());                
+            }
             dependent_expr d(m, g, m.mk_join(dep1, dep2));
+            CTRACE("simplifier", f != g, tout << "updated " << mk_pp(g, m) << "\n");
             add_vars(d, free_vars);
             st.update(i, d);
         }    
@@ -121,3 +140,19 @@ void model_reconstruction_trail::append(generic_model_converter& mc) {
     m_trail_stack.push(value_trail(m_trail_index));
     append(mc, m_trail_index);
 }
+
+std::ostream& model_reconstruction_trail::display(std::ostream& out) const {
+    for (auto* t : m_trail) {
+        if (!t->m_active)
+            continue;
+        else if (t->is_hide())
+            out << "hide " << t->m_decl->get_name() << "\n";
+        else if (t->is_def())
+            out << t->m_decl->get_name() << " <- " << mk_pp(t->m_def, m) << "\n";
+        else {
+            for (auto const& [v, def] : t->m_subst->sub())
+                out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n";
+        }
+    }
+    return out;
+}

src/ast/simplifiers/model_reconstruction_trail.h

@@ -138,5 +138,7 @@ public:
     * Append new updates to model converter, update m_trail_index in the process.
     */
     void append(generic_model_converter& mc);
+
+    std::ostream& display(std::ostream& out) const;
 };
 

src/ast/simplifiers/propagate_values.cpp

@@ -83,13 +83,13 @@ void propagate_values::reduce() {
     };
     
     unsigned rw = m_stats.m_num_rewrites + 1;
-    for (unsigned r = 0; r < m_max_rounds && rw != m_stats.m_num_rewrites; ++r) {            
+    for (unsigned r = 0; r < m_max_rounds && m.inc() && rw != m_stats.m_num_rewrites; ++r) {            
         rw = m_stats.m_num_rewrites;
         init_sub();
-        for (unsigned i = qhead(); i < qtail() && !m_fmls.inconsistent(); ++i)
+        for (unsigned i = qhead(); i < qtail() && m.inc() && !m_fmls.inconsistent(); ++i)
             process_fml(i);
         init_sub();
-        for (unsigned i = qtail(); i-- > qhead() && !m_fmls.inconsistent();)
+        for (unsigned i = qtail(); i-- > qhead() && m.inc() && !m_fmls.inconsistent();)
             process_fml(i);
         if (subst.empty())
             break;

src/ast/simplifiers/pull_nested_quantifiers.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    pull_nested_quantifiers.h
+
+Abstract:
+
+    pull nested quantifiers
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/normal_forms/pull_quant.h"
+
+
+class pull_nested_quantifiers_simplifier : public dependent_expr_simplifier {
+    pull_nested_quant      m_pull;
+
+public:
+    pull_nested_quantifiers_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls),
+        m_pull(m) {
+    }
+
+    char const* name() const override { return "pull-nested-quantifiers"; }
+        
+    void reduce() override {
+        if (!m_fmls.has_quantifiers())
+            return;
+        expr_ref   new_curr(m);
+        proof_ref  new_pr(m);
+        for (unsigned idx : indices()) {
+            auto d = m_fmls[idx];
+            m_pull(d.fml(), new_curr, new_pr);
+            m_fmls.update(idx, dependent_expr(m, new_curr, d.dep()));
+        }
+    }
+};

src/ast/simplifiers/refine_inj_axiom.h

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    refine_inj_axiom.h
+
+Abstract:
+
+    refine injectivity axiom
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/inj_axiom.h"
+
+
+
+class refine_inj_axiom_simplifier : public dependent_expr_simplifier {
+
+public:
+    refine_inj_axiom_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls) {
+    }
+
+    char const* name() const override { return "refine-injectivity"; }
+        
+    void reduce() override {
+        if (!m_fmls.has_quantifiers())
+            return;
+        expr_ref r(m);
+        for (unsigned idx : indices()) {
+            expr* f = m_fmls[idx].fml();
+            if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), r)) 
+                m_fmls.update(idx, dependent_expr(m, r, m_fmls[idx].dep()));            
+        }
+    }
+};

src/ast/simplifiers/rewriter_simplifier.h

@@ -40,16 +40,14 @@ public:
         m_num_steps = 0;
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
-        for (unsigned idx = qhead(); idx < qtail(); idx++) {
+        for (unsigned idx : indices()) {
-            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()));            
         }
     }
-    void collect_statistics(statistics& st) const override { st.update("simplifier", m_num_steps); }
+    void collect_statistics(statistics& st) const override { st.update("simplifier-steps", m_num_steps); }
     void reset_statistics() override { m_num_steps = 0; }
     void updt_params(params_ref const& p) override { m_params.append(p); m_rewriter.updt_params(m_params); }
     void collect_param_descrs(param_descrs& r) override { th_rewriter::get_param_descrs(r); }

src/ast/simplifiers/seq_simplifier.h

@@ -46,7 +46,8 @@ class seq_simplifier : public dependent_expr_simplifier {
                 << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
                 << ")" << "\n";
             s.collect_statistics(st);
-            verbose_stream() << st);
+            if (st.size() > 0)
+                st.display_smt2(verbose_stream()));
         }
     };
 
@@ -63,14 +64,17 @@ public:
     }
         
     void reduce() override {
+        TRACE("simplifier", tout << m_fmls << "\n");
         for (auto* s : m_simplifiers) {
             if (m_fmls.inconsistent())
                 break;
             if (!m.inc())
                 break;
+            s->reset_statistics();
             collect_stats _cs(*s);
             s->reduce();
             m_fmls.flatten_suffix();
+            TRACE("simplifier", tout << s->name() << "\n" << m_fmls << "\n");
         }      
     }
     

src/ast/simplifiers/solve_eqs.cpp

@@ -34,7 +34,7 @@ namespace euf {
 
     void solve_eqs::get_eqs(dep_eq_vector& eqs) {
         for (extract_eq* ex : m_extract_plugins)
-            for (unsigned i = qhead(); i < qtail(); ++i)
+            for (unsigned i : indices())
                 ex->get_eqs(m_fmls[i], eqs);
     }
 
@@ -99,6 +99,9 @@ namespace euf {
                     auto const& [orig, v, t, d] = eq;
                     SASSERT(j == var2id(v));
                     bool is_safe = true;
+                    if (m_fmls.frozen(v))
+                        continue;
+                    
                     unsigned todo_sz = todo.size();
 
                     // determine if substitution is safe.
@@ -187,7 +190,7 @@ namespace euf {
         scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
         rp->set_substitution(m_subst.get());
 
-        for (unsigned i = qhead(); i < qtail() && !m_fmls.inconsistent(); ++i) {
+        for (unsigned i : indices()) {
             auto [f, d] = m_fmls[i]();
             auto [new_f, new_dep] = rp->replace_with_dep(f);
             m_rewriter(new_f);

src/ast/simplifiers/solve_eqs.h

@@ -32,6 +32,10 @@ namespace euf {
         struct stats {
             unsigned m_num_steps = 0;
             unsigned m_num_elim_vars = 0;
+            void reset() {
+                m_num_steps = 0;
+                m_num_elim_vars = 0;
+            }
         };
 
         struct config {
@@ -78,5 +82,7 @@ namespace euf {
 
         void collect_statistics(statistics& st) const override;
 
+        void reset_statistics() override { m_stats.reset(); }
+
     };
 }

src/qe/lite/qe_lite.cpp

@@ -35,6 +35,8 @@ Revision History:
 #include "tactic/tactical.h"
 #include "qe/mbp/mbp_solve_plugin.h"
 #include "qe/lite/qe_lite.h"
+#include "tactic/dependent_expr_state_tactic.h"
+
 
 namespace qel {
 
@@ -2407,122 +2409,50 @@ void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_re
 }
 
 namespace {
-class qe_lite_tactic : public tactic {
+    class qe_lite_simplifier : public dependent_expr_simplifier {
-    ast_manager&             m;
+        params_ref               m_params;
-    params_ref               m_params;
+        qe_lite                  m_qe;
-    qe_lite                  m_qe;
+    public:
+        qe_lite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st) :
+            dependent_expr_simplifier(m, st),
+            m_qe(m, p, true) {
+            updt_params(p);
+        }
 
-    void checkpoint() {
+        char const* name() const override { return "qe-lite"; }
-        tactic::checkpoint(m);
-    }
 
-#if 0
+        void updt_params(params_ref const& p) override {
-    void debug_diff(expr* a, expr* b) {
+            m_params.append(p);
-        ptr_vector<expr> as, bs;
+        }
-        as.push_back(a);
+
-        bs.push_back(b);
+        void reduce() override {
-        expr* a1, *a2, *b1, *b2;
+            if (!m_fmls.has_quantifiers())
-        while (!as.empty()) {
+                return;
-            a = as.back();
+            proof_ref new_pr(m);
-            b = bs.back();
+            expr_ref new_f(m);
-            as.pop_back();
+            for (unsigned i : indices()) {
-            bs.pop_back();
+                expr* f = m_fmls[i].fml();
-            if (a == b) {
+                if (!has_quantifiers(f))
-                continue;
+                    continue;
-            }
+                new_f = f;
-            else if (is_forall(a) && is_forall(b)) {
+                m_qe(new_f, new_pr);
-                as.push_back(to_quantifier(a)->get_expr());
+                m_fmls.update(i, dependent_expr(m, new_f, m_fmls[i].dep()));
-                bs.push_back(to_quantifier(b)->get_expr());
-            }
-            else if (m.is_and(a, a1, a2) && m.is_and(b, b1, b2)) {
-                as.push_back(a1);
-                as.push_back(a2);
-                bs.push_back(b1);
-                bs.push_back(b2);
-            }
-            else if (m.is_eq(a, a1, a2) && m.is_eq(b, b1, b2)) {
-                as.push_back(a1);
-                as.push_back(a2);
-                bs.push_back(b1);
-                bs.push_back(b2);
-            }
-            else {
-                TRACE("qe", tout << mk_pp(a, m) << " != " << mk_pp(b, m) << "\n";);
             }
         }
-    }
+    };
-#endif
 
-public:
+    class qe_lite_tactic_factory : public dependent_expr_simplifier_factory {
-    qe_lite_tactic(ast_manager & m, params_ref const & p):
+    public:
-        m(m),
+        dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
-        m_params(p),
+            return alloc(qe_lite_simplifier, m, p, s);
-        m_qe(m, p, true) {}
-
-    char const* name() const override { return "qe_lite"; }
-
-    tactic * translate(ast_manager & m) override {
-        return alloc(qe_lite_tactic, m, m_params);
-    }
-
-    void updt_params(params_ref const & p) override {
-        m_params.append(p);
-        // m_imp->updt_params(p);
-    }
-
-    void collect_param_descrs(param_descrs & r) override {
-        // m_imp->collect_param_descrs(r);
-    }
-
-    void operator()(goal_ref const & g,
-                    goal_ref_buffer & result) override {
-        tactic_report report("qe-lite", *g);
-        proof_ref new_pr(m);
-        expr_ref new_f(m);
-
-        unsigned sz = g->size();
-        for (unsigned i = 0; i < sz; i++) {
-            checkpoint();
-            if (g->inconsistent())
-                break;
-            expr * f = g->form(i);
-            if (!has_quantifiers(f))
-                continue;
-            new_f = f;
-            m_qe(new_f, new_pr);
-            if (new_pr) {
-                expr* fact = m.get_fact(new_pr);
-                if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) {
-                    new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
-                }
-                else {
-                    new_pr = g->pr(i);
-                }
-            }
-            if (f != new_f) {
-                TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n" << new_pr << "\n";);
-                g->update(i, new_f, new_pr, g->dep(i));
-            }
         }
-        g->inc_depth();
+    };
-        result.push_back(g.get());
-    }
-
-    void collect_statistics(statistics & st) const override {
-        // m_imp->collect_statistics(st);
-    }
-
-    void reset_statistics() override {
-        // m_imp->reset_statistics();
-    }
-
-    void cleanup() override {
-        m_qe.~qe_lite();
-        new (&m_qe) qe_lite(m, m_params, true);
-    }
-};
 }
 
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
-    return alloc(qe_lite_tactic, m, p);
+    return alloc(dependent_expr_state_tactic, m, p, alloc(qe_lite_tactic_factory));
+}
+
+dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st) {
+    return alloc(qe_lite_simplifier, m, p, st);
 }

src/qe/lite/qe_lite.h

@@ -23,6 +23,7 @@ Revision History:
 #include "ast/ast.h"
 #include "util/uint_set.h"
 #include "util/params.h"
+#include "ast/simplifiers/dependent_expr_state.h"
 
 class tactic;
 
@@ -70,3 +71,5 @@ tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref())
 /*
   ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
 */
+
+dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st);

src/sat/sat_solver/sat_smt_preprocess.cpp

@@ -22,9 +22,19 @@ Author:
 #include "ast/simplifiers/propagate_values.h"
 #include "ast/simplifiers/rewriter_simplifier.h"
 #include "ast/simplifiers/solve_eqs.h"
+#include "ast/simplifiers/bv_slice.h"
 #include "ast/simplifiers/eliminate_predicates.h"
+#include "ast/simplifiers/elim_unconstrained.h"
+#include "ast/simplifiers/pull_nested_quantifiers.h"
+#include "ast/simplifiers/distribute_forall.h"
+#include "ast/simplifiers/refine_inj_axiom.h"
+#include "ast/simplifiers/elim_bounds.h"
+#include "ast/simplifiers/bit2int.h"
+#include "ast/simplifiers/bv_elim.h"
 #include "sat/sat_params.hpp"
+#include "smt/params/smt_params.h"
 #include "sat/sat_solver/sat_smt_preprocess.h"
+#include "qe/lite/qe_lite.h"
 
 void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
     params_ref simp1_p = p;
@@ -44,18 +54,38 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
     simp2_p.set_bool("flat_and_or", false);
     
     sat_params sp(p);
+    smt_params smtp(p);
     if (sp.euf() || sp.smt()) {
         s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
         s.add_simplifier(alloc(propagate_values, m, p, st));
+        s.add_simplifier(alloc(euf::solve_eqs, m, st));
+        s.add_simplifier(alloc(elim_unconstrained, m, st));
+        if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
+        if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));
+        if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st));
+        if (smtp.m_max_bv_sharing) s.add_simplifier(mk_max_bv_sharing(m, p, st));
+        if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st));
+        if (smtp.m_bv_size_reduce) s.add_simplifier(alloc(bv::slice, m, st));
+        if (smtp.m_distribute_forall) s.add_simplifier(alloc(distribute_forall_simplifier, m, p, st));
+        if (smtp.m_eliminate_bounds) s.add_simplifier(alloc(elim_bounds_simplifier, m, p, st));
+        if (smtp.m_simplify_bit2int) s.add_simplifier(alloc(bit2int_simplifier, m, p, st));
+        if (smtp.m_bb_quantifiers) s.add_simplifier(alloc(bv::elim_simplifier, m, p, st));
         //
         // add: 
-        // solve_eqs
-        // elim_predicates
-        // elim_uncnstr
         // euf_completion?
         //
-        // add: make it externally configurable
+        // add: make it externally programmable
         // 
+#if 0
+    ?? if (!invoke(m_lift_ite)) return;
+    m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
+    m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
+    ?? if (!invoke(m_ng_lift_ite)) return;
+    if (!invoke(m_elim_term_ite)) return;
+    if (!invoke(m_apply_quasi_macros)) return;
+    if (!invoke(m_flatten_clauses)) return;
+#endif
+
     }
     else {
         s.add_simplifier(alloc(rewriter_simplifier, m, p, st));

src/sat/sat_solver/sat_smt_solver.cpp

@@ -60,6 +60,17 @@ class sat_smt_solver : public solver {
         void add(dependent_expr const& j) override { s.m_fmls.push_back(j); }
         bool inconsistent() override { return s.m_solver.inconsistent(); }
         model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; }
+        std::ostream& display(std::ostream& out) const override {
+            unsigned i = 0;
+            for (auto const& d : s.m_fmls) {
+                if (i == qhead())
+                    out << "---- head ---\n";
+                out << d << "\n";
+                ++i;
+            }
+            m_reconstruction_trail.display(out);
+            return out;
+        }
         void append(generic_model_converter& mc) { model_trail().append(mc); }
         void replay(unsigned qhead) { m_reconstruction_trail.replay(qhead, *this); }
         void flatten_suffix() override {
@@ -421,12 +432,10 @@ public:
     }
 
     expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override {
-        if (!is_internalized()) {
+        lbool r = internalize_formulas();
-            lbool r = internalize_formulas();
+        if (r != l_true) {
-            if (r != l_true) {
+            IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n");
-                IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n");
+            return expr_ref_vector(m);
-                return expr_ref_vector(m);
-            }
         }
         convert_internalized();
         if (m_solver.inconsistent())
@@ -551,8 +560,7 @@ public:
 
     void convert_internalized() {
         m_solver.pop_to_base_level();
-        if (!is_internalized() && m_preprocess_state.qhead() > 0) 
+        internalize_formulas();        
-            internalize_formulas();        
         if (!is_internalized() || m_internalized_converted) 
             return;
         sat2goal s2g;
@@ -723,9 +731,8 @@ private:
         
         for (unsigned v = 0; v < var2expr.size(); ++v) {
             expr * n = var2expr.get(v);
-            if (!n || !is_uninterp_const(n)) {
+            if (!n || !is_uninterp_const(n)) 
-                continue;
+                continue;            
-            }
             switch (sat::value_at(v, ll_m)) {
             case l_true:
                 mdl->register_decl(to_app(n)->get_decl(), m.mk_true());
@@ -747,9 +754,8 @@ private:
     
         TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););        
 
-        if (!gparams::get_ref().get_bool("model_validate", false)) {
+        if (!gparams::get_ref().get_bool("model_validate", false)) 
-            return;
+            return;        
-        }
         IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";);
         model_evaluator eval(*mdl);
         eval.set_model_completion(true);