mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix to proof hypothesis removal facility reported by Arie Gurfinkel

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-28 16:40:29 -08:00
parent 1dfea1324e
commit 9f2743309f
4 changed files with 65 additions and 311 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

290
src/muz_qe/dl_mk_extract_quantifiers2.cpp
View file

@ -31,9 +31,7 @@ namespace datalog {
m_ctx(ctx), m_ctx(ctx),
m(ctx.get_manager()), m(ctx.get_manager()),
rm(ctx.get_rule_manager()), rm(ctx.get_rule_manager()),
m_query_pred(m), m_query_pred(m)
m_quantifiers(m),
m_refs(m)
{} {}
mk_extract_quantifiers2::~mk_extract_quantifiers2() { mk_extract_quantifiers2::~mk_extract_quantifiers2() {
@ -44,135 +42,16 @@ namespace datalog {
m_query_pred = q; m_query_pred = q;
} }
bool mk_extract_quantifiers2::matches_signature(func_decl* head, expr_ref_vector const& binding) {
unsigned sz = head->get_arity();
if (sz != binding.size()) {
return false;
}
for (unsigned i = 0; i < sz; ++i) {
if (head->get_domain(i) != m.get_sort(binding[sz-i-1])) {
return false;
}
}
return true;
}
bool mk_extract_quantifiers2::matches_quantifier(quantifier* q, expr_ref_vector const& binding) {
unsigned sz = q->get_num_decls();
if (sz != binding.size()) {
return false;
}
for (unsigned i = 0; i < sz; ++i) {
if (q->get_decl_sort(i) != m.get_sort(binding[sz-i-1])) {
return false;
}
}
return true;
}
bool mk_extract_quantifiers2::mk_abstract_expr(expr_ref& term) {
if (!is_app(term)) {
return false;
}
expr* r;
if (m_map.find(term, r)) {
term = r;
return true;
}
if (to_app(term)->get_family_id() == null_family_id) {
return false;
}
expr_ref_vector args(m);
expr_ref tmp(m);
for (unsigned i = 0; i < to_app(term)->get_num_args(); ++i) {
tmp = to_app(term)->get_arg(i);
if (!mk_abstract_expr(tmp)) {
return false;
}
args.push_back(tmp);
}
tmp = m.mk_app(to_app(term)->get_decl(), args.size(), args.c_ptr());
m_refs.push_back(tmp);
m_map.insert(term, tmp);
term = tmp;
return true;
}
bool mk_extract_quantifiers2::mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result) {
for (unsigned i = 0; i < binding.size(); ++i) {
expr_ref tmp(m);
tmp = binding[i];
if (!mk_abstract_expr(tmp)) {
return false;
}
result.push_back(tmp);
}
return true;
}
void mk_extract_quantifiers2::mk_abstraction_map(rule& r, expr_ref_vector const& binding) {
m_map.reset();
unsigned sz = binding.size();
SASSERT(sz == r.get_decl()->get_arity());
for (unsigned i = 0; i < sz; ++i) {
m_map.insert(binding[sz-i-1], r.get_head()->get_arg(i));
SASSERT(m.get_sort(binding[sz-i-1]) == m.get_sort(r.get_head()->get_arg(i)));
}
// todo: also make bindings for variables in rule body.
}
void mk_extract_quantifiers2::match_bindings(unsigned i, unsigned j, unsigned k) {
expr_ref_vector resb(m);
rule* r = m_qrules[i];
quantifier* q = m_quantifiers[i].get();
expr_ref_vector const& ruleb = m_rule_bindings[i][j];
expr_ref_vector const& quantb = m_quantifier_bindings[i][k];
mk_abstraction_map(*r, ruleb);
if (!mk_abstract_binding(quantb, resb)) {
return;
}
expr_ref inst(m), tmp(m);
var_shifter shift(m);
for (unsigned l = 0; l < resb.size(); ++l) {
tmp = resb[l].get();
shift(tmp, q->get_num_decls(), tmp);
resb[l] = tmp;
}
instantiate(m, q, resb.c_ptr(), inst);
if (!m_seen.contains(r)) {
m_seen.insert(r, alloc(obj_hashtable<expr>));
}
obj_hashtable<expr>& seen = *m_seen.find(r);
if (seen.contains(inst)) {
return;
}
seen.insert(inst);
m_refs.push_back(inst);
if (!m_quantifier_instantiations.contains(r, q)) {
m_quantifier_instantiations.insert(r, q, alloc(expr_ref_vector, m));
}
expr_ref_vector* vec = 0;
VERIFY(m_quantifier_instantiations.find(r, q, vec));
vec->push_back(inst);
TRACE("dl", tout << "matched: " << mk_pp(q, m) << "\n" << mk_pp(inst, m) << "\n";);
}
app_ref mk_extract_quantifiers2::ensure_app(expr* e) {
if (is_app(e)) {
return app_ref(to_app(e), m);
}
else {
return app_ref(m.mk_eq(e, m.mk_true()), m);
}
}
/*
*
*
*/
void mk_extract_quantifiers2::extract(rule& r, rule_set& new_rules) { void mk_extract_quantifiers2::extract(rule& r, rule_set& new_rules) {
unsigned utsz = r.get_uninterpreted_tail_size(); unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size(); unsigned tsz = r.get_tail_size();
bool has_quantifier = false;
expr_ref_vector conjs(m); expr_ref_vector conjs(m);
quantifier_ref_vector qs(m);
for (unsigned i = utsz; i < tsz; ++i) { for (unsigned i = utsz; i < tsz; ++i) {
conjs.push_back(r.get_tail(i)); conjs.push_back(r.get_tail(i));
} }
@ -181,112 +60,27 @@ namespace datalog {
expr* e = conjs[j].get(); expr* e = conjs[j].get();
quantifier* q; quantifier* q;
if (rule_manager::is_forall(m, e, q)) { if (rule_manager::is_forall(m, e, q)) {
m_quantifiers.push_back(q); qs.push_back(q);
m_qrules.push_back(&r);
m_rule_bindings.push_back(vector<expr_ref_vector>());
m_quantifier_bindings.push_back(vector<expr_ref_vector>());
has_quantifier = true;
} }
} }
if (!has_quantifier) { if (qs.empty()) {
new_rules.add_rule(&r); new_rules.add_rule(&r);
} }
} else {
m_quantifiers.insert(&r, new quantifier_ref_vector(qs));
void mk_extract_quantifiers2::apply(rule& r, rule_set& new_rules) { // TODO
expr_ref_vector tail(m), conjs(m);
expr_ref fml(m);
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
for (unsigned i = 0; i < utsz; ++i) {
SASSERT(!r.is_neg_tail(i));
tail.push_back(r.get_tail(i));
}
bool has_quantifier = false;
for (unsigned i = utsz; i < tsz; ++i) {
conjs.push_back(r.get_tail(i));
}
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)) {
expr_ref_vector* ls;
if (m_quantifier_instantiations.find(&r,q,ls)) {
tail.append(*ls);
}
has_quantifier = true;
}
else {
tail.push_back(e);
}
}
if (has_quantifier) {
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head());
rule_ref_vector rules(rm);
rm.mk_rule(fml, rules, r.name());
for (unsigned i = 0; i < rules.size(); ++i) {
new_rules.add_rule(rules[i].get());
}
} }
} }
#if 0
class mk_extract_quantifiers2::instance_plugin : public smt::quantifier_instance_plugin {
mk_extract_quantifiers2& ex;
ast_manager& m;
expr_ref_vector m_refs;
obj_hashtable<expr> m_bindings;
public:
instance_plugin(mk_extract_quantifiers2& ex): ex(ex), m(ex.m), m_refs(m) {}
virtual void operator()(quantifier* q, unsigned num_bindings, smt::enode*const* bindings) {
expr_ref_vector binding(m);
ptr_vector<sort> sorts;
for (unsigned i = 0; i < num_bindings; ++i) {
binding.push_back(bindings[i]->get_owner());
sorts.push_back(m.get_sort(binding[i].get()));
}
func_decl* f = m.mk_func_decl(symbol("T"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort());
expr_ref tup(m);
tup = m.mk_app(f, binding.size(), binding.c_ptr());
if (!m_bindings.contains(tup)) {
m_bindings.insert(tup);
m_refs.push_back(tup);
ex.m_bindings.push_back(binding);
TRACE("dl", tout << "insert\n" << mk_pp(q, m) << "\n" << mk_pp(tup, m) << "\n";);
}
}
};
#endif
void mk_extract_quantifiers2::reset() { void mk_extract_quantifiers2::reset() {
{ obj_map<rule const, quantifier_ref_vector*>::iterator it = m_quantifiers.begin(),
obj_pair_map<rule,quantifier, expr_ref_vector*>::iterator end = m_quantifiers.end();
it = m_quantifier_instantiations.begin(), for (; it != end; ++it) {
end = m_quantifier_instantiations.end(); dealloc(it->m_value);
for (; it != end; ++it) {
dealloc(it->get_value());
}
} }
{
obj_map<rule,obj_hashtable<expr>*>::iterator
it = m_seen.begin(),
end = m_seen.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
}
m_quantifier_instantiations.reset();
m_seen.reset();
m_has_quantifiers = false; m_has_quantifiers = false;
m_quantifiers.reset(); m_quantifiers.reset();
m_qrules.reset();
m_bindings.reset();
m_rule_bindings.reset();
m_quantifier_bindings.reset();
m_refs.reset();
} }
rule_set * mk_extract_quantifiers2::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { rule_set * mk_extract_quantifiers2::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
@ -305,60 +99,6 @@ namespace datalog {
extract(**it, *rules); extract(**it, *rules);
} }
bmc bmc(m_ctx);
expr_ref_vector fmls(m);
unsigned depth = 2;
// TBD: use cancel_eh to terminate without base-case.
for (unsigned i = 0; i <= depth; ++i) {
bmc.compile(source, fmls, i);
}
expr_ref query = bmc.compile_query(m_query_pred, depth);
fmls.push_back(query);
smt_params fparams;
fparams.m_relevancy_lvl = 0;
fparams.m_model = true;
fparams.m_model_compact = true;
fparams.m_mbqi = false;
smt::kernel solver(m, fparams);
TRACE("dl",
for (unsigned i = 0; i < fmls.size(); ++i) {
tout << mk_pp(fmls[i].get(), m) << "\n";
});
for (unsigned i = 0; i < fmls.size(); ++i) {
solver.assert_expr(fmls[i].get());
}
#if 0
smt::context& ctx = solver.get_context();
smt::quantifier_manager* qm = ctx.get_quantifier_manager();
qm->get_plugin()->set_instance_plugin(alloc(instance_plugin, *this));
#endif
solver.check();
for (unsigned i = 0; i < m_bindings.size(); ++i) {
expr_ref_vector& binding = m_bindings[i];
for (unsigned j = 0; j < m_qrules.size(); ++j) {
rule* r = m_qrules[j];
if (matches_signature(r->get_decl(), binding)) {
m_rule_bindings[j].push_back(binding);
}
else if (matches_quantifier(m_quantifiers[j].get(), binding)) {
m_quantifier_bindings[j].push_back(binding);
}
}
}
for (unsigned i = 0; i < m_qrules.size(); ++i) {
for (unsigned j = 0; j < m_rule_bindings[i].size(); ++j) {
for (unsigned k = 0; k < m_quantifier_bindings[i].size(); ++k) {
match_bindings(i, j, k);
}
}
}
it = source.begin();
for (; it != end; ++it) {
apply(**it, *rules);
}
return rules; return rules;
} }

41
src/muz_qe/dl_mk_extract_quantifiers2.h
View file

@ -31,44 +31,17 @@ namespace datalog {
\brief Extract universal quantifiers from rules. \brief Extract universal quantifiers from rules.
*/ */
class mk_extract_quantifiers2 : public rule_transformer::plugin { class mk_extract_quantifiers2 : public rule_transformer::plugin {
context& m_ctx; context& m_ctx;
ast_manager& m; ast_manager& m;
rule_manager& rm; rule_manager& rm;
func_decl_ref m_query_pred; func_decl_ref m_query_pred;
quantifier_ref_vector m_quantifiers; bool m_has_quantifiers;
ptr_vector<rule> m_qrules; obj_map<rule const, quantifier_ref_vector*> m_quantifiers;
vector<expr_ref_vector>m_bindings;
vector<vector<expr_ref_vector> > m_rule_bindings;
vector<vector<expr_ref_vector> > m_quantifier_bindings;
obj_pair_map<rule,quantifier, expr_ref_vector*> m_quantifier_instantiations;
obj_map<rule, obj_hashtable<expr>*> m_seen;
bool m_has_quantifiers;
obj_map<expr,expr*> m_map;
expr_ref_vector m_refs;
class instance_plugin;
void reset(); void reset();
void extract(rule& r, rule_set& new_rules); void extract(rule& r, rule_set& new_rules);
void apply(rule& r, rule_set& new_rules);
app_ref ensure_app(expr* e);
bool matches_signature(func_decl* head, expr_ref_vector const& binding);
bool matches_quantifier(quantifier* q, expr_ref_vector const& binding);
void match_bindings(unsigned i, unsigned j, unsigned k);
bool mk_abstract_expr(expr_ref& term);
bool mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result);
void mk_abstraction_map(rule& r, expr_ref_vector const& binding);
public: public:
/** /**
\brief Create rule transformer that extracts universal quantifiers (over recursive predicates). \brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
@ -83,6 +56,8 @@ namespace datalog {
bool has_quantifiers() { return m_has_quantifiers; } bool has_quantifiers() { return m_has_quantifiers; }
obj_map<rule const, quantifier_ref_vector*>& quantifiers() { return m_quantifiers; }
}; };
}; };

4
src/muz_qe/pdr_dl_interface.cpp
View file

@ -25,7 +25,7 @@ Revision History:
#include "dl_mk_rule_inliner.h" #include "dl_mk_rule_inliner.h"
#include "dl_rule.h" #include "dl_rule.h"
#include "dl_rule_transformer.h" #include "dl_rule_transformer.h"
#include "dl_mk_extract_quantifiers.h" #include "dl_mk_extract_quantifiers2.h"
#include "smt2parser.h" #include "smt2parser.h"
#include "pdr_context.h" #include "pdr_context.h"
#include "pdr_dl_interface.h" #include "pdr_dl_interface.h"
@ -146,7 +146,7 @@ lbool dl_interface::query(expr * query) {
} }
} }
// remove universal quantifiers from body. // remove universal quantifiers from body.
datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx); datalog::mk_extract_quantifiers2* extract_quantifiers = alloc(datalog::mk_extract_quantifiers2, m_ctx);
datalog::rule_transformer extract_q_tr(m_ctx); datalog::rule_transformer extract_q_tr(m_ctx);
extract_q_tr.register_plugin(extract_quantifiers); extract_q_tr.register_plugin(extract_quantifiers);
m_ctx.transform_rules(extract_q_tr, mc, pc); m_ctx.transform_rules(extract_q_tr, mc, pc);

41
src/muz_qe/proof_utils.cpp
View file

@ -223,7 +223,7 @@ public:
found_false = true; found_false = true;
break; break;
} }
// SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i))); SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
parents.push_back(tmp); parents.push_back(tmp);
if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) { if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
m_units.insert(m.get_fact(tmp), tmp); m_units.insert(m.get_fact(tmp), tmp);
@ -235,6 +235,7 @@ public:
break; break;
} }
tmp = m.get_parent(p, 0); tmp = m.get_parent(p, 0);
expr* old_clause = m.get_fact(tmp);
elim(tmp); elim(tmp);
parents[0] = tmp; parents[0] = tmp;
expr* clause = m.get_fact(tmp); expr* clause = m.get_fact(tmp);
@ -244,6 +245,31 @@ public:
pop(); pop();
break; break;
} }
//
// case where clause is a literal in the old clause.
//
if (is_literal_in_clause(clause, old_clause)) {
bool found = false;
for (unsigned i = 1; !found && i < parents.size(); ++i) {
if (m.is_complement(clause, m.get_fact(parents[i].get()))) {
parents[1] = parents[i];
parents.resize(2);
result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
m_refs.push_back(result);
add_hypotheses(result);
found = true;
}
}
if (!found) {
result = parents[0].get();
}
pop();
break;
}
//
// case where new clause is a subset of old clause.
// the literals in clause should be a subset of literals in old_clause.
//
get_literals(clause); get_literals(clause);
for (unsigned i = 1; i < parents.size(); ++i) { for (unsigned i = 1; i < parents.size(); ++i) {
bool found = false; bool found = false;
@ -309,6 +335,19 @@ public:
m_cache.insert(p, result); m_cache.insert(p, result);
p = result; p = result;
} }
bool is_literal_in_clause(expr* fml, expr* clause) {
if (!m.is_or(clause)) {
return false;
}
app* cl = to_app(clause);
for (unsigned i = 0; i < cl->get_num_args(); ++i) {
if (cl->get_argi(i) == fml) {
return true;
}
}
return false;
}
}; };
void proof_utils::reduce_hypotheses(proof_ref& pr) { void proof_utils::reduce_hypotheses(proof_ref& pr) {