diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-22 22:20:59 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-22 22:20:59 -0700 |
commit | 4576b47b4acbae79c0ea76ebdc103f4c3155c4ab (patch) | |
tree | 88e3803fe39d995aa0e3306efa3d3ec97707b7e3 /src | |
parent | 2ac3d0bf2c00edbbd04033815f10ba0207010f77 (diff) |
Set same options for proofs as for unsat cores (#1957)
In SmtEngine::setDefaults() we were setting options such as
--simplifciation=none for unsat cores but not proofs. Producing unsat
cores relies on the same infrastructure as proofs and should be a subset
of the same work in most cases. Thus, this commit changes
SmtEngine::setDefaults() to set the same options for proofs as we
previously only did for unsat cores. Additionally, it changes the
function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH
if proofs and unsat cores are not enabled. Fixes issue #1953.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 197 |
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() || |