opts.bv.bitvectorAlgebraicSolver = true;
}
- bool isSygus = language::isInputLangSygus(opts.base.inputLanguage);
- bool usesSygus = isSygus;
-
if (opts.bv.bitblastMode == options::BitblastMode::EAGER)
{
if (opts.smt.produceModels
// the bounded integers module will always process internally generated
// quantifiers (those marked with InternalQuantAttribute).
}
- // whether we must disable proofs
- bool disableProofs = false;
- 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.
- disableProofs = true;
- }
// new unsat core specific restrictions for proofs
if (opts.smt.unsatCores
}
}
- // sygus inference may require datatypes
- if (!d_isInternalSubsolver)
- {
- 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 (opts.quantifiers.sygusInst)
- {
- // sygus instantiation uses sygus, but it is not a sygus problem
- usesSygus = true;
- }
- }
-
// We now know whether the input uses sygus. Update the logic to incorporate
// the theories we need internally for handling sygus problems.
- if (usesSygus)
+ if (usesSygus(opts))
{
logic = logic.getUnlockedCopy();
logic.enableSygus();
logic.lock();
- if (isSygus)
- {
- // When sygus answers "unsat", it is not due to showing a set of
- // formulas is unsat in the standard way. Thus, proofs do not apply.
- disableProofs = true;
- }
}
// if we requiring disabling proofs, disable them now
- if (disableProofs && opts.smt.produceProofs)
+ if (mustDisableProofs(opts) && opts.smt.produceProofs)
{
opts.smt.unsatCores = false;
opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
// cases where we need produce models
if (!opts.smt.produceModels
&& (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck
- || usesSygus))
+ || usesSygus(opts)))
{
Notice() << "SmtEngine: turning on produce-models" << std::endl;
opts.smt.produceModels = true;
}
}
- // Set decision mode based on logic (if not set by user)
- if (!opts.decision.decisionModeWasSetByUser)
- {
- options::DecisionMode decMode =
- // anything that uses sygus uses internal
- usesSygus ? options::DecisionMode::INTERNAL :
- // ALL or its supersets
- logic.hasEverything()
- ? options::DecisionMode::JUSTIFICATION
- : ( // QF_BV
- (not logic.isQuantified() && logic.isPure(THEORY_BV)) ||
- // QF_AUFBV or QF_ABV or QF_UFBV
- (not logic.isQuantified()
- && (logic.isTheoryEnabled(THEORY_ARRAYS)
- || logic.isTheoryEnabled(THEORY_UF))
- && logic.isTheoryEnabled(THEORY_BV))
- ||
- // QF_AUFLIA (and may be ends up enabling
- // QF_AUFLRA?)
- (not logic.isQuantified()
- && logic.isTheoryEnabled(THEORY_ARRAYS)
- && logic.isTheoryEnabled(THEORY_UF)
- && logic.isTheoryEnabled(THEORY_ARITH))
- ||
- // QF_LRA
- (not logic.isQuantified()
- && logic.isPure(THEORY_ARITH) && logic.isLinear()
- && !logic.isDifferenceLogic()
- && !logic.areIntegersUsed())
- ||
- // Quantifiers
- logic.isQuantified() ||
- // Strings
- logic.isTheoryEnabled(THEORY_STRINGS)
- ? options::DecisionMode::JUSTIFICATION
- : options::DecisionMode::INTERNAL);
-
- bool stoponly =
- // ALL or its supersets
- logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
- ? false
- : ( // QF_AUFLIA
- (not logic.isQuantified()
- && logic.isTheoryEnabled(THEORY_ARRAYS)
- && logic.isTheoryEnabled(THEORY_UF)
- && logic.isTheoryEnabled(THEORY_ARITH))
- ||
- // QF_LRA
- (not logic.isQuantified()
- && logic.isPure(THEORY_ARITH) && logic.isLinear()
- && !logic.isDifferenceLogic()
- && !logic.areIntegersUsed())
- ? true
- : false);
-
- opts.decision.decisionMode = decMode;
- if (stoponly)
- {
- if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION)
- {
- opts.decision.decisionMode = options::DecisionMode::STOPONLY;
- }
- else
- {
- Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL);
- }
- }
- Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
- << std::endl;
- }
+ // set the default decision mode
+ setDefaultDecisionMode(logic, opts);
// set up of central equality engine
if (opts.theory.eeMode == options::EqEngineMode::CENTRAL)
opts.bv.bvAbstraction = false;
opts.arith.arithMLTrick = false;
}
- if (logic.hasCardinalityConstraints())
- {
- // must have finite model finding on
- opts.quantifiers.finiteModelFind = true;
- }
-
- if (opts.quantifiers.instMaxLevel != -1)
- {
- Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
- << std::endl;
- opts.quantifiers.cegqi = false;
- }
- if ((opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy)
- || (opts.quantifiers.fmfBoundIntWasSetByUser && opts.quantifiers.fmfBoundInt))
- {
- opts.quantifiers.fmfBound = true;
- Trace("smt")
- << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n";
- }
- // now have determined whether fmfBound is on/off
- // apply fmfBound options
- if (opts.quantifiers.fmfBound)
- {
- if (!opts.quantifiers.mbqiModeWasSetByUser
- || (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;
- }
- if (!opts.quantifiers.prenexQuantUserWasSetByUser)
- {
- opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
- }
- }
if (logic.isHigherOrder())
{
opts.uf.ufHo = true;
- // if higher-order, then current variants of model-based instantiation
- // cannot be used
- 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 = opts.quantifiers.hoElim;
- }
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 (opts.quantifiers.macrosQuant)
+ }
+
+ // set all defaults in the quantifiers theory, which includes sygus
+ setDefaultsQuantifiers(logic, opts);
+
+ // until bugs 371,431 are fixed
+ if (!opts.prop.minisatUseElimWasSetByUser)
+ {
+ // cannot use minisat 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.
+ 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.quantifiers.macrosQuant = false;
+ opts.prop.minisatUseElim = false;
}
- // HOL is incompatible with fmfBound
- if (opts.quantifiers.fmfBound)
+ }
+
+ if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+ && opts.arith.nlRlvMode != options::NlRlvMode::NONE)
+ {
+ if (!opts.theory.relevanceFilter)
{
- if (opts.quantifiers.fmfBoundWasSetByUser
- || opts.quantifiers.fmfBoundLazyWasSetByUser
- || opts.quantifiers.fmfBoundIntWasSetByUser)
+ if (opts.theory.relevanceFilterWasSetByUser)
{
- Notice() << "Disabling bound finite-model finding since it is "
- "incompatible with HOL.\n";
+ Warning() << "SmtEngine: turning on relevance filtering to support "
+ "--nl-ext-rlv="
+ << opts.arith.nlRlvMode << std::endl;
}
-
- opts.quantifiers.fmfBound = false;
- Trace("smt") << "turning off fmf-bound, since HOL\n";
+ // must use relevance filtering techniques
+ opts.theory.relevanceFilter = true;
}
}
- if (opts.quantifiers.fmfFunWellDefinedRelevant)
+
+ // For now, these array theory optimizations do not support model-building
+ if (opts.smt.produceModels || opts.smt.produceAssignments
+ || opts.smt.checkModels)
{
- if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser)
- {
- opts.quantifiers.fmfFunWellDefined = true;
- }
+ opts.arrays.arraysOptimizeLinear = false;
}
- if (opts.quantifiers.fmfFunWellDefined)
+
+ if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser)
{
- if (!opts.quantifiers.finiteModelFindWasSetByUser)
- {
- opts.quantifiers.finiteModelFind = true;
- }
+ Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
+ "--strings-fmf enabled"
+ << std::endl;
+ opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE;
}
- // now, have determined whether finite model find is on/off
- // apply finite model finding options
- if (opts.quantifiers.finiteModelFind)
+ // !!! All options that require disabling models go here
+ bool disableModels = false;
+ std::string sOptNoModel;
+ if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp)
{
- // apply conservative quantifiers splitting
- if (!opts.quantifiers.quantDynamicSplitWasSetByUser)
+ disableModels = true;
+ sOptNoModel = "unconstrained-simp";
+ }
+ else if (opts.smt.sortInference)
+ {
+ disableModels = true;
+ sOptNoModel = "sort-inference";
+ }
+ else if (opts.prop.minisatUseElim)
+ {
+ disableModels = true;
+ sOptNoModel = "minisat-elimination";
+ }
+ else if (opts.quantifiers.globalNegate)
+ {
+ disableModels = true;
+ sOptNoModel = "global-negate";
+ }
+ if (disableModels)
+ {
+ if (opts.smt.produceModels)
{
- opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT;
+ if (opts.smt.produceModelsWasSetByUser)
+ {
+ std::stringstream ss;
+ ss << "Cannot use " << sOptNoModel << " with model generation.";
+ throw OptionException(ss.str());
+ }
+ Notice() << "SmtEngine: turning off produce-models to support "
+ << sOptNoModel << std::endl;
+ opts.smt.produceModels = false;
}
- if (!opts.quantifiers.eMatchingWasSetByUser)
+ if (opts.smt.produceAssignments)
{
- opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine;
+ if (opts.smt.produceAssignmentsWasSetByUser)
+ {
+ std::stringstream ss;
+ ss << "Cannot use " << sOptNoModel
+ << " with model generation (produce-assignments).";
+ throw OptionException(ss.str());
+ }
+ Notice() << "SmtEngine: turning off produce-assignments to support "
+ << sOptNoModel << std::endl;
+ opts.smt.produceAssignments = false;
}
- if (!opts.quantifiers.instWhenModeWasSetByUser)
+ if (opts.smt.checkModels)
{
- // instantiate only on last call
- if (opts.quantifiers.eMatching)
+ if (opts.smt.checkModelsWasSetByUser)
{
- opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
+ std::stringstream ss;
+ ss << "Cannot use " << sOptNoModel
+ << " with model generation (check-models).";
+ throw OptionException(ss.str());
}
+ Notice() << "SmtEngine: turning off check-models to support "
+ << sOptNoModel << std::endl;
+ opts.smt.checkModels = false;
}
}
- // apply sygus options
- // if we are attempting to rewrite everything to SyGuS, use sygus()
- if (usesSygus)
+ if (opts.bv.bitblastMode == options::BitblastMode::EAGER
+ && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV"
+ && logic.getLogicString() != "QF_ABV")
{
- setDefaultsSygus(opts);
+ throw OptionException(
+ "Eager bit-blasting does not currently support theory combination. "
+ "Note that in a QF_BV problem UF symbols can be introduced for "
+ "division. "
+ "Try --bv-div-zero-const to interpret division by zero as a constant.");
}
- // counterexample-guided instantiation for non-sygus
- // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
- if ((logic.isQuantified()
- && (logic.isTheoryEnabled(THEORY_ARITH)
- || logic.isTheoryEnabled(THEORY_DATATYPES)
- || logic.isTheoryEnabled(THEORY_BV)
- || logic.isTheoryEnabled(THEORY_FP)))
- || opts.quantifiers.cegqiAll)
+
+#ifdef CVC5_USE_POLY
+ if (logic == LogicInfo("QF_UFNRA"))
{
- if (!opts.quantifiers.cegqiWasSetByUser)
- {
- opts.quantifiers.cegqi = true;
- }
- // check whether we should apply full cbqi
- if (logic.isPure(THEORY_BV))
+ if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser)
{
- if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
+ opts.arith.nlCad = true;
+ if (!opts.arith.nlExtWasSetByUser)
{
- opts.quantifiers.cegqiFullEffort = true;
+ opts.arith.nlExt = options::NlExtMode::LIGHT;
+ }
+ if (!opts.arith.nlRlvModeWasSetByUser)
+ {
+ opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE;
}
}
}
- if (opts.quantifiers.cegqi)
+#else
+ if (opts.arith.nlCad)
{
- if (opts.base.incrementalSolving)
+ if (opts.arith.nlCadWasSetByUser)
{
- // cannot do nested quantifier elimination in incremental mode
- opts.quantifiers.cegqiNestedQE = false;
+ std::stringstream ss;
+ ss << "Cannot use " << options::arith::nlCad__name
+ << " without configuring with --poly.";
+ throw OptionException(ss.str());
}
- if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
+ else
{
- if (!opts.quantifiers.quantConflictFindWasSetByUser)
- {
- opts.quantifiers.quantConflictFind = false;
- }
- if (!opts.quantifiers.instNoEntailWasSetByUser)
- {
- opts.quantifiers.instNoEntail = false;
+ Notice() << "Cannot use --" << options::arith::nlCad__name
+ << " without configuring with --poly." << std::endl;
+ opts.arith.nlCad = false;
+ opts.arith.nlExt = options::NlExtMode::FULL;
+ }
+ }
+#endif
+}
+
+bool SetDefaults::isSygus(const Options& opts) const
+{
+ if (language::isInputLangSygus(opts.base.inputLanguage))
+ {
+ return true;
+ }
+ if (!d_isInternalSubsolver)
+ {
+ 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
+ return true;
+ }
+ }
+ return false;
+}
+
+bool SetDefaults::usesSygus(const Options& opts) const
+{
+ if (isSygus(opts))
+ {
+ return true;
+ }
+ if (!d_isInternalSubsolver && opts.quantifiers.sygusInst)
+ {
+ // sygus instantiation uses sygus, but it is not a sygus problem
+ return true;
+ }
+ return false;
+}
+
+bool SetDefaults::mustDisableProofs(const Options& opts) const
+{
+ 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.
+ return true;
+ }
+ if (isSygus(opts))
+ {
+ // When sygus answers "unsat", it is not due to showing a set of
+ // formulas is unsat in the standard way. Thus, proofs do not apply.
+ return true;
+ }
+ return false;
+}
+
+void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const
+{
+ bool needsUf = false;
+ // strings require LIA, UF; widen the logic
+ if (logic.isTheoryEnabled(THEORY_STRINGS))
+ {
+ LogicInfo log(logic.getUnlockedCopy());
+ // Strings requires arith for length constraints, and also UF
+ needsUf = true;
+ if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
+ {
+ Notice()
+ << "Enabling linear integer arithmetic because strings are enabled"
+ << std::endl;
+ log.enableTheory(THEORY_ARITH);
+ log.enableIntegers();
+ log.arithOnlyLinear();
+ }
+ else if (!logic.areIntegersUsed())
+ {
+ Notice() << "Enabling integer arithmetic because strings are enabled"
+ << std::endl;
+ log.enableIntegers();
+ }
+ logic = log;
+ logic.lock();
+ }
+ if (opts.bv.bvAbstraction)
+ {
+ // bv abstraction may require UF
+ Notice() << "Enabling UF because bvAbstraction requires it." << std::endl;
+ needsUf = true;
+ }
+ else if (opts.quantifiers.preSkolemQuantNested
+ && opts.quantifiers.preSkolemQuantNestedWasSetByUser)
+ {
+ // 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.
+ Notice() << "Enabling UF because preSkolemQuantNested requires it."
+ << std::endl;
+ needsUf = true;
+ }
+ if (needsUf
+ // Arrays, datatypes and sets permit Boolean terms and thus require UF
+ || logic.isTheoryEnabled(THEORY_ARRAYS)
+ || logic.isTheoryEnabled(THEORY_DATATYPES)
+ || logic.isTheoryEnabled(THEORY_SETS)
+ || logic.isTheoryEnabled(THEORY_BAGS)
+ // Non-linear arithmetic requires UF to deal with division/mod because
+ // their expansion introduces UFs for the division/mod-by-zero case.
+ // If we are eliminating non-linear arithmetic via solve-int-as-bv,
+ // then this is not required, since non-linear arithmetic will be
+ // eliminated altogether (or otherwise fail at preprocessing).
+ || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+ && 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).
+ || logic.isTheoryEnabled(THEORY_FP))
+ {
+ if (!logic.isTheoryEnabled(THEORY_UF))
+ {
+ LogicInfo log(logic.getUnlockedCopy());
+ if (!needsUf)
+ {
+ Notice() << "Enabling UF because " << logic << " requires it."
+ << std::endl;
+ }
+ log.enableTheory(THEORY_UF);
+ logic = log;
+ logic.lock();
+ }
+ }
+ if (opts.arith.arithMLTrick)
+ {
+ if (!logic.areIntegersUsed())
+ {
+ // enable integers
+ LogicInfo log(logic.getUnlockedCopy());
+ Notice() << "Enabling integers because arithMLTrick requires it."
+ << std::endl;
+ log.enableIntegers();
+ logic = log;
+ logic.lock();
+ }
+ }
+}
+
+void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
+ Options& opts) const
+{
+ if (logic.hasCardinalityConstraints())
+ {
+ // must have finite model finding on
+ opts.quantifiers.finiteModelFind = true;
+ }
+
+ if (opts.quantifiers.instMaxLevel != -1)
+ {
+ Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
+ << std::endl;
+ opts.quantifiers.cegqi = false;
+ }
+
+ if ((opts.quantifiers.fmfBoundLazyWasSetByUser
+ && opts.quantifiers.fmfBoundLazy)
+ || (opts.quantifiers.fmfBoundIntWasSetByUser
+ && opts.quantifiers.fmfBoundInt))
+ {
+ opts.quantifiers.fmfBound = true;
+ Trace("smt")
+ << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n";
+ }
+ // now have determined whether fmfBound is on/off
+ // apply fmfBound options
+ if (opts.quantifiers.fmfBound)
+ {
+ if (!opts.quantifiers.mbqiModeWasSetByUser
+ || (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;
+ }
+ if (!opts.quantifiers.prenexQuantUserWasSetByUser)
+ {
+ opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
+ }
+ }
+ if (logic.isHigherOrder())
+ {
+ // if higher-order, then current variants of model-based instantiation
+ // cannot be used
+ 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 = opts.quantifiers.hoElim;
+ }
+ // Cannot use macros, since lambda lifting and macro elimination are inverse
+ // operations.
+ if (opts.quantifiers.macrosQuant)
+ {
+ opts.quantifiers.macrosQuant = false;
+ }
+ // HOL is incompatible with fmfBound
+ if (opts.quantifiers.fmfBound)
+ {
+ if (opts.quantifiers.fmfBoundWasSetByUser
+ || opts.quantifiers.fmfBoundLazyWasSetByUser
+ || opts.quantifiers.fmfBoundIntWasSetByUser)
+ {
+ Notice() << "Disabling bound finite-model finding since it is "
+ "incompatible with HOL.\n";
+ }
+
+ opts.quantifiers.fmfBound = false;
+ Trace("smt") << "turning off fmf-bound, since HOL\n";
+ }
+ }
+ if (opts.quantifiers.fmfFunWellDefinedRelevant)
+ {
+ if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser)
+ {
+ opts.quantifiers.fmfFunWellDefined = true;
+ }
+ }
+ if (opts.quantifiers.fmfFunWellDefined)
+ {
+ if (!opts.quantifiers.finiteModelFindWasSetByUser)
+ {
+ opts.quantifiers.finiteModelFind = true;
+ }
+ }
+
+ // now, have determined whether finite model find is on/off
+ // apply finite model finding options
+ if (opts.quantifiers.finiteModelFind)
+ {
+ // apply conservative quantifiers splitting
+ if (!opts.quantifiers.quantDynamicSplitWasSetByUser)
+ {
+ opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::DEFAULT;
+ }
+ if (!opts.quantifiers.eMatchingWasSetByUser)
+ {
+ opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine;
+ }
+ if (!opts.quantifiers.instWhenModeWasSetByUser)
+ {
+ // instantiate only on last call
+ if (opts.quantifiers.eMatching)
+ {
+ opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
+ }
+ }
+ }
+
+ // apply sygus options
+ // if we are attempting to rewrite everything to SyGuS, use sygus()
+ if (usesSygus(opts))
+ {
+ setDefaultsSygus(opts);
+ }
+ // counterexample-guided instantiation for non-sygus
+ // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
+ if ((logic.isQuantified()
+ && (logic.isTheoryEnabled(THEORY_ARITH)
+ || logic.isTheoryEnabled(THEORY_DATATYPES)
+ || logic.isTheoryEnabled(THEORY_BV)
+ || logic.isTheoryEnabled(THEORY_FP)))
+ || opts.quantifiers.cegqiAll)
+ {
+ if (!opts.quantifiers.cegqiWasSetByUser)
+ {
+ opts.quantifiers.cegqi = true;
+ }
+ // check whether we should apply full cbqi
+ if (logic.isPure(THEORY_BV))
+ {
+ if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
+ {
+ opts.quantifiers.cegqiFullEffort = true;
+ }
+ }
+ }
+ if (opts.quantifiers.cegqi)
+ {
+ if (opts.base.incrementalSolving)
+ {
+ // cannot do nested quantifier elimination in incremental mode
+ opts.quantifiers.cegqiNestedQE = false;
+ }
+ if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
+ {
+ if (!opts.quantifiers.quantConflictFindWasSetByUser)
+ {
+ opts.quantifiers.quantConflictFind = false;
+ }
+ if (!opts.quantifiers.instNoEntailWasSetByUser)
+ {
+ opts.quantifiers.instNoEntail = false;
}
- if (!opts.quantifiers.instWhenModeWasSetByUser && opts.quantifiers.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;
{
opts.quantifiers.quantDynamicSplit = options::QuantDSplitMode::NONE;
}
-
- // until bugs 371,431 are fixed
- if (!opts.prop.minisatUseElimWasSetByUser)
- {
- // cannot use minisat 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.
- 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;
- }
- }
-
- if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
- && opts.arith.nlRlvMode != options::NlRlvMode::NONE)
- {
- if (!opts.theory.relevanceFilter)
- {
- if (opts.theory.relevanceFilterWasSetByUser)
- {
- Warning() << "SmtEngine: turning on relevance filtering to support "
- "--nl-ext-rlv="
- << opts.arith.nlRlvMode << std::endl;
- }
- // must use relevance filtering techniques
- opts.theory.relevanceFilter = true;
- }
- }
-
- // For now, these array theory optimizations do not support model-building
- if (opts.smt.produceModels || opts.smt.produceAssignments
- || opts.smt.checkModels)
- {
- opts.arrays.arraysOptimizeLinear = false;
- }
-
- if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser)
- {
- Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
- "--strings-fmf enabled"
- << std::endl;
- opts.strings.stringProcessLoopMode = options::ProcessLoopMode::SIMPLE;
- }
-
- // !!! All options that require disabling models go here
- bool disableModels = false;
- std::string sOptNoModel;
- if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp)
- {
- disableModels = true;
- sOptNoModel = "unconstrained-simp";
- }
- else if (opts.smt.sortInference)
- {
- disableModels = true;
- sOptNoModel = "sort-inference";
- }
- else if (opts.prop.minisatUseElim)
- {
- disableModels = true;
- sOptNoModel = "minisat-elimination";
- }
- else if (opts.quantifiers.globalNegate)
- {
- disableModels = true;
- sOptNoModel = "global-negate";
- }
- if (disableModels)
- {
- if (opts.smt.produceModels)
- {
- if (opts.smt.produceModelsWasSetByUser)
- {
- std::stringstream ss;
- ss << "Cannot use " << sOptNoModel << " with model generation.";
- throw OptionException(ss.str());
- }
- Notice() << "SmtEngine: turning off produce-models to support "
- << sOptNoModel << std::endl;
- opts.smt.produceModels = false;
- }
- if (opts.smt.produceAssignments)
- {
- if (opts.smt.produceAssignmentsWasSetByUser)
- {
- std::stringstream ss;
- ss << "Cannot use " << sOptNoModel
- << " with model generation (produce-assignments).";
- throw OptionException(ss.str());
- }
- Notice() << "SmtEngine: turning off produce-assignments to support "
- << sOptNoModel << std::endl;
- opts.smt.produceAssignments = false;
- }
- if (opts.smt.checkModels)
- {
- if (opts.smt.checkModelsWasSetByUser)
- {
- std::stringstream ss;
- ss << "Cannot use " << sOptNoModel
- << " with model generation (check-models).";
- throw OptionException(ss.str());
- }
- Notice() << "SmtEngine: turning off check-models to support "
- << sOptNoModel << std::endl;
- opts.smt.checkModels = false;
- }
- }
-
- if (opts.bv.bitblastMode == options::BitblastMode::EAGER
- && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV"
- && logic.getLogicString() != "QF_ABV")
- {
- throw OptionException(
- "Eager bit-blasting does not currently support theory combination. "
- "Note that in a QF_BV problem UF symbols can be introduced for "
- "division. "
- "Try --bv-div-zero-const to interpret division by zero as a constant.");
- }
-
- if (logic == LogicInfo("QF_UFNRA"))
- {
-#ifdef CVC5_USE_POLY
- if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser)
- {
- opts.arith.nlCad = true;
- if (!opts.arith.nlExtWasSetByUser)
- {
- opts.arith.nlExt = options::NlExtMode::LIGHT;
- }
- if (!opts.arith.nlRlvModeWasSetByUser)
- {
- opts.arith.nlRlvMode = options::NlRlvMode::INTERLEAVE;
- }
- }
-#endif
- }
-#ifndef CVC5_USE_POLY
- if (opts.arith.nlCad)
- {
- if (opts.arith.nlCadWasSetByUser)
- {
- std::stringstream ss;
- ss << "Cannot use " << options::arith::nlCad__name << " without configuring with --poly.";
- throw OptionException(ss.str());
- }
- else
- {
- Notice() << "Cannot use --" << options::arith::nlCad__name
- << " without configuring with --poly." << std::endl;
- opts.arith.nlCad = false;
- opts.arith.nlExt = options::NlExtMode::FULL;
- }
- }
-#endif
-}
-
-void SetDefaults::widenLogic(LogicInfo& logic, Options& opts)
-{
- bool needsUf = false;
- // strings require LIA, UF; widen the logic
- if (logic.isTheoryEnabled(THEORY_STRINGS))
- {
- LogicInfo log(logic.getUnlockedCopy());
- // Strings requires arith for length constraints, and also UF
- needsUf = true;
- if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
- {
- Notice()
- << "Enabling linear integer arithmetic because strings are enabled"
- << std::endl;
- log.enableTheory(THEORY_ARITH);
- log.enableIntegers();
- log.arithOnlyLinear();
- }
- else if (!logic.areIntegersUsed())
- {
- Notice() << "Enabling integer arithmetic because strings are enabled"
- << std::endl;
- log.enableIntegers();
- }
- logic = log;
- logic.lock();
- }
- if (opts.bv.bvAbstraction)
- {
- // bv abstraction may require UF
- Notice() << "Enabling UF because bvAbstraction requires it." << std::endl;
- needsUf = true;
- }
- else if (opts.quantifiers.preSkolemQuantNested
- && opts.quantifiers.preSkolemQuantNestedWasSetByUser)
- {
- // 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.
- Notice() << "Enabling UF because preSkolemQuantNested requires it."
- << std::endl;
- needsUf = true;
- }
- if (needsUf
- // Arrays, datatypes and sets permit Boolean terms and thus require UF
- || logic.isTheoryEnabled(THEORY_ARRAYS)
- || logic.isTheoryEnabled(THEORY_DATATYPES)
- || logic.isTheoryEnabled(THEORY_SETS)
- || logic.isTheoryEnabled(THEORY_BAGS)
- // Non-linear arithmetic requires UF to deal with division/mod because
- // their expansion introduces UFs for the division/mod-by-zero case.
- // If we are eliminating non-linear arithmetic via solve-int-as-bv,
- // then this is not required, since non-linear arithmetic will be
- // eliminated altogether (or otherwise fail at preprocessing).
- || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
- && 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).
- || logic.isTheoryEnabled(THEORY_FP))
- {
- if (!logic.isTheoryEnabled(THEORY_UF))
- {
- LogicInfo log(logic.getUnlockedCopy());
- if (!needsUf)
- {
- Notice() << "Enabling UF because " << logic << " requires it."
- << std::endl;
- }
- log.enableTheory(THEORY_UF);
- logic = log;
- logic.lock();
- }
- }
- if (opts.arith.arithMLTrick)
- {
- if (!logic.areIntegersUsed())
- {
- // enable integers
- LogicInfo log(logic.getUnlockedCopy());
- Notice() << "Enabling integers because arithMLTrick requires it."
- << std::endl;
- log.enableIntegers();
- logic = log;
- logic.lock();
- }
- }
}
-void SetDefaults::setDefaultsSygus(Options& opts)
+void SetDefaults::setDefaultsSygus(Options& opts) const
{
if (!opts.quantifiers.sygus)
{
opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE;
}
}
- if (!opts.datatypes.dtRewriteErrorSelWasSetByUser)
- {
- opts.datatypes.dtRewriteErrorSel = true;
- }
// do not miniscope
if (!opts.quantifiers.miniscopeQuantWasSetByUser)
{
{
opts.quantifiers.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 (!opts.arith.nlExtTangentPlanesWasSetByUser)
- {
- opts.arith.nlExtTangentPlanes = true;
+}
+void SetDefaults::setDefaultDecisionMode(const LogicInfo& logic,
+ Options& opts) const
+{
+ // Set decision mode based on logic (if not set by user)
+ if (opts.decision.decisionModeWasSetByUser)
+ {
+ return;
+ }
+ options::DecisionMode decMode =
+ // anything that uses sygus uses internal
+ usesSygus(opts) ? options::DecisionMode::INTERNAL :
+ // ALL or its supersets
+ logic.hasEverything()
+ ? options::DecisionMode::JUSTIFICATION
+ : ( // QF_BV
+ (not logic.isQuantified() && logic.isPure(THEORY_BV)) ||
+ // QF_AUFBV or QF_ABV or QF_UFBV
+ (not logic.isQuantified()
+ && (logic.isTheoryEnabled(THEORY_ARRAYS)
+ || logic.isTheoryEnabled(THEORY_UF))
+ && logic.isTheoryEnabled(THEORY_BV))
+ ||
+ // QF_AUFLIA (and may be ends up enabling
+ // QF_AUFLRA?)
+ (not logic.isQuantified()
+ && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_UF)
+ && logic.isTheoryEnabled(THEORY_ARITH))
+ ||
+ // QF_LRA
+ (not logic.isQuantified()
+ && logic.isPure(THEORY_ARITH) && logic.isLinear()
+ && !logic.isDifferenceLogic()
+ && !logic.areIntegersUsed())
+ ||
+ // Quantifiers
+ logic.isQuantified() ||
+ // Strings
+ logic.isTheoryEnabled(THEORY_STRINGS)
+ ? options::DecisionMode::JUSTIFICATION
+ : options::DecisionMode::INTERNAL);
+
+ bool stoponly =
+ // ALL or its supersets
+ logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
+ ? false
+ : ( // QF_AUFLIA
+ (not logic.isQuantified()
+ && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_UF)
+ && logic.isTheoryEnabled(THEORY_ARITH))
+ ||
+ // QF_LRA
+ (not logic.isQuantified() && logic.isPure(THEORY_ARITH)
+ && logic.isLinear() && !logic.isDifferenceLogic()
+ && !logic.areIntegersUsed())
+ ? true
+ : false);
+
+ opts.decision.decisionMode = decMode;
+ if (stoponly)
+ {
+ if (opts.decision.decisionMode == options::DecisionMode::JUSTIFICATION)
+ {
+ opts.decision.decisionMode = options::DecisionMode::STOPONLY;
+ }
+ else
+ {
+ Assert(opts.decision.decisionMode == options::DecisionMode::INTERNAL);
+ }
}
+ Trace("smt") << "setting decision mode to " << opts.decision.decisionMode
+ << std::endl;
}
} // namespace smt
projects / cvc5.git / commitdiff