From f1a00da401ccd42155e3753bc83320e81b89b1bb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 12 Jan 2015 17:43:56 +0000 Subject: [PATCH] BV-SLS Cosmetics Signed-off-by: Christoph M. Wintersteiger --- src/sat/tactic/sat_tactic.cpp | 2 -- src/tactic/portfolio/default_tactic.cpp | 1 - src/tactic/portfolio/smt_strategic_solver.cpp | 5 +--- src/tactic/smtlogics/qfbv_tactic.cpp | 26 ------------------- 4 files changed, 1 insertion(+), 33 deletions(-) diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 717bf7007..677540991 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -66,8 +66,6 @@ class sat_tactic : public tactic { CASSERT("sat_solver", m_solver.check_invariant()); IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream());); TRACE("sat_dimacs", m_solver.display_dimacs(tout);); - //m_solver.display_dimacs(std::cerr); - //exit(0); lbool r = m_solver.check(); if (r == l_false) { diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 5a5cbcf94..9ecc16ecf 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -28,7 +28,6 @@ Notes: #include"probe_arith.h" #include"quant_tactics.h" #include"qffpa_tactic.h" -#include"sls_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index f63b4fd8c..ae79446e3 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/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