mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

more general predicate recognizer for quantified Horn clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-20 11:16:54 -08:00
parent 6a18015622
commit 2c54bbba5f
1 changed files with 20 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/muz_qe/horn_tactic.cpp
View file

@ -90,6 +90,24 @@ class horn_tactic : public tactic {
m_ctx.register_predicate(to_app(a)->get_decl(), true); m_ctx.register_predicate(to_app(a)->get_decl(), true);
} }
void check_predicate(expr* a) {
expr* a1 = 0;
while (true) {
if (is_quantifier(a)) {
a = to_quantifier(a)->get_expr();
continue;
}
if (m.is_not(a, a1)) {
a = a1;
continue;
}
if (is_predicate(a)) {
register_predicate(a);
}
break;
}
}
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE }; enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
formula_kind get_formula_kind(expr_ref& f) { formula_kind get_formula_kind(expr_ref& f) {
@ -99,13 +117,12 @@ class horn_tactic : public tactic {
expr* a = 0, *a1 = 0; expr* a = 0, *a1 = 0;
datalog::flatten_or(f, args); datalog::flatten_or(f, args);
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
a = args[i].get(); a = args[i].get();
check_predicate(a);
if (m.is_not(a, a1) && is_predicate(a1)) { if (m.is_not(a, a1) && is_predicate(a1)) {
register_predicate(a1);
body.push_back(a1); body.push_back(a1);
} }
else if (is_predicate(a)) { else if (is_predicate(a)) {
register_predicate(a);
if (head) { if (head) {
return IS_NONE; return IS_NONE;
} }