From b968eb2b8cf75385523955e51f99e689b31a19b8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Feb 2014 18:13:16 +0000 Subject: [PATCH] FPA probe bugfixes Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/qffpa_tactic.cpp | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index 772fd3996..04ffc281a 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -42,7 +42,7 @@ struct is_non_qffpa_predicate { ast_manager & m; float_util u; - is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {} + is_non_qffpa_predicate(ast_manager & _m) : m(_m), u(m) {} void operator()(var *) { throw found(); } @@ -50,11 +50,9 @@ struct is_non_qffpa_predicate { void operator()(app * n) { sort * s = get_sort(n); - if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s))) + if (!m.is_bool(s) && !u.is_float(s) && !u.is_rm(s)) throw found(); - if (is_uninterp(n) && n->get_num_args() != 0) - throw found(); - family_id fid = s->get_family_id(); + family_id fid = n->get_family_id(); if (fid == m.get_basic_family_id()) return; if (fid == u.get_family_id()) @@ -70,7 +68,7 @@ struct is_non_qffpabv_predicate { bv_util bu; float_util fu; - is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {} + is_non_qffpabv_predicate(ast_manager & _m) : m(_m), bu(m), fu(m) {} void operator()(var *) { throw found(); } @@ -78,11 +76,9 @@ struct is_non_qffpabv_predicate { void operator()(app * n) { sort * s = get_sort(n); - if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s))) + if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s)) throw found(); - if (is_uninterp(n) && n->get_num_args() != 0) - throw found(); - family_id fid = s->get_family_id(); + family_id fid = n->get_family_id(); if (fid == m.get_basic_family_id()) return; if (fid == fu.get_family_id() || fid == bu.get_family_id())