From 2c54bbba5fbf2db6d003077f79b5ae1f69ec564f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Nov 2012 11:16:54 -0800 Subject: [PATCH] more general predicate recognizer for quantified Horn clauses Signed-off-by: Nikolaj Bjorner --- src/muz_qe/horn_tactic.cpp | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 1e76faf13..59e9e6fec 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -90,6 +90,24 @@ class horn_tactic : public tactic { 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 }; formula_kind get_formula_kind(expr_ref& f) { @@ -99,13 +117,12 @@ class horn_tactic : public tactic { expr* a = 0, *a1 = 0; datalog::flatten_or(f, args); 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)) { - register_predicate(a1); body.push_back(a1); } else if (is_predicate(a)) { - register_predicate(a); if (head) { return IS_NONE; }