Merge branch 'main' of https://github.com/cvc5/cvc5 into pfTrustId

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()
 

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

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]});
         }

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,

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())

src/theory/booleans/proof_circuit_propagator.cpp

@@ -31,9 +31,9 @@ namespace {
 
 /** Shorthand to create a Node from a constant number */
 template <typename T>
-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<Node> 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<ProofNode> ProofCircuitPropagator::mkCResolution(
     const std::vector<Node>& lits,
     const std::vector<bool>& polarity)
 {
-  auto* nm = NodeManager::currentNM();
   std::vector<std::shared_ptr<ProofNode>> children = {clause};
   std::vector<Node> cpols;
   std::vector<Node> clits;
@@ -296,12 +296,12 @@ std::shared_ptr<ProofNode> 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<Node> 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<ProofNode> ProofCircuitPropagator::mkCResolution(
 std::shared_ptr<ProofNode> ProofCircuitPropagator::mkResolution(
     const std::shared_ptr<ProofNode>& 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<ProofNode> ProofCircuitPropagator::mkNot(
@@ -345,8 +345,8 @@ std::shared_ptr<ProofNode> 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<ProofNode> 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<ProofNode> ProofCircuitPropagatorBackward::orFalse(
@@ -372,7 +373,7 @@ std::shared_ptr<ProofNode> 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<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c)
@@ -437,8 +438,12 @@ std::shared_ptr<ProofNode> 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<ProofNode> 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<ProofNode> ProofCircuitPropagatorForward::orOneTrue()
@@ -480,11 +485,12 @@ std::shared_ptr<ProofNode> 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<ProofNode> ProofCircuitPropagatorForward::orFalse()

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<ProofNode> assume(Node n);
@@ -117,6 +117,8 @@ class ProofCircuitPropagator
   /** Apply NOT_NOT_ELIM rule if n.getResult() is a nested negation */
   std::shared_ptr<ProofNode> mkNot(const std::shared_ptr<ProofNode>& 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);

src/theory/builtin/generic_op.cpp

@@ -267,11 +267,12 @@ bool convertToNumeralList(const std::vector<Node>& indices,
   return true;
 }
 
-Node GenericOp::getOperatorForIndices(Kind k, const std::vector<Node>& indices)
+Node GenericOp::getOperatorForIndices(NodeManager* nm,
+                                      Kind k,
+                                      const std::vector<Node>& indices)
 {
   // all indices should be constant!
   Assert(isIndexedOperatorKind(k));
-  NodeManager* nm = NodeManager::currentNM();
   if (isNumeralIndexedOperatorKind(k))
   {
     std::vector<uint32_t> 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<Node> 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<Node> 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())
   {

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<Node>& indices);
+  static Node getOperatorForIndices(NodeManager* nm,
+                                    Kind k,
+                                    const std::vector<Node>& indices);
   /**
    * Get the concrete term corresponding to the application of
    * APPLY_INDEXED_SYMBOLIC. Requires all indices to be constant.