From 97e263299d28e5ccb78ce4aef8e3133808c372a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Aug 2017 01:35:28 -0700 Subject: [PATCH] add logic 'SAT' as an alternative name to QF_FD some solverFor(SAT) works too. #1152 Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/smt_strategic_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index bde9e0e98..0ad9e5f19 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); - else if (logic == "QF_FD") + else if (logic == "QF_FD" || logic == "SAT") return mk_solver2tactic(mk_fd_solver(m, p)); //else if (logic=="QF_UFNRA") // return mk_qfufnra_tactic(m, p); @@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const } static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { - if (logic == "QF_FD") + if (logic == "QF_FD" || logic == "SAT") return mk_fd_solver(m, p); return 0; }