From 06f4747e4f6c97be9b6fca4edd1ffff66e386c06 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 12 Aug 2021 17:12:19 -0700 Subject: [PATCH] Refactor setDefaults to use an options object (#6994) This commit refactors the `setDefaults` method to accept an `Options` object as argument instead of using the current (static) `Options` object. --- src/smt/options_manager.cpp | 2 +- src/smt/set_defaults.cpp | 292 ++++++++++++++++++------------------ src/smt/set_defaults.h | 3 +- 3 files changed, 147 insertions(+), 150 deletions(-) diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index a5dee27ae..9ffb396d1 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -41,7 +41,7 @@ void OptionsManager::notifySetOption(const std::string& key) void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver) { // ensure that our heuristics are properly set up - setDefaults(logic, isInternalSubsolver); + setDefaults(logic, *d_options, isInternalSubsolver); } } // namespace smt diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e23323e6d..c916ac962 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -46,35 +46,34 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -void setDefaults(LogicInfo& logic, bool isInternalSubsolver) +void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) { - Options& opts = Options::current(); // implied options - if (options::debugCheckModels()) + if (opts.smt.debugCheckModels) { opts.smt.checkModels = true; } - if (options::checkModels() || options::dumpModels()) + if (opts.smt.checkModels || opts.driver.dumpModels) { opts.smt.produceModels = true; } - if (options::checkModels()) + if (opts.smt.checkModels) { opts.smt.produceAssignments = true; } // unsat cores and proofs shenanigans - if (options::dumpUnsatCoresFull()) + if (opts.driver.dumpUnsatCoresFull) { opts.driver.dumpUnsatCores = true; } - if (options::checkUnsatCores() || options::dumpUnsatCores() - || options::unsatAssumptions() || options::minimalUnsatCores() - || options::unsatCoresMode() != options::UnsatCoresMode::OFF) + if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores + || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores + || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) { opts.smt.unsatCores = true; } - if (options::unsatCores() - && options::unsatCoresMode() == options::UnsatCoresMode::OFF) + if (opts.smt.unsatCores + && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) { if (opts.smt.unsatCoresModeWasSetByUser) { @@ -84,13 +83,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; } - if (options::checkProofs() || options::dumpProofs()) + if (opts.smt.checkProofs || opts.driver.dumpProofs) { opts.smt.produceProofs = true; } - if (options::produceProofs() - && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) + if (opts.smt.produceProofs + && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) { if (opts.smt.unsatCoresModeWasSetByUser) { @@ -103,7 +102,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // set proofs on if not yet set - if (options::unsatCores() && !options::produceProofs()) + if (opts.smt.unsatCores && !opts.smt.produceProofs) { if (opts.smt.produceProofsWasSetByUser) { @@ -114,8 +113,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // if unsat cores are disabled, then unsat cores mode should be OFF - Assert(options::unsatCores() - == (options::unsatCoresMode() != options::UnsatCoresMode::OFF)); + Assert(opts.smt.unsatCores + == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)); if (opts.bv.bitvectorAigSimplificationsWasSetByUser) { @@ -128,12 +127,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.bitvectorAlgebraicSolver = true; } - bool isSygus = language::isInputLangSygus(options::inputLanguage()); + bool isSygus = language::isInputLangSygus(opts.base.inputLanguage); bool usesSygus = isSygus; - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (opts.bv.bitblastMode == options::BitblastMode::EAGER) { - if (options::produceModels() + if (opts.smt.produceModels && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { @@ -149,12 +148,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << "generation" << std::endl; opts.bv.bitblastMode = options::BitblastMode::LAZY; } - else if (!options::incrementalSolving()) + else if (!opts.base.incrementalSolving) { opts.smt.ackermann = true; } - if (options::incrementalSolving() && !logic.isPure(THEORY_BV)) + if (opts.base.incrementalSolving && !logic.isPure(THEORY_BV)) { throw OptionException( "Incremental eager bit-blasting is currently " @@ -163,15 +162,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } /* Disable bit-level propagation by default for the BITBLAST solver. */ - if (options::bvSolver() == options::BVSolver::BITBLAST) + if (opts.bv.bvSolver == options::BVSolver::BITBLAST) { opts.bv.bitvectorPropagate = false; } - if (options::solveIntAsBV() > 0) + if (opts.smt.solveIntAsBV > 0) { // not compatible with incremental - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { throw OptionException( "solving integers as bitvectors is currently not supported " @@ -186,14 +185,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } - if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) + if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) { - if (options::boolToBitvector() != options::BoolToBVMode::OFF) + if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) { throw OptionException( "solving bitvectors as integers is incompatible with --bool-to-bv."); } - if (options::BVAndIntegerGranularity() > 8) + if (opts.smt.BVAndIntegerGranularity > 8) { /** * The granularity sets the size of the ITE in each element @@ -214,7 +213,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // set options about ackermannization - if (options::ackermann() && options::produceModels() + if (opts.smt.ackermann && opts.smt.produceModels && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { @@ -228,9 +227,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.ackermann = false; } - if (options::ackermann()) + if (opts.smt.ackermann) { - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { throw OptionException( "Incremental Ackermannization is currently not supported."); @@ -259,7 +258,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // technique is experimental. This benchmark set also requires removing ITEs // during preprocessing, before repeating simplification. Hence, we enable // this by default. - if (options::doITESimp()) + if (opts.smt.doITESimp) { if (!opts.smt.earlyIteRemovalWasSetByUser) { @@ -280,7 +279,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "Turning stringExp on since logic does not have everything " "and string theory is enabled\n"; } - if (options::stringExp() || !options::stringLazyPreproc()) + if (opts.strings.stringExp || !opts.strings.stringLazyPreproc) { // We require quantifiers since extended functions reduce using them. if (!logic.isQuantified()) @@ -299,7 +298,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // whether we must disable proofs bool disableProofs = false; - if (options::globalNegate()) + if (opts.quantifiers.globalNegate) { // When global negate answers "unsat", it is not due to showing a set of // formulas is unsat. Thus, proofs do not apply. @@ -307,8 +306,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // new unsat core specific restrictions for proofs - if (options::unsatCores() - && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) + if (opts.smt.unsatCores + && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) { // no fine-graininess if (!opts.proof.proofGranularityModeWasSetByUser) @@ -317,7 +316,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::arraysExp()) + if (opts.arrays.arraysExp) { if (!logic.isQuantified()) { @@ -336,15 +335,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // sygus inference may require datatypes if (!isInternalSubsolver) { - if (options::produceAbducts() - || options::produceInterpols() != options::ProduceInterpols::NONE - || options::sygusInference() || options::sygusRewSynthInput()) + if (opts.smt.produceAbducts + || opts.smt.produceInterpols != options::ProduceInterpols::NONE + || opts.quantifiers.sygusInference + || opts.quantifiers.sygusRewSynthInput) { // since we are trying to recast as sygus, we assume the input is sygus isSygus = true; usesSygus = true; } - else if (options::sygusInst()) + else if (opts.quantifiers.sygusInst) { // sygus instantiation uses sygus, but it is not a sygus problem usesSygus = true; @@ -367,11 +367,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // if we requiring disabling proofs, disable them now - if (disableProofs && options::produceProofs()) + if (disableProofs && opts.smt.produceProofs) { opts.smt.unsatCores = false; opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; - if (options::produceProofs()) + if (opts.smt.produceProofs) { Notice() << "SmtEngine: turning off produce-proofs." << std::endl; } @@ -381,29 +381,28 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // sygus core connective requires unsat cores - if (options::sygusCoreConnective()) + if (opts.quantifiers.sygusCoreConnective) { opts.smt.unsatCores = true; - if (options::unsatCoresMode() == options::UnsatCoresMode::OFF) + if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) { opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; } } - if ((options::checkModels() || options::checkSynthSol() - || options::produceAbducts() - || options::produceInterpols() != options::ProduceInterpols::NONE - || options::modelCoresMode() != options::ModelCoresMode::NONE - || options::blockModelsMode() != options::BlockModelsMode::NONE - || options::produceProofs()) - && !options::produceAssertions()) + if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts + || opts.smt.produceInterpols != options::ProduceInterpols::NONE + || opts.smt.modelCoresMode != options::ModelCoresMode::NONE + || opts.smt.blockModelsMode != options::BlockModelsMode::NONE + || opts.smt.produceProofs) + && !opts.smt.produceAssertions) { Notice() << "SmtEngine: turning on produce-assertions to support " << "option requiring assertions." << std::endl; opts.smt.produceAssertions = true; } - if (options::bvAssertInput() && options::produceProofs()) + if (opts.bv.bvAssertInput && opts.smt.produceProofs) { Notice() << "Disabling bv-assert-input since it is incompatible with proofs." << std::endl; @@ -412,8 +411,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // If proofs are required and the user did not specify a specific BV solver, // we make sure to use the proof producing BITBLAST_INTERNAL solver. - if (options::produceProofs() - && options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL + if (opts.smt.produceProofs + && opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL && !opts.bv.bvSolverWasSetByUser && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT) { @@ -425,14 +424,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // whether we want to force safe unsat cores, i.e., if we are in the default // ASSUMPTIONS mode, since other ones are experimental bool safeUnsatCores = - options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS; + opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS; // Disable options incompatible with incremental solving, unsat cores or // output an error if enabled explicitly. It is also currently incompatible // with arithmetic, force the option off. - if (options::incrementalSolving() || safeUnsatCores) + if (opts.base.incrementalSolving || safeUnsatCores) { - if (options::unconstrainedSimp()) + if (opts.smt.unconstrainedSimp) { if (opts.smt.unconstrainedSimpWasSetByUser) { @@ -451,9 +450,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Turn on unconstrained simplification for QF_AUFBV if (!opts.smt.unconstrainedSimpWasSetByUser) { - bool uncSimp = !logic.isQuantified() && !options::produceModels() - && !options::produceAssignments() - && !options::checkModels() + bool uncSimp = !logic.isQuantified() && !opts.smt.produceModels + && !opts.smt.produceAssignments && !opts.smt.checkModels && logic.isTheoryEnabled(THEORY_ARRAYS) && logic.isTheoryEnabled(THEORY_BV) && !logic.isTheoryEnabled(THEORY_ARITH); @@ -463,9 +461,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { - if (options::sygusInference()) + if (opts.quantifiers.sygusInference) { if (opts.quantifiers.sygusInferenceWasSetByUser) { @@ -479,7 +477,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) + if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) { /** * Operations on 1 bits are better handled as Boolean operations @@ -494,7 +492,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // explicitly if (safeUnsatCores) { - if (options::simplificationMode() != options::SimplificationMode::NONE) + if (opts.smt.simplificationMode != options::SimplificationMode::NONE) { if (opts.smt.simplificationModeWasSetByUser) { @@ -507,7 +505,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.simplificationMode = options::SimplificationMode::NONE; } - if (options::learnedRewrite()) + if (opts.smt.learnedRewrite) { if (opts.smt.learnedRewriteWasSetByUser) { @@ -519,7 +517,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.learnedRewrite = false; } - if (options::pbRewrites()) + if (opts.arith.pbRewrites) { if (opts.arith.pbRewritesWasSetByUser) { @@ -531,7 +529,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.arith.pbRewrites = false; } - if (options::sortInference()) + if (opts.smt.sortInference) { if (opts.smt.sortInferenceWasSetByUser) { @@ -542,7 +540,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.sortInference = false; } - if (options::preSkolemQuant()) + if (opts.quantifiers.preSkolemQuant) { if (opts.quantifiers.preSkolemQuantWasSetByUser) { @@ -554,7 +552,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.preSkolemQuant = false; } - if (options::bitvectorToBool()) + if (opts.bv.bitvectorToBool) { if (opts.bv.bitvectorToBoolWasSetByUser) { @@ -565,7 +563,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.bitvectorToBool = false; } - if (options::boolToBitvector() != options::BoolToBVMode::OFF) + if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) { if (opts.bv.boolToBitvectorWasSetByUser) { @@ -576,7 +574,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } - if (options::bvIntroducePow2()) + if (opts.bv.bvIntroducePow2) { if (opts.bv.bvIntroducePow2WasSetByUser) { @@ -586,7 +584,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.bvIntroducePow2 = false; } - if (options::repeatSimp()) + if (opts.smt.repeatSimp) { if (opts.smt.repeatSimpWasSetByUser) { @@ -596,7 +594,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.repeatSimp = false; } - if (options::globalNegate()) + if (opts.quantifiers.globalNegate) { if (opts.quantifiers.globalNegateWasSetByUser) { @@ -607,12 +605,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.globalNegate = false; } - if (options::bitvectorAig()) + if (opts.bv.bitvectorAig) { throw OptionException("bitblast-aig not supported with unsat cores"); } - if (options::doITESimp()) + if (opts.smt.doITESimp) { throw OptionException("ITE simp not supported with unsat cores"); } @@ -635,9 +633,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::cegqiBv() && logic.isQuantified()) + if (opts.quantifiers.cegqiBv && logic.isQuantified()) { - if (options::boolToBitvector() != options::BoolToBVMode::OFF) + if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) { if (opts.bv.boolToBitvectorWasSetByUser) { @@ -652,8 +650,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // cases where we need produce models - if (!options::produceModels() - && (options::produceAssignments() || options::sygusRewSynthCheck() + if (!opts.smt.produceModels + && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck || usesSygus)) { Notice() << "SmtEngine: turning on produce-models" << std::endl; @@ -691,13 +689,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic = log; logic.lock(); } - if (options::bvAbstraction()) + if (opts.bv.bvAbstraction) { // bv abstraction may require UF Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; needsUf = true; } - else if (options::preSkolemQuantNested() + else if (opts.quantifiers.preSkolemQuantNested && opts.quantifiers.preSkolemQuantNestedWasSetByUser) { // if pre-skolem nested is explictly set, then we require UF. If it is @@ -718,7 +716,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // then this is not required, since non-linear arithmetic will be // eliminated altogether (or otherwise fail at preprocessing). || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && options::solveIntAsBV() == 0) + && opts.smt.solveIntAsBV == 0) // FP requires UF since there are multiple operators that are partially // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more // details). @@ -737,7 +735,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } } - if (options::arithMLTrick()) + if (opts.arith.arithMLTrick) { if (!logic.areIntegersUsed()) { @@ -771,7 +769,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (!opts.uf.ufSymmetryBreakerWasSetByUser) { bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified() - && !options::incrementalSolving() && !safeUnsatCores; + && !opts.base.incrementalSolving && !safeUnsatCores; Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << std::endl; opts.uf.ufSymmetryBreaker = qf_uf_noinc; @@ -779,7 +777,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // If in arrays, set the UF handler to arrays if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder() - && !options::finiteModelFind() + && !opts.quantifiers.finiteModelFind && (!logic.isQuantified() || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF)))) { @@ -826,7 +824,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.repeatSimp = repeatSimp; } - if (options::boolToBitvector() == options::BoolToBVMode::ALL + if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL && !logic.isTheoryEnabled(THEORY_BV)) { if (opts.bv.boolToBitvectorWasSetByUser) @@ -999,7 +997,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { // disable modes not supported by incremental opts.smt.sortInference = false; @@ -1014,15 +1012,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.finiteModelFind = true; } - if (options::instMaxLevel() != -1) + if (opts.quantifiers.instMaxLevel != -1) { Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << std::endl; opts.quantifiers.cegqi = false; } - if ((opts.quantifiers.fmfBoundLazyWasSetByUser && options::fmfBoundLazy()) - || (opts.quantifiers.fmfBoundIntWasSetByUser && options::fmfBoundInt())) + if ((opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy) + || (opts.quantifiers.fmfBoundIntWasSetByUser && opts.quantifiers.fmfBoundInt)) { opts.quantifiers.fmfBound = true; Trace("smt") @@ -1030,11 +1028,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // now have determined whether fmfBound is on/off // apply fmfBound options - if (options::fmfBound()) + if (opts.quantifiers.fmfBound) { if (!opts.quantifiers.mbqiModeWasSetByUser - || (options::mbqiMode() != options::MbqiMode::NONE - && options::mbqiMode() != options::MbqiMode::FMC)) + || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE + && opts.quantifiers.mbqiMode != options::MbqiMode::FMC)) { // if bounded integers are set, use no MBQI by default opts.quantifiers.mbqiMode = options::MbqiMode::NONE; @@ -1049,28 +1047,28 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.uf.ufHo = true; // if higher-order, then current variants of model-based instantiation // cannot be used - if (options::mbqiMode() != options::MbqiMode::NONE) + if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE) { opts.quantifiers.mbqiMode = options::MbqiMode::NONE; } if (!opts.quantifiers.hoElimStoreAxWasSetByUser) { // by default, use store axioms only if --ho-elim is set - opts.quantifiers.hoElimStoreAx = options::hoElim(); + opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim; } - if (!options::assignFunctionValues()) + if (!opts.theory.assignFunctionValues) { // must assign function values opts.theory.assignFunctionValues = true; } // Cannot use macros, since lambda lifting and macro elimination are inverse // operations. - if (options::macrosQuant()) + if (opts.quantifiers.macrosQuant) { opts.quantifiers.macrosQuant = false; } // HOL is incompatible with fmfBound - if (options::fmfBound()) + if (opts.quantifiers.fmfBound) { if (opts.quantifiers.fmfBoundWasSetByUser || opts.quantifiers.fmfBoundLazyWasSetByUser @@ -1084,14 +1082,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "turning off fmf-bound, since HOL\n"; } } - if (options::fmfFunWellDefinedRelevant()) + if (opts.quantifiers.fmfFunWellDefinedRelevant) { if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) { opts.quantifiers.fmfFunWellDefined = true; } } - if (options::fmfFunWellDefined()) + if (opts.quantifiers.fmfFunWellDefined) { if (!opts.quantifiers.finiteModelFindWasSetByUser) { @@ -1101,7 +1099,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // now, have determined whether finite model find is on/off // apply finite model finding options - if (options::finiteModelFind()) + if (opts.quantifiers.finiteModelFind) { // apply conservative quantifiers splitting if (!opts.quantifiers.quantDynamicSplitWasSetByUser) @@ -1110,12 +1108,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (!opts.quantifiers.eMatchingWasSetByUser) { - opts.quantifiers.eMatching = options::fmfInstEngine(); + opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine; } if (!opts.quantifiers.instWhenModeWasSetByUser) { // instantiate only on last call - if (options::eMatching()) + if (opts.quantifiers.eMatching) { opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; } @@ -1126,7 +1124,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // if we are attempting to rewrite everything to SyGuS, use sygus() if (usesSygus) { - if (!options::sygus()) + if (!opts.quantifiers.sygus) { Trace("smt") << "turning on sygus" << std::endl; } @@ -1142,14 +1140,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { opts.quantifiers.cegqiBv = false; } - if (options::sygusRepairConst()) + if (opts.quantifiers.sygusRepairConst) { if (!opts.quantifiers.cegqiWasSetByUser) { opts.quantifiers.cegqi = true; } } - if (options::sygusInference()) + if (opts.quantifiers.sygusInference) { // optimization: apply preskolemization, makes it succeed more often if (!opts.quantifiers.preSkolemQuantWasSetByUser) @@ -1179,12 +1177,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // should use full effort cbqi for single invocation and repair const opts.quantifiers.cegqiFullEffort = true; } - if (options::sygusRew()) + if (opts.quantifiers.sygusRew) { opts.quantifiers.sygusRewSynth = true; opts.quantifiers.sygusRewVerify = true; } - if (options::sygusRewSynthInput()) + if (opts.quantifiers.sygusRewSynthInput) { // If we are using synthesis rewrite rules from input, we use // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for @@ -1203,7 +1201,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // template inference for invariant synthesis, and single invocation // techniques. bool reqBasicSygus = false; - if (options::produceAbducts()) + if (opts.smt.produceAbducts) { // if doing abduction, we should filter strong solutions if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) @@ -1214,13 +1212,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // a sygus side condition for consistency with axioms. reqBasicSygus = true; } - if (options::sygusRewSynth() || options::sygusRewVerify() - || options::sygusQueryGen()) + if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify + || opts.quantifiers.sygusQueryGen) { // rewrite rule synthesis implies that sygus stream must be true opts.quantifiers.sygusStream = true; } - if (options::sygusStream() || options::incrementalSolving()) + if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) { // Streaming and incremental mode are incompatible with techniques that // focus the search towards finding a single solution. @@ -1282,7 +1280,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || logic.isTheoryEnabled(THEORY_DATATYPES) || logic.isTheoryEnabled(THEORY_BV) || logic.isTheoryEnabled(THEORY_FP))) - || options::cegqiAll()) + || opts.quantifiers.cegqiAll) { if (!opts.quantifiers.cegqiWasSetByUser) { @@ -1297,9 +1295,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } } - if (options::cegqi()) + if (opts.quantifiers.cegqi) { - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { // cannot do nested quantifier elimination in incremental mode opts.quantifiers.cegqiNestedQE = false; @@ -1314,7 +1312,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { opts.quantifiers.instNoEntail = false; } - if (!opts.quantifiers.instWhenModeWasSetByUser && options::cegqiModel()) + if (!opts.quantifiers.instWhenModeWasSetByUser && opts.quantifiers.cegqiModel) { // only instantiation should happen at last call when model is avaiable opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; @@ -1325,7 +1323,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // only supported in pure arithmetic or pure BV opts.quantifiers.cegqiNestedQE = false; } - if (options::globalNegate()) + if (opts.quantifiers.globalNegate) { if (!opts.quantifiers.prenexQuantWasSetByUser) { @@ -1334,18 +1332,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // implied options... - if (options::strictTriggers()) + if (opts.quantifiers.strictTriggers) { if (!opts.quantifiers.userPatternsQuantWasSetByUser) { opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST; } } - if (opts.quantifiers.qcfModeWasSetByUser || options::qcfTConstraint()) + if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint) { opts.quantifiers.quantConflictFind = true; } - if (options::cegqiNestedQE()) + if (opts.quantifiers.cegqiNestedQE) { opts.quantifiers.prenexQuantUser = true; if (!opts.quantifiers.preSkolemQuantWasSetByUser) @@ -1354,7 +1352,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // for induction techniques - if (options::quantInduction()) + if (opts.quantifiers.quantInduction) { if (!opts.quantifiers.dtStcInductionWasSetByUser) { @@ -1365,7 +1363,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.intWfInduction = true; } } - if (options::dtStcInduction()) + if (opts.quantifiers.dtStcInduction) { // try to remove ITEs from quantified formulas if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser) @@ -1377,14 +1375,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL; } } - if (options::intWfInduction()) + if (opts.quantifiers.intWfInduction) { if (!opts.quantifiers.purifyTriggersWasSetByUser) { opts.quantifiers.purifyTriggers = true; } } - if (options::conjectureNoFilter()) + if (opts.quantifiers.conjectureNoFilter) { if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser) { @@ -1401,7 +1399,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (opts.quantifiers.conjectureGenPerRoundWasSetByUser) { - if (options::conjectureGenPerRound() > 0) + if (opts.quantifiers.conjectureGenPerRound > 0) { opts.quantifiers.conjectureGen = true; } @@ -1411,7 +1409,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // can't pre-skolemize nested quantifiers without UF theory - if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant()) + if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant) { if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) { @@ -1430,11 +1428,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // 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. - if (logic.isTheoryEnabled(THEORY_SETS) - || logic.isTheoryEnabled(THEORY_BAGS) - || logic.isQuantified() - || options::produceModels() || options::produceAssignments() - || options::checkModels() + if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS) + || logic.isQuantified() || opts.smt.produceModels + || opts.smt.produceAssignments || opts.smt.checkModels || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) { opts.prop.minisatUseElim = false; @@ -1442,15 +1438,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && options::nlRlvMode() != options::NlRlvMode::NONE) + && opts.arith.nlRlvMode != options::NlRlvMode::NONE) { - if (!options::relevanceFilter()) + if (!opts.theory.relevanceFilter) { if (opts.theory.relevanceFilterWasSetByUser) { Warning() << "SmtEngine: turning on relevance filtering to support " "--nl-ext-rlv=" - << options::nlRlvMode() << std::endl; + << opts.arith.nlRlvMode << std::endl; } // must use relevance filtering techniques opts.theory.relevanceFilter = true; @@ -1458,13 +1454,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // For now, these array theory optimizations do not support model-building - if (options::produceModels() || options::produceAssignments() - || options::checkModels()) + if (opts.smt.produceModels || opts.smt.produceAssignments + || opts.smt.checkModels) { opts.arrays.arraysOptimizeLinear = false; } - if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser) + if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " "--strings-fmf enabled" @@ -1475,29 +1471,29 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // !!! All options that require disabling models go here bool disableModels = false; std::string sOptNoModel; - if (opts.smt.unconstrainedSimpWasSetByUser && options::unconstrainedSimp()) + if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp) { disableModels = true; sOptNoModel = "unconstrained-simp"; } - else if (options::sortInference()) + else if (opts.smt.sortInference) { disableModels = true; sOptNoModel = "sort-inference"; } - else if (options::minisatUseElim()) + else if (opts.prop.minisatUseElim) { disableModels = true; sOptNoModel = "minisat-elimination"; } - else if (options::globalNegate()) + else if (opts.quantifiers.globalNegate) { disableModels = true; sOptNoModel = "global-negate"; } if (disableModels) { - if (options::produceModels()) + if (opts.smt.produceModels) { if (opts.smt.produceModelsWasSetByUser) { @@ -1509,7 +1505,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << sOptNoModel << std::endl; opts.smt.produceModels = false; } - if (options::produceAssignments()) + if (opts.smt.produceAssignments) { if (opts.smt.produceAssignmentsWasSetByUser) { @@ -1522,7 +1518,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << sOptNoModel << std::endl; opts.smt.produceAssignments = false; } - if (options::checkModels()) + if (opts.smt.checkModels) { if (opts.smt.checkModelsWasSetByUser) { @@ -1537,7 +1533,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::bitblastMode() == options::BitblastMode::EAGER + if (opts.bv.bitblastMode == options::BitblastMode::EAGER && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV" && logic.getLogicString() != "QF_ABV") { @@ -1551,7 +1547,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (logic == LogicInfo("QF_UFNRA")) { #ifdef CVC5_USE_POLY - if (!options::nlCad() && !opts.arith.nlCadWasSetByUser) + if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) { opts.arith.nlCad = true; if (!opts.arith.nlExtWasSetByUser) @@ -1566,7 +1562,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) #endif } #ifndef CVC5_USE_POLY - if (options::nlCad()) + if (opts.arith.nlCad) { if (opts.arith.nlCadWasSetByUser) { diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 6e77b488c..22e271c72 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -16,6 +16,7 @@ #ifndef CVC5__SMT__SET_DEFAULTS_H #define CVC5__SMT__SET_DEFAULTS_H +#include "options/options.h" #include "theory/logic_info.h" namespace cvc5 { @@ -34,7 +35,7 @@ namespace smt { * can be further refactored to modify an options object provided as an * explicit argument. */ -void setDefaults(LogicInfo& logic, bool isInternalSubsolver); +void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver); } // namespace smt } // namespace cvc5 -- 2.30.2