wip - testing solve-eqs2, added as tactic

src/ast/expr_substitution.h

@@ -59,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_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) : m_include_bound(include_bound), m_es(e.m()) {if (e)  m_es.push_back(e); }
+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, true); }
+subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); }
-subterms::iterator subterms::end() { return iterator(*this, false); }
+subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); }
-subterms::iterator::iterator(subterms& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) {
+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 (!start) m_es.reset();
+    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();
+    expr* e = m_esp->back();
-    m_visited.mark(e, true);
+    // 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())) 
+    while (!m_esp->empty() && m_visitedp->is_marked(m_esp->back())) 
-        m_es.pop_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; ) {
+    for (unsigned i = m_esp->size(); i-- > 0; ) {
-        if (m_es.get(i) != other.m_es.get(i))
+        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);
+    ptr_vector<expr>* m_esp = nullptr;
-    subterms(expr_ref_vector const& es, bool include_bound);
+    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;
+        bool              m_include_bound = false;
-        expr_ref_vector m_es;
+        ptr_vector<expr>  m_es;
-        expr_mark       m_visited;        
+        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, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); }
-    static subterms all(expr_ref const& e) { return subterms(e, true); }
+    static subterms ground(expr_ref const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
-    static subterms ground(expr_ref const& e) { return subterms(e, false); }
+    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 all(expr_ref_vector const& e) { return subterms(e, true); }
+    static subterms ground(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
-    static subterms ground(expr_ref_vector const& e) { return subterms(e, false); }
     iterator begin();
     iterator end();
 };

src/ast/rewriter/bool_rewriter.cpp

@@ -244,10 +244,29 @@ 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 (s) {
             ast_lt lt;
             std::sort(buffer.begin(), buffer.end(), lt);       
@@ -556,9 +575,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 (expr * arg_arg : *to_app(arg)) {                                           \
-                for (unsigned j = 0; j < sz; j++) {                                             \
-                    expr * arg_arg = to_app(arg)->get_arg(j);                                   \
                     push_new_arg(arg_arg, new_args, neg_lits, pos_lits);                        \
                 }                                                                               \
             }                                                                                   \

src/ast/simplifiers/extract_eqs.cpp

@@ -37,6 +37,8 @@ namespace euf {
             auto [f, d] = e();
             expr* x, * y;
             if (m.is_eq(f, x, y)) {
+                if (x == y)
+                    return;
                 if (is_uninterp_const(x))
                     eqs.push_back(dependent_eq(e.fml(), to_app(x), expr_ref(y, m), d));
                 if (is_uninterp_const(y))

src/ast/simplifiers/solve_context_eqs.cpp

@@ -30,6 +30,7 @@ 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"
@@ -134,14 +135,6 @@ namespace euf {
         return false;
     }
 
-    void solve_context_eqs::init_contains(expr* v) {
-        m_contains_v.reset();
-        for (unsigned i = 0; i < m_fmls.size(); ++i)
-            m_todo.push_back(m_fmls[i].fml());
-        mark_occurs(m_todo, v, m_contains_v);
-        SASSERT(m_todo.empty());
-    }
-
     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)
@@ -149,7 +142,23 @@ namespace euf {
 
         unsigned j = 0;
         for (auto const& eq : eqs) {
-            init_contains(eq.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());
+            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());
+
+            // subject to occurrences, check if equality is safe
             if (is_safe_eq(eq.orig))
                 eqs[j++] = eq;
         }

src/ast/simplifiers/solve_context_eqs.h

@@ -44,9 +44,7 @@ namespace euf {
         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);
         
-        void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs);
+        void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs);        
-        void init_contains(expr* v);
-        
 
     public:
         

src/ast/simplifiers/solve_eqs.cpp

@@ -20,6 +20,8 @@ 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"
@@ -75,13 +77,15 @@ namespace euf {
 
         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;
         };
 
         unsigned init_level = UINT_MAX;
         unsigned_vector todo;
+        
         for (unsigned id = 0; id < m_id2var.size(); ++id) {
             if (is_explored(id))
                 continue;
@@ -96,14 +100,16 @@ 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& [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);                   
+                    m_subst_ids.push_back(j);                   
-                    for (expr* e : subterms::all(expr_ref(t, m))) 
+                    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;
@@ -113,19 +119,20 @@ namespace euf {
     }
 
     void solve_eqs::normalize() {
-        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
+        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]; });
 
         for (unsigned id : m_subst_ids) {
             if (!m.inc())
-                break;
+                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);
+            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
@@ -139,12 +146,14 @@ 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(vector<dependent_expr>& old_fmls) {
         if (!m.inc())
             return;
-        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, true);
+        scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
         rp->set_substitution(m_subst.get());
 
         for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) {
@@ -152,6 +161,7 @@ namespace euf {
             auto [new_f, new_dep] = rp->replace_with_dep(f);
             if (new_f == f)
                 continue;
+            m_rewriter(new_f);
             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));
@@ -164,29 +174,35 @@ namespace euf {
             ex->pre_process(m_fmls);
 
         unsigned count = 0;
+        vector<dependent_expr> old_fmls;
+        dep_eq_vector eqs;
         do {
-            vector<dependent_expr> old_fmls;
+            old_fmls.reset();
             m_subst_ids.reset();
-            if (!m.inc())
+            eqs.reset();
-                return;
-            dep_eq_vector eqs;
             get_eqs(eqs);
             extract_dep_graph(eqs);
             extract_subst();
+            normalize();
             apply_subst(old_fmls);
             ++count;
         } 
-        while (!m_subst_ids.empty() && count < 20);
+        while (!m_subst_ids.empty() && count < 20 && m.inc());
+
+        if (!m.inc())
+            return;
+
         save_subst({});
 
-        if (m_config.m_context_solve) {
+        if (m_config.m_context_solve) {            
-            vector<dependent_expr> old_fmls;
+            old_fmls.reset();
-            dep_eq_vector eqs;
             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);
         }
@@ -203,7 +219,7 @@ namespace euf {
         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);
     }
 

src/ast/simplifiers/solve_eqs.h

@@ -50,6 +50,8 @@ namespace euf {
         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()]; }

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_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));
         }
         
@@ -620,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 {
@@ -981,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
@@ -1033,6 +1040,9 @@ class solve_eqs_tactic : public tactic {
             g->inc_depth();
             g->add(mc.get());
             result.push_back(g.get());
+
+            
+            IF_VERBOSE(10, statistics st; collect_statistics(st); st.display_smt2(verbose_stream()));
         }
     };
     
@@ -1066,7 +1076,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 {
@@ -1085,7 +1094,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 {

src/tactic/dependent_expr_state_tactic.h

@@ -93,6 +93,10 @@ public:
         if (in->models_enabled())
             in->set(m_model_trail->get_model_converter().get());
         result.push_back(in.get());        
+
+        statistics st;
+        collect_statistics(st);
+        IF_VERBOSE(10, st.display_smt2(verbose_stream()));
     }
 
     void cleanup() override {