{
opts.smt.ackermann = true;
}
-
- if (opts.base.incrementalSolving && !logic.isPure(THEORY_BV))
- {
- throw OptionException(
- "Incremental eager bit-blasting is currently "
- "only supported for QF_BV. Try --bitblast=lazy.");
- }
}
/* Disable bit-level propagation by default for the BITBLAST solver. */
}
// if we requiring disabling proofs, disable them now
- if (mustDisableProofs(opts) && opts.smt.produceProofs)
+ if (opts.smt.produceProofs)
{
- opts.smt.unsatCores = false;
- opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
- if (opts.smt.produceProofs)
+ std::stringstream reasonNoProofs;
+ if (incompatibleWithProofs(opts, reasonNoProofs))
{
- Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
+ opts.smt.unsatCores = false;
+ opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
+ Notice() << "SmtEngine: turning off produce-proofs due to "
+ << reasonNoProofs.str() << "." << std::endl;
+ opts.smt.produceProofs = false;
+ opts.smt.checkProofs = false;
+ opts.proof.proofEagerChecking = false;
}
- opts.smt.produceProofs = false;
- opts.smt.checkProofs = false;
- opts.proof.proofEagerChecking = false;
}
// sygus core connective requires unsat cores
opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
}
- // 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 (opts.base.incrementalSolving || safeUnsatCores(opts))
- {
- if (opts.smt.unconstrainedSimp)
- {
- if (opts.smt.unconstrainedSimpWasSetByUser)
- {
- throw OptionException(
- "unconstrained simplification not supported with old unsat "
- "cores/incremental solving");
- }
- Notice() << "SmtEngine: turning off unconstrained simplification to "
- "support old unsat cores/incremental solving"
- << std::endl;
- opts.smt.unconstrainedSimp = false;
- }
- }
- else
- {
- // Turn on unconstrained simplification for QF_AUFBV
- if (!opts.smt.unconstrainedSimpWasSetByUser)
- {
- 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);
- Trace("smt") << "setting unconstrained simplification to " << uncSimp
- << std::endl;
- opts.smt.unconstrainedSimp = uncSimp;
- }
- }
-
- if (opts.base.incrementalSolving)
- {
- if (opts.quantifiers.sygusInference)
- {
- if (opts.quantifiers.sygusInferenceWasSetByUser)
- {
- throw OptionException(
- "sygus inference not supported with incremental solving");
- }
- Notice() << "SmtEngine: turning off sygus inference to support "
- "incremental solving"
- << std::endl;
- opts.quantifiers.sygusInference = false;
- }
- }
-
if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
{
/**
opts.bv.bitvectorToBool = true;
}
- // Disable options incompatible with unsat cores or output an error if enabled
- // explicitly
- if (safeUnsatCores(opts))
+ // Disable options incompatible with incremental solving, or output an error
+ // if enabled explicitly.
+ if (opts.base.incrementalSolving)
{
- if (opts.smt.simplificationMode != options::SimplificationMode::NONE)
- {
- if (opts.smt.simplificationModeWasSetByUser)
- {
- throw OptionException(
- "simplification not supported with old unsat cores");
- }
- Notice() << "SmtEngine: turning off simplification to support unsat "
- "cores"
- << std::endl;
- opts.smt.simplificationMode = options::SimplificationMode::NONE;
- }
-
- if (opts.smt.learnedRewrite)
- {
- if (opts.smt.learnedRewriteWasSetByUser)
- {
- throw OptionException(
- "learned rewrites not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off learned rewrites to support "
- "unsat cores\n";
- opts.smt.learnedRewrite = false;
- }
-
- if (opts.arith.pbRewrites)
- {
- if (opts.arith.pbRewritesWasSetByUser)
- {
- throw OptionException(
- "pseudoboolean rewrites not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
- "unsat cores\n";
- opts.arith.pbRewrites = false;
- }
-
- if (opts.smt.sortInference)
- {
- if (opts.smt.sortInferenceWasSetByUser)
- {
- throw OptionException("sort inference not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off sort inference to support unsat "
- "cores\n";
- opts.smt.sortInference = false;
- }
-
- if (opts.quantifiers.preSkolemQuant)
+ std::stringstream reasonNoInc;
+ std::stringstream suggestNoInc;
+ if (incompatibleWithIncremental(logic, opts, reasonNoInc, suggestNoInc))
{
- if (opts.quantifiers.preSkolemQuantWasSetByUser)
- {
- throw OptionException(
- "pre-skolemization not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off pre-skolemization to support "
- "unsat cores\n";
- opts.quantifiers.preSkolemQuant = false;
- }
-
- if (opts.bv.bitvectorToBool)
- {
- if (opts.bv.bitvectorToBoolWasSetByUser)
- {
- throw OptionException("bv-to-bool not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off bitvector-to-bool to support "
- "unsat cores\n";
- opts.bv.bitvectorToBool = false;
- }
-
- if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
- {
- if (opts.bv.boolToBitvectorWasSetByUser)
- {
- throw OptionException(
- "bool-to-bv != off not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off bool-to-bv to support unsat cores\n";
- opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
- }
-
- if (opts.bv.bvIntroducePow2)
- {
- if (opts.bv.bvIntroducePow2WasSetByUser)
- {
- throw OptionException("bv-intro-pow2 not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat cores";
- opts.bv.bvIntroducePow2 = false;
- }
-
- if (opts.smt.repeatSimp)
- {
- if (opts.smt.repeatSimpWasSetByUser)
- {
- throw OptionException("repeat-simp not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off repeat-simp to support unsat cores\n";
- opts.smt.repeatSimp = false;
- }
-
- if (opts.quantifiers.globalNegate)
- {
- if (opts.quantifiers.globalNegateWasSetByUser)
- {
- throw OptionException("global-negate not supported with unsat cores");
- }
- Notice() << "SmtEngine: turning off global-negate to support unsat "
- "cores\n";
- opts.quantifiers.globalNegate = false;
- }
-
- if (opts.bv.bitvectorAig)
- {
- throw OptionException("bitblast-aig not supported with unsat cores");
+ std::stringstream ss;
+ ss << reasonNoInc.str() << " not supported with incremental solving. "
+ << suggestNoInc.str();
+ throw OptionException(ss.str());
}
+ }
- if (opts.smt.doITESimp)
+ // Disable options incompatible with unsat cores or output an error if enabled
+ // explicitly
+ if (safeUnsatCores(opts))
+ {
+ // check if the options are not compatible with unsat cores
+ std::stringstream reasonNoUc;
+ if (incompatibleWithUnsatCores(opts, reasonNoUc))
{
- throw OptionException("ITE simp not supported with unsat cores");
+ std::stringstream ss;
+ ss << reasonNoUc.str() << " not supported with unsat cores";
+ throw OptionException(ss.str());
}
}
else
{
+ // Turn on unconstrained simplification for QF_AUFBV
+ if (!opts.smt.unconstrainedSimpWasSetByUser
+ && !opts.base.incrementalSolving)
+ {
+ // It is also currently incompatible with arithmetic, force the option
+ // off.
+ bool uncSimp = !opts.base.incrementalSolving && !logic.isQuantified()
+ && !opts.smt.produceModels && !opts.smt.produceAssignments
+ && !opts.smt.checkModels
+ && logic.isTheoryEnabled(THEORY_ARRAYS)
+ && logic.isTheoryEnabled(THEORY_BV)
+ && !logic.isTheoryEnabled(THEORY_ARITH);
+ Trace("smt") << "setting unconstrained simplification to " << uncSimp
+ << std::endl;
+ opts.smt.unconstrainedSimp = uncSimp;
+ }
+
// by default, nonclausal simplification is off for QF_SAT
if (!opts.smt.simplificationModeWasSetByUser)
{
// quantifiers, not others opts.set(options::simplificationMode, qf_sat ||
// quantifiers ? options::SimplificationMode::NONE :
// options::SimplificationMode::BATCH);
- opts.smt.simplificationMode = qf_sat
- ? options::SimplificationMode::NONE
- : options::SimplificationMode::BATCH;
+ opts.smt.simplificationMode = qf_sat ? options::SimplificationMode::NONE
+ : options::SimplificationMode::BATCH;
}
}
opts.smt.sortInference = false;
opts.uf.ufssFairnessMonotone = false;
opts.quantifiers.globalNegate = false;
+ opts.quantifiers.cegqiNestedQE = false;
opts.bv.bvAbstraction = false;
opts.arith.arithMLTrick = false;
}
}
// !!! 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)
+ std::stringstream reasonNoModel;
+ if (incompatibleWithModels(opts, reasonNoModel))
{
+ std::string sOptNoModel = reasonNoModel.str();
if (opts.smt.produceModels)
{
if (opts.smt.produceModelsWasSetByUser)
return false;
}
-bool SetDefaults::mustDisableProofs(const Options& opts) const
+bool SetDefaults::incompatibleWithProofs(const Options& opts,
+ std::ostream& reason) 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.
+ reason << "global-negate";
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.
+ reason << "sygus";
return true;
}
return false;
}
+bool SetDefaults::incompatibleWithModels(const Options& opts,
+ std::ostream& reason) const
+{
+ if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp)
+ {
+ reason << "unconstrained-simp";
+ return true;
+ }
+ else if (opts.smt.sortInference)
+ {
+ reason << "sort-inference";
+ return true;
+ }
+ else if (opts.prop.minisatUseElim)
+ {
+ reason << "minisat-elimination";
+ return true;
+ }
+ else if (opts.quantifiers.globalNegate)
+ {
+ reason << "global-negate";
+ return true;
+ }
+ return false;
+}
+
+bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
+ Options& opts,
+ std::ostream& reason,
+ std::ostream& suggest) const
+{
+ if (opts.smt.unconstrainedSimp)
+ {
+ if (opts.smt.unconstrainedSimpWasSetByUser)
+ {
+ reason << "unconstrained simplification";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off unconstrained simplification to "
+ "support incremental solving"
+ << std::endl;
+ opts.smt.unconstrainedSimp = false;
+ }
+ if (opts.bv.bitblastMode == options::BitblastMode::EAGER
+ && !logic.isPure(THEORY_BV))
+ {
+ reason << "eager bit-blasting in non-QF_BV logic";
+ suggest << "Try --bitblast=lazy.";
+ return true;
+ }
+ if (opts.quantifiers.sygusInference)
+ {
+ if (opts.quantifiers.sygusInferenceWasSetByUser)
+ {
+ reason << "sygus inference";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off sygus inference to support "
+ "incremental solving"
+ << std::endl;
+ opts.quantifiers.sygusInference = false;
+ }
+ return false;
+}
+
+bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
+ std::ostream& reason) const
+{
+ if (opts.smt.simplificationMode != options::SimplificationMode::NONE)
+ {
+ if (opts.smt.simplificationModeWasSetByUser)
+ {
+ reason << "simplification";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off simplification to support unsat "
+ "cores"
+ << std::endl;
+ opts.smt.simplificationMode = options::SimplificationMode::NONE;
+ }
+
+ if (opts.smt.learnedRewrite)
+ {
+ if (opts.smt.learnedRewriteWasSetByUser)
+ {
+ reason << "learned rewrites";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off learned rewrites to support "
+ "unsat cores\n";
+ opts.smt.learnedRewrite = false;
+ }
+
+ if (opts.arith.pbRewrites)
+ {
+ if (opts.arith.pbRewritesWasSetByUser)
+ {
+ reason << "pseudoboolean rewrites";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
+ "unsat cores\n";
+ opts.arith.pbRewrites = false;
+ }
+
+ if (opts.smt.sortInference)
+ {
+ if (opts.smt.sortInferenceWasSetByUser)
+ {
+ reason << "sort inference";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off sort inference to support unsat "
+ "cores\n";
+ opts.smt.sortInference = false;
+ }
+
+ if (opts.quantifiers.preSkolemQuant)
+ {
+ if (opts.quantifiers.preSkolemQuantWasSetByUser)
+ {
+ reason << "pre-skolemization";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off pre-skolemization to support "
+ "unsat cores\n";
+ opts.quantifiers.preSkolemQuant = false;
+ }
+
+ if (opts.bv.bitvectorToBool)
+ {
+ if (opts.bv.bitvectorToBoolWasSetByUser)
+ {
+ reason << "bv-to-bool";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off bitvector-to-bool to support "
+ "unsat cores\n";
+ opts.bv.bitvectorToBool = false;
+ }
+
+ if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
+ {
+ if (opts.bv.boolToBitvectorWasSetByUser)
+ {
+ reason << "bool-to-bv != off";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off bool-to-bv to support unsat cores\n";
+ opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
+ }
+
+ if (opts.bv.bvIntroducePow2)
+ {
+ if (opts.bv.bvIntroducePow2WasSetByUser)
+ {
+ reason << "bv-intro-pow2";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat cores";
+ opts.bv.bvIntroducePow2 = false;
+ }
+
+ if (opts.smt.repeatSimp)
+ {
+ if (opts.smt.repeatSimpWasSetByUser)
+ {
+ reason << "repeat-simp";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off repeat-simp to support unsat cores\n";
+ opts.smt.repeatSimp = false;
+ }
+
+ if (opts.quantifiers.globalNegate)
+ {
+ if (opts.quantifiers.globalNegateWasSetByUser)
+ {
+ reason << "global-negate";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off global-negate to support unsat "
+ "cores\n";
+ opts.quantifiers.globalNegate = false;
+ }
+
+ if (opts.bv.bitvectorAig)
+ {
+ reason << "bitblast-aig";
+ return true;
+ }
+
+ if (opts.smt.doITESimp)
+ {
+ reason << "ITE simp";
+ return true;
+ }
+ if (opts.smt.unconstrainedSimp)
+ {
+ if (opts.smt.unconstrainedSimpWasSetByUser)
+ {
+ reason << "unconstrained simplification";
+ return true;
+ }
+ Notice() << "SmtEngine: turning off unconstrained simplification to "
+ "support unsat cores"
+ << std::endl;
+ opts.smt.unconstrainedSimp = false;
+ }
+ return false;
+}
+
bool SetDefaults::safeUnsatCores(const Options& opts) const
{
// whether we want to force safe unsat cores, i.e., if we are in the default
}
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)
projects / cvc5.git / commitdiff