From 5369982ff5c493f72e6f8309d8be632866314805 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Sep 2021 21:47:57 -0500 Subject: [PATCH] More refactoring of set defaults (#7160) This moves a large portion of the `finalizeLogic` method to more appropriate places. It also fixes an issue : `opts.datatypes.dtSharedSelectorsWasSetByUser` was checked with wrong polarity, making a previous commit not effective. --- src/smt/set_defaults.cpp | 150 ++++++++++++++++++++------------------- src/smt/set_defaults.h | 2 +- 2 files changed, 77 insertions(+), 75 deletions(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 1e21abc47..6e7939ff7 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -131,6 +131,17 @@ void SetDefaults::setDefaultsPre(Options& opts) Assert(opts.smt.unsatCores == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)); + // new unsat core specific restrictions for proofs + if (opts.smt.unsatCores + && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) + { + // no fine-graininess + if (!opts.proof.proofGranularityModeWasSetByUser) + { + opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; + } + } + if (opts.bv.bitvectorAigSimplificationsWasSetByUser) { Notice() << "SmtEngine: setting bitvectorAig" << std::endl; @@ -141,6 +152,21 @@ void SetDefaults::setDefaultsPre(Options& opts) Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl; opts.bv.bitvectorAlgebraicSolver = true; } + + // if we requiring disabling proofs, disable them now + if (opts.smt.produceProofs) + { + std::stringstream reasonNoProofs; + if (incompatibleWithProofs(opts, reasonNoProofs)) + { + 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; + } + } } void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const @@ -185,12 +211,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const } } - /* Disable bit-level propagation by default for the BITBLAST solver. */ - if (opts.bv.bvSolver == options::BVSolver::BITBLAST) - { - opts.bv.bitvectorPropagate = false; - } - if (opts.smt.solveIntAsBV > 0) { // Int to BV currently always eliminates arithmetic completely (or otherwise @@ -260,18 +280,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const } } - // --ite-simp is an experimental option designed for QF_LIA/nec. This - // technique is experimental. This benchmark set also requires removing ITEs - // during preprocessing, before repeating simplification. Hence, we enable - // this by default. - if (opts.smt.doITESimp) - { - if (!opts.smt.earlyIteRemovalWasSetByUser) - { - opts.smt.earlyIteRemoval = true; - } - } - // Set default options associated with strings-exp. We also set these options // if we are using eager string preprocessing, which may introduce quantified // formulas at preprocess time. @@ -303,17 +311,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const // quantifiers (those marked with InternalQuantAttribute). } - // new unsat core specific restrictions for proofs - if (opts.smt.unsatCores - && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) - { - // no fine-graininess - if (!opts.proof.proofGranularityModeWasSetByUser) - { - opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; - } - } - if (opts.arrays.arraysExp) { if (!logic.isQuantified()) @@ -322,12 +319,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const logic.enableQuantifiers(); logic.lock(); } - // Allows to answer sat more often by default. - if (!opts.quantifiers.fmfBoundWasSetByUser) - { - opts.quantifiers.fmfBound = true; - Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; - } } // We now know whether the input uses sygus. Update the logic to incorporate @@ -339,20 +330,24 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const logic.lock(); } - // if we requiring disabling proofs, disable them now - if (opts.smt.produceProofs) + // widen the logic + widenLogic(logic, opts); + + // check if we have any options that are not supported with quantified logics + if (logic.isQuantified()) { - std::stringstream reasonNoProofs; - if (incompatibleWithProofs(opts, reasonNoProofs)) + std::stringstream reasonNoQuant; + if (incompatibleWithQuantifiers(opts, reasonNoQuant)) { - 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; + std::stringstream ss; + ss << reasonNoQuant.str() << " not supported in quantified logics."; + throw OptionException(ss.str()); } } +} + +void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const +{ // sygus core connective requires unsat cores if (opts.quantifiers.sygusCoreConnective) @@ -473,25 +468,19 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const Notice() << "SmtEngine: turning on produce-models" << std::endl; opts.smt.produceModels = true; } - - // widen the logic - widenLogic(logic, opts); - - // check if we have any options that are not supported with quantified logics - if (logic.isQuantified()) + + // --ite-simp is an experimental option designed for QF_LIA/nec. This + // technique is experimental. This benchmark set also requires removing ITEs + // during preprocessing, before repeating simplification. Hence, we enable + // this by default. + if (opts.smt.doITESimp) { - std::stringstream reasonNoQuant; - if (incompatibleWithQuantifiers(opts, reasonNoQuant)) + if (!opts.smt.earlyIteRemovalWasSetByUser) { - std::stringstream ss; - ss << reasonNoQuant.str() << " not supported in quantified logics."; - throw OptionException(ss.str()); + opts.smt.earlyIteRemoval = true; } } -} - -void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const -{ + // Set the options for the theoryOf if (!opts.theory.theoryOfModeWasSetByUser) { @@ -566,7 +555,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << std::endl; opts.smt.repeatSimp = repeatSimp; } - + + /* Disable bit-level propagation by default for the BITBLAST solver. */ + if (opts.bv.bvSolver == options::BVSolver::BITBLAST) + { + opts.bv.bitvectorPropagate = false; + } + if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL && !logic.isTheoryEnabled(THEORY_BV)) { @@ -678,17 +673,6 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } } - if (opts.base.incrementalSolving) - { - // disable modes not supported by incremental - opts.smt.sortInference = false; - opts.uf.ufssFairnessMonotone = false; - opts.quantifiers.globalNegate = false; - opts.quantifiers.cegqiNestedQE = false; - opts.bv.bvAbstraction = false; - opts.arith.arithMLTrick = false; - } - if (logic.isHigherOrder()) { opts.uf.ufHo = true; @@ -704,7 +688,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // shared selectors are generally not good to combine with standard // quantifier techniques e.g. E-matching - if (opts.datatypes.dtSharedSelectorsWasSetByUser) + if (!opts.datatypes.dtSharedSelectorsWasSetByUser) { if (logic.isQuantified() && !usesSygus(opts)) { @@ -996,6 +980,15 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "solveIntAsBV"; return true; } + + // disable modes not supported by incremental + opts.smt.sortInference = false; + opts.uf.ufssFairnessMonotone = false; + opts.quantifiers.globalNegate = false; + opts.quantifiers.cegqiNestedQE = false; + opts.bv.bvAbstraction = false; + opts.arith.arithMLTrick = false; + return false; } @@ -1173,7 +1166,7 @@ bool SetDefaults::incompatibleWithQuantifiers(Options& opts, return false; } -void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const +void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const { bool needsUf = false; // strings require LIA, UF; widen the logic @@ -1264,6 +1257,15 @@ void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, Options& opts) const { + if (opts.arrays.arraysExp) + { + // Allows to answer sat more often by default. + if (!opts.quantifiers.fmfBoundWasSetByUser) + { + opts.quantifiers.fmfBound = true; + Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; + } + } if (logic.hasCardinalityConstraints()) { // must have finite model finding on diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 293f1398d..4d1bf5bcb 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -115,7 +115,7 @@ class SetDefaults * use of other theories to handle certain operators, e.g. UF to handle * partial functions. */ - void widenLogic(LogicInfo& logic, Options& opts) const; + void widenLogic(LogicInfo& logic, const Options& opts) const; //------------------------- options setting, post finalization of logic /** * Set all default options, after we have finalized the logic. -- 2.30.2