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

relax pre-processing to untangle non-horn formulas, based on Eldarica/linear benchmarks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-05-13 13:21:45 -07:00
parent e35fd58968
commit ac6488a195
1 changed files with 23 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/muz_qe/horn_tactic.cpp
View file

@ -124,6 +124,15 @@ class horn_tactic : public tactic {
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
bool is_implication(expr* f) {
expr* e1;
while (is_forall(f)) {
f = to_quantifier(f)->get_expr();
}
while (m.is_implies(f, e1, f)) ;
return is_predicate(f);
}
formula_kind get_formula_kind(expr_ref& f) {
expr_ref tmp(f);
normalize(tmp);
@ -149,7 +158,10 @@ class horn_tactic : public tactic {
}
}
if (head) {
// f = m.mk_implies(f, head);
if (!is_implication(f)) {
f = m.mk_and(body.size(), body.c_ptr());
f = m.mk_implies(f, head);
}
return IS_RULE;
}
else {
@ -200,6 +212,7 @@ class horn_tactic : public tactic {
break;
default:
msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
TRACE("horn", tout << msg.str(););
throw tactic_exception(msg.str().c_str());
}
}
@ -230,7 +243,15 @@ class horn_tactic : public tactic {
model_converter_ref & mc,
proof_converter_ref & pc) {
lbool is_reachable = m_ctx.query(q);
lbool is_reachable = l_undef;
try {
is_reachable = m_ctx.query(q);
}
catch (default_exception& ex) {
IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";);
throw ex;
}
g->inc_depth();
bool produce_models = g->models_enabled();