diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 0e2005e15..8dd870964 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -15,6 +15,7 @@ z3_add_component(ast ast_util.cpp bv_decl_plugin.cpp char_decl_plugin.cpp + cost_evaluator.cpp datatype_decl_plugin.cpp decl_collector.cpp display_dimacs.cpp diff --git a/src/smt/cost_evaluator.cpp b/src/ast/cost_evaluator.cpp similarity index 98% rename from src/smt/cost_evaluator.cpp rename to src/ast/cost_evaluator.cpp index 51c025e66..bb14b3097 100644 --- a/src/smt/cost_evaluator.cpp +++ b/src/ast/cost_evaluator.cpp @@ -16,7 +16,7 @@ Author: Revision History: --*/ -#include "smt/cost_evaluator.h" +#include "ast/cost_evaluator.h" #include "util/warning.h" cost_evaluator::cost_evaluator(ast_manager & m): diff --git a/src/smt/cost_evaluator.h b/src/ast/cost_evaluator.h similarity index 100% rename from src/smt/cost_evaluator.h rename to src/ast/cost_evaluator.h diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index d908baf87..9eb90b0ba 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -295,8 +295,6 @@ namespace euf { enode_vector const& nodes() const { return m_nodes; } ast_manager& get_manager() { return m; } - bool is_relevant(enode* n) const { return true; } // TODO - bool resource_limits_exceeded() const { return false; } // TODO void invariant(); void copy_from(egraph const& src, std::function& copy_justification); diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index c81a75283..e62b01941 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -29,10 +29,13 @@ z3_add_component(sat_smt euf_relevancy.cpp euf_solver.cpp fpa_solver.cpp + q_clause.cpp q_ematch.cpp + q_eval.cpp q_mam.cpp q_mbi.cpp q_model_fixer.cpp + q_queue.cpp q_solver.cpp sat_dual_solver.cpp sat_th.cpp diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 9dd814a0e..ab3a2ac7c 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -306,6 +306,8 @@ namespace euf { bool is_blocked(literal l, ext_constraint_idx) override; bool check_model(sat::model const& m) const override; void gc_vars(unsigned num_vars) override; + bool resource_limits_exceeded() const { return false; } // TODO + // proof bool use_drat() { return s().get_config().m_drat && (init_drat(), true); } @@ -345,6 +347,7 @@ namespace euf { bool is_relevant(expr* e) const; bool is_relevant(enode* n) const; + // model construction void update_model(model_ref& mdl); obj_map const& values2root(); diff --git a/src/sat/smt/q_clause.cpp b/src/sat/smt/q_clause.cpp new file mode 100644 index 000000000..0e64d5029 --- /dev/null +++ b/src/sat/smt/q_clause.cpp @@ -0,0 +1,53 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_clause.cpp + +Abstract: + + Clause and literals + +Author: + + Nikolaj Bjorner (nbjorner) 2021-01-24 + +--*/ + +#include "sat/smt/q_clause.h" + + +namespace q { + + std::ostream& lit::display(std::ostream& out) const { + ast_manager& m = lhs.m(); + if (m.is_true(rhs) && !sign) + return out << lhs; + if (m.is_false(rhs) && !sign) + return out << "(not " << lhs << ")"; + return + out << mk_bounded_pp(lhs, lhs.m(), 2) + << (sign ? " != " : " == ") + << mk_bounded_pp(rhs, rhs.m(), 2); + } + + std::ostream& clause::display(euf::solver& ctx, std::ostream& out) const { + out << "clause:\n"; + for (auto const& lit : m_lits) + lit.display(out) << "\n"; + binding* b = m_bindings; + if (b) { + do { + for (unsigned i = 0; i < num_decls(); ++i) + out << ctx.bpp((*b)[i]) << " "; + out << "\n"; + b = b->next(); + } + while (b != m_bindings); + } + return out; + } + + +} diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h new file mode 100644 index 000000000..823263964 --- /dev/null +++ b/src/sat/smt/q_clause.h @@ -0,0 +1,90 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_clause.h + +Abstract: + + Clause and literals + +Author: + + Nikolaj Bjorner (nbjorner) 2021-01-24 + +--*/ +#pragma once + +#include "util/dlist.h" +#include "ast/ast.h" +#include "ast/quantifier_stat.h" +#include "ast/euf/euf_enode.h" +#include "sat/smt/euf_solver.h" + +namespace q { + + struct lit { + expr_ref lhs; + expr_ref rhs; + bool sign; + lit(expr_ref const& lhs, expr_ref const& rhs, bool sign): + lhs(lhs), rhs(rhs), sign(sign) {} + std::ostream& display(std::ostream& out) const; + }; + + struct binding : public dll_base { + app* m_pattern; + unsigned m_max_generation; + unsigned m_min_top_generation; + unsigned m_max_top_generation; + euf::enode* m_nodes[0]; + + binding(app* pat, unsigned max_generation, unsigned min_top, unsigned max_top): + m_pattern(pat), + m_max_generation(max_generation), + m_min_top_generation(min_top), + m_max_top_generation(max_top) {} + + euf::enode* const* nodes() { return m_nodes; } + + euf::enode* operator[](unsigned i) const { return m_nodes[i]; } + + }; + + struct clause { + unsigned m_index; + vector m_lits; + quantifier_ref m_q; + sat::literal m_literal; + q::quantifier_stat* m_stat { nullptr }; + binding* m_bindings { nullptr }; + + clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {} + + std::ostream& display(euf::solver& ctx, std::ostream& out) const; + lit const& operator[](unsigned i) const { return m_lits[i]; } + lit& operator[](unsigned i) { return m_lits[i]; } + unsigned size() const { return m_lits.size(); } + unsigned num_decls() const { return m_q->get_num_decls(); } + unsigned index() const { return m_index; } + quantifier* q() const { return m_q; } + }; + + struct justification { + expr* m_lhs, *m_rhs; + bool m_sign; + clause& m_clause; + euf::enode* const* m_binding; + justification(lit const& l, clause& c, euf::enode* const* b): + m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_clause(c), m_binding(b) {} + sat::ext_constraint_idx to_index() const { + return sat::constraint_base::mem2base(this); + } + static justification& from_index(size_t idx) { + return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem()); + } + static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(justification)); } + }; + +} diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 648c94651..d2cc7dac8 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -15,16 +15,16 @@ Author: Todo: -- clausify -- generations -- insert instantiations into priority queue -- cache instantiations and substitutions - nested quantifiers - non-cnf quantifiers (handled in q_solver) Done: +- clausify - propagate without instantiations, produce explanations for eval +- generations +- insert instantiations into priority queue +- cache instantiations and substitutions --*/ @@ -47,23 +47,14 @@ namespace q { ~scoped_mark_reset() { e.m_mark.reset(); } }; - unsigned ematch::fingerprint::hash() const { - NOT_IMPLEMENTED_YET(); - return 0; - } - - bool ematch::fingerprint::eq(fingerprint const& other) const { - NOT_IMPLEMENTED_YET(); - return false; - } - - ematch::ematch(euf::solver& ctx, solver& s): ctx(ctx), m_qs(s), m(ctx.get_manager()), + m_eval(ctx), m_infer_patterns(m, ctx.get_config()), - m_qstat_gen(m, ctx.get_region()) + m_inst_queue(*this, ctx), + m_qstat_gen(m, ctx.get_region()) { std::function _on_merge = [&](euf::enode* root, euf::enode* other) { @@ -85,7 +76,7 @@ namespace q { } void ematch::ensure_ground_enodes(clause const& c) { - quantifier* q = c.m_q; + quantifier* q = c.q(); unsigned num_patterns = q->get_num_patterns(); for (unsigned i = 0; i < num_patterns; i++) ensure_ground_enodes(q->get_pattern(i)); @@ -100,7 +91,7 @@ namespace q { sat::constraint_base::initialize(mem, &m_qs); bool sign = false; expr* l = nullptr, *r = nullptr; - lit lit(expr_ref(l,m), expr_ref(r, m), sign); + lit lit(expr_ref(l, m), expr_ref(r, m), sign); if (idx != UINT_MAX) lit = c[idx]; auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b); @@ -108,16 +99,7 @@ namespace q { } void ematch::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) { - auto& j = justification::from_index(idx); - clause& c = j.m_clause; - unsigned l_idx = 0; - for (; l_idx < c.size(); ++l_idx) { - if (c[l_idx].lhs == j.m_lhs && c[l_idx].rhs == j.m_rhs && c[l_idx].sign == j.m_sign) - break; - } - explain(c, l_idx, j.m_binding); - r.push_back(c.m_literal); - (void)probing; // ignored + m_eval.explain(l, justification::from_index(idx), r, probing); } std::ostream& ematch::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { @@ -138,87 +120,6 @@ namespace q { return out; } - void ematch::explain(clause& c, unsigned literal_idx, euf::enode* const* b) { - unsigned n = c.num_decls(); - for (unsigned i = c.size(); i-- > 0; ) { - if (i == literal_idx) - continue; - auto const& lit = c[i]; - if (lit.sign) - explain_eq(n, b, lit.lhs, lit.rhs); - else - explain_diseq(n, b, lit.lhs, lit.rhs); - } - } - - void ematch::explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t) { - SASSERT(l_true == compare(n, binding, s, t)); - if (s == t) - return; - euf::enode* sn = eval(n, binding, s); - euf::enode* tn = eval(n, binding, t); - if (sn && tn) { - SASSERT(sn->get_root() == tn->get_root()); - ctx.add_antecedent(sn, tn); - return; - } - if (!sn && tn) { - std::swap(sn, tn); - std::swap(s, t); - } - if (sn && !tn) { - for (euf::enode* s1 : euf::enode_class(sn)) { - if (l_true == compare_rec(n, binding, t, s1->get_expr())) { - ctx.add_antecedent(sn, s1); - explain_eq(n, binding, t, s1->get_expr()); - return; - } - } - UNREACHABLE(); - } - SASSERT(is_app(s) && is_app(t)); - SASSERT(to_app(s)->get_decl() == to_app(t)->get_decl()); - for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) - explain_eq(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i)); - } - - void ematch::explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t) { - SASSERT(l_false == compare(n, binding, s, t)); - if (m.are_distinct(s, t)) - return; - euf::enode* sn = eval(n, binding, s); - euf::enode* tn = eval(n, binding, t); - if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) { - ctx.add_diseq_antecedent(sn, tn); - return; - } - if (!sn && tn) { - std::swap(sn, tn); - std::swap(s, t); - } - if (sn && !tn) { - for (euf::enode* s1 : euf::enode_class(sn)) { - if (l_false == compare_rec(n, binding, t, s1->get_expr())) { - ctx.add_antecedent(sn, s1); - explain_diseq(n, binding, t, s1->get_expr()); - return; - } - } - UNREACHABLE(); - } - SASSERT(is_app(s) && is_app(t)); - app* at = to_app(t); - app* as = to_app(s); - SASSERT(as->get_decl() == at->get_decl()); - for (unsigned i = as->get_num_args(); i-- > 0; ) { - if (l_false == compare_rec(n, binding, as->get_arg(i), at->get_arg(i))) { - explain_eq(n, binding, as->get_arg(i), at->get_arg(i)); - return; - } - } - UNREACHABLE(); - } - struct restore_watch : public trail { vector& v; unsigned idx, offset; @@ -252,11 +153,11 @@ namespace q { // watch only nodes introduced in bindings or ground arguments of functions // or functions that have been inserted. - void ematch::add_watch(euf::enode* n, unsigned idx) { + void ematch::add_watch(euf::enode* n, unsigned clause_idx) { unsigned root_id = n->get_root_id(); m_watch.reserve(root_id + 1); ctx.push(restore_watch(m_watch, root_id)); - m_watch[root_id].push_back(idx); + m_watch[root_id].push_back(clause_idx); } void ematch::init_watch(expr* e, unsigned clause_idx) { @@ -280,7 +181,8 @@ namespace q { } } - void ematch::init_watch(clause& c, unsigned idx) { + void ematch::init_watch(clause& c) { + unsigned idx = c.index(); for (auto lit : c.m_lits) { if (!is_ground(lit.lhs)) init_watch(lit.lhs, idx); @@ -307,153 +209,112 @@ namespace q { } }; - ematch::binding* ematch::alloc_binding(unsigned n, unsigned max_generation, unsigned min_top, unsigned max_top) { + binding* ematch::alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top) { unsigned sz = sizeof(binding) + sizeof(euf::enode* const*)*n; void* mem = ctx.get_region().allocate(sz); - return new (mem) binding(max_generation, min_top, max_top); + return new (mem) binding(pat, max_generation, min_top, max_top); } - std::ostream& ematch::lit::display(std::ostream& out) const { - ast_manager& m = lhs.m(); - if (m.is_true(rhs) && !sign) - return out << lhs; - if (m.is_false(rhs) && !sign) - return out << "(not " << lhs << ")"; - return - out << mk_bounded_pp(lhs, lhs.m(), 2) - << (sign ? " != " : " == ") - << mk_bounded_pp(rhs, rhs.m(), 2); - } - - void ematch::clause::add_binding(ematch& em, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) { - unsigned n = num_decls(); - binding* b = em.alloc_binding(n, max_generation, min_top, max_top); + void ematch::add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) { + unsigned n = c.num_decls(); + binding* b = alloc_binding(n, pat, max_generation, min_top, max_top); b->init(b); for (unsigned i = 0; i < n; ++i) b->m_nodes[i] = _binding[i]; - binding::push_to_front(m_bindings, b); - em.ctx.push(remove_binding(*this, b)); + binding::push_to_front(c.m_bindings, b); + ctx.push(remove_binding(c, b)); } void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) { TRACE("q", tout << "on-binding " << mk_pp(q, m) << "\n";); - clause& c = *m_clauses[m_q2clauses[q]]; - if (!propagate(_binding, c)) - c.add_binding(*this, _binding, max_generation, min_gen, max_gen); - } - - std::ostream& ematch::clause::display(euf::solver& ctx, std::ostream& out) const { - out << "clause:\n"; - for (auto const& lit : m_lits) - lit.display(out) << "\n"; - binding* b = m_bindings; - if (b) { - do { - for (unsigned i = 0; i < num_decls(); ++i) - out << ctx.bpp(b->nodes()[i]) << " "; - out << "\n"; - b = b->next(); - } - while (b != m_bindings); + unsigned idx = m_q2clauses[q]; + clause& c = *m_clauses[idx]; + if (!propagate(_binding, max_generation, c)) { + add_binding(c, pat, _binding, max_generation, min_gen, max_gen); + insert_clause_in_queue(idx); } - return out; } - bool ematch::propagate(euf::enode* const* binding, clause& c) { + bool ematch::propagate(euf::enode* const* binding, unsigned max_generation, clause& c) { TRACE("q", c.display(ctx, tout) << "\n";); - unsigned clause_idx = m_q2clauses[c.m_q]; - scoped_mark_reset _sr(*this); - unsigned idx = UINT_MAX; - unsigned sz = c.m_lits.size(); - unsigned n = c.num_decls(); - m_indirect_nodes.reset(); - for (unsigned i = 0; i < sz; ++i) { - unsigned lim = m_indirect_nodes.size(); - lit l = c[i]; - lbool cmp = compare(n, binding, l.lhs, l.rhs); - switch (cmp) { - case l_false: - m_indirect_nodes.shrink(lim); - if (!l.sign) - break; - if (i > 0) - std::swap(c[0], c[i]); - return true; - case l_true: - m_indirect_nodes.shrink(lim); - if (l.sign) - break; - if (i > 0) - std::swap(c[0], c[i]); - return true; - case l_undef: - TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";); - if (idx == 0) { - // attach bindings and indirect nodes - // to watch - for (euf::enode* n : m_indirect_nodes) - add_watch(n, clause_idx); - for (unsigned j = c.num_decls(); j-- > 0; ) - add_watch(binding[j], clause_idx); - if (i > 1) - std::swap(c[1], c[i]); - return false; - } - else if (i > 0) - std::swap(c[0], c[i]); - idx = 0; - break; - } + lbool ev = m_eval(binding, c, idx); + if (ev == l_true) { + ++m_stats.m_num_redundant; + return true; } - TRACE("q", tout << "instantiate " << (idx == UINT_MAX ? "clause is false":"unit propagate") << "\n";); - - auto j_idx = mk_justification(idx, c, binding); - if (idx == UINT_MAX) + if (ev == l_undef && idx == UINT_MAX) { + unsigned clause_idx = c.index(); + for (euf::enode* n : m_eval.get_watch()) + add_watch(n, clause_idx); + for (unsigned j = c.num_decls(); j-- > 0; ) + add_watch(binding[j], clause_idx); + return false; + } + if (ev == l_undef && max_generation > m_generation_propagation_threshold) + return false; + auto j_idx = mk_justification(idx, c, binding); + if (ev == l_false) { + ++m_stats.m_num_conflicts; ctx.set_conflict(j_idx); - else + } + else { + ++m_stats.m_num_propagations; ctx.propagate(instantiate(c, binding, c[idx]), j_idx); + } return true; } - // vanilla instantiation method. void ematch::instantiate(binding& b, clause& c) { - expr_ref_vector _nodes(m); - quantifier* q = c.m_q; + quantifier* q = c.q(); if (m_stats.m_num_instantiations > ctx.get_config().m_qi_max_instances) return; unsigned max_generation = b.m_max_generation; max_generation = std::max(max_generation, c.m_stat->get_generation()); c.m_stat->update_max_generation(max_generation); -#if 0 fingerprint * f = add_fingerprint(c, b, max_generation); - if (f) { - m_queue.insert(f, max_generation); - m_stats.m_num_instantiations++; - } - return; -#endif - - m_stats.m_num_instantiations++; - - for (unsigned i = 0; i < c.num_decls(); ++i) - _nodes.push_back(b.m_nodes[i]->get_expr()); - var_subst subst(m); - expr_ref result = subst(q->get_expr(), _nodes); - sat::literal result_l = ctx.mk_literal(result); - if (is_exists(q)) - result_l.neg(); - m_qs.add_clause(c.m_literal, result_l); + if (!f) + return; + m_inst_queue.insert(f); + m_stats.m_num_instantiations++; } - ematch::fingerprint* ematch::add_fingerprint(clause& c, binding& b, unsigned max_generation) { - NOT_IMPLEMENTED_YET(); - return nullptr; + void ematch::add_instantiation(clause& c, binding& b, sat::literal lit) { + ctx.propagate(lit, mk_justification(UINT_MAX, c, b.nodes())); + } + + void ematch::set_tmp_binding(fingerprint& fp) { + binding& b = *fp.b; + clause& c = *fp.c; + if (c.num_decls() > m_tmp_binding_capacity) { + void* mem = memory::allocate(sizeof(binding) + c.num_decls()*sizeof(euf::enode*)); + m_tmp_binding = new (mem) binding(b.m_pattern, 0, 0, 0); + m_tmp_binding_capacity = c.num_decls(); + } + + fp.b = m_tmp_binding.get(); + for (unsigned i = c.num_decls(); i-- > 0; ) + fp.b->m_nodes[i] = b[i]; + } + + fingerprint* ematch::add_fingerprint(clause& c, binding& b, unsigned max_generation) { + fingerprint fp(c, b, max_generation); + if (m_fingerprints.contains(&fp)) + return nullptr; + set_tmp_binding(fp); + for (unsigned i = c.num_decls(); i-- > 0; ) + fp.b->m_nodes[i] = fp.b->m_nodes[i]->get_root(); + if (m_fingerprints.contains(&fp)) + return nullptr; + fingerprint* f = new (ctx.get_region()) fingerprint(c, b, max_generation); + m_fingerprints.insert(f); + ctx.push(insert_map(m_fingerprints, f)); + return f; } sat::literal ematch::instantiate(clause& c, euf::enode* const* binding, lit const& l) { expr_ref_vector _binding(m); - quantifier* q = c.m_q; + quantifier* q = c.q(); for (unsigned i = 0; i < c.num_decls(); ++i) _binding.push_back(binding[i]->get_expr()); var_subst subst(m); @@ -470,170 +331,30 @@ namespace q { return l.sign ? ~ctx.mk_literal(fml) : ctx.mk_literal(fml); } - lbool ematch::compare(unsigned n, euf::enode* const* binding, expr* s, expr* t) { - if (s == t) - return l_true; - if (m.are_distinct(s, t)) - return l_false; - - euf::enode* sn = eval(n, binding, s); - euf::enode* tn = eval(n, binding, t); - if (sn) sn = sn->get_root(); - if (tn) tn = tn->get_root(); - TRACE("q", tout << mk_pp(s, m) << " ~~ " << mk_pp(t, m) << "\n"; - tout << ctx.bpp(sn) << " " << ctx.bpp(tn) << "\n";); - - lbool c; - if (sn && sn == tn) - return l_true; - if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) - return l_false; - if (sn && tn) - return l_undef; - if (!sn && !tn) - return compare_rec(n, binding, s, t); - if (!tn && sn) { - std::swap(tn, sn); - std::swap(t, s); - } - for (euf::enode* t1 : euf::enode_class(tn)) - if (c = compare_rec(n, binding, s, t1->get_expr()), c != l_undef) - return c; - return l_undef; - } - - // f(p1) = f(p2) if p1 = p2 - // f(p1) != f(p2) if p1 != p2 and f is injective - lbool ematch::compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t) { - if (m.are_equal(s, t)) - return l_true; - if (m.are_distinct(s, t)) - return l_false; - if (!is_app(s) || !is_app(t)) - return l_undef; - if (to_app(s)->get_decl() != to_app(t)->get_decl()) - return l_undef; - if (to_app(s)->get_num_args() != to_app(t)->get_num_args()) - return l_undef; - bool is_injective = to_app(s)->get_decl()->is_injective(); - bool has_undef = false; - for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) { - switch (compare(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i))) { - case l_true: - break; - case l_false: - if (is_injective) - return l_false; - return l_undef; - case l_undef: - if (!is_injective) - return l_undef; - has_undef = true; - break; - } - } - return has_undef ? l_undef : l_true; - } - - euf::enode* ematch::eval(unsigned n, euf::enode* const* binding, expr* e) { - if (is_ground(e)) - return ctx.get_egraph().find(e); - if (m_mark.is_marked(e)) - return m_eval[e->get_id()]; - ptr_buffer todo; - ptr_buffer args; - todo.push_back(e); - while (!todo.empty()) { - expr* t = todo.back(); - SASSERT(!is_ground(t) || ctx.get_egraph().find(t)); - if (is_ground(t)) { - m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); - SASSERT(m_eval[t->get_id()]); - todo.pop_back(); - continue; - } - if (m_mark.is_marked(t)) { - todo.pop_back(); - continue; - } - if (is_var(t)) { - m_mark.mark(t); - m_eval.setx(t->get_id(), binding[n - 1 - to_var(t)->get_idx()], nullptr); - todo.pop_back(); - continue; - } - if (!is_app(t)) - return nullptr; - args.reset(); - for (expr* arg : *to_app(t)) { - if (m_mark.is_marked(arg)) - args.push_back(m_eval[arg->get_id()]); - else - todo.push_back(arg); - } - if (args.size() == to_app(t)->get_num_args()) { - euf::enode* n = ctx.get_egraph().find(t, args.size(), args.c_ptr()); - if (!n) - return nullptr; - m_indirect_nodes.push_back(n); - m_eval.setx(t->get_id(), n, nullptr); - m_mark.mark(t); - todo.pop_back(); - } - } - return m_eval[e->get_id()]; - } - void ematch::insert_to_propagate(unsigned node_id) { m_node_in_queue.assure_domain(node_id); if (m_node_in_queue.contains(node_id)) return; m_node_in_queue.insert(node_id); - for (unsigned idx : m_watch[node_id]) { - m_clause_in_queue.assure_domain(idx); - if (!m_clause_in_queue.contains(idx)) { - m_clause_in_queue.insert(idx); - m_queue.push_back(idx); - } + for (unsigned idx : m_watch[node_id]) + insert_clause_in_queue(idx); + } + + void ematch::insert_clause_in_queue(unsigned idx) { + m_clause_in_queue.assure_domain(idx); + if (!m_clause_in_queue.contains(idx)) { + m_clause_in_queue.insert(idx); + m_clause_queue.push_back(idx); + ctx.push(push_back_vector(m_clause_queue)); } } - bool ematch::propagate() { - m_mam->propagate(); - if (m_qhead >= m_queue.size()) - return false; - bool propagated = false; - ctx.push(value_trail(m_qhead)); - ptr_buffer to_remove; - for (; m_qhead < m_queue.size(); ++m_qhead) { - unsigned idx = m_queue[m_qhead]; - clause& c = *m_clauses[idx]; - binding* b = c.m_bindings; - if (!b) - continue; - do { - if (propagate(b->m_nodes, c)) - to_remove.push_back(b); - b = b->next(); - } - while (b != c.m_bindings); - - for (binding* b : to_remove) { - binding::remove_from(c.m_bindings, b); - ctx.push(insert_binding(c, b)); - } - to_remove.reset(); - } - m_clause_in_queue.reset(); - m_node_in_queue.reset(); - return propagated; - } /** * basic clausifier, assumes q has been normalized. */ - ematch::clause* ematch::clausify(quantifier* _q) { - clause* cl = alloc(clause, m); + clause* ematch::clausify(quantifier* _q) { + clause* cl = alloc(clause, m, m_clauses.size()); cl->m_literal = ctx.mk_literal(_q); quantifier_ref q(_q, m); if (is_exists(q)) { @@ -659,13 +380,9 @@ namespace q { q = to_quantifier(tmp); } cl->m_q = q; - unsigned generation = ctx.generation(); -#if 0 - unsigned _generation; - if (!m_cached_generation.empty() && m_cached_generation.find(q, _generation)) { - generation = _generation; - } -#endif + SASSERT(is_forall(q)); + euf::enode* nq = ctx.get_egraph().find(_q); + unsigned generation = nq ? nq->generation() : ctx.generation(); cl->m_stat = m_qstat_gen(_q, generation); SASSERT(ctx.s().value(cl->m_literal) == l_true); return cl; @@ -689,21 +406,21 @@ namespace q { ematch& em; pop_clause(ematch& em): em(em) {} void undo(euf::solver& ctx) override { - em.m_q2clauses.remove(em.m_clauses.back()->m_q); + em.m_q2clauses.remove(em.m_clauses.back()->q()); dealloc(em.m_clauses.back()); em.m_clauses.pop_back(); } }; - void ematch::add(quantifier* q) { - TRACE("q", tout << "add " << mk_pp(q, m) << "\n";); - clause* c = clausify(q); + void ematch::add(quantifier* _q) { + TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";); + clause* c = clausify(_q); + quantifier* q = c->q(); ensure_ground_enodes(*c); - unsigned idx = m_clauses.size(); m_clauses.push_back(c); - m_q2clauses.insert(q, idx); + m_q2clauses.insert(q, c->index()); ctx.push(pop_clause(*this)); - init_watch(*c, idx); + init_watch(*c); bool has_unary_pattern = false; unsigned num_patterns = q->get_num_patterns(); @@ -733,38 +450,72 @@ namespace q { } } + + bool ematch::propagate(bool flush) { + m_mam->propagate(); + bool propagated = false; + if (m_qhead >= m_clause_queue.size()) + return m_inst_queue.propagate(); + ctx.push(value_trail(m_qhead)); + ptr_buffer to_remove; + for (; m_qhead < m_clause_queue.size(); ++m_qhead) { + unsigned idx = m_clause_queue[m_qhead]; + clause& c = *m_clauses[idx]; + binding* b = c.m_bindings; + if (!b) + continue; + + do { + if (propagate(b->m_nodes, b->m_max_generation, c)) { + to_remove.push_back(b); + propagated = true; + } + else if (flush) { + instantiate(*b, c); + to_remove.push_back(b); + } + b = b->next(); + } + while (b != c.m_bindings); + + for (auto* b : to_remove) { + binding::remove_from(c.m_bindings, b); + ctx.push(insert_binding(c, b)); + } + to_remove.reset(); + } + m_clause_in_queue.reset(); + m_node_in_queue.reset(); + if (m_inst_queue.propagate()) + propagated = true; + return propagated; + } + bool ematch::operator()() { TRACE("q", m_mam->display(tout);); - if (propagate()) + if (propagate(false)) return true; if (m_lazy_mam) { m_lazy_mam->propagate(); - if (propagate()) + if (propagate(false)) return true; } - - // - // loop over pending bindings and instantiate them - // - bool instantiated = false; - for (auto* c : m_clauses) { - binding* b = c->m_bindings; - if (!b) - continue; - instantiated = true; - do { - instantiate(*b, *c); - b = b->next(); - } - while (b != c->m_bindings); - - while (b = c->m_bindings) { - binding::remove_from(c->m_bindings, b); - ctx.push(insert_binding(*c, b)); - } + unsigned idx = 0; + for (clause* c : m_clauses) { + if (c->m_bindings) + insert_clause_in_queue(idx); + idx++; } - TRACE("q", ctx.display(tout << "instantiated: " << instantiated << "\n");); - return instantiated; + if (propagate(true)) + return true; + return m_inst_queue.lazy_propagate(); + } + + void ematch::collect_statistics(statistics& st) const { + m_inst_queue.collect_statistics(st); + st.update("q redundant", m_stats.m_num_redundant); + st.update("q units", m_stats.m_num_propagations); + st.update("q conflicts", m_stats.m_num_conflicts); } std::ostream& ematch::display(std::ostream& out) const { diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index 46e897477..e3db84d4e 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -17,12 +17,15 @@ Author: #pragma once #include "util/nat_set.h" -#include "util/dlist.h" #include "ast/quantifier_stat.h" #include "ast/pattern/pattern_inference.h" #include "solver/solver.h" #include "sat/smt/sat_th.h" #include "sat/smt/q_mam.h" +#include "sat/smt/q_clause.h" +#include "sat/smt/q_fingerprint.h" +#include "sat/smt/q_queue.h" +#include "sat/smt/q_eval.h" namespace euf { class solver; @@ -35,6 +38,9 @@ namespace q { class ematch { struct stats { unsigned m_num_instantiations; + unsigned m_num_propagations; + unsigned m_num_conflicts; + unsigned m_num_redundant; stats() { reset(); } @@ -43,95 +49,27 @@ namespace q { } }; - - struct lit { - expr_ref lhs; - expr_ref rhs; - bool sign; - lit(expr_ref const& lhs, expr_ref const& rhs, bool sign): - lhs(lhs), rhs(rhs), sign(sign) {} - std::ostream& display(std::ostream& out) const; - }; - struct remove_binding; struct insert_binding; - struct binding : public dll_base { - unsigned m_max_generation; - unsigned m_min_top_generation; - unsigned m_max_top_generation; - euf::enode* m_nodes[0]; - - binding(unsigned max_generation, unsigned min_top, unsigned max_top): - m_max_generation(max_generation), - m_min_top_generation(min_top), - m_max_top_generation(max_top) {} - - euf::enode* const* nodes() { return m_nodes; } - - }; - - binding* alloc_binding(unsigned n, unsigned max_generation, unsigned min_top, unsigned max_top); + binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top); + void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top); - struct clause { - vector m_lits; - quantifier_ref m_q; - sat::literal m_literal; - q::quantifier_stat* m_stat { nullptr }; - binding* m_bindings { nullptr }; - - clause(ast_manager& m): m_q(m) {} - - void add_binding(ematch& em, euf::enode* const* b, unsigned max_generation, unsigned min_top, unsigned max_top); - std::ostream& display(euf::solver& ctx, std::ostream& out) const; - lit const& operator[](unsigned i) const { return m_lits[i]; } - lit& operator[](unsigned i) { return m_lits[i]; } - unsigned size() const { return m_lits.size(); } - unsigned num_decls() const { return m_q->get_num_decls(); } - }; - - struct fingerprint { - clause& c; - binding& b; - unsigned max_generation; - fingerprint(clause& c, binding& b, unsigned max_generation): - c(c), b(b), max_generation(max_generation) {} - unsigned hash() const; - bool eq(fingerprint const& other) const; - }; - - struct fingerprint_hash_proc { - bool operator()(fingerprint const* f) const { return f->hash(); } - }; - struct fingerprint_eq_proc { - bool operator()(fingerprint const* a, fingerprint const* b) const { return a->eq(*b); } - }; - typedef ptr_hashtable fingerprints; - - struct justification { - expr* m_lhs, *m_rhs; - bool m_sign; - clause& m_clause; - euf::enode* const* m_binding; - justification(lit const& l, clause& c, euf::enode* const* b): - m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_clause(c), m_binding(b) {} - sat::ext_constraint_idx to_index() const { - return sat::constraint_base::mem2base(this); - } - static justification& from_index(size_t idx) { - return *reinterpret_cast(sat::constraint_base::from_index(idx)->mem()); - } - static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(justification)); } - }; sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b); struct pop_clause; + struct scoped_mark_reset; + euf::solver& ctx; solver& m_qs; ast_manager& m; - q::quantifier_stat_gen m_qstat_gen; + eval m_eval; + quantifier_stat_gen m_qstat_gen; fingerprints m_fingerprints; + scoped_ptr m_tmp_binding; + unsigned m_tmp_binding_capacity { 0 }; + queue m_inst_queue; pattern_inference_rw m_infer_patterns; scoped_ptr m_mam, m_lazy_mam; ptr_vector m_clauses; @@ -139,47 +77,35 @@ namespace q { vector m_watch; // expr_id -> clause-index* stats m_stats; expr_fast_mark1 m_mark; + unsigned m_generation_propagation_threshold{ 3 }; - struct scoped_mark_reset; nat_set m_node_in_queue; nat_set m_clause_in_queue; unsigned m_qhead { 0 }; - unsigned_vector m_queue; + unsigned_vector m_clause_queue; ptr_vector m_ground; void ensure_ground_enodes(expr* e); void ensure_ground_enodes(clause const& c); - // compare s, t modulo sign under binding - lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t); - lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t); - euf::enode_vector m_eval, m_indirect_nodes; - euf::enode* eval(unsigned n, euf::enode* const* binding, expr* e); - - bool propagate(euf::enode* const* binding, clause& c); void instantiate(binding& b, clause& c); sat::literal instantiate(clause& c, euf::enode* const* binding, lit const& l); // register as callback into egraph. void on_merge(euf::enode* root, euf::enode* other); void insert_to_propagate(unsigned node_id); + void insert_clause_in_queue(unsigned idx); void add_watch(euf::enode* root, unsigned clause_idx); void init_watch(expr* e, unsigned clause_idx); - void init_watch(clause& c, unsigned idx); - - // extract explanation - ptr_vector m_explain; - void explain(clause& c, unsigned literal_idx, euf::enode* const* binding); - void explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t); - void explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t); + void init_watch(clause& c); void attach_ground_pattern_terms(expr* pat); clause* clausify(quantifier* q); fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation); - + void set_tmp_binding(fingerprint& fp); public: @@ -187,7 +113,7 @@ namespace q { bool operator()(); - bool propagate(); + bool propagate(bool flush); void init_search(); @@ -200,6 +126,11 @@ namespace q { // callback from mam void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen); + // callback from queue + lbool eval(euf::enode* const* binding, clause& c) { return m_eval(binding, c); } + void add_instantiation(clause& c, binding& b, sat::literal lit); + bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c); + std::ostream& display(std::ostream& out) const; std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const; diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp new file mode 100644 index 000000000..d25e2cb92 --- /dev/null +++ b/src/sat/smt/q_eval.cpp @@ -0,0 +1,293 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_eval.cpp + +Abstract: + + Evaluation of clauses + +Author: + + Nikolaj Bjorner (nbjorner) 2021-01-24 + +--*/ +#pragma once + +#include "sat/smt/q_eval.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/q_solver.h" + +namespace q { + + struct eval::scoped_mark_reset { + eval& e; + scoped_mark_reset(eval& e): e(e) {} + ~scoped_mark_reset() { e.m_mark.reset(); } + }; + + eval::eval(euf::solver& ctx): + ctx(ctx), + m(ctx.get_manager()) + {} + + lbool eval::operator()(euf::enode* const* binding, clause& c, unsigned& idx) { + scoped_mark_reset _sr(*this); + idx = UINT_MAX; + unsigned sz = c.m_lits.size(); + unsigned n = c.num_decls(); + m_indirect_nodes.reset(); + for (unsigned i = 0; i < sz; ++i) { + unsigned lim = m_indirect_nodes.size(); + lit l = c[i]; + lbool cmp = compare(n, binding, l.lhs, l.rhs); + switch (cmp) { + case l_false: + m_indirect_nodes.shrink(lim); + if (!l.sign) + break; + if (i > 0) + std::swap(c[0], c[i]); + return l_true; + case l_true: + m_indirect_nodes.shrink(lim); + if (l.sign) + break; + if (i > 0) + std::swap(c[0], c[i]); + return l_true; + case l_undef: + TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";); + if (idx == 0) { + idx = UINT_MAX; + return l_undef; + } + if (i > 0) + std::swap(c[0], c[i]); + idx = 0; + break; + } + } + if (idx == UINT_MAX) + return l_false; + + return l_undef; + } + + lbool eval::operator()(euf::enode* const* binding, clause& c) { + unsigned idx = 0; + return (*this)(binding, c, idx); + } + + lbool eval::compare(unsigned n, euf::enode* const* binding, expr* s, expr* t) { + if (s == t) + return l_true; + if (m.are_distinct(s, t)) + return l_false; + + euf::enode* sn = (*this)(n, binding, s); + euf::enode* tn = (*this)(n, binding, t); + if (sn) sn = sn->get_root(); + if (tn) tn = tn->get_root(); + TRACE("q", tout << mk_pp(s, m) << " ~~ " << mk_pp(t, m) << "\n"; + tout << ctx.bpp(sn) << " " << ctx.bpp(tn) << "\n";); + + lbool c; + if (sn && sn == tn) + return l_true; + if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) + return l_false; + if (sn && tn) + return l_undef; + if (!sn && !tn) + return compare_rec(n, binding, s, t); + if (!tn && sn) { + std::swap(tn, sn); + std::swap(t, s); + } + for (euf::enode* t1 : euf::enode_class(tn)) + if (c = compare_rec(n, binding, s, t1->get_expr()), c != l_undef) + return c; + return l_undef; + } + + // f(p1) = f(p2) if p1 = p2 + // f(p1) != f(p2) if p1 != p2 and f is injective + lbool eval::compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t) { + if (m.are_equal(s, t)) + return l_true; + if (m.are_distinct(s, t)) + return l_false; + if (!is_app(s) || !is_app(t)) + return l_undef; + if (to_app(s)->get_decl() != to_app(t)->get_decl()) + return l_undef; + if (to_app(s)->get_num_args() != to_app(t)->get_num_args()) + return l_undef; + bool is_injective = to_app(s)->get_decl()->is_injective(); + bool has_undef = false; + for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) { + switch (compare(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i))) { + case l_true: + break; + case l_false: + if (is_injective) + return l_false; + return l_undef; + case l_undef: + if (!is_injective) + return l_undef; + has_undef = true; + break; + } + } + return has_undef ? l_undef : l_true; + } + + euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e) { + if (is_ground(e)) + return ctx.get_egraph().find(e); + if (m_mark.is_marked(e)) + return m_eval[e->get_id()]; + ptr_buffer todo; + ptr_buffer args; + todo.push_back(e); + while (!todo.empty()) { + expr* t = todo.back(); + SASSERT(!is_ground(t) || ctx.get_egraph().find(t)); + if (is_ground(t)) { + m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); + SASSERT(m_eval[t->get_id()]); + todo.pop_back(); + continue; + } + if (m_mark.is_marked(t)) { + todo.pop_back(); + continue; + } + if (is_var(t)) { + m_mark.mark(t); + m_eval.setx(t->get_id(), binding[n - 1 - to_var(t)->get_idx()], nullptr); + todo.pop_back(); + continue; + } + if (!is_app(t)) + return nullptr; + args.reset(); + for (expr* arg : *to_app(t)) { + if (m_mark.is_marked(arg)) + args.push_back(m_eval[arg->get_id()]); + else + todo.push_back(arg); + } + if (args.size() == to_app(t)->get_num_args()) { + euf::enode* n = ctx.get_egraph().find(t, args.size(), args.c_ptr()); + if (!n) + return nullptr; + m_indirect_nodes.push_back(n); + m_eval.setx(t->get_id(), n, nullptr); + m_mark.mark(t); + todo.pop_back(); + } + } + return m_eval[e->get_id()]; + } + + void eval::explain(clause& c, unsigned literal_idx, euf::enode* const* b) { + unsigned n = c.num_decls(); + for (unsigned i = c.size(); i-- > 0; ) { + if (i == literal_idx) + continue; + auto const& lit = c[i]; + if (lit.sign) + explain_eq(n, b, lit.lhs, lit.rhs); + else + explain_diseq(n, b, lit.lhs, lit.rhs); + } + } + + void eval::explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t) { + SASSERT(l_true == compare(n, binding, s, t)); + if (s == t) + return; + euf::enode* sn = (*this)(n, binding, s); + euf::enode* tn = (*this)(n, binding, t); + if (sn && tn) { + SASSERT(sn->get_root() == tn->get_root()); + ctx.add_antecedent(sn, tn); + return; + } + if (!sn && tn) { + std::swap(sn, tn); + std::swap(s, t); + } + if (sn && !tn) { + for (euf::enode* s1 : euf::enode_class(sn)) { + if (l_true == compare_rec(n, binding, t, s1->get_expr())) { + ctx.add_antecedent(sn, s1); + explain_eq(n, binding, t, s1->get_expr()); + return; + } + } + UNREACHABLE(); + } + SASSERT(is_app(s) && is_app(t)); + SASSERT(to_app(s)->get_decl() == to_app(t)->get_decl()); + for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) + explain_eq(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i)); + } + + void eval::explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t) { + SASSERT(l_false == compare(n, binding, s, t)); + if (m.are_distinct(s, t)) + return; + euf::enode* sn = (*this)(n, binding, s); + euf::enode* tn = (*this)(n, binding, t); + if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) { + ctx.add_diseq_antecedent(sn, tn); + return; + } + if (!sn && tn) { + std::swap(sn, tn); + std::swap(s, t); + } + if (sn && !tn) { + for (euf::enode* s1 : euf::enode_class(sn)) { + if (l_false == compare_rec(n, binding, t, s1->get_expr())) { + ctx.add_antecedent(sn, s1); + explain_diseq(n, binding, t, s1->get_expr()); + return; + } + } + UNREACHABLE(); + } + SASSERT(is_app(s) && is_app(t)); + app* at = to_app(t); + app* as = to_app(s); + SASSERT(as->get_decl() == at->get_decl()); + for (unsigned i = as->get_num_args(); i-- > 0; ) { + if (l_false == compare_rec(n, binding, as->get_arg(i), at->get_arg(i))) { + explain_eq(n, binding, as->get_arg(i), at->get_arg(i)); + return; + } + } + UNREACHABLE(); + } + + + void eval::explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing) { + unsigned l_idx = 0; + clause& c = j.m_clause; + for (; l_idx < c.size(); ++l_idx) { + if (c[l_idx].lhs == j.m_lhs && c[l_idx].rhs == j.m_rhs && c[l_idx].sign == j.m_sign) + break; + } + explain(c, l_idx, j.m_binding); + r.push_back(c.m_literal); + (void)probing; // ignored + } + + +} diff --git a/src/sat/smt/q_eval.h b/src/sat/smt/q_eval.h new file mode 100644 index 000000000..6219c473a --- /dev/null +++ b/src/sat/smt/q_eval.h @@ -0,0 +1,55 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_eval.h + +Abstract: + + Evaluation of clauses + +Author: + + Nikolaj Bjorner (nbjorner) 2021-01-24 + +--*/ +#pragma once + +#include "sat/smt/q_clause.h" + +namespace euf { + class solver; +} + +namespace q { + + class eval { + euf::solver& ctx; + ast_manager& m; + expr_fast_mark1 m_mark; + euf::enode_vector m_eval; + euf::enode_vector m_indirect_nodes; + ptr_vector m_explain; + + struct scoped_mark_reset; + + void explain(clause& c, unsigned literal_idx, euf::enode* const* binding); + void explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t); + void explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t); + + // compare s, t modulo binding + lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t); + lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t); + + public: + eval(euf::solver& ctx); + void explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing); + + lbool operator()(euf::enode* const* binding, clause& c); + lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx); + euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e); + + euf::enode_vector const& get_watch() { return m_indirect_nodes; } + }; +} diff --git a/src/sat/smt/q_fingerprint.h b/src/sat/smt/q_fingerprint.h new file mode 100644 index 000000000..99ad602b9 --- /dev/null +++ b/src/sat/smt/q_fingerprint.h @@ -0,0 +1,77 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_fingerprint.h + +Abstract: + + Fingerprint summary of a quantifier instantiation + +Author: + + Nikolaj Bjorner (nbjorner) 2021-01-24 + +--*/ +#pragma once + +#include "util/hashtable.h" +#include "ast/ast.h" +#include "ast/quantifier_stat.h" +#include "ast/euf/euf_enode.h" +#include "sat/smt/q_clause.h" + + +namespace q { + + struct fingerprint { + clause* c; + binding* b; + unsigned m_max_generation; + + unsigned size() const { return c->num_decls(); } + euf::enode* const* nodes() const { return b->nodes(); } + quantifier* q() const { return c->m_q; } + + fingerprint(clause& _c, binding& _b, unsigned mg) : + c(&_c), b(&_b), m_max_generation(mg) {} + + bool eq(fingerprint const& other) const { + if (c->m_q != other.c->m_q) + return false; + for (unsigned i = size(); i--> 0; ) + if ((*b)[i] != (*other.b)[i]) + return false; + return true; + } + }; + + struct fingerprint_khasher { + unsigned operator()(fingerprint const * f) const { return f->c->m_q->get_id(); } + }; + + struct fingerprint_chasher { + unsigned operator()(fingerprint const * f, unsigned idx) const { return f->b->m_nodes[idx]->hash(); } + }; + + struct fingerprint_hash_proc { + unsigned operator()(fingerprint const * f) const { + return get_composite_hash(const_cast(f), f->size()); + } + }; + + struct fingerprint_eq_proc { + bool operator()(fingerprint const* a, fingerprint const* b) const { return a->eq(*b); } + }; + + typedef ptr_hashtable fingerprints; + + inline std::ostream& operator<<(std::ostream& out, fingerprint const& f) { + out << "[fp " << f.q()->get_id() << ":"; + for (unsigned i = 0; i < f.size(); ++i) + out << " " << (*f.b)[i]->get_expr_id(); + return out << "]"; + } + +} diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 680fc7d23..efc5fa6f9 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -1843,7 +1843,7 @@ namespace q { typedef svector backtrack_stack; class interpreter { - egraph & m_egraph; + euf::solver& ctx; ast_manager & m; mam & m_mam; bool m_use_filters; @@ -1976,8 +1976,8 @@ namespace q { #define INIT_ARGS_SIZE 16 public: - interpreter(egraph & ctx, mam & ma, bool use_filters): - m_egraph(ctx), + interpreter(euf::solver& ctx, mam & ma, bool use_filters): + ctx(ctx), m(ctx.get_manager()), m_mam(ma), m_use_filters(use_filters) { @@ -2002,7 +2002,7 @@ namespace q { for (enode* app : t->get_candidates()) { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";); if (!app->is_marked1() && app->is_cgr()) { - if (m_egraph.resource_limits_exceeded() || !execute_core(t, app)) + if (ctx.resource_limits_exceeded() || !execute_core(t, app)) return; app->mark1(); } @@ -2017,7 +2017,7 @@ namespace q { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";); if (app->is_cgr()) { TRACE("trigger_bug", tout << "is_cgr\n";); - if (m_egraph.resource_limits_exceeded() || !execute_core(t, app)) + if (ctx.resource_limits_exceeded() || !execute_core(t, app)) return; } } @@ -2059,7 +2059,7 @@ namespace q { for (enode* p : euf::enode_parents(n)) { if (p->get_decl() == f && i < p->num_args() && - m_egraph.is_relevant(p) && + ctx.is_relevant(p) && p->is_cgr() && p->get_arg(i)->get_root() == n) v->push_back(p); @@ -2080,7 +2080,7 @@ namespace q { enode_vector * v = mk_enode_vector(); for (enode* p : euf::enode_parents(n)) { if (p->get_decl() == j2->m_decl && - m_egraph.is_relevant(p) && + ctx.is_relevant(p) && p->num_args() > j2->m_arg_pos && p->is_cgr() && p->get_arg(j2->m_arg_pos)->get_root() == n) { @@ -2090,7 +2090,7 @@ namespace q { if (p2->get_decl() == f && num_args == n->num_args() && num_args == p2->num_args() && - m_egraph.is_relevant(p2) && + ctx.is_relevant(p2) && p2->is_cgr() && i < num_args && p2->get_arg(i)->get_root() == p) { @@ -2104,7 +2104,7 @@ namespace q { enode * interpreter::init_continue(cont const * c, unsigned expected_num_args) { func_decl * lbl = c->m_label; - unsigned min_sz = m_egraph.enodes_of(lbl).size(); + unsigned min_sz = ctx.get_egraph().enodes_of(lbl).size(); unsigned short num_args = c->m_num_args; enode * r; // quick filter... check if any of the joint points have zero parents... @@ -2172,8 +2172,8 @@ namespace q { TRACE("mam_bug", tout << "m_top: " << m_top << ", m_backtrack_stack.size(): " << m_backtrack_stack.size() << "\n"; tout << *c << "\n";); bp.m_to_recycle = nullptr; - bp.m_it = m_egraph.enodes_of(lbl).begin(); - bp.m_end = m_egraph.enodes_of(lbl).end(); + bp.m_it = ctx.get_egraph().enodes_of(lbl).begin(); + bp.m_end = ctx.get_egraph().enodes_of(lbl).end(); } else { SASSERT(!best_v->empty()); @@ -2184,7 +2184,7 @@ namespace q { // find application with the right number of arguments for (; bp.m_it != bp.m_end; ++bp.m_it) { enode * curr = *bp.m_it; - if (curr->num_args() == expected_num_args && m_egraph.is_relevant(curr)) + if (curr->num_args() == expected_num_args && ctx.is_relevant(curr)) break; } if (bp.m_it == bp.m_end) @@ -2262,7 +2262,7 @@ namespace q { #endif // It doesn't make sense to process an irrelevant enode. TRACE("mam_execute_core", tout << "EXEC " << t->get_root_lbl()->get_name() << "\n";); - SASSERT(m_egraph.is_relevant(n)); + SASSERT(ctx.is_relevant(n)); m_pattern_instances.reset(); m_min_top_generation.reset(); m_max_top_generation.reset(); @@ -2623,8 +2623,8 @@ namespace q { goto backtrack; cgr_common: - m_n1 = m_egraph.get_enode_eq_to(static_cast(m_pc)->m_label, static_cast(m_pc)->m_num_args, m_args.c_ptr()); - if (!m_n1 || !m_egraph.is_relevant(m_n1)) + m_n1 = ctx.get_egraph().get_enode_eq_to(static_cast(m_pc)->m_label, static_cast(m_pc)->m_num_args, m_args.c_ptr()); + if (!m_n1 || !ctx.is_relevant(m_n1)) goto backtrack; update_max_generation(m_n1, nullptr); m_registers[static_cast(m_pc)->m_oreg] = m_n1; @@ -2652,7 +2652,7 @@ namespace q { if (since_last_check++ > 100) { since_last_check = 0; - if (m_egraph.resource_limits_exceeded()) { + if (ctx.resource_limits_exceeded()) { // Soft timeout... // Cleanup before exiting while (m_top != 0) { @@ -2752,8 +2752,8 @@ namespace q { const cont * c = static_cast(bp.m_instr); // bp.m_it may reference an enode in [begin_enodes_of(lbl), end_enodes_of(lbl)) // This enodes are not necessarily relevant. - // So, we must check whether m_egraph.is_relevant(m_app) is true or not. - if (m_app->num_args() == c->m_num_args && m_egraph.is_relevant(m_app)) { + // So, we must check whether ctx.is_relevant(m_app) is true or not. + if (m_app->num_args() == c->m_num_args && ctx.is_relevant(m_app)) { // update the pattern instance SASSERT(!m_pattern_instances.empty()); if (m_pattern_instances.size() == m_max_top_generation.size()) { @@ -3143,7 +3143,7 @@ namespace q { SASSERT(m_is_clbl[lbl_id]); unsigned h = m_lbl_hasher(lbl); for (enode* app : m_egraph.enodes_of(lbl)) { - if (m_egraph.is_relevant(app)) { + if (ctx.is_relevant(app)) { update_lbls(app, h); TRACE("mam_bug", tout << "updating labels of: #" << app->get_expr_id() << "\n"; tout << "new_elem: " << h << "\n"; @@ -3185,7 +3185,7 @@ namespace q { SASSERT(is_plbl(lbl)); unsigned h = m_lbl_hasher(lbl); for (enode * app : m_egraph.enodes_of(lbl)) { - if (m_egraph.is_relevant(app)) + if (ctx.is_relevant(app)) update_children_plbls(app, h); } } @@ -3397,7 +3397,7 @@ namespace q { tout << "updating pc labels " << plbl->get_name() << " " << static_cast(n->get_lbl_hash()) << "\n"; tout << "#" << n->get_expr_id() << " " << n->get_root()->get_lbls() << "\n"; - tout << "relevant: " << m_egraph.is_relevant(n) << "\n";); + tout << "relevant: " << ctx.is_relevant(n) << "\n";); update_pc(m_lbl_hasher(plbl), n->get_lbl_hash(), new_path, qa, mp); continue; } @@ -3553,7 +3553,7 @@ namespace q { if (filter.may_contain(m_lbl_hasher(lbl)) && !curr_parent->is_marked1() && (curr_parent_cg == curr_parent || !is_eq(curr_parent_cg, curr_parent_root)) && - m_egraph.is_relevant(curr_parent) + ctx.is_relevant(curr_parent) ) { path_tree * curr_tree = t; while (curr_tree) { @@ -3711,7 +3711,7 @@ namespace q { SASSERT(!m_egraph.enodes_of(lbl).empty()); m_interpreter.init(tmp_tree); for (enode * app : m_egraph.enodes_of(lbl)) - if (m_egraph.is_relevant(app)) + if (ctx.is_relevant(app)) m_interpreter.execute_core(tmp_tree, app); m_tmp_trees[lbl_id] = nullptr; dealloc(tmp_tree); @@ -3728,7 +3728,7 @@ namespace q { m_use_filters(use_filters), m_ct_manager(m_lbl_hasher, ctx), m_compiler(m_egraph, m_ct_manager, m_lbl_hasher, use_filters), - m_interpreter(m_egraph, *this, use_filters), + m_interpreter(ctx, *this, use_filters), m_trees(m, m_compiler, ctx), m_region(ctx.get_region()) { DEBUG_CODE(m_trees.set_egraph(&m_egraph);); @@ -3802,7 +3802,7 @@ namespace q { m_interpreter.init(t); func_decl * lbl = t->get_root_lbl(); for (enode * curr : m_egraph.enodes_of(lbl)) { - if (use_irrelevant || m_egraph.is_relevant(curr)) + if (use_irrelevant || ctx.is_relevant(curr)) m_interpreter.execute_core(t, curr); } } diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp new file mode 100644 index 000000000..68a81a20d --- /dev/null +++ b/src/sat/smt/q_queue.cpp @@ -0,0 +1,256 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_queue.cpp + +Abstract: + + Instantiation queue for quantifiers + + Based on smt/qi_queue + +Author: + + Nikolaj Bjorner (nbjorner) 2021-01-24 + +--*/ + +#include "sat/smt/euf_solver.h" +#include "sat/smt/q_queue.h" +#include "sat/smt/q_ematch.h" + + +namespace q { + + queue::queue(ematch& em, euf::solver& ctx): + em(em), + ctx(ctx), + m(ctx.get_manager()), + m_params(ctx.get_config()), + m_cost_function(m), + m_new_gen_function(m), + m_parser(m), + m_evaluator(m), + m_subst(m) + {} + + void queue::setup() { + TRACE("q", tout << "qi_cost: " << m_params.m_qi_cost << "\n";); + if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) { + warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str()); + VERIFY(m_parser.parse_string("(+ weight generation)", m_cost_function)); + } + if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function)) { + warning_msg("invalid new_gen function '%s', switching to default one", m_params.m_qi_new_gen.c_str()); + VERIFY(m_parser.parse_string("cost", m_new_gen_function)); + } + m_eager_cost_threshold = m_params.m_qi_eager_threshold; + } + + void queue::init_parser_vars() { +#define COST 14 + m_parser.add_var("cost"); +#define MIN_TOP_GENERATION 13 + m_parser.add_var("min_top_generation"); +#define MAX_TOP_GENERATION 12 + m_parser.add_var("max_top_generation"); +#define INSTANCES 11 + m_parser.add_var("instances"); +#define SIZE 10 + m_parser.add_var("size"); +#define DEPTH 9 + m_parser.add_var("depth"); +#define GENERATION 8 + m_parser.add_var("generation"); +#define QUANT_GENERATION 7 + m_parser.add_var("quant_generation"); +#define WEIGHT 6 + m_parser.add_var("weight"); +#define VARS 5 + m_parser.add_var("vars"); +#define PATTERN_WIDTH 4 + m_parser.add_var("pattern_width"); +#define TOTAL_INSTANCES 3 + m_parser.add_var("total_instances"); +#define SCOPE 2 + m_parser.add_var("scope"); +#define NESTED_QUANTIFIERS 1 + m_parser.add_var("nested_quantifiers"); +#define CS_FACTOR 0 + m_parser.add_var("cs_factor"); + } + + void queue::set_values(fingerprint& f, float cost) { + quantifier_stat * stat = f.c->m_stat; + quantifier* q = f.q(); + app* pat = f.b->m_pattern; + unsigned min_top_generation = f.b->m_min_top_generation; + unsigned max_top_generation = f.b->m_max_top_generation; + m_vals[COST] = cost; + m_vals[MIN_TOP_GENERATION] = static_cast(min_top_generation); + m_vals[MAX_TOP_GENERATION] = static_cast(max_top_generation); + m_vals[INSTANCES] = static_cast(stat->get_num_instances_curr_branch()); + m_vals[SIZE] = static_cast(stat->get_size()); + m_vals[DEPTH] = static_cast(stat->get_depth()); + m_vals[GENERATION] = static_cast(f.m_max_generation); + m_vals[QUANT_GENERATION] = static_cast(stat->get_generation()); + m_vals[WEIGHT] = static_cast(q->get_weight()); + m_vals[VARS] = static_cast(q->get_num_decls()); + m_vals[PATTERN_WIDTH] = pat ? static_cast(pat->get_num_args()) : 1.0f; + m_vals[TOTAL_INSTANCES] = static_cast(stat->get_num_instances_curr_search()); + m_vals[SCOPE] = static_cast(ctx.s().num_scopes()); + m_vals[NESTED_QUANTIFIERS] = static_cast(stat->get_num_nested_quantifiers()); + m_vals[CS_FACTOR] = static_cast(stat->get_case_split_factor()); + TRACE("q_detail", for (unsigned i = 0; i < m_vals.size(); i++) { tout << m_vals[i] << " "; } tout << "\n";); + } + + float queue::get_cost(fingerprint& f) { + set_values(f, 0); + float r = m_evaluator(m_cost_function, m_vals.size(), m_vals.c_ptr()); + f.c->m_stat->update_max_cost(r); + return r; + } + + unsigned queue::get_new_gen(fingerprint& f, float cost) { + set_values(f, cost); + float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr()); + return std::max(f.m_max_generation + 1, static_cast(r)); + } + + struct queue::reset_new_entries : public trail { + svector& m_entries; + reset_new_entries(svector& e): m_entries(e) {} + void undo(euf::solver& ctx) override { + m_entries.reset(); + } + }; + + void queue::insert(fingerprint* f) { + float cost = get_cost(*f); + if (m_new_entries.empty()) + ctx.push(reset_new_entries(m_new_entries)); + m_new_entries.push_back(entry(f, cost)); + } + + void queue::instantiate(entry& ent) { + fingerprint & f = *ent.m_qb; + quantifier * q = f.q(); + unsigned generation = f.m_max_generation; + unsigned num_bindings = f.size(); + euf::enode * const * bindings = f.nodes(); + q::quantifier_stat * stat = f.c->m_stat; + + ent.m_instantiated = true; + + unsigned gen = get_new_gen(f, ent.m_cost); + if (em.propagate(bindings, gen, *f.c)) + return; + + auto* ebindings = m_subst(q, num_bindings); + for (unsigned i = 0; i < num_bindings; ++i) + ebindings[i] = bindings[i]->get_expr(); + expr_ref instance = m_subst(); + ctx.get_rewriter()(instance); + if (m.is_true(instance)) { + stat->inc_num_instances_simplify_true(); + return; + } + stat->inc_num_instances(); + + m_stats.m_num_instances++; + + euf::solver::scoped_generation _sg(ctx, gen); + sat::literal result_l = ctx.mk_literal(instance); + em.add_instantiation(*f.c, *f.b, result_l); + } + + bool queue::propagate() { + if (m_new_entries.empty()) + return false; + unsigned since_last_check = 0; + for (entry & curr : m_new_entries) { + since_last_check = (1 + since_last_check) & 0xFF; + if (!m.inc()) + break; + if (0 == since_last_check && ctx.resource_limits_exceeded()) + break; + + fingerprint& f = *curr.m_qb; + + if (curr.m_cost <= m_eager_cost_threshold) + instantiate(curr); + else if (m_params.m_qi_promote_unsat && l_false == em.eval(f.nodes(), *f.c)) { + // do not delay instances that produce a conflict. + TRACE("q", tout << "promoting instance that produces a conflict\n" << mk_pp(f.q(), m) << "\n";); + instantiate(curr); + } + else { + TRACE("q", tout << "delaying quantifier instantiation... " << f << "\n" << mk_pp(f.q(), m) << "\ncost: " << curr.m_cost << "\n";); + m_delayed_entries.push_back(curr); + ctx.push(push_back_vector>(m_delayed_entries)); + } + } + m_new_entries.reset(); + return true; + } + + struct queue::reset_instantiated : public trail { + queue& q; + unsigned idx; + reset_instantiated(queue& q, unsigned idx): q(q), idx(idx) {} + void undo(euf::solver& ctx) override { + q.m_delayed_entries[idx].m_instantiated = false; + } + }; + + bool queue::lazy_propagate() { + if (m_delayed_entries.empty()) + return false; + + double cost_limit = m_params.m_qi_lazy_threshold; + if (m_params.m_qi_conservative_final_check) { + bool init = false; + cost_limit = 0.0; + for (entry & e : m_delayed_entries) { + TRACE("q", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold && (!init || e.m_cost < cost_limit)) { + init = true; + cost_limit = e.m_cost; + } + } + } + bool instantiated = false; + unsigned idx = 0; + for (entry & e : m_delayed_entries) { + if (!e.m_instantiated && e.m_cost <= cost_limit) { + instantiated = true; + ctx.push(reset_instantiated(*this, idx)); + m_stats.m_num_lazy_instances++; + instantiate(e); + } + ++idx; + } + return instantiated; + } + + void queue::collect_statistics(::statistics & st) const { + float fmin = 0.0f, fmax = 0.0f; + bool found = false; + for (auto const& e : m_delayed_entries) { + if (!e.m_instantiated) { + if (found) + fmin = std::min(fmin, e.m_cost), fmax = std::max(fmax, e.m_cost); + else + fmin = e.m_cost, fmax = e.m_cost, found = true; + } + } + st.update("q instantiations", m_stats.m_num_instances); + st.update("q lazy instantiations", m_stats.m_num_lazy_instances); + st.update("q missed instantiations", m_delayed_entries.size()); + st.update("q min missed cost", fmin); + st.update("q max missed cost", fmax); + } + +} diff --git a/src/sat/smt/q_queue.h b/src/sat/smt/q_queue.h new file mode 100644 index 000000000..c23cb0377 --- /dev/null +++ b/src/sat/smt/q_queue.h @@ -0,0 +1,87 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_queue.h + +Abstract: + + Instantiation queue for quantifiers + +Author: + + Nikolaj Bjorner (nbjorner) 2021-01-24 + +--*/ +#pragma once + +#include "ast/quantifier_stat.h" +#include "ast/cost_evaluator.h" +#include "ast/rewriter/cached_var_subst.h" +#include "parsers/util/cost_parser.h" +#include "sat/smt/q_fingerprint.h" + + + +namespace euf { + class solver; +}; + +namespace q { + + class ematch; + + class queue { + + struct stats { + unsigned m_num_instances, m_num_lazy_instances; + void reset() { memset(this, 0, sizeof(*this)); } + stats() { reset(); } + }; + + ematch& em; + euf::solver& ctx; + ast_manager & m; + qi_params const & m_params; + stats m_stats; + expr_ref m_cost_function; + expr_ref m_new_gen_function; + cost_parser m_parser; + cost_evaluator m_evaluator; + cached_var_subst m_subst; + svector m_vals; + double m_eager_cost_threshold { 0 }; + struct entry { + fingerprint * m_qb; + float m_cost; + bool m_instantiated{ false }; + entry(fingerprint * f, float c):m_qb(f), m_cost(c) {} + }; + struct reset_new_entries; + struct reset_instantiated; + + svector m_new_entries; + svector m_delayed_entries; + + float get_cost(fingerprint& f); + void set_values(fingerprint& f, float cost); + void init_parser_vars(); + void setup(); + unsigned get_new_gen(fingerprint& f, float cost); + void instantiate(entry& e); + + public: + + queue(ematch& em, euf::solver& ctx); + + void insert(fingerprint* f); + + bool propagate(); + + bool lazy_propagate(); + + void collect_statistics(::statistics & st) const; + + }; +} diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index e85878fe5..5f508829c 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -91,7 +91,7 @@ namespace q { } bool solver::unit_propagate() { - return ctx.get_config().m_ematching && m_ematch.propagate(); + return ctx.get_config().m_ematching && m_ematch.propagate(false); } euf::theory_var solver::mk_var(euf::enode* n) { diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index c9b6988cf..78cae3321 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -3,7 +3,6 @@ z3_add_component(smt arith_eq_adapter.cpp arith_eq_solver.cpp asserted_formulas.cpp - cost_evaluator.cpp dyn_ack.cpp expr_context_simplifier.cpp fingerprints.cpp diff --git a/src/smt/qi_queue.h b/src/smt/qi_queue.h index 3de5cb436..bdf4bd50e 100644 --- a/src/smt/qi_queue.h +++ b/src/smt/qi_queue.h @@ -26,7 +26,7 @@ Revision History: #include "smt/smt_quantifier.h" #include "smt/fingerprints.h" #include "smt/params/qi_params.h" -#include "smt/cost_evaluator.h" +#include "ast/cost_evaluator.h" #include "util/statistics.h" namespace smt {