From: Haniel Barbosa Date: Thu, 24 Mar 2022 17:34:59 +0000 (-0300) Subject: [sat] Add option to disable Minisat simplifications (#7992) X-Git-Tag: cvc5-1.0.0~187 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2159129fb16b55de49dbc42c0e71293959e7be3a;p=cvc5.git [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 8404ab920..84fea44d0 100644 --- 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 78fda6ca7..558e2ae16 100644 --- 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 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 3d116d500..deeb98fac 100644 --- 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 f47d768c0..2416b9eff 100644 --- 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)