From 4209fb71c97c06833ef320ad9c73590546c16fa2 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 17 Sep 2021 16:14:42 -0700 Subject: 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. --- src/api/cpp/cvc5.cpp | 144 +-------------------- src/api/cpp/cvc5.h | 2 +- src/expr/node.h | 24 ---- src/expr/node_manager.cpp | 41 +++--- src/expr/node_manager.h | 67 +++------- src/expr/type_node.cpp | 4 - src/expr/type_node.h | 12 -- src/main/main.cpp | 2 + src/smt/smt_engine.cpp | 3 - src/smt/smt_engine_scope.cpp | 3 +- src/smt/smt_engine_scope.h | 2 +- src/theory/arrays/theory_arrays_type_rules.cpp | 1 - .../datatypes/theory_datatypes_type_rules.cpp | 1 - test/unit/node/node_black.cpp | 14 +- test/unit/node/node_builder_black.cpp | 4 +- test/unit/node/type_node_white.cpp | 2 +- test/unit/preprocessing/pass_bv_gauss_white.cpp | 8 +- test/unit/prop/cnf_stream_white.cpp | 11 -- test/unit/test_env.h | 7 +- test/unit/test_node.h | 7 +- test/unit/test_smt.h | 18 ++- test/unit/theory/theory_arith_cad_white.cpp | 2 +- test/unit/theory/theory_bags_type_rules_white.cpp | 6 +- 23 files changed, 78 insertions(+), 307 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& 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& 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& sorts, const std::vector& 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&& 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 Solver::mkDatatypeSorts( const std::vector& 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 Solver::mkDatatypeSorts( const std::vector& dtypedecls, const std::set& 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 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& 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& 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& 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& sorts) const Sort Solver::mkRecordSort( const std::vector>& fields) const { - NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; std::vector> 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& 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& 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(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(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(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(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(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(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(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(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( @@ -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( @@ -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( @@ -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( @@ -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( @@ -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(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& 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& 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& 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& 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& children) const Term Solver::mkTuple(const std::vector& sorts, const std::vector& 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& 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& 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& 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& funs, const std::vector& 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 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 Solver::getUnsatAssumptions(void) const std::vector 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 Solver::getUnsatCore(void) const std::map 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 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 Solver::getValue(const std::vector& 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 Solver::getValue(const std::vector& terms) const std::vector 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 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& sorts, const std::vector& 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& 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& 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& 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& 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 d_originalOptions; /** The node manager of this solver. */ - std::unique_ptr d_nodeMgr; + NodeManager* d_nodeMgr; /** The statistics collected on the Api level. */ std::unique_ptr 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 template inline typename AttrKind::value_type NodeTemplate:: 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 template inline bool NodeTemplate:: 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 template inline bool NodeTemplate::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 template inline void NodeTemplate:: 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::printAst(std::ostream& out, int indent) const { template NodeTemplate NodeTemplate::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::hasOperator() const { template TypeNode NodeTemplate::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 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 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 NodeManager::mkMutualDatatypeTypes( const std::set& unresolvedTypes, uint32_t flags) { - NodeManagerScope nms(this); std::map nameResolutions; std::vector 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 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 - * NodeManager when it is created and reinstates the - * previous thread-global NodeManager when it is - * destroyed, effectively maintaining a set of nested - * NodeManager scopes. This is especially useful on - * public-interface calls into the cvc5 library, where cvc5's notion - * of the "current" NodeManager should be set to match - * the calling context. See, for example, the implementations of - * public calls in the SmtEngine class. - * - * The client must be careful to create and destroy - * NodeManagerScope objects in a well-nested manner (such - * as on the stack). You may create a NodeManagerScope - * with new and destroy it with delete, or - * place it as a data member of an object that is, but if the scope of - * these new/delete pairs isn't properly - * maintained, the incorrect "current" NodeManager - * 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 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::OwningTheory theory_t; NVStorage<1> nvStorage; expr::NodeValue& nvStack = reinterpret_cast(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 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 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 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 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 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(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()) diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 0001b3723..0e8bb62db 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -69,7 +69,7 @@ class TestNodeBlackNode : public TestNode Options opts; opts.base.outputLanguage = Language::LANG_AST; opts.base.outputLanguageWasSetByUser = true; - d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts)); + d_smt.reset(new SmtEngine(d_nodeManager, &opts)); } std::unique_ptr d_smt; @@ -653,7 +653,7 @@ TEST_F(TestNodeBlackNode, dagifier) TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node) { const std::vector skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); Node add = d_nodeManager->mkNode(kind::PLUS, skolems); std::vector children; for (Node child : add) @@ -667,7 +667,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node) TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode) { const std::vector skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); Node add = d_nodeManager->mkNode(kind::PLUS, skolems); std::vector children; for (TNode child : add) @@ -681,7 +681,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode) TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node) { const std::vector skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); TNode add_tnode = add_node; std::vector children; @@ -696,7 +696,7 @@ TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node) TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode) { const std::vector skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); TNode add_tnode = add_node; std::vector children; @@ -801,8 +801,8 @@ TNode level1(NodeManager* nm) { return level0(nm); } TEST_F(TestNodeBlackNode, node_tnode_usage) { Node n; - ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get())); - ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0"); + ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager)); + ASSERT_DEATH(n = level1(d_nodeManager), "d_nv->d_rc > 0"); } } // namespace test diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index fc8b6fb7b..05ccfc90c 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -62,14 +62,14 @@ TEST_F(TestNodeBlackNodeBuilder, ctors) ASSERT_EQ(spec.getKind(), d_specKind); ASSERT_EQ(spec.getNumChildren(), 0u); - NodeBuilder from_nm(d_nodeManager.get()); + NodeBuilder from_nm(d_nodeManager); ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND); #ifdef CVC5_ASSERTIONS ASSERT_DEATH(from_nm.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif - NodeBuilder from_nm_kind(d_nodeManager.get(), d_specKind); + NodeBuilder from_nm_kind(d_nodeManager, d_specKind); ASSERT_EQ(from_nm_kind.getKind(), d_specKind); ASSERT_EQ(from_nm_kind.getNumChildren(), 0u); diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index d8db32a4b..d3d05040f 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -36,7 +36,7 @@ class TestNodeWhiteTypeNode : public TestNode void SetUp() override { TestNode::SetUp(); - d_smt.reset(new SmtEngine(d_nodeManager.get())); + d_smt.reset(new SmtEngine(d_nodeManager)); } std::unique_ptr d_smt; }; diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 68758f766..329c565ea 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -2053,16 +2053,16 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) bv::utils::mkExtract( d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0))); - NodeBuilder nbx(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nbx(d_nodeManager, kind::BITVECTOR_MULT); nbx << d_x << d_one << x; Node x_mul_one_mul_xx = nbx.constructNode(); - NodeBuilder nby(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nby(d_nodeManager, kind::BITVECTOR_MULT); nby << d_y << y << d_one; Node y_mul_yy_mul_one = nby.constructNode(); - NodeBuilder nbz(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nbz(d_nodeManager, kind::BITVECTOR_MULT); nbz << d_three << d_z << z; Node three_mul_z_mul_zz = nbz.constructNode(); - NodeBuilder nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nbz2(d_nodeManager, kind::BITVECTOR_MULT); nbz2 << d_z << d_nine << z; Node z_mul_nine_mul_zz = nbz2.constructNode(); diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp index bc5bfe8f1..46bea5e19 100644 --- a/test/unit/prop/cnf_stream_white.cpp +++ b/test/unit/prop/cnf_stream_white.cpp @@ -150,7 +150,6 @@ class TestPropWhiteCnfStream : public TestSmt TEST_F(TestPropWhiteCnfStream, and) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); @@ -161,7 +160,6 @@ TEST_F(TestPropWhiteCnfStream, and) TEST_F(TestPropWhiteCnfStream, complex_expr) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); @@ -184,21 +182,18 @@ TEST_F(TestPropWhiteCnfStream, complex_expr) TEST_F(TestPropWhiteCnfStream, true) { - NodeManagerScope nms(d_nodeManager.get()); d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false); ASSERT_TRUE(d_satSolver->addClauseCalled()); } TEST_F(TestPropWhiteCnfStream, false) { - NodeManagerScope nms(d_nodeManager.get()); d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false); ASSERT_TRUE(d_satSolver->addClauseCalled()); } TEST_F(TestPropWhiteCnfStream, iff) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( @@ -208,7 +203,6 @@ TEST_F(TestPropWhiteCnfStream, iff) TEST_F(TestPropWhiteCnfStream, implies) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( @@ -218,7 +212,6 @@ TEST_F(TestPropWhiteCnfStream, implies) TEST_F(TestPropWhiteCnfStream, not ) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false); @@ -227,7 +220,6 @@ TEST_F(TestPropWhiteCnfStream, not ) TEST_F(TestPropWhiteCnfStream, or) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); @@ -238,7 +230,6 @@ TEST_F(TestPropWhiteCnfStream, or) TEST_F(TestPropWhiteCnfStream, var) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert(a, false, false); @@ -250,7 +241,6 @@ TEST_F(TestPropWhiteCnfStream, var) TEST_F(TestPropWhiteCnfStream, xor) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); d_cnfStream->convertAndAssert( @@ -260,7 +250,6 @@ TEST_F(TestPropWhiteCnfStream, xor) TEST_F(TestPropWhiteCnfStream, ensure_literal) { - NodeManagerScope nms(d_nodeManager.get()); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b); diff --git a/test/unit/test_env.h b/test/unit/test_env.h index a0c7c68c3..b3f60a98a 100644 --- a/test/unit/test_env.h +++ b/test/unit/test_env.h @@ -33,13 +33,12 @@ class TestEnv : public TestInternal void SetUp() override { d_options.reset(new Options()); - d_nodeManager.reset(new NodeManager()); - d_env.reset(new Env(d_nodeManager.get(), d_options.get())); + d_nodeManager = NodeManager::currentNM(); + d_env.reset(new Env(d_nodeManager, d_options.get())); } - std::unique_ptr d_options; - std::unique_ptr d_nodeManager; + NodeManager* d_nodeManager; std::unique_ptr d_env; }; diff --git a/test/unit/test_node.h b/test/unit/test_node.h index 4250bb7da..a6a85b1b1 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -30,17 +30,16 @@ class TestNode : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager()); + d_nodeManager = NodeManager::currentNM(); + d_nodeManager->init(); d_skolemManager = d_nodeManager->getSkolemManager(); - d_scope.reset(new NodeManagerScope(d_nodeManager.get())); d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType())); d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2))); d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType())); d_realTypeNode.reset(new TypeNode(d_nodeManager->realType())); } - std::unique_ptr d_scope; - std::unique_ptr d_nodeManager; + NodeManager* d_nodeManager; SkolemManager* d_skolemManager; std::unique_ptr d_boolTypeNode; std::unique_ptr d_bvTypeNode; diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 1cc6b0507..92701d60c 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -44,15 +44,14 @@ class TestSmt : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager()); + d_nodeManager = NodeManager::currentNM(); + d_nodeManager->init(); d_skolemManager = d_nodeManager->getSkolemManager(); - d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); - d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); + d_smtEngine.reset(new SmtEngine(d_nodeManager)); d_smtEngine->finishInit(); } - std::unique_ptr d_nmScope; - std::unique_ptr d_nodeManager; + NodeManager* d_nodeManager; SkolemManager* d_skolemManager; std::unique_ptr d_smtEngine; }; @@ -62,14 +61,13 @@ class TestSmtNoFinishInit : public TestInternal protected: void SetUp() override { - d_nodeManager.reset(new NodeManager()); + d_nodeManager = NodeManager::currentNM(); + d_nodeManager->init(); d_skolemManager = d_nodeManager->getSkolemManager(); - d_nmScope.reset(new NodeManagerScope(d_nodeManager.get())); - d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); + d_smtEngine.reset(new SmtEngine(d_nodeManager)); } - std::unique_ptr d_nmScope; - std::unique_ptr d_nodeManager; + NodeManager* d_nodeManager; SkolemManager* d_skolemManager; std::unique_ptr d_smtEngine; }; diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp index 3d5f7a8c5..0a2bcb532 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_cad_white.cpp @@ -51,7 +51,7 @@ class TestTheoryWhiteArithCAD : public TestSmt d_realType.reset(new TypeNode(d_nodeManager->realType())); d_intType.reset(new TypeNode(d_nodeManager->integerType())); Trace.on("cad-check"); - nodeManager = d_nodeManager.get(); + nodeManager = d_nodeManager; } Node dummy(int i) const { return d_nodeManager->mkConst(Rational(i)); } diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index eace59c96..682ae5bb2 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -88,9 +88,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) d_nodeManager->mkConst(Rational(1))); // only positive multiplicity are constants - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative)); - ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero)); - ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive)); + ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative)); + ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, zero)); + ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager, positive)); } TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) -- cgit v1.2.3