diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index ab3dd0b65c2..80e50c61561 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -41,6 +41,7 @@ namespace euf { enode* n = enode::mk(m_region, f, num_args, args); m_nodes.push_back(n); m_exprs.push_back(f); + m_expr2enode.setx(f->get_id(), n, nullptr); push_node(n); for (unsigned i = 0; i < num_args; ++i) set_merge_enabled(args[i], true); @@ -65,7 +66,7 @@ namespace euf { void egraph::reinsert_equality(enode* p) { SASSERT(is_equality(p)); - if (p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) { + if (p->get_arg(0)->get_root() == p->get_arg(1)->get_root() && m_value(p) != l_true) { add_literal(p, true); } } @@ -97,8 +98,7 @@ namespace euf { SASSERT(!find(f)); force_push(); enode *n = mk_enode(f, num_args, args); - SASSERT(n->class_size() == 1); - m_expr2enode.setx(f->get_id(), n, nullptr); + SASSERT(n->class_size() == 1); if (num_args == 0 && m.is_unique_value(f)) n->mark_interpreted(); if (num_args == 0) @@ -110,26 +110,17 @@ namespace euf { } enode_bool_pair p = m_table.insert(n); enode* n2 = p.first; - if (n2 == n) { - update_children(n); - } - else { - merge(n, n2, justification::congruence(p.second)); -#if 0 - SASSERT(n2->get_expr() != n->get_expr()); - SASSERT(n->class_size() == 1); - SASSERT(n->is_root()); - merge_justification(n, n2, justification::congruence(p.second)); - enode* r2 = n2->get_root(); - std::swap(n->m_next, r2->m_next); - n->m_root = r2; - r2->inc_class_size(n->class_size()); - push_eq(n, n, r2->num_parents()); -#endif - } + if (n2 == n) + update_children(n); + else + merge(n, n2, justification::congruence(p.second)); return n; } + egraph::egraph(ast_manager& m) : m(m), m_table(m), m_exprs(m) { + m_tmp_eq = enode::mk_tmp(m_region, 2); + } + egraph::~egraph() { for (enode* n : m_nodes) n->m_parents.finalize(); @@ -142,6 +133,15 @@ namespace euf { ++m_stats.m_num_th_eqs; } + void egraph::add_th_diseq(theory_id id, theory_var v1, theory_var v2, expr* eq) { + if (!th_propagates_diseqs(id)) + return; + TRACE("euf_verbose", tout << "eq: " << v1 << " != " << v2 << "\n";); + m_new_th_eqs.push_back(th_eq(id, v1, v2, eq)); + m_updates.push_back(update_record(update_record::new_th_eq())); + ++m_stats.m_num_th_diseqs; + } + void egraph::add_literal(enode* n, bool is_eq) { TRACE("euf_verbose", tout << "lit: " << n->get_expr_id() << "\n";); m_new_lits.push_back(enode_bool_pair(n, is_eq)); @@ -149,6 +149,68 @@ namespace euf { if (is_eq) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits; } + void egraph::new_diseq(enode* n1) { + SASSERT(m.is_eq(n1->get_expr())); + enode* arg1 = n1->get_arg(0), * arg2 = n1->get_arg(1); + enode* r1 = arg1->get_root(); + enode* r2 = arg2->get_root(); + TRACE("euf", tout << "new-diseq: " << mk_pp(r1->get_expr(), m) << " " << mk_pp(r2->get_expr(), m) << ": " << r1->has_th_vars() << " " << r2->has_th_vars() << "\n";); + if (r1 == r2) + return; + if (!r1->has_th_vars()) + return; + if (!r2->has_th_vars()) + return; + if (r1->has_one_th_var() && r2->has_one_th_var() && r1->get_first_th_id() == r2->get_first_th_id()) { + theory_id id = r1->get_first_th_id(); + if (!th_propagates_diseqs(id)) + return; + theory_var v1 = arg1->get_closest_th_var(id); + theory_var v2 = arg2->get_closest_th_var(id); + add_th_diseq(id, v1, v2, n1->get_expr()); + return; + } + for (auto p : euf::enode_th_vars(r1)) { + if (!th_propagates_diseqs(p.get_id())) + continue; + for (auto q : euf::enode_th_vars(r2)) + if (p.get_id() == q.get_id()) + add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n1->get_expr()); + } + } + + + /* + * Propagate disequalities over equality atoms that are assigned to false. + */ + + void egraph::add_th_diseqs(theory_id id, theory_var v1, enode* r) { + SASSERT(r->is_root()); + if (!th_propagates_diseqs(id)) + return; + for (enode* p : enode_parents(r)) { + if (m.is_eq(p->get_expr()) && m.is_false(p->get_root()->get_expr())) { + enode* n = nullptr; + n = (r == p->get_arg(0)->get_root()) ? p->get_arg(1) : p->get_arg(0); + n = n->get_root(); + theory_var v2 = n->get_closest_th_var(id); + if (v2 != null_theory_var) + add_th_diseq(id, v1, v2, p->get_expr()); + } + } + } + + void egraph::set_th_propagates_diseqs(theory_id id) { + m_th_propagates_diseqs.reserve(id + 1, false); + m_th_propagates_diseqs[id] = true; + } + + bool egraph::th_propagates_diseqs(theory_id id) const { + return m_th_propagates_diseqs.get(id, false); + } + + + void egraph::add_th_var(enode* n, theory_var v, theory_id id) { force_push(); theory_var w = n->get_th_var(id); @@ -159,10 +221,12 @@ namespace euf { m_updates.push_back(update_record(n, id, update_record::add_th_var())); if (r != n) { theory_var u = r->get_th_var(id); - if (u == null_theory_var) + if (u == null_theory_var) { r->add_th_var(v, id, m_region); - else - add_th_eq(id, v, u, n, r); + add_th_diseqs(id, v, r); + } + else + add_th_eq(id, v, u, n, r); } } else { @@ -201,10 +265,12 @@ namespace euf { 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 = [&](enode* n) { - if (n->num_args() > 1) + auto undo_node = [&]() { + enode* n = m_nodes.back(); + expr* e = m_exprs.back(); + if (n->num_args() > 0) m_table.erase(n); - m_expr2enode[n->get_expr_id()] = nullptr; + m_expr2enode[e->get_id()] = nullptr; n->~enode(); m_nodes.pop_back(); m_exprs.pop_back(); @@ -213,7 +279,7 @@ namespace euf { auto const& p = m_updates[i]; switch (p.tag) { case update_record::tag_t::is_add_node: - undo_node(p.r1); + undo_node(); break; case update_record::tag_t::is_toggle_merge: p.r1->set_merge_enabled(!p.r1->merge_enabled()); @@ -257,13 +323,13 @@ namespace euf { SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size()); } - void egraph::merge(enode* n1, enode* n2, justification j) { + void egraph::merge(enode* n1, enode* n2, justification j) { SASSERT(m.get_sort(n1->get_expr()) == m.get_sort(n2->get_expr())); enode* r1 = n1->get_root(); enode* r2 = n2->get_root(); if (r1 == r2) return; - TRACE("euf", j.display(tout << n1->get_expr_id() << " == " << n2->get_expr_id() << " ", m_display_justification) << "\n";); + TRACE("euf", j.display(tout << "merge: " << mk_bounded_pp(n1->get_expr(), m) << " == " << mk_bounded_pp(n2->get_expr(), m) << " ", m_display_justification) << "\n";); force_push(); SASSERT(m_num_scopes == 0); ++m_stats.m_num_merge; @@ -275,9 +341,10 @@ namespace euf { std::swap(r1, r2); std::swap(n1, n2); } - if ((m.is_true(r2->get_expr()) || m.is_false(r2->get_expr())) && j.is_congruence()) { - add_literal(n1, false); - } + if ((m.is_true(r2->get_expr()) || m.is_false(r2->get_expr())) && j.is_congruence()) + add_literal(n1, false); + if (m.is_false(r2->get_expr()) && m.is_eq(n1->get_expr())) + new_diseq(n1); for (enode* p : enode_parents(n1)) m_table.erase(p); for (enode* p : enode_parents(n2)) @@ -301,6 +368,7 @@ namespace euf { if (v == null_theory_var) { root->add_th_var(iv.get_var(), id, m_region); m_updates.push_back(update_record(root, id, update_record::add_th_var())); + add_th_diseqs(id, iv.get_var(), root); } else { SASSERT(v != iv.get_var()); @@ -378,6 +446,25 @@ namespace euf { SASSERT(!n1->get_root()->m_target); } + bool egraph::are_diseq(enode* a, enode* b) const { + enode* ra = a->get_root(), * rb = b->get_root(); + if (ra == rb) + return false; + if (ra->interpreted() && rb->interpreted()) + return true; + if (m.get_sort(ra->get_expr()) != m.get_sort(rb->get_expr())) + return true; + expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m); + m_tmp_eq->m_args[0] = a; + m_tmp_eq->m_args[1] = b; + m_tmp_eq->m_expr = eq; + SASSERT(m_tmp_eq->num_args() == 2); + enode* r = m_table.find(m_tmp_eq); + if (r && m_value(r->get_root()) == l_false) + return true; + return false; + } + /** \brief generate an explanation for a congruence. Each pair of children under a congruence have the same roots @@ -529,9 +616,10 @@ namespace euf { void egraph::collect_statistics(statistics& st) const { st.update("euf merge", m_stats.m_num_merge); st.update("euf conflicts", m_stats.m_num_conflicts); - st.update("euf equality propagations", m_stats.m_num_eqs); - st.update("euf theory equality propagations", m_stats.m_num_th_eqs); - st.update("euf literal propagations", m_stats.m_num_lits); + st.update("euf propagations eqs", m_stats.m_num_eqs); + st.update("euf propagations theory eqs", m_stats.m_num_th_eqs); + st.update("euf propagations theory diseqs", m_stats.m_num_th_diseqs); + st.update("euf propagations literal", m_stats.m_num_lits); } void egraph::copy_from(egraph const& src, std::function& copy_justification) { diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index e47f3d30451..52421f43d7f 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -26,26 +26,47 @@ Module Name: #pragma once #include "util/statistics.h" #include "util/trail.h" +#include "util/lbool.h" #include "ast/euf/euf_enode.h" #include "ast/euf/euf_etable.h" namespace euf { /*** - \brief store derived theory equalities. - Theory 'id' is notified with the equality of theory variables v1, v2 - that are merged into the common root of child and root (their roots may + \brief store derived theory equalities and disequalities + Theory 'id' is notified with the equality/disequality of theory variables v1, v2. + For equalities, v1 and v2 are merged into the common root of child and root (their roots may have been updated since the equality was derived, but the explanation for v1 == v2 is provided by explaining the equality child == root. + For disequalities, m_child refers to an equality atom of the form e1 == e2. + It is equal to false under the current context. + The explanation for the disequality v1 != v2 is derived from explaining the + equality between the expression for v1 and e1, and the expression for v2 and e2 + and the equality of m_eq and false: the literal corresponding to m_eq is false in the + current assignment stack, or m_child is congruent to false in the egraph. */ - struct th_eq { + class th_eq { + theory_id m_id; theory_var m_v1; theory_var m_v2; - enode* m_child; + union { + enode* m_child; + expr* m_eq; + }; enode* m_root; + public: + bool is_eq() const { return m_root != nullptr; } + theory_id id() const { return m_id; } + theory_var v1() const { return m_v1; } + theory_var v2() const { return m_v2; } + enode* child() const { SASSERT(is_eq()); return m_child; } + enode* root() const { SASSERT(is_eq()); return m_root; } + expr* eq() const { SASSERT(!is_eq()); return m_eq; } th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r) : m_id(id), m_v1(v1), m_v2(v2), m_child(c), m_root(r) {} + th_eq(theory_id id, theory_var v1, theory_var v2, expr* eq) : + m_id(id), m_v1(v1), m_v2(v2), m_eq(eq), m_root(nullptr) {} }; class egraph { @@ -53,6 +74,7 @@ namespace euf { struct stats { unsigned m_num_merge; unsigned m_num_th_eqs; + unsigned m_num_th_diseqs; unsigned m_num_lits; unsigned m_num_eqs; unsigned m_num_conflicts; @@ -111,6 +133,7 @@ namespace euf { svector m_updates; unsigned_vector m_scopes; enode_vector m_expr2enode; + enode* m_tmp_eq { nullptr }; enode_vector m_nodes; expr_ref_vector m_exprs; unsigned m_num_scopes { 0 }; @@ -122,11 +145,13 @@ namespace euf { 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; stats m_stats; std::function m_used_eq; std::function m_used_cc; std::function m_display_justification; + std::function m_value; void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) { m_updates.push_back(update_record(r1, n1, r2_num_parents)); @@ -134,6 +159,10 @@ namespace euf { void push_node(enode* n) { m_updates.push_back(update_record(n)); } void add_th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r); + + void new_diseq(enode* n1); + void add_th_diseqs(theory_id id, theory_var v1, enode* r); + bool th_propagates_diseqs(theory_id id) const; void add_literal(enode* n, bool is_eq); void undo_eq(enode* r1, enode* n1, unsigned r2_num_parents); void undo_add_th_var(enode* n, theory_id id); @@ -166,7 +195,7 @@ namespace euf { std::ostream& display(std::ostream& out, unsigned max_args, enode* n) const; public: - egraph(ast_manager& m): m(m), m_table(m), m_exprs(m) {} + egraph(ast_manager& m); ~egraph(); enode* find(expr* f) { return m_expr2enode.get(f->get_id(), nullptr); } enode* mk(expr* f, unsigned n, enode *const* args); @@ -192,12 +221,18 @@ namespace euf { bool propagate(); bool inconsistent() const { return m_inconsistent; } + /** + * \brief check if two nodes are known to be disequal. + */ + bool are_diseq(enode* a, enode* b) const; + /** \brief Maintain and update cursor into propagated consequences. The result of get_literal() is a pair (n, is_eq) where \c n is an enode and \c is_eq indicates whether the enode 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_bool_pair get_literal() const { return m_new_lits[m_new_lits_qhead]; } @@ -205,13 +240,14 @@ namespace euf { 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 add_th_var(enode* n, theory_var v, theory_id id); + void set_th_propagates_diseqs(theory_id id); void set_merge_enabled(enode* n, bool enable_merge); 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; } void set_display_justification(std::function & d) { m_display_justification = d; } + void set_eval(std::function& eval) { m_value = eval; } void begin_explain(); void end_explain(); diff --git a/src/ast/euf/euf_enode.cpp b/src/ast/euf/euf_enode.cpp index 538f2174ce1..c88d34eefdd 100644 --- a/src/ast/euf/euf_enode.cpp +++ b/src/ast/euf/euf_enode.cpp @@ -70,6 +70,21 @@ namespace euf { return true; } + /* + * Find the theory var that that is heuristically + * linked with the fewest equality justifications. + */ + theory_var enode::get_closest_th_var(theory_id id) const { + enode const* n = this; + while (n) { + theory_var v = n->get_th_var(id); + if (v != null_theory_var) + return v; + n = n->m_target; + } + return null_theory_var; + } + bool enode::acyclic() const { enode const* n = this; enode const* p = this; diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index 520b1a44f58..f5a709d0f10 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -36,23 +36,23 @@ namespace euf { const theory_id null_theory_id = -1; class enode { - expr* m_expr{ nullptr }; - bool m_mark1 { false }; - bool m_mark2 { false }; - bool m_commutative { false }; - bool m_update_children { false }; - bool m_interpreted { false }; - bool m_merge_enabled { true }; - unsigned m_class_size { 1 }; - unsigned m_table_id { UINT_MAX }; + expr* m_expr{ nullptr }; + bool m_mark1{ false }; + bool m_mark2{ false }; + bool m_commutative{ false }; + bool m_update_children{ false }; + bool m_interpreted{ false }; + bool m_merge_enabled{ true }; + unsigned m_class_size{ 1 }; + unsigned m_table_id{ UINT_MAX }; enode_vector m_parents; - enode* m_next{ nullptr }; - enode* m_root{ nullptr }; - enode* m_target { nullptr }; + enode* m_next{ nullptr }; + enode* m_root{ nullptr }; + enode* m_target{ nullptr }; th_var_list m_th_vars; justification m_justification; - unsigned m_num_args { 0 }; - enode* m_args[0]; + unsigned m_num_args{ 0 }; + enode* m_args[0]; friend class enode_args; friend class enode_parents; @@ -81,6 +81,20 @@ namespace euf { } return n; } + + static enode* mk_tmp(region& r, unsigned num_args) { + void* mem = r.allocate(get_enode_size(num_args)); + enode* n = new (mem) enode(); + n->m_expr = nullptr; + n->m_next = n; + n->m_root = n; + n->m_commutative = true; + n->m_num_args = 2; + n->m_merge_enabled = true; + for (unsigned i = 0; i < num_args; ++i) + n->m_args[i] = nullptr; + return n; + } void set_update_children() { m_update_children = true; } @@ -148,10 +162,12 @@ namespace euf { unsigned get_expr_id() const { return m_expr->get_id(); } unsigned get_root_id() const { return m_root->m_expr->get_id(); } theory_var get_th_var(theory_id id) const { return m_th_vars.find(id); } + theory_var get_closest_th_var(theory_id id) const; bool is_attached_to(theory_id id) const { return get_th_var(id) != null_theory_var; } bool has_th_vars() const { return !m_th_vars.empty(); } bool has_one_th_var() const { return !m_th_vars.empty() && !m_th_vars.get_next();} theory_var get_first_th_id() const { SASSERT(has_th_vars()); return m_th_vars.get_id(); } + void inc_class_size(unsigned n) { m_class_size += n; } void dec_class_size(unsigned n) { m_class_size -= n; } diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index f7dc7485acd..25af69178f1 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -5,6 +5,7 @@ z3_add_component(sat sat_aig_finder.cpp sat_anf_simplifier.cpp sat_asymm_branch.cpp + sat_bcd.cpp sat_big.cpp sat_binspr.cpp sat_clause.cpp @@ -18,7 +19,7 @@ z3_add_component(sat sat_drat.cpp sat_elim_eqs.cpp sat_elim_vars.cpp - sat_bcd.cpp + sat_gc.cpp sat_integrity_checker.cpp sat_local_search.cpp sat_lookahead.cpp diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp index 155d3a77b8f..aecc77a58d2 100644 --- a/src/sat/dimacs.cpp +++ b/src/sat/dimacs.cpp @@ -235,12 +235,15 @@ namespace dimacs { skip_whitespace(in); switch (*in) { case EOF: - return false; + return false; case 'c': + // parse comment line case 'p': + // parse meta-data information skip_line(in); goto loop; case 'i': + // parse input clause ++in; skip_whitespace(in); read_clause(in, err, m_record.m_lits); @@ -248,6 +251,7 @@ namespace dimacs { m_record.m_status = sat::status::input(); break; case 'a': + // parse non-redundant theory clause ++in; skip_whitespace(in); theory_id = read_theory_id(); @@ -256,16 +260,32 @@ namespace dimacs { m_record.m_tag = drat_record::tag_t::is_clause; m_record.m_status = sat::status::th(false, theory_id); break; + case 'g': + // parse garbage collected Boolean variable + ++in; + skip_whitespace(in); + b = parse_int(in, err); + e = parse_int(in, err); + if (e != 0 || b <= 0) + throw lex_error(); + m_record.m_tag = drat_record::tag_t::is_var_gc; + m_record.m_node_id = b; + break; case 'e': + // parse expression definition parse_ast(drat_record::tag_t::is_node); break; case 'f': + // parse function declaration parse_ast(drat_record::tag_t::is_decl); break; case 's': + // parse sort declaration (not used) parse_ast(drat_record::tag_t::is_sort); break; case 'b': + // parse bridge between Boolean variable identifier b + // and expression identifier e, which is of type Bool ++in; skip_whitespace(in); b = parse_int(in, err); @@ -279,6 +299,7 @@ namespace dimacs { m_record.m_args.push_back(n); break; case 'd': + // parse clause deletion ++in; skip_whitespace(in); read_clause(in, err, m_record.m_lits); @@ -286,6 +307,8 @@ namespace dimacs { m_record.m_status = sat::status::deleted(); break; case 'r': + // parse redundant theory clause + // the clause must be DRUP redundant modulo T ++in; skip_whitespace(in); theory_id = read_theory_id(); @@ -294,6 +317,7 @@ namespace dimacs { m_record.m_status = sat::status::th(true, theory_id); break; default: + // parse clause redundant modulo DRAT (or mostly just DRUP) read_clause(in, err, m_record.m_lits); m_record.m_tag = drat_record::tag_t::is_clause; m_record.m_status = sat::status::redundant(); diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h index 690f5b0fc96..eaf6a3a5fec 100644 --- a/src/sat/dimacs.h +++ b/src/sat/dimacs.h @@ -53,7 +53,7 @@ namespace dimacs { }; struct drat_record { - enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def }; + enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def, is_var_gc }; tag_t m_tag{ tag_t::is_clause }; // a clause populates m_lits and m_status // a node populates m_node_id, m_name, m_args diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index 045ba9a9585..f1a44296ec0 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -165,6 +165,7 @@ namespace sat { explicit clause_wrapper(clause & c):m_cls(&c), m_l2_idx(null_literal.to_uint()) {} bool is_binary() const { return m_l2_idx != null_literal.to_uint(); } + bool is_ternary() const { return size() == 3; } unsigned size() const { return is_binary() ? 2 : m_cls->size(); } literal operator[](unsigned idx) const { SASSERT(idx < size()); @@ -178,6 +179,20 @@ namespace sat { bool contains(bool_var v) const; clause * get_clause() const { SASSERT(!is_binary()); return m_cls; } bool was_removed() const { return !is_binary() && get_clause()->was_removed(); } + bool is_learned() const { return !is_binary() && get_clause()->is_learned(); } + + class iterator { + unsigned m_idx; + clause_wrapper const& m_cw; + public: + iterator(clause_wrapper const& c, unsigned idx): m_idx(idx), m_cw(c) {} + iterator& operator++() { ++m_idx; return *this; } + literal operator*() { return m_cw[m_idx]; } + bool operator==(iterator const& other) const { SASSERT(&m_cw == &other.m_cw); return m_idx == other.m_idx; } + bool operator!=(iterator const& other) const { SASSERT(&m_cw == &other.m_cw); return m_idx != other.m_idx; } + }; + iterator begin() const { return iterator(*this, 0); } + iterator end() const { return iterator(*this, size()); } }; typedef svector clause_wrapper_vector; diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 20d7c8f1e2a..6c30d4ad64e 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -257,6 +257,22 @@ namespace sat { } } + void drat::gc_var(bool_var v) { + sat::literal l(v, false); + // TBD: we want to remove all clauses that mention v. + std::cout << "GC " << v << "\n"; + m_watches[l.index()].reset(); + m_watches[(~l).index()].reset(); + if (m_assignment[l.var()] != l_undef) { + unsigned j = 0; + for (literal lit : m_units) + if (lit.var() != v) + m_units[j++] = lit; + m_units.shrink(j); + m_assignment[l.var()] = l_undef; + } + } + void drat::bool_def(bool_var v, unsigned n) { if (m_out) (*m_out) << "b " << v << " " << n << " 0\n"; @@ -277,6 +293,11 @@ namespace sat { (*m_out) << " 0\n"; } + void drat::log_gc_var(bool_var v) { + if (m_out) + (*m_out) << "g " << v << " 0\n"; + } + void drat::log_adhoc(std::function& fn) { if (m_out) fn(*m_out); diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index f39d1801700..b0f84f7b74a 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -38,6 +38,12 @@ Module Name: Redundant clause (theory lemma if theory id is given) [r []] * 0 + Declaration of an auxiliary function: + f 0 + + Garbage collection of a Boolean variable: + g 0 + Available theories are: - euf The theory lemma should be a consequence of congruence closure. - ba TBD (need to also log cardinality and pb constraints) @@ -125,6 +131,8 @@ namespace sat { void add(literal_vector const& c); // add learned clause void add(unsigned sz, literal const* lits, status st); + void gc_var(bool_var v); + // support for SMT - connect Boolean variables with AST nodes // associate AST node id with Boolean variable v void bool_def(bool_var v, unsigned n); @@ -134,6 +142,8 @@ namespace sat { void def_add_arg(unsigned arg); void def_end(); + void log_gc_var(bool_var v); + // ad-hoc logging until a format is developed void log_adhoc(std::function& fn); diff --git a/src/sat/sat_gc.cpp b/src/sat/sat_gc.cpp new file mode 100644 index 00000000000..96d0f495ac0 --- /dev/null +++ b/src/sat/sat_gc.cpp @@ -0,0 +1,562 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + sat_solver.cpp + +Abstract: + + SAT solver main class. + +Author: + + Leonardo de Moura (leonardo) 2011-05-21. + +Revision History: + +--*/ + + +#include "sat/sat_solver.h" + +#define ENABLE_TERNARY true + +namespace sat { + + // ----------------------- + // + // GC + // + // ----------------------- + + bool solver::should_gc() const { + return + m_conflicts_since_gc > m_gc_threshold && + (m_config.m_gc_strategy != GC_DYN_PSM || at_base_lvl()); + } + + void solver::do_gc() { + if (!should_gc()) return; + TRACE("sat", tout << m_conflicts_since_gc << " " << m_gc_threshold << "\n";); + unsigned gc = m_stats.m_gc_clause; + m_conflicts_since_gc = 0; + m_gc_threshold += m_config.m_gc_increment; + IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";); + CASSERT("sat_gc_bug", check_invariant()); + switch (m_config.m_gc_strategy) { + case GC_GLUE: + gc_glue(); + break; + case GC_PSM: + gc_psm(); + break; + case GC_GLUE_PSM: + gc_glue_psm(); + break; + case GC_PSM_GLUE: + gc_psm_glue(); + break; + case GC_DYN_PSM: + if (!m_assumptions.empty()) { + gc_glue_psm(); + break; + } + if (!at_base_lvl()) + return; + gc_dyn_psm(); + break; + default: + UNREACHABLE(); + break; + } + if (m_ext) m_ext->gc(); + if (gc > 0 && should_defrag()) { + defrag_clauses(); + } + CASSERT("sat_gc_bug", check_invariant()); + } + + /** + \brief Lex on (glue, size) + */ + struct glue_lt { + bool operator()(clause const * c1, clause const * c2) const { + if (c1->glue() < c2->glue()) return true; + return c1->glue() == c2->glue() && c1->size() < c2->size(); + } + }; + + /** + \brief Lex on (psm, size) + */ + struct psm_lt { + bool operator()(clause const * c1, clause const * c2) const { + if (c1->psm() < c2->psm()) return true; + return c1->psm() == c2->psm() && c1->size() < c2->size(); + } + }; + + /** + \brief Lex on (glue, psm, size) + */ + struct glue_psm_lt { + bool operator()(clause const * c1, clause const * c2) const { + if (c1->glue() < c2->glue()) return true; + if (c1->glue() > c2->glue()) return false; + if (c1->psm() < c2->psm()) return true; + if (c1->psm() > c2->psm()) return false; + return c1->size() < c2->size(); + } + }; + + /** + \brief Lex on (psm, glue, size) + */ + struct psm_glue_lt { + bool operator()(clause const * c1, clause const * c2) const { + if (c1->psm() < c2->psm()) return true; + if (c1->psm() > c2->psm()) return false; + if (c1->glue() < c2->glue()) return true; + if (c1->glue() > c2->glue()) return false; + return c1->size() < c2->size(); + } + }; + + void solver::gc_glue() { + std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt()); + gc_half("glue"); + } + + void solver::gc_psm() { + save_psm(); + std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt()); + gc_half("psm"); + } + + void solver::gc_glue_psm() { + save_psm(); + std::stable_sort(m_learned.begin(), m_learned.end(), glue_psm_lt()); + gc_half("glue-psm"); + } + + void solver::gc_psm_glue() { + save_psm(); + std::stable_sort(m_learned.begin(), m_learned.end(), psm_glue_lt()); + gc_half("psm-glue"); + } + + /** + \brief Compute the psm of all learned clauses. + */ + void solver::save_psm() { + for (clause* cp : m_learned) { + cp->set_psm(psm(*cp)); + } + } + + /** + \brief GC (the second) half of the clauses in the database. + */ + void solver::gc_half(char const * st_name) { + TRACE("sat", tout << "gc\n";); + unsigned sz = m_learned.size(); + unsigned new_sz = sz/2; // std::min(sz/2, m_clauses.size()*2); + unsigned j = new_sz; + for (unsigned i = new_sz; i < sz; i++) { + clause & c = *(m_learned[i]); + if (can_delete(c)) { + detach_clause(c); + del_clause(c); + } + else { + m_learned[j] = &c; + j++; + } + } + new_sz = j; + m_stats.m_gc_clause += sz - new_sz; + m_learned.shrink(new_sz); + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";); + } + + bool solver::can_delete3(literal l1, literal l2, literal l3) const { + if (value(l1) == l_true && + value(l2) == l_false && + value(l3) == l_false) { + justification const& j = m_justification[l1.var()]; + if (j.is_ternary_clause()) { + watched w1(l2, l3); + watched w2(j.get_literal1(), j.get_literal2()); + return w1 != w2; + } + } + return true; + } + + bool solver::can_delete(clause const & c) const { + if (c.on_reinit_stack()) + return false; + if (ENABLE_TERNARY && c.size() == 3) { + return + can_delete3(c[0],c[1],c[2]) && + can_delete3(c[1],c[0],c[2]) && + can_delete3(c[2],c[0],c[1]); + } + literal l0 = c[0]; + if (value(l0) != l_true) + return true; + justification const & jst = m_justification[l0.var()]; + return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; + } + + /** + \brief Use gc based on dynamic psm. Clauses are initially frozen. + */ + void solver::gc_dyn_psm() { + TRACE("sat", tout << "gc\n";); + // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact + // that I may miss some propagations for reactivated clauses. + SASSERT(at_base_lvl()); + // compute + // d_tk + unsigned h = 0; + unsigned V_tk = 0; + for (bool_var v = 0; v < num_vars(); v++) { + if (m_assigned_since_gc[v]) { + V_tk++; + m_assigned_since_gc[v] = false; + } + if (m_phase[v] != m_prev_phase[v]) { + h++; + m_prev_phase[v] = m_phase[v]; + } + } + double d_tk = V_tk == 0 ? static_cast(num_vars() + 1) : static_cast(h)/static_cast(V_tk); + if (d_tk < m_min_d_tk) + m_min_d_tk = d_tk; + TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";); + unsigned frozen = 0; + unsigned deleted = 0; + unsigned activated = 0; + clause_vector::iterator it = m_learned.begin(); + clause_vector::iterator it2 = it; + clause_vector::iterator end = m_learned.end(); + for (; it != end; ++it) { + clause & c = *(*it); + if (!c.frozen()) { + // Active clause + if (c.glue() > m_config.m_gc_small_lbd) { + // I never delete clauses with small lbd + if (c.was_used()) { + c.reset_inact_rounds(); + } + else { + c.inc_inact_rounds(); + if (c.inact_rounds() > m_config.m_gc_k) { + detach_clause(c); + del_clause(c); + m_stats.m_gc_clause++; + deleted++; + continue; + } + } + c.unmark_used(); + if (psm(c) > static_cast(c.size() * m_min_d_tk)) { + // move to frozen; + TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";); + detach_clause(c); + c.reset_inact_rounds(); + c.freeze(); + m_num_frozen++; + frozen++; + } + } + } + else { + // frozen clause + clause & c = *(*it); + if (psm(c) <= static_cast(c.size() * m_min_d_tk)) { + c.unfreeze(); + m_num_frozen--; + activated++; + if (!activate_frozen_clause(c)) { + // clause was satisfied, reduced to a conflict, unit or binary clause. + del_clause(c); + continue; + } + } + else { + c.inc_inact_rounds(); + if (c.inact_rounds() > m_config.m_gc_k) { + del_clause(c); + m_stats.m_gc_clause++; + deleted++; + continue; + } + } + } + *it2 = *it; + ++it2; + } + m_learned.set_end(it2); + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk << + " :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";); + } + + // return true if should keep the clause, and false if we should delete it. + bool solver::activate_frozen_clause(clause & c) { + TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";); + SASSERT(at_base_lvl()); + // do some cleanup + unsigned sz = c.size(); + unsigned j = 0; + for (unsigned i = 0; i < sz; i++) { + literal l = c[i]; + switch (value(l)) { + case l_true: + return false; + case l_false: + break; + case l_undef: + if (i != j) { + std::swap(c[i], c[j]); + } + j++; + break; + } + } + TRACE("sat", tout << "after cleanup:\n" << mk_lits_pp(j, c.begin()) << "\n";); + unsigned new_sz = j; + switch (new_sz) { + case 0: + if (m_config.m_drat) m_drat.add(); + set_conflict(); + return false; + case 1: + assign_unit(c[0]); + return false; + case 2: + mk_bin_clause(c[0], c[1], true); + return false; + default: + shrink(c, sz, new_sz); + attach_clause(c); + return true; + } + } + + /** + \brief Compute phase saving measure for the given clause. + */ + unsigned solver::psm(clause const & c) const { + unsigned r = 0; + for (literal l : c) { + if (l.sign() ^ m_phase[l.var()]) { + r++; + } + } + return r; + } + + /** + * Control the size of the reinit-stack. + * by agressively garbage collecting lemmas that are not asserting. + */ + + void solver::gc_reinit_stack(unsigned num_scopes) { + return; + SASSERT (!at_base_lvl()); + unsigned new_lvl = scope_lvl() - num_scopes; + ptr_vector to_gc; + unsigned j = m_scopes[new_lvl].m_clauses_to_reinit_lim; + unsigned sz = m_clauses_to_reinit.size(); + if (sz - j <= 2000) + return; + for (unsigned i = j; i < sz; ++i) { + auto cw = m_clauses_to_reinit[i]; + if (cw.is_binary() || is_asserting(new_lvl, cw)) + m_clauses_to_reinit[j++] = cw; + else + to_gc.push_back(cw.get_clause()); + } + m_clauses_to_reinit.shrink(j); + if (to_gc.empty()) + return; + for (clause* c : to_gc) { + SASSERT(c->on_reinit_stack()); + c->set_removed(true); + c->set_reinit_stack(false); + } + j = 0; + for (unsigned i = 0; i < m_learned.size(); ++i) { + clause & c = *(m_learned[i]); + if (c.was_removed()) { + detach_clause(c); + del_clause(c); + } + else + m_learned[j++] = &c; + } + std::cout << "gc: " << to_gc.size() << " " << m_learned.size() << " -> " << j << "\n"; + SASSERT(m_learned.size() - j == to_gc.size()); + m_learned.shrink(j); + } + + bool solver::is_asserting(unsigned new_lvl, clause_wrapper const& cw) const { + if (!cw.is_learned()) + return true; + bool seen_true = false; + for (literal lit : cw) { + switch (value(lit)) { + case l_true: + if (lvl(lit) > new_lvl || seen_true) + return false; + seen_true = true; + continue; + case l_false: + continue; + case l_undef: + return false; + } + } + return true; + } + +#if 0 + void solver::gc_reinit_stack(unsigned num_scopes) { + SASSERT (!at_base_lvl()); + collect_clauses_to_gc(num_scopes); + for (literal lit : m_watch_literals_to_gc) { + mark_members_of_watch_list(lit); + shrink_watch_list(lit); + } + unsigned j = 0; + for (clause* c : m_learned) + if (!c->was_removed()) + m_learned[j++] = c; + m_learned.shrink(j); + for (clause* c : m_clauses_to_gc) + del_clause(*c); + m_clauses_to_gc.reset(); + } + + void solver::add_to_gc(literal lit, clause_wrapper const& cw) { + m_literal2gc_clause.reserve(lit.index()+1); + m_literal2gc_clause[lit.index()].push_back(cw); + if (!is_visited(lit)) { + mark_visited(lit); + m_watch_literals_to_gc.push_back(lit); + } + } + + void solver::add_to_gc(clause_wrapper const& cw) { + std::cout << "add-to-gc " << cw << "\n"; + if (cw.is_binary()) { + add_to_gc(cw[0], cw); + add_to_gc(cw[1], clause_wrapper(cw[1], cw[0])); + } + else if (ENABLE_TERNARY && cw.is_ternary()) { + SASSERT(cw.is_learned()); + add_to_gc(cw[0], cw); + add_to_gc(cw[1], cw); + add_to_gc(cw[2], cw); + cw.get_clause()->set_removed(true); + } + else { + SASSERT(cw.is_learned()); + add_to_gc(cw[0], cw); + add_to_gc(cw[1], cw); + cw.get_clause()->set_removed(true); + } + } + + void solver::insert_ternary_to_delete(literal lit, clause_wrapper const& cw) { + SASSERT(cw.is_ternary()); + SASSERT(lit == cw[0] || lit == cw[1] || lit == cw[2]); + literal lit1, lit2; + if (cw[0] == lit) + lit1 = cw[1], lit2 = cw[2]; + else if (cw[1] == lit) + lit1 = cw[0], lit2 = cw[2]; + else + lit1 = cw[0], lit2 = cw[1]; + insert_ternary_to_delete(lit1, lit2, true); + } + + void solver::insert_ternary_to_delete(literal lit1, literal lit2, bool should_delete) { + if (lit1.index() > lit2.index()) + std::swap(lit1, lit2); + m_ternary_to_delete.push_back(std::tuple(lit1, lit2, should_delete)); + } + + bool solver::in_ternary_to_delete(literal lit1, literal lit2) { + if (lit1.index() > lit2.index()) + std::swap(lit1, lit2); + bool found = m_ternary_to_delete.contains(std::make_pair(lit1, lit2)); + if (found) std::cout << lit1 << " " << lit2 << "\n"; + return found; + } + + + void solver::collect_clauses_to_gc(unsigned num_scopes) { + unsigned new_lvl = scope_lvl() - num_scopes; + init_visited(); + m_watch_literals_to_gc.reset(); + unsigned j = m_scopes[new_lvl].m_clauses_to_reinit_lim; + for (unsigned i = j, sz = m_clauses_to_reinit.size(); i < sz; ++i) { + auto cw = m_clauses_to_reinit[i]; + if (is_asserting(new_lvl, cw)) + m_clauses_to_reinit[j++] = cw; + else + add_to_gc(cw); + } + m_clauses_to_reinit.shrink(j); + SASSERT(m_clauses_to_reinit.size() >= j); + } + + void solver::mark_members_of_watch_list(literal lit) { + init_visited(); + m_ternary_to_delete.reset(); + for (auto const& cw : m_literal2gc_clause[lit.index()]) { + SASSERT(!cw.is_binary() || lit == cw[0]); + SASSERT(cw.is_binary() || cw.was_removed()); + if (cw.is_binary()) + mark_visited(cw[1]); + else if (ENABLE_TERNARY && cw.is_ternary()) + insert_ternary_to_delete(lit, cw); + } + } + + void solver::shrink_watch_list(literal lit) { + auto& wl = get_wlist((~lit).index()); + unsigned j = 0, sz = wl.size(), end = sz; + for (unsigned i = 0; i < end; ++i) { + auto w = wl[i]; + if (w.is_binary_clause() && !is_visited(w.get_literal())) + wl[j++] = w; + else if (ENABLE_TERNARY && w.is_ternary_clause()) + insert_ternary_to_delete(w.literal1(), w.literal2(), false); + else if (w.is_clause() && !get_clause(w).was_removed()) + wl[j++] = w; + else if (w.is_ext_constraint()) + wl[j++] = w; + } +#if 0 + std::sort(m_ternary_to_delete.begin(), m_ternary_to_delete.end()); + int prev = -1; + unsigned k = 0; + std::tuple p = tuple(null_literal, null_literal, false); + for (unsigned i = 0; i < m_ternary_to_delete.size(); ++i) { + auto const& t = m_ternary_to_delete[i]; + } +#endif + std::cout << "gc-watch-list " << lit << " " << wl.size() << " -> " << j << "\n"; + wl.shrink(j); + m_literal2gc_clause[lit.index()].reset(); + } + + +#endif + +} diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index 266da96e9a3..3453884a489 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -202,6 +202,7 @@ namespace sat { bool integrity_checker::check_reinit_stack() const { for (auto const& c : s.m_clauses_to_reinit) { + SASSERT(c.is_binary() || c.get_clause()->on_reinit_stack()); VERIFY(c.is_binary() || c.get_clause()->on_reinit_stack()); } return true; diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index a485b2a1c45..2ca17e344da 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -167,9 +167,11 @@ namespace sat { return; if (m_probing_binary) { - watch_list & wlist = s.get_wlist(~l); - for (unsigned i = 0; i < wlist.size(); ++i) { + unsigned sz = s.get_wlist(~l).size(); + for (unsigned i = 0; i < sz; ++i) { + watch_list& wlist = s.get_wlist(~l); watched & w = wlist[i]; + sz = wlist.size(); if (!w.is_binary_clause()) continue; literal l2 = w.get_literal(); @@ -177,7 +179,8 @@ namespace sat { continue; if (s.value(l2) != l_undef) continue; - // Note: that try_lit calls propagate, which may update the watch lists. + // Note: that try_lit calls propagate, which may update the watch lists + // and potentially change the set of variables. if (!try_lit(l2, false)) return; if (s.inconsistent()) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 36792ef38cc..daa4b3e5aa7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -38,7 +38,6 @@ Revision History: #endif #define ENABLE_TERNARY true -#define DYNAMIC_VARS true namespace sat { @@ -123,6 +122,7 @@ namespace sat { m_decision.reset(); m_eliminated.reset(); m_external.reset(); + m_var_scope.reset(); m_activity.reset(); m_mark.reset(); m_lit_mark.reset(); @@ -253,6 +253,7 @@ namespace sat { m_decision[v] = dvar; m_eliminated[v] = false; m_external[v] = ext; + m_var_scope[v] = scope_lvl(); m_touched[v] = 0; m_activity[v] = 0; m_mark[v] = false; @@ -291,6 +292,7 @@ namespace sat { m_decision.push_back(dvar); m_eliminated.push_back(false); m_external.push_back(ext); + m_var_scope.push_back(scope_lvl()); m_touched.push_back(0); m_activity.push_back(0); m_mark.push_back(false); @@ -439,12 +441,13 @@ namespace sat { return nullptr; case 2: mk_bin_clause(lits[0], lits[1], st); - if (redundant && m_par) m_par->share_clause(*this, lits[0], lits[1]); + if (redundant && m_par) + m_par->share_clause(*this, lits[0], lits[1]); return nullptr; case 3: - if (ENABLE_TERNARY) { + if (ENABLE_TERNARY) return mk_ter_clause(lits, st); - } + Z3_fallthrough; default: return mk_nary_clause(num_lits, lits, st); } @@ -472,9 +475,10 @@ namespace sat { VERIFY(w0); w0->set_learned(false); } - if (propagate_bin_clause(l1, l2) && !redundant && !at_base_lvl() && !at_search_lvl()) { - m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); - } + if (propagate_bin_clause(l1, l2) && !at_base_lvl() && !redundant) + push_reinit_stack(l1, l2); + else if (has_variables_to_reinit(l1, l2)) + push_reinit_stack(l1, l2); return; } if (m_config.m_drat) @@ -482,14 +486,32 @@ namespace sat { if (propagate_bin_clause(l1, l2)) { if (at_base_lvl()) return; - if (!redundant && !at_search_lvl()) - m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); + push_reinit_stack(l1, l2); } + else if (has_variables_to_reinit(l1, l2)) + push_reinit_stack(l1, l2); m_stats.m_mk_bin_clause++; get_wlist(~l1).push_back(watched(l2, redundant)); get_wlist(~l2).push_back(watched(l1, redundant)); } + bool solver::has_variables_to_reinit(clause const& c) const { + for (auto lit : c) + if (m_var_scope[lit.var()] > 0) + return true; + return false; + } + + bool solver::has_variables_to_reinit(literal l1, literal l2) const { + if (at_base_lvl()) + return false; + if (m_var_scope[l1.var()] > 0) + return true; + if (m_var_scope[l2.var()] > 0) + return true; + return false; + } + bool solver::propagate_bin_clause(literal l1, literal l2) { if (value(l2) == l_false) { m_stats.m_bin_propagate++; @@ -505,18 +527,23 @@ namespace sat { } void solver::push_reinit_stack(clause & c) { + SASSERT(!at_base_lvl()); TRACE("sat_reinit", tout << "adding to reinit stack: " << c << "\n";); m_clauses_to_reinit.push_back(clause_wrapper(c)); c.set_reinit_stack(true); } + void solver::push_reinit_stack(literal l1, literal l2) { + TRACE("sat_reinit", tout << "adding to reinit stack: " << l1 << " " << l2 << "\n";); + m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); + } clause * solver::mk_ter_clause(literal * lits, sat::status st) { VERIFY(ENABLE_TERNARY); m_stats.m_mk_ter_clause++; clause * r = alloc_clause(3, lits, st.is_redundant()); bool reinit = attach_ter_clause(*r, st); - if (reinit && !st.is_redundant()) push_reinit_stack(*r); + if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r); if (st.is_redundant()) m_learned.push_back(r); else @@ -540,17 +567,17 @@ namespace sat { if (value(c[1]) == l_false && value(c[2]) == l_false) { m_stats.m_ter_propagate++; assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2])); - reinit = true; + reinit = !c.is_learned(); } else if (value(c[0]) == l_false && value(c[2]) == l_false) { m_stats.m_ter_propagate++; assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2])); - reinit = true; + reinit = !c.is_learned(); } else if (value(c[0]) == l_false && value(c[1]) == l_false) { m_stats.m_ter_propagate++; assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1])); - reinit = true; + reinit = !c.is_learned(); } } return reinit; @@ -561,7 +588,7 @@ namespace sat { clause * r = alloc_clause(num_lits, lits, st.is_redundant()); SASSERT(!st.is_redundant() || r->is_learned()); bool reinit = attach_nary_clause(*r); - if (reinit && !st.is_redundant()) push_reinit_stack(*r); + if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r); if (st.is_redundant()) { m_learned.push_back(r); } @@ -581,7 +608,7 @@ namespace sat { bool reinit = false; clause_offset cls_off = cls_allocator().get_offset(&c); if (!at_base_lvl()) { - if (c.is_learned()) { + if (c.is_learned() && !c.on_reinit_stack()) { unsigned w2_idx = select_learned_watch_lit(c); std::swap(c[1], c[w2_idx]); } @@ -599,7 +626,7 @@ namespace sat { level = std::max(level, lvl(c[i])); } assign(c[1], justification(level, cls_off)); - reinit = true; + reinit = !c.is_learned(); } else if (value(c[1]) == l_false) { m_stats.m_propagate++; @@ -608,7 +635,7 @@ namespace sat { level = std::max(level, lvl(c[i])); } assign(c[0], justification(level, cls_off)); - reinit = true; + reinit = !c.is_learned(); } } unsigned some_idx = c.size() >> 1; @@ -990,204 +1017,208 @@ namespace sat { // ----------------------- bool solver::propagate_core(bool update) { + while (m_qhead < m_trail.size() && !m_inconsistent) { + do { + checkpoint(); + m_cleaner.dec(); + literal l = m_trail[m_qhead]; + m_qhead++; + if (!propagate_literal(l, update)) + return false; + } while (m_qhead < m_trail.size()); + + if (m_ext) + m_ext->unit_propagate(); + } if (m_inconsistent) return false; - literal l, not_l, l1, l2; + + SASSERT(m_qhead == m_trail.size()); + SASSERT(!m_inconsistent); + return true; + } + + bool solver::propagate(bool update) { + unsigned qhead = m_qhead; + bool r = propagate_core(update); + if (m_config.m_branching_heuristic == BH_CHB) { + update_chb_activity(r, qhead); + } + CASSERT("sat_propagate", check_invariant()); + CASSERT("sat_missed_prop", check_missed_propagation()); + return r; + } + + bool solver::propagate_literal(literal l, bool update) { + literal l1, l2; lbool val1, val2; bool keep; - prop_again: - while (m_qhead < m_trail.size()) { - checkpoint(); - m_cleaner.dec(); - if (m_inconsistent) return false; - l = m_trail[m_qhead]; - unsigned curr_level = lvl(l); - TRACE("sat_propagate", tout << "propagating: " << l << " " << m_justification[l.var()] << "\n"; ); - m_qhead++; - not_l = ~l; - SASSERT(value(l) == l_true); - SASSERT(value(not_l) == l_false); - watch_list & wlist = m_watches[l.index()]; - m_asymm_branch.dec(wlist.size()); - m_probing.dec(wlist.size()); - watch_list::iterator it = wlist.begin(); - watch_list::iterator it2 = it; - watch_list::iterator end = wlist.end(); + unsigned curr_level = lvl(l); + TRACE("sat_propagate", tout << "propagating: " << l << " " << m_justification[l.var()] << "\n"; ); + + literal not_l = ~l; + SASSERT(value(l) == l_true); + SASSERT(value(not_l) == l_false); + watch_list& wlist = m_watches[l.index()]; + m_asymm_branch.dec(wlist.size()); + m_probing.dec(wlist.size()); + watch_list::iterator it = wlist.begin(); + watch_list::iterator it2 = it; + watch_list::iterator end = wlist.end(); #define CONFLICT_CLEANUP() { \ for (; it != end; ++it, ++it2) \ *it2 = *it; \ wlist.set_end(it2); \ } - for (; it != end; ++it) { - switch (it->get_kind()) { - case watched::BINARY: - l1 = it->get_literal(); - switch (value(l1)) { - case l_false: - CONFLICT_CLEANUP(); - set_conflict(justification(curr_level, not_l), ~l1); - return false; - case l_undef: - m_stats.m_bin_propagate++; - assign_core(l1, justification(curr_level, not_l)); - break; - case l_true: - break; // skip - } + for (; it != end; ++it) { + switch (it->get_kind()) { + case watched::BINARY: + l1 = it->get_literal(); + switch (value(l1)) { + case l_false: + CONFLICT_CLEANUP(); + set_conflict(justification(curr_level, not_l), ~l1); + return false; + case l_undef: + m_stats.m_bin_propagate++; + assign_core(l1, justification(curr_level, not_l)); + break; + case l_true: + break; // skip + } + *it2 = *it; + it2++; + break; + case watched::TERNARY: + l1 = it->get_literal1(); + l2 = it->get_literal2(); + val1 = value(l1); + val2 = value(l2); + if (val1 == l_false && val2 == l_undef) { + m_stats.m_ter_propagate++; + assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l)); + } + else if (val1 == l_undef && val2 == l_false) { + m_stats.m_ter_propagate++; + assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l)); + } + else if (val1 == l_false && val2 == l_false) { + CONFLICT_CLEANUP(); + set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2); + return false; + } + *it2 = *it; + it2++; + break; + case watched::CLAUSE: { + if (value(it->get_blocked_literal()) == l_true) { + TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n"; + tout << get_clause(it) << "\n";); *it2 = *it; it2++; break; - case watched::TERNARY: - l1 = it->get_literal1(); - l2 = it->get_literal2(); - val1 = value(l1); - val2 = value(l2); - if (val1 == l_false && val2 == l_undef) { - m_stats.m_ter_propagate++; - assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l)); - } - else if (val1 == l_undef && val2 == l_false) { - m_stats.m_ter_propagate++; - assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l)); - } - else if (val1 == l_false && val2 == l_false) { - CONFLICT_CLEANUP(); - set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2); - return false; - } + } + clause_offset cls_off = it->get_clause_offset(); + clause& c = get_clause(cls_off); + TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";); + if (c[0] == not_l) + std::swap(c[0], c[1]); + CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); + if (c.was_removed() || c.size() == 1 || c[1] != not_l) { + // Remark: this method may be invoked when the watch lists are not in a consistent state, + // and may contain dead/removed clauses, or clauses with removed literals. + // See: method propagate_unit at sat_simplifier.cpp + // So, we must check whether the clause was marked for deletion, or + // c[1] != not_l *it2 = *it; it2++; break; - case watched::CLAUSE: { - if (value(it->get_blocked_literal()) == l_true) { - TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n"; - tout << get_clause(it) << "\n";); - *it2 = *it; - it2++; - break; - } - clause_offset cls_off = it->get_clause_offset(); - clause & c = get_clause(cls_off); - TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";); - if (c[0] == not_l) - std::swap(c[0], c[1]); - CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";); - if (c.was_removed() || c.size() == 1 || c[1] != not_l) { - // Remark: this method may be invoked when the watch lists are not in a consistent state, - // and may contain dead/removed clauses, or clauses with removed literals. - // See: method propagate_unit at sat_simplifier.cpp - // So, we must check whether the clause was marked for deletion, or - // c[1] != not_l - *it2 = *it; - it2++; - break; - } - if (value(c[0]) == l_true) { - it2->set_clause(c[0], cls_off); - it2++; - break; - } - VERIFY(c[1] == not_l); - literal * l_it = c.begin() + 2; - literal * l_end = c.end(); - unsigned assign_level = curr_level; - unsigned max_index = 1; - for (; l_it != l_end; ++l_it) { - if (value(*l_it) != l_false) { - c[1] = *l_it; - *l_it = not_l; - DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off);); - m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off)); - goto end_clause_case; - } + } + if (value(c[0]) == l_true) { + it2->set_clause(c[0], cls_off); + it2++; + break; + } + VERIFY(c[1] == not_l); + literal* l_it = c.begin() + 2; + literal* l_end = c.end(); + unsigned assign_level = curr_level; + unsigned max_index = 1; + for (; l_it != l_end; ++l_it) { + if (value(*l_it) != l_false) { + c[1] = *l_it; + *l_it = not_l; + DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off);); + m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off)); + goto end_clause_case; } - SASSERT(value(c[0]) == l_false || value(c[0]) == l_undef); - if (assign_level != scope_lvl()) { - for (unsigned i = 2; i < c.size(); ++i) { - unsigned level = lvl(c[i]); - if (level > assign_level) { - assign_level = level; - max_index = i; - } + } + SASSERT(value(c[0]) == l_false || value(c[0]) == l_undef); + if (assign_level != scope_lvl()) { + for (unsigned i = 2; i < c.size(); ++i) { + unsigned level = lvl(c[i]); + if (level > assign_level) { + assign_level = level; + max_index = i; } - IF_VERBOSE(20, verbose_stream() << "lower assignment level " << assign_level << " scope: " << scope_lvl() << "\n"); } + IF_VERBOSE(20, verbose_stream() << "lower assignment level " << assign_level << " scope: " << scope_lvl() << "\n"); + } - if (value(c[0]) == l_false) { - assign_level = std::max(assign_level, lvl(c[0])); - c.mark_used(); - CONFLICT_CLEANUP(); - set_conflict(justification(assign_level, cls_off)); - return false; + if (value(c[0]) == l_false) { + assign_level = std::max(assign_level, lvl(c[0])); + c.mark_used(); + CONFLICT_CLEANUP(); + set_conflict(justification(assign_level, cls_off)); + return false; + } + else { + if (max_index != 1) { + IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n"); + std::swap(c[1], c[max_index]); + m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off)); } else { - if (max_index != 1) { - IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n"); - std::swap(c[1], c[max_index]); - m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off)); - } - else { - *it2 = *it; - it2++; - } - m_stats.m_propagate++; - c.mark_used(); - assign_core(c[0], justification(assign_level, cls_off)); - if (update && c.is_learned() && c.glue() > 2) { - unsigned glue; - if (num_diff_levels_below(c.size(), c.begin(), c.glue()-1, glue)) { - c.set_glue(glue); - } - } + *it2 = *it; + it2++; } - end_clause_case: - break; - } - case watched::EXT_CONSTRAINT: - SASSERT(m_ext); - keep = m_ext->propagate(l, it->get_ext_constraint_idx()); - if (m_inconsistent) { - if (!keep) { - ++it; + m_stats.m_propagate++; + c.mark_used(); + assign_core(c[0], justification(assign_level, cls_off)); + if (update && c.is_learned() && c.glue() > 2) { + unsigned glue; + if (num_diff_levels_below(c.size(), c.begin(), c.glue() - 1, glue)) { + c.set_glue(glue); } - CONFLICT_CLEANUP(); - return false; } - if (keep) { - *it2 = *it; - it2++; + } + end_clause_case: + break; + } + case watched::EXT_CONSTRAINT: + SASSERT(m_ext); + keep = m_ext->propagate(l, it->get_ext_constraint_idx()); + if (m_inconsistent) { + if (!keep) { + ++it; } - break; - default: - UNREACHABLE(); - break; + CONFLICT_CLEANUP(); + return false; + } + if (keep) { + *it2 = *it; + it2++; } + break; + default: + UNREACHABLE(); + break; } - wlist.set_end(it2); } - if (m_ext) { - m_ext->unit_propagate(); - if (inconsistent()) - return false; - if (m_qhead < m_trail.size()) - goto prop_again; - } - SASSERT(m_qhead == m_trail.size()); - SASSERT(!m_inconsistent); + wlist.set_end(it2); return true; } - bool solver::propagate(bool update) { - unsigned qhead = m_qhead; - bool r = propagate_core(update); - if (m_config.m_branching_heuristic == BH_CHB) { - update_chb_activity(r, qhead); - } - CASSERT("sat_propagate", check_invariant()); - CASSERT("sat_missed_prop", check_missed_propagation()); - return r; - } - void solver::display_lookahead_scores(std::ostream& out) { lookahead lh(*this); lh.display_lookahead_scores(out); @@ -2284,340 +2315,6 @@ namespace sat { CASSERT("sat_restart", check_invariant()); } - // ----------------------- - // - // GC - // - // ----------------------- - - bool solver::should_gc() const { - return - m_conflicts_since_gc > m_gc_threshold && - (m_config.m_gc_strategy != GC_DYN_PSM || at_base_lvl()); - } - - void solver::do_gc() { - if (!should_gc()) return; - TRACE("sat", tout << m_conflicts_since_gc << " " << m_gc_threshold << "\n";); - unsigned gc = m_stats.m_gc_clause; - m_conflicts_since_gc = 0; - m_gc_threshold += m_config.m_gc_increment; - IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";); - CASSERT("sat_gc_bug", check_invariant()); - switch (m_config.m_gc_strategy) { - case GC_GLUE: - gc_glue(); - break; - case GC_PSM: - gc_psm(); - break; - case GC_GLUE_PSM: - gc_glue_psm(); - break; - case GC_PSM_GLUE: - gc_psm_glue(); - break; - case GC_DYN_PSM: - if (!m_assumptions.empty()) { - gc_glue_psm(); - break; - } - if (!at_base_lvl()) - return; - gc_dyn_psm(); - break; - default: - UNREACHABLE(); - break; - } - if (m_ext) m_ext->gc(); - if (gc > 0 && should_defrag()) { - defrag_clauses(); - } - CASSERT("sat_gc_bug", check_invariant()); - } - - /** - \brief Lex on (glue, size) - */ - struct glue_lt { - bool operator()(clause const * c1, clause const * c2) const { - if (c1->glue() < c2->glue()) return true; - return c1->glue() == c2->glue() && c1->size() < c2->size(); - } - }; - - /** - \brief Lex on (psm, size) - */ - struct psm_lt { - bool operator()(clause const * c1, clause const * c2) const { - if (c1->psm() < c2->psm()) return true; - return c1->psm() == c2->psm() && c1->size() < c2->size(); - } - }; - - /** - \brief Lex on (glue, psm, size) - */ - struct glue_psm_lt { - bool operator()(clause const * c1, clause const * c2) const { - if (c1->glue() < c2->glue()) return true; - if (c1->glue() > c2->glue()) return false; - if (c1->psm() < c2->psm()) return true; - if (c1->psm() > c2->psm()) return false; - return c1->size() < c2->size(); - } - }; - - /** - \brief Lex on (psm, glue, size) - */ - struct psm_glue_lt { - bool operator()(clause const * c1, clause const * c2) const { - if (c1->psm() < c2->psm()) return true; - if (c1->psm() > c2->psm()) return false; - if (c1->glue() < c2->glue()) return true; - if (c1->glue() > c2->glue()) return false; - return c1->size() < c2->size(); - } - }; - - void solver::gc_glue() { - std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt()); - gc_half("glue"); - } - - void solver::gc_psm() { - save_psm(); - std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt()); - gc_half("psm"); - } - - void solver::gc_glue_psm() { - save_psm(); - std::stable_sort(m_learned.begin(), m_learned.end(), glue_psm_lt()); - gc_half("glue-psm"); - } - - void solver::gc_psm_glue() { - save_psm(); - std::stable_sort(m_learned.begin(), m_learned.end(), psm_glue_lt()); - gc_half("psm-glue"); - } - - /** - \brief Compute the psm of all learned clauses. - */ - void solver::save_psm() { - for (clause* cp : m_learned) { - cp->set_psm(psm(*cp)); - } - } - - /** - \brief GC (the second) half of the clauses in the database. - */ - void solver::gc_half(char const * st_name) { - TRACE("sat", tout << "gc\n";); - unsigned sz = m_learned.size(); - unsigned new_sz = sz/2; // std::min(sz/2, m_clauses.size()*2); - unsigned j = new_sz; - for (unsigned i = new_sz; i < sz; i++) { - clause & c = *(m_learned[i]); - if (can_delete(c)) { - detach_clause(c); - del_clause(c); - } - else { - m_learned[j] = &c; - j++; - } - } - new_sz = j; - m_stats.m_gc_clause += sz - new_sz; - m_learned.shrink(new_sz); - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";); - } - - bool solver::can_delete3(literal l1, literal l2, literal l3) const { - if (value(l1) == l_true && - value(l2) == l_false && - value(l3) == l_false) { - justification const& j = m_justification[l1.var()]; - if (j.is_ternary_clause()) { - watched w1(l2, l3); - watched w2(j.get_literal1(), j.get_literal2()); - return w1 != w2; - } - } - return true; - } - - bool solver::can_delete(clause const & c) const { - if (c.on_reinit_stack()) - return false; - if (ENABLE_TERNARY && c.size() == 3) { - return - can_delete3(c[0],c[1],c[2]) && - can_delete3(c[1],c[0],c[2]) && - can_delete3(c[2],c[0],c[1]); - } - literal l0 = c[0]; - if (value(l0) != l_true) - return true; - justification const & jst = m_justification[l0.var()]; - return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c; - } - - /** - \brief Use gc based on dynamic psm. Clauses are initially frozen. - */ - void solver::gc_dyn_psm() { - TRACE("sat", tout << "gc\n";); - // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact - // that I may miss some propagations for reactivated clauses. - SASSERT(at_base_lvl()); - // compute - // d_tk - unsigned h = 0; - unsigned V_tk = 0; - for (bool_var v = 0; v < num_vars(); v++) { - if (m_assigned_since_gc[v]) { - V_tk++; - m_assigned_since_gc[v] = false; - } - if (m_phase[v] != m_prev_phase[v]) { - h++; - m_prev_phase[v] = m_phase[v]; - } - } - double d_tk = V_tk == 0 ? static_cast(num_vars() + 1) : static_cast(h)/static_cast(V_tk); - if (d_tk < m_min_d_tk) - m_min_d_tk = d_tk; - TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";); - unsigned frozen = 0; - unsigned deleted = 0; - unsigned activated = 0; - clause_vector::iterator it = m_learned.begin(); - clause_vector::iterator it2 = it; - clause_vector::iterator end = m_learned.end(); - for (; it != end; ++it) { - clause & c = *(*it); - if (!c.frozen()) { - // Active clause - if (c.glue() > m_config.m_gc_small_lbd) { - // I never delete clauses with small lbd - if (c.was_used()) { - c.reset_inact_rounds(); - } - else { - c.inc_inact_rounds(); - if (c.inact_rounds() > m_config.m_gc_k) { - detach_clause(c); - del_clause(c); - m_stats.m_gc_clause++; - deleted++; - continue; - } - } - c.unmark_used(); - if (psm(c) > static_cast(c.size() * m_min_d_tk)) { - // move to frozen; - TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";); - detach_clause(c); - c.reset_inact_rounds(); - c.freeze(); - m_num_frozen++; - frozen++; - } - } - } - else { - // frozen clause - clause & c = *(*it); - if (psm(c) <= static_cast(c.size() * m_min_d_tk)) { - c.unfreeze(); - m_num_frozen--; - activated++; - if (!activate_frozen_clause(c)) { - // clause was satisfied, reduced to a conflict, unit or binary clause. - del_clause(c); - continue; - } - } - else { - c.inc_inact_rounds(); - if (c.inact_rounds() > m_config.m_gc_k) { - del_clause(c); - m_stats.m_gc_clause++; - deleted++; - continue; - } - } - } - *it2 = *it; - ++it2; - } - m_learned.set_end(it2); - IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk << - " :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";); - } - - // return true if should keep the clause, and false if we should delete it. - bool solver::activate_frozen_clause(clause & c) { - TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";); - SASSERT(at_base_lvl()); - // do some cleanup - unsigned sz = c.size(); - unsigned j = 0; - for (unsigned i = 0; i < sz; i++) { - literal l = c[i]; - switch (value(l)) { - case l_true: - return false; - case l_false: - break; - case l_undef: - if (i != j) { - std::swap(c[i], c[j]); - } - j++; - break; - } - } - TRACE("sat", tout << "after cleanup:\n" << mk_lits_pp(j, c.begin()) << "\n";); - unsigned new_sz = j; - switch (new_sz) { - case 0: - if (m_config.m_drat) m_drat.add(); - set_conflict(); - return false; - case 1: - assign_unit(c[0]); - return false; - case 2: - mk_bin_clause(c[0], c[1], true); - return false; - default: - shrink(c, sz, new_sz); - attach_clause(c); - return true; - } - } - - /** - \brief Compute phase saving measure for the given clause. - */ - unsigned solver::psm(clause const & c) const { - unsigned r = 0; - for (literal l : c) { - if (l.sign() ^ m_phase[l.var()]) { - r++; - } - } - return r; - } // ----------------------- // @@ -2639,6 +2336,7 @@ namespace sat { lbool solver::resolve_conflict_core() { + TRACE("sat", tout << "**************************\n";); m_conflicts_since_init++; m_conflicts_since_restart++; m_conflicts_since_gc++; @@ -2776,6 +2474,10 @@ namespace sat { } SASSERT(lvl(c_var) < m_conflict_lvl); } + if (idx == 0) + for (literal lit : m_trail) + if (is_marked(lit.var())) + TRACE("sat", tout << "missed " << lit << "@" << lvl(lit) << "\n";); SASSERT(idx > 0); idx--; } @@ -3728,9 +3430,7 @@ namespace sat { s.m_clauses_to_reinit_lim = m_clauses_to_reinit.size(); s.m_inconsistent = m_inconsistent; if (m_ext) { -#if DYNAMIC_VARS m_vars_lim.push(m_active_vars.size()); -#endif m_ext->push(); } } @@ -3743,30 +3443,40 @@ namespace sat { } void solver::pop_vars(unsigned num_scopes) { + integrity_checker check(*this); + check.check_reinit_stack(); m_vars_to_reinit.reset(); unsigned old_num_vars = m_vars_lim.pop(num_scopes); if (old_num_vars == m_active_vars.size()) return; + unsigned free_vars_head = m_free_vars.size(); + unsigned sz = m_active_vars.size(), j = old_num_vars; + unsigned new_lvl = m_scopes.size() - num_scopes; + + gc_reinit_stack(num_scopes); + + check.check_reinit_stack(); init_visited(); - unsigned new_lvl = scope_lvl() - num_scopes; unsigned old_sz = m_scopes[new_lvl].m_clauses_to_reinit_lim; for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) { clause_wrapper const& cw = m_clauses_to_reinit[i]; for (unsigned j = cw.size(); j-- > 0; ) - mark_visited(cw[j]); + mark_visited(cw[j].var()); } for (literal lit : m_lemma) - mark_visited(lit); + mark_visited(lit.var()); + auto is_active = [&](bool_var v) { return value(v) != l_undef && lvl(v) <= new_lvl; }; + - unsigned sz = m_active_vars.size(), j = old_num_vars; for (unsigned i = old_num_vars; i < sz; ++i) { bool_var v = m_active_vars[i]; if (is_visited(v) || is_active(v)) { m_vars_to_reinit.push_back(v); m_active_vars[j++] = v; + m_var_scope[v] = new_lvl; } else { set_eliminated(v, true); @@ -3774,9 +3484,25 @@ namespace sat { } } m_active_vars.shrink(j); - IF_VERBOSE(11, verbose_stream() << "vars to reinit: " << m_vars_to_reinit << " free vars " << m_free_vars << "\n"; - display(verbose_stream());); - + + auto cleanup_watch = [&](literal lit) { + for (auto const& w : get_wlist(lit)) { + std::cout << "cleanup: " << lit << " " << w.is_binary_clause() << "\n"; + } + }; + for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) { + bool_var v = m_free_vars[i]; + cleanup_watch(literal(v, false)); + cleanup_watch(literal(v, true)); + } + TRACE("sat", + tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n"; + tout << "new level: " << new_lvl << "\n"; + tout << "vars to reinit: " << m_vars_to_reinit << "\n"; + tout << "free vars: " << bool_var_vector(m_free_vars.size() - free_vars_head, m_free_vars.c_ptr() + free_vars_head) << "\n"; + for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) + tout << "reinit: " << m_clauses_to_reinit[i] << "\n"; + display(tout);); } void solver::shrink_vars(unsigned v) { @@ -3791,6 +3517,7 @@ namespace sat { m_decision.shrink(v); m_eliminated.shrink(v); m_external.shrink(v); + m_var_scope.shrink(v); m_touched.shrink(v); m_activity.shrink(v); m_mark.shrink(v); @@ -3806,9 +3533,7 @@ namespace sat { if (num_scopes == 0) return; if (m_ext) { -#if DYNAMIC_VARS pop_vars(num_scopes); -#endif m_ext->pop(num_scopes); } SASSERT(num_scopes <= scope_lvl()); @@ -3817,8 +3542,8 @@ namespace sat { m_inconsistent = false; // TBD: use model seems to make this redundant: s.m_inconsistent; unassign_vars(s.m_trail_lim, new_lvl); m_scope_lvl -= num_scopes; - m_scopes.shrink(new_lvl); reinit_clauses(s.m_clauses_to_reinit_lim); + m_scopes.shrink(new_lvl); if (m_ext) m_ext->pop_reinit(); } @@ -3864,25 +3589,22 @@ namespace sat { clause_wrapper cw = m_clauses_to_reinit[i]; bool reinit = false; if (cw.is_binary()) { - if (propagate_bin_clause(cw[0], cw[1])) { - if (!at_base_lvl()) { - m_clauses_to_reinit[j] = cw; - j++; - } - } + if (propagate_bin_clause(cw[0], cw[1]) && !at_base_lvl()) + m_clauses_to_reinit[j++] = cw; + else if (has_variables_to_reinit(cw[0], cw[1])) + m_clauses_to_reinit[j++] = cw; } else { clause & c = *(cw.get_clause()); detach_clause(c); attach_clause(c, reinit); - if (!at_base_lvl() && reinit) { + if (!at_base_lvl() && reinit) // clause propagated literal, must keep it in the reinit stack. - m_clauses_to_reinit[j] = cw; - j++; - } - else { - c.set_reinit_stack(false); - } + m_clauses_to_reinit[j++] = cw; + else if (has_variables_to_reinit(c)) + m_clauses_to_reinit[j++] = cw; + else + c.set_reinit_stack(false); } } m_clauses_to_reinit.shrink(j); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index b9bf807cde3..00ade9465f6 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -124,6 +124,7 @@ namespace sat { bool_vector m_lit_mark; bool_vector m_eliminated; bool_vector m_external; + unsigned_vector m_var_scope; unsigned_vector m_touched; unsigned m_touch_index; literal_vector m_replay_assign; @@ -286,6 +287,8 @@ namespace sat { clause * mk_ter_clause(literal * lits, status st); bool attach_ter_clause(clause & c, status st); clause * mk_nary_clause(unsigned num_lits, literal * lits, status st); + bool has_variables_to_reinit(clause const& c) const; + bool has_variables_to_reinit(literal l1, literal l2) const; bool attach_nary_clause(clause & c); void attach_clause(clause & c, bool & reinit); void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); } @@ -320,6 +323,7 @@ namespace sat { void detach_nary_clause(clause & c); void detach_ter_clause(clause & c); void push_reinit_stack(clause & c); + void push_reinit_stack(literal l1, literal l2); void init_visited(); void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; } @@ -441,6 +445,7 @@ namespace sat { protected: bool should_propagate() const; bool propagate_core(bool update); + bool propagate_literal(literal l, bool update); // ----------------------- // @@ -546,6 +551,10 @@ namespace sat { bool can_delete(clause const & c) const; bool can_delete3(literal l1, literal l2, literal l3) const; + // gc for lemmas in the reinit-stack + void gc_reinit_stack(unsigned num_scopes); + bool is_asserting(unsigned new_lvl, clause_wrapper const& cw) const; + clause& get_clause(watch_list::iterator it) const { SASSERT(it->get_kind() == watched::CLAUSE); return get_clause(it->get_clause_offset()); diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index f2bbb909c61..bf83c406198 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -84,6 +84,7 @@ namespace array { } sat::check_result solver::check() { + force_push(); // flet _is_redundant(m_is_redundant, true); bool turn[2] = { false, false }; turn[s().rand()(2)] = true; @@ -96,14 +97,8 @@ namespace array { return sat::check_result::CR_DONE; } - void solver::push() { - th_euf_solver::lazy_push(); - } - - void solver::pop(unsigned n) { - n = lazy_pop(n); - if (n == 0) - return; + void solver::pop_core(unsigned n) { + th_euf_solver::pop_core(n); m_var_data.resize(get_num_vars()); } @@ -111,9 +106,9 @@ namespace array { for (unsigned i = 0; i < get_num_vars(); ++i) { auto& d = get_var_data(i); out << var2enode(i)->get_expr_id() << " " << mk_bounded_pp(var2expr(i), m, 2) << "\n"; - display_info(out, "parent beta", d.m_parent_lambdas); + display_info(out, "parent lambdas", d.m_parent_lambdas); display_info(out, "parent select", d.m_parent_selects); - display_info(out, "beta ", d.m_lambdas); + display_info(out, "b ", d.m_lambdas); } return out; } @@ -159,12 +154,14 @@ namespace array { } void solver::new_eq_eh(euf::th_eq const& eq) { - m_find.merge(eq.m_v1, eq.m_v2); + force_push(); + m_find.merge(eq.v1(), eq.v2()); } bool solver::unit_propagate() { if (m_qhead == m_axiom_trail.size()) return false; + force_push(); bool prop = false; ctx.push(value_trail(m_qhead)); for (; m_qhead < m_axiom_trail.size() && !s().inconsistent(); ++m_qhead) diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 184c449910f..d7bd88d9d90 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -175,6 +175,8 @@ namespace array { var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); } var_data& get_var_data(theory_var v) { return *m_var_data[v]; } var_data const& get_var_data(theory_var v) const { return *m_var_data[v]; } + + void pop_core(unsigned n) override; // models bool have_different_model_values(theory_var v1, theory_var v2); @@ -191,8 +193,7 @@ namespace array { void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {} void asserted(literal l) override {} sat::check_result check() override; - void push() override; - void pop(unsigned n) override; + std::ostream& display(std::ostream& out) const override; std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index 62251d7a0b9..1d7ebfe13ee 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -55,6 +55,25 @@ namespace bv { } } + void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) { + if (v1 == v2) + return; + if (v1 > v2) + std::swap(v1, v2); + vv* n = m_tmp_vv; + n->v1 = v1; + n->v2 = v2; + vv* other = m_table.insert_if_not_there(n); + other->m_count++; + if (other->m_count > m_propagate_high_watermark || other->m_glue == 0) + s.s().set_should_simplify(); + vv::push_to_front(m_queue, other); + if (other == n) { + new_tmp(); + gc(); + } + } + void ackerman::update_glue(vv& v) { unsigned sz = s.m_bits[v.v1].size(); m_diff_levels.reserve(s.s().scope_lvl() + 1, false); diff --git a/src/sat/smt/bv_ackerman.h b/src/sat/smt/bv_ackerman.h index abcc5e60b2c..cba6e50addf 100644 --- a/src/sat/smt/bv_ackerman.h +++ b/src/sat/smt/bv_ackerman.h @@ -72,6 +72,8 @@ namespace bv { void used_eq_eh(euf::theory_var v1, euf::theory_var v2); + void used_diseq_eh(euf::theory_var v1, euf::theory_var v2); + void propagate(); }; diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 2686a65f7ee..6a46dbe45d5 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -62,15 +62,17 @@ namespace bv { m_zero_one_bits.push_back(zero_one_bits()); ctx.attach_th_var(n, this, r); - TRACE("bv", tout << "mk-var: " << r << " " << n->get_expr_id() << " " << mk_pp(n->get_expr(), m) << "\n";); + TRACE("bv", tout << "mk-var: " << r << " " << n->get_expr_id() << " " << mk_bounded_pp(n->get_expr(), m) << "\n";); return r; } void solver::apply_sort_cnstr(euf::enode * n, sort * s) { + force_push(); get_var(n); } sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { + force_push(); SASSERT(m.is_bool(e)); if (!visit_rec(m, e, sign, root, redundant)) return sat::null_literal; @@ -81,6 +83,7 @@ namespace bv { } void solver::internalize(expr* e, bool redundant) { + force_push(); visit_rec(m, e, false, false, redundant); } @@ -337,7 +340,7 @@ namespace bv { for (expr* b : k_bits) args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero)); expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m); - expr_ref eq(m.mk_eq(n, sum), m); + expr_ref eq = mk_eq(n, sum); sat::literal lit = ctx.internalize(eq, false, false, m_is_redundant); add_unit(lit); } @@ -367,7 +370,7 @@ namespace bv { unsigned sz = bv.get_bv_size(n); numeral mod = power(numeral(2), sz); rhs = m_autil.mk_mod(e, m_autil.mk_int(mod)); - expr_ref eq(m.mk_eq(lhs, rhs), m); + expr_ref eq = mk_eq(lhs, rhs); TRACE("bv", tout << eq << "\n";); add_unit(ctx.internalize(eq, false, false, m_is_redundant)); @@ -378,9 +381,9 @@ namespace bv { numeral div = power2(i); rhs = m_autil.mk_idiv(e, m_autil.mk_int(div)); rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2)); - rhs = m.mk_eq(rhs, m_autil.mk_int(1)); + rhs = mk_eq(rhs, m_autil.mk_int(1)); lhs = n_bits.get(i); - expr_ref eq(m.mk_eq(lhs, rhs), m); + expr_ref eq = mk_eq(lhs, rhs); TRACE("bv", tout << eq << "\n";); add_unit(ctx.internalize(eq, false, false, m_is_redundant)); } @@ -403,10 +406,10 @@ namespace bv { void solver::internalize_carry(app* n) { SASSERT(n->get_num_args() == 3); - literal r = ctx.get_literal(n); - literal l1 = ctx.get_literal(n->get_arg(0)); - literal l2 = ctx.get_literal(n->get_arg(1)); - literal l3 = ctx.get_literal(n->get_arg(2)); + literal r = expr2literal(n); + literal l1 = expr2literal(n->get_arg(0)); + literal l2 = expr2literal(n->get_arg(1)); + literal l3 = expr2literal(n->get_arg(2)); add_clause(~r, l1, l2); add_clause(~r, l1, l3); add_clause(~r, l2, l3); @@ -417,7 +420,7 @@ namespace bv { void solver::internalize_xor3(app* n) { SASSERT(n->get_num_args() == 3); - literal r = ctx.get_literal(n); + literal r = expr2literal(n); literal l1 = expr2literal(n->get_arg(0)); literal l2 = expr2literal(n->get_arg(1)); literal l3 = expr2literal(n->get_arg(2)); @@ -483,7 +486,7 @@ namespace bv { expr_ref out(m); fn(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), out); sat::literal def = ctx.internalize(out, false, false, m_is_redundant); - add_def(def, ctx.get_literal(n)); + add_def(def, expr2literal(n)); } void solver::add_def(sat::literal def, sat::literal l) { @@ -568,14 +571,18 @@ namespace bv { } void solver::assert_ackerman(theory_var v1, theory_var v2) { - flet _red(m_is_redundant, true); + if (v1 == v2) + return; + if (v1 > v2) + std::swap(v1, v2); + flet _red(m_is_redundant, true); ++m_stats.m_ackerman; expr* o1 = var2expr(v1); expr* o2 = var2expr(v2); - expr_ref oe(m.mk_eq(o1, o2), m); + expr_ref oe = mk_var_eq(v1, v2); literal oeq = ctx.internalize(oe, false, false, m_is_redundant); - unsigned sz = get_bv_size(v1); - TRACE("bv", tout << oe << "\n";); + unsigned sz = m_bits[v1].size(); + TRACE("bv", tout << "ackerman-eq: " << s().scope_lvl() << " " << oe << "\n";); literal_vector eqs; for (unsigned i = 0; i < sz; ++i) { literal l1 = m_bits[v1][i]; @@ -583,7 +590,7 @@ namespace bv { expr_ref e1(m), e2(m); e1 = bv.mk_bit2bool(o1, i); e2 = bv.mk_bit2bool(o2, i); - expr_ref e(m.mk_eq(e1, e2), m); + expr_ref e = mk_eq(e1, e2); literal eq = ctx.internalize(e, false, false, m_is_redundant); add_clause(l1, ~l2, ~eq); add_clause(~l1, l2, ~eq); diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index cd35b5b2038..a356f5890e6 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -37,15 +37,14 @@ namespace bv { }; class solver::bit_occs_trail : public trail { - solver& s; bit_atom& a; var_pos_occ* m_occs; public: - bit_occs_trail(solver& s, bit_atom& a):s(s), a(a), m_occs(a.m_occs) {} + bit_occs_trail(solver& s, bit_atom& a): a(a), m_occs(a.m_occs) {} virtual void undo(euf::solver& euf) { - std::cout << "add back occurrences " << & a << "\n"; + IF_VERBOSE(1, verbose_stream() << "add back occurrences " << & a << "\n"); a.m_occs = m_occs; } }; @@ -57,6 +56,7 @@ namespace bv { m_ackerman(*this), m_bb(m, get_config()), m_find(*this) { + ctx.get_egraph().set_th_propagates_diseqs(id); } void solver::fixed_var_eh(theory_var v1) { @@ -194,9 +194,37 @@ namespace bv { } void solver::new_eq_eh(euf::th_eq const& eq) { - TRACE("bv", tout << "new eq " << eq.m_v1 << " == " << eq.m_v2 << "\n";); - if (is_bv(eq.m_v1)) - m_find.merge(eq.m_v1, eq.m_v2); + force_push(); + TRACE("bv", tout << "new eq " << eq.v1() << " == " << eq.v2() << "\n";); + if (is_bv(eq.v1())) + m_find.merge(eq.v1(), eq.v2()); + } + + void solver::new_diseq_eh(euf::th_eq const& ne) { + theory_var v1 = ne.v1(), v2 = ne.v2(); + if (!is_bv(v1)) + return; + if (!get_config().m_bv_eq_axioms) + return; + + TRACE("bv", tout << "diff: " << v1 << " != " << v2 << "\n";); + unsigned sz = m_bits[v1].size(); + for (unsigned i = 0; i < sz; ++i) { + sat::literal a = m_bits[v1][i]; + sat::literal b = m_bits[v2][i]; + if (a == ~b) + return; + auto va = s().value(a); + auto vb = s().value(b); + if (va != l_undef && vb != l_undef && va != vb) + return; + } + if (s().at_search_lvl()) { + force_push(); + assert_ackerman(v1, v2); + } + else + m_ackerman.used_diseq_eh(v1, v2); } double solver::get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const { return 0; } @@ -209,6 +237,7 @@ namespace bv { TRACE("bv", display_constraint(tout, idx);); switch (c.m_kind) { case bv_justification::kind_t::bv2bit: + SASSERT(s().value(c.m_antecedent) == l_true); r.push_back(c.m_antecedent); ctx.add_antecedent(var2enode(c.m_v1), var2enode(c.m_v2)); break; @@ -235,9 +264,16 @@ namespace bv { } void solver::log_drat(bv_justification const& c) { - // this has a side-effect so changes provability: - expr_ref eq(m.mk_eq(var2expr(c.m_v1), var2expr(c.m_v2)), m); - sat::literal leq = ctx.internalize(eq, false, false, false); + // introduce dummy literal for equality. + sat::literal leq(s().num_vars() + 1, false); + expr* e1 = var2expr(c.m_v1); + expr* e2 = var2expr(c.m_v2); + expr_ref eq(m.mk_eq(e1, e2), m); + ctx.get_drat().def_begin('e', eq->get_id(), std::string("=")); + ctx.get_drat().def_add_arg(e1->get_id()); + ctx.get_drat().def_add_arg(e2->get_id()); + ctx.get_drat().def_end(); + ctx.get_drat().bool_def(leq.var(), eq->get_id()); sat::literal_vector lits; auto add_bit = [&](sat::literal lit) { if (s().value(lit) == l_true) @@ -263,19 +299,24 @@ namespace bv { break; } ctx.get_drat().add(lits, status()); + ctx.get_drat().log_gc_var(leq.var()); } void solver::asserted(literal l) { + atom* a = get_bv2a(l.var()); TRACE("bv", tout << "asserted: " << l << "\n";); - if (a && a->is_bit()) + if (a && a->is_bit()) { + force_push(); for (auto vp : a->to_bit()) m_prop_queue.push_back(vp); + } } bool solver::unit_propagate() { if (m_prop_queue_head == m_prop_queue.size()) return false; + force_push(); ctx.push(value_trail(m_prop_queue_head)); for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) propagate_bits(m_prop_queue[m_prop_queue_head]); @@ -311,26 +352,26 @@ namespace bv { } sat::check_result solver::check() { + force_push(); SASSERT(m_prop_queue.size() == m_prop_queue_head); return sat::check_result::CR_DONE; } - void solver::push() { - th_euf_solver::lazy_push(); + void solver::push_core() { + th_euf_solver::push_core(); m_prop_queue_lim.push_back(m_prop_queue.size()); } - void solver::pop(unsigned n) { + void solver::pop_core(unsigned n) { + SASSERT(m_num_scopes == 0); unsigned old_sz = m_prop_queue_lim.size() - n; m_prop_queue.shrink(m_prop_queue_lim[old_sz]); m_prop_queue_lim.shrink(old_sz); - n = lazy_pop(n); - if (n > 0) { - old_sz = get_num_vars(); - m_bits.shrink(old_sz); - m_wpos.shrink(old_sz); - m_zero_one_bits.shrink(old_sz); - } + th_euf_solver::pop_core(n); + old_sz = get_num_vars(); + m_bits.shrink(old_sz); + m_wpos.shrink(old_sz); + m_zero_one_bits.shrink(old_sz); } void solver::pre_simplify() {} @@ -559,8 +600,7 @@ namespace bv { SASSERT(s().inconsistent()); } else { - if (get_config().m_bv_eq_axioms && false) { - // TODO - enable when pop_reinit is available + if (false && get_config().m_bv_eq_axioms) { expr_ref eq(m.mk_eq(var2expr(v1), var2expr(v2)), m); flet _is_redundant(m_is_redundant, true); literal eq_lit = ctx.internalize(eq, false, false, m_is_redundant); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index ea9f364c6f2..a70c9d48a4d 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -246,8 +246,8 @@ namespace bv { void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override; void asserted(literal l) override; sat::check_result check() override; - void push() override; - void pop(unsigned n) override; + void push_core() override; + void pop_core(unsigned n) override; void pre_simplify() override; void simplify() override; bool set_root(literal l, literal r) override; @@ -270,6 +270,8 @@ namespace bv { unsigned max_var(unsigned w) const override; void new_eq_eh(euf::th_eq const& eq) override; + void new_diseq_eh(euf::th_eq const& ne) override; + bool use_diseqs() const override { return true; } bool unit_propagate() override; void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index d84eafdbcbd..5bc32013ce3 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -54,9 +54,11 @@ namespace euf { if (is_app(e) && to_app(e)->get_num_args() > 0) { m_stack.push_back(sat::eframe(e)); return false; - } - n = m_egraph.mk(e, 0, nullptr); - attach_node(n); + } + if (auto* s = expr2solver(e)) + s->internalize(e, m_is_redundant); + else + attach_node(m_egraph.mk(e, 0, nullptr)); return true; } @@ -67,12 +69,10 @@ namespace euf { m_args.push_back(m_egraph.find(to_app(e)->get_arg(i))); if (root && internalize_root(to_app(e), sign, m_args)) return false; - if (auto* s = expr2solver(e)) { - s->internalize(e, m_is_redundant); - return true; - } - enode* n = m_egraph.mk(e, num, m_args.c_ptr()); - attach_node(n); + if (auto* s = expr2solver(e)) + s->internalize(e, m_is_redundant); + else + attach_node(m_egraph.mk(e, num, m_args.c_ptr())); return true; } @@ -146,7 +146,7 @@ namespace euf { sat::literal_vector lits; for (unsigned i = 0; i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { - expr_ref eq(m.mk_eq(args[i]->get_expr(), args[j]->get_expr()), m); + expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr()); sat::literal lit = internalize(eq, false, false, m_is_redundant); lits.push_back(lit); } @@ -167,10 +167,10 @@ namespace euf { for (expr* arg : *e) { expr_ref fapp(m.mk_app(f, arg), m); expr_ref gapp(m.mk_app(g, fapp.get()), m); - expr_ref eq(m.mk_eq(gapp, arg), m); + expr_ref eq = mk_eq(gapp, arg); sat::literal lit = internalize(eq, false, false, m_is_redundant); s().add_clause(1, &lit, st); - eqs.push_back(m.mk_eq(fapp, a)); + eqs.push_back(mk_eq(fapp, a)); } pb_util pb(m); expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.c_ptr(), 2), m); @@ -191,7 +191,7 @@ namespace euf { if (sz <= distinct_max_args) { for (unsigned i = 0; i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { - expr_ref eq(m.mk_eq(args[i]->get_expr(), args[j]->get_expr()), m); + expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr()); sat::literal lit = internalize(eq, true, false, m_is_redundant); s().add_clause(1, &lit, st); } @@ -208,7 +208,7 @@ namespace euf { expr_ref fresh(m.mk_fresh_const("dist-value", u), m); enode* n = m_egraph.mk(fresh, 0, nullptr); n->mark_interpreted(); - expr_ref eq(m.mk_eq(fapp, fresh), m); + expr_ref eq = mk_eq(fapp, fresh); sat::literal lit = internalize(eq, false, false, m_is_redundant); s().add_clause(1, &lit, st); } @@ -221,23 +221,30 @@ namespace euf { expr* c = nullptr, * th = nullptr, * el = nullptr; if (!m.is_bool(e) && m.is_ite(e, c, th, el)) { app* a = to_app(e); - sat::bool_var v = si.to_bool_var(c); - SASSERT(v != sat::null_bool_var); - expr_ref eq_th(m.mk_eq(a, th), m); - expr_ref eq_el(m.mk_eq(a, el), m); + expr_ref eq_th = mk_eq(a, th); sat::literal lit_th = internalize(eq_th, false, false, m_is_redundant); - sat::literal lit_el = internalize(eq_el, false, false, m_is_redundant); - literal lits1[2] = { literal(v, true), lit_th }; - literal lits2[2] = { literal(v, false), lit_el }; - s().add_clause(2, lits1, st); - s().add_clause(2, lits2, st); + if (th == el) { + s().add_clause(1, &lit_th, st); + } + else { + sat::bool_var v = si.to_bool_var(c); + SASSERT(v != sat::null_bool_var); + + expr_ref eq_el = mk_eq(a, el); + + sat::literal lit_el = internalize(eq_el, false, false, m_is_redundant); + literal lits1[2] = { literal(v, true), lit_th }; + literal lits2[2] = { literal(v, false), lit_el }; + s().add_clause(2, lits1, st); + s().add_clause(2, lits2, st); + } } else if (m.is_distinct(e)) { expr_ref_vector eqs(m); unsigned sz = n->num_args(); for (unsigned i = 0; i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { - expr_ref eq(m.mk_eq(n->get_arg(i)->get_expr(), n->get_arg(j)->get_expr()), m); + expr_ref eq = mk_eq(n->get_arg(i)->get_expr(), n->get_arg(j)->get_expr()); eqs.push_back(eq); } } @@ -308,4 +315,13 @@ namespace euf { // TODO // return get_theory(th_id)->is_shared(l->get_var()); } + + expr_ref solver::mk_eq(expr* e1, expr* e2) { + if (e1 == e2) + return expr_ref(m.mk_true(), m); + expr_ref r(m.mk_eq(e2, e1), m); + if (!m_egraph.find(r)) + r = m.mk_eq(e1, e2); + return r; + } } diff --git a/src/sat/smt/euf_invariant.cpp b/src/sat/smt/euf_invariant.cpp index e7555a016b6..9b5103dfc3a 100644 --- a/src/sat/smt/euf_invariant.cpp +++ b/src/sat/smt/euf_invariant.cpp @@ -27,19 +27,19 @@ namespace euf { void solver::check_eqc_bool_assignment() const { for (enode* n : m_egraph.nodes()) { VERIFY(!m.is_bool(n->get_expr()) || - s().value(get_literal(n)) == s().value(get_literal(n->get_root()))); + s().value(enode2literal(n)) == s().value(enode2literal(n->get_root()))); } } void solver::check_missing_bool_enode_propagation() const { for (enode* n : m_egraph.nodes()) - if (m.is_bool(n->get_expr()) && l_undef == s().value(get_literal(n))) { + if (m.is_bool(n->get_expr()) && l_undef == s().value(enode2literal(n))) { if (!n->is_root()) { - VERIFY(l_undef == s().value(get_literal(n->get_root()))); + VERIFY(l_undef == s().value(enode2literal(n->get_root()))); } else for (enode* o : enode_class(n)) { - VERIFY(l_undef == s().value(get_literal(o))); + VERIFY(l_undef == s().value(enode2literal(o))); } } } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 2c744f8c984..416a2388d1b 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -42,8 +42,15 @@ namespace euf { updt_params(p); std::function disp = - [&](std::ostream& out, void* j) { display_justification_ptr(out, reinterpret_cast(j)); }; + [&](std::ostream& out, void* j) { + display_justification_ptr(out, reinterpret_cast(j)); + }; + std::function eval = [&](enode* n) { + sat::literal lit = expr2literal(n->get_expr()); + return (lit == sat::null_literal) ? l_undef : s().value(lit); + }; m_egraph.set_display_justification(disp); + m_egraph.set_eval(eval); } void solver::updt_params(params_ref const& p) { @@ -140,8 +147,8 @@ namespace euf { ext->get_antecedents(l, idx, r, probing); for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) { size_t* e = m_explain[qhead]; - if (is_literal(e)) - r.push_back(get_literal(e)); + if (is_literal(e)) + r.push_back(get_literal(e)); else { size_t idx = get_justification(e); auto* ext = sat::constraint_base::to_extension(idx); @@ -150,9 +157,14 @@ namespace euf { ext->get_antecedents(lit, idx, r, probing); } } - m_egraph.end_explain(); + m_egraph.end_explain(); + unsigned j = 0; + for (sat::literal lit : r) + if (s().lvl(lit) > 0) r[j++] = lit; + r.shrink(j); TRACE("euf", tout << "eplain " << l << " <- " << r << " " << probing << "\n";); DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true);); + if (!probing) log_antecedents(l, r); } @@ -204,13 +216,13 @@ namespace euf { void solver::asserted(literal l) { expr* e = m_var2expr.get(l.var(), nullptr); - if (!e) { - return; - } + if (!e) + return; bool sign = l.sign(); - TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";); + euf::enode* n = m_egraph.find(e); + TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";); if (!n) return; for (auto th : enode_th_vars(n)) @@ -220,33 +232,18 @@ namespace euf { size_t* c = to_ptr(l); SASSERT(is_literal(c)); SASSERT(l == get_literal(c)); - if (m.is_eq(e) && n->num_args() == 2) { + if (m.is_eq(e) && n->num_args() == 2 && !sign) { euf::enode* na = n->get_arg(0); euf::enode* nb = n->get_arg(1); - if (!sign) { - m_egraph.merge(na, nb, c); - return; - } - else - new_diseq(na, nb, l); + m_egraph.merge(na, nb, c); } - euf::enode* nb = sign ? mk_false() : mk_true(); - m_egraph.merge(n, nb, c); - } - - void solver::new_diseq(enode* n1, enode* n2, literal lit) { - enode * r1 = n1->get_root(); - enode * r2 = n2->get_root(); - if (r1 == r2) - return; - if (r1->has_one_th_var() && r2->has_one_th_var() && r1->get_first_th_id() == r2->get_first_th_id()) { - theory_id id = r1->get_first_th_id(); - theory_var v1 = r1->get_th_var(id); - theory_var v2 = r2->get_th_var(id); - fid2solver(id)->new_diseq_eh(r1, r2); + else { + euf::enode* nb = sign ? mk_false() : mk_true(); + m_egraph.merge(n, nb, c); } } + bool solver::unit_propagate() { bool propagated = false; while (!s().inconsistent()) { @@ -284,7 +281,7 @@ namespace euf { bool_var v = si.to_bool_var(e); SASSERT(m.is_bool(e)); size_t cnstr; - literal lit; + literal lit; if (is_eq) { VERIFY(m.is_eq(e, a, b)); cnstr = eq_constraint().to_index(); @@ -315,7 +312,10 @@ namespace euf { void solver::propagate_th_eqs() { for (; m_egraph.has_th_eq() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_th_eq()) { th_eq eq = m_egraph.get_th_eq(); - m_id2solver[eq.m_id]->new_eq_eh(eq); + if (eq.is_eq()) + m_id2solver[eq.id()]->new_eq_eh(eq); + else + m_id2solver[eq.id()]->new_diseq_eh(eq); } } @@ -379,6 +379,7 @@ namespace euf { m_scopes.shrink(m_scopes.size() - n); si.pop(n); SASSERT(m_egraph.num_scopes() == m_scopes.size()); + TRACE("euf", tout << "pop to: " << m_scopes.size() << "\n";); } void solver::start_reinit(unsigned n) { @@ -405,9 +406,19 @@ namespace euf { if (expr2var_replay.empty()) return; si.set_expr2var_replay(&expr2var_replay); - for (auto const& kv : expr2var_replay) - attach_lit(si.internalize(kv.m_key, true), kv.m_key); - si.set_expr2var_replay(nullptr); + TRACE("euf", for (auto const& kv : expr2var_replay) tout << "replay: " << kv.m_value << " " << mk_bounded_pp(kv.m_key, m) << "\n";); + for (auto const& kv : expr2var_replay) { + sat::literal lit; + expr* e = kv.m_key; + if (si.is_bool_op(e)) + lit = literal(expr2var_replay[e], false); + else + lit = si.internalize(kv.m_key, true); + VERIFY(lit.var() == kv.m_value); + attach_lit(lit, kv.m_key); + } + si.set_expr2var_replay(nullptr); + TRACE("euf", tout << "replay done\n";); } void solver::pre_simplify() { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 6f90e62a18e..ab20d6b4113 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -49,8 +49,6 @@ namespace euf { size_t to_index() const { return sat::constraint_base::mem2base(this); } }; - - class solver : public sat::extension, public th_internalizer, public th_decompile { typedef top_sort deps_t; friend class ackerman; @@ -194,10 +192,11 @@ namespace euf { sat::sat_internalizer& get_si() { return si; } ast_manager& get_manager() { return m; } enode* get_enode(expr* e) { return m_egraph.find(e); } - sat::literal get_literal(expr* e) const { return literal(si.to_bool_var(e), false); } - sat::literal get_literal(enode* e) const { return get_literal(e->get_expr()); } + sat::literal expr2literal(expr* e) const { return literal(si.to_bool_var(e), false); } + sat::literal enode2literal(enode* e) const { return expr2literal(e->get_expr()); } smt_params const& get_config() { return m_config; } region& get_region() { return m_trail.get_region(); } + egraph& get_egraph() { return m_egraph; } template void push(C const& c) { m_trail.push(c); } euf_trail_stack& get_trail_stack() { return m_trail; } @@ -254,6 +253,8 @@ namespace euf { void internalize(expr* e, bool learned) override; void attach_th_var(enode* n, th_solver* th, theory_var v) { m_egraph.add_th_var(n, v, th->get_id()); } void attach_node(euf::enode* n); + expr_ref mk_eq(expr* e1, expr* e2); + expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); } euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); } expr* bool_var2expr(sat::bool_var v) { return m_var2expr.get(v, nullptr); } void unhandled_function(func_decl* f); diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index c804ff29c17..4173bae8ece 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -74,7 +74,7 @@ namespace euf { } sat::literal th_euf_solver::expr2literal(expr* e) const { - return ctx.get_literal(e); + return ctx.expr2literal(e); } expr* th_euf_solver::bool_var2expr(sat::bool_var v) const { @@ -98,26 +98,23 @@ namespace euf { return get_th_var(ctx.get_enode(e)); } - void th_euf_solver::push() { + void th_euf_solver::push_core() { + TRACE("euf", tout << "push-core\n";); m_var2enode_lim.push_back(m_var2enode.size()); } - void th_euf_solver::pop(unsigned num_scopes) { + void th_euf_solver::pop_core(unsigned num_scopes) { unsigned new_lvl = m_var2enode_lim.size() - num_scopes; m_var2enode.shrink(m_var2enode_lim[new_lvl]); m_var2enode_lim.shrink(new_lvl); } - unsigned th_euf_solver::lazy_pop(unsigned n) { - if (n <= m_num_scopes) { - m_num_scopes -= n; - return 0; - } - else { - n -= m_num_scopes; - pop(n); - return n; - } + void th_euf_solver::pop(unsigned n) { + unsigned k = std::min(m_num_scopes, n); + m_num_scopes -= k; + n -= k; + if (n > 0) + pop_core(n); } bool th_euf_solver::add_unit(sat::literal lit) { @@ -154,4 +151,9 @@ namespace euf { void th_euf_solver::rewrite(expr_ref& a) { ctx.get_rewriter()(a); } + + expr_ref th_euf_solver::mk_eq(expr* e1, expr* e2) { + return ctx.mk_eq(e1, e2); + } + } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 96922f35aef..18d435fe821 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -95,13 +95,15 @@ namespace euf { virtual bool use_diseqs() const { return false; } - virtual void new_diseq_eh(euf::enode* a, euf::enode* b) {} + virtual void new_diseq_eh(euf::th_eq const& eq) {} /** \brief Parametric theories (e.g. Arrays) should implement this method. */ virtual bool is_shared(theory_var v) const { return false; } + + }; class th_euf_solver : public th_solver { @@ -129,9 +131,15 @@ namespace euf { euf::enode* e_internalize(expr* e) { internalize(e, m_is_redundant); return expr2enode(e); } euf::enode* mk_enode(expr* e, bool suppress_args); + expr_ref mk_eq(expr* e1, expr* e2); + expr_ref mk_var_eq(theory_var v1, theory_var v2) { return mk_eq(var2expr(v1), var2expr(v2)); } void rewrite(expr_ref& a); + virtual void push_core(); + virtual void pop_core(unsigned n); + void force_push() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); } + public: th_euf_solver(euf::solver& ctx, euf::theory_id id); virtual ~th_euf_solver() {} @@ -147,12 +155,9 @@ namespace euf { trail_stack & get_trail_stack(); bool is_attached_to_var(enode* n) const; bool is_root(theory_var v) const { return var2enode(v)->is_root(); } - void push() override; - void pop(unsigned n) override; + void push() override { m_num_scopes++; } + void pop(unsigned n) override; - void lazy_push() { ++m_num_scopes; } - void force_push() { for (; m_num_scopes > 0; --m_num_scopes) push(); } - unsigned lazy_pop(unsigned n); }; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 953400063db..12228e8a58a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -155,7 +155,10 @@ struct goal2sat::imp : public sat::sat_internalizer { } sat::bool_var add_var(bool is_ext, expr* n) { - auto v = m_solver.add_var(is_ext); + sat::bool_var v; + if (m_expr2var_replay && m_expr2var_replay->find(n, v)) + return v; + v = m_solver.add_var(is_ext); log_node(n); log_def(v, n); return v; @@ -298,18 +301,17 @@ struct goal2sat::imp : public sat::sat_internalizer { } } - bool process_cached(app * t, bool root, bool sign) { - sat::literal l; - if (m_cache.find(t, l)) { - if (sign) - l.neg(); - if (root) - mk_root_clause(l); - else - m_result_stack.push_back(l); - return true; - } - return false; + bool process_cached(app* t, bool root, bool sign) { + sat::literal l = sat::null_literal; + if (!m_cache.find(t, l)) + return false; + if (sign) + l.neg(); + if (root) + mk_root_clause(l); + else + m_result_stack.push_back(l); + return true; } bool visit(expr * t, bool root, bool sign) { @@ -321,7 +323,7 @@ struct goal2sat::imp : public sat::sat_internalizer { if (process_cached(to_app(t), root, sign)) return true; if (to_app(t)->get_family_id() != m.get_basic_family_id()) - return convert_app(to_app(t), root, sign); + return convert_app(to_app(t), root, sign); switch (to_app(t)->get_decl_kind()) { case OP_NOT: case OP_OR: diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index 3e655fa1855..af170270010 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -128,7 +128,7 @@ class smt_checker { } m_lemma_solver->pop(1); std::cout << "smt\n"; - check_assertion_redundant(lits); + // check_assertion_redundant(lits); } public: @@ -205,9 +205,6 @@ class smt_checker { case sexpr::kind_t::BV_NUMERAL: { std::cout << "bv numeral\n"; goto bail; - unsigned sz = sexpr->get_bv_size(); - rational r = sexpr->get_numeral(); - break; } case sexpr::kind_t::STRING: case sexpr::kind_t::KEYWORD: @@ -314,6 +311,9 @@ static void verify_smt(char const* drat_file, char const* smt_file) { bool_var2expr.reserve(r.m_node_id+1); bool_var2expr.set(r.m_node_id, exprs.get(r.m_args[0])); break; + case dimacs::drat_record::tag_t::is_var_gc: + drat_checker.gc_var(r.m_node_id); + break; default: UNREACHABLE(); break; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ded691aa0ab..20f931e7e46 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2704,84 +2704,6 @@ namespace smt { SASSERT(check_clauses(m_lemmas) && check_clauses(m_aux_clauses)); } - void context::log_stats() { - size_t bin_clauses = 0, bin_lemmas = 0; - for (watch_list const& w : m_watches) { - bin_clauses += w.end_literals() - w.begin_literals(); - } - bin_clauses /= 2; - for (clause* cp : m_lemmas) - if (cp->get_num_literals() == 2) - ++bin_lemmas; - std::stringstream strm; - strm << "(smt.stats " - << std::setw(4) << m_stats.m_num_restarts << " " - << std::setw(6) << m_stats.m_num_conflicts << " " - << std::setw(6) << m_stats.m_num_decisions << " " - << std::setw(6) << m_stats.m_num_propagations << " " - << std::setw(5) << (m_aux_clauses.size() + bin_clauses) << "/" << bin_clauses << " " - << std::setw(5) << m_lemmas.size(); if (bin_lemmas > 0) strm << "/" << bin_lemmas << " "; - strm << std::setw(5) << m_stats.m_num_simplifications << " " - << std::setw(4) << m_stats.m_num_del_clauses << " " - << std::setw(7) << mem_stat() << ")\n"; - - std::string str(strm.str()); - svector offsets; - for (size_t i = 0; i < str.size(); ++i) { - while (i < str.size() && str[i] != ' ') ++i; - while (i < str.size() && str[i] == ' ') ++i; - // position of first character after space - if (i < str.size()) { - offsets.push_back(i); - } - } - bool same = m_last_positions.size() == offsets.size(); - size_t diff = 0; - for (unsigned i = 0; i < offsets.size() && same; ++i) { - if (m_last_positions[i] > offsets[i]) diff += m_last_positions[i] - offsets[i]; - if (m_last_positions[i] < offsets[i]) diff += offsets[i] - m_last_positions[i]; - } - - if (m_last_positions.empty() || - m_stats.m_num_restarts >= 20 + m_last_position_log || - (m_stats.m_num_restarts >= 6 + m_last_position_log && (!same || diff > 3))) { - m_last_position_log = m_stats.m_num_restarts; - // restarts decisions clauses simplifications memory - // conflicts propagations lemmas deletions - int adjust[9] = { -3, -3, -3, -3, -3, -3, -4, -4, -1 }; - char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin ", ":lemmas ", ":simplify ", ":deletions", ":memory" }; - - std::stringstream l1, l2; - l1 << "(smt.stats "; - l2 << "(smt.stats "; - size_t p1 = 11, p2 = 11; - SASSERT(offsets.size() == 9); - for (unsigned i = 0; i < offsets.size(); ++i) { - size_t p = offsets[i]; - if (i & 0x1) { - // odd positions - for (; p2 < p + adjust[i]; ++p2) l2 << " "; - p2 += strlen(tag[i]); - l2 << tag[i]; - } - else { - // even positions - for (; p1 < p + adjust[i]; ++p1) l1 << " "; - p1 += strlen(tag[i]); - l1 << tag[i]; - } - } - for (; p1 + 2 < str.size(); ++p1) l1 << " "; - for (; p2 + 2 < str.size(); ++p2) l2 << " "; - l1 << ")\n"; - l2 << ")\n"; - IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str()); - m_last_positions.reset(); - m_last_positions.append(offsets); - } - IF_VERBOSE(1, verbose_stream() << str); - } - struct clause_lt { bool operator()(clause * cls1, clause * cls2) const { return cls1->get_activity() > cls2->get_activity(); } }; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 0d049877733..0d84ede0071 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -661,7 +661,83 @@ namespace smt { return out << enode_pp(p.p.first, p.ctx) << " = " << enode_pp(p.p.second, p.ctx) << "\n"; } - + void context::log_stats() { + size_t bin_clauses = 0, bin_lemmas = 0; + for (watch_list const& w : m_watches) { + bin_clauses += w.end_literals() - w.begin_literals(); + } + bin_clauses /= 2; + for (clause* cp : m_lemmas) + if (cp->get_num_literals() == 2) + ++bin_lemmas; + std::stringstream strm; + strm << "(smt.stats " + << std::setw(4) << m_stats.m_num_restarts << " " + << std::setw(6) << m_stats.m_num_conflicts << " " + << std::setw(6) << m_stats.m_num_decisions << " " + << std::setw(6) << m_stats.m_num_propagations << " " + << std::setw(5) << (m_aux_clauses.size() + bin_clauses) << "/" << bin_clauses << " " + << std::setw(5) << m_lemmas.size(); if (bin_lemmas > 0) strm << "/" << bin_lemmas << " "; + strm << std::setw(5) << m_stats.m_num_simplifications << " " + << std::setw(4) << m_stats.m_num_del_clauses << " " + << std::setw(7) << mem_stat() << ")\n"; + + std::string str(strm.str()); + svector offsets; + for (size_t i = 0; i < str.size(); ++i) { + while (i < str.size() && str[i] != ' ') ++i; + while (i < str.size() && str[i] == ' ') ++i; + // position of first character after space + if (i < str.size()) { + offsets.push_back(i); + } + } + bool same = m_last_positions.size() == offsets.size(); + size_t diff = 0; + for (unsigned i = 0; i < offsets.size() && same; ++i) { + if (m_last_positions[i] > offsets[i]) diff += m_last_positions[i] - offsets[i]; + if (m_last_positions[i] < offsets[i]) diff += offsets[i] - m_last_positions[i]; + } + + if (m_last_positions.empty() || + m_stats.m_num_restarts >= 20 + m_last_position_log || + (m_stats.m_num_restarts >= 6 + m_last_position_log && (!same || diff > 3))) { + m_last_position_log = m_stats.m_num_restarts; + // restarts decisions clauses simplifications memory + // conflicts propagations lemmas deletions + int adjust[9] = { -3, -3, -3, -3, -3, -3, -4, -4, -1 }; + char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin ", ":lemmas ", ":simplify ", ":deletions", ":memory" }; + + std::stringstream l1, l2; + l1 << "(smt.stats "; + l2 << "(smt.stats "; + size_t p1 = 11, p2 = 11; + SASSERT(offsets.size() == 9); + for (unsigned i = 0; i < offsets.size(); ++i) { + size_t p = offsets[i]; + if (i & 0x1) { + // odd positions + for (; p2 < p + adjust[i]; ++p2) l2 << " "; + p2 += strlen(tag[i]); + l2 << tag[i]; + } + else { + // even positions + for (; p1 < p + adjust[i]; ++p1) l1 << " "; + p1 += strlen(tag[i]); + l1 << tag[i]; + } + } + for (; p1 + 2 < str.size(); ++p1) l1 << " "; + for (; p2 + 2 < str.size(); ++p2) l2 << " "; + l1 << ")\n"; + l2 << ")\n"; + IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str()); + m_last_positions.reset(); + m_last_positions.append(offsets); + } + IF_VERBOSE(1, verbose_stream() << str); + } }; diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index e67b5f9b8c1..8613b8a9b30 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -152,8 +152,8 @@ class bv1_blaster_tactic : public tactic { SASSERT(t_bits.size() == e_bits.size()); bit_buffer new_ites; unsigned num = t_bits.size(); - for (unsigned i = 0; i < num; i++) - new_ites.push_back(m().mk_ite(c, t_bits[i], e_bits[i])); + for (unsigned i = 0; i < num; i++) + new_ites.push_back(t_bits[i] == e_bits[i] ? t_bits[i] : m().mk_ite(c, t_bits[i], e_bits[i])); result = butil().mk_concat(new_ites.size(), new_ites.c_ptr()); } diff --git a/src/test/egraph.cpp b/src/test/egraph.cpp index 04e95095968..4fc5536934b 100644 --- a/src/test/egraph.cpp +++ b/src/test/egraph.cpp @@ -81,7 +81,7 @@ static void test2() { g.propagate(); std::cout << "propagated " << t.get_seconds() << "\n"; for (euf::enode* n : top_nodes) { - SASSERT(n->get_root() == top_nodes[0]->get_root()); + VERIFY(n->get_root() == top_nodes[0]->get_root()); } }