From f2f6fc1994fcbfaa1c4191f51e75babf7f67544e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 29 May 2015 13:58:23 +0100 Subject: [PATCH] Added QF_BVFP logic alias for QF_FPBV --- src/cmd_context/cmd_context.cpp | 2 ++ src/smt/smt_setup.cpp | 2 +- src/tactic/portfolio/smt_strategic_solver.cpp | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 80aa10cde..9aa089096 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -528,6 +528,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "LRA" || s == "QF_FP" || s == "QF_FPBV" || + s == "QF_BVFP" || s == "HORN"; } @@ -547,6 +548,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const { s == "QF_AUFBV" || s == "QF_BVRE" || s == "QF_FPBV" || + s == "QF_BVFP" || s == "HORN"; } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index d4c0e1efb..98ad5e51a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -116,7 +116,7 @@ namespace smt { setup_LRA(); else if (m_logic == "QF_FP") setup_QF_FP(); - else if (m_logic == "QF_FPBV") + else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP") setup_QF_FPBV(); else setup_unknown(); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index b28c8cf3d..687771a30 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -81,7 +81,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_ufbv_tactic(m, p); else if (logic=="QF_FP") return mk_qffp_tactic(m, p); - else if (logic == "QF_FPBV") + else if (logic == "QF_FPBV" || logic == "QF_BVFP") return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p);