void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
{
+ Options& opts = Options::current();
// implied options
if (options::debugCheckModels())
{
- options::checkModels.set(true);
+ opts.set(options::checkModels, true);
}
if (options::checkModels() || options::dumpModels())
{
- options::produceModels.set(true);
+ opts.set(options::produceModels, true);
}
if (options::checkModels())
{
- options::produceAssignments.set(true);
+ opts.set(options::produceAssignments, true);
}
// unsat cores and proofs shenanigans
if (options::dumpUnsatCoresFull())
{
- options::dumpUnsatCores.set(true);
+ opts.set(options::dumpUnsatCores, true);
}
if (options::checkUnsatCores() || options::dumpUnsatCores()
|| options::unsatAssumptions()
|| options::unsatCoresMode() != options::UnsatCoresMode::OFF)
{
- options::unsatCores.set(true);
+ opts.set(options::unsatCores, true);
}
if (options::unsatCores()
&& options::unsatCoresMode() == options::UnsatCoresMode::OFF)
{
- if (options::unsatCoresMode.wasSetByUser())
+ if (opts.wasSetByUser(options::unsatCoresMode))
{
Notice()
<< "Overriding OFF unsat-core mode since cores were requested..\n";
}
- options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
+ opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF);
}
if (options::checkProofs() || options::dumpProofs())
{
- options::produceProofs.set(true);
+ opts.set(options::produceProofs, true);
}
if (options::produceProofs()
&& options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
{
- if (options::unsatCoresMode.wasSetByUser())
+ if (opts.wasSetByUser(options::unsatCoresMode))
{
Notice() << "Forcing full-proof mode for unsat cores mode since proofs "
"were requested.\n";
}
// enable unsat cores, because they are available as a consequence of proofs
- options::unsatCores.set(true);
- options::unsatCoresMode.set(options::UnsatCoresMode::FULL_PROOF);
+ opts.set(options::unsatCores, true);
+ opts.set(options::unsatCoresMode, options::UnsatCoresMode::FULL_PROOF);
}
// set proofs on if not yet set
if (options::unsatCores() && !options::produceProofs()
&& options::unsatCoresMode() != options::UnsatCoresMode::OLD_PROOF)
{
- if (options::produceProofs.wasSetByUser())
+ if (opts.wasSetByUser(options::produceProofs))
{
Notice()
<< "Forcing proof production since new unsat cores were requested.\n";
}
- options::produceProofs.set(true);
+ opts.set(options::produceProofs, true);
}
// if unsat cores are disabled, then unsat cores mode should be OFF
Assert(options::unsatCores()
== (options::unsatCoresMode() != options::UnsatCoresMode::OFF));
- if (options::bitvectorAigSimplifications.wasSetByUser())
+ if (opts.wasSetByUser(options::bitvectorAigSimplifications))
{
Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
- options::bitvectorAig.set(true);
+ opts.set(options::bitvectorAig, true);
}
- if (options::bitvectorAlgebraicBudget.wasSetByUser())
+ if (opts.wasSetByUser(options::bitvectorAlgebraicBudget))
{
Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl;
- options::bitvectorAlgebraicSolver.set(true);
+ opts.set(options::bitvectorAlgebraicSolver, true);
}
bool isSygus = language::isInputLangSygus(options::inputLanguage());
&& (logic.isTheoryEnabled(THEORY_ARRAYS)
|| logic.isTheoryEnabled(THEORY_UF)))
{
- if (options::bitblastMode.wasSetByUser()
- || options::produceModels.wasSetByUser())
+ if (opts.wasSetByUser(options::bitblastMode)
+ || opts.wasSetByUser(options::produceModels))
{
throw OptionException(std::string(
"Eager bit-blasting currently does not support model generation "
}
Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
<< "generation" << std::endl;
- options::bitblastMode.set(options::BitblastMode::LAZY);
+ opts.set(options::bitblastMode, options::BitblastMode::LAZY);
}
else if (!options::incrementalSolving())
{
- options::ackermann.set(true);
+ opts.set(options::ackermann, true);
}
if (options::incrementalSolving() && !logic.isPure(THEORY_BV))
// Force lazy solver since we don't handle EAGER_ATOMS in the
// BVSolver::BITBLAST solver.
- options::bvSolver.set(options::BVSolver::LAZY);
+ opts.set(options::bvSolver, options::BVSolver::LAZY);
}
/* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers
if (options::bvSolver() == options::BVSolver::SIMPLE
|| options::bvSolver() == options::BVSolver::BITBLAST)
{
- options::bvLazyReduceExtf.set(false);
- options::bvLazyRewriteExtf.set(false);
+ opts.set(options::bvLazyReduceExtf, false);
+ opts.set(options::bvLazyRewriteExtf, false);
}
/* Disable bit-level propagation by default for the BITBLAST solver. */
if (options::bvSolver() == options::BVSolver::BITBLAST)
{
- options::bitvectorPropagate.set(false);
+ opts.set(options::bitvectorPropagate, false);
}
if (options::solveIntAsBV() > 0)
&& (logic.isTheoryEnabled(THEORY_ARRAYS)
|| logic.isTheoryEnabled(THEORY_UF)))
{
- if (options::produceModels.wasSetByUser())
+ if (opts.wasSetByUser(options::produceModels))
{
throw OptionException(std::string(
"Ackermannization currently does not support model generation."));
}
Notice() << "SmtEngine: turn off ackermannization to support model"
<< "generation" << std::endl;
- options::ackermann.set(false);
+ opts.set(options::ackermann, false);
}
if (options::ackermann())
// this by default.
if (options::doITESimp())
{
- if (!options::earlyIteRemoval.wasSetByUser())
+ if (!opts.wasSetByUser(options::earlyIteRemoval))
{
- options::earlyIteRemoval.set(true);
+ opts.set(options::earlyIteRemoval, true);
}
}
{
// If the user explicitly set a logic that includes strings, but is not
// the generic "ALL" logic, then enable stringsExp.
- options::stringExp.set(true);
+ opts.set(options::stringExp, true);
}
if (options::stringExp() || !options::stringLazyPreproc())
{
<< std::endl;
}
// We require bounded quantifier handling.
- if (!options::fmfBound.wasSetByUser())
+ if (!opts.wasSetByUser(options::fmfBound))
{
- options::fmfBound.set(true);
+ opts.set(options::fmfBound, true);
Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
}
// Note we allow E-matching by default to support combinations of sequences
&& options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
{
// no fine-graininess
- if (!options::proofGranularityMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::proofGranularityMode))
{
- options::proofGranularityMode.set(options::ProofGranularityMode::OFF);
+ opts.set(options::proofGranularityMode, options::ProofGranularityMode::OFF);
}
}
logic.lock();
}
// Allows to answer sat more often by default.
- if (!options::fmfBound.wasSetByUser())
+ if (!opts.wasSetByUser(options::fmfBound))
{
- options::fmfBound.set(true);
+ opts.set(options::fmfBound, true);
Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl;
}
}
// if we requiring disabling proofs, disable them now
if (disableProofs && options::produceProofs())
{
- options::unsatCores.set(false);
- options::unsatCoresMode.set(options::UnsatCoresMode::OFF);
+ opts.set(options::unsatCores, false);
+ opts.set(options::unsatCoresMode, options::UnsatCoresMode::OFF);
if (options::produceProofs())
{
Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
}
- options::produceProofs.set(false);
- options::checkProofs.set(false);
- options::proofEagerChecking.set(false);
+ opts.set(options::produceProofs, false);
+ opts.set(options::checkProofs, false);
+ opts.set(options::proofEagerChecking, false);
}
// sygus core connective requires unsat cores
if (options::sygusCoreConnective())
{
- options::unsatCores.set(true);
+ opts.set(options::unsatCores, true);
if (options::unsatCoresMode() == options::UnsatCoresMode::OFF)
{
- options::unsatCoresMode.set(options::UnsatCoresMode::OLD_PROOF);
+ opts.set(options::unsatCoresMode, options::UnsatCoresMode::OLD_PROOF);
}
}
{
Notice() << "SmtEngine: turning on produce-assertions to support "
<< "option requiring assertions." << std::endl;
- options::produceAssertions.set(true);
+ opts.set(options::produceAssertions, true);
}
// whether we want to force safe unsat cores, i.e., if we are in the OLD_PROOF
{
if (options::unconstrainedSimp())
{
- if (options::unconstrainedSimp.wasSetByUser())
+ if (opts.wasSetByUser(options::unconstrainedSimp))
{
throw OptionException(
"unconstrained simplification not supported with old unsat "
Notice() << "SmtEngine: turning off unconstrained simplification to "
"support old unsat cores/incremental solving"
<< std::endl;
- options::unconstrainedSimp.set(false);
+ opts.set(options::unconstrainedSimp, false);
}
}
else
{
// Turn on unconstrained simplification for QF_AUFBV
- if (!options::unconstrainedSimp.wasSetByUser())
+ if (!opts.wasSetByUser(options::unconstrainedSimp))
{
bool uncSimp = !logic.isQuantified() && !options::produceModels()
&& !options::produceAssignments()
&& !logic.isTheoryEnabled(THEORY_ARITH);
Trace("smt") << "setting unconstrained simplification to " << uncSimp
<< std::endl;
- options::unconstrainedSimp.set(uncSimp);
+ opts.set(options::unconstrainedSimp, uncSimp);
}
}
{
if (options::sygusInference())
{
- if (options::sygusInference.wasSetByUser())
+ if (opts.wasSetByUser(options::sygusInference))
{
throw OptionException(
"sygus inference not supported with incremental solving");
Notice() << "SmtEngine: turning off sygus inference to support "
"incremental solving"
<< std::endl;
- options::sygusInference.set(false);
+ opts.set(options::sygusInference, false);
}
}
* Therefore, we enable bv-to-bool, which runs before
* the translation to integers.
*/
- options::bitvectorToBool.set(true);
+ opts.set(options::bitvectorToBool, true);
}
// Disable options incompatible with unsat cores or output an error if enabled
{
if (options::simplificationMode() != options::SimplificationMode::NONE)
{
- if (options::simplificationMode.wasSetByUser())
+ if (opts.wasSetByUser(options::simplificationMode))
{
throw OptionException(
"simplification not supported with old unsat cores");
Notice() << "SmtEngine: turning off simplification to support unsat "
"cores"
<< std::endl;
- options::simplificationMode.set(options::SimplificationMode::NONE);
+ opts.set(options::simplificationMode, options::SimplificationMode::NONE);
}
if (options::pbRewrites())
{
- if (options::pbRewrites.wasSetByUser())
+ if (opts.wasSetByUser(options::pbRewrites))
{
throw OptionException(
"pseudoboolean rewrites not supported with old unsat cores");
}
Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
"old unsat cores\n";
- options::pbRewrites.set(false);
+ opts.set(options::pbRewrites, false);
}
if (options::sortInference())
{
- if (options::sortInference.wasSetByUser())
+ if (opts.wasSetByUser(options::sortInference))
{
throw OptionException(
"sort inference not supported with old unsat cores");
}
Notice() << "SmtEngine: turning off sort inference to support old unsat "
"cores\n";
- options::sortInference.set(false);
+ opts.set(options::sortInference, false);
}
if (options::preSkolemQuant())
{
- if (options::preSkolemQuant.wasSetByUser())
+ if (opts.wasSetByUser(options::preSkolemQuant))
{
throw OptionException(
"pre-skolemization not supported with old unsat cores");
}
Notice() << "SmtEngine: turning off pre-skolemization to support old "
"unsat cores\n";
- options::preSkolemQuant.set(false);
+ opts.set(options::preSkolemQuant, false);
}
if (options::bitvectorToBool())
{
- if (options::bitvectorToBool.wasSetByUser())
+ if (opts.wasSetByUser(options::bitvectorToBool))
{
throw OptionException("bv-to-bool not supported with old unsat cores");
}
Notice() << "SmtEngine: turning off bitvector-to-bool to support old "
"unsat cores\n";
- options::bitvectorToBool.set(false);
+ opts.set(options::bitvectorToBool, false);
}
if (options::boolToBitvector() != options::BoolToBVMode::OFF)
{
- if (options::boolToBitvector.wasSetByUser())
+ if (opts.wasSetByUser(options::boolToBitvector))
{
throw OptionException(
"bool-to-bv != off not supported with old unsat cores");
}
Notice()
<< "SmtEngine: turning off bool-to-bv to support old unsat cores\n";
- options::boolToBitvector.set(options::BoolToBVMode::OFF);
+ opts.set(options::boolToBitvector, options::BoolToBVMode::OFF);
}
if (options::bvIntroducePow2())
{
- if (options::bvIntroducePow2.wasSetByUser())
+ if (opts.wasSetByUser(options::bvIntroducePow2))
{
throw OptionException(
"bv-intro-pow2 not supported with old unsat cores");
}
Notice()
<< "SmtEngine: turning off bv-intro-pow2 to support old unsat cores";
- options::bvIntroducePow2.set(false);
+ opts.set(options::bvIntroducePow2, false);
}
if (options::repeatSimp())
{
- if (options::repeatSimp.wasSetByUser())
+ if (opts.wasSetByUser(options::repeatSimp))
{
throw OptionException("repeat-simp not supported with old unsat cores");
}
Notice()
<< "SmtEngine: turning off repeat-simp to support old unsat cores\n";
- options::repeatSimp.set(false);
+ opts.set(options::repeatSimp, false);
}
if (options::globalNegate())
{
- if (options::globalNegate.wasSetByUser())
+ if (opts.wasSetByUser(options::globalNegate))
{
throw OptionException(
"global-negate not supported with old unsat cores");
}
Notice() << "SmtEngine: turning off global-negate to support old unsat "
"cores\n";
- options::globalNegate.set(false);
+ opts.set(options::globalNegate, false);
}
if (options::bitvectorAig())
else
{
// by default, nonclausal simplification is off for QF_SAT
- if (!options::simplificationMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::simplificationMode))
{
bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified();
Trace("smt") << "setting simplification mode to <"
<< logic.getLogicString() << "> " << (!qf_sat) << std::endl;
// simplification=none works better for SMT LIB benchmarks with
- // quantifiers, not others options::simplificationMode.set(qf_sat ||
+ // quantifiers, not others opts.set(options::simplificationMode, qf_sat ||
// quantifiers ? options::SimplificationMode::NONE :
// options::SimplificationMode::BATCH);
- options::simplificationMode.set(qf_sat
+ opts.set(options::simplificationMode, qf_sat
? options::SimplificationMode::NONE
: options::SimplificationMode::BATCH);
}
{
if (options::boolToBitvector() != options::BoolToBVMode::OFF)
{
- if (options::boolToBitvector.wasSetByUser())
+ if (opts.wasSetByUser(options::boolToBitvector))
{
throw OptionException(
"bool-to-bv != off not supported with CBQI BV for quantified "
}
Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
<< std::endl;
- options::boolToBitvector.set(options::BoolToBVMode::OFF);
+ opts.set(options::boolToBitvector, options::BoolToBVMode::OFF);
}
}
|| usesSygus))
{
Notice() << "SmtEngine: turning on produce-models" << std::endl;
- options::produceModels.set(true);
+ opts.set(options::produceModels, true);
}
/////////////////////////////////////////////////////////////////////////////
needsUf = true;
}
else if (options::preSkolemQuantNested()
- && options::preSkolemQuantNested.wasSetByUser())
+ && opts.wasSetByUser(options::preSkolemQuantNested))
{
// if pre-skolem nested is explictly set, then we require UF. If it is
// not explicitly set, it is disabled below if UF is not present.
/////////////////////////////////////////////////////////////////////////////
// Set the options for the theoryOf
- if (!options::theoryOfMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::theoryOfMode))
{
if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
&& !logic.isTheoryEnabled(THEORY_STRINGS)
&& !logic.isQuantified()))
{
Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
- options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
+ opts.set(options::theoryOfMode, options::TheoryOfMode::THEORY_OF_TERM_BASED);
}
}
// by default, symmetry breaker is on only for non-incremental QF_UF
- if (!options::ufSymmetryBreaker.wasSetByUser())
+ if (!opts.wasSetByUser(options::ufSymmetryBreaker))
{
bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
&& !options::incrementalSolving() && !safeUnsatCores;
Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
<< std::endl;
- options::ufSymmetryBreaker.set(qf_uf_noinc);
+ opts.set(options::ufSymmetryBreaker, qf_uf_noinc);
}
// If in arrays, set the UF handler to arrays
Theory::setUninterpretedSortOwner(THEORY_UF);
}
- if (!options::simplifyWithCareEnabled.wasSetByUser())
+ if (!opts.wasSetByUser(options::simplifyWithCareEnabled))
{
bool qf_aufbv =
!logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
bool withCare = qf_aufbv;
Trace("smt") << "setting ite simplify with care to " << withCare
<< std::endl;
- options::simplifyWithCareEnabled.set(withCare);
+ opts.set(options::simplifyWithCareEnabled, withCare);
}
// Turn off array eager index splitting for QF_AUFLIA
- if (!options::arraysEagerIndexSplitting.wasSetByUser())
+ if (!opts.wasSetByUser(options::arraysEagerIndexSplitting))
{
if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
&& logic.isTheoryEnabled(THEORY_UF)
{
Trace("smt") << "setting array eager index splitting to false"
<< std::endl;
- options::arraysEagerIndexSplitting.set(false);
+ opts.set(options::arraysEagerIndexSplitting, false);
}
}
// Turn on multiple-pass non-clausal simplification for QF_AUFBV
- if (!options::repeatSimp.wasSetByUser())
+ if (!opts.wasSetByUser(options::repeatSimp))
{
bool repeatSimp = !logic.isQuantified()
&& (logic.isTheoryEnabled(THEORY_ARRAYS)
&& !safeUnsatCores;
Trace("smt") << "setting repeat simplification to " << repeatSimp
<< std::endl;
- options::repeatSimp.set(repeatSimp);
+ opts.set(options::repeatSimp, repeatSimp);
}
if (options::boolToBitvector() == options::BoolToBVMode::ALL
&& !logic.isTheoryEnabled(THEORY_BV))
{
- if (options::boolToBitvector.wasSetByUser())
+ if (opts.wasSetByUser(options::boolToBitvector))
{
throw OptionException(
"bool-to-bv=all not supported for non-bitvector logics.");
}
Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
<< logic.getLogicString() << std::endl;
- options::boolToBitvector.set(options::BoolToBVMode::OFF);
+ opts.set(options::boolToBitvector, options::BoolToBVMode::OFF);
}
- if (!options::bvEagerExplanations.wasSetByUser()
+ if (!opts.wasSetByUser(options::bvEagerExplanations)
&& logic.isTheoryEnabled(THEORY_ARRAYS)
&& logic.isTheoryEnabled(THEORY_BV))
{
Trace("smt") << "enabling eager bit-vector explanations " << std::endl;
- options::bvEagerExplanations.set(true);
+ opts.set(options::bvEagerExplanations, true);
}
// Turn on arith rewrite equalities only for pure arithmetic
- if (!options::arithRewriteEq.wasSetByUser())
+ if (!opts.wasSetByUser(options::arithRewriteEq))
{
bool arithRewriteEq =
logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
<< std::endl;
- options::arithRewriteEq.set(arithRewriteEq);
+ opts.set(options::arithRewriteEq, arithRewriteEq);
}
- if (!options::arithHeuristicPivots.wasSetByUser())
+ if (!opts.wasSetByUser(options::arithHeuristicPivots))
{
int16_t heuristicPivots = 5;
if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
}
Trace("smt") << "setting arithHeuristicPivots " << heuristicPivots
<< std::endl;
- options::arithHeuristicPivots.set(heuristicPivots);
+ opts.set(options::arithHeuristicPivots, heuristicPivots);
}
- if (!options::arithPivotThreshold.wasSetByUser())
+ if (!opts.wasSetByUser(options::arithPivotThreshold))
{
uint16_t pivotThreshold = 2;
if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
}
Trace("smt") << "setting arith arithPivotThreshold " << pivotThreshold
<< std::endl;
- options::arithPivotThreshold.set(pivotThreshold);
+ opts.set(options::arithPivotThreshold, pivotThreshold);
}
- if (!options::arithStandardCheckVarOrderPivots.wasSetByUser())
+ if (!opts.wasSetByUser(options::arithStandardCheckVarOrderPivots))
{
int16_t varOrderPivots = -1;
if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
}
Trace("smt") << "setting arithStandardCheckVarOrderPivots "
<< varOrderPivots << std::endl;
- options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
+ opts.set(options::arithStandardCheckVarOrderPivots, varOrderPivots);
}
if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
{
- if (!options::nlExtTangentPlanesInterleave.wasSetByUser())
+ if (!opts.wasSetByUser(options::nlExtTangentPlanesInterleave))
{
Trace("smt") << "setting nlExtTangentPlanesInterleave to true"
<< std::endl;
- options::nlExtTangentPlanesInterleave.set(true);
+ opts.set(options::nlExtTangentPlanesInterleave, true);
}
}
// Set decision mode based on logic (if not set by user)
- if (!options::decisionMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::decisionMode))
{
options::DecisionMode decMode =
// anything that uses sygus uses internal
: false);
Trace("smt") << "setting decision mode to " << decMode << std::endl;
- options::decisionMode.set(decMode);
- options::decisionStopOnly.set(stoponly);
+ opts.set(options::decisionMode, decMode);
+ opts.set(options::decisionStopOnly, stoponly);
}
if (options::incrementalSolving())
{
// disable modes not supported by incremental
- options::sortInference.set(false);
- options::ufssFairnessMonotone.set(false);
- options::globalNegate.set(false);
- options::bvAbstraction.set(false);
- options::arithMLTrick.set(false);
+ opts.set(options::sortInference, false);
+ opts.set(options::ufssFairnessMonotone, false);
+ opts.set(options::globalNegate, false);
+ opts.set(options::bvAbstraction, false);
+ opts.set(options::arithMLTrick, false);
}
if (logic.hasCardinalityConstraints())
{
// must have finite model finding on
- options::finiteModelFind.set(true);
+ opts.set(options::finiteModelFind, true);
}
if (options::instMaxLevel() != -1)
{
Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
<< std::endl;
- options::cegqi.set(false);
+ opts.set(options::cegqi, false);
}
- if ((options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy())
- || (options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt()))
+ if ((opts.wasSetByUser(options::fmfBoundLazy) && options::fmfBoundLazy())
+ || (opts.wasSetByUser(options::fmfBoundInt) && options::fmfBoundInt()))
{
- options::fmfBound.set(true);
+ opts.set(options::fmfBound, true);
}
// now have determined whether fmfBoundInt is on/off
// apply fmfBoundInt options
if (options::fmfBound())
{
- if (!options::mbqiMode.wasSetByUser()
+ if (!opts.wasSetByUser(options::mbqiMode)
|| (options::mbqiMode() != options::MbqiMode::NONE
&& options::mbqiMode() != options::MbqiMode::FMC))
{
// if bounded integers are set, use no MBQI by default
- options::mbqiMode.set(options::MbqiMode::NONE);
+ opts.set(options::mbqiMode, options::MbqiMode::NONE);
}
- if (!options::prenexQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::prenexQuant))
{
- options::prenexQuant.set(options::PrenexQuantMode::NONE);
+ opts.set(options::prenexQuant, options::PrenexQuantMode::NONE);
}
}
if (options::ufHo())
// cannot be used
if (options::mbqiMode() != options::MbqiMode::NONE)
{
- options::mbqiMode.set(options::MbqiMode::NONE);
+ opts.set(options::mbqiMode, options::MbqiMode::NONE);
}
- if (!options::hoElimStoreAx.wasSetByUser())
+ if (!opts.wasSetByUser(options::hoElimStoreAx))
{
// by default, use store axioms only if --ho-elim is set
- options::hoElimStoreAx.set(options::hoElim());
+ opts.set(options::hoElimStoreAx, options::hoElim());
}
if (!options::assignFunctionValues())
{
// must assign function values
- options::assignFunctionValues.set(true);
+ opts.set(options::assignFunctionValues, true);
}
// Cannot use macros, since lambda lifting and macro elimination are inverse
// operations.
if (options::macrosQuant())
{
- options::macrosQuant.set(false);
+ opts.set(options::macrosQuant, false);
}
}
if (options::fmfFunWellDefinedRelevant())
{
- if (!options::fmfFunWellDefined.wasSetByUser())
+ if (!opts.wasSetByUser(options::fmfFunWellDefined))
{
- options::fmfFunWellDefined.set(true);
+ opts.set(options::fmfFunWellDefined, true);
}
}
if (options::fmfFunWellDefined())
{
- if (!options::finiteModelFind.wasSetByUser())
+ if (!opts.wasSetByUser(options::finiteModelFind))
{
- options::finiteModelFind.set(true);
+ opts.set(options::finiteModelFind, true);
}
}
if (options::finiteModelFind())
{
// apply conservative quantifiers splitting
- if (!options::quantDynamicSplit.wasSetByUser())
+ if (!opts.wasSetByUser(options::quantDynamicSplit))
{
- options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
+ opts.set(options::quantDynamicSplit, options::QuantDSplitMode::DEFAULT);
}
- if (!options::eMatching.wasSetByUser())
+ if (!opts.wasSetByUser(options::eMatching))
{
- options::eMatching.set(options::fmfInstEngine());
+ opts.set(options::eMatching, options::fmfInstEngine());
}
- if (!options::instWhenMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::instWhenMode))
{
// instantiate only on last call
if (options::eMatching())
{
- options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+ opts.set(options::instWhenMode, options::InstWhenMode::LAST_CALL);
}
}
}
{
Trace("smt") << "turning on sygus" << std::endl;
}
- options::sygus.set(true);
+ opts.set(options::sygus, true);
// must use Ferrante/Rackoff for real arithmetic
- if (!options::cegqiMidpoint.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqiMidpoint))
{
- options::cegqiMidpoint.set(true);
+ opts.set(options::cegqiMidpoint, true);
}
// must disable cegqi-bv since it may introduce witness terms, which
// cannot appear in synthesis solutions
- if (!options::cegqiBv.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqiBv))
{
- options::cegqiBv.set(false);
+ opts.set(options::cegqiBv, false);
}
if (options::sygusRepairConst())
{
- if (!options::cegqi.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqi))
{
- options::cegqi.set(true);
+ opts.set(options::cegqi, true);
}
}
if (options::sygusInference())
{
// optimization: apply preskolemization, makes it succeed more often
- if (!options::preSkolemQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::preSkolemQuant))
{
- options::preSkolemQuant.set(true);
+ opts.set(options::preSkolemQuant, true);
}
- if (!options::preSkolemQuantNested.wasSetByUser())
+ if (!opts.wasSetByUser(options::preSkolemQuantNested))
{
- options::preSkolemQuantNested.set(true);
+ opts.set(options::preSkolemQuantNested, true);
}
}
// counterexample-guided instantiation for sygus
- if (!options::cegqiSingleInvMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqiSingleInvMode))
{
- options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE);
+ opts.set(options::cegqiSingleInvMode, options::CegqiSingleInvMode::USE);
}
- if (!options::quantConflictFind.wasSetByUser())
+ if (!opts.wasSetByUser(options::quantConflictFind))
{
- options::quantConflictFind.set(false);
+ opts.set(options::quantConflictFind, false);
}
- if (!options::instNoEntail.wasSetByUser())
+ if (!opts.wasSetByUser(options::instNoEntail))
{
- options::instNoEntail.set(false);
+ opts.set(options::instNoEntail, false);
}
- if (!options::cegqiFullEffort.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqiFullEffort))
{
// should use full effort cbqi for single invocation and repair const
- options::cegqiFullEffort.set(true);
+ opts.set(options::cegqiFullEffort, true);
}
if (options::sygusRew())
{
- options::sygusRewSynth.set(true);
- options::sygusRewVerify.set(true);
+ opts.set(options::sygusRewSynth, true);
+ opts.set(options::sygusRewVerify, true);
}
if (options::sygusRewSynthInput())
{
// If we are using synthesis rewrite rules from input, we use
// sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
// details on this technique.
- options::sygusRewSynth.set(true);
+ opts.set(options::sygusRewSynth, true);
// we should not use the extended rewriter, since we are interested
// in rewrites that are not in the main rewriter
- if (!options::sygusExtRew.wasSetByUser())
+ if (!opts.wasSetByUser(options::sygusExtRew))
{
- options::sygusExtRew.set(false);
+ opts.set(options::sygusExtRew, false);
}
}
// Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
if (options::produceAbducts())
{
// if doing abduction, we should filter strong solutions
- if (!options::sygusFilterSolMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::sygusFilterSolMode))
{
- options::sygusFilterSolMode.set(options::SygusFilterSolMode::STRONG);
+ opts.set(options::sygusFilterSolMode, options::SygusFilterSolMode::STRONG);
}
// we must use basic sygus algorithms, since e.g. we require checking
// a sygus side condition for consistency with axioms.
|| options::sygusQueryGen())
{
// rewrite rule synthesis implies that sygus stream must be true
- options::sygusStream.set(true);
+ opts.set(options::sygusStream, true);
}
if (options::sygusStream() || options::incrementalSolving())
{
// Now, disable options for non-basic sygus algorithms, if necessary.
if (reqBasicSygus)
{
- if (!options::sygusUnifPbe.wasSetByUser())
+ if (!opts.wasSetByUser(options::sygusUnifPbe))
{
- options::sygusUnifPbe.set(false);
+ opts.set(options::sygusUnifPbe, false);
}
- if (options::sygusUnifPi.wasSetByUser())
+ if (opts.wasSetByUser(options::sygusUnifPi))
{
- options::sygusUnifPi.set(options::SygusUnifPiMode::NONE);
+ opts.set(options::sygusUnifPi, options::SygusUnifPiMode::NONE);
}
- if (!options::sygusInvTemplMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::sygusInvTemplMode))
{
- options::sygusInvTemplMode.set(options::SygusInvTemplMode::NONE);
+ opts.set(options::sygusInvTemplMode, options::SygusInvTemplMode::NONE);
}
- if (!options::cegqiSingleInvMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqiSingleInvMode))
{
- options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE);
+ opts.set(options::cegqiSingleInvMode, options::CegqiSingleInvMode::NONE);
}
}
- if (!options::dtRewriteErrorSel.wasSetByUser())
+ if (!opts.wasSetByUser(options::dtRewriteErrorSel))
{
- options::dtRewriteErrorSel.set(true);
+ opts.set(options::dtRewriteErrorSel, true);
}
// do not miniscope
- if (!options::miniscopeQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::miniscopeQuant))
{
- options::miniscopeQuant.set(false);
+ opts.set(options::miniscopeQuant, false);
}
- if (!options::miniscopeQuantFreeVar.wasSetByUser())
+ if (!opts.wasSetByUser(options::miniscopeQuantFreeVar))
{
- options::miniscopeQuantFreeVar.set(false);
+ opts.set(options::miniscopeQuantFreeVar, false);
}
- if (!options::quantSplit.wasSetByUser())
+ if (!opts.wasSetByUser(options::quantSplit))
{
- options::quantSplit.set(false);
+ opts.set(options::quantSplit, false);
}
// do not do macros
- if (!options::macrosQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::macrosQuant))
{
- options::macrosQuant.set(false);
+ opts.set(options::macrosQuant, false);
}
// use tangent planes by default, since we want to put effort into
// the verification step for sygus queries with non-linear arithmetic
- if (!options::nlExtTangentPlanes.wasSetByUser())
+ if (!opts.wasSetByUser(options::nlExtTangentPlanes))
{
- options::nlExtTangentPlanes.set(true);
+ opts.set(options::nlExtTangentPlanes, true);
}
}
// counterexample-guided instantiation for non-sygus
|| logic.isTheoryEnabled(THEORY_FP)))
|| options::cegqiAll())
{
- if (!options::cegqi.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqi))
{
- options::cegqi.set(true);
+ opts.set(options::cegqi, true);
}
// check whether we should apply full cbqi
if (logic.isPure(THEORY_BV))
{
- if (!options::cegqiFullEffort.wasSetByUser())
+ if (!opts.wasSetByUser(options::cegqiFullEffort))
{
- options::cegqiFullEffort.set(true);
+ opts.set(options::cegqiFullEffort, true);
}
}
}
if (options::incrementalSolving())
{
// cannot do nested quantifier elimination in incremental mode
- options::cegqiNestedQE.set(false);
+ opts.set(options::cegqiNestedQE, false);
}
if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
{
- if (!options::quantConflictFind.wasSetByUser())
+ if (!opts.wasSetByUser(options::quantConflictFind))
{
- options::quantConflictFind.set(false);
+ opts.set(options::quantConflictFind, false);
}
- if (!options::instNoEntail.wasSetByUser())
+ if (!opts.wasSetByUser(options::instNoEntail))
{
- options::instNoEntail.set(false);
+ opts.set(options::instNoEntail, false);
}
- if (!options::instWhenMode.wasSetByUser() && options::cegqiModel())
+ if (!opts.wasSetByUser(options::instWhenMode) && options::cegqiModel())
{
// only instantiation should happen at last call when model is avaiable
- options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+ opts.set(options::instWhenMode, options::InstWhenMode::LAST_CALL);
}
}
else
{
// only supported in pure arithmetic or pure BV
- options::cegqiNestedQE.set(false);
+ opts.set(options::cegqiNestedQE, false);
}
if (options::globalNegate())
{
- if (!options::prenexQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::prenexQuant))
{
- options::prenexQuant.set(options::PrenexQuantMode::NONE);
+ opts.set(options::prenexQuant, options::PrenexQuantMode::NONE);
}
}
}
// implied options...
if (options::strictTriggers())
{
- if (!options::userPatternsQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::userPatternsQuant))
{
- options::userPatternsQuant.set(options::UserPatMode::TRUST);
+ opts.set(options::userPatternsQuant, options::UserPatMode::TRUST);
}
}
- if (options::qcfMode.wasSetByUser() || options::qcfTConstraint())
+ if (opts.wasSetByUser(options::qcfMode) || options::qcfTConstraint())
{
- options::quantConflictFind.set(true);
+ opts.set(options::quantConflictFind, true);
}
if (options::cegqiNestedQE())
{
- options::prenexQuantUser.set(true);
- if (!options::preSkolemQuant.wasSetByUser())
+ opts.set(options::prenexQuantUser, true);
+ if (!opts.wasSetByUser(options::preSkolemQuant))
{
- options::preSkolemQuant.set(true);
+ opts.set(options::preSkolemQuant, true);
}
}
// for induction techniques
if (options::quantInduction())
{
- if (!options::dtStcInduction.wasSetByUser())
+ if (!opts.wasSetByUser(options::dtStcInduction))
{
- options::dtStcInduction.set(true);
+ opts.set(options::dtStcInduction, true);
}
- if (!options::intWfInduction.wasSetByUser())
+ if (!opts.wasSetByUser(options::intWfInduction))
{
- options::intWfInduction.set(true);
+ opts.set(options::intWfInduction, true);
}
}
if (options::dtStcInduction())
{
// try to remove ITEs from quantified formulas
- if (!options::iteDtTesterSplitQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::iteDtTesterSplitQuant))
{
- options::iteDtTesterSplitQuant.set(true);
+ opts.set(options::iteDtTesterSplitQuant, true);
}
- if (!options::iteLiftQuant.wasSetByUser())
+ if (!opts.wasSetByUser(options::iteLiftQuant))
{
- options::iteLiftQuant.set(options::IteLiftQuantMode::ALL);
+ opts.set(options::iteLiftQuant, options::IteLiftQuantMode::ALL);
}
}
if (options::intWfInduction())
{
- if (!options::purifyTriggers.wasSetByUser())
+ if (!opts.wasSetByUser(options::purifyTriggers))
{
- options::purifyTriggers.set(true);
+ opts.set(options::purifyTriggers, true);
}
}
if (options::conjectureNoFilter())
{
- if (!options::conjectureFilterActiveTerms.wasSetByUser())
+ if (!opts.wasSetByUser(options::conjectureFilterActiveTerms))
{
- options::conjectureFilterActiveTerms.set(false);
+ opts.set(options::conjectureFilterActiveTerms, false);
}
- if (!options::conjectureFilterCanonical.wasSetByUser())
+ if (!opts.wasSetByUser(options::conjectureFilterCanonical))
{
- options::conjectureFilterCanonical.set(false);
+ opts.set(options::conjectureFilterCanonical, false);
}
- if (!options::conjectureFilterModel.wasSetByUser())
+ if (!opts.wasSetByUser(options::conjectureFilterModel))
{
- options::conjectureFilterModel.set(false);
+ opts.set(options::conjectureFilterModel, false);
}
}
- if (options::conjectureGenPerRound.wasSetByUser())
+ if (opts.wasSetByUser(options::conjectureGenPerRound))
{
if (options::conjectureGenPerRound() > 0)
{
- options::conjectureGen.set(true);
+ opts.set(options::conjectureGen, true);
}
else
{
- options::conjectureGen.set(false);
+ opts.set(options::conjectureGen, false);
}
}
// can't pre-skolemize nested quantifiers without UF theory
if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant())
{
- if (!options::preSkolemQuantNested.wasSetByUser())
+ if (!opts.wasSetByUser(options::preSkolemQuantNested))
{
- options::preSkolemQuantNested.set(false);
+ opts.set(options::preSkolemQuantNested, false);
}
}
if (!logic.isTheoryEnabled(THEORY_DATATYPES))
{
- options::quantDynamicSplit.set(options::QuantDSplitMode::NONE);
+ opts.set(options::quantDynamicSplit, options::QuantDSplitMode::NONE);
}
// until bugs 371,431 are fixed
- if (!options::minisatUseElim.wasSetByUser())
+ if (!opts.wasSetByUser(options::minisatUseElim))
{
// cannot use minisat elimination for logics where a theory solver
// introduces new literals into the search. This includes quantifiers
|| options::checkModels()
|| (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
{
- options::minisatUseElim.set(false);
+ opts.set(options::minisatUseElim, false);
}
}
{
if (!options::relevanceFilter())
{
- if (options::relevanceFilter.wasSetByUser())
+ if (opts.wasSetByUser(options::relevanceFilter))
{
Warning() << "SmtEngine: turning on relevance filtering to support "
"--nl-ext-rlv="
<< options::nlRlvMode() << std::endl;
}
// must use relevance filtering techniques
- options::relevanceFilter.set(true);
+ opts.set(options::relevanceFilter, true);
}
}
if (options::produceModels() || options::produceAssignments()
|| options::checkModels())
{
- options::arraysOptimizeLinear.set(false);
+ opts.set(options::arraysOptimizeLinear, false);
}
if (!options::bitvectorEqualitySolver())
{
if (options::bvLazyRewriteExtf())
{
- if (options::bvLazyRewriteExtf.wasSetByUser())
+ if (opts.wasSetByUser(options::bvLazyRewriteExtf))
{
throw OptionException(
"--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
Trace("smt")
<< "disabling bvLazyRewriteExtf since equality solver is disabled"
<< std::endl;
- options::bvLazyRewriteExtf.set(false);
+ opts.set(options::bvLazyRewriteExtf, false);
}
- if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser())
+ if (options::stringFMF() && !opts.wasSetByUser(options::stringProcessLoopMode))
{
Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
"--strings-fmf enabled"
<< std::endl;
- options::stringProcessLoopMode.set(options::ProcessLoopMode::SIMPLE);
+ opts.set(options::stringProcessLoopMode, options::ProcessLoopMode::SIMPLE);
}
// !!! All options that require disabling models go here
bool disableModels = false;
std::string sOptNoModel;
- if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp())
+ if (opts.wasSetByUser(options::unconstrainedSimp) && options::unconstrainedSimp())
{
disableModels = true;
sOptNoModel = "unconstrained-simp";
{
if (options::produceModels())
{
- if (options::produceModels.wasSetByUser())
+ if (opts.wasSetByUser(options::produceModels))
{
std::stringstream ss;
ss << "Cannot use " << sOptNoModel << " with model generation.";
}
Notice() << "SmtEngine: turning off produce-models to support "
<< sOptNoModel << std::endl;
- options::produceModels.set(false);
+ opts.set(options::produceModels, false);
}
if (options::produceAssignments())
{
- if (options::produceAssignments.wasSetByUser())
+ if (opts.wasSetByUser(options::produceAssignments))
{
std::stringstream ss;
ss << "Cannot use " << sOptNoModel
}
Notice() << "SmtEngine: turning off produce-assignments to support "
<< sOptNoModel << std::endl;
- options::produceAssignments.set(false);
+ opts.set(options::produceAssignments, false);
}
if (options::checkModels())
{
- if (options::checkModels.wasSetByUser())
+ if (opts.wasSetByUser(options::checkModels))
{
std::stringstream ss;
ss << "Cannot use " << sOptNoModel
}
Notice() << "SmtEngine: turning off check-models to support "
<< sOptNoModel << std::endl;
- options::checkModels.set(false);
+ opts.set(options::checkModels, false);
}
}
if (logic == LogicInfo("QF_UFNRA"))
{
#ifdef CVC5_USE_POLY
- if (!options::nlCad() && !options::nlCad.wasSetByUser())
+ if (!options::nlCad() && !opts.wasSetByUser(options::nlCad))
{
- options::nlCad.set(true);
- if (!options::nlExt.wasSetByUser())
+ opts.set(options::nlCad, true);
+ if (!opts.wasSetByUser(options::nlExt))
{
- options::nlExt.set(false);
+ opts.set(options::nlExt, false);
}
- if (!options::nlRlvMode.wasSetByUser())
+ if (!opts.wasSetByUser(options::nlRlvMode))
{
- options::nlRlvMode.set(options::NlRlvMode::INTERLEAVE);
+ opts.set(options::nlRlvMode, options::NlRlvMode::INTERLEAVE);
}
}
#endif
#ifndef CVC5_USE_POLY
if (options::nlCad())
{
- if (options::nlCad.wasSetByUser())
+ if (opts.wasSetByUser(options::nlCad))
{
std::stringstream ss;
- ss << "Cannot use " << options::nlCad.getName() << " without configuring with --poly.";
+ ss << "Cannot use " << options::nlCad.name << " without configuring with --poly.";
throw OptionException(ss.str());
}
else
{
- Notice() << "Cannot use --" << options::nlCad.getName()
+ Notice() << "Cannot use --" << options::nlCad.name
<< " without configuring with --poly." << std::endl;
- options::nlCad.set(false);
- options::nlExt.set(true);
+ opts.set(options::nlCad, false);
+ opts.set(options::nlExt, true);
}
}
#endif
// d_proofManager must be created before Options has been finished
// being parsed from the input file. Because of this, we cannot trust
- // that options::unsatCores() is set correctly yet.
+ // that d_env->getOption(options::unsatCores) is set correctly yet.
d_proofManager.reset(new ProofManager(getUserContext()));
d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
}
// set the random seed
- Random::getRandom().setSeed(options::seed());
+ Random::getRandom().setSeed(d_env->getOption(options::seed));
// Call finish init on the options manager. This inializes the resource
// manager based on the options, and sets up the best default options
d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
ProofNodeManager* pnm = nullptr;
- if (options::produceProofs())
+ if (d_env->getOption(options::produceProofs))
{
// ensure bound variable uses canonical bound variables
getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
getDumpManager()->finishInit();
// subsolvers
- if (options::produceAbducts())
+ if (d_env->getOption(options::produceAbducts))
{
d_abductSolver.reset(new AbductionSolver(this));
}
- if (options::produceInterpols() != options::ProduceInterpols::NONE)
+ if (d_env->getOption(options::produceInterpols)
+ != options::ProduceInterpols::NONE)
{
d_interpolSolver.reset(new InterpolationSolver(this));
}
// d_proofManager is always created when proofs are enabled at configure
// time. Because of this, this code should not be wrapped in PROOF() which
- // additionally checks flags such as options::produceProofs().
+ // additionally checks flags such as
+ // d_env->getOption(options::produceProofs).
//
// Note: the proof manager must be destroyed before the theory engine.
// Because the destruction of the proofs depends on contexts owned be the
{
d_state->setFilename(value);
}
- else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser())
+ else if (key == "smt-lib-version" && !Options::current().wasSetByUser(options::inputLanguage))
{
language::input::Language ilang = language::input::LANG_SMTLIB_V2_6;
<< " unsupported, defaulting to language (and semantics of) "
"SMT-LIB 2.6\n";
}
- options::inputLanguage.set(ilang);
+ Options::current().set(options::inputLanguage, ilang);
// also update the output language
- if (!options::outputLanguage.wasSetByUser())
+ if (!Options::current().wasSetByUser(options::outputLanguage))
{
language::output::Language olang = language::toOutputLanguage(ilang);
- if (options::outputLanguage() != olang)
+ if (d_env->getOption(options::outputLanguage) != olang)
{
- options::outputLanguage.set(olang);
- *options::out() << language::SetLanguage(olang);
+ Options::current().set(options::outputLanguage, olang);
+ *d_env->getOption(options::out) << language::SetLanguage(olang);
}
}
}
}
Assert(key == "all-options");
// get the options, like all-statistics
- return toSExpr(Options::current()->getOptions());
+ return toSExpr(Options::current().getOptions());
}
void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func)
const std::vector<Node>& formals,
Node func)
{
- TypeNode formulaType = formula.getType(options::typeChecking());
+ TypeNode formulaType =
+ formula.getType(d_env->getOption(options::typeChecking));
TypeNode funcType = func.getType();
// We distinguish here between definitions of constants and functions,
// because the type checking for them is subtly different. Perhaps we
Model* SmtEngine::getAvailableModel(const char* c) const
{
- if (!options::assignFunctionValues())
+ if (!d_env->getOption(options::assignFunctionValues))
{
std::stringstream ss;
ss << "Cannot " << c << " when --assign-function-values is false.";
throw RecoverableModalException(ss.str().c_str());
}
- if (!options::produceModels())
+ if (!d_env->getOption(options::produceModels))
{
std::stringstream ss;
ss << "Cannot " << c << " when produce-models options is off.";
<< "(" << assumptions << ") => " << r << endl;
// Check that SAT results generate a model correctly.
- if(options::checkModels()) {
+ if (d_env->getOption(options::checkModels))
+ {
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
checkModel();
}
}
// Check that UNSAT results generate a proof correctly.
- if (options::checkProofs() || options::proofEagerChecking())
+ if (d_env->getOption(options::checkProofs)
+ || d_env->getOption(options::proofEagerChecking))
{
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
- if ((options::checkProofs() || options::proofEagerChecking())
- && !options::produceProofs())
+ if ((d_env->getOption(options::checkProofs)
+ || d_env->getOption(options::proofEagerChecking))
+ && !d_env->getOption(options::produceProofs))
{
throw ModalException(
"Cannot check-proofs because proofs were disabled.");
}
}
// Check that UNSAT results generate an unsat core correctly.
- if (options::checkUnsatCores())
+ if (d_env->getOption(options::checkUnsatCores))
{
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
{
Trace("smt") << "SMT getUnsatAssumptions()" << endl;
SmtScope smts(this);
- if (!options::unsatAssumptions())
+ if (!d_env->getOption(options::unsatAssumptions))
{
throw ModalException(
"Cannot get unsat assumptions when produce-unsat-assumptions option "
Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
|| resultNode.isConst());
- if(options::abstractValues() && resultNode.getType().isArray()) {
+ if (d_env->getOption(options::abstractValues)
+ && resultNode.getType().isArray())
+ {
resultNode = d_absValues->mkAbstractValue(resultNode);
Trace("smt") << "--- abstract value >> " << resultNode << endl;
}
Assert(te != nullptr);
te->setEagerModelBuilding();
- if (options::modelCoresMode() != options::ModelCoresMode::NONE)
+ if (d_env->getOption(options::modelCoresMode)
+ != options::ModelCoresMode::NONE)
{
// If we enabled model cores, we compute a model core for m based on our
// (expanded) assertions using the model core builder utility
std::vector<Node> eassertsProc = getExpandedAssertions();
- ModelCoreBuilder::setModelCore(
- eassertsProc, m->getTheoryModel(), options::modelCoresMode());
+ ModelCoreBuilder::setModelCore(eassertsProc,
+ m->getTheoryModel(),
+ d_env->getOption(options::modelCoresMode));
}
// set the information on the SMT-level model
Assert(m != nullptr);
Model* m = getAvailableModel("block model");
- if (options::blockModelsMode() == options::BlockModelsMode::NONE)
+ if (d_env->getOption(options::blockModelsMode)
+ == options::BlockModelsMode::NONE)
{
std::stringstream ss;
ss << "Cannot block model when block-models is set to none.";
// get expanded assertions
std::vector<Node> eassertsProc = getExpandedAssertions();
- Node eblocker = ModelBlocker::getModelBlocker(
- eassertsProc, m->getTheoryModel(), options::blockModelsMode());
+ Node eblocker =
+ ModelBlocker::getModelBlocker(eassertsProc,
+ m->getTheoryModel(),
+ d_env->getOption(options::blockModelsMode));
return assertFormula(eblocker);
}
void SmtEngine::checkProof()
{
- Assert(options::produceProofs());
+ Assert(d_env->getOption(options::produceProofs));
// internal check the proof
PropEngine* pe = getPropEngine();
Assert(pe != nullptr);
- if (options::proofEagerChecking())
+ if (d_env->getOption(options::proofEagerChecking))
{
pe->checkProof(d_asserts->getAssertionList());
}
Assert(pe->getProof() != nullptr);
std::shared_ptr<ProofNode> pePfn = pe->getProof();
- if (options::checkProofs())
+ if (d_env->getOption(options::checkProofs))
{
d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
}
UnsatCore SmtEngine::getUnsatCoreInternal()
{
- if (!options::unsatCores())
+ if (!d_env->getOption(options::unsatCores))
{
throw ModalException(
"Cannot get an unsat core when produce-unsat-cores[-new] or "
}
void SmtEngine::checkUnsatCore() {
- Assert(options::unsatCores())
+ Assert(d_env->getOption(options::unsatCores))
<< "cannot check unsat core if unsat cores are turned off";
Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
{
getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
}
- if (!options::produceProofs())
+ if (!d_env->getOption(options::produceProofs))
{
throw ModalException("Cannot get a proof when proof option is off.");
}
void SmtEngine::printInstantiations( std::ostream& out ) {
SmtScope smts(this);
finishInit();
- if (options::instFormatMode() == options::InstFormatMode::SZS)
+ if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
{
out << "% SZS output start Proof for " << d_state->getFilename()
<< std::endl;
// First, extract and print the skolemizations
bool printed = false;
- bool reqNames = !options::printInstFull();
+ bool reqNames = !d_env->getOption(options::printInstFull);
// only print when in list mode
- if (options::printInstMode() == options::PrintInstMode::LIST)
+ if (d_env->getOption(options::printInstMode) == options::PrintInstMode::LIST)
{
std::map<Node, std::vector<Node>> sks;
qe->getSkolemTermVectors(sks);
continue;
}
// must have a name
- if (options::printInstMode() == options::PrintInstMode::NUM)
+ if (d_env->getOption(options::printInstMode) == options::PrintInstMode::NUM)
{
out << "(num-instantiations " << name << " " << i.second.size() << ")"
<< std::endl;
}
else
{
- Assert(options::printInstMode() == options::PrintInstMode::LIST);
+ Assert(d_env->getOption(options::printInstMode)
+ == options::PrintInstMode::LIST);
InstantiationList ilist(name, i.second);
out << ilist;
}
{
out << "No instantiations" << std::endl;
}
- if (options::instFormatMode() == options::InstFormatMode::SZS)
+ if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
{
out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
}
{
SmtScope smts(this);
finishInit();
- if (options::produceProofs()
- && (!options::unsatCores()
- || options::unsatCoresMode() == options::UnsatCoresMode::FULL_PROOF)
+ if (d_env->getOption(options::produceProofs)
+ && (!d_env->getOption(options::unsatCores)
+ || d_env->getOption(options::unsatCoresMode) == options::UnsatCoresMode::FULL_PROOF)
&& getSmtMode() == SmtMode::UNSAT)
{
// minimize instantiations based on proof manager
getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut());
}
Trace("smt") << "SMT getAssertions()" << endl;
- if(!options::produceAssertions()) {
+ if (!d_env->getOption(options::produceAssertions))
+ {
const char* msg =
"Cannot query the current assertion list when not in produce-assertions mode.";
throw ModalException(msg);
projects / cvc5.git / commitdiff