remove binspr experiment

Z3Prover · Jan 12, 2025 · d3183fa · d3183fa
1 parent 8d2b9b4
commit d3183fa
Show file tree

Hide file tree

Showing 8 changed files with 0 additions and 605 deletions.
diff --git a/src/params/sat_params.pyg b/src/params/sat_params.pyg
@@ -72,7 +72,6 @@ def_module_params('sat',
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
                           ('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'),
-                          ('binspr', BOOL, False, 'enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models'),
 	                      ('anf', BOOL, False, 'enable ANF based simplification in-processing'),
 	                      ('anf.delay', UINT, 2, 'delay ANF simplification by in-processing round'),
                           ('anf.exlin', BOOL, False, 'enable extended linear simplification'), 

diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
@@ -7,7 +7,6 @@ z3_add_component(sat
     sat_asymm_branch.cpp
     sat_bcd.cpp
     sat_big.cpp
-    sat_binspr.cpp
     sat_clause.cpp
     sat_clause_set.cpp
     sat_clause_use_list.cpp