mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

hypothesis_reducer: worked around propositional literals

Browse source 
propositional formulas (disjunctions) can appear as literals.  This
makes it tricky to recognize whether a formula is a unit clause when
re-building unit resolution.

Added work-around that identifies whether a formula is a literal based
on its appearance in previous unit resolution step.
This commit is contained in:
Arie Gurfinkel 2018-05-18 14:12:15 -07:00
parent b39c532f19
commit 5a6bd5e782
2 changed files with 43 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

72
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -363,7 +363,7 @@ proof* hypothesis_reducer::reduce_core(proof* pf) {
else if (m.is_unit_resolution(p)) { else if (m.is_unit_resolution(p)) {
// unit: reduce untis; reduce the first premise; rebuild // unit: reduce untis; reduce the first premise; rebuild
// unit resolution // unit resolution
res = mk_unit_resolution_core(args); res = mk_unit_resolution_core(p, args);
// -- re-compute hypsets // -- re-compute hypsets
compute_hypsets(res); compute_hypsets(res);
} }
@ -420,12 +420,13 @@ proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
return res; return res;
} }
proof* hypothesis_reducer::mk_unit_resolution_core(ptr_buffer<proof>& args) { proof* hypothesis_reducer::mk_unit_resolution_core(proof *ures,
ptr_buffer<proof>& args) {
// if any literal is false, we don't need a unit resolution step // if any literal is false, we don't need a unit resolution step
// This can be the case due to some previous transformations // This can be the case due to some previous transformations
for (unsigned i = 1, sz = args.size(); i < sz; ++i) { for (unsigned i = 1, sz = args.size(); i < sz; ++i) {
if (m.is_false(m.get_fact(args[i]))) { if (m.is_false(m.get_fact(args[i]))) {
// XXX just in case // XXX pin just in case
m_pinned.push_back(args[i]); m_pinned.push_back(args[i]);
return args[i]; return args[i];
} }
@ -434,48 +435,58 @@ proof* hypothesis_reducer::mk_unit_resolution_core(ptr_buffer<proof>& args) {
proof* arg0 = args[0]; proof* arg0 = args[0];
app *fact0 = to_app(m.get_fact(arg0)); app *fact0 = to_app(m.get_fact(arg0));
ptr_buffer<proof> pf_args; ptr_buffer<proof> pf_args;
ptr_buffer<expr> pf_fact; ptr_buffer<expr> pf_fact;
pf_args.push_back(arg0); pf_args.push_back(arg0);
// check if fact0 can be resolved as a unit // compute literals to be resolved
// this is required for handling literals with OR ptr_buffer<expr> lits;
for (unsigned j = 1; j < args.size(); ++j) {
if (m.is_complement(fact0, m.get_fact(args[j]))) { // fact0 is a literal whenever the original resolution was a
pf_args.push_back(args[j]); // binary resolution to an empty clause
break; if (m.get_num_parents(ures) == 2 && m.is_false(m.get_fact(ures))) {
lits.push_back(fact0);
}
// fact0 is a literal unless it is a dijsunction
else if (!m.is_or(fact0)) {
lits.push_back(fact0);
}
// fact0 is a literal only if it appears as a literal in the
// original resolution
else {
lits.reset();
app* ures_fact = to_app(m.get_fact(m.get_parent(ures, 0)));
for (unsigned i = 0, sz = ures_fact->get_num_args(); i < sz; ++i) {
if (ures_fact->get_arg(i) == fact0) {
lits.push_back(fact0);
break;
}
} }
if (lits.empty()) {
lits.append(fact0->get_num_args(), fact0->get_args());
}
} }
// -- find all literals that are resolved on
// if failed to find a resolvent, and the fact is a disjunction, for (unsigned i = 0, sz = lits.size(); i < sz; ++i) {
// attempt to resolve each disjunct bool found = false;
if (pf_args.size() == 1 && m.is_or(fact0)) { for (unsigned j = 1; j < args.size(); ++j) {
ptr_buffer<expr> cls; if (m.is_complement(lits.get(i), m.get_fact(args[j]))) {
for (unsigned i = 0, sz = fact0->get_num_args(); i < sz; ++i) found = true;
cls.push_back(fact0->get_arg(i)); pf_args.push_back(args[j]);
break;
// -- find all literals that are resolved on
// XXX quadratic implementation
for (unsigned i = 0, sz = cls.size(); i < sz; ++i) {
bool found = false;
for (unsigned j = 1; j < args.size(); ++j) {
if (m.is_complement(cls.get(i), m.get_fact(args[j]))) {
found = true;
pf_args.push_back(args[j]);
break;
}
} }
if (!found) pf_fact.push_back(cls.get(i));
} }
SASSERT(pf_fact.size() + pf_args.size() - 1 == cls.size()); if (!found) {pf_fact.push_back(lits.get(i));}
} }
// unit resolution got reduced to noop // unit resolution got reduced to noop
if (pf_args.size() == 1) { if (pf_args.size() == 1) {
// XXX pin just in case // XXX pin just in case
m_pinned.push_back(arg0); m_pinned.push_back(arg0);
return arg0; return arg0;
} }
@ -484,6 +495,7 @@ proof* hypothesis_reducer::mk_unit_resolution_core(ptr_buffer<proof>& args) {
tmp = mk_or(m, pf_fact.size(), pf_fact.c_ptr()); tmp = mk_or(m, pf_fact.size(), pf_fact.c_ptr());
proof* res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), tmp); proof* res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), tmp);
m_pinned.push_back(res); m_pinned.push_back(res);
return res; return res;
} }

2
src/muz/spacer/spacer_proof_utils.h
View file

@ -96,7 +96,7 @@ private:
proof* reduce_core(proof* pf); proof* reduce_core(proof* pf);
proof* mk_lemma_core(proof *pf, expr *fact); proof* mk_lemma_core(proof *pf, expr *fact);
proof* mk_unit_resolution_core(ptr_buffer<proof>& args); proof* mk_unit_resolution_core(proof* ures, ptr_buffer<proof>& args);
proof* mk_proof_core(proof* old, ptr_buffer<proof>& args); proof* mk_proof_core(proof* old, ptr_buffer<proof>& args);
}; };
} }