summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp197
1 files changed, 126 insertions, 71 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e96393f11..114527334 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1419,90 +1419,153 @@ void SmtEngine::setDefaults() {
setOption("produce-assertions", SExpr("true"));
}
- if(options::unsatCores()) {
- if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
- if(options::simplificationMode.wasSetByUser()) {
- throw OptionException("simplification not supported with unsat cores");
+ if (options::unsatCores() || options::proof())
+ {
+ if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE)
+ {
+ if (options::simplificationMode.wasSetByUser())
+ {
+ throw OptionException(
+ "simplification not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off simplification to support unsat "
+ "cores/proofs"
+ << endl;
+ options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
}
- Notice() << "SmtEngine: turning off simplification to support unsat-cores"
- << endl;
- options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
- }
- if(options::unconstrainedSimp()) {
- if(options::unconstrainedSimp.wasSetByUser()) {
- throw OptionException("unconstrained simplification not supported with unsat cores");
+ if (options::unconstrainedSimp())
+ {
+ if (options::unconstrainedSimp.wasSetByUser())
+ {
+ throw OptionException(
+ "unconstrained simplification not supported with unsat "
+ "cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off unconstrained simplification to "
+ "support unsat cores/proofs"
+ << endl;
+ options::unconstrainedSimp.set(false);
}
- Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl;
- options::unconstrainedSimp.set(false);
- }
- if(options::pbRewrites()) {
- if(options::pbRewrites.wasSetByUser()) {
- throw OptionException("pseudoboolean rewrites not supported with unsat cores");
+ if (options::pbRewrites())
+ {
+ if (options::pbRewrites.wasSetByUser())
+ {
+ throw OptionException(
+ "pseudoboolean rewrites not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
+ "unsat cores/proofs"
+ << endl;
+ setOption("pb-rewrites", false);
}
- Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl;
- setOption("pb-rewrites", false);
- }
- if(options::sortInference()) {
- if(options::sortInference.wasSetByUser()) {
- throw OptionException("sort inference not supported with unsat cores");
+ if (options::sortInference())
+ {
+ if (options::sortInference.wasSetByUser())
+ {
+ throw OptionException(
+ "sort inference not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off sort inference to support unsat "
+ "cores/proofs"
+ << endl;
+ options::sortInference.set(false);
}
- Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl;
- options::sortInference.set(false);
- }
- if(options::preSkolemQuant()) {
- if(options::preSkolemQuant.wasSetByUser()) {
- throw OptionException("pre-skolemization not supported with unsat cores");
+ if (options::preSkolemQuant())
+ {
+ if (options::preSkolemQuant.wasSetByUser())
+ {
+ throw OptionException(
+ "pre-skolemization not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
+ "cores/proofs"
+ << endl;
+ options::preSkolemQuant.set(false);
}
- Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl;
- options::preSkolemQuant.set(false);
- }
- if(options::bitvectorToBool()) {
- if(options::bitvectorToBool.wasSetByUser()) {
- throw OptionException("bv-to-bool not supported with unsat cores");
+ if (options::bitvectorToBool())
+ {
+ if (options::bitvectorToBool.wasSetByUser())
+ {
+ throw OptionException(
+ "bv-to-bool not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
+ "cores/proofs"
+ << endl;
+ options::bitvectorToBool.set(false);
}
- Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat-cores" << endl;
- options::bitvectorToBool.set(false);
- }
- if(options::boolToBitvector()) {
- if(options::boolToBitvector.wasSetByUser()) {
- throw OptionException("bool-to-bv not supported with unsat cores");
+ if (options::boolToBitvector())
+ {
+ if (options::boolToBitvector.wasSetByUser())
+ {
+ throw OptionException(
+ "bool-to-bv not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat "
+ "cores/proofs"
+ << endl;
+ options::boolToBitvector.set(false);
}
- Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat-cores" << endl;
- options::boolToBitvector.set(false);
- }
- if(options::bvIntroducePow2()) {
- if(options::bvIntroducePow2.wasSetByUser()) {
- throw OptionException("bv-intro-pow2 not supported with unsat cores");
+ if (options::bvIntroducePow2())
+ {
+ if (options::bvIntroducePow2.wasSetByUser())
+ {
+ throw OptionException(
+ "bv-intro-pow2 not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
+ "unsat-cores/proofs"
+ << endl;
+ setOption("bv-intro-pow2", false);
}
- Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat-cores" << endl;
- setOption("bv-intro-pow2", false);
- }
- if(options::repeatSimp()) {
- if(options::repeatSimp.wasSetByUser()) {
- throw OptionException("repeat-simp not supported with unsat cores");
+ if (options::repeatSimp())
+ {
+ if (options::repeatSimp.wasSetByUser())
+ {
+ throw OptionException(
+ "repeat-simp not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off repeat-simp to support unsat "
+ "cores/proofs"
+ << endl;
+ setOption("repeat-simp", false);
}
- Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl;
- setOption("repeat-simp", false);
- }
- if (options::globalNegate())
- {
- if (options::globalNegate.wasSetByUser())
+ if (options::globalNegate())
{
- throw OptionException("global-negate not supported with unsat cores");
+ if (options::globalNegate.wasSetByUser())
+ {
+ throw OptionException(
+ "global-negate not supported with unsat cores/proofs");
+ }
+ Notice() << "SmtEngine: turning off global-negate to support unsat "
+ "cores/proofs"
+ << endl;
+ setOption("global-negate", false);
}
- Notice() << "SmtEngine: turning off global-negate to support unsat-cores"
- << endl;
- setOption("global-negate", false);
}
+ else
+ {
+ // by default, nonclausal simplification is off for QF_SAT
+ if (!options::simplificationMode.wasSetByUser())
+ {
+ bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
+ Trace("smt") << "setting simplification mode to <"
+ << d_logic.getLogicString() << "> " << (!qf_sat) << endl;
+ // simplification=none works better for SMT LIB benchmarks with
+ // quantifiers, not others options::simplificationMode.set(qf_sat ||
+ // quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
+ options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE
+ : SIMPLIFICATION_MODE_BATCH);
+ }
}
if (options::cbqiBv() && d_logic.isQuantified())
@@ -1570,14 +1633,6 @@ void SmtEngine::setDefaults() {
Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
options::ufSymmetryBreaker.set(qf_uf);
}
- // by default, nonclausal simplification is off for QF_SAT
- if(! options::simplificationMode.wasSetByUser()) {
- bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
- Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << endl;
- //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
- //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
- options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
- }
// If in arrays, set the UF handler to arrays
if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() ||
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback