mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

significant update to Horn routines: add module hnf to extract Horn normal form (removed from rule_manager). Associate proof objects with rules to track (all) rewrites, so that proof traces can be tracked back to original rules after transformations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-23 14:11:54 -07:00
parent e73c06a8b0
commit 26f4d3be20
60 changed files with 591 additions and 428 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/z3_api.h
View file

@ -701,7 +701,7 @@ typedef enum
over Boolean connectives 'and' and 'or'. over Boolean connectives 'and' and 'or'.
- Z3_OP_PR_NFF_NEG: Proof for a (negative) NNF step. Examples: - Z3_OP_PR_NNF_NEG: Proof for a (negative) NNF step. Examples:
\nicebox{ \nicebox{
T1: (not s_1) ~ r_1 T1: (not s_1) ~ r_1
... ...

30
src/ast/rewriter/quant_hoist.cpp
View file

@ -80,7 +80,7 @@ public:
instantiate(m, q, exprs, result); instantiate(m, q, exprs, result);
} }
unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) { unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
unsigned index = var_counter().get_next_var(fml); unsigned index = var_counter().get_next_var(fml);
while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) { while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
quantifier* q = to_quantifier(fml); quantifier* q = to_quantifier(fml);
@ -88,6 +88,9 @@ public:
if (names) { if (names) {
names->append(q->get_num_decls(), q->get_decl_names()); names->append(q->get_num_decls(), q->get_decl_names());
} }
if (sorts) {
sorts->append(q->get_num_decls(), q->get_decl_sorts());
}
fml = q->get_expr(); fml = q->get_expr();
} }
if (!has_quantifiers(fml)) { if (!has_quantifiers(fml)) {
@ -100,12 +103,29 @@ public:
} }
// replace vars by de-bruijn indices // replace vars by de-bruijn indices
expr_safe_replace rep(m); expr_safe_replace rep(m);
svector<symbol> bound_names;
ptr_vector<sort> bound_sorts;
for (unsigned i = 0; i < vars.size(); ++i) { for (unsigned i = 0; i < vars.size(); ++i) {
app* v = vars[i].get(); app* v = vars[i].get();
if (names) { if (names) {
names->push_back(v->get_decl()->get_name()); bound_names.push_back(v->get_decl()->get_name());
} }
rep.insert(v, m.mk_var(index++,m.get_sort(v))); if (sorts) {
bound_sorts.push_back(m.get_sort(v));
}
rep.insert(v, m.mk_var(index++, m.get_sort(v)));
}
if (names && !bound_names.empty()) {
bound_names.reverse();
bound_names.append(*names);
names->reset();
names->append(bound_names);
}
if (sorts && !bound_sorts.empty()) {
bound_sorts.reverse();
bound_sorts.append(*sorts);
sorts->reset();
sorts->append(bound_sorts);
} }
rep(fml); rep(fml);
return index; return index;
@ -270,6 +290,6 @@ void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_
m_impl->pull_quantifier(is_forall, fml, vars); m_impl->pull_quantifier(is_forall, fml, vars);
} }
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) { unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
return m_impl->pull_quantifier(is_forall, fml, names); return m_impl->pull_quantifier(is_forall, fml, sorts, names);
} }

2
src/ast/rewriter/quant_hoist.h
View file

@ -66,7 +66,7 @@ public:
Return index of maximal variable. Return index of maximal variable.
*/ */
unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names); unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names);
}; };
#endif #endif

2
src/muz_qe/dl_base.cpp
View file

@ -233,7 +233,7 @@ namespace datalog {
table_fact row; table_fact row;
for(; it!=iend; ++it) { for(; it!=iend; ++it) {
it->get_fact(row); it->get_fact(row);
to_remove.append(row); to_remove.push_back(row);
} }
remove_facts(to_remove.size(), to_remove.c_ptr()); remove_facts(to_remove.size(), to_remove.c_ptr());
} }

40
src/muz_qe/dl_bmc_engine.cpp
View file

@ -307,7 +307,7 @@ namespace datalog {
r1->to_formula(concl); r1->to_formula(concl);
scoped_proof _sp(m); scoped_proof _sp(m);
proof* p = m.mk_asserted(fml); proof* p = r->get_proof();
proof* premises[2] = { pr, p }; proof* premises[2] = { pr, p };
positions.push_back(std::make_pair(0, 1)); positions.push_back(std::make_pair(0, 1));
@ -320,7 +320,7 @@ namespace datalog {
else { else {
r2->to_formula(concl); r2->to_formula(concl);
scoped_proof _sp(m); scoped_proof _sp(m);
proof* p = m.mk_asserted(fml); proof* p = r->get_proof();
if (sub.empty()) { if (sub.empty()) {
pr = p; pr = p;
} }
@ -340,7 +340,7 @@ namespace datalog {
pred = r->get_decl(0); pred = r->get_decl(0);
} }
scoped_proof _sp(m); scoped_proof _sp(m);
apply(m, b.m_pc.get(), pr); apply(m, b.m_ctx.get_proof_converter().get(), pr);
b.m_answer = pr; b.m_answer = pr;
return l_true; return l_true;
} }
@ -474,6 +474,9 @@ namespace datalog {
} }
proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) { proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) {
if (b.m_cancel) {
return proof_ref(0, m);
}
TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";); TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m); expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m);
@ -497,7 +500,7 @@ namespace datalog {
SASSERT(r); SASSERT(r);
r->to_formula(fml); r->to_formula(fml);
IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";); IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";);
prs.push_back(m.mk_asserted(fml)); prs.push_back(r->get_proof());
unsigned sz = r->get_uninterpreted_tail_size(); unsigned sz = r->get_uninterpreted_tail_size();
ptr_vector<sort> rule_vars; ptr_vector<sort> rule_vars;
@ -536,8 +539,9 @@ namespace datalog {
model_ref md; model_ref md;
b.m_solver.get_model(md); b.m_solver.get_model(md);
IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
proof_ref pr = get_proof(md, b.m_query_pred, to_app(level_query), level); proof_ref pr(m);
apply(m, b.m_pc.get(), pr); pr = get_proof(md, b.m_query_pred, to_app(level_query), level);
apply(m, b.m_ctx.get_proof_converter().get(), pr);
b.m_answer = pr; b.m_answer = pr;
} }
@ -1034,7 +1038,7 @@ namespace datalog {
var_subst vs(m, false); var_subst vs(m, false);
mk_subst(*rules[i], path, trace, sub); mk_subst(*rules[i], path, trace, sub);
rules[i]->to_formula(fml); rules[i]->to_formula(fml);
prs.push_back(m.mk_asserted(fml)); prs.push_back(rules[i]->get_proof());
unsigned sz = trace->get_num_args(); unsigned sz = trace->get_num_args();
if (sub.empty() && sz == 0) { if (sub.empty() && sz == 0) {
pr = prs[0].get(); pr = prs[0].get();
@ -1112,7 +1116,6 @@ namespace datalog {
} }
void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) { void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) {
proof_ref pr(m);
IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
md->eval(trace, trace); md->eval(trace, trace);
md->eval(path, path); md->eval(path, path);
@ -1120,7 +1123,11 @@ namespace datalog {
for (unsigned i = 0; i < b.m_solver.size(); ++i) { for (unsigned i = 0; i < b.m_solver.size(); ++i) {
verbose_stream() << mk_pp(b.m_solver.get_formulas()[i], m) << "\n"; verbose_stream() << mk_pp(b.m_solver.get_formulas()[i], m) << "\n";
}); });
b.m_answer = get_proof(md, to_app(trace), to_app(path)); scoped_proof _sp(m);
proof_ref pr(m);
pr = get_proof(md, to_app(trace), to_app(path));
apply(m, b.m_ctx.get_proof_converter().get(), pr);
b.m_answer = pr;
} }
}; };
@ -1155,6 +1162,9 @@ namespace datalog {
private: private:
void get_model(unsigned level) { void get_model(unsigned level) {
if (b.m_cancel) {
return;
}
rule_manager& rm = b.m_ctx.get_rule_manager(); rule_manager& rm = b.m_ctx.get_rule_manager();
expr_ref level_query = mk_level_predicate(b.m_query_pred, level); expr_ref level_query = mk_level_predicate(b.m_query_pred, level);
model_ref md; model_ref md;
@ -1212,7 +1222,7 @@ namespace datalog {
r1->to_formula(concl); r1->to_formula(concl);
scoped_proof _sp(m); scoped_proof _sp(m);
proof* p = m.mk_asserted(fml); proof* p = r->get_proof();
proof* premises[2] = { pr, p }; proof* premises[2] = { pr, p };
positions.push_back(std::make_pair(0, 1)); positions.push_back(std::make_pair(0, 1));
@ -1225,7 +1235,7 @@ namespace datalog {
else { else {
r2->to_formula(concl); r2->to_formula(concl);
scoped_proof _sp(m); scoped_proof _sp(m);
proof* p = m.mk_asserted(fml); proof* p = r->get_proof();
if (sub.empty()) { if (sub.empty()) {
pr = p; pr = p;
} }
@ -1245,7 +1255,7 @@ namespace datalog {
pred = r->get_decl(0); pred = r->get_decl(0);
} }
scoped_proof _sp(m); scoped_proof _sp(m);
apply(m, b.m_pc.get(), pr); apply(m, b.m_ctx.get_proof_converter().get(), pr);
b.m_answer = pr; b.m_answer = pr;
} }
@ -1409,6 +1419,7 @@ namespace datalog {
m_ctx.ensure_opened(); m_ctx.ensure_opened();
m_rules.reset(); m_rules.reset();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
datalog::rule_set old_rules(m_ctx.get_rules()); datalog::rule_set old_rules(m_ctx.get_rules());
datalog::rule_ref_vector query_rules(rule_manager); datalog::rule_ref_vector query_rules(rule_manager);
@ -1417,11 +1428,8 @@ namespace datalog {
m_ctx.add_rules(query_rules); m_ctx.add_rules(query_rules);
expr_ref bg_assertion = m_ctx.get_background_assertion(); expr_ref bg_assertion = m_ctx.get_background_assertion();
model_converter_ref mc = datalog::mk_skip_model_converter();
m_pc = datalog::mk_skip_proof_converter();
m_ctx.set_output_predicate(m_query_pred); m_ctx.set_output_predicate(m_query_pred);
m_ctx.set_model_converter(mc);
m_ctx.set_proof_converter(m_pc);
m_ctx.apply_default_transformation(); m_ctx.apply_default_transformation();
if (m_ctx.get_params().slice()) { if (m_ctx.get_params().slice()) {

1
src/muz_qe/dl_bmc_engine.h
View file

@ -39,7 +39,6 @@ namespace datalog {
func_decl_ref m_query_pred; func_decl_ref m_query_pred;
expr_ref m_answer; expr_ref m_answer;
volatile bool m_cancel; volatile bool m_cancel;
proof_converter_ref m_pc;
void checkpoint(); void checkpoint();

4
src/muz_qe/dl_cmds.cpp
View file

@ -262,8 +262,10 @@ public:
case datalog::OK: case datalog::OK:
break; break;
default: default:
UNREACHABLE(); // exception was raised.
break;
} }
break; break;
} }

32
src/muz_qe/dl_context.cpp
View file

@ -231,6 +231,7 @@ namespace datalog {
m_rule_set(*this), m_rule_set(*this),
m_rule_fmls(m), m_rule_fmls(m),
m_background(m), m_background(m),
m_mc(0),
m_closed(false), m_closed(false),
m_saturation_was_run(false), m_saturation_was_run(false),
m_last_answer(m), m_last_answer(m),
@ -474,8 +475,11 @@ namespace datalog {
void context::flush_add_rules() { void context::flush_add_rules() {
datalog::rule_manager& rm = get_rule_manager(); datalog::rule_manager& rm = get_rule_manager();
datalog::rule_ref_vector rules(rm); datalog::rule_ref_vector rules(rm);
scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED);
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]); expr* fml = m_rule_fmls[i].get();
proof* p = generate_proof_trace()?m.mk_asserted(fml):0;
rm.mk_rule(fml, p, rules, m_rule_names[i]);
} }
add_rules(rules); add_rules(rules);
m_rule_fmls.reset(); m_rule_fmls.reset();
@ -489,7 +493,11 @@ namespace datalog {
void context::update_rule(expr* rl, symbol const& name) { void context::update_rule(expr* rl, symbol const& name) {
datalog::rule_manager& rm = get_rule_manager(); datalog::rule_manager& rm = get_rule_manager();
datalog::rule_ref_vector rules(rm); datalog::rule_ref_vector rules(rm);
rm.mk_rule(rl, rules, name); proof* p = 0;
if (generate_proof_trace()) {
p = m.mk_asserted(rl);
}
rm.mk_rule(rl, p, rules, name);
if (rules.size() != 1) { if (rules.size() != 1) {
std::stringstream strm; std::stringstream strm;
strm << "Rule " << name << " has a non-trivial body. It cannot be modified"; strm << "Rule " << name << " has a non-trivial body. It cannot be modified";
@ -683,7 +691,7 @@ namespace datalog {
todo.push_back(e2); todo.push_back(e2);
} }
else if (is_quantifier(e)) { else if (is_quantifier(e)) {
todo.append(to_quantifier(e)->get_expr()); todo.push_back(to_quantifier(e)->get_expr());
} }
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
m.is_true(e1)) { m.is_true(e1)) {
@ -737,6 +745,9 @@ namespace datalog {
UNREACHABLE(); UNREACHABLE();
break; break;
} }
if (generate_proof_trace() && !r->get_proof()) {
m_rule_manager.mk_rule_asserted_proof(*r.get());
}
} }
void context::add_rule(rule_ref& r) { void context::add_rule(rule_ref& r) {
@ -847,7 +858,7 @@ namespace datalog {
void context::transform_rules(rule_transformer& transf) { void context::transform_rules(rule_transformer& transf) {
SASSERT(m_closed); //we must finish adding rules before we start transforming them SASSERT(m_closed); //we must finish adding rules before we start transforming them
TRACE("dl", display_rules(tout);); TRACE("dl", display_rules(tout););
if (transf(m_rule_set, m_mc, m_pc)) { if (transf(m_rule_set, m_mc)) {
//we have already ensured the negation is stratified and transformations //we have already ensured the negation is stratified and transformations
//should not break the stratification //should not break the stratification
m_rule_set.ensure_closed(); m_rule_set.ensure_closed();
@ -887,9 +898,9 @@ namespace datalog {
m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890)); m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890));
m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880)); m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880));
m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 34870));
m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 34860));
m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010)); m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 34850));
transform_rules(m_transf); transform_rules(m_transf);
} }
@ -1035,6 +1046,8 @@ namespace datalog {
} }
void context::new_query() { void context::new_query() {
m_mc = mk_skip_model_converter();
flush_add_rules(); flush_add_rules();
m_last_status = OK; m_last_status = OK;
m_last_answer = 0; m_last_answer = 0;
@ -1146,6 +1159,7 @@ namespace datalog {
switch(get_engine()) { switch(get_engine()) {
case DATALOG_ENGINE: case DATALOG_ENGINE:
return false; return false;
case PDR_ENGINE:
case QPDR_ENGINE: case QPDR_ENGINE:
ensure_pdr(); ensure_pdr();
m_pdr->display_certificate(out); m_pdr->display_certificate(out);
@ -1239,7 +1253,7 @@ namespace datalog {
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
get_free_vars(m_rule_fmls[i].get(), sorts); get_free_vars(m_rule_fmls[i].get(), sorts);
if (!sorts.empty()) { if (!sorts.empty()) {
rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]); rm.mk_rule(m_rule_fmls[i].get(), 0, rule_refs, m_rule_names[i]);
m_rule_fmls[i] = m_rule_fmls.back(); m_rule_fmls[i] = m_rule_fmls.back();
m_rule_names[i] = m_rule_names.back(); m_rule_names[i] = m_rule_names.back();
m_rule_fmls.pop_back(); m_rule_fmls.pop_back();
@ -1256,7 +1270,7 @@ namespace datalog {
} }
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
rules.push_back(m_rule_fmls[i].get()); rules.push_back(m_rule_fmls[i].get());
names.push_back(m_rule_names[i]); names.push_back(m_rule_names[i]);
} }
} }

13
src/muz_qe/dl_context.h
View file

@ -42,7 +42,6 @@ Revision History:
#include"params.h" #include"params.h"
#include"trail.h" #include"trail.h"
#include"model_converter.h" #include"model_converter.h"
#include"proof_converter.h"
#include"model2expr.h" #include"model2expr.h"
#include"smt_params.h" #include"smt_params.h"
#include"dl_rule_transformer.h" #include"dl_rule_transformer.h"
@ -142,6 +141,7 @@ namespace datalog {
var_subst & get_var_subst() { return m_var_subst; } var_subst & get_var_subst() { return m_var_subst; }
dl_decl_util & get_decl_util() { return m_decl_util; } dl_decl_util & get_decl_util() { return m_decl_util; }
bool generate_proof_trace() const { return m_params.generate_proof_trace(); }
bool output_profile() const { return m_params.output_profile(); } bool output_profile() const { return m_params.output_profile(); }
bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); } bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); }
symbol default_table() const { return m_params.default_table(); } symbol default_table() const { return m_params.default_table(); }
@ -315,14 +315,15 @@ namespace datalog {
void reopen(); void reopen();
void ensure_opened(); void ensure_opened();
void set_model_converter(model_converter_ref& mc) { m_mc = mc; } model_converter_ref& get_model_converter() { return m_mc; }
void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; } proof_converter_ref& get_proof_converter() { return m_pc; }
void add_proof_converter(proof_converter* pc) { m_pc = concat(m_pc.get(), pc); }
void transform_rules(); // model_converter_ref& mc, proof_converter_ref& pc); void transform_rules();
void transform_rules(rule_transformer& transf); // , model_converter_ref& mc, proof_converter_ref& pc); void transform_rules(rule_transformer& transf);
void replace_rules(rule_set & rs); void replace_rules(rule_set & rs);
void apply_default_transformation(); // model_converter_ref& mc, proof_converter_ref& pc); void apply_default_transformation();
void collect_params(param_descrs& r); void collect_params(param_descrs& r);

18
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -197,25 +197,18 @@ namespace datalog {
} }
fml2 = m.mk_implies(body, head); fml2 = m.mk_implies(body, head);
rm.mk_rule(fml2, new_rules, r.name()); proof_ref p(m);
rm.mk_rule(fml2, p, new_rules, r.name());
SASSERT(new_rules.size() == 1); SASSERT(new_rules.size() == 1);
TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n");); TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n"););
rules.add_rule(new_rules[0].get()); rules.add_rule(new_rules[0].get());
if (m_pc) { rm.mk_rule_rewrite_proof(r, *new_rules[0].get());
new_rules[0]->to_formula(fml2);
m_pc->insert(fml1, fml2);
}
return true; return true;
} }
rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc) {
ref<equiv_proof_converter> epc;
if (pc) {
epc = alloc(equiv_proof_converter, m);
}
m_pc = epc.get();
rule_set* rules = alloc(rule_set, m_ctx); rule_set* rules = alloc(rule_set, m_ctx);
rule_set::iterator it = source.begin(), end = source.end(); rule_set::iterator it = source.begin(), end = source.end();
@ -227,9 +220,6 @@ namespace datalog {
dealloc(rules); dealloc(rules);
rules = 0; rules = 0;
} }
if (pc) {
pc = concat(pc.get(), epc.get());
}
return rules; return rules;
} }

3
src/muz_qe/dl_mk_array_blast.h
View file

@ -37,7 +37,6 @@ namespace datalog {
rule_manager& rm; rule_manager& rm;
params_ref m_params; params_ref m_params;
th_rewriter m_rewriter; th_rewriter m_rewriter;
equiv_proof_converter* m_pc;
typedef obj_map<app, var*> defs_t; typedef obj_map<app, var*> defs_t;
@ -55,7 +54,7 @@ namespace datalog {
virtual ~mk_array_blast(); virtual ~mk_array_blast();
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };

119
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -21,7 +21,8 @@ Revision History:
#include "bit_blaster_rewriter.h" #include "bit_blaster_rewriter.h"
#include "rewriter_def.h" #include "rewriter_def.h"
#include "ast_pp.h" #include "ast_pp.h"
#include "expr_safe_replace.h"
#include "filter_model_converter.h"
namespace datalog { namespace datalog {
@ -35,6 +36,73 @@ namespace datalog {
// P(bv(x,y)) :- P_bv(x,y) // P(bv(x,y)) :- P_bv(x,y)
// Query // Query
// this model converter should be composed with a filter converter
// that gets rid of the new functions.
class bit_blast_model_converter : public model_converter {
ast_manager& m;
bv_util m_bv;
func_decl_ref_vector m_old_funcs;
func_decl_ref_vector m_new_funcs;
public:
bit_blast_model_converter(ast_manager& m):
m(m),
m_bv(m),
m_old_funcs(m),
m_new_funcs(m) {}
void insert(func_decl* old_f, func_decl* new_f) {
m_old_funcs.push_back(old_f);
m_new_funcs.push_back(new_f);
}
virtual model_converter * translate(ast_translation & translator) {
return alloc(bit_blast_model_converter, m);
}
virtual void operator()(model_ref & model) {
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();
func_interp* f = 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);
model->register_decl(p, f);
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();
}
unsigned idx = 0;
expr_ref arg(m), proj(m);
expr_safe_replace sub(m);
for (unsigned j = 0; j < arity_q; ++j) {
sort* s = q->get_domain(j);
arg = m.mk_var(j, s);
if (m_bv.is_bv_sort(s)) {
expr* args[1] = { arg };
unsigned sz = m_bv.get_bv_size(s);
for (unsigned k = 0; k < sz; ++k) {
proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args);
sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj);
}
}
else {
sub.insert(m.mk_var(idx++, s), arg);
}
}
sub(body);
g->set_else(body);
model->register_decl(q, g);
}
}
};
class expand_mkbv_cfg : public default_rewriter_cfg { class expand_mkbv_cfg : public default_rewriter_cfg {
@ -43,7 +111,8 @@ namespace datalog {
ast_manager& m; ast_manager& m;
bv_util m_util; bv_util m_util;
expr_ref_vector m_args, m_f_vars, m_g_vars; expr_ref_vector m_args, m_f_vars, m_g_vars;
func_decl_ref_vector m_pinned; func_decl_ref_vector m_old_funcs;
func_decl_ref_vector m_new_funcs;
obj_map<func_decl,func_decl*> m_pred2blast; obj_map<func_decl,func_decl*> m_pred2blast;
@ -57,10 +126,14 @@ namespace datalog {
m_args(m), m_args(m),
m_f_vars(m), m_f_vars(m),
m_g_vars(m), m_g_vars(m),
m_pinned(m) m_old_funcs(m),
m_new_funcs(m)
{} {}
~expand_mkbv_cfg() {} ~expand_mkbv_cfg() {}
func_decl_ref_vector const& old_funcs() const { return m_old_funcs; }
func_decl_ref_vector const& new_funcs() const { return m_new_funcs; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
rule_manager& rm = m_context.get_rule_manager(); rule_manager& rm = m_context.get_rule_manager();
@ -105,13 +178,18 @@ namespace datalog {
domain.push_back(m.get_sort(m_args[i].get())); domain.push_back(m.get_sort(m_args[i].get()));
} }
g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f); g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f);
m_pinned.push_back(g); m_old_funcs.push_back(f);
m_new_funcs.push_back(g);
m_pred2blast.insert(f, g); m_pred2blast.insert(f, g);
// Create rule f(mk_mkbv(args)) :- g(args) // Create rule f(mk_mkbv(args)) :- g(args)
fml = m.mk_implies(m.mk_app(g, m_g_vars.size(), m_g_vars.c_ptr()), m.mk_app(f, m_f_vars.size(), m_f_vars.c_ptr())); fml = m.mk_implies(m.mk_app(g, m_g_vars.size(), m_g_vars.c_ptr()), m.mk_app(f, m_f_vars.size(), m_f_vars.c_ptr()));
rm.mk_rule(fml, m_rules, g->get_name()); proof_ref pr(m);
if (m_context.generate_proof_trace()) {
pr = m.mk_asserted(fml); // or a def?
}
rm.mk_rule(fml, pr, m_rules, g->get_name());
} }
result = m.mk_app(g, m_args.size(), m_args.c_ptr()); result = m.mk_app(g, m_args.size(), m_args.c_ptr());
result_pr = 0; result_pr = 0;
@ -170,14 +248,11 @@ namespace datalog {
m_blaster.updt_params(m_params); m_blaster.updt_params(m_params);
} }
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc // TODO pc
if (!m_context.get_params().bit_blast()) { if (!m_context.get_params().bit_blast()) {
return 0; return 0;
} }
if (m_context.get_engine() != PDR_ENGINE) {
return 0;
}
rule_manager& rm = m_context.get_rule_manager(); rule_manager& rm = m_context.get_rule_manager();
unsigned sz = source.get_num_rules(); unsigned sz = source.get_num_rules();
expr_ref fml(m); expr_ref fml(m);
@ -185,9 +260,13 @@ namespace datalog {
rule_set * result = alloc(rule_set, m_context); rule_set * result = alloc(rule_set, m_context);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
rule * r = source.get_rule(i); rule * r = source.get_rule(i);
r->to_formula(fml); r->to_formula(fml);
if (blast(fml)) { if (blast(fml)) {
rm.mk_rule(fml, m_rules, r->name()); proof_ref pr(m);
if (m_context.generate_proof_trace()) {
pr = m.mk_asserted(fml); // loses original proof of r.
}
rm.mk_rule(fml, pr, m_rules, r->name());
} }
else { else {
m_rules.push_back(r); m_rules.push_back(r);
@ -197,6 +276,18 @@ namespace datalog {
for (unsigned i = 0; i < m_rules.size(); ++i) { for (unsigned i = 0; i < m_rules.size(); ++i) {
result->add_rule(m_rules.get(i)); result->add_rule(m_rules.get(i));
} }
if (mc) {
filter_model_converter* fmc = alloc(filter_model_converter, m);
bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m);
func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs();
func_decl_ref_vector const& new_funcs = m_rewriter.m_cfg.new_funcs();
for (unsigned i = 0; i < old_funcs.size(); ++i) {
fmc->insert(new_funcs[i]);
bvmc->insert(old_funcs[i], new_funcs[i]);
}
mc = concat(mc.get(), concat(bvmc, fmc));
}
return result; return result;
} }
@ -210,8 +301,8 @@ namespace datalog {
dealloc(m_impl); dealloc(m_impl);
} }
rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc) {
return (*m_impl)(source, mc, pc); return (*m_impl)(source, mc);
} }
}; };

2
src/muz_qe/dl_mk_bit_blast.h
View file

@ -44,7 +44,7 @@ namespace datalog {
mk_bit_blast(context & ctx, unsigned priority = 35000); mk_bit_blast(context & ctx, unsigned priority = 35000);
~mk_bit_blast(); ~mk_bit_blast();
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

20
src/muz_qe/dl_mk_coalesce.cpp
View file

@ -133,7 +133,7 @@ namespace datalog {
tail.push_back(to_app(fml)); tail.push_back(to_app(fml));
is_neg.push_back(false); is_neg.push_back(false);
res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name()); res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name());
if (m_pc) { if (m_ctx.generate_proof_trace()) {
src.to_formula(fml1); src.to_formula(fml1);
tgt->to_formula(fml2); tgt->to_formula(fml2);
res->to_formula(fml); res->to_formula(fml);
@ -142,12 +142,13 @@ namespace datalog {
sort* domain[3] = { ps, ps, m.mk_bool_sort() }; sort* domain[3] = { ps, ps, m.mk_bool_sort() };
func_decl* merge = m.mk_func_decl(symbol("merge-clauses"), 3, domain, ps); // TBD: ad-hoc proof rule func_decl* merge = m.mk_func_decl(symbol("merge-clauses"), 3, domain, ps); // TBD: ad-hoc proof rule
expr* args[3] = { m.mk_asserted(fml1), m.mk_asserted(fml2), fml }; expr* args[3] = { m.mk_asserted(fml1), m.mk_asserted(fml2), fml };
m_pc->insert(m.mk_app(merge, 3, args)); // ...m_pc->insert(m.mk_app(merge, 3, args));
#else #else
svector<std::pair<unsigned, unsigned> > pos; svector<std::pair<unsigned, unsigned> > pos;
vector<expr_ref_vector> substs; vector<expr_ref_vector> substs;
proof* p = m.mk_asserted(fml1); proof* p = src.get_proof();
m_pc->insert(m.mk_hyper_resolve(1, &p, fml, pos, substs)); p = m.mk_hyper_resolve(1, &p, fml, pos, substs);
res->set_proof(m, p);
#endif #endif
} }
tgt = res; tgt = res;
@ -170,13 +171,7 @@ namespace datalog {
return true; return true;
} }
rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc) {
m_pc = 0;
ref<replace_proof_converter> rpc;
if (pc) {
rpc = alloc(replace_proof_converter, m);
m_pc = rpc.get();
}
rule_set* rules = alloc(rule_set, m_ctx); rule_set* rules = alloc(rule_set, m_ctx);
rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules(); rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
for (; it != end; ++it) { for (; it != end; ++it) {
@ -195,9 +190,6 @@ namespace datalog {
rules->add_rule(r1.get()); rules->add_rule(r1.get());
} }
} }
if (pc) {
pc = concat(pc.get(), rpc.get());
}
return rules; return rules;
} }

3
src/muz_qe/dl_mk_coalesce.h
View file

@ -37,7 +37,6 @@ namespace datalog {
rule_manager& rm; rule_manager& rm;
expr_ref_vector m_sub1, m_sub2; expr_ref_vector m_sub1, m_sub2;
unsigned m_idx; unsigned m_idx;
replace_proof_converter* m_pc;
void mk_pred(app_ref& pred, app* p1, app* p2); void mk_pred(app_ref& pred, app* p1, app* p2);
@ -53,7 +52,7 @@ namespace datalog {
*/ */
mk_coalesce(context & ctx); mk_coalesce(context & ctx);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

3
src/muz_qe/dl_mk_coi_filter.cpp
View file

@ -35,8 +35,7 @@ namespace datalog {
rule_set * mk_coi_filter::operator()( rule_set * mk_coi_filter::operator()(
rule_set const & source, rule_set const & source,
model_converter_ref& mc, model_converter_ref& mc)
proof_converter_ref& pc)
{ {
if (source.get_num_rules()==0) { if (source.get_num_rules()==0) {
return 0; return 0;

3
src/muz_qe/dl_mk_coi_filter.h
View file

@ -40,8 +40,7 @@ namespace datalog {
rule_set * operator()(rule_set const & source, rule_set * operator()(rule_set const & source,
model_converter_ref& mc, model_converter_ref& mc);
proof_converter_ref& pc);
}; };
}; };

4
src/muz_qe/dl_mk_explanations.cpp
View file

@ -875,8 +875,8 @@ namespace datalog {
} }
} }
rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc) {
SASSERT(!mc && !pc); SASSERT(!mc);
if(source.get_num_rules()==0) { if(source.get_num_rules()==0) {
return 0; return 0;
} }

2
src/muz_qe/dl_mk_explanations.h
View file

@ -82,7 +82,7 @@ namespace datalog {
return get_union_decl(m_context); return get_union_decl(m_context);
} }
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
static expr* get_explanation(relation_base const& r); static expr* get_explanation(relation_base const& r);
}; };

12
src/muz_qe/dl_mk_extract_quantifiers.cpp
View file

@ -168,7 +168,15 @@ namespace datalog {
fml = m.mk_implies(m.mk_and(fmls.size(), fmls.c_ptr()), r.get_head()); fml = m.mk_implies(m.mk_and(fmls.size(), fmls.c_ptr()), r.get_head());
TRACE("dl", tout << "new rule\n" << mk_pp(fml, m) << "\n";); TRACE("dl", tout << "new rule\n" << mk_pp(fml, m) << "\n";);
rule_ref_vector rules(rm); rule_ref_vector rules(rm);
rm.mk_rule(fml, rules, r.name()); proof_ref pr(m);
if (m_ctx.generate_proof_trace()) {
scoped_proof _scp(m);
expr_ref fml1(m);
r.to_formula(fml1);
pr = m.mk_rewrite(fml1, fml);
pr = m.mk_modus_ponens(r.get_proof(), pr);
}
rm.mk_rule(fml, pr, rules, r.name());
for (unsigned i = 0; i < rules.size(); ++i) { for (unsigned i = 0; i < rules.size(); ++i) {
new_rules.add_rule(rules[i].get()); new_rules.add_rule(rules[i].get());
m_quantifiers.insert(rules[i].get(), alloc(quantifier_ref_vector, qs)); m_quantifiers.insert(rules[i].get(), alloc(quantifier_ref_vector, qs));
@ -347,7 +355,7 @@ namespace datalog {
m_quantifiers.reset(); m_quantifiers.reset();
} }
rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc) {
reset(); reset();
rule_set::iterator it = source.begin(), end = source.end(); rule_set::iterator it = source.begin(), end = source.end();
for (; !m_has_quantifiers && it != end; ++it) { for (; !m_has_quantifiers && it != end; ++it) {

2
src/muz_qe/dl_mk_extract_quantifiers.h
View file

@ -77,7 +77,7 @@ namespace datalog {
void set_query(func_decl* q); void set_query(func_decl* q);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
bool has_quantifiers() { return m_has_quantifiers; } bool has_quantifiers() { return m_has_quantifiers; }

6
src/muz_qe/dl_mk_filter_rules.cpp
View file

@ -90,6 +90,7 @@ namespace datalog {
rule * filter_rule = m_context.get_rule_manager().mk(filter_head, 1, &filter_tail, (const bool *)0); rule * filter_rule = m_context.get_rule_manager().mk(filter_head, 1, &filter_tail, (const bool *)0);
filter_rule->set_accounting_parent_object(m_context, m_current); filter_rule->set_accounting_parent_object(m_context, m_current);
m_result->add_rule(filter_rule); m_result->add_rule(filter_rule);
m_context.get_rule_manager().mk_rule_asserted_proof(*filter_rule);
} }
else { else {
dealloc(key); dealloc(key);
@ -135,12 +136,13 @@ namespace datalog {
} }
new_is_negated.push_back(r->is_neg_tail(i)); new_is_negated.push_back(r->is_neg_tail(i));
} }
if(rule_modified) { if (rule_modified) {
remove_duplicate_tails(new_tail, new_is_negated); remove_duplicate_tails(new_tail, new_is_negated);
SASSERT(new_tail.size() == new_is_negated.size()); SASSERT(new_tail.size() == new_is_negated.size());
rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr()); rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr());
new_rule->set_accounting_parent_object(m_context, m_current); new_rule->set_accounting_parent_object(m_context, m_current);
m_result->add_rule(new_rule); m_result->add_rule(new_rule);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule);
m_modified = true; m_modified = true;
} }
else { else {
@ -148,7 +150,7 @@ namespace datalog {
} }
} }
rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc // TODO mc, pc
m_tail2filter.reset(); m_tail2filter.reset();
m_result = alloc(rule_set, m_context); m_result = alloc(rule_set, m_context);

2
src/muz_qe/dl_mk_filter_rules.h
View file

@ -72,7 +72,7 @@ namespace datalog {
/** /**
\brief Return a new rule set where only filter rules contain atoms with repeated variables and/or values. \brief Return a new rule set where only filter rules contain atoms with repeated variables and/or values.
*/ */
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

7
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -554,11 +554,13 @@ namespace datalog {
bool mk_interp_tail_simplifier::transform_rules(const rule_set & orig, rule_set & tgt) { bool mk_interp_tail_simplifier::transform_rules(const rule_set & orig, rule_set & tgt) {
bool modified = false; bool modified = false;
rule_manager& rm = m_context.get_rule_manager();
rule_set::iterator rit = orig.begin(); rule_set::iterator rit = orig.begin();
rule_set::iterator rend = orig.end(); rule_set::iterator rend = orig.end();
for (; rit!=rend; ++rit) { for (; rit!=rend; ++rit) {
rule_ref new_rule(m_context.get_rule_manager()); rule_ref new_rule(rm);
if (transform_rule(*rit, new_rule)) { if (transform_rule(*rit, new_rule)) {
rm.mk_rule_rewrite_proof(**rit, *new_rule.get());
bool is_modified = *rit != new_rule; bool is_modified = *rit != new_rule;
modified |= is_modified; modified |= is_modified;
tgt.add_rule(new_rule); tgt.add_rule(new_rule);
@ -570,8 +572,7 @@ namespace datalog {
return modified; return modified;
} }
rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc
if (source.get_num_rules() == 0) { if (source.get_num_rules() == 0) {
return 0; return 0;
} }

2
src/muz_qe/dl_mk_interp_tail_simplifier.h
View file

@ -93,7 +93,7 @@ namespace datalog {
*/ */
bool transform_rule(rule * r, rule_ref& res); bool transform_rule(rule * r, rule_ref& res);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

5
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -310,7 +310,7 @@ namespace datalog {
m_hb.reset(); m_hb.reset();
for (unsigned i = 0; i < src.size(); ++i) { for (unsigned i = 0; i < src.size(); ++i) {
vector<rational> v(src.A[i]); vector<rational> v(src.A[i]);
v.append(src.b[i]); v.push_back(src.b[i]);
if (src.eq[i]) { if (src.eq[i]) {
m_hb.add_eq(v, rational(0)); m_hb.add_eq(v, rational(0));
} }
@ -420,6 +420,7 @@ namespace datalog {
new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name()); new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name());
} }
rules.add_rule(new_rule); rules.add_rule(new_rule);
rm.mk_rule_rewrite_proof(r, *new_rule); // should be weakening rule.
} }
class mk_karr_invariants::add_invariant_model_converter : public model_converter { class mk_karr_invariants::add_invariant_model_converter : public model_converter {
@ -519,7 +520,7 @@ namespace datalog {
m_hb.set_cancel(true); m_hb.set_cancel(true);
} }
rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc) {
if (!m_ctx.get_params().karr()) { if (!m_ctx.get_params().karr()) {
return 0; return 0;
} }

2
src/muz_qe/dl_mk_karr_invariants.h
View file

@ -69,7 +69,7 @@ namespace datalog {
virtual void cancel(); virtual void cancel();
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };

4
src/muz_qe/dl_mk_magic_sets.cpp
View file

@ -317,8 +317,8 @@ namespace datalog {
m_rules.push_back(r); m_rules.push_back(r);
} }
rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc) {
SASSERT(!mc && !pc); SASSERT(!mc);
unsigned init_rule_cnt = source.get_num_rules(); unsigned init_rule_cnt = source.get_num_rules();
{ {
func_decl_set intentional; func_decl_set intentional;

2
src/muz_qe/dl_mk_magic_sets.h
View file

@ -121,7 +121,7 @@ namespace datalog {
*/ */
mk_magic_sets(context & ctx, rule * goal_rule); mk_magic_sets(context & ctx, rule * goal_rule);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

4
src/muz_qe/dl_mk_partial_equiv.cpp
View file

@ -86,8 +86,8 @@ namespace datalog {
} }
rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc // TODO mc
if (source.get_num_rules() == 0) { if (source.get_num_rules() == 0) {
return 0; return 0;

2
src/muz_qe/dl_mk_partial_equiv.h
View file

@ -35,7 +35,7 @@ namespace datalog {
m(ctx.get_manager()), m(ctx.get_manager()),
m_context(ctx) {} m_context(ctx) {}
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
private: private:

14
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -181,10 +181,10 @@ namespace datalog {
} }
if (m_unifier.apply(tgt, tail_index, src, res)) { if (m_unifier.apply(tgt, tail_index, src, res)) {
if (m_pc) { if (m_context.generate_proof_trace()) {
expr_ref_vector s1 = m_unifier.get_rule_subst(tgt, true); expr_ref_vector s1 = m_unifier.get_rule_subst(tgt, true);
expr_ref_vector s2 = m_unifier.get_rule_subst(src, false); expr_ref_vector s2 = m_unifier.get_rule_subst(src, false);
datalog::resolve_rule(m_pc, tgt, src, tail_index, s1, s2, *res.get()); datalog::resolve_rule(tgt, src, tail_index, s1, s2, *res.get());
} }
return true; return true;
} }
@ -837,11 +837,10 @@ namespace datalog {
return done_something; return done_something;
} }
rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc) {
bool something_done = false; bool something_done = false;
ref<horn_subsume_model_converter> hsmc; ref<horn_subsume_model_converter> hsmc;
ref<replace_proof_converter> hpc;
if (source.get_num_rules() == 0) { if (source.get_num_rules() == 0) {
return 0; return 0;
@ -858,11 +857,7 @@ namespace datalog {
if (mc) { if (mc) {
hsmc = alloc(horn_subsume_model_converter, m); hsmc = alloc(horn_subsume_model_converter, m);
} }
if (pc) {
hpc = alloc(replace_proof_converter, m);
}
m_mc = hsmc.get(); m_mc = hsmc.get();
m_pc = hpc.get();
scoped_ptr<rule_set> res = alloc(rule_set, m_context); scoped_ptr<rule_set> res = alloc(rule_set, m_context);
@ -889,9 +884,6 @@ namespace datalog {
if (mc) { if (mc) {
mc = concat(mc.get(), hsmc.get()); mc = concat(mc.get(), hsmc.get());
} }
if (pc) {
pc = concat(pc.get(), hpc.get());
}
} }
return res.detach(); return res.detach();

4
src/muz_qe/dl_mk_rule_inliner.h
View file

@ -114,7 +114,6 @@ namespace datalog {
ast_counter m_tail_pred_ctr; ast_counter m_tail_pred_ctr;
rule_set m_inlined_rules; rule_set m_inlined_rules;
horn_subsume_model_converter* m_mc; horn_subsume_model_converter* m_mc;
replace_proof_converter* m_pc;
//used in try_to_inline_rule and do_eager_inlining //used in try_to_inline_rule and do_eager_inlining
@ -188,7 +187,6 @@ namespace datalog {
m_pinned(m_rm), m_pinned(m_rm),
m_inlined_rules(m_context), m_inlined_rules(m_context),
m_mc(0), m_mc(0),
m_pc(0),
m_unifier(ctx), m_unifier(ctx),
m_head_index(m), m_head_index(m),
m_tail_index(m), m_tail_index(m),
@ -198,7 +196,7 @@ namespace datalog {
{} {}
virtual ~mk_rule_inliner() { } virtual ~mk_rule_inliner() { }
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

4
src/muz_qe/dl_mk_similarity_compressor.cpp
View file

@ -500,8 +500,8 @@ namespace datalog {
} }
} }
rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc // TODO mc
m_modified = false; m_modified = false;
unsigned init_rule_cnt = source.get_num_rules(); unsigned init_rule_cnt = source.get_num_rules();
SASSERT(m_rules.empty()); SASSERT(m_rules.empty());

2
src/muz_qe/dl_mk_similarity_compressor.h
View file

@ -69,7 +69,7 @@ namespace datalog {
public: public:
mk_similarity_compressor(context & ctx, unsigned threshold_count); mk_similarity_compressor(context & ctx, unsigned threshold_count);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

9
src/muz_qe/dl_mk_simple_joins.cpp
View file

@ -706,19 +706,20 @@ namespace datalog {
negs.c_ptr()); negs.c_ptr());
new_rule->set_accounting_parent_object(m_context, orig_r); new_rule->set_accounting_parent_object(m_context, orig_r);
m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule);
result->add_rule(new_rule); result->add_rule(new_rule);
} }
while(!m_introduced_rules.empty()) { while (!m_introduced_rules.empty()) {
result->add_rule(m_introduced_rules.back()); result->add_rule(m_introduced_rules.back());
m_context.get_rule_manager().mk_rule_asserted_proof(*m_introduced_rules.back());
m_introduced_rules.pop_back(); m_introduced_rules.pop_back();
} }
return result; return result;
} }
}; };
rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc // TODO mc
rule_set rs_aux_copy(m_context); rule_set rs_aux_copy(m_context);
rs_aux_copy.add_rules(source); rs_aux_copy.add_rules(source);
if(!rs_aux_copy.is_closed()) { if(!rs_aux_copy.is_closed()) {

2
src/muz_qe/dl_mk_simple_joins.h
View file

@ -53,7 +53,7 @@ namespace datalog {
public: public:
mk_simple_joins(context & ctx); mk_simple_joins(context & ctx);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

15
src/muz_qe/dl_mk_slice.cpp
View file

@ -164,10 +164,8 @@ namespace datalog {
TRACE("dl", tout << "does not have fact\n" << mk_pp(fact, m) << "\n";); TRACE("dl", tout << "does not have fact\n" << mk_pp(fact, m) << "\n";);
return false; return false;
} }
expr_ref fml(m);
proof_ref new_p(m); proof_ref new_p(m);
r->to_formula(fml); new_p = r->get_proof();
new_p = m.mk_asserted(fml);
m_pinned_exprs.push_back(new_p); m_pinned_exprs.push_back(new_p);
m_todo.pop_back(); m_todo.pop_back();
m_new_proof.insert(p, new_p); m_new_proof.insert(p, new_p);
@ -784,6 +782,9 @@ namespace datalog {
rm.fix_unbound_vars(new_rule, false); rm.fix_unbound_vars(new_rule, false);
TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n");); TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n"););
if (m_ctx.generate_proof_trace()) {
rm.mk_rule_asserted_proof(*new_rule.get());
}
} }
else { else {
new_rule = &r; new_rule = &r;
@ -801,7 +802,7 @@ namespace datalog {
} }
} }
rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc) {
for (unsigned i = 0; i < src.get_num_rules(); ++i) { for (unsigned i = 0; i < src.get_num_rules(); ++i) {
if (src.get_rule(i)->has_quantifiers()) { if (src.get_rule(i)->has_quantifiers()) {
return 0; return 0;
@ -809,8 +810,8 @@ namespace datalog {
} }
ref<slice_proof_converter> spc; ref<slice_proof_converter> spc;
ref<slice_model_converter> smc; ref<slice_model_converter> smc;
if (pc) { if (m_ctx.generate_proof_trace()) {
spc = alloc(slice_proof_converter, m_ctx); spc = alloc(slice_proof_converter, m_ctx);
} }
if (mc) { if (mc) {
smc = alloc(slice_model_converter, *this, m); smc = alloc(slice_model_converter, *this, m);
@ -834,7 +835,7 @@ namespace datalog {
m_mc->add_sliceable(it->m_key, it->m_value); m_mc->add_sliceable(it->m_key, it->m_value);
} }
} }
pc = concat(pc.get(), spc.get()); m_ctx.add_proof_converter(spc.get());
mc = concat(mc.get(), smc.get()); mc = concat(mc.get(), smc.get());
return result; return result;
} }

2
src/muz_qe/dl_mk_slice.h
View file

@ -102,7 +102,7 @@ namespace datalog {
virtual ~mk_slice() { } virtual ~mk_slice() { }
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; } func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; }

13
src/muz_qe/dl_mk_subsumption_checker.cpp
View file

@ -166,7 +166,8 @@ namespace datalog {
res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
res->set_accounting_parent_object(m_context, r); res->set_accounting_parent_object(m_context, r);
m_context.get_rule_manager().fix_unbound_vars(res, true); m_context.get_rule_manager().fix_unbound_vars(res, true);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get());
return true; return true;
} }
@ -208,10 +209,10 @@ namespace datalog {
continue; continue;
} }
rule * defining_rule; rule * defining_rule;
TRUSTME(m_total_relation_defining_rules.find(head_pred, defining_rule)); VERIFY(m_total_relation_defining_rules.find(head_pred, defining_rule));
if(defining_rule) { if (defining_rule) {
rule_ref totality_rule(m_context.get_rule_manager()); rule_ref totality_rule(m_context.get_rule_manager());
TRUSTME(transform_rule(defining_rule, subs_index, totality_rule)); VERIFY(transform_rule(defining_rule, subs_index, totality_rule));
if(defining_rule!=totality_rule) { if(defining_rule!=totality_rule) {
modified = true; modified = true;
} }
@ -331,8 +332,8 @@ namespace datalog {
} }
} }
rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc // TODO mc
m_have_new_total_rule = false; m_have_new_total_rule = false;
collect_ground_unconditional_rule_heads(source); collect_ground_unconditional_rule_heads(source);

2
src/muz_qe/dl_mk_subsumption_checker.h
View file

@ -84,7 +84,7 @@ namespace datalog {
reset_dealloc_values(m_ground_unconditional_rule_heads); reset_dealloc_values(m_ground_unconditional_rule_heads);
} }
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

5
src/muz_qe/dl_mk_unbound_compressor.cpp
View file

@ -238,6 +238,7 @@ namespace datalog {
unsigned new_rule_index = m_rules.size(); unsigned new_rule_index = m_rules.size();
m_rules.push_back(new_rule); m_rules.push_back(new_rule);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule.get());
m_head_occurrence_ctr.inc(new_rule->get_head()->get_decl()); m_head_occurrence_ctr.inc(new_rule->get_head()->get_decl());
@ -333,8 +334,8 @@ namespace datalog {
} }
} }
rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc) {
// TODO mc, pc // TODO mc
m_modified = false; m_modified = false;
m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels); m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);

2
src/muz_qe/dl_mk_unbound_compressor.h
View file

@ -82,7 +82,7 @@ namespace datalog {
public: public:
mk_unbound_compressor(context & ctx); mk_unbound_compressor(context & ctx);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

15
src/muz_qe/dl_mk_unfold.cpp
View file

@ -42,29 +42,20 @@ namespace datalog {
if (m_unify.unify_rules(r, tail_idx, r2) && if (m_unify.unify_rules(r, tail_idx, r2) &&
m_unify.apply(r, tail_idx, r2, new_rule)) { m_unify.apply(r, tail_idx, r2, new_rule)) {
expr_ref_vector s1 = m_unify.get_rule_subst(r, true); expr_ref_vector s1 = m_unify.get_rule_subst(r, true);
expr_ref_vector s2 = m_unify.get_rule_subst(r2, false); expr_ref_vector s2 = m_unify.get_rule_subst(r2, false);
resolve_rule(m_pc, r, r2, tail_idx, s1, s2, *new_rule.get()); resolve_rule(r, r2, tail_idx, s1, s2, *new_rule.get());
expand_tail(*new_rule.get(), tail_idx+r2.get_uninterpreted_tail_size(), src, dst); expand_tail(*new_rule.get(), tail_idx+r2.get_uninterpreted_tail_size(), src, dst);
} }
} }
} }
} }
rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc) {
m_pc = 0;
ref<replace_proof_converter> rpc;
if (pc) {
rpc = alloc(replace_proof_converter, m);
m_pc = rpc.get();
}
rule_set* rules = alloc(rule_set, m_ctx); rule_set* rules = alloc(rule_set, m_ctx);
rule_set::iterator it = source.begin(), end = source.end(); rule_set::iterator it = source.begin(), end = source.end();
for (; it != end; ++it) { for (; it != end; ++it) {
expand_tail(**it, 0, source, *rules); expand_tail(**it, 0, source, *rules);
} }
if (pc) {
pc = concat(pc.get(), rpc.get());
}
return rules; return rules;
} }

3
src/muz_qe/dl_mk_unfold.h
View file

@ -35,7 +35,6 @@ namespace datalog {
ast_manager& m; ast_manager& m;
rule_manager& rm; rule_manager& rm;
rule_unifier m_unify; rule_unifier m_unify;
replace_proof_converter* m_pc;
void expand_tail(rule& r, unsigned tail_idx, rule_set const& src, rule_set& dst); void expand_tail(rule& r, unsigned tail_idx, rule_set const& src, rule_set& dst);
@ -45,7 +44,7 @@ namespace datalog {
*/ */
mk_unfold(context & ctx); mk_unfold(context & ctx);
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); rule_set * operator()(rule_set const & source, model_converter_ref& mc);
}; };
}; };

333
src/muz_qe/dl_rule.cpp
View file

@ -42,13 +42,13 @@ Revision History:
#include"bool_rewriter.h" #include"bool_rewriter.h"
#include"qe_lite.h" #include"qe_lite.h"
#include"expr_safe_replace.h" #include"expr_safe_replace.h"
#include"hnf.h"
namespace datalog { namespace datalog {
rule_manager::rule_manager(context& ctx) rule_manager::rule_manager(context& ctx)
: m(ctx.get_manager()), : m(ctx.get_manager()),
m_ctx(ctx), m_ctx(ctx) {}
m_refs(ctx.get_manager()) {}
bool rule_manager::is_predicate(func_decl * f) const { bool rule_manager::is_predicate(func_decl * f) const {
return m_ctx.is_predicate(f); return m_ctx.is_predicate(f);
@ -89,72 +89,32 @@ namespace datalog {
} }
}; };
void rule_manager::remove_labels(expr_ref& fml) { void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) {
expr_ref tmp(m); expr_ref tmp(m);
remove_label_cfg r_cfg(m); remove_label_cfg r_cfg(m);
rewriter_tpl<remove_label_cfg> rwr(m, false, r_cfg); rewriter_tpl<remove_label_cfg> rwr(m, false, r_cfg);
rwr(fml, tmp); rwr(fml, tmp);
if (pr && fml != tmp) {
pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
}
fml = tmp; fml = tmp;
} }
void rule_manager::mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name) { void rule_manager::mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name) {
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
proof_ref pr(p, m);
expr_ref fml1(m); expr_ref fml1(m);
m_memoize_disj.reset();
m_refs.reset();
bind_variables(fml, true, fml1); bind_variables(fml, true, fml1);
remove_labels(fml1); if (fml1 != fml && pr) {
mk_rule_core(fml1, rules, name); pr = m.mk_asserted(fml1);
}
remove_labels(fml1, pr);
mk_rule_core_new(fml1, pr, rules, name);
} }
void rule_manager::mk_negations(app_ref_vector& body, svector<bool>& is_negated) {
void rule_manager::mk_rule_core(expr* _fml, rule_ref_vector& rules, symbol const& name) {
app_ref_vector body(m);
app_ref head(m);
expr_ref e(m), fml(_fml, m);
svector<bool> is_negated;
TRACE("dl_rule", tout << mk_pp(fml, m) << "\n";);
quantifier_hoister qh(m);
unsigned index = qh.pull_quantifier(true, fml, 0);
check_app(fml);
head = to_app(fml);
while (m.is_implies(head)) {
e = head->get_arg(0);
th_rewriter th_rwr(m);
th_rwr(e);
body.push_back(ensure_app(e));
e = to_app(head)->get_arg(1);
check_app(e);
head = to_app(e.get());
}
symbol head_name = (name == symbol::null)?head->get_decl()->get_name():name;
flatten_body(body);
if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) {
app* _or = to_app(body[0].get());
for (unsigned i = 0; i < _or->get_num_args(); ++i) {
e = m.mk_implies(_or->get_arg(i), head);
mk_rule_core(e, rules, head_name);
}
return;
}
eliminate_disjunctions(body, rules, head_name);
eliminate_quantifier_body(body, rules, head_name);
hoist_compound(index, head, body);
unsigned sz = body.size();
for (unsigned i = 0; i < sz; ++i) {
app_ref b(body[i].get(), m);
hoist_compound(index, b, body);
body[i] = b;
}
TRACE("dl_rule",
tout << mk_pp(head, m) << " :- ";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << " ";
}
tout << "\n";);
for (unsigned i = 0; i < body.size(); ++i) { for (unsigned i = 0; i < body.size(); ++i) {
expr* e = body[i].get(), *e1; expr* e = body[i].get(), *e1;
if (m.is_not(e, e1) && is_predicate(e1)) { if (m.is_not(e, e1) && is_predicate(e1)) {
@ -165,23 +125,105 @@ namespace datalog {
else { else {
is_negated.push_back(false); is_negated.push_back(false);
} }
} }
check_valid_rule(head, body.size(), body.c_ptr()); }
rules.push_back(mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name)); void rule_manager::mk_rule_core_new(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name) {
hnf h(m);
if (m_ctx.fix_unbound_vars()) { expr_ref_vector fmls(m);
unsigned rule_cnt = rules.size(); proof_ref_vector prs(m);
for (unsigned i=0; i<rule_cnt; ++i) { h.set_name(name);
rule_ref r(rules[i].get(), *this); h(fml, p, fmls, prs);
fix_unbound_vars(r, true); for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) {
if (r.get()!=rules[i].get()) { m_ctx.register_predicate(h.get_fresh_predicates()[i]);
rules[i] = r; }
} for (unsigned i = 0; i < fmls.size(); ++i) {
} mk_rule_core2(fmls[i].get(), prs[i].get(), rules, name);
} }
} }
void rule_manager::mk_rule_core2(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name) {
app_ref_vector body(m);
app_ref head(m);
svector<bool> is_negated;
unsigned index = extract_horn(fml, body, head);
hoist_compound_predicates(index, head, body);
TRACE("dl_rule",
tout << mk_pp(head, m) << " :- ";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << " ";
}
tout << "\n";);
mk_negations(body, is_negated);
check_valid_rule(head, body.size(), body.c_ptr());
rule_ref r(*this);
r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name);
expr_ref fml1(m);
if (p) {
r->to_formula(fml1);
if (fml1 == fml) {
// no-op.
}
else if (is_quantifier(fml1)) {
p = m.mk_modus_ponens(p, m.mk_symmetry(m.mk_der(to_quantifier(fml1), fml)));
}
else {
p = m.mk_modus_ponens(p, m.mk_rewrite(fml, fml1));
}
}
if (m_ctx.fix_unbound_vars()) {
fix_unbound_vars(r, true);
}
if (p) {
expr_ref fml2(m);
r->to_formula(fml2);
if (fml1 != fml2) {
p = m.mk_modus_ponens(p, m.mk_rewrite(fml1, fml2));
}
r->set_proof(m, p);
}
rules.push_back(r);
}
unsigned rule_manager::extract_horn(expr* fml, app_ref_vector& body, app_ref& head) {
expr* e1, *e2;
unsigned index = m_counter.get_next_var(fml);
if (::is_forall(fml)) {
index += to_quantifier(fml)->get_num_decls();
fml = to_quantifier(fml)->get_expr();
}
if (m.is_implies(fml, e1, e2)) {
expr_ref_vector es(m);
head = ensure_app(e2);
datalog::flatten_and(e1, es);
for (unsigned i = 0; i < es.size(); ++i) {
body.push_back(ensure_app(es[i].get()));
}
}
else {
head = ensure_app(fml);
}
return index;
}
void rule_manager::hoist_compound_predicates(unsigned index, app_ref& head, app_ref_vector& body) {
unsigned sz = body.size();
hoist_compound(index, head, body);
for (unsigned i = 0; i < sz; ++i) {
app_ref b(body[i].get(), m);
hoist_compound(index, b, body);
body[i] = b;
}
}
void rule_manager::mk_query(expr* query, func_decl_ref& qpred, rule_ref_vector& query_rules, rule_ref& query_rule) { void rule_manager::mk_query(expr* query, func_decl_ref& qpred, rule_ref_vector& query_rules, rule_ref& query_rule) {
ptr_vector<sort> vars; ptr_vector<sort> vars;
svector<symbol> names; svector<symbol> names;
@ -192,7 +234,7 @@ namespace datalog {
// Remove existential prefix. // Remove existential prefix.
bind_variables(query, false, q); bind_variables(query, false, q);
quantifier_hoister qh(m); quantifier_hoister qh(m);
qh.pull_quantifier(false, q, &names); qh.pull_quantifier(false, q, 0, &names);
// retrieve free variables. // retrieve free variables.
get_free_vars(q, vars); get_free_vars(q, vars);
if (vars.contains(static_cast<sort*>(0))) { if (vars.contains(static_cast<sort*>(0))) {
@ -250,7 +292,12 @@ namespace datalog {
rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl); rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl);
} }
mk_rule(rule_expr, query_rules); scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
proof_ref pr(m);
if (m_ctx.generate_proof_trace()) {
pr = m.mk_asserted(rule_expr);
}
mk_rule(rule_expr, pr, query_rules);
SASSERT(query_rules.size() >= 1); SASSERT(query_rules.size() >= 1);
query_rule = query_rules.back(); query_rule = query_rules.back();
} }
@ -330,73 +377,6 @@ namespace datalog {
return false; return false;
} }
void rule_manager::eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) {
app* b = body.get();
expr* e1;
bool negate_args = false;
bool is_disj = false;
unsigned num_disj = 0;
expr* const* disjs = 0;
if (!contains_predicate(b)) {
return;
}
TRACE("dl_rule", tout << mk_ismt2_pp(b, m) << "\n";);
if (m.is_or(b)) {
is_disj = true;
negate_args = false;
num_disj = b->get_num_args();
disjs = b->get_args();
}
if (m.is_not(b, e1) && m.is_and(e1)) {
is_disj = true;
negate_args = true;
num_disj = to_app(e1)->get_num_args();
disjs = to_app(e1)->get_args();
}
if (is_disj) {
ptr_vector<sort> sorts0, sorts1;
get_free_vars(b, sorts0);
expr_ref_vector args(m);
for (unsigned i = 0; i < sorts0.size(); ++i) {
if (sorts0[i]) {
args.push_back(m.mk_var(i,sorts0[i]));
sorts1.push_back(sorts0[i]);
}
}
app* old_head = 0;
if (m_memoize_disj.find(b, old_head)) {
body = old_head;
}
else {
app_ref head(m);
func_decl_ref f(m);
f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort());
m_ctx.register_predicate(f);
head = m.mk_app(f, args.size(), args.c_ptr());
for (unsigned i = 0; i < num_disj; ++i) {
expr_ref fml(m);
expr* e = disjs[i];
if (negate_args) e = m.mk_not(e);
fml = m.mk_implies(e,head);
mk_rule_core(fml, rules, name);
}
m_memoize_disj.insert(b, head);
m_refs.push_back(b);
m_refs.push_back(head);
// update the body to be the newly introduced head relation
body = head;
}
}
}
void rule_manager::eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) {
for (unsigned i = 0; i < body.size(); ++i) {
app_ref_vector::element_ref t = body[i];
eliminate_disjunctions(t, rules, name);
}
}
bool rule_manager::is_forall(ast_manager& m, expr* e, quantifier*& q) { bool rule_manager::is_forall(ast_manager& m, expr* e, quantifier*& q) {
expr* e1, *e2; expr* e1, *e2;
@ -415,40 +395,6 @@ namespace datalog {
return false; return false;
} }
void rule_manager::eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) {
quantifier* q;
if (is_forall(m, body.get(), q) && contains_predicate(q)) {
expr* e = q->get_expr();
if (!is_predicate(e)) {
ptr_vector<sort> sorts0, sorts1;
get_free_vars(e, sorts0);
expr_ref_vector args(m);
for (unsigned i = 0; i < sorts0.size(); ++i) {
if (sorts0[i]) {
args.push_back(m.mk_var(i,sorts0[i]));
sorts1.push_back(sorts0[i]);
}
}
app_ref head(m), fml(m);
func_decl_ref f(m);
f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort());
m_ctx.register_predicate(f);
head = m.mk_app(f, args.size(), args.c_ptr());
fml = m.mk_implies(e, head);
mk_rule_core(fml, rules, name);
// update the body to be the newly introduced head relation
body = m.mk_eq(m.mk_true(), m.update_quantifier(q, head));
}
}
}
void rule_manager::eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) {
for (unsigned i = 0; i < body.size(); ++i) {
app_ref_vector::element_ref t = body[i];
eliminate_quantifier_body(t, rules, name);
}
}
app_ref rule_manager::ensure_app(expr* e) { app_ref rule_manager::ensure_app(expr* e) {
SASSERT(m.is_bool(e)); SASSERT(m.is_bool(e));
@ -476,6 +422,7 @@ namespace datalog {
r->m_head = head; r->m_head = head;
r->m_name = name; r->m_name = name;
r->m_tail_size = n; r->m_tail_size = n;
r->m_proof = 0;
m.inc_ref(r->m_head); m.inc_ref(r->m_head);
app * * uninterp_tail = r->m_tail; //grows upwards app * * uninterp_tail = r->m_tail; //grows upwards
@ -533,6 +480,11 @@ namespace datalog {
if (normalize) { if (normalize) {
r->norm_vars(*this); r->norm_vars(*this);
} }
DEBUG_CODE(ptr_vector<sort> sorts;
::get_free_vars(head, sorts);
for (unsigned i = 0; i < n; ++i) {
::get_free_vars(tail[i], sorts);
});
return r; return r;
} }
@ -754,6 +706,27 @@ namespace datalog {
r->set_accounting_parent_object(m_ctx, old_r); r->set_accounting_parent_object(m_ctx, old_r);
} }
void rule_manager::mk_rule_rewrite_proof(rule& old_rule, rule& new_rule) {
if (&old_rule != &new_rule &&
!new_rule.get_proof() &&
old_rule.get_proof()) {
expr_ref fml(m);
new_rule.to_formula(fml);
scoped_proof _sc(m);
proof* p = m.mk_rewrite(m.get_fact(old_rule.get_proof()), fml);
new_rule.set_proof(m, m.mk_modus_ponens(old_rule.get_proof(), p));
}
}
void rule_manager::mk_rule_asserted_proof(rule& r) {
if (m_ctx.generate_proof_trace()) {
scoped_proof _scp(m);
expr_ref fml(m);
r.to_formula(fml);
r.set_proof(m, m.mk_asserted(fml));
}
}
void rule_manager::substitute(rule_ref& r, unsigned sz, expr*const* es) { void rule_manager::substitute(rule_ref& r, unsigned sz, expr*const* es) {
expr_ref tmp(m); expr_ref tmp(m);
app_ref new_head(m); app_ref new_head(m);
@ -812,10 +785,23 @@ namespace datalog {
for (unsigned i = 0; i < n; i++) { for (unsigned i = 0; i < n; i++) {
m.dec_ref(get_tail(i)); m.dec_ref(get_tail(i));
} }
if (m_proof) {
m.dec_ref(m_proof);
}
this->~rule(); this->~rule();
m.get_allocator().deallocate(get_obj_size(n), this); m.get_allocator().deallocate(get_obj_size(n), this);
} }
void rule::set_proof(ast_manager& m, proof* p) {
if (p) {
m.inc_ref(p);
}
if (m_proof) {
m.dec_ref(m_proof);
}
m_proof = p;
}
bool rule::is_in_tail(const func_decl * p, bool only_positive) const { bool rule::is_in_tail(const func_decl * p, bool only_positive) const {
unsigned len = only_positive ? get_positive_tail_size() : get_uninterpreted_tail_size(); unsigned len = only_positive ? get_positive_tail_size() : get_uninterpreted_tail_size();
for (unsigned i = 0; i < len; i++) { for (unsigned i = 0; i < len; i++) {
@ -993,6 +979,9 @@ namespace datalog {
out << '}'; out << '}';
} }
out << '\n'; out << '\n';
if (m_proof) {
out << mk_pp(m_proof, m) << '\n';
}
} }
void rule::to_formula(expr_ref& fml) const { void rule::to_formula(expr_ref& fml) const {

45
src/muz_qe/dl_rule.h
View file

@ -43,11 +43,9 @@ namespace datalog {
*/ */
class rule_manager class rule_manager
{ {
ast_manager& m; ast_manager& m;
context& m_ctx; context& m_ctx;
rule_counter m_counter; rule_counter m_counter;
obj_map<expr, app*> m_memoize_disj;
expr_ref_vector m_refs;
// only the context can create a rule_manager // only the context can create a rule_manager
friend class context; friend class context;
@ -57,19 +55,13 @@ namespace datalog {
/** /**
\brief Move functions from predicate tails into the interpreted tail by introducing new variables. \brief Move functions from predicate tails into the interpreted tail by introducing new variables.
*/ */
void hoist_compound_predicates(unsigned num_bound, app_ref& head, app_ref_vector& body);
void hoist_compound(unsigned& num_bound, app_ref& fml, app_ref_vector& body); void hoist_compound(unsigned& num_bound, app_ref& fml, app_ref_vector& body);
void flatten_body(app_ref_vector& body); void flatten_body(app_ref_vector& body);
void remove_labels(expr_ref& fml); void remove_labels(expr_ref& fml, proof_ref& pr);
void eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name);
void eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name);
void eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name);
void eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name);
app_ref ensure_app(expr* e); app_ref ensure_app(expr* e);
@ -81,6 +73,16 @@ namespace datalog {
void mk_rule_core(expr* fml, rule_ref_vector& rules, symbol const& name); void mk_rule_core(expr* fml, rule_ref_vector& rules, symbol const& name);
void mk_negations(app_ref_vector& body, svector<bool>& is_negated);
void mk_rule_core_new(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name);
void mk_rule_core2(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name);
static expr_ref mk_implies(app_ref_vector const& body, expr* head);
unsigned extract_horn(expr* fml, app_ref_vector& body, app_ref& head);
/** /**
\brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail. \brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail.
*/ */
@ -99,7 +101,7 @@ namespace datalog {
The formula is of the form (forall (...) (forall (...) (=> (and ...) head))) The formula is of the form (forall (...) (forall (...) (=> (and ...) head)))
*/ */
void mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name = symbol::null); void mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name = symbol::null);
/** /**
\brief Create a Datalog query from an expression. \brief Create a Datalog query from an expression.
@ -129,7 +131,15 @@ namespace datalog {
/** make sure there are not non-quantified variables that occur only in interpreted predicates */ /** make sure there are not non-quantified variables that occur only in interpreted predicates */
void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination); void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination);
/**
\brief add proof that new rule is obtained by rewriting old rule.
*/
void mk_rule_rewrite_proof(rule& old_rule, rule& new_rule);
/**
\brief tag rule as asserted.
*/
void mk_rule_asserted_proof(rule& r);
/** /**
\brief apply substitution to variables of rule. \brief apply substitution to variables of rule.
@ -168,6 +178,7 @@ namespace datalog {
friend class rule_manager; friend class rule_manager;
app * m_head; app * m_head;
proof* m_proof;
unsigned m_tail_size:20; unsigned m_tail_size:20;
// unsigned m_reserve:12; // unsigned m_reserve:12;
unsigned m_ref_cnt; unsigned m_ref_cnt;
@ -199,6 +210,10 @@ namespace datalog {
void get_used_vars(used_vars& uv) const; void get_used_vars(used_vars& uv) const;
public: public:
proof * get_proof() const { return m_proof; }
void set_proof(ast_manager& m, proof* p);
app * get_head() const { return m_head; } app * get_head() const { return m_head; }

4
src/muz_qe/dl_rule_transformer.cpp
View file

@ -73,7 +73,7 @@ namespace datalog {
m_dirty=true; m_dirty=true;
} }
bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc) { bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc) {
ensure_ordered(); ensure_ordered();
bool modified = false; bool modified = false;
@ -87,7 +87,7 @@ namespace datalog {
for(; it!=end && !m_cancel; ++it) { for(; it!=end && !m_cancel; ++it) {
plugin & p = **it; plugin & p = **it;
rule_set * new_rules = p(rules, mc, pc); rule_set * new_rules = p(rules, mc);
if (!new_rules) { if (!new_rules) {
continue; continue;
} }

6
src/muz_qe/dl_rule_transformer.h
View file

@ -24,7 +24,6 @@ Revision History:
#include"dl_rule.h" #include"dl_rule.h"
#include"dl_rule_set.h" #include"dl_rule_set.h"
#include"model_converter.h" #include"model_converter.h"
#include"proof_converter.h"
namespace datalog { namespace datalog {
@ -69,7 +68,7 @@ namespace datalog {
\brief Transform the rule set using the registered transformation plugins. If the rule \brief Transform the rule set using the registered transformation plugins. If the rule
set has changed, return true; otherwise return false. set has changed, return true; otherwise return false.
*/ */
bool operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc); bool operator()(rule_set & rules, model_converter_ref& mc);
}; };
class rule_transformer::plugin { class rule_transformer::plugin {
@ -106,8 +105,7 @@ namespace datalog {
The caller takes ownership of the returned \c rule_set object. The caller takes ownership of the returned \c rule_set object.
*/ */
virtual rule_set * operator()(rule_set const & source, virtual rule_set * operator()(rule_set const & source,
model_converter_ref& mc, model_converter_ref& mc) = 0;
proof_converter_ref& pc) = 0;
virtual void cancel() { m_cancel = true; } virtual void cancel() { m_cancel = true; }

38
src/muz_qe/dl_util.cpp
View file

@ -511,6 +511,44 @@ namespace datalog {
pc->insert(pr); pc->insert(pr);
} }
void resolve_rule(rule const& r1, rule const& r2, unsigned idx,
expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) {
if (!r1.get_proof()) {
return;
}
SASSERT(r2.get_proof());
ast_manager& m = s1.get_manager();
expr_ref fml(m);
res.to_formula(fml);
vector<expr_ref_vector> substs;
svector<std::pair<unsigned, unsigned> > positions;
substs.push_back(s1);
substs.push_back(s2);
scoped_proof _sc(m);
proof_ref pr(m);
proof_ref_vector premises(m);
premises.push_back(r1.get_proof());
premises.push_back(r2.get_proof());
positions.push_back(std::make_pair(idx+1, 0));
TRACE("dl",
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
for (unsigned i = 0; i < s1.size(); ++i) {
tout << mk_pp(s1[i], m) << " ";
}
tout << "\n";
tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
for (unsigned i = 0; i < s2.size(); ++i) {
tout << mk_pp(s2[i], m) << " ";
}
tout << "\n";
);
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs);
res.set_proof(m, pr);
}
class skip_model_converter : public model_converter { class skip_model_converter : public model_converter {
public: public:
skip_model_converter() {} skip_model_converter() {}

3
src/muz_qe/dl_util.h
View file

@ -425,6 +425,9 @@ namespace datalog {
void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx,
expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res); expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res);
void resolve_rule(rule const& r1, rule const& r2, unsigned idx,
expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res);
model_converter* mk_skip_model_converter(); model_converter* mk_skip_model_converter();
proof_converter* mk_skip_proof_converter(); proof_converter* mk_skip_proof_converter();

18
src/muz_qe/equiv_proof_converter.cpp
View file

@ -22,12 +22,14 @@ Revision History:
#include "dl_util.h" #include "dl_util.h"
void equiv_proof_converter::insert(expr* fml1, expr* fml2) { void equiv_proof_converter::insert(expr* fml1, expr* fml2) {
datalog::scoped_proof _sp(m); if (fml1 != fml2) {
proof_ref p1(m), p2(m), p3(m); datalog::scoped_proof _sp(m);
p1 = m.mk_asserted(fml1); proof_ref p1(m), p2(m), p3(m);
p2 = m.mk_rewrite(fml1, fml2); p1 = m.mk_asserted(fml1);
p3 = m.mk_modus_ponens(p1, p2); p2 = m.mk_rewrite(fml1, fml2);
TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";); p3 = m.mk_modus_ponens(p1, p2);
SASSERT(m.has_fact(p3)); TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";);
m_replace.insert(p3); SASSERT(m.has_fact(p3));
m_replace.insert(p3);
}
} }

14
src/muz_qe/horn_tactic.cpp
View file

@ -113,8 +113,8 @@ class horn_tactic : public tactic {
todo.append(to_app(a)->get_num_args(), to_app(a)->get_args()); todo.append(to_app(a)->get_num_args(), to_app(a)->get_args());
} }
else if (m.is_ite(a)) { else if (m.is_ite(a)) {
todo.append(to_app(a)->get_arg(1)); todo.push_back(to_app(a)->get_arg(1));
todo.append(to_app(a)->get_arg(2)); todo.push_back(to_app(a)->get_arg(2));
} }
else if (is_predicate(a)) { else if (is_predicate(a)) {
register_predicate(a); register_predicate(a);
@ -270,20 +270,10 @@ class horn_tactic : public tactic {
proof_converter_ref & pc) { proof_converter_ref & pc) {
expr_ref fml(m); expr_ref fml(m);
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
if (produce_models) {
mc = datalog::mk_skip_model_converter();
}
if (produce_proofs) {
pc = datalog::mk_skip_proof_converter();
}
func_decl* query_pred = to_app(q)->get_decl(); func_decl* query_pred = to_app(q)->get_decl();
m_ctx.set_output_predicate(query_pred); m_ctx.set_output_predicate(query_pred);
m_ctx.set_model_converter(mc);
m_ctx.set_proof_converter(pc);
m_ctx.get_rules(); // flush adding rules. m_ctx.get_rules(); // flush adding rules.
m_ctx.apply_default_transformation(); m_ctx.apply_default_transformation();

49
src/muz_qe/pdr_context.cpp
View file

@ -950,16 +950,45 @@ namespace pdr {
return out; return out;
} }
/**
\brief Ensure that all nodes in the tree have associated models.
get_trace and get_proof_trace rely on models to extract rules.
*/
void model_search::update_models() {
obj_map<expr, model*> models;
ptr_vector<model_node> todo;
todo.push_back(m_root);
while (!todo.empty()) {
model_node* n = todo.back();
if (n->get_model_ptr()) {
models.insert(n->state(), n->get_model_ptr());
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
}
todo.push_back(m_root);
while (!todo.empty()) {
model_node* n = todo.back();
model* md = 0;
if (!n->get_model_ptr() && models.find(n->state(), md)) {
model_ref mr(md);
n->set_model(mr);
}
todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr());
}
}
/** /**
Extract trace comprising of constraints Extract trace comprising of constraints
and predicates that are satisfied from facts to the query. and predicates that are satisfied from facts to the query.
The resulting trace The resulting trace
*/ */
expr_ref model_search::get_trace(context const& ctx) const { expr_ref model_search::get_trace(context const& ctx) {
pred_transformer& pt = get_root().pt(); pred_transformer& pt = get_root().pt();
ast_manager& m = pt.get_manager(); ast_manager& m = pt.get_manager();
manager& pm = pt.get_pdr_manager(); manager& pm = pt.get_pdr_manager();
datalog::context& dctx = ctx.get_context(); datalog::context& dctx = ctx.get_context();
datalog::rule_manager& rm = dctx.get_rule_manager(); datalog::rule_manager& rm = dctx.get_rule_manager();
expr_ref_vector constraints(m), predicates(m); expr_ref_vector constraints(m), predicates(m);
@ -974,13 +1003,15 @@ namespace pdr {
rule = n->get_rule(); rule = n->get_rule();
unsigned max_var = vc.get_max_rule_var(*rule); unsigned max_var = vc.get_max_rule_var(*rule);
predicates.push_back(rule->get_head()); predicates.push_back(rule->get_head());
children.append(n); children.push_back(n);
bool first = true; bool first = true;
update_models();
while (!children.empty()) { while (!children.empty()) {
SASSERT(children.size() == predicates.size()); SASSERT(children.size() == predicates.size());
expr_ref_vector binding(m); expr_ref_vector binding(m);
n = children.back(); n = children.back();
children.pop_back(); children.pop_back();
TRACE("pdr", n->display(tout, 0););
n->mk_instantiate(r0, rule, binding); n->mk_instantiate(r0, rule, binding);
max_var = std::max(max_var, vc.get_max_rule_var(*rule)); max_var = std::max(max_var, vc.get_max_rule_var(*rule));
@ -1026,7 +1057,7 @@ namespace pdr {
return pm.mk_and(constraints); return pm.mk_and(constraints);
} }
proof_ref model_search::get_proof_trace(context const& ctx) const { proof_ref model_search::get_proof_trace(context const& ctx) {
pred_transformer& pt = get_root().pt(); pred_transformer& pt = get_root().pt();
ast_manager& m = pt.get_manager(); ast_manager& m = pt.get_manager();
datalog::context& dctx = ctx.get_context(); datalog::context& dctx = ctx.get_context();
@ -1042,8 +1073,10 @@ namespace pdr {
proof* pr = 0; proof* pr = 0;
unifier.set_normalize(false); unifier.set_normalize(false);
todo.push_back(m_root); todo.push_back(m_root);
update_models();
while (!todo.empty()) { while (!todo.empty()) {
model_node* n = todo.back(); model_node* n = todo.back();
TRACE("pdr", n->display(tout, 0););
if (cache.find(n->state(), pr)) { if (cache.find(n->state(), pr)) {
todo.pop_back(); todo.pop_back();
continue; continue;
@ -1066,12 +1099,14 @@ namespace pdr {
continue; continue;
} }
proof_ref rl(m); proof_ref rl(m);
expr_ref fml0(m);
expr_ref_vector binding(m); expr_ref_vector binding(m);
n->mk_instantiate(r0, r1, binding); n->mk_instantiate(r0, r1, binding);
r0->to_formula(fml0);
proof_ref p1(m), p2(m); proof_ref p1(m), p2(m);
p1 = m.mk_asserted(fml0); p1 = r0->get_proof();
if (!p1) {
r0->display(dctx, std::cout);
}
SASSERT(p1);
pfs[0] = p1; pfs[0] = p1;
rls[0] = r1; rls[0] = r1;
TRACE("pdr", TRACE("pdr",

7
src/muz_qe/pdr_context.h
View file

@ -240,6 +240,7 @@ namespace pdr {
void erase_leaf(model_node& n); void erase_leaf(model_node& n);
void remove_node(model_node& n); void remove_node(model_node& n);
void enqueue_leaf(model_node& n); // add leaf to priority queue. void enqueue_leaf(model_node& n); // add leaf to priority queue.
void update_models();
public: public:
model_search(bool bfs): m_bfs(bfs), m_root(0) {} model_search(bool bfs): m_bfs(bfs), m_root(0) {}
~model_search(); ~model_search();
@ -253,8 +254,8 @@ namespace pdr {
void set_root(model_node* n); void set_root(model_node* n);
model_node& get_root() const { return *m_root; } model_node& get_root() const { return *m_root; }
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
expr_ref get_trace(context const& ctx) const; expr_ref get_trace(context const& ctx);
proof_ref get_proof_trace(context const& ctx) const; proof_ref get_proof_trace(context const& ctx);
void backtrack_level(bool uses_level, model_node& n); void backtrack_level(bool uses_level, model_node& n);
}; };
@ -299,7 +300,7 @@ namespace pdr {
decl2rel m_rels; // Map from relation predicate to fp-operator. decl2rel m_rels; // Map from relation predicate to fp-operator.
func_decl_ref m_query_pred; func_decl_ref m_query_pred;
pred_transformer* m_query; pred_transformer* m_query;
model_search m_search; mutable model_search m_search;
lbool m_last_result; lbool m_last_result;
unsigned m_inductive_lvl; unsigned m_inductive_lvl;
ptr_vector<core_generalizer> m_core_generalizers; ptr_vector<core_generalizer> m_core_generalizers;

13
src/muz_qe/pdr_dl_interface.cpp
View file

@ -85,6 +85,7 @@ lbool dl_interface::query(expr * query) {
m_pred2slice.reset(); m_pred2slice.reset();
ast_manager& m = m_ctx.get_manager(); ast_manager& m = m_ctx.get_manager();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
datalog::rule_set old_rules(m_ctx.get_rules()); datalog::rule_set old_rules(m_ctx.get_rules());
func_decl_ref query_pred(m); func_decl_ref query_pred(m);
datalog::rule_ref_vector query_rules(rule_manager); datalog::rule_ref_vector query_rules(rule_manager);
@ -105,14 +106,8 @@ lbool dl_interface::query(expr * query) {
m_ctx.display_rules(tout); m_ctx.display_rules(tout);
); );
model_converter_ref mc = datalog::mk_skip_model_converter();
proof_converter_ref pc;
if (m_ctx.get_params().generate_proof_trace()) {
pc = datalog::mk_skip_proof_converter();
}
m_ctx.set_output_predicate(query_pred); m_ctx.set_output_predicate(query_pred);
m_ctx.set_model_converter(mc);
m_ctx.set_proof_converter(pc);
m_ctx.apply_default_transformation(); m_ctx.apply_default_transformation();
if (m_ctx.get_params().slice()) { if (m_ctx.get_params().slice()) {
@ -164,8 +159,8 @@ lbool dl_interface::query(expr * query) {
datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode. datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode.
m_context->set_proof_converter(pc); m_context->set_proof_converter(m_ctx.get_proof_converter());
m_context->set_model_converter(mc); m_context->set_model_converter(m_ctx.get_model_converter());
m_context->set_query(query_pred); m_context->set_query(query_pred);
m_context->set_axioms(bg_assertion); m_context->set_axioms(bg_assertion);
m_context->update_rules(m_pdr_rules); m_context->update_rules(m_pdr_rules);

6
src/muz_qe/pdr_generalizers.cpp
View file

@ -228,11 +228,13 @@ namespace pdr {
is_lower = !is_lower; is_lower = !is_lower;
} }
vector<term_loc_t> bound;
bound.push_back(std::make_pair(x, i));
if (is_lower) { if (is_lower) {
m_lb.insert(abs(r), std::make_pair(x, i)); m_lb.insert(abs(r), bound);
} }
else { else {
m_ub.insert(abs(r), std::make_pair(x, i)); m_ub.insert(abs(r), bound);
} }
} }

8
src/muz_qe/qe_lite.cpp
View file

@ -2492,7 +2492,13 @@ class qe_lite_tactic : public tactic {
new_f = f; new_f = f;
m_qe(new_f, new_pr); m_qe(new_f, new_pr);
if (produce_proofs) { if (produce_proofs) {
new_pr = m.mk_modus_ponens(g->pr(i), new_pr); expr* fact = m.get_fact(new_pr);
if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) {
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
}
else {
new_pr = g->pr(i);
}
} }
g->update(i, new_f, new_pr, g->dep(i)); g->update(i, new_f, new_pr, g->dep(i));
} }

13
src/muz_qe/tab_context.cpp
View file

@ -1644,9 +1644,7 @@ namespace datalog {
void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2, void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2,
expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const { expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const {
unsigned idx = r1.get_predicate_index(); unsigned idx = r1.get_predicate_index();
expr_ref fml1 = r1.to_formula(); expr_ref fml = res.to_formula();
expr_ref fml2 = r2.to_formula();
expr_ref fml3 = res.to_formula();
vector<expr_ref_vector> substs; vector<expr_ref_vector> substs;
svector<std::pair<unsigned, unsigned> > positions; svector<std::pair<unsigned, unsigned> > positions;
substs.push_back(s1); substs.push_back(s1);
@ -1654,13 +1652,12 @@ namespace datalog {
scoped_proof _sc(m); scoped_proof _sc(m);
proof_ref pr(m); proof_ref pr(m);
proof_ref_vector premises(m); proof_ref_vector premises(m);
premises.push_back(m.mk_asserted(fml1)); premises.push_back(m.mk_asserted(r1.to_formula()));
premises.push_back(m.mk_asserted(fml2)); premises.push_back(m.mk_asserted(r2.to_formula()));
positions.push_back(std::make_pair(idx+1, 0)); positions.push_back(std::make_pair(idx+1, 0));
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs); pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs);
pc.insert(pr); pc.insert(pr);
} }
}; };
tab::tab(context& ctx): tab::tab(context& ctx):

17
src/util/vector.h
View file

@ -151,23 +151,6 @@ public:
} }
} }
vector(T const & e) :
m_data(0) {
push_back(e);
}
vector(T const & t1, T const & t2) :
m_data(0) {
push_back(t1);
push_back(t2);
}
vector(T const & t1, T const & t2, T const & t3) :
m_data(0) {
push_back(t1);
push_back(t2);
push_back(t3);
}
~vector() { ~vector() {
destroy(); destroy();