From: Andres Noetzli Date: Wed, 13 Jun 2018 17:04:34 +0000 (-0700) Subject: Disable unconstrainedSimp pass when proofs enabled (#1976) X-Git-Tag: cvc5-1.0.0~4967 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7c4cd3ecacb1e484a076edde0274c282bb43ffb;p=cvc5.git Disable unconstrainedSimp pass when proofs enabled (#1976) Currently, we may end up enabling the unconstrainedSimp pass when proofs are enabled because the check that this pass is disabled happens before a check for automatically enabling it. This lead to issues when running for example on regress0/aufbv/bug00.smt with --check-proofs. This commit moves the code for automatically enabling the pass to only be run if proofs and unsat cores are disabled. Note: This commit is mostly a simple code move but formatting in setDefaults was a bit off, so there are a lot of formatting changes. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 69cea8b06..1b5e88536 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1422,155 +1422,181 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning on produce-assertions to support " << "check-models or check-synth-sol." << endl; setOption("produce-assertions", SExpr("true")); - } + } - if (options::unsatCores() || options::proof()) + // Disable options incompatible with incremental solving, unsat cores, and + // proofs or output an error if enabled explicitly + if (options::incrementalSolving() || options::unsatCores() + || options::proof()) + { + if (options::unconstrainedSimp()) { - if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE) + if (options::unconstrainedSimp.wasSetByUser()) { - 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); + throw OptionException( + "unconstrained simplification not supported with unsat " + "cores/proofs/incremental solving"); } - - if (options::unconstrainedSimp()) + Notice() << "SmtEngine: turning off unconstrained simplification to " + "support unsat cores/proofs/incremental solving" + << endl; + options::unconstrainedSimp.set(false); + } + } + else + { + // Turn on unconstrained simplification for QF_AUFBV + if (!options::unconstrainedSimp.wasSetByUser()) + { + // bool qf_sat = d_logic.isPure(THEORY_BOOL) && + // !d_logic.isQuantified(); bool uncSimp = false && !qf_sat && + // !options::incrementalSolving(); + bool uncSimp = !d_logic.isQuantified() && !options::produceModels() + && !options::produceAssignments() + && !options::checkModels() + && (d_logic.isTheoryEnabled(THEORY_ARRAYS) + && d_logic.isTheoryEnabled(THEORY_BV)); + Trace("smt") << "setting unconstrained simplification to " << uncSimp + << endl; + options::unconstrainedSimp.set(uncSimp); + } + } + + // Disable options incompatible with unsat cores and proofs or output an + // error if enabled explicitly + if (options::unsatCores() || options::proof()) + { + if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE) + { + if (options::simplificationMode.wasSetByUser()) { - 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); + 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); + } - if (options::pbRewrites()) + if (options::pbRewrites()) + { + if (options::pbRewrites.wasSetByUser()) { - 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); + 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); + } - if (options::sortInference()) + if (options::sortInference()) + { + if (options::sortInference.wasSetByUser()) { - 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); + 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); + } - if (options::preSkolemQuant()) + if (options::preSkolemQuant()) + { + if (options::preSkolemQuant.wasSetByUser()) { - 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); + 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); + } - if (options::bitvectorToBool()) + if (options::bitvectorToBool()) + { + if (options::bitvectorToBool.wasSetByUser()) { - 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); + 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); + } - if (options::boolToBitvector()) + if (options::boolToBitvector()) + { + if (options::boolToBitvector.wasSetByUser()) { - 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); + 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); + } - if (options::bvIntroducePow2()) + if (options::bvIntroducePow2()) + { + if (options::bvIntroducePow2.wasSetByUser()) { - 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); + 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); + } - if (options::repeatSimp()) + if (options::repeatSimp()) + { + if (options::repeatSimp.wasSetByUser()) { - 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); + 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); + } - if (options::globalNegate()) + if (options::globalNegate()) + { + if (options::globalNegate.wasSetByUser()) { - 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); + 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); } - else + } + else + { + // by default, nonclausal simplification is off for QF_SAT + if (!options::simplificationMode.wasSetByUser()) { - // 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); - } + 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()) @@ -1717,21 +1743,6 @@ void SmtEngine::setDefaults() { Trace("smt") << "setting repeat simplification to " << repeatSimp << endl; options::repeatSimp.set(repeatSimp); } - // Turn on unconstrained simplification for QF_AUFBV - if(!options::unconstrainedSimp.wasSetByUser() || - options::incrementalSolving()) { - // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); - // bool uncSimp = false && !qf_sat && !options::incrementalSolving(); - bool uncSimp = !options::incrementalSolving() && - !d_logic.isQuantified() && - !options::produceModels() && - !options::produceAssignments() && - !options::checkModels() && - !options::unsatCores() && - (d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV)); - Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl; - options::unconstrainedSimp.set(uncSimp); - } // Unconstrained simp currently does *not* support model generation if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) { if (options::produceModels()) {