From 46f754c43d43f0cd6cc692494b0cf5dc3a8a83d9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 31 Jan 2021 16:17:52 -0800
Subject: [PATCH] add priority queue to instantiation
---
src/ast/CMakeLists.txt | 1 +
src/{smt => ast}/cost_evaluator.cpp | 2 +-
src/{smt => ast}/cost_evaluator.h | 0
src/ast/euf/euf_egraph.h | 2 -
src/sat/smt/CMakeLists.txt | 3 +
src/sat/smt/euf_solver.h | 3 +
src/sat/smt/q_clause.cpp | 53 +++
src/sat/smt/q_clause.h | 90 +++++
src/sat/smt/q_ematch.cpp | 579 ++++++++--------------------
src/sat/smt/q_ematch.h | 123 ++----
src/sat/smt/q_eval.cpp | 293 ++++++++++++++
src/sat/smt/q_eval.h | 55 +++
src/sat/smt/q_fingerprint.h | 77 ++++
src/sat/smt/q_mam.cpp | 50 +--
src/sat/smt/q_queue.cpp | 256 ++++++++++++
src/sat/smt/q_queue.h | 87 +++++
src/sat/smt/q_solver.cpp | 2 +-
src/smt/CMakeLists.txt | 1 -
src/smt/qi_queue.h | 2 +-
19 files changed, 1138 insertions(+), 541 deletions(-)
rename src/{smt => ast}/cost_evaluator.cpp (98%)
rename src/{smt => ast}/cost_evaluator.h (100%)
create mode 100644 src/sat/smt/q_clause.cpp
create mode 100644 src/sat/smt/q_clause.h
create mode 100644 src/sat/smt/q_eval.cpp
create mode 100644 src/sat/smt/q_eval.h
create mode 100644 src/sat/smt/q_fingerprint.h
create mode 100644 src/sat/smt/q_queue.cpp
create mode 100644 src/sat/smt/q_queue.h
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<void*(void*)>& 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<expr, enode*> 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<binding> {
+ 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<lit> 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<justification*>(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<void(euf::enode*, euf::enode*)> _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<euf::solver> {
vector<unsigned_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<euf::solver, fingerprints, fingerprint*>(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<expr> todo;
- ptr_buffer<euf::enode> 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<euf::solver, unsigned_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<euf::solver, unsigned>(m_qhead));
- ptr_buffer<binding> 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<euf::solver, unsigned>(m_qhead));
+ ptr_buffer<binding> 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<binding> {
- 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<lit> 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<fingerprint, fingerprint_hash_proc, fingerprint_eq_proc> 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<justification*>(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<binding> m_tmp_binding;
+ unsigned m_tmp_binding_capacity { 0 };
+ queue m_inst_queue;
pattern_inference_rw m_infer_patterns;
scoped_ptr<q::mam> m_mam, m_lazy_mam;
ptr_vector<clause> m_clauses;
@@ -139,47 +77,35 @@ namespace q {
vector<unsigned_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<app> 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<size_t> 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<expr> todo;
+ ptr_buffer<euf::enode> 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<size_t> 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<fingerprint *, fingerprint_khasher, fingerprint_chasher>(const_cast<fingerprint*>(f), f->size());
+ }
+ };
+
+ struct fingerprint_eq_proc {
+ bool operator()(fingerprint const* a, fingerprint const* b) const { return a->eq(*b); }
+ };
+
+ typedef ptr_hashtable<fingerprint, fingerprint_hash_proc, fingerprint_eq_proc> 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_point> 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<const get_cgr *>(m_pc)->m_label, static_cast<const get_cgr *>(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<const get_cgr *>(m_pc)->m_label, static_cast<const get_cgr *>(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<const get_cgr *>(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<const cont*>(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<unsigned>(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<float>(min_top_generation);
+ m_vals[MAX_TOP_GENERATION] = static_cast<float>(max_top_generation);
+ m_vals[INSTANCES] = static_cast<float>(stat->get_num_instances_curr_branch());
+ m_vals[SIZE] = static_cast<float>(stat->get_size());
+ m_vals[DEPTH] = static_cast<float>(stat->get_depth());
+ m_vals[GENERATION] = static_cast<float>(f.m_max_generation);
+ m_vals[QUANT_GENERATION] = static_cast<float>(stat->get_generation());
+ m_vals[WEIGHT] = static_cast<float>(q->get_weight());
+ m_vals[VARS] = static_cast<float>(q->get_num_decls());
+ m_vals[PATTERN_WIDTH] = pat ? static_cast<float>(pat->get_num_args()) : 1.0f;
+ m_vals[TOTAL_INSTANCES] = static_cast<float>(stat->get_num_instances_curr_search());
+ m_vals[SCOPE] = static_cast<float>(ctx.s().num_scopes());
+ m_vals[NESTED_QUANTIFIERS] = static_cast<float>(stat->get_num_nested_quantifiers());
+ m_vals[CS_FACTOR] = static_cast<float>(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<unsigned>(r));
+ }
+
+ struct queue::reset_new_entries : public trail<euf::solver> {
+ svector<entry>& m_entries;
+ reset_new_entries(svector<entry>& 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<euf::solver,svector<entry>>(m_delayed_entries));
+ }
+ }
+ m_new_entries.reset();
+ return true;
+ }
+
+ struct queue::reset_instantiated : public trail<euf::solver> {
+ 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<float> 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<entry> m_new_entries;
+ svector<entry> 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 {