From ea7a520f737813827ac10da9e108adf1df2764c1 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 14 Jan 2025 14:32:53 -0600 Subject: [PATCH 1/2] Keep platform-dependent python extension filename (#11516) By default, Python extension filenames include a platform-dependent suffix. To facilitate the specification of the dependencies of the Python extension file in CMake, this behavior was previously overwritten by eliminating the suffix so that the filename was the same across all platforms. Although CPython, the reference implementation of Python, can load Python extensions with the new name without any problems, I recently discovered that PyPy cannot do so properly. This PR reverses the change, retains the original name, and updates the CMake and Setuptools files to handle the different filenames. --- src/api/python/CMakeLists.txt | 16 +++++++++++----- src/api/python/setup.py.in | 18 ++---------------- 2 files changed, 13 insertions(+), 21 deletions(-) diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 0e575939ed8..5d158199c81 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -116,14 +116,20 @@ copy_file_from_src(py_plugin.h) copy_file_from_src(py_plugin.cpp) copy_file_from_src(pyproject.toml) +# Get python extension filename +execute_process(COMMAND + ${Python_EXECUTABLE} -c + "import sysconfig;\ + print('cvc5_python_base' + sysconfig.get_config_var('EXT_SUFFIX'))" + OUTPUT_VARIABLE PYTHON_EXT_FILENAME + OUTPUT_STRIP_TRAILING_WHITESPACE) + # Set include_dirs and library_dirs variables that are used in setup.cfg.in if (WIN32) - set(PYTHON_EXT "pyd") set(SETUP_INCLUDE_DIRS "${PROJECT_SOURCE_DIR}/include;${CMAKE_BINARY_DIR}/include") set(SETUP_LIBRARY_DIRS "${CMAKE_BINARY_DIR}/src;${CMAKE_BINARY_DIR}/src/parser") set(SETUP_COMPILER "[build]\ncompiler=mingw32") else() - set(PYTHON_EXT "so") set(SETUP_INCLUDE_DIRS "${PROJECT_SOURCE_DIR}/include:${CMAKE_BINARY_DIR}/include") set(SETUP_LIBRARY_DIRS "${CMAKE_BINARY_DIR}/src:${CMAKE_BINARY_DIR}/src/parser") # On Linux and macOS, set rpath variable too @@ -153,20 +159,20 @@ set(PYTHON_EXT_SRC_FILES if(NOT ONLY_PYTHON_EXT_SRC) set(CVC5_PYTHON_BASE_LIB - "${CMAKE_CURRENT_BINARY_DIR}/cvc5/cvc5_python_base.${PYTHON_EXT}") + "${CMAKE_CURRENT_BINARY_DIR}/cvc5/${PYTHON_EXT_FILENAME}") add_custom_command( OUTPUT ${CVC5_PYTHON_BASE_LIB} COMMAND # Force a new build if any dependency has changed - ${CMAKE_COMMAND} -E remove cvc5_python_base.cpp cvc5/cvc5_python_base.${PYTHON_EXT} + ${CMAKE_COMMAND} -E remove cvc5_python_base.cpp cvc5/${PYTHON_EXT_FILENAME} COMMAND "${Python_EXECUTABLE}" setup.py build_ext --inplace DEPENDS cvc5 cvc5parser ${PYTHON_EXT_SRC_FILES} - COMMENT "Generating cvc5_python_base.${PYTHON_EXT}" + COMMENT "Generating ${PYTHON_EXT_FILENAME}" ) endif() diff --git a/src/api/python/setup.py.in b/src/api/python/setup.py.in index f7272f5401e..61069555c7e 100644 --- a/src/api/python/setup.py.in +++ b/src/api/python/setup.py.in @@ -20,10 +20,10 @@ ## import os +import sysconfig from setuptools import setup -ext_suffix = 'pyd' if os.name == 'nt' else 'so' -ext_filename = 'cvc5_python_base.' + ext_suffix +ext_filename = 'cvc5_python_base' + sysconfig.get_config_var('EXT_SUFFIX') packages=['cvc5', 'cvc5.pythonic'] license_files=["COPYING", "licenses/*"] @@ -44,8 +44,6 @@ else: import sys import sysconfig from setuptools.extension import Extension - - from Cython.Distutils import build_ext from Cython.Build import cythonize if sys.platform == 'darwin': @@ -90,19 +88,7 @@ else: ext_module = Extension(mod_name, mod_src_files, **ext_options) ext_module.cython_directives = {"embedsignature": True} - class ExtensionBuilder(build_ext): - def get_ext_filename(self, ext_name): - # Do not include the python version, the ABI tag, and - # the platform name in the extension module name. - # This facilitates specifying the dependencies of - # the module in CMake. - filename = super().get_ext_filename(ext_name) - suffix = sysconfig.get_config_var('EXT_SUFFIX') - ext = os.path.splitext(filename)[1] - return filename.replace(suffix, "") + ext - setup( - cmdclass={'build_ext': ExtensionBuilder}, ext_modules=cythonize([ext_module], compiler_directives=compiler_directives), packages=packages, license_files=license_files From 8dca52eb78a01c1c831680cb180284d5d1c797fc Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 14 Jan 2025 15:51:29 -0600 Subject: [PATCH 2/2] booleans/builtin: Refactor to not use NodeManager::currentNM() (#11522) This PR introduces some calls to NodeManager::currentNM(), which will be removed in subsequent PRs. --- src/smt/proof_post_processor.cpp | 3 +- src/theory/arith/pp_rewrite_eq.cpp | 3 +- src/theory/booleans/circuit_propagator.cpp | 18 +++-- .../booleans/proof_circuit_propagator.cpp | 66 ++++++++++--------- .../booleans/proof_circuit_propagator.h | 10 ++- src/theory/builtin/generic_op.cpp | 10 +-- src/theory/builtin/generic_op.h | 4 +- src/theory/builtin/proof_checker.cpp | 5 +- src/theory/builtin/proof_checker.h | 2 +- src/theory/ff/cocoa_encoder.cpp | 5 +- src/theory/ff/cocoa_encoder.h | 2 +- src/theory/ff/split_gb.cpp | 2 +- src/theory/ff/sub_theory.cpp | 7 +- src/theory/ff/util.cpp | 4 +- src/theory/ff/util.h | 2 +- src/theory/rewriter.cpp | 3 +- src/theory/theory_engine.cpp | 15 +++-- src/theory/uf/symmetry_breaker.cpp | 8 +-- src/theory/uf/symmetry_breaker.h | 20 +++--- 19 files changed, 112 insertions(+), 77 deletions(-) diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index c6991503781..2c6b9bb2271 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -881,7 +881,8 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id, { // update to TRUST_THEORY_REWRITE with idr Assert(args.size() >= 1); - Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); + Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode( + nodeManager(), theoryId); cdp->addStep( eq, ProofRule::TRUST_THEORY_REWRITE, {}, {eq, tid, args[1]}); } diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp index 8baf6b30abc..53ddf81a9d2 100644 --- a/src/theory/arith/pp_rewrite_eq.cpp +++ b/src/theory/arith/pp_rewrite_eq.cpp @@ -45,7 +45,8 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom) // don't need to rewrite terms since rewritten is not a non-standard op if (d_env.isTheoryProofProducing()) { - Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH); + Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(nodeManager(), + THEORY_ARITH); Node eq = atom.eqNode(rewritten); return d_ppPfGen.mkTrustedRewrite( atom, diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index b3bf5c6095e..965442d2836 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -75,7 +75,7 @@ void CircuitPropagator::assertTrue(TNode assertion) else if (assertion.getKind() == Kind::AND) { ProofCircuitPropagatorBackward prover{ - d_env.getProofNodeManager(), assertion, true}; + d_env.getNodeManager(), d_env.getProofNodeManager(), assertion, true}; if (isProofEnabled()) { addProof(assertion, prover.assume(assertion)); @@ -167,7 +167,8 @@ void CircuitPropagator::makeConflict(Node n) { return; } - ProofCircuitPropagator pcp(d_env.getProofNodeManager()); + ProofCircuitPropagator pcp(d_env.getNodeManager(), + d_env.getProofNodeManager()); if (n == bfalse) { d_epg->setProofFor(bfalse, pcp.assume(bfalse)); @@ -239,8 +240,10 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) { Trace("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl; - ProofCircuitPropagatorBackward prover{ - d_env.getProofNodeManager(), parent, parentAssignment}; + ProofCircuitPropagatorBackward prover{d_env.getNodeManager(), + d_env.getProofNodeManager(), + parent, + parentAssignment}; // backward rules switch (parent.getKind()) @@ -452,8 +455,11 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) Trace("circuit-prop") << "Parent: " << parent << endl; Assert(expr::hasSubterm(parent, child)); - ProofCircuitPropagatorForward prover{ - d_env.getProofNodeManager(), child, childAssignment, parent}; + ProofCircuitPropagatorForward prover{d_env.getNodeManager(), + d_env.getProofNodeManager(), + child, + childAssignment, + parent}; // Forward rules switch (parent.getKind()) diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index ee9822f19cc..781260e8803 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -31,9 +31,9 @@ namespace { /** Shorthand to create a Node from a constant number */ template -Node mkInt(T val) +Node mkInt(NodeManager* nm, T val) { - return NodeManager::currentNM()->mkConstInt(Rational(val)); + return nm->mkConstInt(Rational(val)); } /** @@ -58,8 +58,9 @@ inline std::vector collectButHoldout(TNode parent, } // namespace -ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm) - : d_pnm(pnm) +ProofCircuitPropagator::ProofCircuitPropagator(NodeManager* nm, + ProofNodeManager* pnm) + : d_nm(nm), d_pnm(pnm) { } @@ -270,7 +271,6 @@ std::shared_ptr ProofCircuitPropagator::mkCResolution( const std::vector& lits, const std::vector& polarity) { - auto* nm = NodeManager::currentNM(); std::vector> children = {clause}; std::vector cpols; std::vector clits; @@ -296,12 +296,12 @@ std::shared_ptr ProofCircuitPropagator::mkCResolution( { children.emplace_back(assume(lit)); } - cpols.emplace_back(nm->mkConst(pol)); + cpols.emplace_back(d_nm->mkConst(pol)); clits.emplace_back(lit); } std::vector args; - args.push_back(nm->mkNode(Kind::SEXPR, cpols)); - args.push_back(nm->mkNode(Kind::SEXPR, clits)); + args.push_back(d_nm->mkNode(Kind::SEXPR, cpols)); + args.push_back(d_nm->mkNode(Kind::SEXPR, clits)); return mkProof(ProofRule::CHAIN_RESOLUTION, children, args); } @@ -316,21 +316,21 @@ std::shared_ptr ProofCircuitPropagator::mkCResolution( std::shared_ptr ProofCircuitPropagator::mkResolution( const std::shared_ptr& clause, const Node& lit, bool polarity) { - auto* nm = NodeManager::currentNM(); if (polarity) { if (lit.getKind() == Kind::NOT) { return mkProof(ProofRule::RESOLUTION, {clause, assume(lit[0])}, - {nm->mkConst(false), lit[0]}); + {d_nm->mkConst(false), lit[0]}); } return mkProof(ProofRule::RESOLUTION, {clause, assume(lit.notNode())}, - {nm->mkConst(true), lit}); + {d_nm->mkConst(true), lit}); } - return mkProof( - ProofRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit}); + return mkProof(ProofRule::RESOLUTION, + {clause, assume(lit)}, + {d_nm->mkConst(false), lit}); } std::shared_ptr ProofCircuitPropagator::mkNot( @@ -345,8 +345,8 @@ std::shared_ptr ProofCircuitPropagator::mkNot( } ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward( - ProofNodeManager* pnm, TNode parent, bool parentAssignment) - : ProofCircuitPropagator(pnm), + NodeManager* nm, ProofNodeManager* pnm, TNode parent, bool parentAssignment) + : ProofCircuitPropagator(nm, pnm), d_parent(parent), d_parentAssignment(parentAssignment) { @@ -359,8 +359,9 @@ std::shared_ptr ProofCircuitPropagatorBackward::andTrue( { return nullptr; } - return mkProof( - ProofRule::AND_ELIM, {assume(d_parent)}, {mkInt(i - d_parent.begin())}); + return mkProof(ProofRule::AND_ELIM, + {assume(d_parent)}, + {mkInt(d_nm, i - d_parent.begin())}); } std::shared_ptr ProofCircuitPropagatorBackward::orFalse( @@ -372,7 +373,7 @@ std::shared_ptr ProofCircuitPropagatorBackward::orFalse( } return mkNot(mkProof(ProofRule::NOT_OR_ELIM, {assume(d_parent.notNode())}, - {mkInt(i - d_parent.begin())})); + {mkInt(d_nm, i - d_parent.begin())})); } std::shared_ptr ProofCircuitPropagatorBackward::iteC(bool c) @@ -437,8 +438,12 @@ std::shared_ptr ProofCircuitPropagatorBackward::impliesNegY() } ProofCircuitPropagatorForward::ProofCircuitPropagatorForward( - ProofNodeManager* pnm, Node child, bool childAssignment, Node parent) - : ProofCircuitPropagator{pnm}, + NodeManager* nm, + ProofNodeManager* pnm, + Node child, + bool childAssignment, + Node parent) + : ProofCircuitPropagator{nm, pnm}, d_child(child), d_childAssignment(childAssignment), d_parent(parent) @@ -466,11 +471,11 @@ std::shared_ptr ProofCircuitPropagatorForward::andOneFalse() return nullptr; } auto it = std::find(d_parent.begin(), d_parent.end(), d_child); - return mkResolution( - mkProof( - ProofRule::CNF_AND_POS, {}, {d_parent, mkInt(it - d_parent.begin())}), - d_child, - true); + return mkResolution(mkProof(ProofRule::CNF_AND_POS, + {}, + {d_parent, mkInt(d_nm, it - d_parent.begin())}), + d_child, + true); } std::shared_ptr ProofCircuitPropagatorForward::orOneTrue() @@ -480,11 +485,12 @@ std::shared_ptr ProofCircuitPropagatorForward::orOneTrue() return nullptr; } auto it = std::find(d_parent.begin(), d_parent.end(), d_child); - return mkNot(mkResolution( - mkProof( - ProofRule::CNF_OR_NEG, {}, {d_parent, mkInt(it - d_parent.begin())}), - d_child, - false)); + return mkNot( + mkResolution(mkProof(ProofRule::CNF_OR_NEG, + {}, + {d_parent, mkInt(d_nm, it - d_parent.begin())}), + d_child, + false)); } std::shared_ptr ProofCircuitPropagatorForward::orFalse() diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index 56d3d2c4854..0903c264a00 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -39,7 +39,7 @@ namespace booleans { class ProofCircuitPropagator { public: - ProofCircuitPropagator(ProofNodeManager* pnm); + ProofCircuitPropagator(NodeManager* nm, ProofNodeManager* pnm); /** Assuming the given node */ std::shared_ptr assume(Node n); @@ -117,6 +117,8 @@ class ProofCircuitPropagator /** Apply NOT_NOT_ELIM rule if n.getResult() is a nested negation */ std::shared_ptr mkNot(const std::shared_ptr& n); + /** The associated node manager */ + NodeManager* d_nm; /** The proof node manager */ ProofNodeManager* d_pnm; }; @@ -128,7 +130,8 @@ class ProofCircuitPropagator class ProofCircuitPropagatorBackward : public ProofCircuitPropagator { public: - ProofCircuitPropagatorBackward(ProofNodeManager* pnm, + ProofCircuitPropagatorBackward(NodeManager* nm, + ProofNodeManager* pnm, TNode parent, bool parentAssignment); @@ -172,7 +175,8 @@ class ProofCircuitPropagatorBackward : public ProofCircuitPropagator class ProofCircuitPropagatorForward : public ProofCircuitPropagator { public: - ProofCircuitPropagatorForward(ProofNodeManager* pnm, + ProofCircuitPropagatorForward(NodeManager* nm, + ProofNodeManager* pnm, Node child, bool childAssignment, Node parent); diff --git a/src/theory/builtin/generic_op.cpp b/src/theory/builtin/generic_op.cpp index 7a324756167..cf36bb61096 100644 --- a/src/theory/builtin/generic_op.cpp +++ b/src/theory/builtin/generic_op.cpp @@ -267,11 +267,12 @@ bool convertToNumeralList(const std::vector& indices, return true; } -Node GenericOp::getOperatorForIndices(Kind k, const std::vector& indices) +Node GenericOp::getOperatorForIndices(NodeManager* nm, + Kind k, + const std::vector& indices) { // all indices should be constant! Assert(isIndexedOperatorKind(k)); - NodeManager* nm = NodeManager::currentNM(); if (isNumeralIndexedOperatorKind(k)) { std::vector numerals; @@ -400,7 +401,8 @@ Node GenericOp::getConcreteApp(const Node& app) // usually one, but we handle cases where it is >1. size_t nargs = metakind::getMinArityForKind(okind); std::vector indices(app.begin(), app.end() - nargs); - Node op = getOperatorForIndices(okind, indices); + NodeManager* nm = NodeManager::currentNM(); + Node op = getOperatorForIndices(nm, okind, indices); // could have a bad index, in which case we don't rewrite if (op.isNull()) { @@ -409,7 +411,7 @@ Node GenericOp::getConcreteApp(const Node& app) std::vector args; args.push_back(op); args.insert(args.end(), app.end() - nargs, app.end()); - Node ret = NodeManager::currentNM()->mkNode(okind, args); + Node ret = nm->mkNode(okind, args); // could be ill typed, in which case we don't rewrite if (ret.getTypeOrNull(true).isNull()) { diff --git a/src/theory/builtin/generic_op.h b/src/theory/builtin/generic_op.h index bd596aca32a..fc39640611f 100644 --- a/src/theory/builtin/generic_op.h +++ b/src/theory/builtin/generic_op.h @@ -53,7 +53,9 @@ class GenericOp * Return the operator of kind k whose indices are the constants in the * given vector. */ - static Node getOperatorForIndices(Kind k, const std::vector& indices); + static Node getOperatorForIndices(NodeManager* nm, + Kind k, + const std::vector& indices); /** * Get the concrete term corresponding to the application of * APPLY_INDEXED_SYMBOLIC. Requires all indices to be constant. diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 1075167b2a6..93ab18814e5 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -497,10 +497,9 @@ bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid) return true; } -Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid) +Node BuiltinProofRuleChecker::mkTheoryIdNode(NodeManager* nm, TheoryId tid) { - return NodeManager::currentNM()->mkConstInt( - Rational(static_cast(tid))); + return nm->mkConstInt(Rational(static_cast(tid))); } } // namespace builtin diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 3df4546fc54..d42f0a23985 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -106,7 +106,7 @@ class BuiltinProofRuleChecker : public ProofRuleChecker /** get a TheoryId from a node, return false if we fail */ static bool getTheoryId(TNode n, TheoryId& tid); /** Make a TheoryId into a node */ - static Node mkTheoryIdNode(TheoryId tid); + static Node mkTheoryIdNode(NodeManager* nm, TheoryId tid); /** * @param nm The node manager. * @param n The term to rewrite via ENCODE_EQ_INTRO. diff --git a/src/theory/ff/cocoa_encoder.cpp b/src/theory/ff/cocoa_encoder.cpp index 00880e30bb6..e88e2383060 100644 --- a/src/theory/ff/cocoa_encoder.cpp +++ b/src/theory/ff/cocoa_encoder.cpp @@ -76,7 +76,10 @@ CoCoA::symbol cocoaSym(const std::string& varName, std::optional index) return index.has_value() ? CoCoA::symbol(s, *index) : CoCoA::symbol(s); } -CocoaEncoder::CocoaEncoder(const FfSize& size) : FieldObj(size) {} +CocoaEncoder::CocoaEncoder(NodeManager* nm, const FfSize& size) + : FieldObj(nm, size) +{ +} CoCoA::symbol CocoaEncoder::freshSym(const std::string& varName, std::optional index) diff --git a/src/theory/ff/cocoa_encoder.h b/src/theory/ff/cocoa_encoder.h index 52352b63afe..7420b0d86f7 100644 --- a/src/theory/ff/cocoa_encoder.h +++ b/src/theory/ff/cocoa_encoder.h @@ -64,7 +64,7 @@ class CocoaEncoder : public FieldObj { public: /** Create a new encoder, for this field. */ - CocoaEncoder(const FfSize& size); + CocoaEncoder(NodeManager* nm, const FfSize& size); /** Add a fact (one must call this twice per fact, once per stage). */ void addFact(const Node& fact); /** Start Stage::Encode. */ diff --git a/src/theory/ff/split_gb.cpp b/src/theory/ff/split_gb.cpp index ab3e3d15aee..e5352ed4869 100644 --- a/src/theory/ff/split_gb.cpp +++ b/src/theory/ff/split_gb.cpp @@ -41,7 +41,7 @@ std::optional> split( const std::vector& facts, const FfSize& size, const Env& env) { std::unordered_set bits{}; - CocoaEncoder enc(size); + CocoaEncoder enc(env.getNodeManager(), size); for (const auto& fact : facts) { enc.addFact(fact); diff --git a/src/theory/ff/sub_theory.cpp b/src/theory/ff/sub_theory.cpp index 741aac7bdee..fadf82ff5ef 100644 --- a/src/theory/ff/sub_theory.cpp +++ b/src/theory/ff/sub_theory.cpp @@ -47,7 +47,10 @@ namespace theory { namespace ff { SubTheory::SubTheory(Env& env, FfStatistics* stats, Integer modulus) - : EnvObj(env), FieldObj(modulus), d_facts(context()), d_stats(stats) + : EnvObj(env), + FieldObj(nodeManager(), modulus), + d_facts(context()), + d_stats(stats) { AlwaysAssert(modulus.isProbablePrime()) << "non-prime fields are unsupported"; // must be initialized before using CoCoA. @@ -85,7 +88,7 @@ Result SubTheory::postCheck(Theory::Effort e) } else if (options().ff.ffSolver == options::FfSolver::GB) { - CocoaEncoder enc(size()); + CocoaEncoder enc(nodeManager(), size()); // collect leaves for (const Node& node : d_facts) { diff --git a/src/theory/ff/util.cpp b/src/theory/ff/util.cpp index 27e3f1194a4..3874fee1345 100644 --- a/src/theory/ff/util.cpp +++ b/src/theory/ff/util.cpp @@ -30,9 +30,9 @@ namespace cvc5::internal { namespace theory { namespace ff { -FieldObj::FieldObj(const FfSize& size) +FieldObj::FieldObj(NodeManager* nm, const FfSize& size) : d_size(size), - d_nm(NodeManager::currentNM()), + d_nm(nm), d_zero(d_nm->mkConst(FiniteFieldValue(0, d_size))), d_one(d_nm->mkConst(FiniteFieldValue(1, d_size))) #ifdef CVC5_USE_COCOA diff --git a/src/theory/ff/util.h b/src/theory/ff/util.h index 16e5672dae5..321771ced23 100644 --- a/src/theory/ff/util.h +++ b/src/theory/ff/util.h @@ -47,7 +47,7 @@ using FfModel = std::unordered_map; class FieldObj { public: - FieldObj(const FfSize& size); + FieldObj(NodeManager* nm, const FfSize& size); /** create a sum (with as few as 0 elements); accepts Nodes or TNodes */ template Node mkAdd(const std::vector>& summands); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index a80eefa162d..cebbb343ee4 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -496,7 +496,8 @@ RewriteResponse Rewriter::processTrustRewriteResponse( ProofGenerator* pg = trn.getGenerator(); if (pg == nullptr) { - Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); + Node tidn = + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(d_nm, theoryId); // add small step trusted rewrite Node rid = mkMethodId(d_nm, isPre ? MethodId::RW_REWRITE_THEORY_PRE diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5a8a00a88c1..13f7e2eb8b9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -925,7 +925,8 @@ TrustNode TheoryEngine::ppRewrite(TNode term, if (tskl.getGenerator() == nullptr) { Node proven = tskl.getProven(); - Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid); + Node tidn = + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(nodeManager(), tid); d_lazyProof->addTrustedStep( proven, TrustId::THEORY_PREPROCESS_LEMMA, {}, {tidn}); skl.d_lemma = TrustNode::mkTrustLemma(proven, d_lazyProof.get()); @@ -1316,7 +1317,8 @@ TrustNode TheoryEngine::getExplanation(TNode node) { Node proven = texplanation.getProven(); TheoryId tid = theoryOf(atom)->getId(); - Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid); + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode( + nodeManager(), tid); d_lazyProof->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn}); texplanation = TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get()); @@ -1507,7 +1509,8 @@ void TheoryEngine::lemma(TrustNode tlemma, if (tlemma.getGenerator() == nullptr) { // add theory lemma step to proof - Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from); + Node tidn = + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(nodeManager(), from); d_lazyProof->addTrustedStep(lemma, TrustId::THEORY_LEMMA, {}, {tidn}); // update the trust node tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get()); @@ -1608,7 +1611,8 @@ void TheoryEngine::conflict(TrustNode tconflict, else { // add theory lemma step - Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode( + nodeManager(), theoryId); Node conf = tconflict.getProven(); d_lazyProof->addTrustedStep(conf, TrustId::THEORY_LEMMA, {}, {tidn}); } @@ -2007,7 +2011,8 @@ TrustNode TheoryEngine::getExplanation( { Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl; // otherwise, trusted theory lemma - Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(ttid); + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode( + nodeManager(), ttid); lcp->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn}); } std::vector pfChildren; diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 73c09f53a64..7a96e1068a5 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -54,8 +54,8 @@ namespace uf { using namespace cvc5::context; -SymmetryBreaker::Template::Template() - : d_template(), d_assertions(NodeManager::currentNM()), d_sets(), d_reps() +SymmetryBreaker::Template::Template(NodeManager* nm) + : d_template(), d_assertions(nm), d_sets(), d_reps() { } @@ -173,7 +173,7 @@ SymmetryBreaker::SymmetryBreaker(Env& env, std::string name) d_phiSet(), d_permutations(), d_terms(), - d_template(), + d_template(nodeManager()), d_normalizationCache(), d_termEqs(), d_termEqsOnly(), @@ -438,7 +438,7 @@ void SymmetryBreaker::assertFormula(TNode phi) { d_phi.push_back(phi); if (phi.getKind() == Kind::OR) { - Template t; + Template t(nodeManager()); Node::iterator i = phi.begin(); t.match(*i++); while(i != phi.end()) { diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 4e53c3d7da9..2b912922258 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -70,15 +70,17 @@ class SymmetryBreaker : protected EnvObj, public context::ContextNotifyObj bool matchRecursive(TNode t, TNode n); public: - Template(); - bool match(TNode n); - std::unordered_map>& partitions() { return d_sets; } - Node assertions() { - switch(d_assertions.getNumChildren()) { - case 0: return Node::null(); - case 1: return d_assertions[0]; - default: return Node(d_assertions); - } + Template(NodeManager* nm); + bool match(TNode n); + std::unordered_map>& partitions() { return d_sets; } + Node assertions() + { + switch (d_assertions.getNumChildren()) + { + case 0: return Node::null(); + case 1: return d_assertions[0]; + default: return Node(d_assertions); + } } void reset(); };/* class SymmetryBreaker::Template */