[sat] Add option to disable Minisat simplifications (#7992)

Useful to better control behavior, specially in terms of how the solver performs
when these simplifications (mainly variable and clause elimination) are
disabled, e.g. with incremental and/or proofs.

Also renames the previously confusing "--minisat--elimination" option, which
only refers to variable elimination, a subset of the Minisat simplifications.

Moreover deletes an old comment which no longer applies.

diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
index 8404ab9202973433732a1f8f04ddffcb3d0c80c6..84fea44d08c55a184f3664d8c4e9afbf18fde70c 100644 (file)
--- a/src/options/prop_options.toml
+++ b/src/options/prop_options.toml
@@ -56,12 +56,22 @@ name   = "SAT Layer"
   help       = "sets the restart interval increase factor for the sat solver (F=3.0 by default)"
 
 [[option]]
-  name       = "minisatUseElim"
+  name       = "minisatSimpMode"
   category   = "regular"
-  long       = "minisat-elimination"
-  type       = "bool"
-  default    = "true"
-  help       = "use Minisat elimination"
+  long       = "minisat-simplification=MODE"
+  type       = "MinisatSimpMode"
+  default    = "ALL"
+  help       = "Simplifications to be performed by Minisat."
+  help_mode  = "Modes for Minisat simplifications."
+[[option.mode.ALL]]
+  name = "all"
+  help = "Variable and clause elimination, plus other simplifications."
+[[option.mode.CLAUSE_ELIM]]
+  name = "clause-elim"
+  help = "Caluse elimination and other simplifications, except variable elimination."
+[[option.mode.NONE]]
+  name = "none"
+  help = "No simplifications."
 
 [[option]]
   name       = "minisatDumpDimacs"

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 78fda6ca76e0db06a73d12c840f1b295032593e2..558e2ae16e05c0c3bcb3229d87c64ad4d9f09556 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -38,7 +38,6 @@ static const char* _cat = "SIMP";
 
 static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);
 static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);
-static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);
 static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);
 static IntOption    opt_clause_lim       (_cat, "cl-lim",       "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20,   IntRange(-1, INT32_MAX));
 static IntOption    opt_subsumption_lim  (_cat, "sub-lim",      "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
@@ -62,27 +61,18 @@ SimpSolver::SimpSolver(Env& env,
       use_asymm(opt_use_asymm),
       // make sure this is not enabled if unsat cores or proofs are on
       use_rcheck(opt_use_rcheck && !options().smt.unsatCores && !pnm),
-      use_elim(options().prop.minisatUseElim && !enableIncremental),
       merges(0),
       asymm_lits(0),
       eliminated_vars(0),
       elimorder(1),
-      use_simplification(!enableIncremental && !options().smt.unsatCores
-                         && !pnm)  // TODO: turn off simplifications if
-                                   // proofs are on initially
-      ,
+      use_simplification(
+          options().prop.minisatSimpMode != options::MinisatSimpMode::NONE
+          && !enableIncremental && !options().smt.unsatCores && !pnm),
       occurs(ClauseDeleted(ca)),
       elim_heap(ElimLt(n_occ)),
       bwdsub_assigns(0),
       n_touched(0)
 {
-  if (options().prop.minisatUseElim && options().prop.minisatUseElimWasSetByUser
-      && enableIncremental)
-  {
-    WarningOnce() << "Incremental mode incompatible with --minisat-elim"
-                  << std::endl;
-  }
-
     vec<Lit> dummy(1,lit_Undef);
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(0, dummy);
@@ -701,8 +691,14 @@ bool SimpSolver::eliminate(bool turn_off_elim)
 
             // At this point, the variable may have been set by assymetric branching, so check it
             // again. Also, don't eliminate frozen variables:
-            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
-                ok = false; goto cleanup; }
+            if (options().prop.minisatSimpMode
+                    != options::MinisatSimpMode::CLAUSE_ELIM
+                && value(elim) == l_Undef && !frozen[elim]
+                && !eliminateVar(elim))
+            {
+              ok = false;
+              goto cleanup;
+            }
 
             checkGarbage(simp_garbage_frac);
         }

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 3d116d500209261a1c283c9044c664c042e1adca..deeb98facfb10dacadb57cefcb7de3cc5f9da28c 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -121,7 +121,6 @@ class SimpSolver : public Solver {
 
     bool    use_asymm;         // Shrink clauses by asymmetric branching.
     bool    use_rcheck;        // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
-    bool    use_elim;          // Perform variable elimination.
 
     // Statistics:
     //

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index f47d768c06e704e2e3860c249205ee2665d1bc04..2416b9effd11fb244d04732b52ed5a2a806d6b1e 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -469,7 +469,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     verbose(1) << "SolverEngine: turning on produce-models" << std::endl;
     opts.smt.produceModels = true;
   }
-  
+
   // --ite-simp is an experimental option designed for QF_LIA/nec. This
   // technique is experimental. This benchmark set also requires removing ITEs
   // during preprocessing, before repeating simplification. Hence, we enable
@@ -481,7 +481,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       opts.smt.earlyIteRemoval = true;
     }
   }
-  
+
   // Set the options for the theoryOf
   if (!opts.theory.theoryOfModeWasSetByUser)
   {
@@ -556,13 +556,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
                  << std::endl;
     opts.smt.repeatSimp = repeatSimp;
   }
-  
+
   /* Disable bit-level propagation by default for the BITBLAST solver. */
   if (opts.bv.bvSolver == options::BVSolver::BITBLAST)
   {
     opts.bv.bitvectorPropagate = false;
   }
-  
+
   if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL
       && !logic.isTheoryEnabled(THEORY_BV))
   {
@@ -691,10 +691,10 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
   }
 
-  // until bugs 371,431 are fixed
-  if (!opts.prop.minisatUseElimWasSetByUser)
+  if (!opts.prop.minisatSimpModeWasSetByUser
+      && opts.prop.minisatSimpMode == options::MinisatSimpMode::ALL)
   {
-    // cannot use minisat elimination for logics where a theory solver
+    // cannot use minisat variable elimination for logics where a theory solver
     // introduces new literals into the search. This includes quantifiers
     // (quantifier instantiation), and the lemma schemas used in non-linear
     // and sets. We also can't use it if models are enabled.
@@ -703,7 +703,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
         || opts.smt.produceAssignments || opts.smt.checkModels
         || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
     {
-      opts.prop.minisatUseElim = false;
+      opts.prop.minisatSimpMode = options::MinisatSimpMode::CLAUSE_ELIM;
     }
   }
 
@@ -960,9 +960,9 @@ bool SetDefaults::incompatibleWithModels(const Options& opts,
     reason << "sort-inference";
     return true;
   }
-  else if (opts.prop.minisatUseElim)
+  else if (opts.prop.minisatSimpMode == options::MinisatSimpMode::ALL)
   {
-    reason << "minisat-elimination";
+    reason << "minisat-simplification";
     return true;
   }
   else if (opts.quantifiers.globalNegate)