From 0746ede53733c6a4191dd588cba14ec83236e490 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jan 2015 15:59:25 +0000 Subject: [PATCH] BV SLS: Final adjustments Signed-off-by: Christoph M. Wintersteiger --- src/tactic/portfolio/smt_strategic_solver.cpp | 5 +--- src/tactic/sls/sls_tactic.cpp | 3 +-- src/tactic/sls/sls_tactic.h | 2 +- src/tactic/smtlogics/qfbv_tactic.cpp | 26 ------------------- 4 files changed, 3 insertions(+), 33 deletions(-) diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index f63b4fd8c..586c3a349 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -37,14 +37,11 @@ Notes: #include"horn_tactic.h" #include"smt_solver.h" -#include"sls_tactic.h" - tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) { if (logic=="QF_UF") return mk_qfuf_tactic(m, p); else if (logic=="QF_BV") - // return mk_qfbv_tactic(m, p); - return mk_qfbv_sls_tactic(m, p); + return mk_qfbv_tactic(m, p); else if (logic=="QF_IDL") return mk_qfidl_tactic(m, p); else if (logic=="QF_LIA") diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 9bbed20bb..b06a047f7 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -158,8 +158,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { - tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m)); - //tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m)); + tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m, p)); t->updt_params(p); return t; } diff --git a/src/tactic/sls/sls_tactic.h b/src/tactic/sls/sls_tactic.h index 50b8f0d5b..82ac1ce88 100644 --- a/src/tactic/sls/sls_tactic.h +++ b/src/tactic/sls/sls_tactic.h @@ -23,8 +23,8 @@ Notes: class ast_manager; class tactic; -tactic * mk_sls_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p = params_ref()); + /* ADD_TACTIC("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_sls_tactic(m, p)") */ diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 3b4da2f2d..ac53ca0c8 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -93,32 +93,6 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { mk_sat_tactic(m)); #endif - /* use full sls - tactic * st = using_params(and_then(preamble_st, - cond(mk_is_qfbv_probe(), - cond(mk_is_qfbv_eq_probe(), - and_then(mk_bv1_blaster_tactic(m), - using_params(mk_smt_tactic(), solver_p)), - and_then(mk_nnf_tactic(m, p), mk_sls_tactic(m))), - mk_smt_tactic())), - main_p);*/ - - /* use pure dpll - tactic * st = using_params(and_then(mk_simplify_tactic(m), - cond(mk_is_qfbv_probe(), - and_then(mk_bit_blaster_tactic(m), - when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), - and_then(using_params(and_then(mk_simplify_tactic(m), - mk_solve_eqs_tactic(m)), - local_ctx_p), - if_no_proofs(cond(mk_produce_unsat_cores_probe(), - mk_aig_tactic(), - using_params(mk_aig_tactic(), - big_aig_p))))), - new_sat), - mk_smt_tactic())), - main_p);*/ - tactic * st = using_params(and_then(preamble_st, // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function // symbols. In this case, we should not use