From 6c12aaad747d11b35113c3166029b6a33baaa916 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Nov 2022 22:42:59 -0700
Subject: [PATCH] wip - testing solve-eqs2, added as tactic
---
src/ast/expr_substitution.h | 4 ++
src/ast/for_each_expr.cpp | 41 +++++++++++--------
src/ast/for_each_expr.h | 26 ++++++------
src/ast/rewriter/bool_rewriter.cpp | 23 +++++++++--
src/ast/simplifiers/extract_eqs.cpp | 2 +
src/ast/simplifiers/solve_context_eqs.cpp | 27 ++++++++-----
src/ast/simplifiers/solve_context_eqs.h | 4 +-
src/ast/simplifiers/solve_eqs.cpp | 48 +++++++++++++++--------
src/ast/simplifiers/solve_eqs.h | 2 +
src/tactic/core/CMakeLists.txt | 1 +
src/tactic/core/solve_eqs_tactic.cpp | 13 +++++-
src/tactic/dependent_expr_state_tactic.h | 4 ++
12 files changed, 135 insertions(+), 60 deletions(-)
diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h
index 0e285ff7d..8f756e061 100644
--- a/src/ast/expr_substitution.h
+++ b/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;
diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp
index 54e176fc5..0790b418d 100644
--- a/src/ast/for_each_expr.cpp
+++ b/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;
diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h
index b724bed86..99a0f6b9d 100644
--- a/src/ast/for_each_expr.h
+++ b/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();
};
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 1964e6528..442bef855 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/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 (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); \
} \
} \
diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp
index e77ce9e06..543030e91 100644
--- a/src/ast/simplifiers/extract_eqs.cpp
+++ b/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))
diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp
index 766c18535..c11505726 100644
--- a/src/ast/simplifiers/solve_context_eqs.cpp
+++ b/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;
}
diff --git a/src/ast/simplifiers/solve_context_eqs.h b/src/ast/simplifiers/solve_context_eqs.h
index b3db74127..fb330b57b 100644
--- a/src/ast/simplifiers/solve_context_eqs.h
+++ b/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 init_contains(expr* v);
-
+ void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs);
public:
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 31e063119..b611e0144 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/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);
- 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;
@@ -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())
- return;
- dep_eq_vector eqs;
+ eqs.reset();
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) {
- vector<dependent_expr> old_fmls;
- dep_eq_vector eqs;
+ 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);
}
@@ -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);
}
diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h
index 35044b373..8f5988a38 100644
--- a/src/ast/simplifiers/solve_eqs.h
+++ b/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()]; }
diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt
index e57510d4f..38d2699f0 100644
--- a/src/tactic/core/CMakeLists.txt
+++ b/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
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index cfc4d8eeb..fdba65b3f 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/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 {
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index 41b32baac..01e135e8a 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/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 {