From 7368f9f7d3185198fd6b66db483f75f83ab697d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Jan 2023 14:07:07 -0800 Subject: [PATCH] increase build version, better propagation in euf-egraph, handle assumptions in sat.smt - increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86 - move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing) - fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen. --- CMakeLists.txt | 2 +- scripts/mk_project.py | 2 +- scripts/nightly.yaml | 2 +- scripts/release.yml | 2 +- src/ast/euf/euf_egraph.cpp | 49 +++++----- src/ast/euf/euf_egraph.h | 19 +--- src/ast/simplifiers/dependent_expr_state.h | 2 +- .../model_reconstruction_trail.cpp | 27 +++++- .../simplifiers/model_reconstruction_trail.h | 12 ++- src/sat/sat_solver/sat_smt_solver.cpp | 20 ++-- src/sat/smt/euf_solver.cpp | 96 ++++++++++--------- src/sat/smt/euf_solver.h | 2 +- src/smt/smt_context.cpp | 1 + src/tactic/arith/arith_bounds_tactic.h | 2 + src/tactic/core/cofactor_elim_term_ite.cpp | 34 +++---- src/tactic/core/cofactor_term_ite_tactic.h | 13 ++- src/tactic/core/euf_completion_tactic.h | 16 ++++ src/tactic/core/reduce_args_tactic.h | 27 +----- src/tactic/core/tseitin_cnf_tactic.cpp | 10 +- src/tactic/fpa/fpa2bv_tactic.h | 11 ++- src/tactic/fpa/qffp_tactic.h | 11 ++- src/tactic/fpa/qffplra_tactic.h | 3 +- 22 files changed, 201 insertions(+), 162 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d79a01da71f..78929fed61d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.12.0.0 LANGUAGES CXX) +project(Z3 VERSION 4.12.1.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/scripts/mk_project.py b/scripts/mk_project.py index a16913317f3..3e7386601d5 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 12, 0, 0) # express a default build version or pick up ci build version + set_version(4, 12, 1, 0) # express a default build version or pick up ci build version # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index c93738e58c2..4e602797610 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,7 +1,7 @@ variables: Major: '4' Minor: '12' - Patch: '0' + Patch: '1' AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName) diff --git a/scripts/release.yml b/scripts/release.yml index 4421f515386..42a5bbcc6c0 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.12.0' + ReleaseVersion: '4.12.1' stages: diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index ad88f839fc8..115a3f53f6f 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -91,9 +91,7 @@ namespace euf { m_scopes.push_back(m_updates.size()); m_region.push_scope(); m_updates.push_back(update_record(m_new_th_eqs_qhead, update_record::new_th_eq_qhead())); - m_updates.push_back(update_record(m_new_lits_qhead, update_record::new_lits_qhead())); } - SASSERT(m_new_lits_qhead <= m_new_lits.size()); SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size()); } @@ -156,12 +154,29 @@ namespace euf { } void egraph::add_literal(enode* n, enode* ante) { + /* if (n->bool_var() == sat::null_bool_var) return; - TRACE("euf_verbose", tout << "lit: " << n->get_expr_id() << "\n";); - m_new_lits.push_back(enode_pair(n, ante)); - m_updates.push_back(update_record(update_record::new_lit())); + */ if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits; + if (!ante) + m_on_propagate_literal(n, ante); + else if (m.is_true(ante->get_expr()) || m.is_false(ante->get_expr())) { + for (enode* k : enode_class(n)) { + if (k != ante) { + //verbose_stream() << "eq: " << k->value() << " " <value() << "\n"; + m_on_propagate_literal(k, ante); + } + } + } + else { + for (enode* k : enode_class(n)) { + if (k->value() != ante->value()) { + //verbose_stream() << "eq: " << k->value() << " " <value() << "\n"; + m_on_propagate_literal(k, ante); + } + } + } } void egraph::new_diseq(enode* n) { @@ -339,7 +354,6 @@ namespace euf { num_scopes -= m_num_scopes; m_num_scopes = 0; - SASSERT(m_new_lits_qhead <= m_new_lits.size()); unsigned old_lim = m_scopes.size() - num_scopes; unsigned num_updates = m_scopes[old_lim]; auto undo_node = [&]() { @@ -378,18 +392,12 @@ namespace euf { SASSERT(p.r1->get_th_var(p.m_th_id) != null_theory_var); p.r1->replace_th_var(p.m_old_th_var, p.m_th_id); break; - case update_record::tag_t::is_new_lit: - m_new_lits.pop_back(); - break; case update_record::tag_t::is_new_th_eq: m_new_th_eqs.pop_back(); break; case update_record::tag_t::is_new_th_eq_qhead: m_new_th_eqs_qhead = p.qhead; break; - case update_record::tag_t::is_new_lits_qhead: - m_new_lits_qhead = p.qhead; - break; case update_record::tag_t::is_inconsistent: m_inconsistent = p.m_inconsistent; break; @@ -424,7 +432,6 @@ namespace euf { m_region.pop_scope(num_scopes); m_to_merge.reset(); - SASSERT(m_new_lits_qhead <= m_new_lits.size()); SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size()); // DEBUG_CODE(invariant();); @@ -461,12 +468,6 @@ namespace euf { std::swap(n1, n2); } - if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr()))) - add_literal(n1, r2); - if (r2->value() != l_undef && n1->value() == l_undef) - add_literal(n1, r2); - else if (r1->value() != l_undef && n2->value() == l_undef) - add_literal(n2, r1); remove_parents(r1); push_eq(r1, n1, r2->num_parents()); merge_justification(n1, n2, j); @@ -476,6 +477,13 @@ namespace euf { r2->inc_class_size(r1->class_size()); merge_th_eq(r1, r2); reinsert_parents(r1, r2); + if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr()))) + add_literal(n1, r2); + else if (n2->value() != l_undef && n1->value() != n2->value()) + add_literal(n1, n2); + else if (n1->value() != l_undef && n2->value() != n1->value()) + add_literal(n2, n1); + for (auto& cb : m_on_merge) cb(r2, r1); } @@ -565,7 +573,6 @@ namespace euf { bool egraph::propagate() { - SASSERT(m_new_lits_qhead <= m_new_lits.size()); SASSERT(m_num_scopes == 0 || m_to_merge.empty()); force_push(); for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) { @@ -574,7 +581,6 @@ namespace euf { } m_to_merge.reset(); return - (m_new_lits_qhead < m_new_lits.size()) || (m_new_th_eqs_qhead < m_new_th_eqs.size()) || inconsistent(); } @@ -851,7 +857,6 @@ namespace euf { std::ostream& egraph::display(std::ostream& out) const { out << "updates " << m_updates.size() << "\n"; - out << "newlits " << m_new_lits.size() << " qhead: " << m_new_lits_qhead << "\n"; out << "neweqs " << m_new_th_eqs.size() << " qhead: " << m_new_th_eqs_qhead << "\n"; m_table.display(out); unsigned max_args = 0; diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 1686be38469..c1b9b784953 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -105,10 +105,8 @@ namespace euf { struct toggle_merge_tf {}; struct add_th_var {}; struct replace_th_var {}; - struct new_lit {}; struct new_th_eq {}; struct new_th_eq_qhead {}; - struct new_lits_qhead {}; struct inconsistent {}; struct value_assignment {}; struct lbl_hash {}; @@ -116,8 +114,8 @@ namespace euf { struct update_children {}; struct set_relevant {}; enum class tag_t { is_set_parent, is_add_node, is_toggle_cgc, is_toggle_merge_tf, is_update_children, - is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq, - is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, + is_add_th_var, is_replace_th_var, is_new_th_eq, + is_lbl_hash, is_new_th_eq_qhead, is_inconsistent, is_value_assignment, is_lbl_set, is_set_relevant }; tag_t tag; enode* r1; @@ -145,14 +143,10 @@ namespace euf { tag(tag_t::is_add_th_var), r1(n), n1(nullptr), r2_num_parents(id) {} update_record(enode* n, theory_id id, theory_var v, replace_th_var) : tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th_id(id), m_old_th_var(v) {} - update_record(new_lit) : - tag(tag_t::is_new_lit), r1(nullptr), n1(nullptr), r2_num_parents(0) {} update_record(new_th_eq) : tag(tag_t::is_new_th_eq), r1(nullptr), n1(nullptr), r2_num_parents(0) {} update_record(unsigned qh, new_th_eq_qhead): tag(tag_t::is_new_th_eq_qhead), r1(nullptr), n1(nullptr), qhead(qh) {} - update_record(unsigned qh, new_lits_qhead): - tag(tag_t::is_new_lits_qhead), r1(nullptr), n1(nullptr), qhead(qh) {} update_record(bool inc, inconsistent) : tag(tag_t::is_inconsistent), r1(nullptr), n1(nullptr), m_inconsistent(inc) {} update_record(enode* n, value_assignment) : @@ -187,9 +181,7 @@ namespace euf { enode *m_n1 = nullptr; enode *m_n2 = nullptr; justification m_justification; - unsigned m_new_lits_qhead = 0; unsigned m_new_th_eqs_qhead = 0; - svector m_new_lits; svector m_new_th_eqs; bool_vector m_th_propagates_diseqs; enode_vector m_todo; @@ -198,7 +190,8 @@ namespace euf { bool m_default_relevant = true; uint64_t m_congruence_timestamp = 0; - std::vector> m_on_merge; + std::vector> m_on_merge; + std::function m_on_propagate_literal; std::function m_on_make; std::function m_used_eq; std::function m_used_cc; @@ -290,11 +283,8 @@ namespace euf { is an equality consequence. */ void add_th_diseq(theory_id id, theory_var v1, theory_var v2, expr* eq); - bool has_literal() const { return m_new_lits_qhead < m_new_lits.size(); } bool has_th_eq() const { return m_new_th_eqs_qhead < m_new_th_eqs.size(); } - enode_pair get_literal() const { return m_new_lits[m_new_lits_qhead]; } th_eq get_th_eq() const { return m_new_th_eqs[m_new_th_eqs_qhead]; } - void next_literal() { force_push(); SASSERT(m_new_lits_qhead < m_new_lits.size()); m_new_lits_qhead++; } void next_th_eq() { force_push(); SASSERT(m_new_th_eqs_qhead < m_new_th_eqs.size()); m_new_th_eqs_qhead++; } void set_lbl_hash(enode* n); @@ -311,6 +301,7 @@ namespace euf { void set_default_relevant(bool b) { m_default_relevant = b; } void set_on_merge(std::function& on_merge) { m_on_merge.push_back(on_merge); } + void set_on_propagate(std::function& on_propagate) { m_on_propagate_literal = on_propagate; } void set_on_make(std::function& on_make) { m_on_make = on_make; } void set_used_eq(std::function& used_eq) { m_used_eq = used_eq; } void set_used_cc(std::function& used_cc) { m_used_cc = used_cc; } diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index ef9263686c2..c3b5043a5a7 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -51,7 +51,6 @@ class dependent_expr_state { void freeze_recfun(); void freeze_lambda(); void freeze_terms(expr* term, bool only_as_array, ast_mark& visited); - void freeze(expr* term); void freeze(func_decl* f); struct thaw : public trail { unsigned sz; @@ -89,6 +88,7 @@ class dependent_expr_state { /** * Freeze internal functions */ + void freeze(expr* term); bool frozen(func_decl* f) const { return m_frozen.is_marked(f); } bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); } void freeze_suffix(); diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 567546e67b1..e3cfc5c6fec 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -23,11 +23,13 @@ Module Name: // substitutions that use variables from the dependent expressions. // TODO: add filters to skip sections of the trail that do not touch the current free variables. -void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st) { +void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& st) { ast_mark free_vars; scoped_ptr rp = mk_default_expr_replacer(m, false); - for (unsigned i = qhead; i < st.qtail(); ++i) + for (unsigned i = qhead; i < st.qtail(); ++i) add_vars(st[i], free_vars); + for (expr* a : assumptions) + add_vars(a, free_vars); for (auto& t : m_trail) { if (!t->m_active) @@ -63,7 +65,7 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st mrp.insert(head, t->m_def, t->m_dep); dependent_expr de(m, t->m_def, nullptr, t->m_dep); add_vars(de, free_vars); - + for (unsigned i = qhead; i < st.qtail(); ++i) { auto [f, p, dep1] = st[i](); expr_ref g(m); @@ -73,6 +75,15 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st if (f != g) st.update(i, dependent_expr(m, g, nullptr, dep2)); } + for (unsigned i = 0; i < assumptions.size(); ++i) { + expr* a = assumptions.get(i); + expr_ref g(m); + expr_dependency_ref dep(m); + mrp(a, nullptr, g, dep); + if (a != g) + assumptions[i] = g; + // ignore dep. + } continue; } @@ -103,7 +114,15 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st CTRACE("simplifier", f != g, tout << "updated " << mk_pp(g, m) << "\n"); add_vars(d, free_vars); st.update(i, d); - } + } + + for (unsigned i = 0; i < assumptions.size(); ++i) { + expr* a = assumptions.get(i); + auto [g, dep2] = rp->replace_with_dep(a); + if (a != g) + assumptions[i] = g; + // ignore dep. + } } } diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index 7f8c7dc8f09..4bc09e646a4 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -74,13 +74,17 @@ class model_reconstruction_trail { scoped_ptr_vector m_trail; unsigned m_trail_index = 0; - void add_vars(dependent_expr const& d, ast_mark& free_vars) { - for (expr* t : subterms::all(expr_ref(d.fml(), d.get_manager()))) + void add_vars(expr* e, ast_mark& free_vars) { + for (expr* t : subterms::all(expr_ref(e, m))) free_vars.mark(t, true); } + + void add_vars(dependent_expr const& d, ast_mark& free_vars) { + add_vars(d.fml(), free_vars); + } bool intersects(ast_mark const& free_vars, dependent_expr const& d) { - expr_ref term(d.fml(), d.get_manager()); + expr_ref term(d.fml(), m); auto iter = subterms::all(term); return any_of(iter, [&](expr* t) { return free_vars.is_marked(t); }); } @@ -126,7 +130,7 @@ class model_reconstruction_trail { * register a new depedent expression, update the trail * by removing substitutions that are not equivalence preserving. */ - void replay(unsigned qhead, dependent_expr_state& fmls); + void replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& fmls); /** * retrieve the current model converter corresponding to chaining substitutions from the trail. diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index fd970a44ac5..8060afcd7ac 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -70,7 +70,7 @@ class sat_smt_solver : public solver { return out; } void append(generic_model_converter& mc) { model_trail().append(mc); } - void replay(unsigned qhead) { m_reconstruction_trail.replay(qhead, *this); } + void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); } void flatten_suffix() override { expr_mark seen; unsigned j = qhead(); @@ -237,8 +237,10 @@ class sat_smt_solver : public solver { expr_ref_vector assumptions(m); for (unsigned i = 0; i < sz; ++i) assumptions.push_back(ensure_literal(_assumptions[i])); + for (expr* a : assumptions) + m_preprocess_state.freeze(a); TRACE("sat", tout << assumptions << "\n";); - lbool r = internalize_formulas(); + lbool r = internalize_formulas(assumptions); if (r != l_true) return r; @@ -271,7 +273,8 @@ class sat_smt_solver : public solver { void push() override { try { - internalize_formulas(); + expr_ref_vector none(m); + internalize_formulas(none); } catch (...) { push_internal(); @@ -430,7 +433,7 @@ class sat_smt_solver : public solver { } expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override { - lbool r = internalize_formulas(); + lbool r = internalize_formulas(vs); if (r != l_true) { IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n"); return expr_ref_vector(m); @@ -561,7 +564,8 @@ class sat_smt_solver : public solver { void convert_internalized() { m_solver.pop_to_base_level(); - internalize_formulas(); + expr_ref_vector none(m); + internalize_formulas(none); if (!is_internalized() || m_internalized_converted) return; sat2goal s2g; @@ -641,9 +645,9 @@ class sat_smt_solver : public solver { add_assumption(a); } - lbool internalize_formulas() { + lbool internalize_formulas(expr_ref_vector& assumptions) { - if (is_internalized()) + if (is_internalized() && assumptions.empty()) return l_true; unsigned qhead = m_preprocess_state.qhead(); @@ -651,7 +655,7 @@ class sat_smt_solver : public solver { m_internalized_converted = false; - m_preprocess_state.replay(qhead); + m_preprocess_state.replay(qhead, assumptions); m_preprocess.reduce(); if (!m.inc()) return l_undef; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index c9b0430b584..8efb433ffaf 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -63,6 +63,11 @@ namespace euf { }; m_egraph.set_display_justification(disp); + std::function on_literal = [&](enode* n, enode* ante) { + propagate_literal(n, ante); + }; + m_egraph.set_on_propagate(on_literal); + if (m_relevancy.enabled()) { std::function on_merge = [&](enode* root, enode* other) { @@ -414,7 +419,6 @@ namespace euf { } bool propagated1 = false; if (m_egraph.propagate()) { - propagate_literals(); propagate_th_eqs(); propagated1 = true; } @@ -435,52 +439,52 @@ namespace euf { return propagated; } - void solver::propagate_literals() { - for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) { - auto [n, ante] = m_egraph.get_literal(); - expr* e = n->get_expr(); - expr* a = nullptr, *b = nullptr; - bool_var v = n->bool_var(); - SASSERT(m.is_bool(e)); - size_t cnstr; - literal lit; - if (!ante) { - VERIFY(m.is_eq(e, a, b)); - cnstr = eq_constraint().to_index(); - lit = literal(v, false); - } - else { - // - // There are the following three cases for propagation of literals - // - // 1. n == ante is true from equallity, ante = true/false - // 2. n == ante is true from equality, value(ante) != l_undef - // 3. value(n) != l_undef, ante = true/false, merge_tf is set on n - // - lbool val = ante->value(); - if (val == l_undef) { - SASSERT(m.is_value(ante->get_expr())); - val = m.is_true(ante->get_expr()) ? l_true : l_false; - } - auto& c = lit_constraint(ante); - cnstr = c.to_index(); - lit = literal(v, val == l_false); - } - unsigned lvl = s().scope_lvl(); - - CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";); - if (s().value(lit) == l_false && m_ackerman && a && b) - m_ackerman->cg_conflict_eh(a, b); - switch (s().value(lit)) { - case l_true: - if (n->merge_tf() && !m.is_value(n->get_root()->get_expr())) - m_egraph.merge(n, ante, to_ptr(lit)); - break; - case l_undef: - case l_false: - s().assign(lit, sat::justification::mk_ext_justification(lvl, cnstr)); - break; + + void solver::propagate_literal(enode* n, enode* ante) { + expr* e = n->get_expr(); + expr* a = nullptr, *b = nullptr; + bool_var v = n->bool_var(); + if (v == sat::null_bool_var) + return; + SASSERT(m.is_bool(e)); + size_t cnstr; + literal lit; + if (!ante) { + VERIFY(m.is_eq(e, a, b)); + cnstr = eq_constraint().to_index(); + lit = literal(v, false); + } + else { + // + // There are the following three cases for propagation of literals + // + // 1. n == ante is true from equallity, ante = true/false + // 2. n == ante is true from equality, value(ante) != l_undef + // 3. value(n) != l_undef, ante = true/false, merge_tf is set on n + // + lbool val = ante->value(); + if (val == l_undef) { + SASSERT(m.is_value(ante->get_expr())); + val = m.is_true(ante->get_expr()) ? l_true : l_false; } + auto& c = lit_constraint(ante); + cnstr = c.to_index(); + lit = literal(v, val == l_false); + } + unsigned lvl = s().scope_lvl(); + + CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";); + if (s().value(lit) == l_false && m_ackerman && a && b) + m_ackerman->cg_conflict_eh(a, b); + switch (s().value(lit)) { + case l_true: + if (n->merge_tf() && !m.is_value(n->get_root()->get_expr())) + m_egraph.merge(n, ante, to_ptr(lit)); + break; + case l_undef: + case l_false: + s().assign(lit, sat::justification::mk_ext_justification(lvl, cnstr)); + break; } } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 675ec150099..96079fbec92 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -206,7 +206,7 @@ namespace euf { void validate_model(model& mdl); // solving - void propagate_literals(); + void propagate_literal(enode* n, enode* ante); void propagate_th_eqs(); bool is_self_propagated(th_eq const& e); void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 01e0aba7c81..d84535a9c86 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -866,6 +866,7 @@ namespace smt { SASSERT(curr != m_false_enode); bool_var v = enode2bool_var(curr); literal l(v, sign); + CTRACE("propagate", (get_assignment(l) != l_true), tout << enode_pp(curr, *this) << " " << l << "\n"); if (get_assignment(l) != l_true) assign(l, mk_justification(eq_root_propagation_justification(curr))); curr = curr->m_next; diff --git a/src/tactic/arith/arith_bounds_tactic.h b/src/tactic/arith/arith_bounds_tactic.h index 4606f61441d..014a6dde34c 100644 --- a/src/tactic/arith/arith_bounds_tactic.h +++ b/src/tactic/arith/arith_bounds_tactic.h @@ -27,6 +27,8 @@ Module Name: for assembling bounds, but it does not have a way to check for subsumption of atoms. +## Tactic arith-bounds + --*/ #pragma once #include "tactic/tactic.h" diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index eda079e4691..63455864d98 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -128,9 +128,8 @@ struct cofactor_elim_term_ite::imp { fr.m_first = false; bool visited = true; if (is_app(t)) { - unsigned num_args = to_app(t)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - visit(to_app(t)->get_arg(i), form_ctx, visited); + for (expr* arg : *to_app(t)) + visit(arg, form_ctx, visited); } // ignoring quantifiers if (!visited) @@ -138,16 +137,13 @@ struct cofactor_elim_term_ite::imp { } if (is_app(t)) { - unsigned num_args = to_app(t)->get_num_args(); - unsigned i; - for (i = 0; i < num_args; i++) { - if (m_has_term_ite.is_marked(to_app(t)->get_arg(i))) + for (expr* arg : *to_app(t)) { + if (m_has_term_ite.is_marked(arg)) { + m_has_term_ite.mark(t); + TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); + save_candidate(t, form_ctx); break; - } - if (i < num_args) { - m_has_term_ite.mark(t); - TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";); - save_candidate(t, form_ctx); + } } } else { @@ -284,16 +280,14 @@ struct cofactor_elim_term_ite::imp { } expr * best = nullptr; unsigned best_occs = 0; - obj_map::iterator it = occs.begin(); - obj_map::iterator end = occs.end(); - for (; it != end; ++it) { + for (auto const& [k, v] : occs) { if ((!best) || - (get_depth(it->m_key) < get_depth(best)) || - (get_depth(it->m_key) == get_depth(best) && it->m_value > best_occs) || + (get_depth(k) < get_depth(best)) || + (get_depth(k) == get_depth(best) && v > best_occs) || // break ties by giving preference to equalities - (get_depth(it->m_key) == get_depth(best) && it->m_value == best_occs && m.is_eq(it->m_key) && !m.is_eq(best))) { - best = it->m_key; - best_occs = it->m_value; + (get_depth(k) == get_depth(best) && v == best_occs && m.is_eq(k) && !m.is_eq(best))) { + best = k; + best_occs = v; } } visited.reset(); diff --git a/src/tactic/core/cofactor_term_ite_tactic.h b/src/tactic/core/cofactor_term_ite_tactic.h index e10a310f2ae..68568c8cef1 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.h +++ b/src/tactic/core/cofactor_term_ite_tactic.h @@ -8,13 +8,22 @@ Module Name: Abstract: Wrap cofactor_elim_term_ite as a tactic. - Eliminate (ground) term if-then-else's using cofactors. Author: Leonardo de Moura (leonardo) 2012-02-20. -Revision History: +Tactic Documentation: + +## Tactic cofactor-term-ite + +### Short Description +Eliminate (ground) term if-then-else's using cofactors. +It hoists nested if-then-else expressions inside terms into the top level of the formula. + +### Notes + +* does not support proofs, does not support cores --*/ #pragma once diff --git a/src/tactic/core/euf_completion_tactic.h b/src/tactic/core/euf_completion_tactic.h index 36511bbe343..a1c9166ea23 100644 --- a/src/tactic/core/euf_completion_tactic.h +++ b/src/tactic/core/euf_completion_tactic.h @@ -13,6 +13,22 @@ Module Name: Nikolaj Bjorner (nbjorner) 2022-10-30 +Tactic Documentation: + +## Tactic euf-completion + +### Short Description + +Uses the ground equalities as a rewrite system. The formulas are simplified +using the rewrite system. + +### Long Description + +The tactic uses congruence closure to represent and orient the rewrite system. Equalities from the formula +are inserted in the an E-graph (congruence closure structure) and then a representative that is most shallow +is extracted. + + --*/ #pragma once diff --git a/src/tactic/core/reduce_args_tactic.h b/src/tactic/core/reduce_args_tactic.h index 615b4d70fc8..749aadd9c06 100644 --- a/src/tactic/core/reduce_args_tactic.h +++ b/src/tactic/core/reduce_args_tactic.h @@ -34,31 +34,10 @@ Thus, we replace the $f(t_1, t_2)$ with Since $f_a$, $f_b$, $f_c$ are new symbols, satisfiability is preserved. This transformation is very similar in spirit to the Ackermman's reduction. +For each function `f` and argument position of `f` it checks if all occurrences of `f` uses a value at position `i`. +The values may be different, but all occurrences have to be values for the reduction to be applicable. +It creates a fresh function for each of the different values at position `i`. -This transformation should work in the following way: - -``` - 1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)] - means that f is a declaration with 3 arguments where the first and third arguments are always values. - 2- Traverse the formula and populate the mapping. - For each function application f(t1, ..., tn) do - a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do - the logical-and with the tuple that is already in the mapping. If there is no such tuple - in the mapping, we just add a new entry. - - If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable. - - Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry, - but it is the same for the same declaration. - For example, suppose we have [f -> (true, false, true)] in decl2arg_map, - and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula. - Then, decl2arg_map would contain - (f, 1, 2) -> f_1_2 - (f, 1, 3) -> f_1_3 - (f, 2, 3) -> f_2_3 - where f_1_2, f_1_3 and f_2_3 are new function symbols. - Using the new map, we can replace the occurrences of f. -``` ### Example diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index 667d53626b9..bd2f58b442e 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -865,11 +865,11 @@ class tseitin_cnf_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { insert_max_memory(r); - r.insert("common_patterns", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns"); - r.insert("distributivity", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas"); - r.insert("distributivity_blowup", CPK_UINT, "(default: 32) maximum overhead for applying distributivity during CNF encoding"); - r.insert("ite_chaing", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains"); - r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas"); + r.insert("common_patterns", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns", "true"); + r.insert("distributivity", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas", "true"); + r.insert("distributivity_blowup", CPK_UINT, "maximum overhead for applying distributivity during CNF encoding", "32"); + r.insert("ite_chaing", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains", "true"); + r.insert("ite_extra", CPK_BOOL, "add redundant clauses (that improve unit propagation) when encoding if-then-else formulas", "true"); } void operator()(goal_ref const & in, goal_ref_buffer & result) override { diff --git a/src/tactic/fpa/fpa2bv_tactic.h b/src/tactic/fpa/fpa2bv_tactic.h index 0845aafa200..57b6d498529 100644 --- a/src/tactic/fpa/fpa2bv_tactic.h +++ b/src/tactic/fpa/fpa2bv_tactic.h @@ -5,15 +5,16 @@ Module Name: fpa2bv_tactic.h -Abstract: - - Tactic that converts floating points to bit-vectors - Author: Christoph (cwinter) 2012-02-09 -Notes: +Tactic Documentation: + +## Tactic fpa2bv + +### Short Description +Converts floating points to bit-vector representation. --*/ #pragma once diff --git a/src/tactic/fpa/qffp_tactic.h b/src/tactic/fpa/qffp_tactic.h index e4c8eb38699..fb1a46afd5f 100644 --- a/src/tactic/fpa/qffp_tactic.h +++ b/src/tactic/fpa/qffp_tactic.h @@ -13,8 +13,17 @@ Module Name: Christoph (cwinter) 2012-01-16 -Notes: +Tactic Documentation: +## Tactic qffp + +### Short Description +Tactic for QF_FP formulas + +## Tactic qffpbv + +### Short Description +Tactic for QF_FPBV formulas --*/ #pragma once diff --git a/src/tactic/fpa/qffplra_tactic.h b/src/tactic/fpa/qffplra_tactic.h index af862db2997..543e6f23afe 100644 --- a/src/tactic/fpa/qffplra_tactic.h +++ b/src/tactic/fpa/qffplra_tactic.h @@ -14,7 +14,8 @@ Module Name: Christoph (cwinter) 2018-04-24 -Notes: + +## Tactic qffplra --*/