Merge branch 'master' of https://github.com/z3prover/z3 into xor

azure-pipelines.yml

@@ -202,7 +202,7 @@ jobs:
         setupCmd2: 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env'
         setupCmd3: 'set /P JlCxxDir=<tmp.env'
         bindings:  '-DJlCxx_DIR=%JlCxxDir%\..\lib\cmake\JlCxx $(cmakeJava) $(cmakeNet) $(cmakePy) -DCMAKE_BUILD_TYPE=RelWithDebInfo'
-        runTests:  'True'
+        runTests:  'False'
       arm64:
         arch: 'amd64_arm64'
         setupCmd1: ''

src/api/api_seq.cpp

@@ -212,6 +212,8 @@ extern "C" {
                 buffer.push_back('\\');
                 buffer.push_back('u');
                 buffer.push_back('{');
+                if (ch == 0)
+                    buff.push_back('0');
                 while (ch > 0) {
                     unsigned d = ch & 0xF;
                     if (d < 10)

src/api/python/z3/z3.py

@@ -10079,7 +10079,7 @@ def FPs(names, fpsort, ctx=None):
     >>> x.ebits()
     8
     >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
-    fpMul(RNE(), fpAdd(RNE(), x, y), z)
+    x + y * z
     """
     ctx = _get_ctx(ctx)
     if isinstance(names, str):
@@ -10186,9 +10186,9 @@ def fpAdd(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpAdd(rm, x, y)
-    fpAdd(RNE(), x, y)
-    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
     x + y
+    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
+    fpAdd(RTZ(), x, y)
     >>> fpAdd(rm, x, y).sort()
     FPSort(8, 24)
     """
@@ -10203,7 +10203,7 @@ def fpSub(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpSub(rm, x, y)
-    fpSub(RNE(), x, y)
+    x - y
     >>> fpSub(rm, x, y).sort()
     FPSort(8, 24)
     """
@@ -10218,7 +10218,7 @@ def fpMul(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpMul(rm, x, y)
-    fpMul(RNE(), x, y)
+    x * y
     >>> fpMul(rm, x, y).sort()
     FPSort(8, 24)
     """
@@ -10233,7 +10233,7 @@ def fpDiv(rm, a, b, ctx=None):
     >>> x = FP('x', s)
     >>> y = FP('y', s)
     >>> fpDiv(rm, x, y)
-    fpDiv(RNE(), x, y)
+    x / y
     >>> fpDiv(rm, x, y).sort()
     FPSort(8, 24)
     """

src/ast/ast.cpp

@@ -2250,7 +2250,9 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
     if (type_error) {
         std::ostringstream buffer;
         buffer << "Wrong number of arguments (" << num_args
-               << ") passed to function " << mk_pp(decl, *this);
+               << ") passed to function " << mk_pp(decl, *this) << " ";
+        for (unsigned i = 0; i < num_args; ++i)
+            buffer << "\narg: " << mk_pp(args[i], *this) << "\n";
         throw ast_exception(std::move(buffer).str());
     }
     app * r = nullptr;

src/ast/bv_decl_plugin.h

@@ -430,6 +430,9 @@ public:
     }
     app * mk_concat(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_CONCAT, num, args);  }
     app * mk_concat(expr_ref_vector const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
+    app * mk_concat(expr_ref_buffer const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
+    app * mk_concat(ptr_buffer<expr> const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
+    app * mk_concat(ptr_vector<expr> const& es) { return m_manager.mk_app(get_fid(), OP_CONCAT, es.size(), es.data());  }
     app * mk_bv_or(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BOR, num, args);  }
     app * mk_bv_and(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BAND, num, args);  }
     app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args);  }

src/ast/expr_substitution.h

@@ -44,8 +44,10 @@ public:
     bool empty() const { return m_subst.empty(); }
     unsigned size() const { return m_subst.size(); }
     void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr);
+    void insert(expr* s, expr* def, expr_dependency* def_dep) { insert(s, def, nullptr, def_dep); }
     void erase(expr * s);
-    expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; }
+    expr* find(expr* s) { return m_subst[s]; }
+    expr_dependency* dep(expr* s) { return (*m_subst_dep)[s]; }
     bool find(expr * s, expr * & def, proof * & def_pr);
     bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep);
     bool contains(expr * s);
@@ -57,6 +59,10 @@ public:
     std::ostream& display(std::ostream& out);
 };
 
+inline std::ostream& operator<<(std::ostream& out, expr_substitution& s) {
+    return s.display(out);
+}
+
 class scoped_expr_substitution {
     expr_substitution& m_subst;
     expr_ref_vector    m_trail;

src/ast/for_each_expr.cpp

@@ -64,15 +64,22 @@ bool has_skolem_functions(expr * n) {
     return false;
 }
 
-subterms::subterms(expr_ref_vector const& es, bool include_bound): m_include_bound(include_bound), m_es(es) {}
-subterms::subterms(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) {if (e)  m_es.push_back(e); }
-subterms::iterator subterms::begin() { return iterator(*this, true); }
-subterms::iterator subterms::end() { return iterator(*this, false); }
-subterms::iterator::iterator(subterms& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) {
-    if (!start) m_es.reset();
+subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {}
+subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); }
+subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); }
+subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); }
+subterms::iterator::iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
+    if (!esp)
+        m_esp = &m_es;
+    else
+        m_esp->reset();
+    if (!m_visitedp)
+        m_visitedp = &m_visited;
+    if (start)
+        m_esp->append(f.m_es.size(), f.m_es.data());
 }
 expr* subterms::iterator::operator*() {
-    return m_es.back();
+    return m_esp->back();
 }
 subterms::iterator subterms::iterator::operator++(int) {
     iterator tmp = *this;
@@ -80,27 +87,29 @@ subterms::iterator subterms::iterator::operator++(int) {
     return tmp;
 }
 subterms::iterator& subterms::iterator::operator++() {
-    expr* e = m_es.back();
-    m_visited.mark(e, true);
+    expr* e = m_esp->back();
+    // IF_VERBOSE(0, verbose_stream() << e->get_ref_count() << "\n");
+    SASSERT(e->get_ref_count() > 0);
+    m_visitedp->mark(e, true);
     if (is_app(e)) 
         for (expr* arg : *to_app(e)) 
-            m_es.push_back(arg);            
+            m_esp->push_back(arg);            
     else if (is_quantifier(e) && m_include_bound)
-        m_es.push_back(to_quantifier(e)->get_expr());
+        m_esp->push_back(to_quantifier(e)->get_expr());
 
-    while (!m_es.empty() && m_visited.is_marked(m_es.back())) 
-        m_es.pop_back();
+    while (!m_esp->empty() && m_visitedp->is_marked(m_esp->back())) 
+        m_esp->pop_back();
     
     return *this;
 }
 
 bool subterms::iterator::operator==(iterator const& other) const {
     // ignore state of visited
-    if (other.m_es.size() != m_es.size()) {
+    if (other.m_esp->size() != m_esp->size()) {
         return false;
     }
-    for (unsigned i = m_es.size(); i-- > 0; ) {
-        if (m_es.get(i) != other.m_es.get(i))
+    for (unsigned i = m_esp->size(); i-- > 0; ) {
+        if (m_esp->get(i) != other.m_esp->get(i))
             return false;
     }
     return true;

src/ast/for_each_expr.h

@@ -170,15 +170,20 @@ bool has_skolem_functions(expr * n);
 class subterms {
     bool            m_include_bound = false;
     expr_ref_vector m_es;
-    subterms(expr_ref const& e, bool include_bound);
-    subterms(expr_ref_vector const& es, bool include_bound);
+    ptr_vector<expr>* m_esp = nullptr;
+    expr_mark* m_vp = nullptr;
+    subterms(expr_ref const& e, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp);
+    subterms(expr_ref_vector const& es, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp);
 public:
+    ~subterms() { if (m_vp) m_vp->reset(); }
     class iterator {
-        bool            m_include_bound = false;
-        expr_ref_vector m_es;
-        expr_mark       m_visited;        
+        bool              m_include_bound = false;
+        ptr_vector<expr>  m_es;
+        ptr_vector<expr>* m_esp = nullptr;
+        expr_mark         m_visited;   
+        expr_mark*        m_visitedp = nullptr;
     public:
-        iterator(subterms& f, bool start);
+        iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
         expr* operator*();
         iterator operator++(int);
         iterator& operator++();
@@ -186,11 +191,10 @@ public:
         bool operator!=(iterator const& other) const;
     };
 
-
-    static subterms all(expr_ref const& e) { return subterms(e, true); }
-    static subterms ground(expr_ref const& e) { return subterms(e, false); }
-    static subterms all(expr_ref_vector const& e) { return subterms(e, true); }
-    static subterms ground(expr_ref_vector const& e) { return subterms(e, false); }
+    static subterms all(expr_ref const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); }
+    static subterms ground(expr_ref const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
+    static subterms all(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); }
+    static subterms ground(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
     iterator begin();
     iterator end();
 };

src/ast/normal_forms/nnf.cpp

@@ -22,6 +22,7 @@ Notes:
 #include "ast/normal_forms/nnf.h"
 #include "ast/normal_forms/nnf_params.hpp"
 #include "ast/used_vars.h"
+#include "ast/ast_util.h"
 #include "ast/well_sorted.h"
 #include "ast/act_cache.h"
 #include "ast/rewriter/var_subst.h"
@@ -137,7 +138,7 @@ class skolemizer {
                 if (is_sk_hack(p)) {
                     expr * sk_hack = to_app(p)->get_arg(0);
                     if (q->get_kind() == forall_k) // check whether is in negative/positive context.
-                        tmp  = m.mk_or(body, m.mk_not(sk_hack)); // negative context
+                        tmp  = m.mk_or(body, mk_not(m, sk_hack)); // negative context
                     else
                         tmp  = m.mk_and(body, sk_hack); // positive context
                     body = tmp;
@@ -148,7 +149,7 @@ class skolemizer {
         p = nullptr;
         if (m_proofs_enabled) {
             if (q->get_kind() == forall_k) 
-                p = m.mk_skolemization(m.mk_not(q), m.mk_not(r));
+                p = m.mk_skolemization(mk_not(m, q), mk_not(m, r));
             else
                 p = m.mk_skolemization(q, r);
         }
@@ -388,7 +389,7 @@ struct nnf::imp {
     }
 
     void skip(expr * t, bool pol) {
-        expr * r = pol ? t : m.mk_not(t);
+        expr * r = pol ? t : mk_not(m, t);
         m_result_stack.push_back(r);
         if (proofs_enabled()) {
             m_result_pr_stack.push_back(m.mk_oeq_reflexivity(r));
@@ -639,7 +640,7 @@ struct nnf::imp {
                 m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
 
             if (!fr.m_pol)
-                n2 = m.mk_not(n2);
+                n2 = mk_not(m, n2);
             m_result_stack.push_back(n2);
             if (proofs_enabled()) {
                 if (!fr.m_pol) {

src/ast/occurs.cpp

@@ -74,3 +74,46 @@ bool occurs(func_decl * d, expr * n) {
     return false;
 }
 
+void mark_occurs(ptr_vector<expr>& to_check, expr* v, expr_mark& occ) {
+    expr_fast_mark2 visited;
+    occ.mark(v, true);
+    visited.mark(v, true);
+    while (!to_check.empty()) {
+        expr* e = to_check.back();
+        if (visited.is_marked(e)) {
+            to_check.pop_back();
+            continue;
+        }
+        if (is_app(e)) {
+            bool does_occur = false;
+            bool all_visited = true;
+            for (expr* arg : *to_app(e)) {
+                if (!visited.is_marked(arg)) {
+                    to_check.push_back(arg);
+                    all_visited = false;
+                }
+                else 
+                    does_occur |= occ.is_marked(arg);                
+            }
+            if (all_visited) {
+                occ.mark(e, does_occur);
+                visited.mark(e, true);
+                to_check.pop_back();
+            }
+        }
+        else if (is_quantifier(e)) {
+            expr* body = to_quantifier(e)->get_expr();
+            if (visited.is_marked(body)) {
+                visited.mark(e, true);
+                occ.mark(e, occ.is_marked(body));
+                to_check.pop_back();
+            }
+            else 
+                to_check.push_back(body);            
+        }
+        else {
+            visited.mark(e, true);
+            to_check.pop_back();
+        }
+    }
+}

src/ast/occurs.h

@@ -18,8 +18,8 @@ Revision History:
 --*/
 #pragma once
 
-class expr; 
-class func_decl;
+#include "util/vector.h"
+#include "ast/ast.h"
 
 /**
    \brief Return true if n1 occurs in n2
@@ -31,4 +31,9 @@ bool occurs(expr * n1, expr * n2);
 */
 bool occurs(func_decl * d, expr * n);
 
+/**
+* \brief Mark sub-expressions of to_check by whether v occurs in these.
+*/
+void mark_occurs(ptr_vector<expr>& to_check, expr* v, expr_mark& occurs);
+
 

src/ast/recfun_decl_plugin.cpp

@@ -442,17 +442,18 @@ namespace recfun {
             return promise_def(&u(), d);
         }
 
-        void plugin::inherit(decl_plugin* other, ast_translation& tr) {
-            for (auto [k, v] : static_cast<plugin*>(other)->m_defs) {
+        void plugin::inherit(decl_plugin* _other, ast_translation& tr) {
+            plugin* other = static_cast<plugin*>(_other);
+            for (auto [k, v] : other->m_defs) {
                 func_decl_ref f(tr(k), tr.to());
                 if (m_defs.contains(f))
                     continue;
                 def* d = v->copy(u(), tr);
                 m_defs.insert(f, d);
                 for (case_def & c : d->get_cases())
-                    m_case_defs.insert(c.get_decl(), &c);
-                    
+                    m_case_defs.insert(c.get_decl(), &c);                    
             }
+            m_has_rec_defs = other->m_has_rec_defs;
         }
 
         promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) {
@@ -473,6 +474,7 @@ namespace recfun {
         }
         
         void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
+            m_has_rec_defs |= !is_macro;
             u().set_definition(r, d, is_macro, n_vars, vars, rhs);
             for (case_def & c : d.get_def()->get_cases()) 
                 m_case_defs.insert(c.get_decl(), &c);

src/ast/recfun_decl_plugin.h

@@ -165,6 +165,7 @@ namespace recfun {
             mutable scoped_ptr<util> m_util;
             def_map                  m_defs;       // function->def
             case_def_map             m_case_defs;  // case_pred->def
+            bool                     m_has_rec_defs = false;
             
             ast_manager & m() { return *m_manager; }
 
@@ -200,6 +201,7 @@ namespace recfun {
 
             bool has_def(func_decl* f) const { return m_defs.contains(f); }
             bool has_defs() const;
+            bool has_rec_defs() const { return m_has_rec_defs; }
             def const& get_def(func_decl* f) const { return *(m_defs[f]); }
             promise_def get_promise_def(func_decl* f) const { return promise_def(&u(), m_defs[f]); }
             def& get_def(func_decl* f) { return *(m_defs[f]); }
@@ -249,6 +251,8 @@ namespace recfun {
         //<! don't use native theory if recursive function declarations are not populated with defs
         bool has_defs() const { return m_plugin->has_defs(); }
 
+        bool has_rec_defs() const { return m_plugin->has_rec_defs(); }
+
         //<! add a function declaration
         def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range, bool is_generated);
 

src/ast/rewriter/bool_rewriter.cpp

@@ -24,7 +24,7 @@ Notes:
 
 void bool_rewriter::updt_params(params_ref const & _p) {
     bool_rewriter_params p(_p);
-    m_flat_and_or          = p.flat();
+    m_flat_and_or          = p.flat_and_or();
     m_elim_and             = p.elim_and();
     m_elim_ite             = p.elim_ite();
     m_local_ctx            = p.local_ctx();
@@ -244,10 +244,38 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
         result = buffer.back();
         return BR_DONE;
     default:
+#if 0
+        // stupid or removal. A very special case of circuit optimization.
+        expr* x, * y, * z, * u;
+        auto is_complement = [&](expr* a, expr* b) {
+            expr* c;
+            if (m().is_not(a, c) && c == b)
+                return true;
+            if (m().is_not(b, c) && c == a)
+                return true;
+            return false;
+        };
+
+        if (sz == 2 && m().is_and(buffer[0], x, y) && m().is_and(buffer[1], z, u) && x == z && is_complement(y, u)) {
+            result = x;
+            return BR_DONE;
+        }
+#endif
+
         if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) {
             if (local_ctx_simp(sz, buffer.data(), result)) 
                 return BR_DONE;
         }
+
+#if 1
+        br_status st;
+        st = m_hoist.mk_or(buffer.size(), buffer.data(), result);
+        if (st == BR_DONE)
+            return BR_REWRITE1;
+        if (st != BR_FAILED)
+            return st;
+#endif
+
         if (s) {
             ast_lt lt;
             std::sort(buffer.begin(), buffer.end(), lt);       
@@ -556,9 +584,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
                 return true;                                                                    \
             }                                                                                   \
             if (m_flat_and_or && m().is_or(arg)) {                                              \
-                unsigned sz = to_app(arg)->get_num_args();                                      \
-                for (unsigned j = 0; j < sz; j++) {                                             \
-                    expr * arg_arg = to_app(arg)->get_arg(j);                                   \
+                for (expr * arg_arg : *to_app(arg)) {                                           \
                     push_new_arg(arg_arg, new_args, neg_lits, pos_lits);                        \
                 }                                                                               \
             }                                                                                   \

src/ast/rewriter/bool_rewriter.h

@@ -20,6 +20,7 @@ Notes:
 
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/hoist_rewriter.h"
 #include "util/params.h"
 
 /**
@@ -50,6 +51,7 @@ Notes:
 */
 class bool_rewriter {
     ast_manager &  m_manager;
+    hoist_rewriter m_hoist;
     bool           m_flat_and_or;
     bool           m_local_ctx;
     bool           m_elim_and;
@@ -78,7 +80,7 @@ class bool_rewriter {
     void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
 
 public:
-    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); }
+    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { updt_params(p); }
     ast_manager & m() const { return m_manager; }
     family_id get_fid() const { return m().get_basic_family_id(); }
     bool is_eq(expr * t) const { return m().is_eq(t); }

src/ast/rewriter/bv_rewriter.cpp

@@ -1513,11 +1513,14 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
     bool fused_numeral = false;
     bool expanded      = false;
     bool fused_extract = false;
+    bool eq_args = true;
     for (unsigned i = 0; i < num_args; i++) {
         expr * arg = args[i];
         expr * prev = nullptr;
-        if (i > 0)
+        if (i > 0) {
             prev = new_args.back();
+            eq_args &= prev == arg;
+        }
         if (is_numeral(arg, v1, sz1) && prev != nullptr && is_numeral(prev, v2, sz2)) {
             v2  *= rational::power_of_two(sz1);
             v2  += v1;
@@ -1526,10 +1529,8 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
             fused_numeral = true;
         }
         else if (m_flat && m_util.is_concat(arg)) {
-            unsigned num2 = to_app(arg)->get_num_args();
-            for (unsigned j = 0; j < num2; j++) {
-                new_args.push_back(to_app(arg)->get_arg(j));
-            }
+            for (expr* arg2 : *to_app(arg)) 
+                new_args.push_back(arg2);
             expanded = true;
         }
         else if (m_util.is_extract(arg) &&
@@ -1539,8 +1540,8 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
                  m_util.get_extract_low(prev) == m_util.get_extract_high(arg) + 1) {
             // (concat (extract[h1,l1] a) (extract[h2,l2] a)) --> (extract[h1,l2] a)  if l1 == h2+1
             expr * new_arg = m_mk_extract(m_util.get_extract_high(prev),
-                                               m_util.get_extract_low(arg),
-                                               to_app(arg)->get_arg(0));
+                                          m_util.get_extract_low(arg),
+                                          to_app(arg)->get_arg(0));
             new_args.pop_back();
             new_args.push_back(new_arg);
             fused_extract = true;
@@ -1549,14 +1550,26 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
             new_args.push_back(arg);
         }
     }
-    if (!fused_numeral && !expanded && !fused_extract)
+    if (!fused_numeral && !expanded && !fused_extract) {
+        expr* x, *y, *z;
+        if (eq_args) {
+            if (m().is_ite(new_args.back(), x, y, z)) {
+                ptr_buffer<expr> args1, args2;
+                for (expr* arg : new_args)
+                    args1.push_back(y), args2.push_back(z);
+                result = m().mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2));
+                return BR_REWRITE2;
+            }
+        }
         return BR_FAILED;
+
+    }
     SASSERT(!new_args.empty());
     if (new_args.size() == 1) {
         result = new_args.back();
         return fused_extract ? BR_REWRITE1 : BR_DONE;
     }
-    result = m_util.mk_concat(new_args.size(), new_args.data());
+    result = m_util.mk_concat(new_args);
     if (fused_extract)
         return BR_REWRITE2;
     else if (expanded)
@@ -2013,6 +2026,19 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
         return BR_REWRITE2;
     }
 
+    expr* x, *y, *z;
+    if (m().is_ite(arg, x, y, z) && m_util.is_numeral(y, val, bv_size)) {
+        val = bitwise_not(bv_size, val);
+        result = m().mk_ite(x, m_util.mk_numeral(val, bv_size), m_util.mk_bv_not(z));
+        return BR_REWRITE2;
+    }
+
+    if (m().is_ite(arg, x, y, z) && m_util.is_numeral(z, val, bv_size)) {
+        val = bitwise_not(bv_size, val);
+        result = m().mk_ite(x, m_util.mk_bv_not(y), m_util.mk_numeral(val, bv_size));
+        return BR_REWRITE2;
+    }
+
     if (m_bvnot_simpl) {
         expr *s(nullptr), *t(nullptr);
         if (m_util.is_bv_mul(arg, s, t)) {

src/ast/rewriter/expr_replacer.cpp

@@ -25,6 +25,11 @@ void expr_replacer::operator()(expr * t, expr_ref & result, proof_ref & result_p
     operator()(t, result, result_pr, result_dep);
 }
 
+void expr_replacer::operator()(expr* t, expr_ref& result, expr_dependency_ref& result_dep) {
+    proof_ref result_pr(m());
+    operator()(t, result, result_pr, result_dep);
+}
+
 void expr_replacer::operator()(expr * t, expr_ref & result) {
     proof_ref pr(m());
     operator()(t, result, pr);

src/ast/rewriter/expr_replacer.h

@@ -34,9 +34,12 @@ public:
     virtual void set_substitution(expr_substitution * s) = 0;
 
     virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & deps) = 0;
-    virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
-    virtual void operator()(expr * t, expr_ref & result);
-    virtual void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); }
+    void operator()(expr* t, expr_ref& result, expr_dependency_ref& deps);
+    void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
+    void operator()(expr * t, expr_ref & result);
+    void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); }
+    void operator()(expr_ref_vector& v) { expr_ref t(m());  for (unsigned i = 0; i < v.size(); ++i) (*this)(v.get(i), t), v[i] = t; }
+    std::pair<expr_ref, expr_dependency_ref> replace_with_dep(expr* t) { expr_ref r(m()); expr_dependency_ref d(m()); (*this)(t, r, d); return { r, d }; }
 
     virtual unsigned get_num_steps() const { return 0; }
     virtual void reset() = 0;

src/ast/rewriter/hoist_rewriter.cpp

@@ -13,8 +13,6 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2019-2-4
 
-Notes:
-
 --*/
 
 
@@ -25,19 +23,17 @@ Notes:
 
 
 hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
-    m_manager(m), m_args1(m), m_args2(m), m_subst(m) { 
+    m(m), m_args1(m), m_args2(m), m_subst(m) { 
     updt_params(p); 
 }
 
 br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
-    if (num_args < 2) {
+    if (num_args < 2) 
         return BR_FAILED;
-    }
-    for (unsigned i = 0; i < num_args; ++i) {
-        if (!is_and(es[i], nullptr)) {
+
+    for (unsigned i = 0; i < num_args; ++i) 
+        if (!is_and(es[i], nullptr)) 
             return BR_FAILED;
-        }
-    }
 
     bool turn = false;
     m_preds1.reset(); 
@@ -52,12 +48,10 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
     VERIFY(is_and(es[0], args[turn]));
     expr* e1, *e2;
     for (expr* e : *(args[turn])) {
-        if (m().is_eq(e, e1, e2)) {            
+        if (m.is_eq(e, e1, e2))             
             (*uf)[turn].merge(mk_var(e1), mk_var(e2));
-        }
-        else {
+        else 
             (*preds)[turn].insert(e);
-        }
     }
     unsigned round = 0;
     for (unsigned j = 1; j < num_args; ++j) {
@@ -72,44 +66,39 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
         VERIFY(is_and(es[j], args[turn]));
 
         for (expr* e : *args[turn]) {
-            if (m().is_eq(e, e1, e2)) {
+            if (m.is_eq(e, e1, e2)) {
                 m_es.push_back(e1);                
                 m_uf0.merge(mk_var(e1), mk_var(e2));
             }    
-            else if ((*preds)[last].contains(e)) {
+            else if ((*preds)[last].contains(e)) 
                 (*preds)[turn].insert(e);
-            }
         }
 
-        if ((*preds)[turn].empty() && m_es.empty()) {
+        if ((*preds)[turn].empty() && m_es.empty()) 
             return BR_FAILED;
-        }
 
         m_eqs.reset();
         for (expr* e : m_es) {
-            if (m_mark.is_marked(e)) {
+            if (m_mark.is_marked(e)) 
                 continue;
-            }
             unsigned u = mk_var(e);
             unsigned v = u;
             m_roots.reset();
             do {
                 m_mark.mark(e);
                 unsigned r = (*uf)[last].find(v);
-                if (m_roots.find(r, e2)) {
-                    m_eqs.push_back(std::make_pair(e, e2));
-                }
-                else {
+                if (m_roots.find(r, e2)) 
+                    m_eqs.push_back({e, e2});
+                else 
                     m_roots.insert(r, e);
-                }
                 v = m_uf0.next(v);
                 e = mk_expr(v);
             }
             while (u != v);
         }
         reset((*uf)[turn]);
-        for (auto const& p : m_eqs) 
-            (*uf)[turn].merge(mk_var(p.first), mk_var(p.second));
+        for (auto const& [e1, e2] : m_eqs) 
+            (*uf)[turn].merge(mk_var(e1), mk_var(e2));
         if ((*preds)[turn].empty() && m_eqs.empty()) 
             return BR_FAILED;
     }
@@ -118,25 +107,23 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
         return BR_DONE;
     }
     // p & eqs & (or fmls)
-    expr_ref_vector fmls(m());
+    expr_ref_vector fmls(m);
     m_subst.reset();
     for (expr * p : (*preds)[turn]) {
         expr* q = nullptr;
-        if (m().is_not(p, q)) {
-            m_subst.insert(q, m().mk_false());
-        }
-        else {
-            m_subst.insert(p, m().mk_true());
-        }
+        if (m.is_not(p, q)) 
+            m_subst.insert(q, m.mk_false());
+        else 
+            m_subst.insert(p, m.mk_true());
         fmls.push_back(p);
     }
     for (auto& p : m_eqs) {
-        if (m().is_value(p.first))
+        if (m.is_value(p.first))
             std::swap(p.first, p.second);
         m_subst.insert(p.first, p.second);
-        fmls.push_back(m().mk_eq(p.first, p.second));
+        fmls.push_back(m.mk_eq(p.first, p.second));
     }    
-    expr_ref ors(::mk_or(m(), num_args, es), m());
+    expr_ref ors(::mk_or(m, num_args, es), m);
     m_subst(ors);
     fmls.push_back(ors);
     result = mk_and(fmls);
@@ -146,9 +133,8 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
 
 unsigned hoist_rewriter::mk_var(expr* e) {
     unsigned v = 0;
-    if (m_expr2var.find(e, v)) {
+    if (m_expr2var.find(e, v)) 
         return v;
-    }
     m_uf1.mk_var();
     v = m_uf2.mk_var();
     SASSERT(v == m_var2expr.size());
@@ -158,15 +144,14 @@ unsigned hoist_rewriter::mk_var(expr* e) {
 }
 
 expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
-    expr_ref result(m());
-    expr_ref_vector args(m()), fmls(m());
+    expr_ref result(m);
+    expr_ref_vector args(m), fmls(m);
     for (unsigned i = 0; i < num_args; ++i) {
         VERIFY(is_and(es[i], &m_args1));
         fmls.reset();
-        for (expr* e : m_args1) {
+        for (expr* e : m_args1) 
             if (!preds.contains(e))
                 fmls.push_back(e);
-        }
         args.push_back(::mk_and(fmls));
     }
     fmls.reset();
@@ -188,19 +173,18 @@ br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
 }
 
 bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
-    if (m().is_and(e)) {
+    if (m.is_and(e)) {
         if (args) {
             args->reset();
             args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
         }
         return true;
     }
-    if (m().is_not(e, e) && m().is_or(e)) {
+    if (m.is_not(e, e) && m.is_or(e)) {
         if (args) {
             args->reset();
-            for (expr* arg : *to_app(e)) {
-                args->push_back(::mk_not(m(), arg));
-            }
+            for (expr* arg : *to_app(e)) 
+                args->push_back(::mk_not(m, arg));
         }
         return true;
     }

src/ast/rewriter/hoist_rewriter.h

@@ -26,7 +26,7 @@ Notes:
 #include "util/obj_hashtable.h"
 
 class hoist_rewriter {
-    ast_manager &  m_manager;
+    ast_manager &                   m;
     expr_ref_vector                 m_args1, m_args2;
     obj_hashtable<expr>             m_preds1, m_preds2;
     basic_union_find                m_uf1, m_uf2, m_uf0;
@@ -34,11 +34,9 @@ class hoist_rewriter {
     svector<std::pair<expr*,expr*>> m_eqs;
     u_map<expr*>                    m_roots;
     expr_safe_replace               m_subst;
-    obj_map<expr, unsigned> m_expr2var;
-    ptr_vector<expr>        m_var2expr;
-    expr_mark               m_mark;
-
-    br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);
+    obj_map<expr, unsigned>         m_expr2var;
+    ptr_vector<expr>                m_var2expr;
+    expr_mark                       m_mark;
 
     bool is_and(expr* e, expr_ref_vector* args);
 
@@ -52,12 +50,12 @@ class hoist_rewriter {
 
 public:
     hoist_rewriter(ast_manager & m, params_ref const & p = params_ref());
-    ast_manager& m() const { return m_manager; }
-    family_id get_fid() const { return m().get_basic_family_id(); }
-    bool is_eq(expr * t) const { return m().is_eq(t); }       
+    family_id get_fid() const { return m.get_basic_family_id(); }
+    bool is_eq(expr * t) const { return m.is_eq(t); }       
     void updt_params(params_ref const & p) {}
     static void get_param_descrs(param_descrs & r) {}
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);    
+    br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);    
 };
 
 struct hoist_rewriter_cfg : public default_rewriter_cfg {

src/ast/rewriter/th_rewriter.cpp

@@ -924,6 +924,11 @@ void th_rewriter::get_param_descrs(param_descrs & r) {
     rewriter_params::collect_param_descrs(r);
 }
 
+void th_rewriter::set_flat_and_or(bool f) {
+    m_imp->cfg().m_b_rw.set_flat_and_or(f);
+}
+
+
 th_rewriter::~th_rewriter() {
     dealloc(m_imp);
 }

src/ast/rewriter/th_rewriter.h

@@ -38,6 +38,9 @@ public:
 
     void updt_params(params_ref const & p);
     static void get_param_descrs(param_descrs & r);
+
+    void set_flat_and_or(bool f);
+
     unsigned get_cache_size() const;
     unsigned get_num_steps() const;
    

src/ast/simplifiers/CMakeLists.txt

@@ -4,6 +4,7 @@ z3_add_component(simplifiers
     euf_completion.cpp
     extract_eqs.cpp
     model_reconstruction_trail.cpp
+    solve_context_eqs.cpp
     solve_eqs.cpp
   COMPONENT_DEPENDENCIES
     euf

src/ast/simplifiers/bv_slice.cpp

@@ -109,12 +109,12 @@ namespace bv {
         };
         if (lo > 0 && !b.contains(lo)) {
             b.insert(lo); 
-            if (m_num_scopes > 0)
+            if (num_scopes() > 0)
                 m_trail.push(remove_set(b, lo));
         }
         if (hi + 1 < sz && !b.contains(hi + 1)) {
             b.insert(hi + 1); 
-            if (m_num_scopes > 0)
+            if (num_scopes() > 0)
                 m_trail.push(remove_set(b, hi+ 1));
         }
     }

src/ast/simplifiers/dependent_expr.h

@@ -68,6 +68,12 @@ public:
         m_fml = nullptr;
         m_dep = nullptr;
     }
+
+    ast_manager& get_manager() const { return m; }
+
+    expr* fml() const { return m_fml; }
+
+    expr_dependency* dep() const { return m_dep; }
     
     std::tuple<expr*, expr_dependency*> operator()() const { 
         return { m_fml, m_dep }; 

src/ast/simplifiers/dependent_expr_state.h

@@ -34,6 +34,8 @@ Author:
 #include "util/params.h"
 #include "ast/converters/model_converter.h"
 #include "ast/simplifiers/dependent_expr.h"
+#include "ast/simplifiers/model_reconstruction_trail.h"
+
 
 
 /**
@@ -46,6 +48,12 @@ public:
     virtual dependent_expr const& operator[](unsigned i) = 0;
     virtual void update(unsigned i, dependent_expr const& j) = 0;
     virtual bool inconsistent() = 0;
+    virtual model_reconstruction_trail& model_trail() = 0;
+
+    trail_stack    m_trail;
+    void push() { m_trail.push_scope(); }
+    void pop(unsigned n) { m_trail.pop_scope(n); }
+
 };
 
 /**
@@ -55,20 +63,21 @@ class dependent_expr_simplifier {
 protected:
     ast_manager&          m;
     dependent_expr_state& m_fmls;
-    unsigned       m_qhead = 0;          // pointer into last processed formula in m_fmls
-    unsigned       m_num_scopes = 0;
-    trail_stack    m_trail;    
-    void advance_qhead(unsigned sz) { if (m_num_scopes > 0) m_trail.push(value_trail(m_qhead)); m_qhead = sz; }
+    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(unsigned sz) { if (num_scopes() > 0) m_trail.push(value_trail(m_qhead)); m_qhead = sz; }
 public:
-    dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s) {}
+    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 void push() { m_num_scopes++; m_trail.push_scope(); }
-    virtual void pop(unsigned n) { m_num_scopes -= n; m_trail.pop_scope(n); }
+    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 model_converter_ref get_model_converter() { return model_converter_ref(); }
 };
 
 /**

src/ast/simplifiers/euf_completion.cpp

@@ -213,7 +213,7 @@ namespace euf {
                 old_value = nullptr;
             }
         };
-        if (m_num_scopes > 0)
+        if (num_scopes() > 0)
             m_trail.push(vtrail(m_canonical, n->get_id()));
         m_canonical.setx(n->get_id(), e);
         m_epochs.setx(n->get_id(), m_epoch, 0);

src/ast/simplifiers/extract_eqs.cpp

@@ -29,22 +29,36 @@ namespace euf {
     class basic_extract_eq : public extract_eq {
         ast_manager& m;
         bool m_ite_solver = true;
+        bool m_allow_bool = true;
+
 
     public:
         basic_extract_eq(ast_manager& m) : m(m) {}
 
+        virtual void set_allow_booleans(bool f) {
+            m_allow_bool = f;
+        }
+
+
         void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
             auto [f, d] = e();
             expr* x, * y;
             if (m.is_eq(f, x, y)) {
+                if (x == y)
+                    return;
+                if (!m_allow_bool && m.is_bool(x))
+                    return;
                 if (is_uninterp_const(x))
-                    eqs.push_back(dependent_eq(to_app(x), expr_ref(y, m), d));
+                    eqs.push_back(dependent_eq(e.fml(), to_app(x), expr_ref(y, m), d));
                 if (is_uninterp_const(y))
-                    eqs.push_back(dependent_eq(to_app(y), expr_ref(x, m), d));
+                    eqs.push_back(dependent_eq(e.fml(), to_app(y), expr_ref(x, m), d));
             }
             expr* c, * th, * el, * x1, * y1, * x2, * y2;
             if (m_ite_solver && m.is_ite(f, c, th, el)) {
                 if (m.is_eq(th, x1, y1) && m.is_eq(el, x2, y2)) {
+                    if (!m_allow_bool && m.is_bool(x1))
+                        return;
+
                     if (x1 == y2 && is_uninterp_const(x1))
                         std::swap(x2, y2);
                     if (x2 == y2 && is_uninterp_const(x2))
@@ -52,13 +66,15 @@ namespace euf {
                     if (x2 == y1 && is_uninterp_const(x2))
                         std::swap(x1, y1);
                     if (x1 == x2 && is_uninterp_const(x1)) 
-                        eqs.push_back(dependent_eq(to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d));                    
+                        eqs.push_back(dependent_eq(e.fml(), to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d));
                 }
             }
+            if (!m_allow_bool)
+                return;
             if (is_uninterp_const(f))
-                eqs.push_back(dependent_eq(to_app(f), expr_ref(m.mk_true(), m), d));
+                eqs.push_back(dependent_eq(e.fml(), to_app(f), expr_ref(m.mk_true(), m), d));
             if (m.is_not(f, x) && is_uninterp_const(x))
-                eqs.push_back(dependent_eq(to_app(x), expr_ref(m.mk_false(), m), d));
+                eqs.push_back(dependent_eq(e.fml(), to_app(x), expr_ref(m.mk_false(), m), d));
         }
 
         void updt_params(params_ref const& p) {
@@ -76,7 +92,7 @@ namespace euf {
 
 
         // solve u mod r1 = y -> u = r1*mod!1 + y
-        void solve_mod(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+        void solve_mod(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
             expr* u, * z;
             rational r1, r2;
             if (!a.is_mod(x, u, z))
@@ -87,7 +103,11 @@ namespace euf {
                 return;
             expr_ref term(m);
             term = a.mk_add(a.mk_mul(z, m.mk_fresh_const("mod", a.mk_int())), y);
-            solve_eq(u, term, d, eqs);
+
+            if (is_uninterp_const(u))
+                eqs.push_back(dependent_eq(orig, to_app(u), term, d));
+            else
+                solve_eq(orig, u, term, d, eqs);
         }
 
         /***
@@ -96,7 +116,7 @@ namespace euf {
         *    -1*x + Y = Z -> x = Y - Z
         *    a*x + Y = Z  -> x = (Z - Y)/a for is-real(x)        
         */
-        void solve_add(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+        void solve_add(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
             if (!a.is_add(x))
                 return;
             expr* u, * z;
@@ -115,18 +135,18 @@ namespace euf {
             for (expr* arg : *to_app(x)) {
                 if (is_uninterp_const(arg)) {
                     mk_term(i);
-                    eqs.push_back(dependent_eq(to_app(arg), term, d));
+                    eqs.push_back(dependent_eq(orig, to_app(arg), term, d));
                 }
                 else if (a.is_mul(arg, u, z) && a.is_numeral(u, r) && is_uninterp_const(z)) {
                     if (r == -1) {
                         mk_term(i);
                         term = a.mk_uminus(term);
-                        eqs.push_back(dependent_eq(to_app(z), term, d));
+                        eqs.push_back(dependent_eq(orig, to_app(z), term, d));
                     }
                     else if (a.is_real(arg) && r != 0) {
                         mk_term(i);
                         term = a.mk_div(term, u);
-                        eqs.push_back(dependent_eq(to_app(z), term, d));
+                        eqs.push_back(dependent_eq(orig, to_app(z), term, d));
                     }
                 }
                 else if (a.is_real(arg) && a.is_mul(arg)) {
@@ -155,7 +175,7 @@ namespace euf {
                         }
                         mk_term(i);
                         term = a.mk_div(term, a.mk_mul(args.size(), args.data()));
-                        eqs.push_back(dependent_eq(to_app(xarg), term, d));
+                        eqs.push_back(dependent_eq(orig, to_app(xarg), term, d));
                     }
                 }
                 ++i;
@@ -165,7 +185,7 @@ namespace euf {
         /***
         * Solve for x * Y = Z, where Y != 0 -> x = Z / Y
         */
-        void solve_mul(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+        void solve_mul(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
             if (!a.is_mul(x))
                 return;
             rational r;
@@ -175,6 +195,8 @@ namespace euf {
                 ++i;
                 if (!is_uninterp_const(arg))
                     continue;
+                if (!a.is_real(arg))
+                    continue;
                 unsigned j = 0;
                 bool nonzero = true;
                 for (expr* arg2 : *to_app(x)) {
@@ -193,7 +215,7 @@ namespace euf {
                         args.push_back(arg2);
                 }
                 term = a.mk_div(y, a.mk_mul(args));
-                eqs.push_back(dependent_eq(to_app(arg), term, d));
+                eqs.push_back(dependent_eq(orig, to_app(arg), term, d));
             }
         }
 
@@ -214,22 +236,24 @@ namespace euf {
             }
         }
 
-        void solve_eq(expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
-            solve_add(x, y, d, eqs);
-            solve_mod(x, y, d, eqs);
-            solve_mul(x, y, d, eqs);
+        void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) {
+            solve_add(orig, x, y, d, eqs);
+            solve_mod(orig, x, y, d, eqs);
+            solve_mul(orig, x, y, d, eqs);
         }
 
     public:
+
         arith_extract_eq(ast_manager& m) : m(m), a(m), m_args(m) {}
+
         void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
             if (!m_enabled)
                 return;
             auto [f, d] = e();
             expr* x, * y;
             if (m.is_eq(f, x, y) && a.is_int_real(x)) {
-                solve_eq(x, y, d, eqs);
-                solve_eq(y, x, d, eqs);
+                solve_eq(f, x, y, d, eqs);
+                solve_eq(f, y, x, d, eqs);
             }
         }
 
@@ -237,10 +261,8 @@ namespace euf {
             if (!m_enabled)
                 return;
             m_nonzero.reset();
-            for (unsigned i = 0; i < fmls.size(); ++i) {
-                auto [f, d] = fmls[i]();
-                add_pos(f);
-            }
+            for (unsigned i = 0; i < fmls.size(); ++i) 
+                add_pos(fmls[i].fml());            
         }
 
 

src/ast/simplifiers/extract_eqs.h

@@ -18,6 +18,8 @@ Author:
 
 #pragma once
 
+
+#include "ast/ast_pp.h"
 #include "ast/simplifiers/dependent_expr_state.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/expr_substitution.h"
@@ -27,10 +29,11 @@ Author:
 namespace euf {
 
     struct dependent_eq {
-        app* var;
-        expr_ref term;
+        expr* orig;       // original expression that encoded equation
+        app* var;         // isolated variable
+        expr_ref term;    // defined term
         expr_dependency* dep;
-        dependent_eq(app* var, expr_ref const& term, expr_dependency* d) : var(var), term(term), dep(d) {}
+        dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : orig(orig), var(var), term(term), dep(d) {}
     };
 
     typedef vector<dependent_eq> dep_eq_vector;
@@ -41,8 +44,13 @@ namespace euf {
         virtual void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) = 0;
         virtual void pre_process(dependent_expr_state& fmls) {}
         virtual void updt_params(params_ref const& p) {}
+        virtual void set_allow_booleans(bool f) {}
     };
 
     void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex);
 
 }
+
+inline std::ostream& operator<<(std::ostream& out, euf::dependent_eq const& eq) {
+    return out << mk_pp(eq.var, eq.term.m()) << " = " << eq.term << "\n";
+}

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -21,24 +21,84 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
     // accumulate a set of dependent exprs, updating m_trail to exclude loose 
     // substitutions that use variables from the dependent expressions.
     ast_mark free_vars;
-    auto [f, dep] = d();
-    for (expr* t : subterms::all(expr_ref(f, m))) 
-        free_vars.mark(t, true);
-    
-    NOT_IMPLEMENTED_YET();
+    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
+    add_vars(d, free_vars);
+
+    added.push_back(d);
+
+    for (auto& t : m_trail) {
+        if (!t->m_active)
+            continue;
+
+        // updates that have no intersections with current variables are skipped
+        if (!t->intersects(free_vars)) 
+            continue;        
+
+        // loose entries that intersect with free vars are deleted from the trail
+        // and their removed formulas are added to the resulting constraints.
+        if (t->is_loose()) {
+            added.append(t->m_removed); 
+            for (auto r : t->m_removed) 
+                add_vars(r, free_vars);            
+            m_trail_stack.push(value_trail(t->m_active));
+            t->m_active = false;      
+            continue;
+        }
+        
+        rp->set_substitution(t->m_subst.get());
+        // rigid entries:
+        // apply substitution to added in case of rigid model convertions
+        for (auto& d : added) {
+            auto [f, dep1] = d();
+            auto [g, dep2] = rp->replace_with_dep(f);
+            d = dependent_expr(m, g, m.mk_join(dep1, dep2));
+        }    
+    }
 }
 
 /**
  * retrieve the current model converter corresponding to chaining substitutions from the trail.
  */
 model_converter_ref model_reconstruction_trail::get_model_converter() {
-    model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
+
+
+    //
     // walk the trail from the back
     // add substitutions from the back to the generic model converter
     // after they have been normalized using a global replace that replaces 
     // substituted variables by their terms.
-    NOT_IMPLEMENTED_YET();
-    return mc;
+    //
 
+    
+    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
+    expr_substitution subst(m, true, false);
+    rp->set_substitution(&subst);
+    generic_model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
+    bool first = true;
+    for (unsigned i = m_trail.size(); i-- > 0; ) {
+        auto* t = m_trail[i];
+        if (!t->m_active)
+            continue;
+
+        if (first) {
+            first = false;
+            for (auto const& [v, def] : t->m_subst->sub()) {
+                expr_dependency* dep = t->m_subst->dep(v);
+                subst.insert(v, def, dep);
+                mc->add(v, def);
+            }
+            continue;
+        }
+
+        for (auto const& [v, def] : t->m_subst->sub()) {
+            auto [new_def, new_dep] = rp->replace_with_dep(def);
+            expr_dependency* dep = t->m_subst->dep(v);
+            new_dep = m.mk_join(dep, new_dep);
+            subst.insert(v, new_def, new_dep);
+            mc->add(v, new_def);
+        }
+
+    }
+    return model_converter_ref(mc.get());
 }
 

src/ast/simplifiers/model_reconstruction_trail.h

@@ -24,33 +24,64 @@ Author:
 #pragma once
 
 #include "util/scoped_ptr_vector.h"
+#include "util/trail.h"
+#include "ast/for_each_expr.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/simplifiers/dependent_expr.h"
 #include "ast/converters/model_converter.h"
 
 class model_reconstruction_trail {
 
-    ast_manager& m;
+    struct entry {
+        scoped_ptr<expr_substitution> m_subst;
+        vector<dependent_expr>        m_removed;
+        bool                          m_active = true;
+
+        entry(expr_substitution* s, vector<dependent_expr> const& rem) :
+            m_subst(s), m_removed(rem) {}
+
+        bool is_loose() const { return !m_removed.empty(); }
+
+        bool intersects(ast_mark const& free_vars) const {
+            for (auto const& [k, v] : m_subst->sub())
+                if (free_vars.is_marked(k))
+                    return true;
+            return false;
+        }
+
 
-    struct model_reconstruction_trail_entry {
-        scoped_ptr<expr_replacer> m_replace;
-        vector<dependent_expr>    m_removed;
-        model_reconstruction_trail_entry(expr_replacer* r, vector<dependent_expr> const& rem) :
-            m_replace(r), m_removed(rem) {}
     };
 
-    scoped_ptr_vector<model_reconstruction_trail_entry> m_trail;
-    unsigned_vector m_limit;
+    ast_manager&             m;
+    trail_stack&             m_trail_stack;
+    scoped_ptr_vector<entry> m_trail;
+
+    void add_vars(dependent_expr const& d, ast_mark& free_vars) {
+        for (expr* t : subterms::all(expr_ref(d.fml(), d.get_manager())))
+            free_vars.mark(t, true);
+    }
+
+    bool intersects(ast_mark const& free_vars, dependent_expr const& d) {
+        expr_ref term(d.fml(), d.get_manager());
+        auto iter = subterms::all(term);
+        return any_of(iter, [&](expr* t) { return free_vars.is_marked(t); });
+    }
+
+    bool intersects(ast_mark const& free_vars, vector<dependent_expr> const& added) {
+        return any_of(added, [&](dependent_expr const& d) { return intersects(free_vars, d); });
+    }
 
 public:
 
-    model_reconstruction_trail(ast_manager& m) : m(m) {}
+    model_reconstruction_trail(ast_manager& m, trail_stack& tr): 
+        m(m), m_trail_stack(tr) {}
 
     /**
-    * add a new substitution to the stack
+    * add a new substitution to the trail
     */
-    void push(expr_replacer* r, vector<dependent_expr> const& removed) {
-        m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed));
+    void push(expr_substitution* s, vector<dependent_expr> const& removed) {
+        m_trail.push_back(alloc(entry, s, removed));
+        m_trail_stack.push(push_back_vector(m_trail));
     }
 
     /**
@@ -63,18 +94,5 @@ public:
     * retrieve the current model converter corresponding to chaining substitutions from the trail.
     */
     model_converter_ref get_model_converter();
-
-    /**
-    * push a context. Portions of the trail added within a context are removed after a context pop.
-    */
-    void push() {
-        m_limit.push_back(m_trail.size());
-    }
-
-    void pop(unsigned n) {
-        unsigned old_sz = m_limit[m_limit.size() - n];
-        m_trail.resize(old_sz);
-        m_limit.shrink(m_limit.size() - n);
-    }
 };
 

src/ast/simplifiers/solve_context_eqs.cpp

@@ -0,0 +1,239 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    solve_context_eqs.cpp
+
+Abstract:
+
+    simplifier for solving equations within a context
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+Notes:
+
+The variable v is solved based on expression e.
+Check that every occurrence of v uses e in conjunctive context.
+     
+Walk formulas containing v in as and-or.
+Equalities that occur within at least one alternation of or are
+considered as candidates.
+     
+To constrain how formulas are traversed, first
+label sub-expressions that contain v. An equality eq is safe for v
+if every occurrence of v occurs in the same conjunctive context as eq.
+
+--*/
+
+#include "ast/ast.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/occurs.h"
+#include "ast/simplifiers/solve_context_eqs.h"
+#include "ast/simplifiers/solve_eqs.h"
+
+namespace euf {
+
+        
+    solve_context_eqs::solve_context_eqs(solve_eqs& s): m(s.m), m_fmls(s.m_fmls), m_solve_eqs(s) {}
+
+    bool solve_context_eqs::is_safe_eq(expr* e) {
+        m_and_pos.reset(); m_and_neg.reset(); m_or_pos.reset(); m_or_neg.reset();        
+        for (unsigned i = 0; i < m_fmls.size(); ++i)
+            if (!is_safe_eq(m_fmls[i].fml(), e))
+                return false;
+        return true;
+    }
+
+    /**
+    * Check if some conjunction of f contains equality 'e'.
+    * If this is not the case, then check that every conjunct that contains v
+    * recursively contains a disjunction that contains 'e'.
+    */
+    bool solve_context_eqs::is_safe_eq(unsigned recursion_depth, expr* f, bool sign, expr* e) {
+        if (!contains_v(f))
+            return true;                
+        signed_expressions conjuncts;
+        if (contains_conjunctively(f, sign, e, conjuncts)) 
+            return true;
+        if (recursion_depth > 3)
+            return false;
+        return all_of(conjuncts, [&](std::pair<bool,expr*> const& p) { return is_disjunctively_safe(recursion_depth, p.second, p.first, e); });
+    }
+
+    /*
+    * Every disjunction in f that contains v also contains the equation e.
+    */
+    bool solve_context_eqs::is_disjunctively_safe(unsigned recursion_depth, expr* f0, bool sign, expr* e) {
+        signed_expressions todo;
+        todo.push_back({sign, f0});
+        while (!todo.empty()) {
+            auto [s, f] = todo.back();
+            todo.pop_back();
+            if (s && m_or_neg.is_marked(f))
+                continue;
+            if (!s && m_or_pos.is_marked(f))
+                continue;
+            if (s)
+                m_or_neg.mark(f, true);
+            else
+                m_or_pos.mark(f, true);
+            if (!s && f == e)
+                continue;
+            else if (!contains_v(f))
+                continue;
+            else if (s && m.is_and(f)) 
+                for (auto* arg : *to_app(f))
+                    todo.push_back({s, arg});            
+            else if (!s && m.is_or(f)) 
+                for (auto* arg : *to_app(f))
+                    todo.push_back({s, arg});            
+            else if (m.is_not(f, f))
+                todo.push_back({!s, f});
+            else if (!is_conjunction(s, f))
+                return false;
+            else if (!is_safe_eq(recursion_depth + 1, f, s, e))
+                return false;
+        }
+        return true;
+    }
+
+    bool solve_context_eqs::is_conjunction(bool sign, expr* f) const {
+        if (!sign && m.is_and(f))
+            return true;
+        if (sign && m.is_or(f))
+            return true;
+        return false;
+    }
+   
+    /**
+    * Determine whether some conjunction in f contains e. 
+    * If no conjunction contains e, then return the set of conjunctions that contain v.
+    */
+    bool solve_context_eqs::contains_conjunctively(expr* f, bool sign, expr* e, signed_expressions& conjuncts) {
+        signed_expressions todo;
+        todo.push_back({sign, f});
+        while (!todo.empty()) {
+            auto [s, f] = todo.back();
+            todo.pop_back();
+            if (!s && f == e)
+                return true;
+            if (!s && m_and_pos.is_marked(f))
+                continue;
+            if (s && m_and_neg.is_marked(f))
+                continue;
+            if (s)
+                m_and_neg.mark(f, true);
+            else
+                m_and_pos.mark(f, true);
+            if (!contains_v(f))
+                continue;
+            if (!s && m.is_and(f)) 
+                for (auto* arg : *to_app(f))
+                    todo.push_back({false, arg});            
+            else if (s && m.is_or(f)) 
+                for (auto* arg : *to_app(f))
+                    todo.push_back({true, arg});            
+            else if (m.is_not(f, f))
+                todo.push_back({!s, f});
+            else
+                conjuncts.push_back({s, f});
+        }
+        return false;
+    }
+
+    void solve_context_eqs::collect_nested_equalities(dep_eq_vector& eqs) {
+        expr_mark visited;
+        for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i)
+            collect_nested_equalities(m_fmls[i], visited, eqs);
+
+        std::stable_sort(eqs.begin(), eqs.end(), [&](dependent_eq const& e1, dependent_eq const& e2) {
+                return e1.var->get_id() < e2.var->get_id(); });
+        unsigned j = 0;
+        expr* last_var = nullptr;
+        for (auto const& eq : eqs) {
+
+            SASSERT(!m.is_bool(eq.var));
+
+            if (eq.var != last_var) {
+
+                m_contains_v.reset();
+                
+                // first check if v is in term. If it is, then the substitution candidate is unsafe
+                m_todo.push_back(eq.term);
+                mark_occurs(m_todo, eq.var, m_contains_v);
+                SASSERT(m_todo.empty());
+                last_var = eq.var;
+                if (m_contains_v.is_marked(eq.term))
+                    continue;
+
+                // then mark occurrences
+                for (unsigned i = 0; i < m_fmls.size(); ++i)
+                    m_todo.push_back(m_fmls[i].fml());
+                mark_occurs(m_todo, eq.var, m_contains_v);
+                SASSERT(m_todo.empty());
+            }
+            else if (m_contains_v.is_marked(eq.term))
+                continue;
+
+            // subject to occurrences, check if equality is safe
+            if (is_safe_eq(eq.orig)) 
+                eqs[j++] = eq;
+        }
+        eqs.shrink(j);
+        TRACE("solve_eqs",
+              for (auto const& eq : eqs)
+                  tout << eq << "\n");
+    }
+
+    void solve_context_eqs::collect_nested_equalities(dependent_expr const& df, expr_mark& visited, dep_eq_vector& eqs) {
+
+        svector<std::tuple<bool,unsigned,expr*>> todo;
+        todo.push_back({ false, 0, df.fml()});
+
+        // even depth is conjunctive context, odd is disjunctive
+        // when alternating between conjunctive and disjunctive context, increment depth.
+        auto inc_or = [](unsigned depth) {
+            return (0 == depth % 2) ? depth + 1 : depth;
+        };
+        auto inc_and = [](unsigned depth) {
+            return (0 == depth % 2) ? depth : depth + 1;
+        };
+
+        while (!todo.empty()) {
+            auto [s, depth, f] = todo.back();
+            todo.pop_back();
+            if (visited.is_marked(f))
+                continue;
+            visited.mark(f, true);
+            if (s && m.is_and(f)) {
+                for (auto* arg : *to_app(f))
+                    todo.push_back({ s, inc_or(depth), arg });
+            }
+            else if (!s && m.is_or(f)) {
+                for (auto* arg : *to_app(f))
+                    todo.push_back({ s, inc_or(depth), arg });
+            }
+            if (!s && m.is_and(f)) {
+                for (auto* arg : *to_app(f))
+                    todo.push_back({ s, inc_and(depth), arg });
+            }
+            else if (s && m.is_or(f)) {
+                for (auto* arg : *to_app(f))
+                    todo.push_back({ s, inc_and(depth), arg });
+            }
+            else if (m.is_not(f, f))
+                todo.push_back({ !s, depth, f });
+            else if (!s && 1 == depth % 2) {
+                for (extract_eq* ex : m_solve_eqs.m_extract_plugins) {
+                    ex->set_allow_booleans(false);
+                    ex->get_eqs(dependent_expr(m, f, df.dep()), eqs);
+                    ex->set_allow_booleans(true);
+                }
+            }
+        }
+    }
+}

src/ast/simplifiers/solve_context_eqs.h

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    solve_context_eqs.h
+
+Abstract:
+
+    simplifier for solving equations within a context
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/simplifiers/extract_eqs.h"
+
+namespace euf {
+
+    class solve_eqs;
+    
+
+    class solve_context_eqs {
+
+        ast_manager&              m;
+        dependent_expr_state&     m_fmls;
+        solve_eqs&                m_solve_eqs;
+        expr_mark                 m_and_pos, m_and_neg, m_or_pos, m_or_neg;
+        expr_mark                 m_contains_v;
+        ptr_vector<expr>          m_todo;
+
+        typedef svector<std::pair<bool, expr*>> signed_expressions;
+
+        bool contains_v(expr* f) const { return m_contains_v.is_marked(f); }
+        bool is_safe_eq(expr* e);
+        bool is_safe_eq(unsigned recursion_depth, expr* f, bool sign, expr* e);
+        bool is_safe_eq(expr* f, expr* e) { return is_safe_eq(0, f, false, e); }
+        bool is_disjunctively_safe(unsigned recursion_depth, expr* f, bool sign, expr* e);
+        bool contains_conjunctively(expr* f, bool sign, expr* e, signed_expressions& conjuncts);
+        bool is_conjunction(bool sign, expr* f) const;
+        
+        void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs);        
+
+    public:
+        
+        solve_context_eqs(solve_eqs& s);
+
+        void collect_nested_equalities(dep_eq_vector& eqs);
+
+    };
+}

src/ast/simplifiers/solve_eqs.cpp

@@ -20,25 +20,35 @@ Author:
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/occurs.h"
 #include "ast/recfun_decl_plugin.h"
 #include "ast/rewriter/expr_replacer.h"
 #include "ast/simplifiers/solve_eqs.h"
+#include "ast/simplifiers/solve_context_eqs.h"
 #include "ast/converters/generic_model_converter.h"
 #include "params/tactic_params.hpp"
 
 
 namespace euf {
 
+
+    void solve_eqs::get_eqs(dep_eq_vector& eqs) {
+        for (extract_eq* ex : m_extract_plugins)
+            for (unsigned i = m_qhead; i < m_fmls.size(); ++i)
+                ex->get_eqs(m_fmls[i], eqs);
+    }
+
     // initialize graph that maps variable ids to next ids
     void solve_eqs::extract_dep_graph(dep_eq_vector& eqs) {
         m_var2id.reset();
         m_id2var.reset();
         m_next.reset();
         unsigned sz = 0;
-        for (auto const& [v, t, d] : eqs)
+        for (auto const& [orig, v, t, d] : eqs)
             sz = std::max(sz, v->get_id());
         m_var2id.resize(sz + 1, UINT_MAX);
-        for (auto const& [v, t, d] : eqs) {
+        for (auto const& [orig, v, t, d] : eqs) {
             if (is_var(v) || !can_be_var(v))
                 continue;
             m_var2id[v->get_id()] = m_id2var.size();
@@ -60,16 +70,17 @@ namespace euf {
         m_id2level.reset();
         m_id2level.resize(m_id2var.size(), UINT_MAX);
         m_subst_ids.reset();
-        m_subst = alloc(expr_substitution, m, false, false);
+
+        m_subst = alloc(expr_substitution, m, true, false);        
 
         auto is_explored = [&](unsigned id) {
             return m_id2level[id] != UINT_MAX;
         };
 
         auto is_safe = [&](unsigned lvl, expr* t) {
-            for (auto* e : subterms::all(expr_ref(t, m)))
+            for (auto* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited)) 
                 if (is_var(e) && m_id2level[var2id(e)] < lvl)
-                    return false;
+                    return false;            
             return true;
         };
 
@@ -89,14 +100,17 @@ namespace euf {
                 todo.pop_back();
                 if (is_explored(j))
                     continue;
-                m_id2level[id] = curr_level++;
+
+                m_id2level[j] = curr_level++;
                 for (auto const& eq : m_next[j]) {
-                    auto const& [v, t, d] = eq;
+                    auto const& [orig, v, t, d] = eq;
+                    SASSERT(j == var2id(v));
                     if (!is_safe(curr_level, t))
                         continue;
+                    SASSERT(!occurs(v, t));
                     m_next[j][0] = eq;
-                    m_subst_ids.push_back(id);                   
-                    for (expr* e : subterms::all(expr_ref(t, m))) 
+                    m_subst_ids.push_back(j);                   
+                    for (expr* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited))
                         if (is_var(e) && !is_explored(var2id(e))) 
                             todo.push_back(var2id(e));   
                     break;
@@ -105,31 +119,25 @@ namespace euf {
         }
     }
 
-    void solve_eqs::add_subst(dependent_eq const& eq) {
-        SASSERT(can_be_var(eq.var));
-        m_subst->insert(eq.var, eq.term, nullptr, eq.dep);
-        ++m_stats.m_num_elim_vars;
-    }
-
     void solve_eqs::normalize() {
-        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
-        m_subst->reset();
+        if (m_subst_ids.empty())
+            return;
+        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
         rp->set_substitution(m_subst.get());
 
         std::sort(m_subst_ids.begin(), m_subst_ids.end(), [&](unsigned u, unsigned v) { return m_id2level[u] > m_id2level[v]; });
 
-        expr_dependency_ref new_dep(m);
-        expr_ref new_def(m);
-        proof_ref new_pr(m);
-
         for (unsigned id : m_subst_ids) {
             if (!m.inc())
-                break;
-            auto const& [v, def, dep] = m_next[id][0];
-            rp->operator()(def, new_def, new_pr, new_dep);
+                return;
+            auto const& [orig, v, def, dep] = m_next[id][0];
+            auto [new_def, new_dep] = rp->replace_with_dep(def);
             m_stats.m_num_steps += rp->get_num_steps() + 1;
+            ++m_stats.m_num_elim_vars;
             new_dep = m.mk_join(dep, new_dep);
-            m_subst->insert(v, new_def, new_pr, new_dep);
+            IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(v, m) << " -> " << mk_bounded_pp(new_def, m) << "\n");
+            m_subst->insert(v, new_def, new_dep);
+            SASSERT(can_be_var(v));
             // we updated the substitution, but we don't need to reset rp
             // because all cached values there do not depend on v.
         }
@@ -141,22 +149,27 @@ namespace euf {
             expr* def = m_subst->find(eq.var);
             tout << mk_pp(eq.var, m) << "\n----->\n" << mk_pp(def, m) << "\n\n";
         });
+
+
     }
 
-    void solve_eqs::apply_subst() {
+    void solve_eqs::apply_subst(vector<dependent_expr>& old_fmls) {
         if (!m.inc())
             return;
-        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
+        if (m_subst_ids.empty())
+            return;
+        
+        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
         rp->set_substitution(m_subst.get());
-        expr_ref new_f(m);
-        proof_ref new_pr(m);
-        expr_dependency_ref new_dep(m);
+
         for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) {
             auto [f, d] = m_fmls[i]();
-            rp->operator()(f, new_f, new_pr, new_dep);
+            auto [new_f, new_dep] = rp->replace_with_dep(f);
+            m_rewriter(new_f);
             if (new_f == f)
                 continue;
             new_dep = m.mk_join(d, new_dep);
+            old_fmls.push_back(m_fmls[i]);
             m_fmls.update(i, dependent_expr(m, new_f, new_dep));
         }
     }
@@ -166,37 +179,60 @@ namespace euf {
         for (extract_eq* ex : m_extract_plugins)
             ex->pre_process(m_fmls);
 
-        // TODO add a loop.
+
+        unsigned count = 0;
+        vector<dependent_expr> old_fmls;
         dep_eq_vector eqs;
-        get_eqs(eqs);
-        extract_dep_graph(eqs);
-        extract_subst();
-        apply_subst();
+        do {
+            old_fmls.reset();
+            m_subst_ids.reset();
+            eqs.reset();
+            get_eqs(eqs);
+            extract_dep_graph(eqs);
+            extract_subst();
+            normalize();
+            apply_subst(old_fmls);
+            ++count;
+            save_subst({});
+        } 
+        while (!m_subst_ids.empty() && count < 20 && m.inc());
+
+        if (!m.inc())
+            return;
+
+        if (m_config.m_context_solve) {            
+            old_fmls.reset();
+            m_subst_ids.reset();
+            eqs.reset();
+            solve_context_eqs context_solve(*this);
+            context_solve.collect_nested_equalities(eqs);
+            extract_dep_graph(eqs);
+            extract_subst();
+            normalize();
+            apply_subst(old_fmls);
+            save_subst(old_fmls);
+        }
+
         advance_qhead(m_fmls.size());
     }
 
+    void solve_eqs::save_subst(vector<dependent_expr> const& old_fmls) {
+        if (!m_subst->empty())   
+            m_fmls.model_trail().push(m_subst.detach(), old_fmls);                
+    }
+
     void solve_eqs::filter_unsafe_vars() {
         m_unsafe_vars.reset();
         recfun::util rec(m);
         for (func_decl* f : rec.get_rec_funs())
-            for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m)))
+            for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m), &m_todo, &m_visited))
                 m_unsafe_vars.mark(term);
     }
 
-    typedef generic_model_converter gmc;
-
-    model_converter_ref solve_eqs::get_model_converter() {
-        model_converter_ref mc = alloc(gmc, m, "solve-eqs");
-        for (unsigned id : m_subst_ids) {
-            auto* v = m_id2var[id];
-            static_cast<gmc*>(mc.get())->add(v, m_subst->find(v));
-        }
-        return mc;
-    }
-
     solve_eqs::solve_eqs(ast_manager& m, dependent_expr_state& fmls) : 
         dependent_expr_simplifier(m, fmls), m_rewriter(m) {
         register_extract_eqs(m, m_extract_plugins);
+        m_rewriter.set_flat_and_or(false);
     }
 
     void solve_eqs::updt_params(params_ref const& p) {

src/ast/simplifiers/solve_eqs.h

@@ -26,6 +26,9 @@ Author:
 namespace euf {
 
     class solve_eqs : public dependent_expr_simplifier {
+
+        friend class solve_context_eqs;
+
         struct stats {
             unsigned m_num_steps = 0;
             unsigned m_num_elim_vars = 0;
@@ -35,50 +38,43 @@ namespace euf {
             unsigned m_max_occs = UINT_MAX;
         };
 
-        th_rewriter                   m_rewriter;
-        scoped_ptr_vector<extract_eq> m_extract_plugins;
-        unsigned_vector               m_var2id, m_id2level, m_subst_ids;
-        ptr_vector<app>               m_id2var;
-        vector<dep_eq_vector>         m_next;  
-        scoped_ptr<expr_substitution> m_subst;
 
-        expr_mark                     m_unsafe_vars;   // expressions that cannot be replaced
         stats                         m_stats;
         config                        m_config;
-
-        void add_subst(dependent_eq const& eq);
+        th_rewriter                   m_rewriter;
+        scoped_ptr_vector<extract_eq> m_extract_plugins;
+        unsigned_vector               m_var2id;        // app->get_id() |-> small numeral
+        ptr_vector<app>               m_id2var;        // small numeral |-> app
+        unsigned_vector               m_id2level;      // small numeral |-> level in substitution ordering
+        unsigned_vector               m_subst_ids;     // sorted list of small numeral by level
+        vector<dep_eq_vector>         m_next;          // adjacency list for solved equations
+        scoped_ptr<expr_substitution> m_subst;         // current substitution
+        expr_mark                     m_unsafe_vars;   // expressions that cannot be replaced
+        ptr_vector<expr>              m_todo;
+        expr_mark                     m_visited;
 
         bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; }
         unsigned var2id(expr* v) const { return m_var2id[v->get_id()]; }
-
-        void get_eqs(dep_eq_vector& eqs) {
-            for (unsigned i = m_qhead; i < m_fmls.size(); ++i) 
-                get_eqs(m_fmls[i], eqs);            
-        }
-
-        void get_eqs(dependent_expr const& f, dep_eq_vector& eqs) {
-            for (extract_eq* ex : m_extract_plugins)
-                ex->get_eqs(f, eqs);
-        }
-
-        void filter_unsafe_vars();
         bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); }
+        void get_eqs(dep_eq_vector& eqs);
+        void filter_unsafe_vars();        
         void extract_subst();
         void extract_dep_graph(dep_eq_vector& eqs);
         void normalize();
-        void apply_subst();
+        void apply_subst(vector<dependent_expr>& old_fmls);
+        void save_subst(vector<dependent_expr> const& old_fmls);
+
 
     public:
 
         solve_eqs(ast_manager& m, dependent_expr_state& fmls);
 
-        void push() override { dependent_expr_simplifier::push(); }
-        void pop(unsigned n) override { dependent_expr_simplifier::pop(n); }
+
         void reduce() override;
 
         void updt_params(params_ref const& p) override;
+
         void collect_statistics(statistics& st) const override;
 
-        model_converter_ref get_model_converter() override;
     };
 }

src/muz/fp/datalog_parser.cpp

@@ -286,9 +286,8 @@ public:
 
 
     dtoken read_num() {
-        while(isdigit(m_curr_char)) {
+        while (isdigit(m_curr_char)) 
             save_and_next();
-        }        
         return TK_NUM;
     }
 
@@ -781,15 +780,29 @@ protected:
         symbol td1(td);
         expr_ref v1(m), v2(m);
         sort* s = nullptr;
-        dtoken tok2 = m_lexer->next_token();
-        if (tok2 != TK_NEQ && tok2 != TK_GT && tok2 != TK_LT && tok2 != TK_EQ) {
-            return unexpected(tok2, "built-in infix operator");
+        uint64_t num1(0), num3(0);
+        if (tok1 == TK_NUM) {
+            char const* data = m_lexer->get_token_data();
+            rational num(data);
+            if (!num.is_uint64()) 
+                return unexpected(tok1, "integer expected");
+            num1 = num.get_uint64();
         }
+        dtoken tok2 = m_lexer->next_token();
+        if (tok2 != TK_NEQ && tok2 != TK_GT && tok2 != TK_LT && tok2 != TK_EQ) 
+            return unexpected(tok2, "built-in infix operator");
         dtoken tok3 = m_lexer->next_token();
         td = m_lexer->get_token_data();
-        if (tok3 != TK_STRING && tok3 != TK_NUM && !(tok3 == TK_ID && m_vars.contains(td))) {
+        if (tok3 != TK_STRING && tok3 != TK_NUM && !(tok3 == TK_ID && m_vars.contains(td))) 
             return unexpected(tok3, "identifier");
+        if (tok3 == TK_NUM) {
+            char const* data = m_lexer->get_token_data();
+            rational num(data);
+            if (!num.is_uint64()) 
+                return unexpected(tok1, "integer expected");
+            num3 = num.get_uint64();
         }
+        
         symbol td2(td);
 
         if (tok1 == TK_ID) {
@@ -805,18 +818,21 @@ protected:
         if (!v1 && !v2) {
             return unexpected(tok3, "at least one argument should be a variable");
         }
-        if (v1) {
+        if (v1) 
             s = v1->get_sort();
-        }        
-        else {
+        else 
             s = v2->get_sort();
-        }
-        if (!v1) {
+         
+        if (tok1 == TK_NUM) 
+            v1 = mk_symbol_const(num1, s);
+
+        if (tok3 == TK_NUM)
+            v2 = mk_symbol_const(num3, s);
+        
+        if (!v1) 
             v1 = mk_const(td1, s);
-        }
-        if (!v2) {
+        if (!v2) 
             v2 = mk_const(td2, s);
-        }
 
         switch(tok2) {
         case TK_EQ:
@@ -1126,8 +1142,11 @@ protected:
         if (m_arith.is_int(s)) 
             return m_arith.mk_numeral(rational(el, rational::ui64()), s);
         else if (m_decl_util.try_get_size(s, sz)) {
-            if (el >= sz)
-                throw default_exception("numeric value out of bounds of domain");
+            if (el >= sz) {
+                std::ostringstream ous;
+                ous << "numeric value " << el << " is out of bounds of domain size " << sz;
+                throw default_exception(ous.str());
+            }
             return m_decl_util.mk_numeral(el, s);
         }
         else {

src/muz/spacer/spacer_iuc_solver.cpp

@@ -244,12 +244,10 @@ namespace spacer {
     }
     
     void iuc_solver::elim_proxies (expr_ref_vector &v) {
-        expr_ref f = mk_and (v);
         scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer (m);
         rep->set_substitution (&m_elim_proxies_sub);
-        (*rep)(f);
-        v.reset();
-        flatten_and(f, v);
+        (*rep)(v);
+        flatten_and(v);
     }
     
     void iuc_solver::get_iuc(expr_ref_vector &core) {

src/nlsat/tactic/qfnra_nlsat_tactic.cpp

@@ -27,6 +27,7 @@ Notes:
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_term_ite_tactic.h"
 
 tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {

src/opt/opt_context.cpp

@@ -31,6 +31,7 @@ Notes:
 #include "tactic/tactic.h"
 #include "tactic/arith/lia2card_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"

src/params/bool_rewriter_params.pyg

@@ -1,8 +1,9 @@
 def_module_params(module_name='rewriter',
                   class_name='bool_rewriter_params',
                   export=True,
-                  params=(("ite_extra_rules", BOOL, False, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"),
-                          ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"),
+                  params=(("ite_extra_rules", BOOL, True, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"),
+                          ("flat", BOOL, True, "create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor"),
+                          ("flat_and_or", BOOL, True, "create nary applications for and,or"),
                           ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"),
                           ('elim_ite', BOOL, True,  "eliminate ite in favor of and/or"),
                           ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"),

src/sat/sat_config.cpp

@@ -46,7 +46,7 @@ namespace sat {
         else if (s == symbol("static"))
             m_restart = RS_STATIC;
         else
-            throw sat_param_exception("invalid restart strategy");
+            throw sat_param_exception("invalid restart strategy. Use ema (default), luby, geometric, static");
 
         m_fast_glue_avg = p.restart_emafastglue();
         m_slow_glue_avg = p.restart_emaslowglue();

src/sat/sat_solver.h

@@ -353,10 +353,8 @@ namespace sat {
         void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); }
         bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); }
         bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); }
-        unsigned num_visited(bool_var v) const { return m_visited.num_visited(v); }
         void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); }
         void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
-        void inc_visited(bool_var v) { m_visited.inc_visited(v); }
         bool all_distinct(literal_vector const& lits);
         bool all_distinct(clause const& cl);
 

src/smt/smt_clause_proof.cpp

@@ -147,18 +147,22 @@ namespace smt {
         for (auto& info : m_trail) {
             expr_ref fact = mk_or(info.m_clause);
             proof* pr = info.m_proof;
+            expr* args[2] = { pr, fact };
+            unsigned num_args = 2, offset = 0;
+            if (!pr) 
+                offset = 1;
             switch (info.m_status) {
             case status::assumption:
-                ps.push_back(m.mk_assumption_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("assumption"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::lemma:
-                ps.push_back(m.mk_lemma_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("lemma"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::th_assumption:
-                ps.push_back(m.mk_th_assumption_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("th-assumption"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::th_lemma:
-                ps.push_back(m.mk_th_lemma_add(pr, fact)); 
+                ps.push_back(m.mk_app(symbol("th-lemma"), num_args - offset, args + offset, m.mk_proof_sort()));
                 break;
             case status::deleted:
                 ps.push_back(m.mk_redundant_del(fact));

src/smt/smt_internalizer.cpp

@@ -1593,6 +1593,18 @@ namespace smt {
             TRACE("gate_clause", tout << mk_ll_pp(pr, m););
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }
+        else if (m_clause_proof.on_clause_active()) {
+            ptr_buffer<expr> new_lits;
+            for (unsigned i = 0; i < num_lits; i++) {
+                literal l      = lits[i];
+                bool_var v     = l.var();
+                expr * atom    = m_bool_var2expr[v]; 
+                new_lits.push_back(l.sign() ? m.mk_not(atom) : atom);
+            }
+            // expr* fact = m.mk_or(new_lits);
+            proof* pr = m.mk_app(symbol("tseitin"), new_lits.size(), new_lits.data(), m.mk_proof_sort());
+            mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
+        }
         else {
             mk_clause(num_lits, lits, nullptr);
         }

src/smt/theory_recfun.cpp

@@ -102,9 +102,8 @@ namespace smt {
     void theory_recfun::relevant_eh(app * n) {
         SASSERT(ctx.relevancy());
         // TRACEFN("relevant_eh: (defined) " <<  u().is_defined(n) << " " << mk_pp(n, m));        
-        if (u().is_defined(n) && u().has_defs()) {
+        if (u().is_defined(n) && u().has_defs()) 
             push_case_expand(n);
-        }
     }
 
     void theory_recfun::push_scope_eh() {
@@ -418,7 +417,7 @@ namespace smt {
     }
 
     void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
-        if (u().has_defs() || !m_disabled_guards.empty()) {
+        if (u().has_rec_defs() || !m_disabled_guards.empty()) {
             app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
             TRACEFN("add_theory_assumption " << dlimit);
             assumptions.push_back(dlimit);

src/solver/assertions/asserted_formulas.cpp

@@ -306,7 +306,7 @@ void asserted_formulas::reduce() {
     if (!invoke(m_flatten_clauses)) return;
 //    if (!invoke(m_propagate_values)) return;
 
-    IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";);
+    IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done :num-exprs " << get_total_size() << ")\n";);
     TRACE("after_reduce", display(tout););
     TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
     TRACE("macros", m_macro_manager.display(tout););
@@ -327,8 +327,8 @@ unsigned asserted_formulas::get_formulas_last_level() const {
 
 bool asserted_formulas::invoke(simplify_fmls& s) {
     if (!s.should_apply()) return true;
-    IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";);
     s();
+    IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << " :num-exprs " << get_total_size() << ")\n";);
     IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
     TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited););
     CASSERT("well_sorted",check_well_sorted());
@@ -514,9 +514,9 @@ void asserted_formulas::simplify_fmls::operator()() {
 
 
 void asserted_formulas::reduce_and_solve() {
-    IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
     flush_cache(); // collect garbage
     m_reduce_asserted_formulas();
+    IF_VERBOSE(10, verbose_stream() << "(smt.reduced " << get_total_size() << ")\n";);
 }
 
 

src/tactic/core/CMakeLists.txt

@@ -49,6 +49,7 @@ z3_add_component(core_tactics
     reduce_invertible_tactic.h
     simplify_tactic.h
     solve_eqs_tactic.h
+    solve_eqs2_tactic.h
     special_relations_tactic.h
     split_clause_tactic.h
     symmetry_reduce_tactic.h

src/tactic/core/solve_eqs2_tactic.h

@@ -29,10 +29,15 @@ public:
     }
 };
 
-inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p) {
-    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs2");
+inline tactic * mk_solve_eqs2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs2_tactic_factory), "solve-eqs");
 }
 
+#if 1
+inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+    return mk_solve_eqs2_tactic(m, p);
+}
+#endif
 
 /*
   ADD_TACTIC("solve-eqs2", "solve for variables.", "mk_solve_eqs2_tactic(m, p)")

src/tactic/core/solve_eqs_tactic.cpp

@@ -425,6 +425,7 @@ class solve_eqs_tactic : public tactic {
                 else
                     pr = m().mk_modus_ponens(g.pr(idx), pr);
             }
+            IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(var, m()) << " -> " << mk_bounded_pp(def, m()) << "\n");
             m_subst->insert(var, def, pr, g.dep(idx));
         }
         
@@ -479,52 +480,11 @@ class solve_eqs_tactic : public tactic {
 
         ptr_vector<expr> m_todo;       
         void mark_occurs(expr_mark& occ, goal const& g, expr* v) {
-            expr_fast_mark2 visited;
-            occ.mark(v, true);
-            visited.mark(v, true);
-            for (unsigned j = 0; j < g.size(); ++j) {              
-                m_todo.push_back(g.form(j));
-            }
-            while (!m_todo.empty()) {
-                expr* e = m_todo.back();
-                if (visited.is_marked(e)) {
-                    m_todo.pop_back();
-                    continue;
-                }
-                if (is_app(e)) {
-                    bool does_occur = false;
-                    bool all_visited = true;
-                    for (expr* arg : *to_app(e)) {
-                        if (!visited.is_marked(arg)) {
-                            m_todo.push_back(arg);
-                            all_visited = false;
-                        }
-                        else {
-                            does_occur |= occ.is_marked(arg);
-                        }
-                    }
-                    if (all_visited) {
-                        occ.mark(e, does_occur);
-                        visited.mark(e, true);
-                        m_todo.pop_back();
-                    }
-                }
-                else if (is_quantifier(e)) {
-                    expr* body = to_quantifier(e)->get_expr();
-                    if (visited.is_marked(body)) {
-                        visited.mark(e, true);
-                        occ.mark(e, occ.is_marked(body));
-                        m_todo.pop_back();
-                    }
-                    else {
-                        m_todo.push_back(body);
-                    }
-                }
-                else {
-                    visited.mark(e, true);
-                    m_todo.pop_back();
-                }
-            }
+            SASSERT(m_todo.empty());
+            for (unsigned j = 0; j < g.size(); ++j)             
+                m_todo.push_back(g.form(j));            
+            ::mark_occurs(m_todo, v, occ);
+            SASSERT(m_todo.empty());
         }
 
         expr_mark m_compatible_tried;
@@ -661,9 +621,11 @@ class solve_eqs_tactic : public tactic {
                     expr* arg = args.get(i), *lhs = nullptr, *rhs = nullptr;
                     if (m().is_eq(arg, lhs, rhs) && !m().is_bool(lhs)) {                
                         if (trivial_solve1(lhs, rhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
+                            IF_VERBOSE(11, verbose_stream() << "nested " << mk_bounded_pp(var.get(), m()) << " -> " << mk_bounded_pp(def, m()) << "\n");
                             insert_solution(g, idx, arg, var, def, pr);
                         }
                         else if (trivial_solve1(rhs, lhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
+                            IF_VERBOSE(11, verbose_stream() << "nested " << mk_bounded_pp(var.get(), m()) << " -> " << mk_bounded_pp(def, m()) << "\n");
                             insert_solution(g, idx, arg, var, def, pr);
                         }
                         else {
@@ -1022,6 +984,10 @@ class solve_eqs_tactic : public tactic {
         unsigned get_num_eliminated_vars() const {
             return m_num_eliminated_vars;
         }
+
+        void collect_statistics(statistics& st) {
+            st.update("solve eqs elim vars", get_num_eliminated_vars());
+        }
         
         //
         // TBD: rewrite the tactic to first apply a topological sorting that
@@ -1031,6 +997,8 @@ class solve_eqs_tactic : public tactic {
         //
         void operator()(goal_ref const & g, goal_ref_buffer & result) {
             model_converter_ref mc;
+            std::function<void(statistics&)> coll = [&](statistics& st) { collect_statistics(st); };
+            statistics_report sreport(coll);
             tactic_report report("solve_eqs", *g);
             TRACE("goal", g->display(tout););
             m_produce_models = g->models_enabled();
@@ -1074,6 +1042,8 @@ class solve_eqs_tactic : public tactic {
             g->inc_depth();
             g->add(mc.get());
             result.push_back(g.get());
+
+            
         }
     };
     
@@ -1107,7 +1077,6 @@ public:
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
         (*m_imp)(in, result);
-        report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars());
     }
     
     void cleanup() override {
@@ -1126,7 +1095,7 @@ public:
     }
 
     void collect_statistics(statistics & st) const override {
-        st.update("eliminated vars", m_imp->get_num_eliminated_vars());
+        m_imp->collect_statistics(st);        
     }
 
     void reset_statistics() override {
@@ -1135,6 +1104,7 @@ public:
     
 };
 
-tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p) {
+
+tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p) {
     return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true));
 }

src/tactic/core/solve_eqs_tactic.h

@@ -22,10 +22,17 @@ Revision History:
 class ast_manager;
 class tactic;
 
-tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+tactic * mk_solve_eqs1_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#if 0
+inline tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+    return mk_solve_eqs1_tactic(m, p);
+}
+#endif
 
 /*
-  ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs_tactic(m, p)")
+  ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs1_tactic(m, p)")
 */
 
 

src/tactic/dependent_expr_state_tactic.h

@@ -22,14 +22,21 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
     ast_manager&    m;
     params_ref      m_params;
     std::string     m_name;
-    ref<dependent_expr_simplifier_factory>  m_factory;
-    scoped_ptr<dependent_expr_simplifier>   m_simp;
+    trail_stack     m_trail;
     goal_ref        m_goal;
     dependent_expr  m_dep;
+    statistics      m_st;
+    ref<dependent_expr_simplifier_factory>  m_factory;
+    scoped_ptr<dependent_expr_simplifier>   m_simp;
+    scoped_ptr<model_reconstruction_trail>  m_model_trail;
 
     void init() {
-        if (!m_simp)
+        if (!m_simp) {
             m_simp = m_factory->mk(m, m_params, *this);
+            m_st.reset();
+        }
+        if (!m_model_trail)
+            m_model_trail = alloc(model_reconstruction_trail, m, m_trail);
     }
 
 public:
@@ -39,7 +46,7 @@ public:
         m_params(p),
         m_name(name),
         m_factory(f),
-        m_simp(f->mk(m, p, *this)),
+        m_simp(nullptr),
         m_dep(m, m.mk_true(), nullptr)
     {}
 
@@ -60,6 +67,10 @@ public:
     bool inconsistent() override {
         return m_goal->inconsistent();
     }
+
+    model_reconstruction_trail& model_trail() override {
+        return *m_model_trail;
+    }
         
     char const* name() const override { return m_name.c_str(); }
 
@@ -75,29 +86,39 @@ public:
 
     void operator()(goal_ref const & in, 
                     goal_ref_buffer & result) override {
-        if (in->proofs_enabled())
-            throw tactic_exception("tactic does not support low level proofs");
+
         init();
+        statistics_report sreport(*this);
         tactic_report report(name(), *in);
         m_goal = in.get();
-        m_simp->reduce();
+        if (!in->proofs_enabled())
+            m_simp->reduce();
+        m_goal->elim_true();
         m_goal->inc_depth();
         if (in->models_enabled())
-            in->set(m_simp->get_model_converter().get());
-        result.push_back(in.get());        
+            in->add(m_model_trail->get_model_converter().get());
+        result.push_back(in.get());   
+        cleanup();
     }
 
     void cleanup() override {
+        if (m_simp) 
+            m_simp->collect_statistics(m_st);
+        m_simp = nullptr;
+        m_model_trail = nullptr;
     }
 
     void collect_statistics(statistics & st) const override {
-        if (m_simp)
+        if (m_simp) 
             m_simp->collect_statistics(st);
+        else
+            st.copy(m_st);
     }
     
     void reset_statistics() override {
         if (m_simp)
             m_simp->reset_statistics();
+        m_st.reset();
     }
 };
 

src/tactic/sls/sls_tactic.cpp

@@ -18,6 +18,7 @@ Notes:
 --*/
 #include "ast/normal_forms/nnf.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/core/simplify_tactic.h"

src/tactic/smtlogics/qfaufbv_tactic.cpp

@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/bv/bit_blaster_tactic.h"

src/tactic/smtlogics/qfauflia_tactic.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/smtlogics/smt_tactic.h"
 

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -20,6 +20,7 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/bv/bit_blaster_tactic.h"
 #include "tactic/bv/bv1_blaster_tactic.h"
@@ -39,6 +40,9 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
     // conservative gaussian elimination.
     solve_eq_p.set_uint("solve_eqs_max_occs", 2);
 
+    params_ref flat_and_or_p = p;
+    flat_and_or_p.set_bool("flat_and_or", false);
+
     params_ref simp2_p = p;
     simp2_p.set_bool("som", true);
     simp2_p.set_bool("pull_cheap_ite", true);
@@ -47,15 +51,17 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
     simp2_p.set_uint("local_ctx_limit", 10000000);
     simp2_p.set_bool("flat", true); // required by som
     simp2_p.set_bool("hoist_mul", false); // required by som
+    simp2_p.set_bool("flat_and_or", false);
 
     params_ref hoist_p;
     hoist_p.set_bool("hoist_mul", true);
     hoist_p.set_bool("som", false);
+    hoist_p.set_bool("flat_and_or", false);
 
     return
         and_then(
-            mk_simplify_tactic(m),
-            mk_propagate_values_tactic(m),
+            using_params(mk_simplify_tactic(m), flat_and_or_p),
+            using_params(mk_propagate_values_tactic(m), flat_and_or_p),
             using_params(mk_solve_eqs_tactic(m), solve_eq_p),
             mk_elim_uncnstr_tactic(m),
             if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
@@ -87,6 +93,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
     params_ref local_ctx_p = p;
     local_ctx_p.set_bool("local_ctx", true);
     local_ctx_p.set_bool("flat", false);
+    local_ctx_p.set_bool("flat_and_or", false);
 
     params_ref solver_p;
     solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.

src/tactic/smtlogics/qfidl_tactic.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/arith/normalize_bounds_tactic.h"
 #include "tactic/arith/fix_dl_var_tactic.h"

src/tactic/smtlogics/qflia_tactic.cpp

@@ -22,6 +22,7 @@ Notes:
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/arith/normalize_bounds_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/arith/add_bounds_tactic.h"
 #include "tactic/arith/pb2bv_tactic.h"

src/tactic/smtlogics/qfuf_tactic.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/symmetry_reduce_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/smtlogics/smt_tactic.h"
 

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
@@ -136,22 +137,23 @@ private:
 };
 
 static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
-    params_ref simp2_p = p;
+    params_ref simp2_p = p, flat_and_or_p = p;
+    flat_and_or_p.set_bool("flat_and_or", false);
     simp2_p.set_bool("pull_cheap_ite", true);
     simp2_p.set_bool("push_ite_bv", false);
     simp2_p.set_bool("local_ctx", true);
     simp2_p.set_uint("local_ctx_limit", 10000000);
-
     simp2_p.set_bool("ite_extra_rules", true);
     simp2_p.set_bool("mul2concat", true);
+    simp2_p.set_bool("flat_and_or", false);
 
     params_ref ctx_simp_p;
     ctx_simp_p.set_uint("max_depth", 32);
     ctx_simp_p.set_uint("max_steps", 5000000);
 
     return and_then(
-        mk_simplify_tactic(m),
-        mk_propagate_values_tactic(m),
+        using_params(mk_simplify_tactic(m), flat_and_or_p),
+        using_params(mk_propagate_values_tactic(m), flat_and_or_p),
         if_no_proofs(if_no_unsat_cores(mk_bv_bound_chk_tactic(m))),
         //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p),
         mk_solve_eqs_tactic(m),
@@ -163,8 +165,10 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
 }
 
 static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
-    return and_then(mk_simplify_tactic(m),
-                    mk_propagate_values_tactic(m),
+    params_ref simp2_p = p, flat_and_or_p = p;
+    flat_and_or_p.set_bool("flat_and_or", false);
+    return and_then(using_params(mk_simplify_tactic(m), flat_and_or_p),
+                    using_params(mk_propagate_values_tactic(m), flat_and_or_p),
                     mk_solve_eqs_tactic(m),
                     mk_elim_uncnstr_tactic(m),
                     if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),

src/tactic/smtlogics/quant_tactics.cpp

@@ -20,6 +20,7 @@ Revision History:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "qe/lite/qe_lite.h"
 #include "qe/qsat.h"

src/tactic/tactic.cpp

@@ -75,6 +75,18 @@ void report_tactic_progress(char const * id, unsigned val) {
     }
 }
 
+statistics_report::~statistics_report() {
+    statistics st;
+    if (m_tactic)
+        m_tactic->collect_statistics(st);
+    else if (m_collector)
+        m_collector(st);
+    if (st.size() == 0)
+        return;
+    IF_VERBOSE(TACTIC_VERBOSITY_LVL, st.display_smt2(verbose_stream()));
+}
+
+
 void skip_tactic::operator()(goal_ref const & in, goal_ref_buffer& result) {
     result.push_back(in.get());
 }

src/tactic/tactic.h

@@ -115,6 +115,15 @@ public:
 
 void report_tactic_progress(char const * id, unsigned val);
 
+class statistics_report {
+    tactic* m_tactic = nullptr;
+    std::function<void(statistics& st)> m_collector;
+public:
+    statistics_report(tactic& t):m_tactic(&t) {}
+    statistics_report(std::function<void(statistics&)>& coll): m_collector(coll) {}
+    ~statistics_report();
+};
+
 class skip_tactic : public tactic {
 public:
     void operator()(goal_ref const & in, goal_ref_buffer& result) override;

src/tactic/ufbv/ufbv_tactic.cpp

@@ -20,6 +20,7 @@ Notes:
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
+#include "tactic/core/solve_eqs2_tactic.h"
 #include "tactic/core/distribute_forall_tactic.h"
 #include "tactic/core/der_tactic.h"
 #include "tactic/core/reduce_args_tactic.h"

src/test/hashtable.cpp

@@ -26,8 +26,8 @@ Revision History:
 
 struct int_hash_proc { unsigned operator()(int x) const { return x * 3; } };
 typedef int_hashtable<int_hash_proc, default_eq<int> > int_set;
-typedef std::unordered_set<int, std::hash_compare<int, std::less<int> > > safe_int_set;
 // typedef safe_int_set int_set;
+typedef std::unordered_set<int> safe_int_set;
 
 inline bool contains(int_set & h, int i) {
     // return h.find(i) != h.end();

src/util/mpn.cpp

@@ -34,8 +34,8 @@ int mpn_manager::compare(mpn_digit const * a, unsigned lnga,
 
     trace(a, lnga);
 
-    unsigned j = max(lnga, lngb) - 1;
-    for (; j != -1u && res == 0; j--) {
+    unsigned j = max(lnga, lngb);
+    for (; j-- > 0 && res == 0;) {
         mpn_digit const & u_j = (j < lnga) ? a[j] : zero;
         mpn_digit const & v_j = (j < lngb) ? b[j] : zero;
         if (u_j > v_j) 
@@ -310,7 +310,7 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
     mpn_double_digit q_hat, temp, r_hat;
     mpn_digit borrow;
 
-    for (unsigned j = m-1; j != -1u; j--) {
+    for (unsigned j = m; j-- > 0; ) {
         temp = (((mpn_double_digit)numer[j+n]) << DIGIT_BITS) | ((mpn_double_digit)numer[j+n-1]);
         q_hat = temp / (mpn_double_digit) denom[n-1];
         r_hat = temp % (mpn_double_digit) denom[n-1];
@@ -388,7 +388,7 @@ char * mpn_manager::to_string(mpn_digit const * a, unsigned lng, char * buf, uns
 
 void mpn_manager::display_raw(std::ostream & out, mpn_digit const * a, unsigned lng) const {
     out << "[";
-    for (unsigned i = lng-1; i != -1u; i-- ) { out << a[i]; if (i != 0) out << "|"; } 
+    for (unsigned i = lng; i-- > 0; ) { out << a[i]; if (i != 0) out << "|"; }
     out << "]";
 }
 

src/util/util.h

@@ -25,6 +25,7 @@ Revision History:
 #include<limits>
 #include<stdint.h>
 #include <string>
+#include <functional>
 
 #ifndef SIZE_MAX
 #define SIZE_MAX std::numeric_limits<std::size_t>::max()
@@ -180,9 +181,8 @@ void display(std::ostream & out, const IT & begin, const IT & end, const char *
 template<typename T>
 struct delete_proc {
     void operator()(T * ptr) { 
-    if (ptr) {
-        dealloc(ptr);
-    }
+    if (ptr) 
+        dealloc(ptr);    
     }
 };
 
@@ -361,6 +361,22 @@ void fatal_error(int error_code);
 void set_fatal_error_handler(void (*pfn)(int error_code));
 
 
+template<typename S, typename T>
+bool any_of(S& set, T const& p) {
+    for (auto const& s : set)
+        if (p(s))
+            return true;
+    return false;
+}
+
+template<typename S, typename T>
+bool all_of(S& set, T const& p) {
+    for (auto const& s : set)
+        if (!p(s))
+            return false;
+    return true;
+}
+
 /**
    \brief Iterator for the [0..sz[0]) X [0..sz[1]) X ... X [0..sz[n-1]).
    it contains the current value.

src/util/visit_helper.h

@@ -45,5 +45,5 @@ public:
         m_visited[v] = std::min(m_visited_end, std::max(m_visited_begin, m_visited[v]) + 1);
     }
     bool is_visited(unsigned v) const { return m_visited[v] > m_visited_begin; }
-    unsigned num_visited(unsigned v) const { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; }
+    unsigned num_visited(unsigned v) { return std::max(m_visited_begin, m_visited[v]) - m_visited_begin; }
 };