From 80c025b2893cc6adc9d8747f0eb9145bfa04d2ec Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 31 Dec 2014 16:15:55 +0000 Subject: [PATCH] Improved default tactic for QF_FP Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/qffpa_tactic.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index fc292bca6..6cfc699c7 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include"bit_blaster_tactic.h" #include"sat_tactic.h" #include"fpa2bv_tactic.h" +#include"smt_tactic.h" #include"qffpa_tactic.h" @@ -28,13 +29,17 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { params_ref sat_simp_p = p; sat_simp_p .set_bool("elim_and", true); - return and_then(mk_simplify_tactic(m, p), + return cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()), + and_then(mk_simplify_tactic(m), + mk_smt_tactic()), + and_then( + mk_simplify_tactic(m, p), mk_fpa2bv_tactic(m, p), using_params(mk_simplify_tactic(m, p), sat_simp_p), mk_bit_blaster_tactic(m, p), using_params(mk_simplify_tactic(m, p), sat_simp_p), mk_sat_tactic(m, p), - mk_fail_if_undecided_tactic()); + mk_fail_if_undecided_tactic())); } struct is_non_qffp_predicate {