From 06f4747e4f6c97be9b6fca4edd1ffff66e386c06 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 12 Aug 2021 17:12:19 -0700 Subject: Refactor setDefaults to use an options object (#6994) This commit refactors the `setDefaults` method to accept an `Options` object as argument instead of using the current (static) `Options` object. --- src/smt/options_manager.cpp | 2 +- src/smt/set_defaults.cpp | 292 ++++++++++++++++++++++---------------------- src/smt/set_defaults.h | 3 +- 3 files changed, 147 insertions(+), 150 deletions(-) (limited to 'src') diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index a5dee27ae..9ffb396d1 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -41,7 +41,7 @@ void OptionsManager::notifySetOption(const std::string& key) void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver) { // ensure that our heuristics are properly set up - setDefaults(logic, isInternalSubsolver); + setDefaults(logic, *d_options, isInternalSubsolver); } } // namespace smt diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e23323e6d..c916ac962 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -46,35 +46,34 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -void setDefaults(LogicInfo& logic, bool isInternalSubsolver) +void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) { - Options& opts = Options::current(); // implied options - if (options::debugCheckModels()) + if (opts.smt.debugCheckModels) { opts.smt.checkModels = true; } - if (options::checkModels() || options::dumpModels()) + if (opts.smt.checkModels || opts.driver.dumpModels) { opts.smt.produceModels = true; } - if (options::checkModels()) + if (opts.smt.checkModels) { opts.smt.produceAssignments = true; } // unsat cores and proofs shenanigans - if (options::dumpUnsatCoresFull()) + if (opts.driver.dumpUnsatCoresFull) { opts.driver.dumpUnsatCores = true; } - if (options::checkUnsatCores() || options::dumpUnsatCores() - || options::unsatAssumptions() || options::minimalUnsatCores() - || options::unsatCoresMode() != options::UnsatCoresMode::OFF) + if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores + || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores + || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF) { opts.smt.unsatCores = true; } - if (options::unsatCores() - && options::unsatCoresMode() == options::UnsatCoresMode::OFF) + if (opts.smt.unsatCores + && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) { if (opts.smt.unsatCoresModeWasSetByUser) { @@ -84,13 +83,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; } - if (options::checkProofs() || options::dumpProofs()) + if (opts.smt.checkProofs || opts.driver.dumpProofs) { opts.smt.produceProofs = true; } - if (options::produceProofs() - && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) + if (opts.smt.produceProofs + && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) { if (opts.smt.unsatCoresModeWasSetByUser) { @@ -103,7 +102,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // set proofs on if not yet set - if (options::unsatCores() && !options::produceProofs()) + if (opts.smt.unsatCores && !opts.smt.produceProofs) { if (opts.smt.produceProofsWasSetByUser) { @@ -114,8 +113,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // if unsat cores are disabled, then unsat cores mode should be OFF - Assert(options::unsatCores() - == (options::unsatCoresMode() != options::UnsatCoresMode::OFF)); + Assert(opts.smt.unsatCores + == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)); if (opts.bv.bitvectorAigSimplificationsWasSetByUser) { @@ -128,12 +127,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.bitvectorAlgebraicSolver = true; } - bool isSygus = language::isInputLangSygus(options::inputLanguage()); + bool isSygus = language::isInputLangSygus(opts.base.inputLanguage); bool usesSygus = isSygus; - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (opts.bv.bitblastMode == options::BitblastMode::EAGER) { - if (options::produceModels() + if (opts.smt.produceModels && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { @@ -149,12 +148,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << "generation" << std::endl; opts.bv.bitblastMode = options::BitblastMode::LAZY; } - else if (!options::incrementalSolving()) + else if (!opts.base.incrementalSolving) { opts.smt.ackermann = true; } - if (options::incrementalSolving() && !logic.isPure(THEORY_BV)) + if (opts.base.incrementalSolving && !logic.isPure(THEORY_BV)) { throw OptionException( "Incremental eager bit-blasting is currently " @@ -163,15 +162,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } /* Disable bit-level propagation by default for the BITBLAST solver. */ - if (options::bvSolver() == options::BVSolver::BITBLAST) + if (opts.bv.bvSolver == options::BVSolver::BITBLAST) { opts.bv.bitvectorPropagate = false; } - if (options::solveIntAsBV() > 0) + if (opts.smt.solveIntAsBV > 0) { // not compatible with incremental - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { throw OptionException( "solving integers as bitvectors is currently not supported " @@ -186,14 +185,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } - if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) + if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) { - if (options::boolToBitvector() != options::BoolToBVMode::OFF) + if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) { throw OptionException( "solving bitvectors as integers is incompatible with --bool-to-bv."); } - if (options::BVAndIntegerGranularity() > 8) + if (opts.smt.BVAndIntegerGranularity > 8) { /** * The granularity sets the size of the ITE in each element @@ -214,7 +213,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // set options about ackermannization - if (options::ackermann() && options::produceModels() + if (opts.smt.ackermann && opts.smt.produceModels && (logic.isTheoryEnabled(THEORY_ARRAYS) || logic.isTheoryEnabled(THEORY_UF))) { @@ -228,9 +227,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.ackermann = false; } - if (options::ackermann()) + if (opts.smt.ackermann) { - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { throw OptionException( "Incremental Ackermannization is currently not supported."); @@ -259,7 +258,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // technique is experimental. This benchmark set also requires removing ITEs // during preprocessing, before repeating simplification. Hence, we enable // this by default. - if (options::doITESimp()) + if (opts.smt.doITESimp) { if (!opts.smt.earlyIteRemovalWasSetByUser) { @@ -280,7 +279,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "Turning stringExp on since logic does not have everything " "and string theory is enabled\n"; } - if (options::stringExp() || !options::stringLazyPreproc()) + if (opts.strings.stringExp || !opts.strings.stringLazyPreproc) { // We require quantifiers since extended functions reduce using them. if (!logic.isQuantified()) @@ -299,7 +298,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // whether we must disable proofs bool disableProofs = false; - if (options::globalNegate()) + 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. @@ -307,8 +306,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // new unsat core specific restrictions for proofs - if (options::unsatCores() - && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) + if (opts.smt.unsatCores + && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) { // no fine-graininess if (!opts.proof.proofGranularityModeWasSetByUser) @@ -317,7 +316,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::arraysExp()) + if (opts.arrays.arraysExp) { if (!logic.isQuantified()) { @@ -336,15 +335,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // sygus inference may require datatypes if (!isInternalSubsolver) { - if (options::produceAbducts() - || options::produceInterpols() != options::ProduceInterpols::NONE - || options::sygusInference() || options::sygusRewSynthInput()) + if (opts.smt.produceAbducts + || opts.smt.produceInterpols != options::ProduceInterpols::NONE + || opts.quantifiers.sygusInference + || opts.quantifiers.sygusRewSynthInput) { // since we are trying to recast as sygus, we assume the input is sygus isSygus = true; usesSygus = true; } - else if (options::sygusInst()) + else if (opts.quantifiers.sygusInst) { // sygus instantiation uses sygus, but it is not a sygus problem usesSygus = true; @@ -367,11 +367,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // if we requiring disabling proofs, disable them now - if (disableProofs && options::produceProofs()) + if (disableProofs && opts.smt.produceProofs) { opts.smt.unsatCores = false; opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; - if (options::produceProofs()) + if (opts.smt.produceProofs) { Notice() << "SmtEngine: turning off produce-proofs." << std::endl; } @@ -381,29 +381,28 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // sygus core connective requires unsat cores - if (options::sygusCoreConnective()) + if (opts.quantifiers.sygusCoreConnective) { opts.smt.unsatCores = true; - if (options::unsatCoresMode() == options::UnsatCoresMode::OFF) + if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF) { opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS; } } - if ((options::checkModels() || options::checkSynthSol() - || options::produceAbducts() - || options::produceInterpols() != options::ProduceInterpols::NONE - || options::modelCoresMode() != options::ModelCoresMode::NONE - || options::blockModelsMode() != options::BlockModelsMode::NONE - || options::produceProofs()) - && !options::produceAssertions()) + if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts + || opts.smt.produceInterpols != options::ProduceInterpols::NONE + || opts.smt.modelCoresMode != options::ModelCoresMode::NONE + || opts.smt.blockModelsMode != options::BlockModelsMode::NONE + || opts.smt.produceProofs) + && !opts.smt.produceAssertions) { Notice() << "SmtEngine: turning on produce-assertions to support " << "option requiring assertions." << std::endl; opts.smt.produceAssertions = true; } - if (options::bvAssertInput() && options::produceProofs()) + if (opts.bv.bvAssertInput && opts.smt.produceProofs) { Notice() << "Disabling bv-assert-input since it is incompatible with proofs." << std::endl; @@ -412,8 +411,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // If proofs are required and the user did not specify a specific BV solver, // we make sure to use the proof producing BITBLAST_INTERNAL solver. - if (options::produceProofs() - && options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL + if (opts.smt.produceProofs + && opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL && !opts.bv.bvSolverWasSetByUser && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT) { @@ -425,14 +424,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // whether we want to force safe unsat cores, i.e., if we are in the default // ASSUMPTIONS mode, since other ones are experimental bool safeUnsatCores = - options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS; + opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS; // 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 (options::incrementalSolving() || safeUnsatCores) + if (opts.base.incrementalSolving || safeUnsatCores) { - if (options::unconstrainedSimp()) + if (opts.smt.unconstrainedSimp) { if (opts.smt.unconstrainedSimpWasSetByUser) { @@ -451,9 +450,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Turn on unconstrained simplification for QF_AUFBV if (!opts.smt.unconstrainedSimpWasSetByUser) { - bool uncSimp = !logic.isQuantified() && !options::produceModels() - && !options::produceAssignments() - && !options::checkModels() + 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); @@ -463,9 +461,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { - if (options::sygusInference()) + if (opts.quantifiers.sygusInference) { if (opts.quantifiers.sygusInferenceWasSetByUser) { @@ -479,7 +477,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) + if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) { /** * Operations on 1 bits are better handled as Boolean operations @@ -494,7 +492,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // explicitly if (safeUnsatCores) { - if (options::simplificationMode() != options::SimplificationMode::NONE) + if (opts.smt.simplificationMode != options::SimplificationMode::NONE) { if (opts.smt.simplificationModeWasSetByUser) { @@ -507,7 +505,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.simplificationMode = options::SimplificationMode::NONE; } - if (options::learnedRewrite()) + if (opts.smt.learnedRewrite) { if (opts.smt.learnedRewriteWasSetByUser) { @@ -519,7 +517,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.learnedRewrite = false; } - if (options::pbRewrites()) + if (opts.arith.pbRewrites) { if (opts.arith.pbRewritesWasSetByUser) { @@ -531,7 +529,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.arith.pbRewrites = false; } - if (options::sortInference()) + if (opts.smt.sortInference) { if (opts.smt.sortInferenceWasSetByUser) { @@ -542,7 +540,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.sortInference = false; } - if (options::preSkolemQuant()) + if (opts.quantifiers.preSkolemQuant) { if (opts.quantifiers.preSkolemQuantWasSetByUser) { @@ -554,7 +552,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.preSkolemQuant = false; } - if (options::bitvectorToBool()) + if (opts.bv.bitvectorToBool) { if (opts.bv.bitvectorToBoolWasSetByUser) { @@ -565,7 +563,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.bitvectorToBool = false; } - if (options::boolToBitvector() != options::BoolToBVMode::OFF) + if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) { if (opts.bv.boolToBitvectorWasSetByUser) { @@ -576,7 +574,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.boolToBitvector = options::BoolToBVMode::OFF; } - if (options::bvIntroducePow2()) + if (opts.bv.bvIntroducePow2) { if (opts.bv.bvIntroducePow2WasSetByUser) { @@ -586,7 +584,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.bv.bvIntroducePow2 = false; } - if (options::repeatSimp()) + if (opts.smt.repeatSimp) { if (opts.smt.repeatSimpWasSetByUser) { @@ -596,7 +594,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.repeatSimp = false; } - if (options::globalNegate()) + if (opts.quantifiers.globalNegate) { if (opts.quantifiers.globalNegateWasSetByUser) { @@ -607,12 +605,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.globalNegate = false; } - if (options::bitvectorAig()) + if (opts.bv.bitvectorAig) { throw OptionException("bitblast-aig not supported with unsat cores"); } - if (options::doITESimp()) + if (opts.smt.doITESimp) { throw OptionException("ITE simp not supported with unsat cores"); } @@ -635,9 +633,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::cegqiBv() && logic.isQuantified()) + if (opts.quantifiers.cegqiBv && logic.isQuantified()) { - if (options::boolToBitvector() != options::BoolToBVMode::OFF) + if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF) { if (opts.bv.boolToBitvectorWasSetByUser) { @@ -652,8 +650,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // cases where we need produce models - if (!options::produceModels() - && (options::produceAssignments() || options::sygusRewSynthCheck() + if (!opts.smt.produceModels + && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck || usesSygus)) { Notice() << "SmtEngine: turning on produce-models" << std::endl; @@ -691,13 +689,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic = log; logic.lock(); } - if (options::bvAbstraction()) + if (opts.bv.bvAbstraction) { // bv abstraction may require UF Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; needsUf = true; } - else if (options::preSkolemQuantNested() + else if (opts.quantifiers.preSkolemQuantNested && opts.quantifiers.preSkolemQuantNestedWasSetByUser) { // if pre-skolem nested is explictly set, then we require UF. If it is @@ -718,7 +716,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // then this is not required, since non-linear arithmetic will be // eliminated altogether (or otherwise fail at preprocessing). || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && options::solveIntAsBV() == 0) + && opts.smt.solveIntAsBV == 0) // FP requires UF since there are multiple operators that are partially // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more // details). @@ -737,7 +735,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } } - if (options::arithMLTrick()) + if (opts.arith.arithMLTrick) { if (!logic.areIntegersUsed()) { @@ -771,7 +769,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (!opts.uf.ufSymmetryBreakerWasSetByUser) { bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified() - && !options::incrementalSolving() && !safeUnsatCores; + && !opts.base.incrementalSolving && !safeUnsatCores; Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << std::endl; opts.uf.ufSymmetryBreaker = qf_uf_noinc; @@ -779,7 +777,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // If in arrays, set the UF handler to arrays if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder() - && !options::finiteModelFind() + && !opts.quantifiers.finiteModelFind && (!logic.isQuantified() || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF)))) { @@ -826,7 +824,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.smt.repeatSimp = repeatSimp; } - if (options::boolToBitvector() == options::BoolToBVMode::ALL + if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL && !logic.isTheoryEnabled(THEORY_BV)) { if (opts.bv.boolToBitvectorWasSetByUser) @@ -999,7 +997,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { // disable modes not supported by incremental opts.smt.sortInference = false; @@ -1014,15 +1012,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.finiteModelFind = true; } - if (options::instMaxLevel() != -1) + if (opts.quantifiers.instMaxLevel != -1) { Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << std::endl; opts.quantifiers.cegqi = false; } - if ((opts.quantifiers.fmfBoundLazyWasSetByUser && options::fmfBoundLazy()) - || (opts.quantifiers.fmfBoundIntWasSetByUser && options::fmfBoundInt())) + if ((opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy) + || (opts.quantifiers.fmfBoundIntWasSetByUser && opts.quantifiers.fmfBoundInt)) { opts.quantifiers.fmfBound = true; Trace("smt") @@ -1030,11 +1028,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // now have determined whether fmfBound is on/off // apply fmfBound options - if (options::fmfBound()) + if (opts.quantifiers.fmfBound) { if (!opts.quantifiers.mbqiModeWasSetByUser - || (options::mbqiMode() != options::MbqiMode::NONE - && options::mbqiMode() != options::MbqiMode::FMC)) + || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE + && opts.quantifiers.mbqiMode != options::MbqiMode::FMC)) { // if bounded integers are set, use no MBQI by default opts.quantifiers.mbqiMode = options::MbqiMode::NONE; @@ -1049,28 +1047,28 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.uf.ufHo = true; // if higher-order, then current variants of model-based instantiation // cannot be used - if (options::mbqiMode() != options::MbqiMode::NONE) + if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE) { opts.quantifiers.mbqiMode = options::MbqiMode::NONE; } if (!opts.quantifiers.hoElimStoreAxWasSetByUser) { // by default, use store axioms only if --ho-elim is set - opts.quantifiers.hoElimStoreAx = options::hoElim(); + opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim; } - if (!options::assignFunctionValues()) + if (!opts.theory.assignFunctionValues) { // must assign function values opts.theory.assignFunctionValues = true; } // Cannot use macros, since lambda lifting and macro elimination are inverse // operations. - if (options::macrosQuant()) + if (opts.quantifiers.macrosQuant) { opts.quantifiers.macrosQuant = false; } // HOL is incompatible with fmfBound - if (options::fmfBound()) + if (opts.quantifiers.fmfBound) { if (opts.quantifiers.fmfBoundWasSetByUser || opts.quantifiers.fmfBoundLazyWasSetByUser @@ -1084,14 +1082,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "turning off fmf-bound, since HOL\n"; } } - if (options::fmfFunWellDefinedRelevant()) + if (opts.quantifiers.fmfFunWellDefinedRelevant) { if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser) { opts.quantifiers.fmfFunWellDefined = true; } } - if (options::fmfFunWellDefined()) + if (opts.quantifiers.fmfFunWellDefined) { if (!opts.quantifiers.finiteModelFindWasSetByUser) { @@ -1101,7 +1099,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // now, have determined whether finite model find is on/off // apply finite model finding options - if (options::finiteModelFind()) + if (opts.quantifiers.finiteModelFind) { // apply conservative quantifiers splitting if (!opts.quantifiers.quantDynamicSplitWasSetByUser) @@ -1110,12 +1108,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (!opts.quantifiers.eMatchingWasSetByUser) { - opts.quantifiers.eMatching = options::fmfInstEngine(); + opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine; } if (!opts.quantifiers.instWhenModeWasSetByUser) { // instantiate only on last call - if (options::eMatching()) + if (opts.quantifiers.eMatching) { opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; } @@ -1126,7 +1124,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // if we are attempting to rewrite everything to SyGuS, use sygus() if (usesSygus) { - if (!options::sygus()) + if (!opts.quantifiers.sygus) { Trace("smt") << "turning on sygus" << std::endl; } @@ -1142,14 +1140,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { opts.quantifiers.cegqiBv = false; } - if (options::sygusRepairConst()) + if (opts.quantifiers.sygusRepairConst) { if (!opts.quantifiers.cegqiWasSetByUser) { opts.quantifiers.cegqi = true; } } - if (options::sygusInference()) + if (opts.quantifiers.sygusInference) { // optimization: apply preskolemization, makes it succeed more often if (!opts.quantifiers.preSkolemQuantWasSetByUser) @@ -1179,12 +1177,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // should use full effort cbqi for single invocation and repair const opts.quantifiers.cegqiFullEffort = true; } - if (options::sygusRew()) + if (opts.quantifiers.sygusRew) { opts.quantifiers.sygusRewSynth = true; opts.quantifiers.sygusRewVerify = true; } - if (options::sygusRewSynthInput()) + if (opts.quantifiers.sygusRewSynthInput) { // If we are using synthesis rewrite rules from input, we use // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for @@ -1203,7 +1201,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // template inference for invariant synthesis, and single invocation // techniques. bool reqBasicSygus = false; - if (options::produceAbducts()) + if (opts.smt.produceAbducts) { // if doing abduction, we should filter strong solutions if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) @@ -1214,13 +1212,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // a sygus side condition for consistency with axioms. reqBasicSygus = true; } - if (options::sygusRewSynth() || options::sygusRewVerify() - || options::sygusQueryGen()) + if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify + || opts.quantifiers.sygusQueryGen) { // rewrite rule synthesis implies that sygus stream must be true opts.quantifiers.sygusStream = true; } - if (options::sygusStream() || options::incrementalSolving()) + if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) { // Streaming and incremental mode are incompatible with techniques that // focus the search towards finding a single solution. @@ -1282,7 +1280,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || logic.isTheoryEnabled(THEORY_DATATYPES) || logic.isTheoryEnabled(THEORY_BV) || logic.isTheoryEnabled(THEORY_FP))) - || options::cegqiAll()) + || opts.quantifiers.cegqiAll) { if (!opts.quantifiers.cegqiWasSetByUser) { @@ -1297,9 +1295,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } } - if (options::cegqi()) + if (opts.quantifiers.cegqi) { - if (options::incrementalSolving()) + if (opts.base.incrementalSolving) { // cannot do nested quantifier elimination in incremental mode opts.quantifiers.cegqiNestedQE = false; @@ -1314,7 +1312,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { opts.quantifiers.instNoEntail = false; } - if (!opts.quantifiers.instWhenModeWasSetByUser && options::cegqiModel()) + if (!opts.quantifiers.instWhenModeWasSetByUser && opts.quantifiers.cegqiModel) { // only instantiation should happen at last call when model is avaiable opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL; @@ -1325,7 +1323,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // only supported in pure arithmetic or pure BV opts.quantifiers.cegqiNestedQE = false; } - if (options::globalNegate()) + if (opts.quantifiers.globalNegate) { if (!opts.quantifiers.prenexQuantWasSetByUser) { @@ -1334,18 +1332,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // implied options... - if (options::strictTriggers()) + if (opts.quantifiers.strictTriggers) { if (!opts.quantifiers.userPatternsQuantWasSetByUser) { opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST; } } - if (opts.quantifiers.qcfModeWasSetByUser || options::qcfTConstraint()) + if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint) { opts.quantifiers.quantConflictFind = true; } - if (options::cegqiNestedQE()) + if (opts.quantifiers.cegqiNestedQE) { opts.quantifiers.prenexQuantUser = true; if (!opts.quantifiers.preSkolemQuantWasSetByUser) @@ -1354,7 +1352,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // for induction techniques - if (options::quantInduction()) + if (opts.quantifiers.quantInduction) { if (!opts.quantifiers.dtStcInductionWasSetByUser) { @@ -1365,7 +1363,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.intWfInduction = true; } } - if (options::dtStcInduction()) + if (opts.quantifiers.dtStcInduction) { // try to remove ITEs from quantified formulas if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser) @@ -1377,14 +1375,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL; } } - if (options::intWfInduction()) + if (opts.quantifiers.intWfInduction) { if (!opts.quantifiers.purifyTriggersWasSetByUser) { opts.quantifiers.purifyTriggers = true; } } - if (options::conjectureNoFilter()) + if (opts.quantifiers.conjectureNoFilter) { if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser) { @@ -1401,7 +1399,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (opts.quantifiers.conjectureGenPerRoundWasSetByUser) { - if (options::conjectureGenPerRound() > 0) + if (opts.quantifiers.conjectureGenPerRound > 0) { opts.quantifiers.conjectureGen = true; } @@ -1411,7 +1409,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } // can't pre-skolemize nested quantifiers without UF theory - if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant()) + if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant) { if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) { @@ -1430,11 +1428,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // introduces new literals into the search. This includes quantifiers // (quantifier instantiation), and the lemma schemas used in non-linear // and sets. We also can't use it if models are enabled. - if (logic.isTheoryEnabled(THEORY_SETS) - || logic.isTheoryEnabled(THEORY_BAGS) - || logic.isQuantified() - || options::produceModels() || options::produceAssignments() - || options::checkModels() + if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS) + || logic.isQuantified() || opts.smt.produceModels + || opts.smt.produceAssignments || opts.smt.checkModels || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear())) { opts.prop.minisatUseElim = false; @@ -1442,15 +1438,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && options::nlRlvMode() != options::NlRlvMode::NONE) + && opts.arith.nlRlvMode != options::NlRlvMode::NONE) { - if (!options::relevanceFilter()) + if (!opts.theory.relevanceFilter) { if (opts.theory.relevanceFilterWasSetByUser) { Warning() << "SmtEngine: turning on relevance filtering to support " "--nl-ext-rlv=" - << options::nlRlvMode() << std::endl; + << opts.arith.nlRlvMode << std::endl; } // must use relevance filtering techniques opts.theory.relevanceFilter = true; @@ -1458,13 +1454,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // For now, these array theory optimizations do not support model-building - if (options::produceModels() || options::produceAssignments() - || options::checkModels()) + if (opts.smt.produceModels || opts.smt.produceAssignments + || opts.smt.checkModels) { opts.arrays.arraysOptimizeLinear = false; } - if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser) + if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " "--strings-fmf enabled" @@ -1475,29 +1471,29 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // !!! All options that require disabling models go here bool disableModels = false; std::string sOptNoModel; - if (opts.smt.unconstrainedSimpWasSetByUser && options::unconstrainedSimp()) + if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp) { disableModels = true; sOptNoModel = "unconstrained-simp"; } - else if (options::sortInference()) + else if (opts.smt.sortInference) { disableModels = true; sOptNoModel = "sort-inference"; } - else if (options::minisatUseElim()) + else if (opts.prop.minisatUseElim) { disableModels = true; sOptNoModel = "minisat-elimination"; } - else if (options::globalNegate()) + else if (opts.quantifiers.globalNegate) { disableModels = true; sOptNoModel = "global-negate"; } if (disableModels) { - if (options::produceModels()) + if (opts.smt.produceModels) { if (opts.smt.produceModelsWasSetByUser) { @@ -1509,7 +1505,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << sOptNoModel << std::endl; opts.smt.produceModels = false; } - if (options::produceAssignments()) + if (opts.smt.produceAssignments) { if (opts.smt.produceAssignmentsWasSetByUser) { @@ -1522,7 +1518,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) << sOptNoModel << std::endl; opts.smt.produceAssignments = false; } - if (options::checkModels()) + if (opts.smt.checkModels) { if (opts.smt.checkModelsWasSetByUser) { @@ -1537,7 +1533,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - if (options::bitblastMode() == options::BitblastMode::EAGER + if (opts.bv.bitblastMode == options::BitblastMode::EAGER && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV" && logic.getLogicString() != "QF_ABV") { @@ -1551,7 +1547,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (logic == LogicInfo("QF_UFNRA")) { #ifdef CVC5_USE_POLY - if (!options::nlCad() && !opts.arith.nlCadWasSetByUser) + if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) { opts.arith.nlCad = true; if (!opts.arith.nlExtWasSetByUser) @@ -1566,7 +1562,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) #endif } #ifndef CVC5_USE_POLY - if (options::nlCad()) + if (opts.arith.nlCad) { if (opts.arith.nlCadWasSetByUser) { diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 6e77b488c..22e271c72 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -16,6 +16,7 @@ #ifndef CVC5__SMT__SET_DEFAULTS_H #define CVC5__SMT__SET_DEFAULTS_H +#include "options/options.h" #include "theory/logic_info.h" namespace cvc5 { @@ -34,7 +35,7 @@ namespace smt { * can be further refactored to modify an options object provided as an * explicit argument. */ -void setDefaults(LogicInfo& logic, bool isInternalSubsolver); +void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver); } // namespace smt } // namespace cvc5 -- cgit v1.2.3 From bb0b36445b37c5b7fd22f4b12e590ade4646589e Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Mon, 16 Aug 2021 04:24:25 +0100 Subject: Correct copyright print for GLPK (#7015) In `master`, starting `cvc5` interactively will give you: ``` glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit See http://github.com/timothy-king/glpk-cut-log for copyrightinformation ``` Notice: there's a double-space after the dash following the library name, and there's no space between "copyrightinformation". This commit corrects this print such that it gives: ``` glpk-cut-log - a modified version of GPLK, the GNU Linear Programming Kit See http://github.com/timothy-king/glpk-cut-log for copyright information ``` Signed-off-by: Andrew V. Jones --- src/base/configuration.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index c6b004574..a370a0c47 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -195,10 +195,10 @@ std::string Configuration::copyright() { << " See http://www.ginac.de/CLN for copyright information.\n\n"; } if (Configuration::isBuiltWithGlpk()) { - ss << " glpk-cut-log - a modified version of GPLK, " + ss << " glpk-cut-log - a modified version of GPLK, " << "the GNU Linear Programming Kit\n" << " See http://github.com/timothy-king/glpk-cut-log for copyright" - << "information\n\n"; + << " information\n\n"; } } -- cgit v1.2.3 From 0711ec521f01888b059d152d1c1f20382d5ce432 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 16 Aug 2021 06:58:43 -0700 Subject: [Strings] Make fact detection more robust (#7007) Currently, our check for whether an inference is a fact or a lemma involves checking whether the kind of the conclusion is a conjunction or a disjunction. However, this does not take into account inferences of other kinds such as ites, which is a problem because they require a decision from the SAT solver. This commit changes the condition to check the theory of the conclusion. If the conclusion belongs to the theory of strings, it considers it as a fact. --- src/theory/strings/infer_info.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 432aa39d0..aabefe74e 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -17,6 +17,7 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/theory.h" namespace cvc5 { namespace theory { @@ -60,8 +61,8 @@ bool InferInfo::isFact() const // we could process inferences with conjunctive conclusions as facts, where // the explanation is copied. However, for simplicity, we always send these // as lemmas. This case happens very infrequently. - return !atom.isConst() && atom.getKind() != kind::OR - && atom.getKind() != kind::AND && d_noExplain.empty(); + return !atom.isConst() && Theory::theoryOf(atom) == THEORY_STRINGS + && d_noExplain.empty(); } Node InferInfo::getPremises() const -- cgit v1.2.3 From 5e31ee3a34388d6d44129e898897bdb1297009de Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 16 Aug 2021 07:20:22 -0700 Subject: Make Theory class use Env (#7011) This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager. --- src/smt/env.cpp | 9 ++++ src/smt/env.h | 8 ++++ src/smt/smt_solver.cpp | 10 +---- src/theory/arith/theory_arith.cpp | 24 +++++------ src/theory/arith/theory_arith.h | 7 +-- src/theory/arrays/theory_arrays.cpp | 61 +++++++++++++-------------- src/theory/arrays/theory_arrays.h | 5 +-- src/theory/bags/theory_bags.cpp | 13 ++---- src/theory/bags/theory_bags.h | 7 +-- src/theory/booleans/theory_bool.cpp | 9 +--- src/theory/booleans/theory_bool.h | 7 +-- src/theory/builtin/theory_builtin.cpp | 13 ++---- src/theory/builtin/theory_builtin.h | 7 +-- src/theory/bv/theory_bv.cpp | 18 ++++---- src/theory/bv/theory_bv.h | 5 +-- src/theory/datatypes/theory_datatypes.cpp | 29 ++++++------- src/theory/datatypes/theory_datatypes.h | 7 +-- src/theory/fp/theory_fp.cpp | 27 +++++------- src/theory/fp/theory_fp.h | 7 +-- src/theory/quantifiers/theory_quantifiers.cpp | 16 +++---- src/theory/quantifiers/theory_quantifiers.h | 7 +-- src/theory/sep/theory_sep.cpp | 19 +++------ src/theory/sep/theory_sep.h | 7 +-- src/theory/sets/theory_sets.cpp | 15 +++---- src/theory/sets/theory_sets.h | 7 +-- src/theory/strings/theory_strings.cpp | 21 ++++----- src/theory/strings/theory_strings.h | 7 +-- src/theory/theory.cpp | 33 +++++++-------- src/theory/theory.h | 33 ++++++--------- src/theory/theory_engine.cpp | 6 +-- src/theory/theory_engine.h | 10 ++--- src/theory/uf/theory_uf.cpp | 15 +++---- src/theory/uf/theory_uf.h | 5 +-- test/unit/test_smt.h | 11 ++--- test/unit/theory/theory_white.cpp | 15 +------ 35 files changed, 185 insertions(+), 315 deletions(-) (limited to 'src') diff --git a/src/smt/env.cpp b/src/smt/env.cpp index b6cdfb67b..a4e07d2c9 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -19,6 +19,7 @@ #include "context/context.h" #include "expr/node.h" #include "options/base_options.h" +#include "options/smt_options.h" #include "printer/printer.h" #include "proof/conv_proof_generator.h" #include "smt/dump_manager.h" @@ -80,6 +81,14 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; } ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } +bool Env::isTheoryProofProducing() const +{ + return d_proofNodeManager != nullptr + && (!d_options.smt.unsatCores + || d_options.smt.unsatCoresMode + == options::UnsatCoresMode::FULL_PROOF); +} + theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); } theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions() diff --git a/src/smt/env.h b/src/smt/env.h index 57b5ad9c7..fa2fe6ab8 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -82,6 +82,14 @@ class Env */ ProofNodeManager* getProofNodeManager(); + /** + * Check whether theories should produce proofs as well. Other than whether + * the proof node manager is set, theory engine proofs are conditioned on the + * relationship between proofs and unsat cores: the unsat cores are in + * FULL_PROOF mode, no proofs are generated on theory engine. + */ + bool isTheoryProofProducing() const; + /** Get a pointer to the Rewriter owned by this Env. */ theory::Rewriter* getRewriter(); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 503d9d1db..595a3808c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -52,15 +52,7 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) { // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine.reset(new TheoryEngine( - d_env, - // Other than whether d_pm is set, theory engine proofs are conditioned on - // the relationshup between proofs and unsat cores: the unsat cores are in - // FULL_PROOF mode, no proofs are generated on theory engine. - (options::unsatCores() - && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF) - ? nullptr - : d_pnm)); + d_theoryEngine.reset(new TheoryEngine(d_env)); // Add the theories for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 2c7187089..8cb607dd7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -35,24 +35,20 @@ namespace cvc5 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm), +TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_ARITH, env, out, valuation), d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( "theory::arith::ppRewriteTimer")), - d_astate(c, u, valuation), - d_im(*this, d_astate, pnm), - d_ppre(c, pnm), - d_bab(d_astate, d_im, d_ppre, pnm), + d_astate(getSatContext(), getUserContext(), valuation), + d_im(*this, d_astate, d_pnm), + d_ppre(getSatContext(), d_pnm), + d_bab(d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), - d_internal(new TheoryArithPrivate(*this, c, u, d_bab, pnm)), + d_internal(new TheoryArithPrivate( + *this, getSatContext(), getUserContext(), d_bab, d_pnm)), d_nonlinearExtension(nullptr), - d_opElim(pnm, logicInfo), - d_arithPreproc(d_astate, d_im, pnm, d_opElim), + d_opElim(d_pnm, getLogicInfo()), + d_arithPreproc(d_astate, d_im, d_pnm, d_opElim), d_rewriter(d_opElim) { // currently a cyclic dependency to TheoryArithPrivate diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ee99f44e8..4b0c88fd2 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -44,12 +44,7 @@ class TheoryArithPrivate; class TheoryArith : public Theory { friend class TheoryArithPrivate; public: - TheoryArith(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryArith(Env& env, OutputChannel& out, Valuation valuation); virtual ~TheoryArith(); //--------------------------------- initialization diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6c9c162ab..eaa9c9294 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -55,14 +55,11 @@ const bool d_solveWrite2 = false; //bool d_useNonLinearOpt = true; //bool d_eagerIndexSplitting = false; -TheoryArrays::TheoryArrays(context::Context* c, - context::UserContext* u, +TheoryArrays::TheoryArrays(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string name) - : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name), + : Theory(THEORY_ARRAYS, env, out, valuation, name), d_numRow( smtStatisticsRegistry().registerInt(name + "number of Row lemmas")), d_numExt( @@ -83,37 +80,37 @@ TheoryArrays::TheoryArrays(context::Context* c, name + "number of setModelVal splits")), d_numSetModelValConflicts(smtStatisticsRegistry().registerInt( name + "number of setModelVal conflicts")), - d_ppEqualityEngine(u, name + "pp", true), - d_ppFacts(u), - d_rewriter(pnm), - d_state(c, u, valuation), - d_im(*this, d_state, pnm), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, name + "mayEqual", true), + d_ppEqualityEngine(getUserContext(), name + "pp", true), + d_ppFacts(getUserContext()), + d_rewriter(d_pnm), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm), + d_literalsToPropagate(getSatContext()), + d_literalsToPropagateIndex(getSatContext(), 0), + d_isPreRegistered(getSatContext()), + d_mayEqualEqualityEngine(getSatContext(), name + "mayEqual", true), d_notify(*this), - d_backtracker(c), - d_infoMap(c, &d_backtracker, name), - d_mergeQueue(c), + d_backtracker(getSatContext()), + d_infoMap(getSatContext(), &d_backtracker, name), + d_mergeQueue(getSatContext()), d_mergeInProgress(false), - d_RowQueue(c), - d_RowAlreadyAdded(u), - d_sharedArrays(c), - d_sharedOther(c), - d_sharedTerms(c, false), - d_reads(c), - d_constReadsList(c), + d_RowQueue(getSatContext()), + d_RowAlreadyAdded(getUserContext()), + d_sharedArrays(getSatContext()), + d_sharedOther(getSatContext()), + d_sharedTerms(getSatContext(), false), + d_reads(getSatContext()), + d_constReadsList(getSatContext()), d_constReadsContext(new context::Context()), - d_contextPopper(c, d_constReadsContext), - d_skolemIndex(c, 0), - d_decisionRequests(c), - d_permRef(c), - d_modelConstraints(c), - d_lemmasSaved(c), - d_defValues(c), + d_contextPopper(getSatContext(), d_constReadsContext), + d_skolemIndex(getSatContext(), 0), + d_decisionRequests(getSatContext()), + d_permRef(getSatContext()), + d_modelConstraints(getSatContext()), + d_lemmasSaved(getSatContext()), + d_defValues(getSatContext()), d_readTableContext(new context::Context()), - d_arrayMerges(c), + d_arrayMerges(getSatContext()), d_inCheckModel(false), d_dstrat(new TheoryArraysDecisionStrategy(this)), d_dstratInit(false) diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 772fc1b79..d255e44f1 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -132,12 +132,9 @@ class TheoryArrays : public Theory { IntStat d_numSetModelValConflicts; public: - TheoryArrays(context::Context* c, - context::UserContext* u, + TheoryArrays(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr, std::string name = "theory::arrays::"); ~TheoryArrays(); diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 580d26c08..42a1e2c6b 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -27,15 +27,10 @@ namespace cvc5 { namespace theory { namespace bags { -TheoryBags::TheoryBags(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm), - d_state(c, u, valuation), - d_im(*this, d_state, pnm), +TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BAGS, env, out, valuation), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm), d_ig(&d_state, &d_im), d_notify(*this, d_im), d_statistics(), diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 4ed131e64..671623d05 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -36,12 +36,7 @@ class TheoryBags : public Theory { public: /** Constructs a new instance of TheoryBags w.r.t. the provided contexts. */ - TheoryBags(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm); + TheoryBags(Env& env, OutputChannel& out, Valuation valuation); ~TheoryBags() override; //--------------------------------- initialization diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 3aac5ecfb..33bb820b4 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -32,13 +32,8 @@ namespace cvc5 { namespace theory { namespace booleans { -TheoryBool::TheoryBool(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm) +TheoryBool::TheoryBool(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BOOL, env, out, valuation) { } diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index dd574a455..e0b7e6511 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -29,12 +29,7 @@ namespace booleans { class TheoryBool : public Theory { public: - TheoryBool(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryBool(Env& env, OutputChannel& out, Valuation valuation); /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 1db03d22b..f12d2caf9 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -25,15 +25,10 @@ namespace cvc5 { namespace theory { namespace builtin { -TheoryBuiltin::TheoryBuiltin(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::builtin::") +TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BUILTIN, env, out, valuation), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::builtin::") { // indicate we are using the default theory state and inference managers d_theoryState = &d_state; diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 72485f0ea..29a3cfb36 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -31,12 +31,7 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation); /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 547d24b23..1976177b7 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -30,35 +30,33 @@ namespace cvc5 { namespace theory { namespace bv { -TheoryBV::TheoryBV(context::Context* c, - context::UserContext* u, +TheoryBV::TheoryBV(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string name) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name), + : Theory(THEORY_BV, env, out, valuation, name), d_internal(nullptr), d_rewriter(), - d_state(c, u, valuation), + d_state(getSatContext(), getUserContext(), valuation), d_im(*this, d_state, nullptr, "theory::bv::"), d_notify(d_im), - d_invalidateModelCache(c, true), + d_invalidateModelCache(getSatContext(), true), d_stats("theory::bv::") { switch (options::bvSolver()) { case options::BVSolver::BITBLAST: - d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm)); + d_internal.reset(new BVSolverBitblast(&d_state, d_im, d_pnm)); break; case options::BVSolver::LAYERED: - d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name)); + d_internal.reset(new BVSolverLayered( + *this, getSatContext(), getUserContext(), d_pnm, name)); break; default: AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL); - d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm)); + d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, d_pnm)); } d_theoryState = &d_state; d_inferManager = &d_im; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index da44d7022..b4afb5f5d 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -39,12 +39,9 @@ class TheoryBV : public Theory friend class BVSolverLayered; public: - TheoryBV(context::Context* c, - context::UserContext* u, + TheoryBV(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr, std::string name = ""); ~TheoryBV(); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 50c955d48..759cc4c87 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -47,24 +47,21 @@ namespace cvc5 { namespace theory { namespace datatypes { -TheoryDatatypes::TheoryDatatypes(Context* c, - UserContext* u, +TheoryDatatypes::TheoryDatatypes(Env& env, OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm), - d_term_sk(u), - d_labels(c), - d_selector_apps(c), - d_collectTermsCache(c), - d_collectTermsCacheU(u), - d_functionTerms(c), - d_singleton_eq(u), - d_lemmas_produced_c(u), + Valuation valuation) + : Theory(THEORY_DATATYPES, env, out, valuation), + d_term_sk(getUserContext()), + d_labels(getSatContext()), + d_selector_apps(getSatContext()), + d_collectTermsCache(getSatContext()), + d_collectTermsCacheU(getUserContext()), + d_functionTerms(getSatContext()), + d_singleton_eq(getUserContext()), + d_lemmas_produced_c(getUserContext()), d_sygusExtension(nullptr), - d_state(c, u, valuation), - d_im(*this, d_state, pnm), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm), d_notify(d_im, *this) { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 951aea804..ecfa6f02a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -183,12 +183,7 @@ private: void computeCareGraph() override; public: - TheoryDatatypes(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryDatatypes(Env& env, OutputChannel& out, Valuation valuation); ~TheoryDatatypes(); //--------------------------------- initialization diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 9b5ac66d3..a016c7897 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -60,24 +60,19 @@ Node buildConjunct(const std::vector &assumptions) { } // namespace helper /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ -TheoryFp::TheoryFp(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm), +TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_FP, env, out, valuation), d_notification(*this), - d_registeredTerms(u), - d_conv(new FpConverter(u)), + d_registeredTerms(getUserContext()), + d_conv(new FpConverter(getUserContext())), d_expansionRequested(false), - d_realToFloatMap(u), - d_floatToRealMap(u), - d_abstractionMap(u), - d_rewriter(u), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::fp::", false), - d_wbFactsCache(u) + d_realToFloatMap(getUserContext()), + d_floatToRealMap(getUserContext()), + d_abstractionMap(getUserContext()), + d_rewriter(getUserContext()), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::fp::", false), + d_wbFactsCache(getUserContext()) { // indicate we are using the default theory state and inference manager d_theoryState = &d_state; diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 14779cc3d..1e1041980 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -39,12 +39,7 @@ class TheoryFp : public Theory { public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ - TheoryFp(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryFp(Env& env, OutputChannel& out, Valuation valuation); //--------------------------------- initialization /** Get the official theory rewriter of this theory. */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index c74146c9c..3adf53b57 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -30,17 +30,14 @@ namespace cvc5 { namespace theory { namespace quantifiers { -TheoryQuantifiers::TheoryQuantifiers(Context* c, - context::UserContext* u, +TheoryQuantifiers::TheoryQuantifiers(Env& env, OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), - d_qstate(c, u, valuation, logicInfo), + Valuation valuation) + : Theory(THEORY_QUANTIFIERS, env, out, valuation), + d_qstate(getSatContext(), getUserContext(), valuation, getLogicInfo()), d_qreg(), d_treg(d_qstate, d_qreg), - d_qim(*this, d_qstate, d_qreg, d_treg, pnm), + d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm), d_qengine(nullptr) { out.handleUserAttribute( "fun-def", this ); @@ -50,7 +47,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, out.handleUserAttribute( "quant-elim-partial", this ); // construct the quantifiers engine - d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm)); + d_qengine.reset( + new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, d_pnm)); // indicate we are using the quantifiers theory state object d_theoryState = &d_qstate; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 544be84d6..0ef5cfcbb 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -37,12 +37,7 @@ class QuantifiersMacros; class TheoryQuantifiers : public Theory { public: - TheoryQuantifiers(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheoryQuantifiers(Env& env, OutputChannel& out, Valuation valuation); ~TheoryQuantifiers(); //--------------------------------- initialization diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 98130beb5..0b16ddd27 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -42,20 +42,15 @@ namespace cvc5 { namespace theory { namespace sep { -TheorySep::TheorySep(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm), - d_lemmas_produced_c(u), +TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_SEP, env, out, valuation), + d_lemmas_produced_c(getUserContext()), d_bounds_init(false), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::sep::"), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::sep::"), d_notify(*this), - d_reduce(u), - d_spatial_assertions(c) + d_reduce(getUserContext()), + d_spatial_assertions(getSatContext()) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index b028f0686..985513fd8 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -77,12 +77,7 @@ class TheorySep : public Theory { bool underSpatial); public: - TheorySep(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr); + TheorySep(Env& env, OutputChannel& out, Valuation valuation); ~TheorySep(); /** diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 718077888..5ea13ea4d 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -27,17 +27,12 @@ namespace cvc5 { namespace theory { namespace sets { -TheorySets::TheorySets(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm), +TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_SETS, env, out, valuation), d_skCache(), - d_state(c, u, valuation, d_skCache), - d_im(*this, d_state, pnm), - d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)), + d_state(getSatContext(), getUserContext(), valuation, d_skCache), + d_im(*this, d_state, d_pnm), + d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, d_pnm)), d_notify(*d_internal.get(), d_im) { // use the official theory state and inference manager objects diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index e99d25d36..e9510d70e 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -41,12 +41,7 @@ class TheorySets : public Theory friend class TheorySetsRels; public: /** Constructs a new instance of TheorySets w.r.t. the provided contexts. */ - TheorySets(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm); + TheorySets(Env& env, OutputChannel& out, Valuation valuation); ~TheorySets() override; //--------------------------------- initialization diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c526decf1..319a6698b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -50,21 +50,16 @@ struct SeqModelVarAttributeId }; using SeqModelVarAttribute = expr::Attribute; -TheoryStrings::TheoryStrings(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm), +TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) + : Theory(THEORY_STRINGS, env, out, valuation), d_notify(*this), d_statistics(), - d_state(c, u, d_valuation), + d_state(getSatContext(), getUserContext(), d_valuation), d_eagerSolver(d_state), - d_termReg(d_state, d_statistics, pnm), + d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_extTheory(d_extTheoryCb, c, u, out), - d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm), + d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), out), + d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), @@ -82,8 +77,8 @@ TheoryStrings::TheoryStrings(context::Context* c, d_csolver, d_esolver, d_statistics), - d_regexp_elim(options::regExpElimAgg(), pnm, u), - d_stringsFmf(c, u, valuation, d_termReg) + d_regexp_elim(options::regExpElimAgg(), d_pnm, getUserContext()), + d_stringsFmf(getSatContext(), getUserContext(), valuation, d_termReg) { d_termReg.finishInit(&d_im); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fc5e47194..c1ce71cef 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -64,12 +64,7 @@ class TheoryStrings : public Theory { typedef context::CDHashSet> TypeNodeSet; public: - TheoryStrings(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm); + TheoryStrings(Env& env, OutputChannel& out, Valuation valuation); ~TheoryStrings(); //--------------------------------- initialization /** get the official theory rewriter of this theory */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 96bc85336..b774d456a 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -60,27 +60,22 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ }/* ostream& operator<<(ostream&, Theory::Effort) */ Theory::Theory(TheoryId id, - context::Context* satContext, - context::UserContext* userContext, + Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string name) : d_id(id), - d_satContext(satContext), - d_userContext(userContext), - d_logicInfo(logicInfo), - d_facts(satContext), - d_factsHead(satContext, 0), - d_sharedTermsIndex(satContext, 0), + d_env(env), + d_facts(d_env.getContext()), + d_factsHead(d_env.getContext(), 0), + d_sharedTermsIndex(d_env.getContext(), 0), d_careGraph(nullptr), d_instanceName(name), d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id) + name + "checkTime")), d_computeCareGraphTime(smtStatisticsRegistry().registerTimer( getStatsPrefix(id) + name + "computeCareGraphTime")), - d_sharedTerms(satContext), + d_sharedTerms(d_env.getContext()), d_out(&out), d_valuation(valuation), d_equalityEngine(nullptr), @@ -88,7 +83,8 @@ Theory::Theory(TheoryId id, d_theoryState(nullptr), d_inferManager(nullptr), d_quantEngine(nullptr), - d_pnm(pnm) + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr) { } @@ -135,9 +131,12 @@ void Theory::finishInitStandalone() EeSetupInfo esi; if (needsEqualityEngine(esi)) { - // always associated with the same SAT context as the theory (d_satContext) - d_allocEqualityEngine.reset(new eq::EqualityEngine( - *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers)); + // always associated with the same SAT context as the theory + d_allocEqualityEngine.reset( + new eq::EqualityEngine(*esi.d_notify, + getSatContext(), + esi.d_name, + esi.d_constantsAreTriggers)); // use it as the official equality engine setEqualityEngine(d_allocEqualityEngine.get()); } @@ -339,7 +338,7 @@ bool Theory::isLegalElimination(TNode x, TNode val) { return false; } - if (!options::produceModels() && !d_logicInfo.isQuantified()) + if (!options::produceModels() && !getLogicInfo().isQuantified()) { // Don't care about the model and logic is not quantified, we can eliminate. return true; @@ -467,7 +466,7 @@ void Theory::getCareGraph(CareGraph* careGraph) { bool Theory::proofsEnabled() const { - return d_pnm != nullptr; + return d_env.getProofNodeManager() != nullptr; } EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) diff --git a/src/theory/theory.h b/src/theory/theory.h index 41f35601b..a857931a8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -29,6 +29,7 @@ #include "expr/node.h" #include "options/theory_options.h" #include "proof/trust_node.h" +#include "smt/env.h" #include "theory/assertion.h" #include "theory/care_graph.h" #include "theory/logic_info.h" @@ -105,14 +106,8 @@ class Theory { /** An integer identifying the type of the theory. */ TheoryId d_id; - /** The SAT search context for the Theory. */ - context::Context* d_satContext; - - /** The user level assertion context for the Theory. */ - context::UserContext* d_userContext; - - /** Information about the logic we're operating within. */ - const LogicInfo& d_logicInfo; + /** The environment class */ + Env& d_env; /** * The assertFact() queue. @@ -169,12 +164,9 @@ class Theory { * w.r.t. the SmtEngine. */ Theory(TheoryId id, - context::Context* satContext, - context::UserContext* userContext, + Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string instance = ""); // taking : No default. /** @@ -241,9 +233,7 @@ class Theory { */ inline Assertion get(); - const LogicInfo& getLogicInfo() const { - return d_logicInfo; - } + const LogicInfo& getLogicInfo() const { return d_env.getLogicInfo(); } /** * Set separation logic heap. This is called when the location and data @@ -454,18 +444,21 @@ class Theory { return d_id; } + /** + * Get a reference to the environment. + */ + Env& getEnv() const { return d_env; } + /** * Get the SAT context associated to this Theory. */ - context::Context* getSatContext() const { - return d_satContext; - } + context::Context* getSatContext() const { return d_env.getContext(); } /** * Get the context associated to this Theory. */ context::UserContext* getUserContext() const { - return d_userContext; + return d_env.getUserContext(); } /** @@ -512,7 +505,7 @@ class Theory { */ void assertFact(TNode assertion, bool isPreregistered) { Trace("theory") << "Theory<" << getId() << ">::assertFact[" - << d_satContext->getLevel() << "](" << assertion << ", " + << getSatContext()->getLevel() << "](" << assertion << ", " << (isPreregistered ? "true" : "false") << ")" << std::endl; d_facts.push_back(Assertion(assertion, isPreregistered)); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 233ea64ed..21c22586b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -218,12 +218,12 @@ context::UserContext* TheoryEngine::getUserContext() const return d_env.getUserContext(); } -TheoryEngine::TheoryEngine(Env& env, - ProofNodeManager* pnm) +TheoryEngine::TheoryEngine(Env& env) : d_propEngine(nullptr), d_env(env), d_logicInfo(env.getLogicInfo()), - d_pnm(pnm), + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr), d_lazyProof(d_pnm != nullptr ? new LazyCDProof(d_pnm, nullptr, diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0c4a80c98..1c42e336f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -295,7 +295,7 @@ class TheoryEngine { public: /** Constructs a theory engine */ - TheoryEngine(Env& env, ProofNodeManager* pnm); + TheoryEngine(Env& env); /** Destroys a theory engine */ ~TheoryEngine(); @@ -314,12 +314,8 @@ class TheoryEngine { { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = new TheoryClass(getSatContext(), - getUserContext(), - *d_theoryOut[theoryId], - theory::Valuation(this), - d_logicInfo, - d_pnm); + d_theoryTable[theoryId] = + new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this)); theory::Rewriter::registerTheoryRewriter( theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4224ec854..633934f61 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -40,20 +40,17 @@ namespace theory { namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, - context::UserContext* u, +TheoryUF::TheoryUF(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm, std::string instanceName) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName), + : Theory(THEORY_UF, env, out, valuation, instanceName), d_thss(nullptr), d_ho(nullptr), - d_functionsTerms(c), - d_symb(u, instanceName), - d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false), + d_functionsTerms(getSatContext()), + d_symb(getUserContext(), instanceName), + d_state(getSatContext(), getUserContext(), valuation), + d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index c953cfe5c..6f04035ed 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -98,12 +98,9 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c, - context::UserContext* u, + TheoryUF(Env& env, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm = nullptr, std::string instanceName = ""); ~TheoryUF(); diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 4226f8095..c27c02925 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -206,14 +206,9 @@ template class DummyTheory : public theory::Theory { public: - DummyTheory(context::Context* ctxt, - context::UserContext* uctxt, - theory::OutputChannel& out, - theory::Valuation valuation, - const LogicInfo& logicInfo, - ProofNodeManager* pnm) - : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm), - d_state(ctxt, uctxt, valuation) + DummyTheory(Env& env, theory::OutputChannel& out, theory::Valuation valuation) + : Theory(theoryId, env, out, valuation), + d_state(getSatContext(), getUserContext(), valuation) { // use a default theory state object d_theoryState = &d_state; diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index 94021a9e3..915b469db 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -37,30 +37,19 @@ class TestTheoryWhite : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_context = d_smtEngine->getContext(); - d_user_context = d_smtEngine->getUserContext(); - d_logicInfo.reset(new LogicInfo()); - d_logicInfo->lock(); d_smtEngine->finishInit(); delete d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN]; delete d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN]; d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = nullptr; d_smtEngine->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = nullptr; - d_dummy_theory.reset(new DummyTheory(d_context, - d_user_context, - d_outputChannel, - Valuation(nullptr), - *d_logicInfo, - nullptr)); + d_dummy_theory.reset(new DummyTheory( + d_smtEngine->getEnv(), d_outputChannel, Valuation(nullptr))); d_outputChannel.clear(); d_atom0 = d_nodeManager->mkConst(true); d_atom1 = d_nodeManager->mkConst(false); } - Context* d_context; - UserContext* d_user_context; - std::unique_ptr d_logicInfo; DummyOutputChannel d_outputChannel; std::unique_ptr> d_dummy_theory; Node d_atom0; -- cgit v1.2.3 From 11b6d67d32160681d4495fd92930ffb6ddb79abe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 16 Aug 2021 09:11:18 -0700 Subject: Use InferenceManager in ExtTheory (#7006) This PR refactors the ExtTheory class to use a given inference manager instead of a given output channel. --- src/theory/arith/nl/nonlinear_extension.cpp | 2 +- src/theory/ext_theory.cpp | 14 +++++++------- src/theory/ext_theory.h | 9 +++++---- src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 3 +++ src/theory/strings/theory_strings.cpp | 2 +- src/theory/strings/theory_strings.h | 4 ++-- 7 files changed, 20 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index a8b056d45..785127db5 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -48,7 +48,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_extTheory(d_extTheoryCb, containing.getSatContext(), containing.getUserContext(), - containing.getOutputChannel()), + d_im), d_model(containing.getSatContext()), d_trSlv(d_im, d_model, pnm, containing.getUserContext()), d_extState(d_im, d_model, pnm, containing.getUserContext()), diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index b4bb896ae..627129c3a 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -84,9 +84,9 @@ bool ExtTheoryCallback::getReduction(int effort, ExtTheory::ExtTheory(ExtTheoryCallback& p, context::Context* c, context::UserContext* u, - OutputChannel& out) + TheoryInferenceManager& im) : d_parent(p), - d_out(out), + d_im(im), d_ext_func_terms(c), d_extfExtReducedIdMap(c), d_ci_inactive(u), @@ -237,7 +237,7 @@ bool ExtTheory::doInferencesInternal(int effort, if (!nr.isNull() && n != nr) { Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr); - if (sendLemma(lem, true)) + if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY, true)) { Trace("extt-lemma") << "ExtTheory : reduction lemma : " << lem << std::endl; @@ -287,7 +287,7 @@ bool ExtTheory::doInferencesInternal(int effort, Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << exp[i] << std::endl; Trace("extt-debug") << "...send lemma " << lem << std::endl; - if (sendLemma(lem)) + if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY)) { Trace("extt-lemma") << "ExtTheory : substitution + rewrite lemma : " << lem @@ -359,14 +359,14 @@ bool ExtTheory::doInferencesInternal(int effort, return false; } -bool ExtTheory::sendLemma(Node lem, bool preprocess) +bool ExtTheory::sendLemma(Node lem, InferenceId id, bool preprocess) { if (preprocess) { if (d_pp_lemmas.find(lem) == d_pp_lemmas.end()) { d_pp_lemmas.insert(lem); - d_out.lemma(lem); + d_im.lemma(lem, id); return true; } } @@ -375,7 +375,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess) if (d_lemmas.find(lem) == d_lemmas.end()) { d_lemmas.insert(lem); - d_out.lemma(lem); + d_im.lemma(lem, id); return true; } } diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index f5e08e2f5..01b191e0a 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -41,6 +41,7 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" +#include "theory/theory_inference_manager.h" namespace cvc5 { namespace theory { @@ -176,7 +177,7 @@ class ExtTheory ExtTheory(ExtTheoryCallback& p, context::Context* c, context::UserContext* u, - OutputChannel& out); + TheoryInferenceManager& im); virtual ~ExtTheory() {} /** Tells this class to treat terms with Kind k as extended functions */ void addFunctionKind(Kind k) { d_extf_kind[k] = true; } @@ -291,11 +292,11 @@ class ExtTheory bool batch, bool isRed); /** send lemma on the output channel */ - bool sendLemma(Node lem, bool preprocess = false); + bool sendLemma(Node lem, InferenceId id, bool preprocess = false); /** reference to the callback */ ExtTheoryCallback& d_parent; - /** Reference to the output channel we are using */ - OutputChannel& d_out; + /** inference manager used to send lemmas */ + TheoryInferenceManager& d_im; /** the true node */ Node d_true; /** extended function terms, map to whether they are active */ diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 9d8cddb69..7bb87819e 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -28,6 +28,7 @@ const char* toString(InferenceId i) { case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE"; case InferenceId::COMBINATION_SPLIT: return "COMBINATION_SPLIT"; + case InferenceId::EXTT_SIMPLIFY: return "EXTT_SIMPLIFY"; case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX"; case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ"; case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 3a317e0a4..4c6140872 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -45,6 +45,9 @@ enum class InferenceId EQ_CONSTANT_MERGE, // a split from theory combination COMBINATION_SPLIT, + // ---------------------------------- ext theory + // a simplification from the extended theory utility + EXTT_SIMPLIFY, // ---------------------------------- arith theory //-------------------- linear core // black box conflicts. It's magic. diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 319a6698b..19713d0a1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -58,8 +58,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_eagerSolver(d_state), d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), - d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), out), d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm), + d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), d_im), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c1ce71cef..8f0205b48 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -262,10 +262,10 @@ class TheoryStrings : public Theory { TermRegistry d_termReg; /** The extended theory callback */ StringsExtfCallback d_extTheoryCb; - /** Extended theory, responsible for context-dependent simplification. */ - ExtTheory d_extTheory; /** The (custom) output channel of the theory of strings */ InferenceManager d_im; + /** Extended theory, responsible for context-dependent simplification. */ + ExtTheory d_extTheory; /** The theory rewriter for this theory. */ StringsRewriter d_rewriter; /** The proof rule checker */ -- cgit v1.2.3 From a11de769885cf9ac4b2c2f06409976080b326fe6 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 16 Aug 2021 17:20:27 -0700 Subject: Push Env class into TheoryState (#7012) This PR is a follow-up to #7011, making the Env object available in the TheoryState base class. --- src/theory/arith/arith_state.cpp | 6 ++---- src/theory/arith/arith_state.h | 3 ++- src/theory/arith/theory_arith.cpp | 2 +- src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/bags/solver_state.cpp | 5 +---- src/theory/bags/solver_state.h | 3 ++- src/theory/bags/theory_bags.cpp | 2 +- src/theory/builtin/theory_builtin.cpp | 2 +- src/theory/bv/theory_bv.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 2 +- src/theory/fp/theory_fp.cpp | 2 +- src/theory/quantifiers/quantifiers_state.cpp | 7 ++++--- src/theory/quantifiers/quantifiers_state.h | 3 +-- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- src/theory/sep/theory_sep.cpp | 2 +- src/theory/sets/solver_state.cpp | 7 ++----- src/theory/sets/solver_state.h | 3 +-- src/theory/sets/theory_sets.cpp | 2 +- src/theory/strings/solver_state.cpp | 11 ++++++----- src/theory/strings/solver_state.h | 3 +-- src/theory/strings/theory_strings.cpp | 2 +- src/theory/theory_state.cpp | 19 +++++++++++-------- src/theory/theory_state.h | 12 +++++++----- src/theory/uf/theory_uf.cpp | 2 +- test/unit/test_smt.h | 2 +- 25 files changed, 53 insertions(+), 55 deletions(-) (limited to 'src') diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp index 93d410bf8..3d43077e5 100644 --- a/src/theory/arith/arith_state.cpp +++ b/src/theory/arith/arith_state.cpp @@ -21,10 +21,8 @@ namespace cvc5 { namespace theory { namespace arith { -ArithState::ArithState(context::Context* c, - context::UserContext* u, - Valuation val) - : TheoryState(c, u, val), d_parent(nullptr) +ArithState::ArithState(Env& env, Valuation val) + : TheoryState(env, val), d_parent(nullptr) { } diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h index a54ae6bf0..0f0f02f02 100644 --- a/src/theory/arith/arith_state.h +++ b/src/theory/arith/arith_state.h @@ -38,7 +38,8 @@ class TheoryArithPrivate; class ArithState : public TheoryState { public: - ArithState(context::Context* c, context::UserContext* u, Valuation val); + ArithState(Env& env, + Valuation val); ~ArithState() {} /** Are we currently in conflict? */ bool isInConflict() const override; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 8cb607dd7..37069d8b8 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -39,7 +39,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARITH, env, out, valuation), d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( "theory::arith::ppRewriteTimer")), - d_astate(getSatContext(), getUserContext(), valuation), + d_astate(env, valuation), d_im(*this, d_astate, d_pnm), d_ppre(getSatContext(), d_pnm), d_bab(d_astate, d_im, d_ppre, d_pnm), diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index eaa9c9294..1a6dfedbb 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -83,7 +83,7 @@ TheoryArrays::TheoryArrays(Env& env, d_ppEqualityEngine(getUserContext(), name + "pp", true), d_ppFacts(getUserContext()), d_rewriter(d_pnm), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, d_pnm), d_literalsToPropagate(getSatContext()), d_literalsToPropagateIndex(getSatContext(), 0), diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index 6c80e00bd..50c6919fa 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -27,10 +27,7 @@ namespace cvc5 { namespace theory { namespace bags { -SolverState::SolverState(context::Context* c, - context::UserContext* u, - Valuation val) - : TheoryState(c, u, val) +SolverState::SolverState(Env& env, Valuation val) : TheoryState(env, val) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index 9c2222e95..68fffacbd 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -29,7 +29,8 @@ namespace bags { class SolverState : public TheoryState { public: - SolverState(context::Context* c, context::UserContext* u, Valuation val); + SolverState(Env& env, + Valuation val); /** * This function adds the bag representative n to the set d_bags if it is not diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 42a1e2c6b..f8483064d 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -29,7 +29,7 @@ namespace bags { TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_BAGS, env, out, valuation), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, d_pnm), d_ig(&d_state, &d_im), d_notify(*this, d_im), diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index f12d2caf9..092bcc9ab 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -27,7 +27,7 @@ namespace builtin { TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_BUILTIN, env, out, valuation), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, d_pnm, "theory::builtin::") { // indicate we are using the default theory state and inference managers diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 1976177b7..d4926a785 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -37,7 +37,7 @@ TheoryBV::TheoryBV(Env& env, : Theory(THEORY_BV, env, out, valuation, name), d_internal(nullptr), d_rewriter(), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, nullptr, "theory::bv::"), d_notify(d_im), d_invalidateModelCache(getSatContext(), true), diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 759cc4c87..3dfd9b458 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -60,7 +60,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env, d_singleton_eq(getUserContext()), d_lemmas_produced_c(getUserContext()), d_sygusExtension(nullptr), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, d_pnm), d_notify(d_im, *this) { diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index a016c7897..bd5662cdd 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -70,7 +70,7 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) d_floatToRealMap(getUserContext()), d_abstractionMap(getUserContext()), d_rewriter(getUserContext()), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, d_pnm, "theory::fp::", false), d_wbFactsCache(getUserContext()) { diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 7654a6326..39af9c2c9 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -22,11 +22,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -QuantifiersState::QuantifiersState(context::Context* c, - context::UserContext* u, +QuantifiersState::QuantifiersState(Env& env, Valuation val, const LogicInfo& logicInfo) - : TheoryState(c, u, val), d_ierCounterc(c), d_logicInfo(logicInfo) + : TheoryState(env, val), + d_ierCounterc(env.getContext()), + d_logicInfo(logicInfo) { // allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h index e4a05b078..92b744cd0 100644 --- a/src/theory/quantifiers/quantifiers_state.h +++ b/src/theory/quantifiers/quantifiers_state.h @@ -32,8 +32,7 @@ namespace quantifiers { class QuantifiersState : public TheoryState { public: - QuantifiersState(context::Context* c, - context::UserContext* u, + QuantifiersState(Env& env, Valuation val, const LogicInfo& logicInfo); ~QuantifiersState() {} diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 3adf53b57..a108d4614 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -34,7 +34,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_QUANTIFIERS, env, out, valuation), - d_qstate(getSatContext(), getUserContext(), valuation, getLogicInfo()), + d_qstate(env, valuation, getLogicInfo()), d_qreg(), d_treg(d_qstate, d_qreg), d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm), diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 0b16ddd27..92d15653e 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -46,7 +46,7 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_SEP, env, out, valuation), d_lemmas_produced_c(getUserContext()), d_bounds_init(false), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, d_pnm, "theory::sep::"), d_notify(*this), d_reduce(getUserContext()), diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 2aaa82706..6f8976f4d 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -26,11 +26,8 @@ namespace cvc5 { namespace theory { namespace sets { -SolverState::SolverState(context::Context* c, - context::UserContext* u, - Valuation val, - SkolemCache& skc) - : TheoryState(c, u, val), d_skCache(skc), d_members(c) +SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc) + : TheoryState(env, val), d_skCache(skc), d_members(env.getContext()) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 63039eddd..ff9bc8bf9 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -46,8 +46,7 @@ class SolverState : public TheoryState typedef context::CDHashMap NodeIntMap; public: - SolverState(context::Context* c, - context::UserContext* u, + SolverState(Env& env, Valuation val, SkolemCache& skc); //-------------------------------- initialize per check diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 5ea13ea4d..23ac08749 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -30,7 +30,7 @@ namespace sets { TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_SETS, env, out, valuation), d_skCache(), - d_state(getSatContext(), getUserContext(), valuation, d_skCache), + d_state(env, valuation, d_skCache), d_im(*this, d_state, d_pnm), d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, d_pnm)), d_notify(*d_internal.get(), d_im) diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 1ddf2af58..32ed6896c 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -28,10 +28,11 @@ namespace cvc5 { namespace theory { namespace strings { -SolverState::SolverState(context::Context* c, - context::UserContext* u, - Valuation& v) - : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN) +SolverState::SolverState(Env& env, Valuation& v) + : TheoryState(env, v), + d_eeDisequalities(env.getContext()), + d_pendingConflictSet(env.getContext(), false), + d_pendingConflict(InferenceId::UNKNOWN) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_false = NodeManager::currentNM()->mkConst(false); @@ -64,7 +65,7 @@ EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake) } if (doMake) { - EqcInfo* ei = new EqcInfo(d_context); + EqcInfo* ei = new EqcInfo(d_env.getContext()); d_eqcInfo[eqc] = ei; return ei; } diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 422c29760..bbeb470f7 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -48,8 +48,7 @@ class SolverState : public TheoryState typedef context::CDList NodeList; public: - SolverState(context::Context* c, - context::UserContext* u, + SolverState(Env& env, Valuation& v); ~SolverState(); //-------------------------------------- disequality information diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 19713d0a1..8b71df31b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -54,7 +54,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) : Theory(THEORY_STRINGS, env, out, valuation), d_notify(*this), d_statistics(), - d_state(getSatContext(), getUserContext(), d_valuation), + d_state(env, d_valuation), d_eagerSolver(d_state), d_termReg(d_state, d_statistics, d_pnm), d_extTheoryCb(), diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index 5ac5e6ae9..72ab24a7e 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -20,22 +20,25 @@ namespace cvc5 { namespace theory { -TheoryState::TheoryState(context::Context* c, - context::UserContext* u, - Valuation val) - : d_context(c), - d_ucontext(u), +TheoryState::TheoryState(Env& env, Valuation val) + : d_env(env), d_valuation(val), d_ee(nullptr), - d_conflict(c, false) + d_conflict(d_env.getContext(), false) { } void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; } -context::Context* TheoryState::getSatContext() const { return d_context; } +context::Context* TheoryState::getSatContext() const +{ + return d_env.getContext(); +} -context::UserContext* TheoryState::getUserContext() const { return d_ucontext; } +context::UserContext* TheoryState::getUserContext() const +{ + return d_env.getUserContext(); +} bool TheoryState::hasTerm(TNode a) const { diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 2c7bad60b..58a66ef46 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -20,6 +20,7 @@ #include "context/cdo.h" #include "expr/node.h" +#include "smt/env.h" #include "theory/valuation.h" namespace cvc5 { @@ -32,7 +33,8 @@ class EqualityEngine; class TheoryState { public: - TheoryState(context::Context* c, context::UserContext* u, Valuation val); + TheoryState(Env& env, + Valuation val); virtual ~TheoryState() {} /** * Set equality engine, where ee is a pointer to the official equality engine @@ -43,6 +45,8 @@ class TheoryState context::Context* getSatContext() const; /** Get the user context */ context::UserContext* getUserContext() const; + /** Get the environment */ + Env& getEnv() const { return d_env; } //-------------------------------------- equality information /** Is t registered as a term in the equality engine of this class? */ virtual bool hasTerm(TNode a) const; @@ -111,10 +115,8 @@ class TheoryState Valuation& getValuation(); protected: - /** Pointer to the SAT context object used by the theory. */ - context::Context* d_context; - /** Pointer to the user context object used by the theory. */ - context::UserContext* d_ucontext; + /** Reference to the environment. */ + Env& d_env; /** * The valuation proxy for the Theory to communicate back with the * theory engine (and other theories). diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 633934f61..3525786d5 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -49,7 +49,7 @@ TheoryUF::TheoryUF(Env& env, d_ho(nullptr), d_functionsTerms(getSatContext()), d_symb(getUserContext(), instanceName), - d_state(getSatContext(), getUserContext(), valuation), + d_state(env, valuation), d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), d_notify(d_im, *this) { diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index c27c02925..f1644dfcd 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -208,7 +208,7 @@ class DummyTheory : public theory::Theory public: DummyTheory(Env& env, theory::OutputChannel& out, theory::Valuation valuation) : Theory(theoryId, env, out, valuation), - d_state(getSatContext(), getUserContext(), valuation) + d_state(env, valuation) { // use a default theory state object d_theoryState = &d_state; -- cgit v1.2.3 From 1d81aaef0d3a3f6a9cadc57d0e667506138af003 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Aug 2021 20:57:40 -0500 Subject: Initial refactoring of set defaults (#7021) This commit starts to carve out better control flow structure in setDefaults. It makes setDefaults contained in a class, and moves a few blocks of code to their own functions. This class also makes options manager obsolete, it is deleted in this PR. There should be no behavior change in this PR. --- src/CMakeLists.txt | 2 - src/smt/options_manager.cpp | 48 ----- src/smt/options_manager.h | 72 ------- src/smt/set_defaults.cpp | 488 +++++++++++++++++++++++--------------------- src/smt/set_defaults.h | 47 +++-- src/smt/smt_engine.cpp | 14 +- src/smt/smt_engine.h | 6 - 7 files changed, 290 insertions(+), 387 deletions(-) delete mode 100644 src/smt/options_manager.cpp delete mode 100644 src/smt/options_manager.h (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 698c38cae..bc7103f0d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -311,8 +311,6 @@ libcvc5_add_sources( smt/node_command.h smt/optimization_solver.cpp smt/optimization_solver.h - smt/options_manager.cpp - smt/options_manager.h smt/output_manager.cpp smt/output_manager.h smt/quant_elim_solver.cpp diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp deleted file mode 100644 index 9ffb396d1..000000000 --- a/src/smt/options_manager.cpp +++ /dev/null @@ -1,48 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Module for managing options of an SmtEngine. - */ - -#include "smt/options_manager.h" - -#include "base/output.h" -#include "expr/expr_iomanip.h" -#include "options/base_options.h" -#include "options/expr_options.h" -#include "options/smt_options.h" -#include "smt/command.h" -#include "smt/dump.h" -#include "smt/set_defaults.h" -#include "util/resource_manager.h" - -namespace cvc5 { -namespace smt { - -OptionsManager::OptionsManager(Options* opts) : d_options(opts) -{ -} - -OptionsManager::~OptionsManager() {} - -void OptionsManager::notifySetOption(const std::string& key) -{ -} - -void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver) -{ - // ensure that our heuristics are properly set up - setDefaults(logic, *d_options, isInternalSubsolver); -} - -} // namespace smt -} // namespace cvc5 diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h deleted file mode 100644 index e7c9d61cb..000000000 --- a/src/smt/options_manager.h +++ /dev/null @@ -1,72 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Tim King, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Module for managing options of an SmtEngine. - */ - -#ifndef CVC5__SMT__OPTIONS_MANAGER_H -#define CVC5__SMT__OPTIONS_MANAGER_H - -#include "options/options_listener.h" - -namespace cvc5 { - -class LogicInfo; -class Options; -class ResourceManager; -class SmtEngine; - -namespace smt { - -/** - * This class is intended to be used by SmtEngine, and is responsible for: - * (1) Implementing core options including timeouts and output preferences, - * (2) Setting default values for options based on a logic. - * - * Notice that the constructor of this class retroactively sets all - * necessary options that have already been set in the options object it is - * given. This is to ensure that the command line arguments, which modified - * on an options object in the driver, immediately take effect upon creation of - * this class. - */ -class OptionsManager : public OptionsListener -{ - public: - OptionsManager(Options* opts); - ~OptionsManager(); - /** - * Called when a set option call is made on the options object associated - * with this class. This handles all options that should be taken into account - * immediately instead of e.g. at SmtEngine::finishInit time. This primarily - * includes options related to parsing and output. - * - * This function call is made after the option has been updated. This means - * that the value of the option can be queried in the options object that - * this class is listening to. - */ - void notifySetOption(const std::string& key) override; - /** - * Finish init, which is called at the beginning of SmtEngine::finishInit, - * just before solving begins. This initializes the options pertaining to - * time limits, and sets the default options. - */ - void finishInit(LogicInfo& logic, bool isInternalSubsolver); - - private: - /** Reference to the options object */ - Options* d_options; -}; - -} // namespace smt -} // namespace cvc5 - -#endif /* CVC5__SMT__OPTIONS_MANAGER_H */ diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c916ac962..6fd2a3f68 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -46,7 +46,12 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) +SetDefaults::SetDefaults(bool isInternalSubsolver) + : d_isInternalSubsolver(isInternalSubsolver) +{ +} + +void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) { // implied options if (opts.smt.debugCheckModels) @@ -333,7 +338,7 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) } // sygus inference may require datatypes - if (!isInternalSubsolver) + if (!d_isInternalSubsolver) { if (opts.smt.produceAbducts || opts.smt.produceInterpols != options::ProduceInterpols::NONE @@ -659,95 +664,9 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) } ///////////////////////////////////////////////////////////////////////////// - // Theory widening - // - // Some theories imply the use of other theories to handle certain operators, - // e.g. UF to handle partial functions. + // Widen logic ///////////////////////////////////////////////////////////////////////////// - bool needsUf = false; - // strings require LIA, UF; widen the logic - if (logic.isTheoryEnabled(THEORY_STRINGS)) - { - LogicInfo log(logic.getUnlockedCopy()); - // Strings requires arith for length constraints, and also UF - needsUf = true; - if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) - { - Notice() - << "Enabling linear integer arithmetic because strings are enabled" - << std::endl; - log.enableTheory(THEORY_ARITH); - log.enableIntegers(); - log.arithOnlyLinear(); - } - else if (!logic.areIntegersUsed()) - { - Notice() << "Enabling integer arithmetic because strings are enabled" - << std::endl; - log.enableIntegers(); - } - logic = log; - logic.lock(); - } - if (opts.bv.bvAbstraction) - { - // bv abstraction may require UF - Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; - needsUf = true; - } - else if (opts.quantifiers.preSkolemQuantNested - && opts.quantifiers.preSkolemQuantNestedWasSetByUser) - { - // if pre-skolem nested is explictly set, then we require UF. If it is - // not explicitly set, it is disabled below if UF is not present. - Notice() << "Enabling UF because preSkolemQuantNested requires it." - << std::endl; - needsUf = true; - } - if (needsUf - // Arrays, datatypes and sets permit Boolean terms and thus require UF - || logic.isTheoryEnabled(THEORY_ARRAYS) - || logic.isTheoryEnabled(THEORY_DATATYPES) - || logic.isTheoryEnabled(THEORY_SETS) - || logic.isTheoryEnabled(THEORY_BAGS) - // Non-linear arithmetic requires UF to deal with division/mod because - // their expansion introduces UFs for the division/mod-by-zero case. - // If we are eliminating non-linear arithmetic via solve-int-as-bv, - // then this is not required, since non-linear arithmetic will be - // eliminated altogether (or otherwise fail at preprocessing). - || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && opts.smt.solveIntAsBV == 0) - // FP requires UF since there are multiple operators that are partially - // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more - // details). - || logic.isTheoryEnabled(THEORY_FP)) - { - if (!logic.isTheoryEnabled(THEORY_UF)) - { - LogicInfo log(logic.getUnlockedCopy()); - if (!needsUf) - { - Notice() << "Enabling UF because " << logic << " requires it." - << std::endl; - } - log.enableTheory(THEORY_UF); - logic = log; - logic.lock(); - } - } - if (opts.arith.arithMLTrick) - { - if (!logic.areIntegersUsed()) - { - // enable integers - LogicInfo log(logic.getUnlockedCopy()); - Notice() << "Enabling integers because arithMLTrick requires it." - << std::endl; - log.enableIntegers(); - logic = log; - logic.lock(); - } - } + widenLogic(logic, opts); ///////////////////////////////////////////////////////////////////////////// // Set the options for the theoryOf @@ -1124,154 +1043,7 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) // if we are attempting to rewrite everything to SyGuS, use sygus() if (usesSygus) { - if (!opts.quantifiers.sygus) - { - Trace("smt") << "turning on sygus" << std::endl; - } - opts.quantifiers.sygus = true; - // must use Ferrante/Rackoff for real arithmetic - if (!opts.quantifiers.cegqiMidpointWasSetByUser) - { - opts.quantifiers.cegqiMidpoint = true; - } - // must disable cegqi-bv since it may introduce witness terms, which - // cannot appear in synthesis solutions - if (!opts.quantifiers.cegqiBvWasSetByUser) - { - opts.quantifiers.cegqiBv = false; - } - if (opts.quantifiers.sygusRepairConst) - { - if (!opts.quantifiers.cegqiWasSetByUser) - { - opts.quantifiers.cegqi = true; - } - } - if (opts.quantifiers.sygusInference) - { - // optimization: apply preskolemization, makes it succeed more often - if (!opts.quantifiers.preSkolemQuantWasSetByUser) - { - opts.quantifiers.preSkolemQuant = true; - } - if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) - { - opts.quantifiers.preSkolemQuantNested = true; - } - } - // counterexample-guided instantiation for sygus - if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) - { - opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE; - } - if (!opts.quantifiers.quantConflictFindWasSetByUser) - { - opts.quantifiers.quantConflictFind = false; - } - if (!opts.quantifiers.instNoEntailWasSetByUser) - { - opts.quantifiers.instNoEntail = false; - } - if (!opts.quantifiers.cegqiFullEffortWasSetByUser) - { - // should use full effort cbqi for single invocation and repair const - opts.quantifiers.cegqiFullEffort = true; - } - if (opts.quantifiers.sygusRew) - { - opts.quantifiers.sygusRewSynth = true; - opts.quantifiers.sygusRewVerify = true; - } - if (opts.quantifiers.sygusRewSynthInput) - { - // If we are using synthesis rewrite rules from input, we use - // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for - // details on this technique. - opts.quantifiers.sygusRewSynth = true; - // we should not use the extended rewriter, since we are interested - // in rewrites that are not in the main rewriter - if (!opts.quantifiers.sygusExtRewWasSetByUser) - { - opts.quantifiers.sygusExtRew = false; - } - } - // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm - // is one that is specialized for returning a single solution. Non-basic - // sygus algorithms currently include the PBE solver, UNIF+PI, static - // template inference for invariant synthesis, and single invocation - // techniques. - bool reqBasicSygus = false; - if (opts.smt.produceAbducts) - { - // if doing abduction, we should filter strong solutions - if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) - { - opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG; - } - // we must use basic sygus algorithms, since e.g. we require checking - // a sygus side condition for consistency with axioms. - reqBasicSygus = true; - } - if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify - || opts.quantifiers.sygusQueryGen) - { - // rewrite rule synthesis implies that sygus stream must be true - opts.quantifiers.sygusStream = true; - } - if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) - { - // Streaming and incremental mode are incompatible with techniques that - // focus the search towards finding a single solution. - reqBasicSygus = true; - } - // Now, disable options for non-basic sygus algorithms, if necessary. - if (reqBasicSygus) - { - if (!opts.quantifiers.sygusUnifPbeWasSetByUser) - { - opts.quantifiers.sygusUnifPbe = false; - } - if (opts.quantifiers.sygusUnifPiWasSetByUser) - { - opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE; - } - if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) - { - opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE; - } - if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) - { - opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; - } - } - if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) - { - opts.datatypes.dtRewriteErrorSel = true; - } - // do not miniscope - if (!opts.quantifiers.miniscopeQuantWasSetByUser) - { - opts.quantifiers.miniscopeQuant = false; - } - if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser) - { - opts.quantifiers.miniscopeQuantFreeVar = false; - } - if (!opts.quantifiers.quantSplitWasSetByUser) - { - opts.quantifiers.quantSplit = false; - } - // do not do macros - if (!opts.quantifiers.macrosQuantWasSetByUser) - { - opts.quantifiers.macrosQuant = false; - } - // use tangent planes by default, since we want to put effort into - // the verification step for sygus queries with non-linear arithmetic - if (!opts.arith.nlExtTangentPlanesWasSetByUser) - { - opts.arith.nlExtTangentPlanes = true; - } + setDefaultsSygus(opts); } // counterexample-guided instantiation for non-sygus // enable if any possible quantifiers with arithmetic, datatypes or bitvectors @@ -1581,5 +1353,245 @@ void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver) #endif } +void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) +{ + bool needsUf = false; + // strings require LIA, UF; widen the logic + if (logic.isTheoryEnabled(THEORY_STRINGS)) + { + LogicInfo log(logic.getUnlockedCopy()); + // Strings requires arith for length constraints, and also UF + needsUf = true; + if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()) + { + Notice() + << "Enabling linear integer arithmetic because strings are enabled" + << std::endl; + log.enableTheory(THEORY_ARITH); + log.enableIntegers(); + log.arithOnlyLinear(); + } + else if (!logic.areIntegersUsed()) + { + Notice() << "Enabling integer arithmetic because strings are enabled" + << std::endl; + log.enableIntegers(); + } + logic = log; + logic.lock(); + } + if (opts.bv.bvAbstraction) + { + // bv abstraction may require UF + Notice() << "Enabling UF because bvAbstraction requires it." << std::endl; + needsUf = true; + } + else if (opts.quantifiers.preSkolemQuantNested + && opts.quantifiers.preSkolemQuantNestedWasSetByUser) + { + // if pre-skolem nested is explictly set, then we require UF. If it is + // not explicitly set, it is disabled below if UF is not present. + Notice() << "Enabling UF because preSkolemQuantNested requires it." + << std::endl; + needsUf = true; + } + if (needsUf + // Arrays, datatypes and sets permit Boolean terms and thus require UF + || logic.isTheoryEnabled(THEORY_ARRAYS) + || logic.isTheoryEnabled(THEORY_DATATYPES) + || logic.isTheoryEnabled(THEORY_SETS) + || logic.isTheoryEnabled(THEORY_BAGS) + // Non-linear arithmetic requires UF to deal with division/mod because + // their expansion introduces UFs for the division/mod-by-zero case. + // If we are eliminating non-linear arithmetic via solve-int-as-bv, + // then this is not required, since non-linear arithmetic will be + // eliminated altogether (or otherwise fail at preprocessing). + || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() + && opts.smt.solveIntAsBV == 0) + // FP requires UF since there are multiple operators that are partially + // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more + // details). + || logic.isTheoryEnabled(THEORY_FP)) + { + if (!logic.isTheoryEnabled(THEORY_UF)) + { + LogicInfo log(logic.getUnlockedCopy()); + if (!needsUf) + { + Notice() << "Enabling UF because " << logic << " requires it." + << std::endl; + } + log.enableTheory(THEORY_UF); + logic = log; + logic.lock(); + } + } + if (opts.arith.arithMLTrick) + { + if (!logic.areIntegersUsed()) + { + // enable integers + LogicInfo log(logic.getUnlockedCopy()); + Notice() << "Enabling integers because arithMLTrick requires it." + << std::endl; + log.enableIntegers(); + logic = log; + logic.lock(); + } + } +} + +void SetDefaults::setDefaultsSygus(Options& opts) +{ + if (!opts.quantifiers.sygus) + { + Trace("smt") << "turning on sygus" << std::endl; + } + opts.quantifiers.sygus = true; + // must use Ferrante/Rackoff for real arithmetic + if (!opts.quantifiers.cegqiMidpointWasSetByUser) + { + opts.quantifiers.cegqiMidpoint = true; + } + // must disable cegqi-bv since it may introduce witness terms, which + // cannot appear in synthesis solutions + if (!opts.quantifiers.cegqiBvWasSetByUser) + { + opts.quantifiers.cegqiBv = false; + } + if (opts.quantifiers.sygusRepairConst) + { + if (!opts.quantifiers.cegqiWasSetByUser) + { + opts.quantifiers.cegqi = true; + } + } + if (opts.quantifiers.sygusInference) + { + // optimization: apply preskolemization, makes it succeed more often + if (!opts.quantifiers.preSkolemQuantWasSetByUser) + { + opts.quantifiers.preSkolemQuant = true; + } + if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser) + { + opts.quantifiers.preSkolemQuantNested = true; + } + } + // counterexample-guided instantiation for sygus + if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) + { + opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE; + } + if (!opts.quantifiers.quantConflictFindWasSetByUser) + { + opts.quantifiers.quantConflictFind = false; + } + if (!opts.quantifiers.instNoEntailWasSetByUser) + { + opts.quantifiers.instNoEntail = false; + } + if (!opts.quantifiers.cegqiFullEffortWasSetByUser) + { + // should use full effort cbqi for single invocation and repair const + opts.quantifiers.cegqiFullEffort = true; + } + if (opts.quantifiers.sygusRew) + { + opts.quantifiers.sygusRewSynth = true; + opts.quantifiers.sygusRewVerify = true; + } + if (opts.quantifiers.sygusRewSynthInput) + { + // If we are using synthesis rewrite rules from input, we use + // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for + // details on this technique. + opts.quantifiers.sygusRewSynth = true; + // we should not use the extended rewriter, since we are interested + // in rewrites that are not in the main rewriter + if (!opts.quantifiers.sygusExtRewWasSetByUser) + { + opts.quantifiers.sygusExtRew = false; + } + } + // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm + // is one that is specialized for returning a single solution. Non-basic + // sygus algorithms currently include the PBE solver, UNIF+PI, static + // template inference for invariant synthesis, and single invocation + // techniques. + bool reqBasicSygus = false; + if (opts.smt.produceAbducts) + { + // if doing abduction, we should filter strong solutions + if (!opts.quantifiers.sygusFilterSolModeWasSetByUser) + { + opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG; + } + // we must use basic sygus algorithms, since e.g. we require checking + // a sygus side condition for consistency with axioms. + reqBasicSygus = true; + } + if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify + || opts.quantifiers.sygusQueryGen) + { + // rewrite rule synthesis implies that sygus stream must be true + opts.quantifiers.sygusStream = true; + } + if (opts.quantifiers.sygusStream || opts.base.incrementalSolving) + { + // Streaming and incremental mode are incompatible with techniques that + // focus the search towards finding a single solution. + reqBasicSygus = true; + } + // Now, disable options for non-basic sygus algorithms, if necessary. + if (reqBasicSygus) + { + if (!opts.quantifiers.sygusUnifPbeWasSetByUser) + { + opts.quantifiers.sygusUnifPbe = false; + } + if (opts.quantifiers.sygusUnifPiWasSetByUser) + { + opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE; + } + if (!opts.quantifiers.sygusInvTemplModeWasSetByUser) + { + opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE; + } + if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser) + { + opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE; + } + } + if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) + { + opts.datatypes.dtRewriteErrorSel = true; + } + // do not miniscope + if (!opts.quantifiers.miniscopeQuantWasSetByUser) + { + opts.quantifiers.miniscopeQuant = false; + } + if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser) + { + opts.quantifiers.miniscopeQuantFreeVar = false; + } + if (!opts.quantifiers.quantSplitWasSetByUser) + { + opts.quantifiers.quantSplit = false; + } + // do not do macros + if (!opts.quantifiers.macrosQuantWasSetByUser) + { + opts.quantifiers.macrosQuant = false; + } + // use tangent planes by default, since we want to put effort into + // the verification step for sygus queries with non-linear arithmetic + if (!opts.arith.nlExtTangentPlanesWasSetByUser) + { + opts.arith.nlExtTangentPlanes = true; + } +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 22e271c72..99db64b4a 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -23,19 +23,42 @@ namespace cvc5 { namespace smt { /** - * The purpose of this method is to set the default options and update the logic - * info for an SMT engine. - * - * @param logic A reference to the logic of SmtEngine, which can be - * updated by this method based on the current options and the logic itself. - * @param isInternalSubsolver Whether we are setting the options for an - * internal subsolver (see SmtEngine::isInternalSubsolver). - * - * NOTE: we currently modify the current options in scope. This method - * can be further refactored to modify an options object provided as an - * explicit argument. + * Class responsible for setting default options, which includes managing + * implied options and dependencies between the options and the logic. */ -void setDefaults(LogicInfo& logic, Options& opts, bool isInternalSubsolver); +class SetDefaults +{ + public: + /** + * @param isInternalSubsolver Whether we are setting the options for an + * internal subsolver (see SmtEngine::isInternalSubsolver). + */ + SetDefaults(bool isInternalSubsolver); + /** + * The purpose of this method is to set the default options and update the + * logic info for an SMT engine. + * + * @param logic A reference to the logic of SmtEngine, which can be + * updated by this method based on the current options and the logic itself. + * @param opts The options to modify, typically the main options of the + * SmtEngine in scope. + */ + void setDefaults(LogicInfo& logic, Options& opts); + + private: + /** + * Widen logic to theories that are required, since some theories imply the + * use of other theories to handle certain operators, e.g. UF to handle + * partial functions. + */ + void widenLogic(LogicInfo& logic, Options& opts); + /** + * Set defaults related to SyGuS, called when SyGuS is enabled. + */ + void setDefaultsSygus(Options& opts); + /** Are we an internal subsolver? */ + bool d_isInternalSubsolver; +}; } // namespace smt } // namespace cvc5 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5f3920929..3e4c1efa7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -49,10 +49,10 @@ #include "smt/model_blocker.h" #include "smt/model_core_builder.h" #include "smt/node_command.h" -#include "smt/options_manager.h" #include "smt/preprocessor.h" #include "smt/proof_manager.h" #include "smt/quant_elim_solver.h" +#include "smt/set_defaults.h" #include "smt/smt_engine_scope.h" #include "smt/smt_engine_state.h" #include "smt/smt_engine_stats.h" @@ -103,7 +103,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) d_isInternalSubsolver(false), d_stats(nullptr), d_outMgr(this), - d_optm(nullptr), d_pp(nullptr), d_scope(nullptr) { @@ -120,8 +119,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // On the other hand, this hack breaks use cases where multiple SmtEngine // objects are created by the user. d_scope.reset(new SmtScope(this)); - // set the options manager - d_optm.reset(new smt::OptionsManager(&getOptions())); // listen to node manager events getNodeManager()->subscribeEvents(d_snmListener.get()); // listen to resource out @@ -195,10 +192,10 @@ void SmtEngine::finishInit() // set the random seed Random::getRandom().setSeed(d_env->getOptions().driver.seed); - // Call finish init on the options manager. This inializes the resource - // manager based on the options, and sets up the best default options - // based on our heuristics. - d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver); + // Call finish init on the set defaults module. This inializes the logic + // and the best default options based on our heuristics. + SetDefaults sdefaults(d_isInternalSubsolver); + sdefaults.setDefaults(d_env->d_logic, getOptions()); ProofNodeManager* pnm = nullptr; if (d_env->getOptions().smt.produceProofs) @@ -324,7 +321,6 @@ SmtEngine::~SmtEngine() getNodeManager()->unsubscribeEvents(d_snmListener.get()); d_snmListener.reset(nullptr); d_routListener.reset(nullptr); - d_optm.reset(nullptr); d_pp.reset(nullptr); // destroy the state d_state.reset(nullptr); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d00fa0c76..f42d791e2 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1111,12 +1111,6 @@ class CVC5_EXPORT SmtEngine /** the output manager for commands */ mutable OutputManager d_outMgr; - /** - * The options manager, which is responsible for implementing core options - * such as those related to time outs and printing. It is also responsible - * for set default options based on the logic. - */ - std::unique_ptr d_optm; /** * The preprocessor. */ -- cgit v1.2.3 From c783a90bc4dbf43a2d054a4e04ae0cae280bea30 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Aug 2021 00:24:39 -0500 Subject: Improve conversion to skolems in expression miner (#7019) Work towards a new expression miner for caching satisfiability queries. --- src/theory/quantifiers/expr_miner.cpp | 37 +++++++++-------------------------- src/theory/quantifiers/expr_miner.h | 8 +++++--- 2 files changed, 14 insertions(+), 31 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 72605e9d1..0f46fa790 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -38,38 +38,19 @@ void ExprMiner::initialize(const std::vector& vars, SygusSampler* ss) Node ExprMiner::convertToSkolem(Node n) { - std::vector fvs; - TermUtil::computeVarContains(n, fvs); - if (fvs.empty()) + if (d_skolems.empty()) { - return n; - } - std::vector sfvs; - std::vector sks; - // map to skolems - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - for (unsigned i = 0, size = fvs.size(); i < size; i++) - { - Node v = fvs[i]; - // only look at the sampler variables - if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end()) + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + for (const Node& v : d_vars) { - sfvs.push_back(v); - std::map::iterator itf = d_fv_to_skolem.find(v); - if (itf == d_fv_to_skolem.end()) - { - Node sk = sm->mkDummySkolem("rrck", v.getType()); - d_fv_to_skolem[v] = sk; - sks.push_back(sk); - } - else - { - sks.push_back(itf->second); - } + Node sk = sm->mkDummySkolem("rrck", v.getType()); + d_skolems.push_back(sk); + d_fv_to_skolem[v] = sk; } } - return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end()); + return n.substitute( + d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end()); } void ExprMiner::initializeChecker(std::unique_ptr& checker, diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 36fae1549..79d0c6650 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -62,13 +62,15 @@ class ExprMiner protected: /** the set of variables used by this class */ std::vector d_vars; - /** pointer to the sygus sampler object we are using */ - SygusSampler* d_sampler; /** - * Maps to skolems for each free variable that appears in a check. This is + * The set of skolems corresponding to the above variables. These are * used during initializeChecker so that query (which may contain free * variables) is converted to a formula without free variables. */ + std::vector d_skolems; + /** pointer to the sygus sampler object we are using */ + SygusSampler* d_sampler; + /** Maps to skolems for each free variable based on d_vars/d_skolems. */ std::map d_fv_to_skolem; /** convert */ Node convertToSkolem(Node n); -- cgit v1.2.3 From df8caeeb9490ba712744f814ba92916a8ae4ab1e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Aug 2021 00:44:20 -0500 Subject: Cosmetic improvements to theory datatypes (#7020) Mainly just indentation / formatting changes. In preparation for playing around with heuristics to datatypes theory motivated by Facebook benchmarks. --- src/theory/datatypes/theory_datatypes.cpp | 248 ++++++++++++++++-------------- src/theory/datatypes/theory_datatypes.h | 9 +- 2 files changed, 140 insertions(+), 117 deletions(-) (limited to 'src') diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3dfd9b458..2162c4d14 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -58,7 +58,6 @@ TheoryDatatypes::TheoryDatatypes(Env& env, d_collectTermsCacheU(getUserContext()), d_functionTerms(getSatContext()), d_singleton_eq(getUserContext()), - d_lemmas_produced_c(getUserContext()), d_sygusExtension(nullptr), d_state(env, valuation), d_im(*this, d_state, d_pnm), @@ -539,129 +538,151 @@ void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2) } void TheoryDatatypes::merge( Node t1, Node t2 ){ - if (!d_state.isInConflict()) + if (d_state.isInConflict()) { - Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl; - Assert(areEqual(t1, t2)); - TNode trep1 = t1; - TNode trep2 = t2; - EqcInfo* eqc2 = getOrMakeEqcInfo( t2 ); - if( eqc2 ){ - bool checkInst = false; - if( !eqc2->d_constructor.get().isNull() ){ - trep2 = eqc2->d_constructor.get(); - } - EqcInfo* eqc1 = getOrMakeEqcInfo( t1 ); - if( eqc1 ){ - Trace("datatypes-debug") << " merge eqc info " << eqc2 << " into " << eqc1 << std::endl; - if( !eqc1->d_constructor.get().isNull() ){ - trep1 = eqc1->d_constructor.get(); - } - //check for clash - TNode cons1 = eqc1->d_constructor.get(); - TNode cons2 = eqc2->d_constructor.get(); - //if both have constructor, then either clash or unification - if( !cons1.isNull() && !cons2.isNull() ){ - Trace("datatypes-debug") << " constructors : " << cons1 << " " << cons2 << std::endl; - Node unifEq = cons1.eqNode( cons2 ); - std::vector< Node > rew; - if (utils::checkClash(cons1, cons2, rew)) - { - std::vector conf; - conf.push_back(unifEq); - Trace("dt-conflict") - << "CONFLICT: Clash conflict : " << conf << std::endl; - d_im.sendDtConflict(conf, InferenceId::DATATYPES_CLASH_CONFLICT); - return; - } - else - { - Assert(areEqual(cons1, cons2)); - //do unification - for( int i=0; i<(int)cons1.getNumChildren(); i++ ) { - if( !areEqual( cons1[i], cons2[i] ) ){ - Node eq = cons1[i].eqNode( cons2[i] ); - d_im.addPendingInference( - eq, InferenceId::DATATYPES_UNIF, unifEq); - Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl; - } - } - } - } - Trace("datatypes-debug") << " instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl; - eqc1->d_inst = eqc1->d_inst || eqc2->d_inst; - if( !cons2.isNull() ){ - if( cons1.isNull() ){ - Trace("datatypes-debug") << " must check if it is okay to set the constructor." << std::endl; - checkInst = true; - addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); - if (d_state.isInConflict()) - { - return; - } - } - } - }else{ - Trace("datatypes-debug") << " no eqc info for " << t1 << ", must create" << std::endl; - //just copy the equivalence class information - eqc1 = getOrMakeEqcInfo( t1, true ); - eqc1->d_inst.set( eqc2->d_inst ); - eqc1->d_constructor.set( eqc2->d_constructor ); - eqc1->d_selectors.set( eqc2->d_selectors ); + return; + } + Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl; + Assert(areEqual(t1, t2)); + TNode trep1 = t1; + TNode trep2 = t2; + EqcInfo* eqc2 = getOrMakeEqcInfo(t2); + if (eqc2 == nullptr) + { + return; + } + bool checkInst = false; + if (!eqc2->d_constructor.get().isNull()) + { + trep2 = eqc2->d_constructor.get(); + } + EqcInfo* eqc1 = getOrMakeEqcInfo(t1); + if (eqc1) + { + Trace("datatypes-debug") + << " merge eqc info " << eqc2 << " into " << eqc1 << std::endl; + if (!eqc1->d_constructor.get().isNull()) + { + trep1 = eqc1->d_constructor.get(); + } + // check for clash + TNode cons1 = eqc1->d_constructor.get(); + TNode cons2 = eqc2->d_constructor.get(); + // if both have constructor, then either clash or unification + if (!cons1.isNull() && !cons2.isNull()) + { + Trace("datatypes-debug") + << " constructors : " << cons1 << " " << cons2 << std::endl; + Node unifEq = cons1.eqNode(cons2); + std::vector rew; + if (utils::checkClash(cons1, cons2, rew)) + { + std::vector conf; + conf.push_back(unifEq); + Trace("dt-conflict") + << "CONFLICT: Clash conflict : " << conf << std::endl; + d_im.sendDtConflict(conf, InferenceId::DATATYPES_CLASH_CONFLICT); + return; } - - - //merge labels - NodeUIntMap::iterator lbl_i = d_labels.find(t2); - if( lbl_i != d_labels.end() ){ - Trace("datatypes-debug") << " merge labels from " << eqc2 << " " << t2 << std::endl; - size_t n_label = (*lbl_i).second; - for (size_t i = 0; i < n_label; i++) + else + { + Assert(areEqual(cons1, cons2)); + // do unification + for (size_t i = 0, nchild = cons1.getNumChildren(); i < nchild; i++) { - Assert(i < d_labels_data[t2].size()); - Node t = d_labels_data[ t2 ][i]; - Node t_arg = d_labels_args[t2][i]; - unsigned tindex = d_labels_tindex[t2][i]; - addTester( tindex, t, eqc1, t1, t_arg ); - if (d_state.isInConflict()) + if (!areEqual(cons1[i], cons2[i])) { - Trace("datatypes-debug") << " conflict!" << std::endl; - return; + Node eq = cons1[i].eqNode(cons2[i]); + d_im.addPendingInference(eq, InferenceId::DATATYPES_UNIF, unifEq); + Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " + << unifEq << std::endl; } } - } - //merge selectors - if( !eqc1->d_selectors && eqc2->d_selectors ){ - eqc1->d_selectors = true; + } + Trace("datatypes-debug") << " instantiated : " << eqc1->d_inst << " " + << eqc2->d_inst << std::endl; + eqc1->d_inst = eqc1->d_inst || eqc2->d_inst; + if (!cons2.isNull()) + { + if (cons1.isNull()) + { + Trace("datatypes-debug") + << " must check if it is okay to set the constructor." + << std::endl; checkInst = true; - } - NodeUIntMap::iterator sel_i = d_selector_apps.find(t2); - if( sel_i != d_selector_apps.end() ){ - Trace("datatypes-debug") << " merge selectors from " << eqc2 << " " << t2 << std::endl; - size_t n_sel = (*sel_i).second; - for (size_t j = 0; j < n_sel; j++) - { - addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() ); - } - } - if( checkInst ){ - Trace("datatypes-debug") << " checking instantiate" << std::endl; - instantiate( eqc1, t1 ); + addConstructor(eqc2->d_constructor.get(), eqc1, t1); if (d_state.isInConflict()) { return; } } } - Trace("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl; } + else + { + Trace("datatypes-debug") + << " no eqc info for " << t1 << ", must create" << std::endl; + // just copy the equivalence class information + eqc1 = getOrMakeEqcInfo(t1, true); + eqc1->d_inst.set(eqc2->d_inst); + eqc1->d_constructor.set(eqc2->d_constructor); + eqc1->d_selectors.set(eqc2->d_selectors); + } + + // merge labels + NodeUIntMap::iterator lbl_i = d_labels.find(t2); + if (lbl_i != d_labels.end()) + { + Trace("datatypes-debug") + << " merge labels from " << eqc2 << " " << t2 << std::endl; + size_t n_label = (*lbl_i).second; + for (size_t i = 0; i < n_label; i++) + { + Assert(i < d_labels_data[t2].size()); + Node t = d_labels_data[t2][i]; + Node t_arg = d_labels_args[t2][i]; + unsigned tindex = d_labels_tindex[t2][i]; + addTester(tindex, t, eqc1, t1, t_arg); + if (d_state.isInConflict()) + { + Trace("datatypes-debug") << " conflict!" << std::endl; + return; + } + } + } + // merge selectors + if (!eqc1->d_selectors && eqc2->d_selectors) + { + eqc1->d_selectors = true; + checkInst = true; + } + NodeUIntMap::iterator sel_i = d_selector_apps.find(t2); + if (sel_i != d_selector_apps.end()) + { + Trace("datatypes-debug") + << " merge selectors from " << eqc2 << " " << t2 << std::endl; + size_t n_sel = (*sel_i).second; + for (size_t j = 0; j < n_sel; j++) + { + addSelector(d_selector_apps_data[t2][j], + eqc1, + t1, + eqc2->d_constructor.get().isNull()); + } + } + if (checkInst) + { + Trace("datatypes-debug") << " checking instantiate" << std::endl; + instantiate(eqc1, t1); + } + Trace("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl; } -TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) - : d_inst( c, false ) - , d_constructor( c, Node::null() ) - , d_selectors( c, false ) +TheoryDatatypes::EqcInfo::EqcInfo(context::Context* c) + : d_inst(c, false), + d_constructor(c, Node::null()), + d_selectors(c, false) {} bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){ @@ -823,7 +844,7 @@ void TheoryDatatypes::addTester( const DType& dt = t_arg.getType().getDType(); Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl; if( tpolarity ){ - instantiate( eqc, n ); + instantiate(eqc, n); // We could propagate is-C1(x) => not is-C2(x) here for all other // constructors, but empirically this hurts performance. }else{ @@ -1409,13 +1430,14 @@ Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index) return n_ic; } -void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ +bool TheoryDatatypes::instantiate(EqcInfo* eqc, Node n) +{ Trace("datatypes-debug") << "Instantiate: " << n << std::endl; //add constructor to equivalence class if not done so already int index = getLabelIndex( eqc, n ); if (index == -1 || eqc->d_inst) { - return; + return false; } Node exp; Node tt; @@ -1437,7 +1459,8 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ Node eq; if (tt == tt_cons) { - return; + // not necessary + return false; } eq = tt.eqNode(tt_cons); // Determine if the equality must be sent out as a lemma. Notice that @@ -1460,9 +1483,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ } Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq << " forceLemma = " << forceLemma << std::endl; - d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma); Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl; + d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma); + return true; } void TheoryDatatypes::checkCycles() { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index ecfa6f02a..68dedb6f3 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -158,8 +158,6 @@ private: std::map< TypeNode, Node > d_singleton_lemma[2]; /** Cache for singleton equalities processed */ BoolMap d_singleton_eq; - /** list of all lemmas produced */ - BoolMap d_lemmas_produced_c; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -268,9 +266,10 @@ private: void collectTerms( Node n ); /** get instantiate cons */ Node getInstantiateCons(Node n, const DType& dt, int index); - /** check instantiate */ - void instantiate( EqcInfo* eqc, Node n ); -private: + /** check instantiate, return true if an inference was generated. */ + bool instantiate(EqcInfo* eqc, Node n); + + private: //equality queries bool hasTerm( TNode a ); bool areEqual( TNode a, TNode b ); -- cgit v1.2.3 From d39e1b906b47ef8e953dac297fa0fb565dd040a4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Aug 2021 09:45:23 -0500 Subject: Make theory BV use central eq engine when option is enabled (#7025) --- src/theory/theory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index b774d456a..04bab16e2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -620,7 +620,7 @@ bool Theory::usesCentralEqualityEngine(TheoryId id) } return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS - || id == THEORY_SEP || id == THEORY_ARRAYS; + || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV; } bool Theory::expUsingCentralEqualityEngine(TheoryId id) -- cgit v1.2.3 From cf5376c18d8e4d6b3ed2d7b341279cf65fc16418 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Aug 2021 12:07:00 -0500 Subject: Fix policy for eliminating quantified formulas (#7017) This also consolidates the option strictTriggers into userPatMode. Fixes #6996. --- src/options/quantifiers_options.toml | 11 +++-------- src/smt/set_defaults.cpp | 7 ------- src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 5 ++++- src/theory/quantifiers/ematching/instantiation_engine.cpp | 10 +++++++--- src/theory/quantifiers/quantifiers_attributes.cpp | 3 +-- src/theory/quantifiers/quantifiers_attributes.h | 3 +-- src/theory/quantifiers/quantifiers_rewriter.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2 | 6 ++++++ 9 files changed, 24 insertions(+), 24 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2 (limited to 'src') diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 58632aafc..ad74e4ab9 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -226,14 +226,6 @@ name = "Quantifiers" default = "false" help = "consider ground terms within bodies of quantified formulas for matching" -[[option]] - name = "strictTriggers" - category = "regular" - long = "strict-triggers" - type = "bool" - default = "false" - help = "only instantiate quantifiers with user patterns based on triggers" - [[option]] name = "relevantTriggers" category = "regular" @@ -388,6 +380,9 @@ name = "Quantifiers" [[option.mode.TRUST]] name = "trust" help = "When provided, use only user-provided patterns for a quantified formula." +[[option.mode.STRICT]] + name = "trust" + help = "When provided, use only user-provided patterns for a quantified formula, and do not use any other instantiation techniques." [[option.mode.RESORT]] name = "resort" help = "Use user-provided patterns only after auto-generated patterns saturate." diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 6fd2a3f68..12433d8ac 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1104,13 +1104,6 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) } } // implied options... - if (opts.quantifiers.strictTriggers) - { - if (!opts.quantifiers.userPatternsQuantWasSetByUser) - { - opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST; - } - } if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint) { opts.quantifiers.quantConflictFind = true; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index ab237fc6c..8901ec314 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -111,7 +111,10 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f, int e) { options::UserPatMode upMode = getInstUserPatMode(); - if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST) + // we don't auto-generate triggers if the mode is trust or strict + if (hasUserPatterns(f) + && (upMode == options::UserPatMode::TRUST + || upMode == options::UserPatMode::STRICT)) { return InstStrategyStatus::STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index d490dce83..d9bec820c 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -200,11 +200,15 @@ bool InstantiationEngine::checkCompleteFor( Node q ) { void InstantiationEngine::checkOwnership(Node q) { - if( options::strictTriggers() && q.getNumChildren()==3 ){ + if (options::userPatternsQuant() == options::UserPatMode::STRICT + && q.getNumChildren() == 3) + { //if strict triggers, take ownership of this quantified formula bool hasPat = false; - for( unsigned i=0; i Date: Tue, 17 Aug 2021 12:31:35 -0500 Subject: Refactoring theory-specific variable elimination in quantifiers rewriter (#7026) No behavior changes in this PR, just code reorganization. --- src/theory/quantifiers/quantifiers_rewriter.cpp | 108 ++++++++++++++---------- src/theory/quantifiers/quantifiers_rewriter.h | 24 ++++-- 2 files changed, 81 insertions(+), 51 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index aba2d79bf..02af92887 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -701,9 +701,65 @@ bool QuantifiersRewriter::isVarElim(Node v, Node s) return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType()); } -Node QuantifiersRewriter::getVarElimLitBv(Node lit, - const std::vector& args, - Node& var) +Node QuantifiersRewriter::getVarElimEq(Node lit, + const std::vector& args, + Node& var) +{ + Assert(lit.getKind() == EQUAL); + Node slv; + TypeNode tt = lit[0].getType(); + if (tt.isReal()) + { + slv = getVarElimEqReal(lit, args, var); + } + else if (tt.isBitVector()) + { + slv = getVarElimEqBv(lit, args, var); + } + else if (tt.isStringLike()) + { + slv = getVarElimEqString(lit, args, var); + } + return slv; +} + +Node QuantifiersRewriter::getVarElimEqReal(Node lit, + const std::vector& args, + Node& var) +{ + // for arithmetic, solve the equality + std::map msum; + if (!ArithMSum::getMonomialSumLit(lit, msum)) + { + return Node::null(); + } + std::vector::const_iterator ita; + for (std::map::iterator itm = msum.begin(); itm != msum.end(); + ++itm) + { + if (itm->first.isNull()) + { + continue; + } + ita = std::find(args.begin(), args.end(), itm->first); + if (ita != args.end()) + { + Node veq_c; + Node val; + int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL); + if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val)) + { + var = itm->first; + return val; + } + } + } + return Node::null(); +} + +Node QuantifiersRewriter::getVarElimEqBv(Node lit, + const std::vector& args, + Node& var) { if (Trace.isOn("quant-velim-bv")) { @@ -752,9 +808,9 @@ Node QuantifiersRewriter::getVarElimLitBv(Node lit, return Node::null(); } -Node QuantifiersRewriter::getVarElimLitString(Node lit, - const std::vector& args, - Node& var) +Node QuantifiersRewriter::getVarElimEqString(Node lit, + const std::vector& args, + Node& var) { Assert(lit.getKind() == EQUAL); NodeManager* nm = NodeManager::currentNM(); @@ -900,48 +956,10 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, return true; } } - if (lit.getKind() == EQUAL && lit[0].getType().isReal() && pol) - { - // for arithmetic, solve the equality - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(lit, msum)) - { - for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ - if( !itm->first.isNull() ){ - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first ); - if( ita!=args.end() ){ - Assert(pol); - Node veq_c; - Node val; - int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL); - if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val)) - { - Trace("var-elim-quant") - << "Variable eliminate based on solved equality : " - << itm->first << " -> " << val << std::endl; - vars.push_back(itm->first); - subs.push_back(val); - args.erase(ita); - return true; - } - } - } - } - } - } if (lit.getKind() == EQUAL && pol) { Node var; - Node slv; - TypeNode tt = lit[0].getType(); - if (tt.isBitVector()) - { - slv = getVarElimLitBv(lit, args, var); - } - else if (tt.isStringLike()) - { - slv = getVarElimLitString(lit, args, var); - } + Node slv = getVarElimEq(lit, args, var); if (!slv.isNull()) { Assert(!var.isNull()); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index ae7f75f34..f0c3b0414 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -80,22 +80,34 @@ class QuantifiersRewriter : public TheoryRewriter std::vector& args, std::vector& vars, std::vector& subs); + /** + * Get variable eliminate for an equality based on theory-specific reasoning. + */ + static Node getVarElimEq(Node lit, const std::vector& args, Node& var); + /** variable eliminate for real equalities + * + * If this returns a non-null value ret, then var is updated to a member of + * args, lit is equivalent to ( var = ret ). + */ + static Node getVarElimEqReal(Node lit, + const std::vector& args, + Node& var); /** variable eliminate for bit-vector equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitBv(Node lit, - const std::vector& args, - Node& var); + static Node getVarElimEqBv(Node lit, + const std::vector& args, + Node& var); /** variable eliminate for string equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitString(Node lit, - const std::vector& args, - Node& var); + static Node getVarElimEqString(Node lit, + const std::vector& args, + Node& var); /** get variable elimination * * If n asserted with polarity pol entails a literal lit that corresponds -- cgit v1.2.3 From e8f18dd65c829c3c12158d57e1fc7d2c9dcdcfd4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Aug 2021 12:52:15 -0500 Subject: Make SmtEngineState use Env (#7028) Also moves d_filename to Env. --- src/smt/env.cpp | 4 ++++ src/smt/env.h | 14 +++++++++++ src/smt/smt_engine.cpp | 19 +++++++-------- src/smt/smt_engine_state.cpp | 57 +++++++++++++++++++------------------------- src/smt/smt_engine_state.h | 30 +++++++---------------- src/smt/smt_solver.cpp | 2 +- 6 files changed, 60 insertions(+), 66 deletions(-) (limited to 'src') diff --git a/src/smt/env.cpp b/src/smt/env.cpp index a4e07d2c9..3ec9899ad 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -65,6 +65,8 @@ void Env::setProofNodeManager(ProofNodeManager* pnm) d_topLevelSubs->setProofNodeManager(pnm); } +void Env::setFilename(const std::string& filename) { d_filename = filename; } + void Env::shutdown() { d_rewriter.reset(nullptr); @@ -81,6 +83,8 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; } ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } +const std::string& Env::getFilename() const { return d_filename; } + bool Env::isTheoryProofProducing() const { return d_proofNodeManager != nullptr diff --git a/src/smt/env.h b/src/smt/env.h index fa2fe6ab8..9887aea08 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -82,6 +82,9 @@ class Env */ ProofNodeManager* getProofNodeManager(); + /** Return the input name, or the empty string if not set */ + const std::string& getFilename() const; + /** * Check whether theories should produce proofs as well. Other than whether * the proof node manager is set, theory engine proofs are conditioned on the @@ -133,6 +136,11 @@ class Env /** Set proof node manager if it exists */ void setProofNodeManager(ProofNodeManager* pnm); + /** + * Set that the file name of the current instance is the given string. This + * is used for various purposes (e.g. get-info, SZS status). + */ + void setFilename(const std::string& filename); /* Private shutdown ------------------------------------------------------- */ /** @@ -199,6 +207,12 @@ class Env const Options* d_originalOptions; /** Manager for limiting time and abstract resource usage. */ std::unique_ptr d_resourceManager; + + /** + * The input file name or the name set through (set-info :filename ...), if + * any. + */ + std::string d_filename; }; /* class Env */ } // namespace cvc5 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3e4c1efa7..43177a73a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -86,7 +86,7 @@ namespace cvc5 { SmtEngine::SmtEngine(NodeManager* nm, Options* optr) : d_env(new Env(nm, optr)), - d_state(new SmtEngineState(getContext(), getUserContext(), *this)), + d_state(new SmtEngineState(*d_env.get(), *this)), d_absValues(new AbstractValues(getNodeManager())), d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), d_routListener(new ResourceOutListener(*this)), @@ -381,7 +381,7 @@ LogicInfo SmtEngine::getUserLogicInfo() const void SmtEngine::notifyStartParsing(const std::string& filename) { - d_state->setFilename(filename); + d_env->setFilename(filename); d_env->getStatisticsRegistry().registerValue("driver::filename", filename); // Copy the original options. This is called prior to beginning parsing. @@ -391,7 +391,7 @@ void SmtEngine::notifyStartParsing(const std::string& filename) const std::string& SmtEngine::getFilename() const { - return d_state->getFilename(); + return d_env->getFilename(); } void SmtEngine::setResultStatistic(const std::string& result) { @@ -436,7 +436,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) if (key == "filename") { - d_state->setFilename(value); + d_env->setFilename(value); } else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser) { @@ -728,7 +728,7 @@ void SmtEngine::defineFunctionRec(Node func, Result SmtEngine::quickCheck() { Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; - const std::string& filename = d_state->getFilename(); + const std::string& filename = d_env->getFilename(); return Result( Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); } @@ -944,7 +944,7 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, { printStatisticsDiff(); } - return Result(Result::SAT_UNKNOWN, why, d_state->getFilename()); + return Result(Result::SAT_UNKNOWN, why, d_env->getFilename()); } } @@ -1213,7 +1213,7 @@ Model* SmtEngine::getModel() { } // set the information on the SMT-level model Assert(m != nullptr); - m->d_inputName = d_state->getFilename(); + m->d_inputName = d_env->getFilename(); m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT); return m; } @@ -1603,8 +1603,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { finishInit(); if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { - out << "% SZS output start Proof for " << d_state->getFilename() - << std::endl; + out << "% SZS output start Proof for " << d_env->getFilename() << std::endl; } QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); @@ -1694,7 +1693,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { } if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { - out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; + out << "% SZS output end Proof for " << d_env->getFilename() << std::endl; } } diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index cb0a94123..a61c18384 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -19,17 +19,15 @@ #include "options/base_options.h" #include "options/option_exception.h" #include "options/smt_options.h" +#include "smt/env.h" #include "smt/smt_engine.h" namespace cvc5 { namespace smt { -SmtEngineState::SmtEngineState(context::Context* c, - context::UserContext* u, - SmtEngine& smt) +SmtEngineState::SmtEngineState(Env& env, SmtEngine& smt) : d_smt(smt), - d_context(c), - d_userContext(u), + d_env(env), d_pendingPops(0), d_fullyInited(false), d_queryMade(false), @@ -45,7 +43,7 @@ void SmtEngineState::notifyExpectedStatus(const std::string& status) Assert(status == "sat" || status == "unsat" || status == "unknown") << "SmtEngineState::notifyExpectedStatus: unexpected status string " << status; - d_expectedStatus = Result(status, d_filename); + d_expectedStatus = Result(status, d_env.getFilename()); } void SmtEngineState::notifyResetAssertions() @@ -57,7 +55,7 @@ void SmtEngineState::notifyResetAssertions() } // Remember the global push/pop around everything when beyond Start mode // (see solver execution modes in the SMT-LIB standard) - Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1); + Assert(d_userLevels.size() == 0 && getUserContext()->getLevel() == 1); popto(0); } @@ -158,7 +156,7 @@ void SmtEngineState::shutdown() { doPendingPops(); - while (options::incrementalSolving() && d_userContext->getLevel() > 1) + while (options::incrementalSolving() && getUserContext()->getLevel() > 1) { internalPop(true); } @@ -170,11 +168,6 @@ void SmtEngineState::cleanup() popto(0); } -void SmtEngineState::setFilename(const std::string& filename) -{ - d_filename = filename; -} - void SmtEngineState::userPush() { if (!options::incrementalSolving()) @@ -187,10 +180,10 @@ void SmtEngineState::userPush() // staying symmetric with pop. d_smtMode = SmtMode::ASSERT; - d_userLevels.push_back(d_userContext->getLevel()); + d_userLevels.push_back(getUserContext()->getLevel()); internalPush(); Trace("userpushpop") << "SmtEngineState: pushed to level " - << d_userContext->getLevel() << std::endl; + << getUserContext()->getLevel() << std::endl; } void SmtEngineState::userPop() @@ -212,37 +205,37 @@ void SmtEngineState::userPop() // is no longer in scope!). d_smtMode = SmtMode::ASSERT; - AlwaysAssert(d_userContext->getLevel() > 0); - AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); - while (d_userLevels.back() < d_userContext->getLevel()) + AlwaysAssert(getUserContext()->getLevel() > 0); + AlwaysAssert(d_userLevels.back() < getUserContext()->getLevel()); + while (d_userLevels.back() < getUserContext()->getLevel()) { internalPop(true); } d_userLevels.pop_back(); } - +context::Context* SmtEngineState::getContext() { return d_env.getContext(); } +context::UserContext* SmtEngineState::getUserContext() +{ + return d_env.getUserContext(); +} void SmtEngineState::push() { - d_userContext->push(); - d_context->push(); + getUserContext()->push(); + getContext()->push(); } void SmtEngineState::pop() { - d_userContext->pop(); - d_context->pop(); + getUserContext()->pop(); + getContext()->pop(); } void SmtEngineState::popto(int toLevel) { - d_context->popto(toLevel); - d_userContext->popto(toLevel); + getContext()->popto(toLevel); + getUserContext()->popto(toLevel); } -context::UserContext* SmtEngineState::getUserContext() { return d_userContext; } - -context::Context* SmtEngineState::getContext() { return d_context; } - Result SmtEngineState::getStatus() const { return d_status; } bool SmtEngineState::isFullyInited() const { return d_fullyInited; } @@ -255,8 +248,6 @@ size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); } SmtMode SmtEngineState::getMode() const { return d_smtMode; } -const std::string& SmtEngineState::getFilename() const { return d_filename; } - void SmtEngineState::internalPush() { Assert(d_fullyInited); @@ -266,7 +257,7 @@ void SmtEngineState::internalPush() { // notifies the SmtEngine to process the assertions immediately d_smt.notifyPushPre(); - d_userContext->push(); + getUserContext()->push(); // the context push is done inside of the SAT solver d_smt.notifyPushPost(); } @@ -300,7 +291,7 @@ void SmtEngineState::doPendingPops() // the context pop is done inside of the SAT solver d_smt.notifyPopPre(); // pop the context - d_userContext->pop(); + getUserContext()->pop(); --d_pendingPops; // no need for pop post (for now) } diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index 042efb4de..f20180672 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -27,6 +27,7 @@ namespace cvc5 { class SmtEngine; +class Env; namespace smt { @@ -48,7 +49,7 @@ namespace smt { class SmtEngineState { public: - SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt); + SmtEngineState(Env& env, SmtEngine& smt); ~SmtEngineState() {} /** * Notify that the expected status of the next check-sat is given by the @@ -126,11 +127,6 @@ class SmtEngineState * Cleanup, which pops all contexts to level zero. */ void cleanup(); - /** - * Set that the file name of the current instance is the given string. This - * is used for various purposes (e.g. get-info, SZS status). - */ - void setFilename(const std::string& filename); //---------------------------- context management /** @@ -149,10 +145,6 @@ class SmtEngineState * the SMT-LIB command pop. */ void userPop(); - /** Get a pointer to the UserContext owned by this SmtEngine. */ - context::UserContext* getUserContext(); - /** Get a pointer to the Context owned by this SmtEngine. */ - context::Context* getContext(); //---------------------------- end context management //---------------------------- queries @@ -179,11 +171,13 @@ class SmtEngineState Result getStatus() const; /** Get the SMT mode we are in */ SmtMode getMode() const; - /** return the input name (if any) */ - const std::string& getFilename() const; //---------------------------- end queries private: + /** get the sat context we are using */ + context::Context* getContext(); + /** get the user context we are using */ + context::UserContext* getUserContext(); /** Pushes the user and SAT contexts */ void push(); /** Pops the user and SAT contexts */ @@ -203,10 +197,8 @@ class SmtEngineState void internalPop(bool immediate = false); /** Reference to the SmtEngine */ SmtEngine& d_smt; - /** Expr manager context */ - context::Context* d_context; - /** User level context */ - context::UserContext* d_userContext; + /** Reference to the env of the parent SmtEngine */ + Env& d_env; /** The context levels of user pushes */ std::vector d_userLevels; @@ -253,12 +245,6 @@ class SmtEngineState /** The SMT mode, for details see enumeration above. */ SmtMode d_smtMode; - - /** - * The input file name or the name set through (set-info :filename ...), if - * any. - */ - std::string d_filename; }; } // namespace smt diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 595a3808c..1014b218d 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -133,7 +133,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, Trace("smt") << "SmtSolver::check()" << endl; - const std::string& filename = d_state.getFilename(); + const std::string& filename = d_env.getFilename(); ResourceManager* rm = d_env.getResourceManager(); if (rm->out()) { -- cgit v1.2.3