mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

for Arie

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-04 14:23:52 +02:00
parent bcedb66911
commit ef284cca5d
6 changed files with 122 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

57
src/ast/simplifiers/euf_completion.cpp
View file

@ -149,8 +149,10 @@ namespace euf {
for (unsigned i = 0; i < q->get_num_decls(); ++i)
_binding.push_back(binding[i]->get_expr());
expr_ref r = subst(q->get_expr(), _binding);
IF_VERBOSE(12, verbose_stream() << "add " << r << "\n");
add_constraint(r, get_dependency(q));
m_should_propagate = true;
++m_stats.m_num_instances;
}
void completion::read_egraph() {
@ -164,8 +166,7 @@ namespace euf {
unsigned sz = qtail();
for (unsigned i = qhead(); i < sz; ++i) {
auto [f, p, d] = m_fmls[i]();
auto [f, p, d] = m_fmls[i]();
expr_dependency_ref dep(d, m);
expr_ref g = canonize_fml(f, dep);
if (g != f) {
@ -388,6 +389,53 @@ namespace euf {
void completion::collect_statistics(statistics& st) const {
st.update("euf-completion-rewrites", m_stats.m_num_rewrites);
st.update("euf-completion-instances", m_stats.m_num_instances);
}
bool completion::is_gt(expr* lhs, expr* rhs) const {
if (lhs == rhs)
return false;
// values are always less in ordering than non-values.
bool v1 = m.is_value(lhs);
bool v2 = m.is_value(rhs);
if (!v1 && v2)
return true;
if (v1 && !v2)
return false;
if (get_depth(lhs) > get_depth(rhs))
return true;
if (get_depth(lhs) < get_depth(rhs))
return false;
// slow path
auto n1 = get_num_exprs(lhs);
auto n2 = get_num_exprs(rhs);
if (n1 > n2)
return true;
if (n1 < n2)
return false;
if (is_app(lhs) && is_app(rhs)) {
app* l = to_app(lhs);
app* r = to_app(rhs);
if (l->get_decl()->get_id() != r->get_decl()->get_id())
return l->get_decl()->get_id() > r->get_decl()->get_id();
if (l->get_num_args() != r->get_num_args())
return l->get_num_args() > r->get_num_args();
for (unsigned i = 0; i < l->get_num_args(); ++i)
if (l->get_arg(i) != r->get_arg(i))
return is_gt(l->get_arg(i), r->get_arg(i));
UNREACHABLE();
}
if (is_quantifier(lhs) && is_quantifier(rhs)) {
expr* l = to_quantifier(lhs)->get_expr();
expr* r = to_quantifier(rhs)->get_expr();
return is_gt(l, r);
}
if (is_quantifier(lhs))
return true;
return false;
}
void completion::map_canonical() {
@ -403,8 +451,9 @@ namespace euf {
roots.push_back(n);
enode* rep = nullptr;
for (enode* k : enode_class(n))
if (!rep || m.is_value(k->get_expr()) || get_depth(rep->get_expr()) > get_depth(k->get_expr()))
rep = k;
if (!rep || m.is_value(k->get_expr()) || is_gt(rep->get_expr(), k->get_expr()))
rep = k;
// IF_VERBOSE(0, verbose_stream() << m_egraph.bpp(n) << " ->\n" << m_egraph.bpp(rep) << "\n";);
m_reps.setx(n->get_id(), rep, nullptr);
TRACE(euf_completion, tout << "rep " << m_egraph.bpp(n) << " -> " << m_egraph.bpp(rep) << "\n";

3
src/ast/simplifiers/euf_completion.h
View file

@ -28,6 +28,7 @@ namespace euf {
struct stats {
unsigned m_num_rewrites = 0;
unsigned m_num_instances = 0;
void reset() { memset(this, 0, sizeof(*this)); }
};
@ -63,6 +64,8 @@ namespace euf {
expr_dependency* explain_eq(enode* a, enode* b);
expr_dependency* explain_conflict();
expr_dependency* get_dependency(quantifier* q) { return m_q2dep.contains(q) ? m_q2dep[q] : nullptr; }
bool is_gt(expr* a, expr* b) const;
public:
completion(ast_manager& m, dependent_expr_state& fmls);
char const* name() const override { return "euf-reduce"; }

58
src/ast/simplifiers/extract_eqs.cpp
View file

@ -33,6 +33,40 @@ namespace euf {
bool m_ite_solver = true;
bool m_allow_bool = true;
bool is_eq_of(expr* x, expr* y, expr*& z, expr*& s, expr*& t) {
expr* x1 = nullptr, *x2 = nullptr, *y1 = nullptr, *y2 = nullptr;
if (!m.is_eq(x, x1, x2))
return false;
if (!m.is_eq(y, y1, y2))
return false;
if (x1 == y1) {
z = x1;
s = x2;
t = y2;
return true;
}
if (x1 == y2) {
z = x1;
s = x2;
t = y1;
return true;
}
if (x2 == y1) {
z = x2;
s = x1;
t = y2;
return true;
}
return false;
}
bool is_complementary(expr* x, expr* y) {
expr* z = nullptr;
if (m.is_not(x, z) && z == y)
return true;
if (m.is_not(y, z) && z == x)
return true;
return false;
}
public:
basic_extract_eq(ast_manager& m) : m(m) {}
@ -68,6 +102,30 @@ namespace euf {
eqs.push_back(dependent_eq(e.fml(), to_app(x1), expr_ref(m.mk_ite(c, y1, y2), m), d));
}
}
// (or (and a (= x t)) (and (not a) (= x s)))
// -> x = if a s t
if (m.is_or(f, x1, y1) && m.is_and(x1, x1, x2) && m.is_and(y1, y1, y2)) {
expr* z = nullptr, *t = nullptr, *s = nullptr;
if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x2, s, t), m), d));
if (is_eq_of(x1, y2, z, s, t) && is_complementary(x2, y1))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x2, s, t), m), d));
if (is_eq_of(x2, y2, z, s, t) && is_complementary(x1, y1))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d));
if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d));
}
if (m.is_and(f, x1, y1) && m.is_or(x, x1, x2) && m.is_or(y1, y1, y2)) {
expr* z = nullptr, *t = nullptr, *s = nullptr;
if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d));
if (is_eq_of(x1, y2, z, s, t) && is_complementary(x2, y1))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y1, s, t), m), d));
if (is_eq_of(x2, y2, z, s, t) && is_complementary(x1, y1))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y1, s, t), m), d));
if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d));
}
if (!m_allow_bool)
return;
if (is_uninterp_const(f))

6
src/math/grobner/pdd_solver.cpp
View file

@ -72,7 +72,7 @@ namespace dd {
void solver::adjust_cfg() {
auto & cfg = m_config;
IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
IF_VERBOSE(5, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
cfg.m_eqs_threshold = static_cast<unsigned>(cfg.m_eqs_growth * ceil(log(1 + m_to_simplify.size()))* m_to_simplify.size());
cfg.m_expr_size_limit = 0;
cfg.m_expr_degree_limit = 0;
@ -83,7 +83,7 @@ namespace dd {
cfg.m_expr_size_limit *= cfg.m_expr_size_growth;
cfg.m_expr_degree_limit *= cfg.m_expr_degree_growth;;
IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold " << m_config.m_eqs_threshold << "\n";
IF_VERBOSE(5, verbose_stream() << "set m_config.m_eqs_threshold " << m_config.m_eqs_threshold << "\n";
verbose_stream() << "set m_config.m_expr_size_limit to " << m_config.m_expr_size_limit << "\n";
verbose_stream() << "set m_config.m_expr_degree_limit to " << m_config.m_expr_degree_limit << "\n";
);
@ -98,7 +98,7 @@ namespace dd {
while (!done() && step()) {
TRACE(dd_solver, display(tout););
DEBUG_CODE(invariant(););
IF_VERBOSE(3, display_statistics(verbose_stream()));
IF_VERBOSE(6, display_statistics(verbose_stream()));
}
DEBUG_CODE(invariant(););
}

4
src/math/lp/nla_grobner.cpp
View file

@ -86,8 +86,8 @@ namespace nla {
if (m_quota > 0)
--m_quota;
IF_VERBOSE(3, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
IF_VERBOSE(5, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
IF_VERBOSE(5, diagnose_pdd_miss(verbose_stream()));
}
dd::solver::equation_vector const& grobner::core_equations(bool all_eqs) {

6
src/smt/theory_lra.cpp
View file

@ -3789,19 +3789,19 @@ public:
unsigned m_num_dumped_lemmas = 0;
void dump_assign_lemma(literal lit) {
std::cout << "; assign lemma " << (m_num_dumped_lemmas++) << "\n";
std::cout << "(echo \"assign lemma " << (m_num_dumped_lemmas++) << "\")\n";
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
std::cout << "(reset)\n";
}
void dump_conflict() {
std::cout << "; conflict " << (m_num_dumped_lemmas++) << "\n";
std::cout << "(echo \"conflict " << (m_num_dumped_lemmas++) << "\")\n";
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data());
std::cout << "(reset)\n";
}
void dump_eq(enode* x, enode* y) {
std::cout << "; equality propagation " << (m_num_dumped_lemmas++) << "\n";
std::cout << "(echo \"equality propagation " << (m_num_dumped_lemmas++) << "\")\n";
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal, symbol::null, x, y);
std::cout << "(reset)\n";
}