fix #3938

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_config.cpp

@@ -244,7 +244,7 @@ namespace sat {
             throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected");
 
         m_card_solver = p.cardinality_solver();
-        m_xor_solver = false && p.xor_solver(); // hide this option until thoroughly tested
+        m_xor_solver = false; // prevent users from playing with this option
 
         sat_simplifier_params sp(_p);
         m_elim_vars = sp.elim_vars();

src/sat/sat_params.pyg

@@ -53,7 +53,6 @@ def_module_params('sat',
                           ('cardinality.solver', BOOL, True, 'use cardinality solver'),
                           ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver)'),
                           ('pb.min_arity', UINT, 9, 'minimal arity to compile pb/cardinality constraints to CNF'),
-                          ('xor.solver', BOOL, False, 'use xor solver'),
                           ('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
                           ('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
                           ('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),

src/sat/sat_solver/inc_sat_solver.cpp

@@ -325,7 +325,6 @@ class inc_sat_solver : public solver {
         sat_params p1(p);
         m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
         m_params.set_sym("pb.solver", p1.pb_solver());
-        m_params.set_bool("xor_solver", p1.xor_solver());
         m_solver.updt_params(m_params);
         m_solver.set_incremental(is_incremental() && !override_incremental());
 

src/sat/tactic/sat_tactic.cpp

@@ -156,15 +156,12 @@ class sat_tactic : public tactic {
     imp *      m_imp;
     params_ref m_params;
     statistics m_stats;
-    symbol     m_xor_solver;
 
 public:
     sat_tactic(ast_manager & m, params_ref const & p):
         m_imp(nullptr),
-        m_params(p),
-        m_xor_solver("xor_solver") {
+        m_params(p) {
         sat_params p1(p);
-        m_params.set_bool(m_xor_solver, p1.xor_solver());
     }
 
     tactic * translate(ast_manager & m) override {
@@ -177,8 +174,6 @@ class sat_tactic : public tactic {
 
     void updt_params(params_ref const & p) override {
         m_params = p;
-        sat_params p1(p);
-        m_params.set_bool(m_xor_solver, p1.xor_solver());
         if (m_imp) m_imp->updt_params(p);
     }
 

src/shell/dimacs_frontend.cpp

@@ -228,9 +228,6 @@ unsigned read_dimacs(char const * file_name) {
     sat_params sp(p);
     reslimit limit;
     sat::solver solver(p, limit);
-    if (sp.xor_solver()) {
-        solver.set_extension(alloc(sat::ba_solver));
-    }
     g_solver = &solver;
 
     if (file_name) {