diff options
27 files changed, 89 insertions, 92 deletions
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_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<Node>& 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<Node>& assumptions, { try { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); Trace("smt") << "SolverEngine::" @@ -921,7 +921,7 @@ Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions, std::vector<Node> 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<Node> 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<Node>& 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<Node> 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<TypeNode>& declaredSorts, const std::vector<Node>& 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<TypeNode>& 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<Node>& 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<Node, std::vector<std::vector<Node>>>& insts) { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); QuantifiersEngine* qe = getAvailableQuantifiersEngine("getInstantiationTermVectors"); @@ -1692,14 +1692,14 @@ void SolverEngine::getInstantiationTermVectors( bool SolverEngine::getSynthSolutions(std::map<Node, Node>& 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<Node> 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<Node> 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<Node>& qs) { - SmtScope smts(this); + SolverEngineScope smts(this); QuantifiersEngine* qe = getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas"); qe->getInstantiatedQuantifiedFormulas(qs); @@ -1763,7 +1763,7 @@ void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) void SolverEngine::getInstantiationTermVectors( Node q, std::vector<std::vector<Node>>& tvecs) { - SmtScope smts(this); + SolverEngineScope smts(this); QuantifiersEngine* qe = getAvailableQuantifiersEngine("getInstantiationTermVectors"); qe->getInstantiationTermVectors(q, tvecs); @@ -1771,7 +1771,7 @@ void SolverEngine::getInstantiationTermVectors( std::vector<Node> SolverEngine::getAssertions() { - SmtScope smts(this); + SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); if (Dump.isOn("benchmark")) @@ -1792,7 +1792,7 @@ std::vector<Node> SolverEngine::getAssertions() void SolverEngine::getDifficultyMap(std::map<Node, Node>& 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<Node, Node>& 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<smt::SmtScope> d_scope; + std::unique_ptr<smt::SolverEngineScope> d_scope; }; /* class SolverEngine */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/solver_engine_scope.cpp index 07a0c1e4c..6b12e4f74 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/solver_engine_scope.cpp @@ -16,7 +16,7 @@ * \todo document this file */ -#include "smt/smt_engine_scope.h" +#include "smt/solver_engine_scope.h" #include "base/check.h" #include "base/configuration_private.h" @@ -34,14 +34,14 @@ SolverEngine* currentSolverEngine() return s_slvEngine_current; } -bool smtEngineInScope() { return s_slvEngine_current != nullptr; } +bool solverEngineInScope() { return s_slvEngine_current != nullptr; } ResourceManager* currentResourceManager() { return s_slvEngine_current->getResourceManager(); } -SmtScope::SmtScope(const SolverEngine* smt) +SolverEngineScope::SolverEngineScope(const SolverEngine* smt) : d_oldSlvEngine(s_slvEngine_current), d_optionsScope(smt ? &const_cast<SolverEngine*>(smt)->getOptions() : nullptr) @@ -51,15 +51,16 @@ SmtScope::SmtScope(const SolverEngine* smt) Debug("current") << "smt scope: " << s_slvEngine_current << std::endl; } -SmtScope::~SmtScope() { +SolverEngineScope::~SolverEngineScope() +{ s_slvEngine_current = d_oldSlvEngine; Debug("current") << "smt scope: returning to " << s_slvEngine_current << std::endl; } -StatisticsRegistry& SmtScope::currentStatisticsRegistry() +StatisticsRegistry& SolverEngineScope::currentStatisticsRegistry() { - Assert(smtEngineInScope()); + Assert(solverEngineInScope()); return s_slvEngine_current->getStatisticsRegistry(); } diff --git a/src/smt/smt_engine_scope.h b/src/smt/solver_engine_scope.h index a4c1f0eaf..309321dc3 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/solver_engine_scope.h @@ -18,11 +18,10 @@ #include "cvc5_private.h" -#ifndef CVC5__SMT__SMT_ENGINE_SCOPE_H -#define CVC5__SMT__SMT_ENGINE_SCOPE_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 { @@ -33,16 +32,16 @@ class StatisticsRegistry; namespace smt { SolverEngine* currentSolverEngine(); -bool smtEngineInScope(); +bool solverEngineInScope(); /** get the current resource manager */ ResourceManager* currentResourceManager(); -class SmtScope +class SolverEngineScope { public: - SmtScope(const SolverEngine* smt); - ~SmtScope(); + SolverEngineScope(const SolverEngine* smt); + ~SolverEngineScope(); /** * This returns the StatisticsRegistry attached to the currently in scope * SolverEngine. @@ -54,7 +53,7 @@ class SmtScope SolverEngine* d_oldSlvEngine; /** Options scope */ Options::OptionsScope d_optionsScope; -};/* class SmtScope */ +}; /* class SolverEngineScope */ } // namespace smt } // namespace cvc5 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" diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp index fef1184a2..b69ba203c 100644 --- a/test/unit/node/attribute_white.cpp +++ b/test/unit/node/attribute_white.cpp @@ -22,8 +22,8 @@ #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" #include "expr/node_value.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "test_node.h" #include "theory/theory.h" #include "theory/theory_engine.h" diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index aca4239d5..eb462006c 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -22,8 +22,8 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/preprocessing_pass_context.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "test_smt.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" diff --git a/test/unit/test_env.h b/test/unit/test_env.h index 4b4fb72e9..b06254e7e 100644 --- a/test/unit/test_env.h +++ b/test/unit/test_env.h @@ -20,8 +20,8 @@ #include "expr/skolem_manager.h" #include "options/options.h" #include "smt/env.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "test.h" namespace cvc5 { diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 08fa8eb30..7d3db971c 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -18,8 +18,8 @@ #include "expr/node_manager.h" #include "expr/skolem_manager.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "test.h" namespace cvc5 { diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 9dda1e588..f97b01931 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -21,8 +21,8 @@ #include "expr/node_manager.h" #include "expr/skolem_manager.h" #include "proof/proof_checker.h" -#include "smt/smt_engine_scope.h" #include "smt/solver_engine.h" +#include "smt/solver_engine_scope.h" #include "test.h" #include "theory/output_channel.h" #include "theory/rewriter.h" diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index 9a98b174d..c6b921542 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -20,7 +20,7 @@ #include "api/cpp/cvc5.h" #include "expr/node.h" #include "expr/node_manager.h" -#include "smt/smt_engine_scope.h" +#include "smt/solver_engine_scope.h" #include "test_smt.h" #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" |