From 9c49dc9383a6c55a973b1a75e619c296206b12f5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 11 Oct 2021 12:13:46 -0700 Subject: Rename SmtScope to SolverEngineScope. (#7284) --- src/CMakeLists.txt | 4 +- src/preprocessing/passes/sygus_inference.cpp | 2 +- src/preprocessing/preprocessing_pass.cpp | 6 +- src/proof/unsat_core.cpp | 2 +- src/prop/cnf_stream.cpp | 2 +- src/smt/listeners.cpp | 6 +- src/smt/smt_engine_scope.cpp | 67 ------------------ src/smt/smt_engine_scope.h | 62 ---------------- src/smt/smt_statistics_registry.cpp | 4 +- src/smt/smt_statistics_registry.h | 2 +- src/smt/solver_engine.cpp | 82 +++++++++++----------- src/smt/solver_engine.h | 6 +- src/smt/solver_engine_scope.cpp | 68 ++++++++++++++++++ src/smt/solver_engine_scope.h | 61 ++++++++++++++++ src/theory/bv/abstraction.cpp | 2 - src/theory/bv/bitblast/bitblaster.h | 2 +- src/theory/bv/bv_subtheory_algebraic.cpp | 2 +- src/theory/bv/theory_bv_rewrite_rules.h | 2 +- .../quantifiers/candidate_rewrite_database.cpp | 2 +- .../quantifiers/ematching/candidate_generator.cpp | 2 +- src/theory/rewriter.cpp | 9 +-- src/theory/smt_engine_subsolver.cpp | 2 +- src/theory/theory_inference_manager.cpp | 2 +- 23 files changed, 198 insertions(+), 201 deletions(-) delete mode 100644 src/smt/smt_engine_scope.cpp delete mode 100644 src/smt/smt_engine_scope.h create mode 100644 src/smt/solver_engine_scope.cpp create mode 100644 src/smt/solver_engine_scope.h (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 583ce8bc5..61be39f97 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -349,8 +349,8 @@ libcvc5_add_sources( smt/set_defaults.h smt/solver_engine.cpp smt/solver_engine.h - smt/smt_engine_scope.cpp - smt/smt_engine_scope.h + smt/solver_engine_scope.cpp + smt/solver_engine_scope.h smt/smt_engine_state.cpp smt/smt_engine_state.h smt/smt_engine_stats.cpp diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 16ecc2d6a..3da75beb2 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -17,9 +17,9 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 758f119f5..244e551f7 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -21,8 +21,8 @@ #include "smt/dump.h" #include "smt/env.h" #include "smt/output_manager.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine_scope.h" #include "util/statistics_stats.h" namespace cvc5 { @@ -65,9 +65,7 @@ PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext, { } -PreprocessingPass::~PreprocessingPass() { - Assert(smt::smtEngineInScope()); -} +PreprocessingPass::~PreprocessingPass() { Assert(smt::solverEngineInScope()); } } // namespace preprocessing } // namespace cvc5 diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index f7e600fe8..e2e3e85fe 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -19,7 +19,7 @@ #include "expr/expr_iomanip.h" #include "options/base_options.h" #include "printer/printer.h" -#include "smt/smt_engine_scope.h" +#include "smt/solver_engine_scope.h" namespace cvc5 { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e04651fc3..1bac953fd 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -28,8 +28,8 @@ #include "prop/theory_proxy.h" #include "smt/dump.h" #include "smt/env.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine_scope.h" #include "theory/theory.h" #include "theory/theory_engine.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index f10d039b8..de6368951 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -23,8 +23,8 @@ #include "smt/dump.h" #include "smt/dump_manager.h" #include "smt/node_command.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" namespace cvc5 { namespace smt { @@ -33,8 +33,8 @@ ResourceOutListener::ResourceOutListener(SolverEngine& slv) : d_slv(slv) {} void ResourceOutListener::notify() { - SmtScope scope(&d_slv); - Assert(smt::smtEngineInScope()); + SolverEngineScope scope(&d_slv); + Assert(smt::solverEngineInScope()); d_slv.interrupt(); } diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp deleted file mode 100644 index 07a0c1e4c..000000000 --- a/src/smt/smt_engine_scope.cpp +++ /dev/null @@ -1,67 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andres Noetzli, Andrew Reynolds, Morgan Deters - * - * 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. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "smt/smt_engine_scope.h" - -#include "base/check.h" -#include "base/configuration_private.h" -#include "base/output.h" -#include "smt/solver_engine.h" - -namespace cvc5 { -namespace smt { - -thread_local SolverEngine* s_slvEngine_current = nullptr; - -SolverEngine* currentSolverEngine() -{ - Assert(s_slvEngine_current != nullptr); - return s_slvEngine_current; -} - -bool smtEngineInScope() { return s_slvEngine_current != nullptr; } - -ResourceManager* currentResourceManager() -{ - return s_slvEngine_current->getResourceManager(); -} - -SmtScope::SmtScope(const SolverEngine* smt) - : d_oldSlvEngine(s_slvEngine_current), - d_optionsScope(smt ? &const_cast(smt)->getOptions() - : nullptr) -{ - Assert(smt != nullptr); - s_slvEngine_current = const_cast(smt); - Debug("current") << "smt scope: " << s_slvEngine_current << std::endl; -} - -SmtScope::~SmtScope() { - s_slvEngine_current = d_oldSlvEngine; - Debug("current") << "smt scope: returning to " << s_slvEngine_current - << std::endl; -} - -StatisticsRegistry& SmtScope::currentStatisticsRegistry() -{ - Assert(smtEngineInScope()); - return s_slvEngine_current->getStatisticsRegistry(); -} - -} // namespace smt -} // namespace cvc5 diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h deleted file mode 100644 index a4c1f0eaf..000000000 --- a/src/smt/smt_engine_scope.h +++ /dev/null @@ -1,62 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Andres Noetzli, Tim King - * - * 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. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "cvc5_private.h" - -#ifndef CVC5__SMT__SMT_ENGINE_SCOPE_H -#define CVC5__SMT__SMT_ENGINE_SCOPE_H - -#include "expr/node_manager.h" - -#include "options/options.h" - -namespace cvc5 { - -class SolverEngine; -class StatisticsRegistry; - -namespace smt { - -SolverEngine* currentSolverEngine(); -bool smtEngineInScope(); - -/** get the current resource manager */ -ResourceManager* currentResourceManager(); - -class SmtScope -{ - public: - SmtScope(const SolverEngine* smt); - ~SmtScope(); - /** - * This returns the StatisticsRegistry attached to the currently in scope - * SolverEngine. - */ - static StatisticsRegistry& currentStatisticsRegistry(); - - private: - /** The old SolverEngine, to be restored on destruction. */ - SolverEngine* d_oldSlvEngine; - /** Options scope */ - Options::OptionsScope d_optionsScope; -};/* class SmtScope */ - -} // namespace smt -} // namespace cvc5 - -#endif /* CVC5__SMT__SMT_ENGINE_SCOPE_H */ diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp index 1c948df60..74f60ba75 100644 --- a/src/smt/smt_statistics_registry.cpp +++ b/src/smt/smt_statistics_registry.cpp @@ -15,14 +15,14 @@ #include "smt/smt_statistics_registry.h" -#include "smt/smt_engine_scope.h" +#include "smt/solver_engine_scope.h" #include "util/statistics_stats.h" namespace cvc5 { StatisticsRegistry& smtStatisticsRegistry() { - return smt::SmtScope::currentStatisticsRegistry(); + return smt::SolverEngineScope::currentStatisticsRegistry(); } } // namespace cvc5 diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index 66e8b522d..d2b598209 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -25,7 +25,7 @@ namespace cvc5 { /** * This returns the StatisticsRegistry attached to the currently in scope * SolverEngine. This is a synonym for - * smt::SmtScope::currentStatisticsRegistry(). + * smt::SolverEngineScope::currentStatisticsRegistry(). */ StatisticsRegistry& smtStatisticsRegistry(); diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 52f47f037..4c8ec4ff2 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -53,10 +53,10 @@ #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" #include "smt/smt_solver.h" +#include "smt/solver_engine_scope.h" #include "smt/sygus_solver.h" #include "smt/unsat_core_manager.h" #include "theory/quantifiers/instantiation_list.h" @@ -115,7 +115,7 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) // SolverEngine. Thus the hack here does not break this use case. On the other // hand, this hack breaks use cases where multiple SolverEngine objects are // created by the user. - d_scope.reset(new SmtScope(this)); + d_scope.reset(new SolverEngineScope(this)); // listen to node manager events getNodeManager()->subscribeEvents(d_snmListener.get()); // listen to resource out @@ -276,7 +276,7 @@ void SolverEngine::shutdown() SolverEngine::~SolverEngine() { - SmtScope smts(this); + SolverEngineScope smts(this); try { @@ -318,7 +318,7 @@ SolverEngine::~SolverEngine() void SolverEngine::setLogic(const LogicInfo& logic) { - SmtScope smts(this); + SolverEngineScope smts(this); if (d_state->isFullyInited()) { throw ModalException( @@ -332,7 +332,7 @@ void SolverEngine::setLogic(const LogicInfo& logic) void SolverEngine::setLogic(const std::string& s) { - SmtScope smts(this); + SolverEngineScope smts(this); try { setLogic(LogicInfo(s)); @@ -370,7 +370,7 @@ void SolverEngine::setLogicInternal() void SolverEngine::setInfo(const std::string& key, const std::string& value) { - SmtScope smts(this); + SolverEngineScope smts(this); Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; @@ -429,7 +429,7 @@ bool SolverEngine::isValidGetInfoFlag(const std::string& key) const std::string SolverEngine::getInfo(const std::string& key) const { - SmtScope smts(this); + SolverEngineScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; if (key == "all-statistics") @@ -572,7 +572,7 @@ void SolverEngine::defineFunction(Node func, Node formula, bool global) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); Trace("smt") << "SMT defineFunction(" << func << ")" << endl; @@ -610,7 +610,7 @@ void SolverEngine::defineFunctionsRec( const std::vector& formulas, bool global) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); Trace("smt") << "SMT defineFunctionsRec(...)" << endl; @@ -843,7 +843,7 @@ Result SolverEngine::checkSatInternal(const std::vector& assumptions, { try { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); Trace("smt") << "SolverEngine::" @@ -921,7 +921,7 @@ Result SolverEngine::checkSatInternal(const std::vector& assumptions, std::vector SolverEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; - SmtScope smts(this); + SolverEngineScope smts(this); if (!d_env->getOptions().smt.unsatAssumptions) { throw ModalException( @@ -954,7 +954,7 @@ std::vector SolverEngine::getUnsatAssumptions(void) Result SolverEngine::assertFormula(const Node& formula) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); @@ -975,7 +975,7 @@ Result SolverEngine::assertFormula(const Node& formula) void SolverEngine::declareSygusVar(Node var) { - SmtScope smts(this); + SolverEngineScope smts(this); d_sygusSolver->declareSygusVar(var); } @@ -984,7 +984,7 @@ void SolverEngine::declareSynthFun(Node func, bool isInv, const std::vector& vars) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars); @@ -1000,7 +1000,7 @@ void SolverEngine::declareSynthFun(Node func, void SolverEngine::assertSygusConstraint(Node n, bool isAssume) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_sygusSolver->assertSygusConstraint(n, isAssume); } @@ -1010,14 +1010,14 @@ void SolverEngine::assertSygusInvConstraint(Node inv, Node trans, Node post) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); } Result SolverEngine::checkSynth() { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); return d_sygusSolver->checkSynth(*d_asserts); } @@ -1039,7 +1039,7 @@ void SolverEngine::declarePool(const Node& p, Node SolverEngine::simplify(const Node& ex) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); // ensure we've processed assertions @@ -1050,7 +1050,7 @@ Node SolverEngine::simplify(const Node& ex) Node SolverEngine::expandDefinitions(const Node& ex) { getResourceManager()->spendResource(Resource::PreprocessStep); - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); return d_smtSolver->getPreprocessor()->expandDefinitions(ex); @@ -1059,7 +1059,7 @@ Node SolverEngine::expandDefinitions(const Node& ex) // TODO(#1108): Simplify the error reporting of this method. Node SolverEngine::getValue(const Node& ex) const { - SmtScope smts(this); + SolverEngineScope smts(this); Trace("smt") << "SMT getValue(" << ex << ")" << endl; if (Dump.isOn("benchmark")) @@ -1132,7 +1132,7 @@ std::vector SolverEngine::getModelDomainElements(TypeNode tn) const bool SolverEngine::isModelCoreSymbol(Node n) { - SmtScope smts(this); + SolverEngineScope smts(this); Assert(n.isVar()); const Options& opts = d_env->getOptions(); if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE) @@ -1159,7 +1159,7 @@ bool SolverEngine::isModelCoreSymbol(Node n) std::string SolverEngine::getModel(const std::vector& declaredSorts, const std::vector& declaredFuns) { - SmtScope smts(this); + SolverEngineScope smts(this); // !!! Note that all methods called here should have a version at the API // level. This is to ensure that the information associated with a model is // completely accessible by the user. This is currently not rigorously @@ -1204,7 +1204,7 @@ std::string SolverEngine::getModel(const std::vector& declaredSorts, Result SolverEngine::blockModel() { Trace("smt") << "SMT blockModel()" << endl; - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); @@ -1233,7 +1233,7 @@ Result SolverEngine::blockModel() Result SolverEngine::blockModelValues(const std::vector& exprs) { Trace("smt") << "SMT blockModelValues()" << endl; - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); @@ -1303,7 +1303,7 @@ void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT) "Cannot declare heap if not using the separation logic theory."; throw RecoverableModalException(msg); } - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); TheoryEngine* te = getTheoryEngine(); te->declareSepHeap(locT, dataT); @@ -1311,7 +1311,7 @@ void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT) bool SolverEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); TheoryEngine* te = getTheoryEngine(); return te->getSepHeapTypes(locT, dataT); @@ -1535,7 +1535,7 @@ void SolverEngine::checkModel(bool hardFailure) UnsatCore SolverEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << std::endl; - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); if (Dump.isOn("benchmark")) { @@ -1560,7 +1560,7 @@ void SolverEngine::getRelevantInstantiationTermVectors( std::string SolverEngine::getProof() { Trace("smt") << "SMT getProof()\n"; - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); if (Dump.isOn("benchmark")) { @@ -1588,7 +1588,7 @@ std::string SolverEngine::getProof() void SolverEngine::printInstantiations(std::ostream& out) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); @@ -1682,7 +1682,7 @@ void SolverEngine::printInstantiations(std::ostream& out) void SolverEngine::getInstantiationTermVectors( std::map>>& insts) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); QuantifiersEngine* qe = getAvailableQuantifiersEngine("getInstantiationTermVectors"); @@ -1692,14 +1692,14 @@ void SolverEngine::getInstantiationTermVectors( bool SolverEngine::getSynthSolutions(std::map& solMap) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); return d_sygusSolver->getSynthSolutions(solMap); } Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); const LogicInfo& logic = getLogicInfo(); if (!logic.isPure(THEORY_ARITH) && strict) @@ -1715,7 +1715,7 @@ bool SolverEngine::getInterpol(const Node& conj, const TypeNode& grammarType, Node& interpol) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); std::vector axioms = getExpandedAssertions(); bool success = @@ -1736,7 +1736,7 @@ bool SolverEngine::getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); std::vector axioms = getExpandedAssertions(); bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd); @@ -1754,7 +1754,7 @@ bool SolverEngine::getAbduct(const Node& conj, Node& abd) void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) { - SmtScope smts(this); + SolverEngineScope smts(this); QuantifiersEngine* qe = getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas"); qe->getInstantiatedQuantifiedFormulas(qs); @@ -1763,7 +1763,7 @@ void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) void SolverEngine::getInstantiationTermVectors( Node q, std::vector>& tvecs) { - SmtScope smts(this); + SolverEngineScope smts(this); QuantifiersEngine* qe = getAvailableQuantifiersEngine("getInstantiationTermVectors"); qe->getInstantiationTermVectors(q, tvecs); @@ -1771,7 +1771,7 @@ void SolverEngine::getInstantiationTermVectors( std::vector SolverEngine::getAssertions() { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); if (Dump.isOn("benchmark")) @@ -1792,7 +1792,7 @@ std::vector SolverEngine::getAssertions() void SolverEngine::getDifficultyMap(std::map& dmap) { Trace("smt") << "SMT getDifficultyMap()\n"; - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); if (Dump.isOn("benchmark")) { @@ -1814,7 +1814,7 @@ void SolverEngine::getDifficultyMap(std::map& dmap) void SolverEngine::push() { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); Trace("smt") << "SMT push()" << endl; @@ -1828,7 +1828,7 @@ void SolverEngine::push() void SolverEngine::pop() { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); Trace("smt") << "SMT pop()" << endl; if (Dump.isOn("benchmark")) @@ -1850,7 +1850,7 @@ void SolverEngine::pop() void SolverEngine::resetAssertions() { - SmtScope smts(this); + SolverEngineScope smts(this); if (!d_state->isFullyInited()) { diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 0cb83cb0b..8ec0b15f3 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -94,7 +94,7 @@ class InterpolationSolver; class QuantElimSolver; struct SmtEngineStatistics; -class SmtScope; +class SolverEngineScope; class PfManager; class UnsatCoreManager; @@ -114,7 +114,7 @@ class CVC5_EXPORT SolverEngine { friend class ::cvc5::api::Solver; friend class ::cvc5::smt::SmtEngineState; - friend class ::cvc5::smt::SmtScope; + friend class ::cvc5::smt::SolverEngineScope; /* ....................................................................... */ public: @@ -1111,7 +1111,7 @@ class CVC5_EXPORT SolverEngine * SolverEngine in scope. It says the SolverEngine in scope until it is * destructed, or another SolverEngine is created. */ - std::unique_ptr d_scope; + std::unique_ptr d_scope; }; /* class SolverEngine */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/solver_engine_scope.cpp b/src/smt/solver_engine_scope.cpp new file mode 100644 index 000000000..6b12e4f74 --- /dev/null +++ b/src/smt/solver_engine_scope.cpp @@ -0,0 +1,68 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Andrew Reynolds, Morgan Deters + * + * 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ + +#include "smt/solver_engine_scope.h" + +#include "base/check.h" +#include "base/configuration_private.h" +#include "base/output.h" +#include "smt/solver_engine.h" + +namespace cvc5 { +namespace smt { + +thread_local SolverEngine* s_slvEngine_current = nullptr; + +SolverEngine* currentSolverEngine() +{ + Assert(s_slvEngine_current != nullptr); + return s_slvEngine_current; +} + +bool solverEngineInScope() { return s_slvEngine_current != nullptr; } + +ResourceManager* currentResourceManager() +{ + return s_slvEngine_current->getResourceManager(); +} + +SolverEngineScope::SolverEngineScope(const SolverEngine* smt) + : d_oldSlvEngine(s_slvEngine_current), + d_optionsScope(smt ? &const_cast(smt)->getOptions() + : nullptr) +{ + Assert(smt != nullptr); + s_slvEngine_current = const_cast(smt); + Debug("current") << "smt scope: " << s_slvEngine_current << std::endl; +} + +SolverEngineScope::~SolverEngineScope() +{ + s_slvEngine_current = d_oldSlvEngine; + Debug("current") << "smt scope: returning to " << s_slvEngine_current + << std::endl; +} + +StatisticsRegistry& SolverEngineScope::currentStatisticsRegistry() +{ + Assert(solverEngineInScope()); + return s_slvEngine_current->getStatisticsRegistry(); +} + +} // namespace smt +} // namespace cvc5 diff --git a/src/smt/solver_engine_scope.h b/src/smt/solver_engine_scope.h new file mode 100644 index 000000000..309321dc3 --- /dev/null +++ b/src/smt/solver_engine_scope.h @@ -0,0 +1,61 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Tim King + * + * 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ + +#include "cvc5_private.h" + +#ifndef CVC5__SMT__SOLVER_ENGINE_SCOPE_H +#define CVC5__SMT__SOLVER_ENGINE_SCOPE_H + +#include "expr/node_manager.h" +#include "options/options.h" + +namespace cvc5 { + +class SolverEngine; +class StatisticsRegistry; + +namespace smt { + +SolverEngine* currentSolverEngine(); +bool solverEngineInScope(); + +/** get the current resource manager */ +ResourceManager* currentResourceManager(); + +class SolverEngineScope +{ + public: + SolverEngineScope(const SolverEngine* smt); + ~SolverEngineScope(); + /** + * This returns the StatisticsRegistry attached to the currently in scope + * SolverEngine. + */ + static StatisticsRegistry& currentStatisticsRegistry(); + + private: + /** The old SolverEngine, to be restored on destruction. */ + SolverEngine* d_oldSlvEngine; + /** Options scope */ + Options::OptionsScope d_optionsScope; +}; /* class SolverEngineScope */ + +} // namespace smt +} // namespace cvc5 + +#endif /* CVC5__SMT__SMT_ENGINE_SCOPE_H */ diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 1c4633b5a..3d25f19d6 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -19,9 +19,7 @@ #include "options/bv_options.h" #include "printer/printer.h" #include "smt/dump.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "smt/solver_engine.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 17c233789..0471f11e5 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -28,7 +28,7 @@ #include "prop/registrar.h" #include "prop/sat_solver.h" #include "prop/sat_solver_types.h" -#include "smt/smt_engine_scope.h" +#include "smt/solver_engine_scope.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" #include "theory/rewriter.h" #include "theory/theory.h" diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 27afdbbaa..e607444c2 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -20,9 +20,9 @@ #include "options/bv_options.h" #include "printer/printer.h" #include "smt/dump.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "smt_util/boolean_simplification.h" #include "theory/bv/bv_quick_check.h" #include "theory/bv/bv_solver_layered.h" diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 638c2aa26..f893c89d7 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -25,8 +25,8 @@ #include "context/context.h" #include "printer/printer.h" #include "smt/dump.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" #include "util/statistics_stats.h" diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index eda56ef52..3b4babe75 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -17,9 +17,9 @@ #include "options/base_options.h" #include "printer/printer.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index f891b0e99..583a70e3d 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -18,8 +18,8 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "options/quantifiers_options.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_state.h" diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 4c23db9bc..234b3d142 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -17,9 +17,9 @@ #include "options/theory_options.h" #include "proof/conv_proof_generator.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "theory/builtin/proof_checker.h" #include "theory/evaluator.h" #include "theory/quantifiers/extended_rewrite.h" @@ -197,13 +197,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, rewriteStack.push_back(RewriteStackElement(node, theoryId)); ResourceManager* rm = NULL; - bool hasSmtEngine = smt::smtEngineInScope(); - if (hasSmtEngine) { + bool hasSlvEngine = smt::solverEngineInScope(); + if (hasSlvEngine) + { rm = smt::currentResourceManager(); } // Rewrite until the stack is empty for (;;){ - if (hasSmtEngine) + if (hasSlvEngine) { rm->spendResource(Resource::RewriteStep); } diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index fb0a2dbda..99e3f7768 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -17,8 +17,8 @@ #include "theory/smt_engine_subsolver.h" #include "smt/env.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "theory/rewriter.h" namespace cvc5 { diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 08d713b0f..5fc946147 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -15,8 +15,8 @@ #include "theory/theory_inference_manager.h" -#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "smt/solver_engine_scope.h" #include "theory/output_channel.h" #include "theory/rewriter.h" #include "theory/theory.h" -- cgit v1.2.3