From fc3cbcbe026d6cacec681b4f39d7f9715022980b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Dec 2017 10:16:35 -0800
Subject: [PATCH] remove deprecated options
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_config.cpp | 4 ----
src/sat/sat_config.h | 3 ---
src/sat/sat_params.pyg | 6 ++----
src/sat/sat_solver.cpp | 6 ------
4 files changed, 2 insertions(+), 17 deletions(-)
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 24d2bca9b..ed951fd93 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -38,8 +38,6 @@ namespace sat {
m_glue_psm("glue_psm"),
m_psm_glue("psm_glue") {
m_num_threads = 1;
- m_local_search = 0;
- m_lookahead_search = false;
m_lookahead_simplify = false;
m_lookahead_simplify_bca = false;
m_elim_vars = false;
@@ -92,7 +90,6 @@ namespace sat {
m_local_search_threads = p.local_search_threads();
m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_simplify_bca = p.lookahead_simplify_bca();
- m_lookahead_search = p.lookahead_search();
if (p.lookahead_reward() == symbol("heule_schur")) {
m_lookahead_reward = heule_schur_reward;
}
@@ -195,7 +192,6 @@ namespace sat {
else {
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
}
- m_dimacs_inprocess_display = p.dimacs_inprocess_display();
sat_simplifier_params sp(_p);
m_elim_vars = sp.elim_vars();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 9a20bbc63..c3018ef29 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -82,7 +82,6 @@ namespace sat {
unsigned m_num_threads;
unsigned m_local_search_threads;
bool m_local_search;
- bool m_lookahead_search;
bool m_lookahead_simplify;
bool m_lookahead_simplify_bca;
unsigned m_lookahead_cube_cutoff;
@@ -112,8 +111,6 @@ namespace sat {
bool m_drat_check_unsat;
bool m_drat_check_sat;
- bool m_dimacs_inprocess_display;
-
symbol m_always_true;
symbol m_always_false;
symbol m_caching;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 4f65b100b..e8ae53dca 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -35,15 +35,13 @@ def_module_params('sat',
('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
('xor.solver', BOOL, False, 'use xor solver'),
('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
- ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search', BOOL, False, 'use local search instead of CDCL'),
+ ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
- ('lookahead_search', BOOL, False, 'use lookahead solver'),
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
- ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
- ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))
+ ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index f8425b9bc..b3fc95f47 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -950,12 +950,6 @@ namespace sat {
if (m_config.m_inprocess_max <= m_simplifications) {
m_reason_unknown = "sat.max.inprocess";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";);
- if (m_config.m_dimacs_inprocess_display) {
- display_dimacs(std::cout);
- for (unsigned i = 0; i < num_lits; ++lits) {
- std::cout << dimacs_lit(lits[i]) << " 0\n";
- }
- }
return l_undef;
}