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 Issue #405: Horn normal form ignores implication

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-10 19:16:59 -08:00
parent fce286db91
commit 082dcda7f7
3 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz/base/dl_rule.cpp
View file

@ -282,6 +282,8 @@ namespace datalog {
func_decl* rule_manager::mk_query(expr* query, rule_set& rules) { func_decl* rule_manager::mk_query(expr* query, rule_set& rules) {
TRACE("dl", tout << mk_pp(query, m) << "\n";);
ptr_vector<sort> vars; ptr_vector<sort> vars;
svector<symbol> names; svector<symbol> names;
app_ref_vector body(m); app_ref_vector body(m);
@ -290,6 +292,7 @@ namespace datalog {
// Add implicit variables. // Add implicit variables.
// 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, 0, &names); qh.pull_quantifier(false, q, 0, &names);
// retrieve free variables. // retrieve free variables.
@ -358,6 +361,7 @@ namespace datalog {
if (!vars.empty()) { if (!vars.empty()) {
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);
} }
TRACE("dl", tout << rule_expr << "\n";);
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED); scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
proof_ref pr(m); proof_ref pr(m);

11
src/muz/base/hnf.cpp
View file

@ -325,9 +325,10 @@ private:
void eliminate_disjunctions(expr_ref_vector::element_ref& body, proof_ref_vector& proofs) { void eliminate_disjunctions(expr_ref_vector::element_ref& body, proof_ref_vector& proofs) {
expr* b = body.get(); expr* b = body.get();
expr* e1; expr* e1, *e2;
bool negate_args = false; bool negate_args = false;
bool is_disj = false; bool is_disj = false;
expr_ref_vector _body(m);
unsigned num_disj = 0; unsigned num_disj = 0;
expr* const* disjs = 0; expr* const* disjs = 0;
if (!contains_predicate(b)) { if (!contains_predicate(b)) {
@ -346,6 +347,14 @@ private:
num_disj = to_app(e1)->get_num_args(); num_disj = to_app(e1)->get_num_args();
disjs = to_app(e1)->get_args(); disjs = to_app(e1)->get_args();
} }
if (m.is_implies(b, e1, e2)) {
is_disj = true;
_body.push_back(mk_not(m, e1));
_body.push_back(e2);
disjs = _body.c_ptr();
num_disj = 2;
negate_args = false;
}
if (is_disj) { if (is_disj) {
app* old_head = 0; app* old_head = 0;
if (m_memoize_disj.find(b, old_head)) { if (m_memoize_disj.find(b, old_head)) {

2
src/smt/smt_context.cpp
View file

@ -4126,7 +4126,7 @@ namespace smt {
if (m_fparams.m_model_compact) if (m_fparams.m_model_compact)
m_proto_model->compress(); m_proto_model->compress();
TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
SASSERT(validate_model()); //SASSERT(validate_model());
} }
} }