mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Merge branch 'dl_transforms' into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-03 17:06:47 -07:00
parent 359d2326f8 0b7a270883
commit 282173773f
5 changed files with 870 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/datalog_parser.cpp
View file

@ -441,6 +441,7 @@ protected:
unsigned m_sym_idx;
std::string m_path;
str2sort m_sort_dict;
// true if an error occured during the current call to the parse_stream
// function
@ -812,7 +813,8 @@ protected:
}
f = m_manager.mk_func_decl(s, domain.size(), domain.c_ptr(), m_manager.mk_bool_sort());
m_context.register_predicate(f);
m_context.register_predicate(f, true);
while (tok == TK_ID) {
char const* pred_pragma = m_lexer->get_token_data();
if(strcmp(pred_pragma, "printtuples")==0 || strcmp(pred_pragma, "outputtuples")==0) {

367
src/muz_qe/dl_mk_quantifier_abstraction.cpp Normal file
View file

@ -0,0 +1,367 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_quantifier_abstraction.cpp
Abstract:
Create quantified Horn clauses from benchmarks with arrays.
Author:
Ken McMillan
Andrey Rybalchenko
Nikolaj Bjorner (nbjorner) 2013-04-02
Revision History:
--*/
#include "dl_mk_quantifier_abstraction.h"
#include "dl_context.h"
#include "expr_safe_replace.h"
#include "expr_abstract.h"
namespace datalog {
// model converter:
// Given model for P^(x, y, i, a[i])
// create model: P(x,y,a) == forall i . P^(x,y,i,a[i])
// requires substitution and list of bound variables.
class mk_quantifier_abstraction::qa_model_converter : public model_converter {
ast_manager& m;
func_decl_ref_vector m_old_funcs;
func_decl_ref_vector m_new_funcs;
vector<expr_ref_vector> m_subst;
vector<sort_ref_vector> m_sorts;
vector<svector<bool> > m_bound;
public:
qa_model_converter(ast_manager& m):
m(m), m_old_funcs(m), m_new_funcs(m) {}
virtual ~qa_model_converter() {}
virtual model_converter * translate(ast_translation & translator) {
return alloc(qa_model_converter, m);
}
void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector<bool> const& bound) {
m_old_funcs.push_back(old_p);
m_new_funcs.push_back(new_p);
m_subst.push_back(sub);
m_bound.push_back(bound);
m_sorts.push_back(sorts);
}
virtual void operator()(model_ref & old_model) {
model_ref new_model = alloc(model, m);
for (unsigned i = 0; i < m_new_funcs.size(); ++i) {
func_decl* p = m_new_funcs[i].get();
func_decl* q = m_old_funcs[i].get();
expr_ref_vector const& sub = m_subst[i];
sort_ref_vector const& sorts = m_sorts[i];
svector<bool> const& is_bound = m_bound[i];
func_interp* f = old_model->get_func_interp(p);
expr_ref body(m);
unsigned arity_p = p->get_arity();
unsigned arity_q = q->get_arity();
SASSERT(0 < arity_p);
func_interp* g = alloc(func_interp, m, arity_q);
if (f) {
body = f->get_interp();
SASSERT(!f->is_partial());
SASSERT(body);
}
else {
body = m.mk_false();
}
// Create quantifier wrapper around body.
TRACE("dl", tout << mk_pp(body, m) << "\n";);
// 1. replace variables by the compound terms from
// the original predicate.
expr_safe_replace rep(m);
for (unsigned i = 0; i < sub.size(); ++i) {
rep.insert(m.mk_var(i, m.get_sort(sub[i])), sub[i]);
}
rep(body);
rep.reset();
TRACE("dl", tout << mk_pp(body, m) << "\n";);
// 2. replace bound variables by constants.
expr_ref_vector consts(m), bound(m), free(m);
svector<symbol> names;
ptr_vector<sort> bound_sorts;
for (unsigned i = 0; i < sorts.size(); ++i) {
sort* s = sorts[i];
consts.push_back(m.mk_fresh_const("C", s));
rep.insert(m.mk_var(i, s), consts.back());
if (is_bound[i]) {
bound.push_back(consts.back());
names.push_back(symbol(i));
bound_sorts.push_back(s);
}
else {
free.push_back(consts.back());
}
}
rep(body);
rep.reset();
TRACE("dl", tout << mk_pp(body, m) << "\n";);
// 3. abstract and quantify those variables that should be bound.
expr_abstract(m, 0, bound.size(), bound.c_ptr(), body, body);
body = m.mk_forall(names.size(), bound_sorts.c_ptr(), names.c_ptr(), body);
TRACE("dl", tout << mk_pp(body, m) << "\n";);
// 4. replace remaining constants by variables.
for (unsigned i = 0; i < free.size(); ++i) {
rep.insert(free[i].get(), m.mk_var(i, m.get_sort(free[i].get())));
}
rep(body);
g->set_else(body);
TRACE("dl", tout << mk_pp(body, m) << "\n";);
new_model->register_decl(q, g);
}
old_model = new_model;
}
};
mk_quantifier_abstraction::mk_quantifier_abstraction(
context & ctx, unsigned priority):
plugin(priority),
m(ctx.get_manager()),
m_ctx(ctx),
a(m),
m_refs(m) {
}
mk_quantifier_abstraction::~mk_quantifier_abstraction() {
}
func_decl* mk_quantifier_abstraction::declare_pred(func_decl* old_p) {
if (m_ctx.is_output_predicate(old_p)) {
return 0;
}
unsigned sz = old_p->get_arity();
unsigned num_arrays = 0;
for (unsigned i = 0; i < sz; ++i) {
if (a.is_array(old_p->get_domain(i))) {
num_arrays++;
}
}
if (num_arrays == 0) {
return 0;
}
func_decl* new_p = 0;
if (!m_old2new.find(old_p, new_p)) {
expr_ref_vector sub(m), vars(m);
svector<bool> bound;
sort_ref_vector domain(m), sorts(m);
expr_ref arg(m);
for (unsigned i = 0; i < sz; ++i) {
sort* s0 = old_p->get_domain(i);
unsigned lookahead = 0;
sort* s = s0;
while (a.is_array(s)) {
lookahead += get_array_arity(s);
s = get_array_range(s);
}
arg = m.mk_var(bound.size() + lookahead, s0);
s = s0;
while (a.is_array(s)) {
unsigned arity = get_array_arity(s);
expr_ref_vector args(m);
for (unsigned j = 0; j < arity; ++j) {
sort* s1 = get_array_domain(s, j);
domain.push_back(s1);
args.push_back(m.mk_var(bound.size(), s1));
bound.push_back(true);
sorts.push_back(s1);
}
arg = mk_select(arg, args.size(), args.c_ptr());
s = get_array_range(s);
}
domain.push_back(s);
bound.push_back(false);
sub.push_back(arg);
sorts.push_back(s0);
}
SASSERT(old_p->get_range() == m.mk_bool_sort());
new_p = m.mk_func_decl(old_p->get_name(), domain.size(), domain.c_ptr(), old_p->get_range());
m_refs.push_back(new_p);
m_ctx.register_predicate(new_p, false);
if (m_mc) {
m_mc->insert(old_p, new_p, sub, sorts, bound);
}
m_old2new.insert(old_p, new_p);
}
return new_p;
}
app_ref mk_quantifier_abstraction::mk_head(app* p, unsigned idx) {
func_decl* new_p = declare_pred(p->get_decl());
if (!new_p) {
return app_ref(p, m);
}
expr_ref_vector args(m);
expr_ref arg(m);
unsigned sz = p->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
arg = p->get_arg(i);
sort* s = m.get_sort(arg);
while (a.is_array(s)) {
unsigned arity = get_array_arity(s);
for (unsigned j = 0; j < arity; ++j) {
args.push_back(m.mk_var(idx++, get_array_domain(s, j)));
}
arg = mk_select(arg, arity, args.c_ptr()+args.size()-arity);
s = get_array_range(s);
}
args.push_back(arg);
}
TRACE("dl",
tout << mk_pp(new_p, m) << "\n";
for (unsigned i = 0; i < args.size(); ++i) {
tout << mk_pp(args[i].get(), m) << "\n";
});
return app_ref(m.mk_app(new_p, args.size(), args.c_ptr()), m);
}
app_ref mk_quantifier_abstraction::mk_tail(app* p) {
func_decl* old_p = p->get_decl();
func_decl* new_p = declare_pred(old_p);
if (!new_p) {
return app_ref(p, m);
}
SASSERT(new_p->get_arity() > old_p->get_arity());
unsigned num_extra_args = new_p->get_arity() - old_p->get_arity();
var_shifter shift(m);
expr_ref p_shifted(m);
shift(p, num_extra_args, p_shifted);
app* ps = to_app(p_shifted);
expr_ref_vector args(m);
app_ref_vector pats(m);
sort_ref_vector vars(m);
svector<symbol> names;
expr_ref arg(m);
unsigned idx = 0;
unsigned sz = p->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
arg = ps->get_arg(i);
sort* s = m.get_sort(arg);
bool is_pattern = false;
while (a.is_array(s)) {
is_pattern = true;
unsigned arity = get_array_arity(s);
for (unsigned j = 0; j < arity; ++j) {
vars.push_back(get_array_domain(s, j));
names.push_back(symbol(idx));
args.push_back(m.mk_var(idx++, vars.back()));
}
arg = mk_select(arg, arity, args.c_ptr()+args.size()-arity);
s = get_array_range(s);
}
if (is_pattern) {
pats.push_back(to_app(arg));
}
args.push_back(arg);
}
expr* pat = 0;
expr_ref pattern(m);
pattern = m.mk_pattern(pats.size(), pats.c_ptr());
pat = pattern.get();
app_ref result(m);
symbol qid, skid;
result = m.mk_app(new_p, args.size(), args.c_ptr());
result = m.mk_eq(m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), result, 1, qid, skid, 1, &pat), m.mk_true());
return result;
}
expr * mk_quantifier_abstraction::mk_select(expr* arg, unsigned num_args, expr* const* args) {
ptr_vector<expr> args2;
args2.push_back(arg);
args2.append(num_args, args);
return a.mk_select(args2.size(), args2.c_ptr());
}
rule_set * mk_quantifier_abstraction::operator()(rule_set const & source) {
TRACE("dl", tout << "quantify " << source.get_num_rules() << " " << m_ctx.get_params().quantify_arrays() << "\n";);
if (!m_ctx.get_params().quantify_arrays()) {
return 0;
}
unsigned sz = source.get_num_rules();
for (unsigned i = 0; i < sz; ++i) {
rule& r = *source.get_rule(i);
if (r.has_negation()) {
return 0;
}
}
m_refs.reset();
m_old2new.reset();
m_new2old.reset();
rule_manager& rm = source.get_rule_manager();
rule_ref new_rule(rm);
expr_ref_vector tail(m);
app_ref head(m);
expr_ref fml(m);
rule_counter& vc = rm.get_counter();
if (m_ctx.get_model_converter()) {
m_mc = alloc(qa_model_converter, m);
}
rule_set * result = alloc(rule_set, m_ctx);
for (unsigned i = 0; i < sz; ++i) {
tail.reset();
rule & r = *source.get_rule(i);
TRACE("dl", r.display(m_ctx, tout); );
unsigned cnt = vc.get_max_rule_var(r)+1;
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
for (unsigned j = 0; j < utsz; ++j) {
tail.push_back(mk_tail(r.get_tail(j)));
}
for (unsigned j = utsz; j < tsz; ++j) {
tail.push_back(r.get_tail(j));
}
head = mk_head(r.get_head(), cnt);
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head);
rule_ref_vector added_rules(rm);
proof_ref pr(m);
rm.mk_rule(fml, pr, added_rules);
result->add_rules(added_rules.size(), added_rules.c_ptr());
TRACE("dl", added_rules.back()->display(m_ctx, tout););
}
// proof converter: proofs are not necessarily preserved using this transformation.
if (m_old2new.empty()) {
dealloc(result);
dealloc(m_mc);
result = 0;
}
else {
m_ctx.add_model_converter(m_mc);
}
m_mc = 0;
return result;
}
};

64
src/muz_qe/dl_mk_quantifier_abstraction.h Normal file
View file

@ -0,0 +1,64 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_quantifier_abstraction.h
Abstract:
Convert clauses with array arguments to predicates
into Quantified Horn clauses.
Author:
Ken McMillan
Andrey Rybalchenko
Nikolaj Bjorner (nbjorner) 2013-04-02
Revision History:
Based on approach suggested in SAS 2013 paper
"On Solving Universally Quantified Horn Clauses"
--*/
#ifndef _DL_MK_QUANTIFIER_ABSTRACTION_H_
#define _DL_MK_QUANTIFIER_ABSTRACTION_H_
#include"dl_rule_transformer.h"
#include"array_decl_plugin.h"
namespace datalog {
class context;
class mk_quantifier_abstraction : public rule_transformer::plugin {
class qa_model_converter;
ast_manager& m;
context& m_ctx;
array_util a;
func_decl_ref_vector m_refs;
obj_map<func_decl, func_decl*> m_new2old;
obj_map<func_decl, func_decl*> m_old2new;
qa_model_converter* m_mc;
func_decl* declare_pred(func_decl* old_p);
app_ref mk_head(app* p, unsigned idx);
app_ref mk_tail(app* p);
expr* mk_select(expr* a, unsigned num_args, expr* const* args);
public:
mk_quantifier_abstraction(context & ctx, unsigned priority);
virtual ~mk_quantifier_abstraction();
rule_set * operator()(rule_set const & source);
};
};
#endif /* _DL_MK_QUANTIFIER_ABSTRACTION_H_ */

300
src/muz_qe/dl_mk_quantifier_instantiation.cpp Normal file
View file

@ -0,0 +1,300 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_quantifier_instantiation.cpp
Abstract:
Convert Quantified Horn clauses into non-quantified clauses using
instantiation.
Author:
Ken McMillan
Andrey Rybalchenko
Nikolaj Bjorner (nbjorner) 2013-04-02
Revision History:
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 {
mk_quantifier_instantiation::mk_quantifier_instantiation(
context & ctx, unsigned priority):
plugin(priority),
m(ctx.get_manager()),
m_ctx(ctx),
m_var2cnst(m),
m_cnst2var(m) {
}
mk_quantifier_instantiation::~mk_quantifier_instantiation() {
}
void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs) {
conjs.reset();
qs.reset();
unsigned tsz = r.get_tail_size();
for (unsigned j = 0; j < tsz; ++j) {
conjs.push_back(r.get_tail(j));
}
datalog::flatten_and(conjs);
for (unsigned j = 0; j < conjs.size(); ++j) {
expr* e = conjs[j].get();
quantifier* q;
if (rule_manager::is_forall(m, e, q)) {
qs.push_back(q);
conjs[j] = conjs.back();
conjs.pop_back();
--j;
}
}
}
void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, expr_ref_vector & conjs) {
expr_ref qe(m);
qe = q;
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);
SASSERT(m.is_pattern(pat));
instantiate_quantifier(q, to_app(pat), conjs);
}
}
void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs) {
unsigned sz = pat->get_num_args();
m_binding.reset();
m_binding.resize(q->get_num_decls());
term_pairs todo;
match(0, pat, 0, todo, q, conjs);
}
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;
if (is_var(p)) {
unsigned idx = to_var(p)->get_idx();
if (!m_binding[idx]) {
m_binding[idx] = t;
match(i, pat, j + 1, todo, q, conjs);
m_binding[idx] = 0;
return;
}
++j;
continue;
}
if (!is_app(p)) {
return;
}
app* a1 = to_app(p);
unsigned id = t->get_id();
unsigned next_id = id;
unsigned sz = todo.size();
do {
expr* t2 = m_terms[next_id];
if (is_app(t2)) {
app* a2 = to_app(t2);
if (a1->get_decl() == a2->get_decl() &&
a1->get_num_args() == a2->get_num_args()) {
for (unsigned k = 0; k < a1->get_num_args(); ++k) {
todo.push_back(std::make_pair(a1->get_arg(k), a2->get_arg(k)));
}
match(i, pat, j + 1, todo, q, conjs);
todo.resize(sz);
}
}
next_id = m_uf.next(next_id);
}
while (next_id != id);
return;
}
if (i == pat->get_num_args()) {
yield_binding(q, conjs);
return;
}
expr* arg = pat->get_arg(i);
ptr_vector<expr>* terms = 0;
if (m_funs.find(to_app(arg)->get_decl(), terms)) {
for (unsigned k = 0; k < terms->size(); ++k) {
todo.push_back(std::make_pair(arg, (*terms)[k]));
match(i + 1, pat, j, todo, q, conjs);
todo.pop_back();
}
}
}
void mk_quantifier_instantiation::yield_binding(quantifier* q, expr_ref_vector& conjs) {
DEBUG_CODE(
for (unsigned i = 0; i < m_binding.size(); ++i) {
SASSERT(m_binding[i]);
});
m_binding.reverse();
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::collect_egraph(expr* e) {
expr* e1, *e2;
m_todo.push_back(e);
expr_fast_mark1 visited;
while (!m_todo.empty()) {
e = m_todo.back();
m_todo.pop_back();
if (visited.is_marked(e)) {
continue;
}
unsigned n = e->get_id();
if (n >= m_terms.size()) {
m_terms.resize(n+1);
}
m_terms[n] = e;
visited.mark(e);
if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) {
m_uf.merge(e1->get_id(), e2->get_id());
}
if (is_app(e)) {
app* ap = to_app(e);
ptr_vector<expr>* terms = 0;
if (!m_funs.find(ap->get_decl(), terms)) {
terms = alloc(ptr_vector<expr>);
m_funs.insert(ap->get_decl(), terms);
}
terms->push_back(e);
m_todo.append(ap->get_num_args(), ap->get_args());
}
}
}
void mk_quantifier_instantiation::instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules) {
rule_manager& rm = m_ctx.get_rule_manager();
expr_ref fml(m), cnst(m);
var_ref var(m);
ptr_vector<sort> sorts;
r.get_vars(sorts);
m_uf.reset();
m_terms.reset();
m_var2cnst.reset();
m_cnst2var.reset();
fml = m.mk_and(conjs.size(), conjs.c_ptr());
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
var = m.mk_var(i, sorts[i]);
cnst = m.mk_fresh_const("C", sorts[i]);
m_var2cnst.insert(var, cnst);
m_cnst2var.insert(cnst, var);
}
fml = m.mk_and(conjs.size(), conjs.c_ptr());
m_var2cnst(fml);
collect_egraph(fml);
for (unsigned i = 0; i < qs.size(); ++i) {
instantiate_quantifier(qs[i].get(), conjs);
}
obj_map<func_decl, ptr_vector<expr>*>::iterator it = m_funs.begin(), end = m_funs.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
m_funs.reset();
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);
rm.mk_rule(fml, pr, added_rules);
if (r.get_proof()) {
// use def-axiom to encode that new rule is a weakening of the original.
proof* p1 = r.get_proof();
for (unsigned i = 0; i < added_rules.size(); ++i) {
rule* r2 = added_rules[i].get();
r2->to_formula(fml);
pr = m.mk_modus_ponens(m.mk_def_axiom(m.mk_implies(m.get_fact(p1), fml)), p1);
r2->set_proof(m, pr);
}
}
rules.add_rules(added_rules.size(), added_rules.c_ptr());
}
rule_set * mk_quantifier_instantiation::operator()(rule_set const & source) {
TRACE("dl", tout << m_ctx.get_params().instantiate_quantifiers() << "\n";);
if (!m_ctx.get_params().instantiate_quantifiers()) {
return 0;
}
bool has_quantifiers = false;
unsigned sz = source.get_num_rules();
for (unsigned i = 0; !has_quantifiers && i < sz; ++i) {
rule& r = *source.get_rule(i);
has_quantifiers = has_quantifiers || r.has_quantifiers();
if (r.has_negation()) {
return 0;
}
}
if (!has_quantifiers) {
return 0;
}
expr_ref_vector conjs(m);
quantifier_ref_vector qs(m);
rule_set * result = alloc(rule_set, m_ctx);
bool instantiated = false;
for (unsigned i = 0; i < sz; ++i) {
rule * r = source.get_rule(i);
extract_quantifiers(*r, conjs, qs);
if (qs.empty()) {
result->add_rule(r);
}
else {
instantiate_rule(*r, conjs, qs, *result);
instantiated = true;
}
}
// model convertion: identity function.
if (!instantiated) {
dealloc(result);
result = 0;
}
return result;
}
};

136
src/muz_qe/dl_mk_quantifier_instantiation.h Normal file
View file

@ -0,0 +1,136 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
dl_mk_quantifier_instantiation.h
Abstract:
Convert Quantified Horn clauses into non-quantified clauses using
instantiation.
Author:
Ken McMillan
Andrey Rybalchenko
Nikolaj Bjorner (nbjorner) 2013-04-02
Revision History:
Based on approach suggested in the SAS 2013 paper
"On Solving Universally Quantified Horn Clauses"
--*/
#ifndef _DL_MK_QUANTIFIER_INSTANTIATION_H_
#define _DL_MK_QUANTIFIER_INSTANTIATION_H_
#include"dl_rule_transformer.h"
#include"expr_safe_replace.h"
namespace datalog {
class context;
class mk_quantifier_instantiation : public rule_transformer::plugin {
typedef svector<std::pair<expr*,expr*> > term_pairs;
class union_find {
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();
m_find.push_back(r);
m_size.push_back(1);
m_next.push_back(r);
return r;
}
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)
return v;
v = new_v;
}
}
unsigned next(unsigned v) const {
if (v >= get_num_vars()) {
return v;
}
return m_next[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;
m_size[r2] += m_size[r1];
std::swap(m_next[r1], m_next[r2]);
}
void reset() {
m_find.reset();
m_next.reset();
m_size.reset();
}
};
ast_manager& m;
context& m_ctx;
expr_safe_replace m_var2cnst;
expr_safe_replace m_cnst2var;
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;
void extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs);
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 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);
virtual ~mk_quantifier_instantiation();
rule_set * operator()(rule_set const & source);
};
};
#endif /* _DL_MK_QUANTIFIER_INSTANTIATION_H_ */