mirror of
https://github.com/Z3Prover/z3
synced 2025-04-14 04:48:45 +00:00
debugging quantifier instantiation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
cda29bc03b
commit
477e8cc46a
|
|
@ -18,13 +18,14 @@ Author:
|
|||
|
||||
Revision History:
|
||||
|
||||
Based on approach suggested in SAS 2013 paper
|
||||
Based on approach suggested in the SAS 2013 paper
|
||||
"On Solving Universally Quantified Horn Clauses"
|
||||
|
||||
--*/
|
||||
|
||||
#include "dl_mk_quantifier_instantiation.h"
|
||||
#include "dl_context.h"
|
||||
#include "pattern_inference.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
@ -34,12 +35,10 @@ namespace datalog {
|
|||
m(ctx.get_manager()),
|
||||
m_ctx(ctx),
|
||||
m_var2cnst(m),
|
||||
m_cnst2var(m),
|
||||
a(m) {
|
||||
m_cnst2var(m) {
|
||||
}
|
||||
|
||||
mk_quantifier_instantiation::~mk_quantifier_instantiation() {
|
||||
|
||||
mk_quantifier_instantiation::~mk_quantifier_instantiation() {
|
||||
}
|
||||
|
||||
void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs) {
|
||||
|
|
@ -66,8 +65,15 @@ namespace datalog {
|
|||
void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, expr_ref_vector & conjs) {
|
||||
expr_ref qe(m);
|
||||
qe = q;
|
||||
m_var2cnst(qe);
|
||||
m_var2cnst(qe);
|
||||
q = to_quantifier(qe);
|
||||
if (q->get_num_patterns() == 0) {
|
||||
proof_ref new_pr(m);
|
||||
pattern_inference_params params;
|
||||
pattern_inference infer(m, params);
|
||||
infer(q, qe, new_pr);
|
||||
q = to_quantifier(qe);
|
||||
}
|
||||
unsigned num_patterns = q->get_num_patterns();
|
||||
for (unsigned i = 0; i < num_patterns; ++i) {
|
||||
expr * pat = q->get_pattern(i);
|
||||
|
|
@ -86,6 +92,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void mk_quantifier_instantiation::match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs) {
|
||||
TRACE("dl", tout << "match" << mk_pp(pat, m) << "\n";);
|
||||
while (j < todo.size()) {
|
||||
expr* p = todo[j].first;
|
||||
expr* t = todo[j].second;
|
||||
|
|
@ -102,7 +109,7 @@ namespace datalog {
|
|||
// matching failed.
|
||||
return;
|
||||
}
|
||||
j += 1;
|
||||
++j;
|
||||
continue;
|
||||
}
|
||||
if (!is_app(p)) {
|
||||
|
|
@ -125,7 +132,7 @@ namespace datalog {
|
|||
todo.resize(sz);
|
||||
}
|
||||
}
|
||||
next_id = m_uf.next(id);
|
||||
next_id = m_uf.next(next_id);
|
||||
}
|
||||
while (next_id != id);
|
||||
return;
|
||||
|
|
@ -156,16 +163,14 @@ namespace datalog {
|
|||
expr_ref res(m);
|
||||
instantiate(m, q, m_binding.c_ptr(), res);
|
||||
m_binding.reverse();
|
||||
m_cnst2var(res);
|
||||
conjs.push_back(res);
|
||||
TRACE("dl", tout << mk_pp(q, m) << "\n==>\n" << mk_pp(res, m) << "\n";);
|
||||
}
|
||||
|
||||
void mk_quantifier_instantiation::merge(expr* e1, expr* e2) {
|
||||
unsigned i1 = e1->get_id();
|
||||
unsigned i2 = e2->get_id();
|
||||
unsigned n = std::max(i1, i2);
|
||||
while (n >= m_uf.get_num_vars()) {
|
||||
m_uf.mk_var();
|
||||
}
|
||||
m_uf.merge(i1, i2);
|
||||
}
|
||||
|
||||
|
|
@ -179,7 +184,8 @@ namespace datalog {
|
|||
if (visited.is_marked(e)) {
|
||||
continue;
|
||||
}
|
||||
if (e->get_id() >= m_terms.size()) {
|
||||
unsigned n = e->get_id();
|
||||
if (n >= m_terms.size()) {
|
||||
m_terms.resize(e->get_id()+1);
|
||||
}
|
||||
m_terms[e->get_id()] = e;
|
||||
|
|
@ -190,7 +196,7 @@ namespace datalog {
|
|||
if (is_app(e)) {
|
||||
app* ap = to_app(e);
|
||||
ptr_vector<expr>* terms = 0;
|
||||
if (m_funs.find(ap->get_decl(), terms)) {
|
||||
if (!m_funs.find(ap->get_decl(), terms)) {
|
||||
terms = alloc(ptr_vector<expr>);
|
||||
m_funs.insert(ap->get_decl(), terms);
|
||||
}
|
||||
|
|
@ -237,6 +243,7 @@ namespace datalog {
|
|||
|
||||
fml = m.mk_and(conjs.size(), conjs.c_ptr());
|
||||
fml = m.mk_implies(fml, r.get_head());
|
||||
TRACE("dl", r.display(m_ctx, tout); tout << mk_pp(fml, m) << "\n";);
|
||||
|
||||
rule_ref_vector added_rules(rm);
|
||||
proof_ref pr(m); // proofs are TBD.
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ Author:
|
|||
|
||||
Revision History:
|
||||
|
||||
Based on approach suggested in SAS 2013 paper
|
||||
Based on approach suggested in the SAS 2013 paper
|
||||
"On Solving Universally Quantified Horn Clauses"
|
||||
|
||||
--*/
|
||||
|
|
@ -27,7 +27,6 @@ Revision History:
|
|||
|
||||
|
||||
#include"dl_rule_transformer.h"
|
||||
#include"array_decl_plugin.h"
|
||||
#include"expr_safe_replace.h"
|
||||
|
||||
|
||||
|
|
@ -42,6 +41,12 @@ namespace datalog {
|
|||
unsigned_vector m_find;
|
||||
unsigned_vector m_size;
|
||||
unsigned_vector m_next;
|
||||
|
||||
void ensure_size(unsigned v) {
|
||||
while (v >= get_num_vars()) {
|
||||
mk_var();
|
||||
}
|
||||
}
|
||||
public:
|
||||
unsigned mk_var() {
|
||||
unsigned r = m_find.size();
|
||||
|
|
@ -53,6 +58,9 @@ namespace datalog {
|
|||
unsigned get_num_vars() const { return m_find.size(); }
|
||||
|
||||
unsigned find(unsigned v) const {
|
||||
if (v >= get_num_vars()) {
|
||||
return v;
|
||||
}
|
||||
while (true) {
|
||||
unsigned new_v = m_find[v];
|
||||
if (new_v == v)
|
||||
|
|
@ -61,15 +69,24 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
unsigned next(unsigned v) const { return m_next[v]; }
|
||||
unsigned next(unsigned v) const {
|
||||
if (v >= get_num_vars()) {
|
||||
return v;
|
||||
}
|
||||
return m_next[v];
|
||||
}
|
||||
|
||||
bool is_root(unsigned v) const { return m_find[v] == v; }
|
||||
bool is_root(unsigned v) const {
|
||||
return v >= get_num_vars() || m_find[v] == v;
|
||||
}
|
||||
|
||||
void merge(unsigned v1, unsigned v2) {
|
||||
unsigned r1 = find(v1);
|
||||
unsigned r2 = find(v2);
|
||||
if (r1 == r2)
|
||||
return;
|
||||
ensure_size(v1);
|
||||
ensure_size(v2);
|
||||
if (m_size[r1] > m_size[r2])
|
||||
std::swap(r1, r2);
|
||||
m_find[r1] = r2;
|
||||
|
|
@ -83,15 +100,15 @@ namespace datalog {
|
|||
m_size.reset();
|
||||
}
|
||||
};
|
||||
ast_manager& m;
|
||||
context& m_ctx;
|
||||
|
||||
ast_manager& m;
|
||||
context& m_ctx;
|
||||
expr_safe_replace m_var2cnst;
|
||||
expr_safe_replace m_cnst2var;
|
||||
array_util a;
|
||||
union_find m_uf;
|
||||
ptr_vector<expr> m_todo;
|
||||
ptr_vector<expr> m_terms;
|
||||
ptr_vector<expr> m_binding;
|
||||
union_find m_uf;
|
||||
ptr_vector<expr> m_todo;
|
||||
ptr_vector<expr> m_terms;
|
||||
ptr_vector<expr> m_binding;
|
||||
obj_map<func_decl, ptr_vector<expr>*> m_funs;
|
||||
|
||||
|
||||
|
|
@ -100,9 +117,9 @@ namespace datalog {
|
|||
void collect_egraph(expr* e);
|
||||
void instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules);
|
||||
void instantiate_quantifier(quantifier* q, expr_ref_vector & conjs);
|
||||
void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs);
|
||||
void mk_quantifier_instantiation::match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs);
|
||||
void mk_quantifier_instantiation::yield_binding(quantifier* q, expr_ref_vector& conjs);
|
||||
void instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs);
|
||||
void match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs);
|
||||
void yield_binding(quantifier* q, expr_ref_vector& conjs);
|
||||
|
||||
public:
|
||||
mk_quantifier_instantiation(context & ctx, unsigned priority);
|
||||
|
|
|
|||
Loading…
Reference in a new issue