diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-17 16:14:42 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-17 23:14:42 +0000 |
commit | 4209fb71c97c06833ef320ad9c73590546c16fa2 (patch) | |
tree | 5155ab68258970de7485b5e3e65d3cd3f79d1078 /src | |
parent | 1704b74ffa93b36a2e08e42ca21aad0991ad4d70 (diff) |
Use a single `NodeManager` per thread (#7204)
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 144 | ||||
-rw-r--r-- | src/api/cpp/cvc5.h | 2 | ||||
-rw-r--r-- | src/expr/node.h | 24 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 41 | ||||
-rw-r--r-- | src/expr/node_manager.h | 67 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 4 | ||||
-rw-r--r-- | src/expr/type_node.h | 12 | ||||
-rw-r--r-- | src/main/main.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 3 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.cpp | 3 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.cpp | 1 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.cpp | 1 |
13 files changed, 46 insertions, 260 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 6aa556ed8..2a98ee36a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -994,9 +994,6 @@ Sort::~Sort() { if (d_solver != nullptr) { - // Ensure that the correct node manager is in scope when the node is - // destroyed. - NodeManagerScope scope(d_solver->getNodeManager()); d_type.reset(); } } @@ -1354,7 +1351,6 @@ bool Sort::isComparableTo(const Sort& s) const Datatype Sort::getDatatype() const { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK(isDatatype()) << "Expected datatype sort."; @@ -1366,7 +1362,6 @@ Datatype Sort::getDatatype() const Sort Sort::instantiate(const std::vector<Sort>& params) const { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_SORTS(params); @@ -1386,7 +1381,6 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const Sort Sort::substitute(const Sort& sort, const Sort& replacement) const { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_SORT(sort); @@ -1402,7 +1396,6 @@ Sort Sort::substitute(const Sort& sort, const Sort& replacement) const Sort Sort::substitute(const std::vector<Sort>& sorts, const std::vector<Sort>& replacements) const { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_SORTS(sorts); @@ -1427,7 +1420,6 @@ std::string Sort::toString() const //////// all checks before this line if (d_solver != nullptr) { - NodeManagerScope scope(d_solver->getNodeManager()); return d_type->toString(); } return d_type->toString(); @@ -1811,7 +1803,6 @@ Op::~Op() { // Ensure that the correct node manager is in scope when the type node is // destroyed. - NodeManagerScope scope(d_solver->getNodeManager()); d_node.reset(); } } @@ -2267,7 +2258,6 @@ std::string Op::toString() const << "Expecting a non-null internal expression"; if (d_solver != nullptr) { - NodeManagerScope scope(d_solver->getNodeManager()); return d_node->toString(); } return d_node->toString(); @@ -2303,8 +2293,6 @@ Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {} Term::Term(const Solver* slv, const cvc5::Node& n) : d_solver(slv) { - // Ensure that we create the node in the correct node manager. - NodeManagerScope scope(d_solver->getNodeManager()); d_node.reset(new cvc5::Node(n)); } @@ -2312,9 +2300,6 @@ Term::~Term() { if (d_solver != nullptr) { - // Ensure that the correct node manager is in scope when the node is - // destroyed. - NodeManagerScope scope(d_solver->getNodeManager()); d_node.reset(); } } @@ -2445,7 +2430,6 @@ Sort Term::getSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - NodeManagerScope scope(d_solver->getNodeManager()); //////// all checks before this line return Sort(d_solver, d_node->getType()); //////// @@ -2635,7 +2619,6 @@ std::string Term::toString() const //////// all checks before this line if (d_solver != nullptr) { - NodeManagerScope scope(d_solver->getNodeManager()); return d_node->toString(); } return d_node->toString(); @@ -3468,8 +3451,6 @@ DatatypeConstructorDecl::~DatatypeConstructorDecl() { if (d_ctor != nullptr) { - // ensure proper node manager is in scope - NodeManagerScope scope(d_solver->getNodeManager()); d_ctor.reset(); } } @@ -3477,7 +3458,6 @@ DatatypeConstructorDecl::~DatatypeConstructorDecl() void DatatypeConstructorDecl::addSelector(const std::string& name, const Sort& sort) { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_SORT(sort); @@ -3491,7 +3471,6 @@ void DatatypeConstructorDecl::addSelector(const std::string& name, void DatatypeConstructorDecl::addSelectorSelf(const std::string& name) { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; //////// all checks before this line @@ -3574,15 +3553,12 @@ DatatypeDecl::~DatatypeDecl() { if (d_dtype != nullptr) { - // ensure proper node manager is in scope - NodeManagerScope scope(d_solver->getNodeManager()); d_dtype.reset(); } } void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_ARG_CHECK_NOT_NULL(ctor); @@ -3667,8 +3643,6 @@ DatatypeSelector::~DatatypeSelector() { if (d_stor != nullptr) { - // ensure proper node manager is in scope - NodeManagerScope scope(d_solver->getNodeManager()); d_stor.reset(); } } @@ -3758,8 +3732,6 @@ DatatypeConstructor::~DatatypeConstructor() { if (d_ctor != nullptr) { - // ensure proper node manager is in scope - NodeManagerScope scope(d_solver->getNodeManager()); d_ctor.reset(); } } @@ -3787,7 +3759,6 @@ Term DatatypeConstructor::getConstructorTerm() const Term DatatypeConstructor::getSpecializedConstructorTerm( const Sort& retSort) const { - NodeManagerScope scope(d_solver->getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK(d_ctor->isResolved()) @@ -4021,8 +3992,6 @@ Datatype::~Datatype() { if (d_dtype != nullptr) { - // ensure proper node manager is in scope - NodeManagerScope scope(d_solver->getNodeManager()); d_dtype.reset(); } } @@ -4974,9 +4943,10 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats) Solver::Solver(std::unique_ptr<Options>&& original) { - d_nodeMgr.reset(new NodeManager()); + d_nodeMgr = NodeManager::currentNM(); + d_nodeMgr->init(); d_originalOptions = std::move(original); - d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get())); + d_smtEngine.reset(new SmtEngine(d_nodeMgr, d_originalOptions.get())); d_smtEngine->setSolver(this); d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed)); resetStatistics(); @@ -4989,7 +4959,7 @@ Solver::~Solver() {} /* Helpers and private functions */ /* -------------------------------------------------------------------------- */ -NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); } +NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr; } void Solver::increment_term_stats(Kind kind) const { @@ -5433,7 +5403,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const Sort Solver::getNullSort(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, TypeNode()); @@ -5443,7 +5412,6 @@ Sort Solver::getNullSort(void) const Sort Solver::getBooleanSort(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, getNodeManager()->booleanType()); @@ -5453,7 +5421,6 @@ Sort Solver::getBooleanSort(void) const Sort Solver::getIntegerSort(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, getNodeManager()->integerType()); @@ -5463,7 +5430,6 @@ Sort Solver::getIntegerSort(void) const Sort Solver::getRealSort(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, getNodeManager()->realType()); @@ -5473,7 +5439,6 @@ Sort Solver::getRealSort(void) const Sort Solver::getRegExpSort(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, getNodeManager()->regExpType()); @@ -5483,7 +5448,6 @@ Sort Solver::getRegExpSort(void) const Sort Solver::getStringSort(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, getNodeManager()->stringType()); @@ -5493,7 +5457,6 @@ Sort Solver::getStringSort(void) const Sort Solver::getRoundingModeSort(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, getNodeManager()->roundingModeType()); @@ -5505,7 +5468,6 @@ Sort Solver::getRoundingModeSort(void) const Sort Solver::mkArraySort(const Sort& indexSort, const Sort& elemSort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(indexSort); CVC5_API_SOLVER_CHECK_SORT(elemSort); @@ -5518,7 +5480,6 @@ Sort Solver::mkArraySort(const Sort& indexSort, const Sort& elemSort) const Sort Solver::mkBitVectorSort(uint32_t size) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0"; //////// all checks before this line @@ -5529,7 +5490,6 @@ Sort Solver::mkBitVectorSort(uint32_t size) const Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0"; @@ -5541,7 +5501,6 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const Sort Solver::mkDatatypeSort(const DatatypeDecl& dtypedecl) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl); //////// all checks before this line @@ -5553,7 +5512,6 @@ Sort Solver::mkDatatypeSort(const DatatypeDecl& dtypedecl) const std::vector<Sort> Solver::mkDatatypeSorts( const std::vector<DatatypeDecl>& dtypedecls) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line @@ -5566,7 +5524,6 @@ std::vector<Sort> Solver::mkDatatypeSorts( const std::vector<DatatypeDecl>& dtypedecls, const std::set<Sort>& unresolvedSorts) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls); CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts); @@ -5578,7 +5535,6 @@ std::vector<Sort> Solver::mkDatatypeSorts( Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain); CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain); @@ -5592,7 +5548,6 @@ Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, const Sort& codomain) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for function sort"; @@ -5608,7 +5563,6 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort Solver::mkParamSort(const std::string& symbol) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort( @@ -5620,7 +5574,6 @@ Sort Solver::mkParamSort(const std::string& symbol) const Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts) << "at least one parameter sort for predicate sort"; @@ -5636,7 +5589,6 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const Sort Solver::mkRecordSort( const std::vector<std::pair<std::string, Sort>>& fields) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; std::vector<std::pair<std::string, TypeNode>> f; for (size_t i = 0, size = fields.size(); i < size; ++i) @@ -5657,7 +5609,6 @@ Sort Solver::mkRecordSort( Sort Solver::mkSetSort(const Sort& elemSort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(elemSort); //////// all checks before this line @@ -5668,7 +5619,6 @@ Sort Solver::mkSetSort(const Sort& elemSort) const Sort Solver::mkBagSort(const Sort& elemSort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(elemSort); //////// all checks before this line @@ -5679,7 +5629,6 @@ Sort Solver::mkBagSort(const Sort& elemSort) const Sort Solver::mkSequenceSort(const Sort& elemSort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(elemSort); //////// all checks before this line @@ -5690,7 +5639,6 @@ Sort Solver::mkSequenceSort(const Sort& elemSort) const Sort Solver::mkUninterpretedSort(const std::string& symbol) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Sort(this, getNodeManager()->mkSort(symbol)); @@ -5701,7 +5649,6 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; //////// all checks before this line @@ -5712,7 +5659,6 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol, Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts); //////// all checks before this line @@ -5726,7 +5672,6 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const Term Solver::mkTrue(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Term(this, d_nodeMgr->mkConst<bool>(true)); @@ -5736,7 +5681,6 @@ Term Solver::mkTrue(void) const Term Solver::mkFalse(void) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Term(this, d_nodeMgr->mkConst<bool>(false)); @@ -5746,7 +5690,6 @@ Term Solver::mkFalse(void) const Term Solver::mkBoolean(bool val) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return Term(this, d_nodeMgr->mkConst<bool>(val)); @@ -5756,7 +5699,6 @@ Term Solver::mkBoolean(bool val) const Term Solver::mkPi() const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = @@ -5769,7 +5711,6 @@ Term Solver::mkPi() const Term Solver::mkInteger(const std::string& s) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s), s) << " an integer "; Term integer = mkRealFromStrHelper(s); @@ -5783,7 +5724,6 @@ Term Solver::mkInteger(const std::string& s) const Term Solver::mkInteger(int64_t val) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Term integer = mkValHelper<cvc5::Rational>(cvc5::Rational(val)); @@ -5795,7 +5735,6 @@ Term Solver::mkInteger(int64_t val) const Term Solver::mkReal(const std::string& s) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP * throws an std::invalid_argument exception. For consistency, we treat it @@ -5811,7 +5750,6 @@ Term Solver::mkReal(const std::string& s) const Term Solver::mkReal(int64_t val) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Term rational = mkValHelper<cvc5::Rational>(cvc5::Rational(val)); @@ -5822,7 +5760,6 @@ Term Solver::mkReal(int64_t val) const Term Solver::mkReal(int64_t num, int64_t den) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Term rational = mkValHelper<cvc5::Rational>(cvc5::Rational(num, den)); @@ -5833,7 +5770,6 @@ Term Solver::mkReal(int64_t num, int64_t den) const Term Solver::mkRegexpEmpty() const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = @@ -5846,7 +5782,6 @@ Term Solver::mkRegexpEmpty() const Term Solver::mkRegexpSigma() const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = @@ -5859,7 +5794,6 @@ Term Solver::mkRegexpSigma() const Term Solver::mkEmptySet(const Sort& sort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(sort.isNull() || sort.isSet(), sort) << "null sort or set sort"; @@ -5873,7 +5807,6 @@ Term Solver::mkEmptySet(const Sort& sort) const Term Solver::mkEmptyBag(const Sort& sort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(sort.isNull() || sort.isBag(), sort) << "null sort or bag sort"; @@ -5887,7 +5820,6 @@ Term Solver::mkEmptyBag(const Sort& sort) const Term Solver::mkSepNil(const Sort& sort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line @@ -5901,7 +5833,6 @@ Term Solver::mkSepNil(const Sort& sort) const Term Solver::mkString(const std::string& s, bool useEscSequences) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::String>(cvc5::String(s, useEscSequences)); @@ -5911,7 +5842,6 @@ Term Solver::mkString(const std::string& s, bool useEscSequences) const Term Solver::mkString(const std::wstring& s) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::String>(cvc5::String(s)); @@ -5921,7 +5851,6 @@ Term Solver::mkString(const std::wstring& s) const Term Solver::mkEmptySequence(const Sort& sort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line @@ -5934,7 +5863,6 @@ Term Solver::mkEmptySequence(const Sort& sort) const Term Solver::mkUniverseSet(const Sort& sort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line @@ -5950,7 +5878,6 @@ Term Solver::mkUniverseSet(const Sort& sort) const Term Solver::mkBitVector(uint32_t size, uint64_t val) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkBVFromIntHelper(size, val); @@ -5962,7 +5889,6 @@ Term Solver::mkBitVector(uint32_t size, const std::string& s, uint32_t base) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkBVFromStrHelper(size, s, base); @@ -5972,7 +5898,6 @@ Term Solver::mkBitVector(uint32_t size, Term Solver::mkConstArray(const Sort& sort, const Term& val) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); CVC5_API_SOLVER_CHECK_TERM(val); @@ -5997,7 +5922,6 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( @@ -6008,7 +5932,6 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( @@ -6019,7 +5942,6 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const Term Solver::mkNaN(uint32_t exp, uint32_t sig) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( @@ -6030,7 +5952,6 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( @@ -6041,7 +5962,6 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::FloatingPoint>( @@ -6052,7 +5972,6 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const Term Solver::mkRoundingMode(RoundingMode rm) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm)); @@ -6062,7 +5981,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line @@ -6074,7 +5992,6 @@ Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const Term Solver::mkAbstractValue(const std::string& index) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string"; @@ -6091,7 +6008,6 @@ Term Solver::mkAbstractValue(const std::string& index) const Term Solver::mkAbstractValue(uint64_t index) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; //////// all checks before this line @@ -6105,7 +6021,6 @@ Term Solver::mkAbstractValue(uint64_t index) const Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(val); CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; @@ -6128,7 +6043,6 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const Term Solver::mkConst(const Sort& sort, const std::string& symbol) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line @@ -6142,7 +6056,6 @@ Term Solver::mkConst(const Sort& sort, const std::string& symbol) const Term Solver::mkConst(const Sort& sort) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line @@ -6159,7 +6072,6 @@ Term Solver::mkConst(const Sort& sort) const Term Solver::mkVar(const Sort& sort, const std::string& symbol) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line @@ -6178,7 +6090,6 @@ Term Solver::mkVar(const Sort& sort, const std::string& symbol) const DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( const std::string& name) { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return DatatypeConstructorDecl(this, name); @@ -6191,7 +6102,6 @@ DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl( DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype) { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line return DatatypeDecl(this, name, isCoDatatype); @@ -6203,7 +6113,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, Sort param, bool isCoDatatype) { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(param); //////// all checks before this line @@ -6216,7 +6125,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, const std::vector<Sort>& params, bool isCoDatatype) { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORTS(params); //////// all checks before this line @@ -6230,7 +6138,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, Term Solver::mkTerm(Kind kind) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_KIND_CHECK(kind); //////// all checks before this line @@ -6241,7 +6148,6 @@ Term Solver::mkTerm(Kind kind) const Term Solver::mkTerm(Kind kind, const Term& child) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_KIND_CHECK(kind); CVC5_API_SOLVER_CHECK_TERM(child); @@ -6253,7 +6159,6 @@ Term Solver::mkTerm(Kind kind, const Term& child) const Term Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_KIND_CHECK(kind); CVC5_API_SOLVER_CHECK_TERM(child1); @@ -6269,7 +6174,6 @@ Term Solver::mkTerm(Kind kind, const Term& child2, const Term& child3) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_KIND_CHECK(kind); CVC5_API_SOLVER_CHECK_TERM(child1); @@ -6284,7 +6188,6 @@ Term Solver::mkTerm(Kind kind, Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_KIND_CHECK(kind); CVC5_API_SOLVER_CHECK_TERMS(children); @@ -6296,7 +6199,6 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const Term Solver::mkTerm(const Op& op) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_OP(op); checkMkTerm(op.d_kind, 0); @@ -6318,7 +6220,6 @@ Term Solver::mkTerm(const Op& op) const Term Solver::mkTerm(const Op& op, const Term& child) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_OP(op); CVC5_API_SOLVER_CHECK_TERM(child); @@ -6330,7 +6231,6 @@ Term Solver::mkTerm(const Op& op, const Term& child) const Term Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_OP(op); CVC5_API_SOLVER_CHECK_TERM(child1); @@ -6346,7 +6246,6 @@ Term Solver::mkTerm(const Op& op, const Term& child2, const Term& child3) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_OP(op); CVC5_API_SOLVER_CHECK_TERM(child1); @@ -6360,7 +6259,6 @@ Term Solver::mkTerm(const Op& op, Term Solver::mkTerm(const Op& op, const std::vector<Term>& children) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_OP(op); CVC5_API_SOLVER_CHECK_TERMS(children); @@ -6373,7 +6271,6 @@ Term Solver::mkTerm(const Op& op, const std::vector<Term>& children) const Term Solver::mkTuple(const std::vector<Sort>& sorts, const std::vector<Term>& terms) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(sorts.size() == terms.size()) << "Expected the same number of sorts and elements"; @@ -6630,7 +6527,6 @@ Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const Term Solver::simplify(const Term& term) { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(term); //////// all checks before this line @@ -6641,7 +6537,6 @@ Term Solver::simplify(const Term& term) Result Solver::checkEntailed(const Term& term) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(!d_smtEngine->isQueryMade() || d_smtEngine->getOptions().base.incrementalSolving) @@ -6657,7 +6552,6 @@ Result Solver::checkEntailed(const Term& term) const Result Solver::checkEntailed(const std::vector<Term>& terms) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " @@ -6686,7 +6580,6 @@ void Solver::assertFormula(const Term& term) const Result Solver::checkSat(void) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " @@ -6700,7 +6593,6 @@ Result Solver::checkSat(void) const Result Solver::checkSatAssuming(const Term& assumption) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " @@ -6715,7 +6607,6 @@ Result Solver::checkSatAssuming(const Term& assumption) const Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 || d_smtEngine->getOptions().base.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " @@ -6857,7 +6748,6 @@ Term Solver::defineFunRec(const std::string& symbol, const Term& term, bool global) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -6902,7 +6792,6 @@ Term Solver::defineFunRec(const Term& fun, const Term& term, bool global) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -6944,7 +6833,6 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, const std::vector<Term>& terms, bool global) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified()) @@ -7245,7 +7133,6 @@ DriverOptions Solver::getDriverOptions() const { return DriverOptions(*this); } std::vector<Term> Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; @@ -7273,7 +7160,6 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const std::vector<Term> Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; @@ -7297,7 +7183,6 @@ std::vector<Term> Solver::getUnsatCore(void) const std::map<Term, Term> Solver::getDifficulty() const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT || d_smtEngine->getSmtMode() == SmtMode::SAT || d_smtEngine->getSmtMode() @@ -7319,7 +7204,6 @@ std::map<Term, Term> Solver::getDifficulty() const std::string Solver::getProof(void) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceProofs) << "Cannot get proof explicitly enabled (try --produce-proofs)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -7341,7 +7225,6 @@ Term Solver::getValue(const Term& term) const std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; @@ -7364,7 +7247,6 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const std::vector<Term> Solver::getModelDomainElements(const Sort& s) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get domain elements unless model generation is enabled " "(try --produce-models)"; @@ -7390,7 +7272,6 @@ std::vector<Term> Solver::getModelDomainElements(const Sort& s) const bool Solver::isModelCoreSymbol(const Term& v) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot check if model core symbol unless model generation is enabled " "(try --produce-models)"; @@ -7410,7 +7291,6 @@ std::string Solver::getModel(const std::vector<Sort>& sorts, const std::vector<Term>& vars) const { CVC5_API_TRY_CATCH_BEGIN; - NodeManagerScope scope(getNodeManager()); CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get model unless model generation is enabled " "(try --produce-models)"; @@ -7438,7 +7318,6 @@ std::string Solver::getModel(const std::vector<Sort>& sorts, Term Solver::getQuantifierElimination(const Term& q) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line @@ -7450,7 +7329,6 @@ Term Solver::getQuantifierElimination(const Term& q) const Term Solver::getQuantifierEliminationDisjunct(const Term& q) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(q); //////// all checks before this line @@ -7478,7 +7356,6 @@ void Solver::declareSeparationHeap(const Sort& locSort, Term Solver::getSeparationHeap() const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK( d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) @@ -7497,7 +7374,6 @@ Term Solver::getSeparationHeap() const Term Solver::getSeparationNilTerm() const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK( d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) @@ -7518,7 +7394,6 @@ Term Solver::declarePool(const std::string& symbol, const Sort& sort, const std::vector<Term>& initValue) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_SORT(sort); CVC5_API_SOLVER_CHECK_TERMS(initValue); @@ -7534,7 +7409,6 @@ Term Solver::declarePool(const std::string& symbol, void Solver::pop(uint32_t nscopes) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; @@ -7551,7 +7425,6 @@ void Solver::pop(uint32_t nscopes) const bool Solver::getInterpolant(const Term& conj, Term& output) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); //////// all checks before this line @@ -7570,7 +7443,6 @@ bool Solver::getInterpolant(const Term& conj, Grammar& grammar, Term& output) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); //////// all checks before this line @@ -7588,7 +7460,6 @@ bool Solver::getInterpolant(const Term& conj, bool Solver::getAbduct(const Term& conj, Term& output) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); //////// all checks before this line @@ -7605,7 +7476,6 @@ bool Solver::getAbduct(const Term& conj, Term& output) const bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); //////// all checks before this line @@ -7623,7 +7493,6 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const void Solver::blockModel() const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " @@ -7638,7 +7507,6 @@ void Solver::blockModel() const void Solver::blockModelValues(const std::vector<Term>& terms) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " @@ -7656,7 +7524,6 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const void Solver::printInstantiations(std::ostream& out) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line d_smtEngine->printInstantiations(out); @@ -7666,7 +7533,6 @@ void Solver::printInstantiations(std::ostream& out) const void Solver::push(uint32_t nscopes) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; @@ -7834,7 +7700,6 @@ Term Solver::synthInv(const std::string& symbol, void Solver::addSygusConstraint(const Term& term) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(term); CVC5_API_ARG_CHECK_EXPECTED( @@ -7848,7 +7713,6 @@ void Solver::addSygusConstraint(const Term& term) const void Solver::addSygusAssume(const Term& term) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(term); CVC5_API_ARG_CHECK_EXPECTED( diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 4f1c60814..248bb8bda 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4491,7 +4491,7 @@ class CVC5_EXPORT Solver /** Keep a copy of the original option settings (for resets). */ std::unique_ptr<Options> d_originalOptions; /** The node manager of this solver. */ - std::unique_ptr<NodeManager> d_nodeMgr; + NodeManager* d_nodeMgr; /** The statistics collected on the Api level. */ std::unique_ptr<APIStatistics> d_stats; /** The SMT engine of this solver. */ diff --git a/src/expr/node.h b/src/expr/node.h index 1ce915472..13885a0f2 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1007,10 +1007,6 @@ template <bool ref_count> template <class AttrKind> inline typename AttrKind::value_type NodeTemplate<ref_count>:: getAttribute(const AttrKind&) const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; - assertTNodeNotExpired(); return NodeManager::currentNM()->getAttribute(*this, AttrKind()); @@ -1020,10 +1016,6 @@ template <bool ref_count> template <class AttrKind> inline bool NodeTemplate<ref_count>:: hasAttribute(const AttrKind&) const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; - assertTNodeNotExpired(); return NodeManager::currentNM()->hasAttribute(*this, AttrKind()); @@ -1033,10 +1025,6 @@ template <bool ref_count> template <class AttrKind> inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; - assertTNodeNotExpired(); return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret); @@ -1046,10 +1034,6 @@ template <bool ref_count> template <class AttrKind> inline void NodeTemplate<ref_count>:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; - assertTNodeNotExpired(); NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); @@ -1246,10 +1230,6 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const { template <bool ref_count> NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; - assertTNodeNotExpired(); kind::MetaKind mk = getMetaKind(); @@ -1276,10 +1256,6 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { template <bool ref_count> TypeNode NodeTemplate<ref_count>::getType(bool check) const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; - assertTNodeNotExpired(); return NodeManager::currentNM()->getType(*this, check); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index fe7d75ca3..1222f3c9e 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -41,8 +41,6 @@ using namespace cvc5::expr; namespace cvc5 { -thread_local NodeManager* NodeManager::s_current = NULL; - namespace { /** @@ -97,6 +95,7 @@ typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAtt NodeManager::NodeManager() : d_skManager(new SkolemManager), d_bvManager(new BoundVarManager), + d_initialized(false), next_id(0), d_attrManager(new expr::attr::AttributeManager()), d_nodeUnderDeletion(nullptr), @@ -104,7 +103,12 @@ NodeManager::NodeManager() d_abstractValueCount(0), d_skolemCounter(0) { - init(); +} + +NodeManager* NodeManager::currentNM() +{ + thread_local static NodeManager nm; + return &nm; } bool NodeManager::isNAryKind(Kind k) @@ -183,10 +187,15 @@ TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) } void NodeManager::init() { - // `mkConst()` indirectly needs the correct NodeManager in scope because we - // call `NodeValue::inc()` which uses `NodeManager::curentNM()` - NodeManagerScope nms(this); + if (d_initialized) + { + return; + } + d_initialized = true; + // Note: This code cannot be part of the constructor because it indirectly + // calls `NodeManager::currentNM()`, which is where the `NodeManager` is + // being constructed. poolInsert( &expr::NodeValue::null() ); for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { @@ -199,11 +208,6 @@ void NodeManager::init() { } NodeManager::~NodeManager() { - // have to ensure "this" is the current NodeManager during - // destruction of operators, because they get GCed. - - NodeManagerScope nms(this); - // Destroy skolem and bound var manager before cleaning up attributes and // zombies d_skManager = nullptr; @@ -253,7 +257,10 @@ NodeManager::~NodeManager() { } } - poolRemove( &expr::NodeValue::null() ); + if (d_initialized) + { + poolRemove(&expr::NodeValue::null()); + } if(Debug.isOn("gc:leaks")) { Debug("gc:leaks") << "still in pool:" << endl; @@ -434,15 +441,6 @@ std::vector<NodeValue*> NodeManager::TopologicalSort( TypeNode NodeManager::getType(TNode n, bool check) { - // Many theories' type checkers call Node::getType() directly. This - // is incorrect, since "this" might not be the caller's current node - // manager. Rather than force the individual typecheckers not to do - // this (by policy, which would be imperfect and lead to - // hard-to-find bugs, which it has in the past), we just set this - // node manager to be current for the duration of this check. - // - NodeManagerScope nms(this); - TypeNode typeNode; bool hasType = getAttribute(n, TypeAttr(), typeNode); bool needsCheck = check && !getAttribute(n, TypeCheckedAttr()); @@ -562,7 +560,6 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes( const std::set<TypeNode>& unresolvedTypes, uint32_t flags) { - NodeManagerScope nms(this); std::map<std::string, TypeNode> nameResolutions; std::vector<TypeNode> dtts; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b651c055a..204cdb677 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -90,7 +90,6 @@ class NodeManager friend class SkolemManager; friend class NodeBuilder; - friend class NodeManagerScope; public: /** @@ -101,6 +100,14 @@ class NodeManager static bool isNAryKind(Kind k); private: + /** + * Instead of creating an instance using the constructor, + * `NodeManager::currentNM()` should be used to retrieve an instance of + * `NodeManager`. + */ + explicit NodeManager(); + ~NodeManager(); + /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } @@ -113,8 +120,6 @@ class NodeManager expr::NodeValueIDHashFunction, expr::NodeValueIDEquality> NodeValueIDSet; - static thread_local NodeManager* s_current; - /** The skolem manager */ std::unique_ptr<SkolemManager> d_skManager; /** The bound variable manager */ @@ -122,6 +127,8 @@ class NodeManager NodeValuePool d_nodeValuePool; + bool d_initialized; + size_t next_id; expr::attr::AttributeManager* d_attrManager; @@ -346,8 +353,6 @@ class NodeManager NodeManager& operator=(const NodeManager&) = delete; - void init(); - /** * Create a variable with the given name and type. NOTE that no * lookup is done on the name. If you mkVar("a", type) and then @@ -374,11 +379,16 @@ class NodeManager int flags = SKOLEM_DEFAULT); public: - explicit NodeManager(); - ~NodeManager(); + /** + * Initialize the node manager by adding a null node to the pool and filling + * the caches for `operatorOf()`. This method must be called before using the + * NodeManager. This method may be called multiple times. Subsequent calls to + * this method have no effect. + */ + void init(); /** The node manager in the current public-facing cvc5 library context */ - static NodeManager* currentNM() { return s_current; } + static NodeManager* currentNM(); /** Get this node manager's skolem manager */ SkolemManager* getSkolemManager() { return d_skManager.get(); } /** Get this node manager's bound variable manager */ @@ -1052,43 +1062,6 @@ class NodeManager void debugHook(int debugFlag); }; /* class NodeManager */ -/** - * This class changes the "current" thread-global - * <code>NodeManager</code> when it is created and reinstates the - * previous thread-global <code>NodeManager</code> when it is - * destroyed, effectively maintaining a set of nested - * <code>NodeManager</code> scopes. This is especially useful on - * public-interface calls into the cvc5 library, where cvc5's notion - * of the "current" <code>NodeManager</code> should be set to match - * the calling context. See, for example, the implementations of - * public calls in the <code>SmtEngine</code> class. - * - * The client must be careful to create and destroy - * <code>NodeManagerScope</code> objects in a well-nested manner (such - * as on the stack). You may create a <code>NodeManagerScope</code> - * with <code>new</code> and destroy it with <code>delete</code>, or - * place it as a data member of an object that is, but if the scope of - * these <code>new</code>/<code>delete</code> pairs isn't properly - * maintained, the incorrect "current" <code>NodeManager</code> - * pointer may be restored after a delete. - */ -class NodeManagerScope { - /** The old NodeManager, to be restored on destruction. */ - NodeManager* d_oldNodeManager; -public: - NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) - { - NodeManager::s_current = nm; - Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; - } - - ~NodeManagerScope() { - NodeManager::s_current = d_oldNodeManager; - Debug("current") << "node manager scope: " - << "returning to " << NodeManager::s_current << "\n"; - } -};/* class NodeManagerScope */ - inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType, @@ -1310,10 +1283,6 @@ TypeNode NodeManager::mkTypeConst(const T& val) { template <class NodeClass, class T> NodeClass NodeManager::mkConstInternal(const T& val) { - // This method indirectly calls `NodeValue::inc()`, which relies on having - // the correct `NodeManager` in scope. - NodeManagerScope nms(this); - // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t; NVStorage<1> nvStorage; expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage); diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index a7747c674..6f522bbe8 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -466,10 +466,6 @@ TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ } TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; - Assert(!t0.isNull()); Assert(!t1.isNull()); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 2f854f581..89b5b7299 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -852,35 +852,23 @@ inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) { template <class AttrKind> inline typename AttrKind::value_type TypeNode:: getAttribute(const AttrKind&) const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->getAttribute(d_nv, AttrKind()); } template <class AttrKind> inline bool TypeNode:: hasAttribute(const AttrKind&) const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind()); } template <class AttrKind> inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret); } template <class AttrKind> inline void TypeNode:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { - Assert(NodeManager::currentNM() != NULL) - << "There is no current cvc5::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?"; NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value); } diff --git a/src/main/main.cpp b/src/main/main.cpp index 141b0c46c..26997e084 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -74,5 +74,7 @@ int main(int argc, char* argv[]) main::pExecutor->printStatistics(solver->getDriverOptions().err()); } } + // Make sure that the command executor is destroyed before the node manager. + main::pExecutor.reset(); exit(1); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index aa7534f26..96a1aa8ea 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1256,7 +1256,6 @@ std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void) "separation logic theory."; throw RecoverableModalException(msg); } - NodeManagerScope nms(getNodeManager()); Node heap; Node nil; TheoryModel* tm = getAvailableModel("get separation logic heap and nil"); @@ -1920,7 +1919,6 @@ void SmtEngine::printStatisticsDiff() const void SmtEngine::setOption(const std::string& key, const std::string& value) { - NodeManagerScope nms(getNodeManager()); Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if (Dump.isOn("benchmark")) @@ -1963,7 +1961,6 @@ bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } std::string SmtEngine::getOption(const std::string& key) const { - NodeManagerScope nms(getNodeManager()); NodeManager* nm = d_env->getNodeManager(); Trace("smt") << "SMT getOption(" << key << ")" << endl; diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 98f4c8d70..ebaa73b03 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -41,8 +41,7 @@ ResourceManager* currentResourceManager() } SmtScope::SmtScope(const SmtEngine* smt) - : NodeManagerScope(smt->getNodeManager()), - d_oldSmtEngine(s_smtEngine_current), + : d_oldSmtEngine(s_smtEngine_current), d_optionsScope(smt ? &const_cast<SmtEngine*>(smt)->getOptions() : nullptr) { Assert(smt != NULL); diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index cc231fa3c..f9b024a3b 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -38,7 +38,7 @@ bool smtEngineInScope(); /** get the current resource manager */ ResourceManager* currentResourceManager(); -class SmtScope : public NodeManagerScope +class SmtScope { public: SmtScope(const SmtEngine* smt); diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 6d16e4020..e1b4813ec 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -92,7 +92,6 @@ TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager, bool ArrayStoreTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) { Assert(n.getKind() == kind::STORE); - NodeManagerScope nms(nodeManager); TNode store = n[0]; TNode index = n[1]; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 6cb1f44e1..503eaf4df 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -99,7 +99,6 @@ bool DatatypeConstructorTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) { Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); - NodeManagerScope nms(nodeManager); for (TNode::const_iterator i = n.begin(); i != n.end(); ++i) { if (!(*i).isConst()) |