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

ajreynol · Dec 20, 2024 · 32a9337 · 32a9337
2 parents 11abba1 + b76c2b5
commit 32a9337
Show file tree

Hide file tree

Showing 83 changed files with 419 additions and 178 deletions.
diff --git a/proofs/eo/cpc/rules/Quantifiers.eo b/proofs/eo/cpc/rules/Quantifiers.eo
@@ -127,7 +127,8 @@
   (($mk_quant_unused_vars_rec @list.nil F)    @list.nil)
   (($mk_quant_unused_vars_rec (@list x xs) F) (eo::define ((r ($mk_quant_unused_vars_rec xs F)))
                                               (eo::ite ($contains_subterm F x)
-                                                (eo::ite ($contains_subterm r x) r (eo::cons @list x r))
+                                                ; remove the duplicate of x in r if it exists
+                                                (eo::cons @list x ($nary_remove @list @list.nil x r))
                                                 r)))
   )
 )

diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
@@ -63,7 +63,7 @@ class BoundVarManager
       Assert(n.getAttribute(attr).getType() == tn);
       return n.getAttribute(attr);
     }
-    Node v = NodeManager::currentNM()->mkBoundVar(tn);
+    Node v = NodeManager::mkBoundVar(tn);
     n.setAttribute(attr, v);
     // if we are keeping cache values, insert it to the set
     if (d_keepCacheVals)

diff --git a/src/expr/elim_shadow_converter.cpp b/src/expr/elim_shadow_converter.cpp
@@ -123,7 +123,7 @@ Node ElimShadowNodeConverter::eliminateShadow(const Node& q)
   {
     children.push_back(esnc.convert(q[i]));
   }
-  return NodeManager::currentNM()->mkNode(q.getKind(), children);
+  return nm->mkNode(q.getKind(), children);
 }
 
 }  // namespace cvc5::internal
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
@@ -161,22 +161,23 @@ Node SkolemManager::mkSkolemFunctionTyped(SkolemId id,
   return mkSkolemFunctionTyped(id, tn, cacheVal);
 }
 
-bool SkolemManager::isSkolemFunction(TNode k) const
+bool SkolemManager::isSkolemFunction(TNode k)
 {
   return k.getKind() == Kind::SKOLEM;
 }
 
 bool SkolemManager::isSkolemFunction(TNode k,
                                      SkolemId& id,
-                                     Node& cacheVal) const
+                                     Node& cacheVal)
 {
+  SkolemManager* skm = k.getNodeManager()->getSkolemManager();
   if (k.getKind() != Kind::SKOLEM)
   {
     return false;
   }
   std::map<Node, std::tuple<SkolemId, TypeNode, Node>>::const_iterator it =
-      d_skolemFunMap.find(k);
-  Assert(it != d_skolemFunMap.end());
+      skm->d_skolemFunMap.find(k);
+  Assert(it != skm->d_skolemFunMap.end());
   id = std::get<0>(it->second);
   cacheVal = std::get<2>(it->second);
   return true;

diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
@@ -149,12 +149,12 @@ class SkolemManager
    * Is k a skolem function? Returns true if k was generated by the above
    * call.
    */
-  bool isSkolemFunction(TNode k) const;
+  static bool isSkolemFunction(TNode k);
   /**
    * Is k a skolem function? Returns true if k was generated by the above
    * call. Updates the arguments to the values used when constructing it.
    */
-  bool isSkolemFunction(TNode k, SkolemId& id, Node& cacheVal) const;
+  static bool isSkolemFunction(TNode k, SkolemId& id, Node& cacheVal);
   /**
    * @param k The skolem.
    * @return skolem function id for k.

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -51,11 +51,11 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 }
 
 std::vector<TypeNode> SynthRewRulesPass::getGrammarsFrom(
-    const std::vector<Node>& assertions, uint64_t nvars)
+    NodeManager* nm, const std::vector<Node>& assertions, uint64_t nvars)
 {
   std::vector<TypeNode> ret;
   std::map<TypeNode, TypeNode> tlGrammarTypes =
-      constructTopLevelGrammar(assertions, nvars);
+      constructTopLevelGrammar(nm, assertions, nvars);
   for (std::pair<const TypeNode, TypeNode> ttp : tlGrammarTypes)
   {
     ret.push_back(ttp.second);
@@ -64,14 +64,13 @@ std::vector<TypeNode> SynthRewRulesPass::getGrammarsFrom(
 }
 
 std::map<TypeNode, TypeNode> SynthRewRulesPass::constructTopLevelGrammar(
-    const std::vector<Node>& assertions, uint64_t nvars)
+    NodeManager* nm, const std::vector<Node>& assertions, uint64_t nvars)
 {
   std::map<TypeNode, TypeNode> tlGrammarTypes;
   if (assertions.empty())
   {
     return tlGrammarTypes;
   }
-  NodeManager* nm = NodeManager::currentNM();
   // initialize the candidate rewrite
   std::unordered_map<TNode, bool> visited;
   std::unordered_map<TNode, bool>::iterator it;

diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h
@@ -66,11 +66,11 @@ class SynthRewRulesPass : public PreprocessingPass
   SynthRewRulesPass(PreprocessingPassContext* preprocContext);
 
   static std::vector<TypeNode> getGrammarsFrom(
-      const std::vector<Node>& assertions, uint64_t nvars);
+      NodeManager* nm, const std::vector<Node>& assertions, uint64_t nvars);
 
  protected:
   static std::map<TypeNode, TypeNode> constructTopLevelGrammar(
-      const std::vector<Node>& assertions, uint64_t nvars);
+      NodeManager* nm, const std::vector<Node>& assertions, uint64_t nvars);
   PreprocessingPassResult applyInternal(
       AssertionPipeline* assertionsToPreprocess) override;
 };

diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp
@@ -178,8 +178,7 @@ void LetBinding::updateCounts(Node n)
       {
         SkolemId skid;
         Node cacheVal;
-        SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
-        if (sm->isSkolemFunction(cur, skid, cacheVal) && !cacheVal.isNull())
+        if (SkolemManager::isSkolemFunction(cur, skid, cacheVal) && !cacheVal.isNull())
         {
           if (cacheVal.getKind() == Kind::SEXPR)
           {

diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
@@ -501,7 +501,7 @@ Node AletheNodeConverter::mkInternalSymbol(const std::string& name,
 
 Node AletheNodeConverter::mkInternalSymbol(const std::string& name)
 {
-  return mkInternalSymbol(name, NodeManager::currentNM()->sExprType());
+  return mkInternalSymbol(name, d_nm->sExprType());
 }
 
 const std::string& AletheNodeConverter::getError() { return d_error; }

diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp
@@ -23,6 +23,7 @@
 #include "proof/proof_checker.h"
 #include "proof/proof_node.h"
 #include "proof/proof_node_algorithm.h"
+#include "rewriter/rewrites.h"
 
 using namespace cvc5::internal::kind;
 
@@ -112,6 +113,15 @@ void TConvProofGenerator::addRewriteStep(Node t,
   }
 }
 
+void TConvProofGenerator::addTheoryRewriteStep(
+    Node t, Node s, ProofRewriteRule id, bool isPre, uint32_t tctx)
+{
+  std::vector<Node> sargs;
+  sargs.push_back(rewriter::mkRewriteRuleNode(id));
+  sargs.push_back(t.eqNode(s));
+  addRewriteStep(t, s, ProofRule::THEORY_REWRITE, {}, sargs, isPre, tctx);
+}
+
 bool TConvProofGenerator::hasRewriteStep(Node t,
                                          uint32_t tctx,
                                          bool isPre) const

diff --git a/src/proof/conv_proof_generator.h b/src/proof/conv_proof_generator.h
@@ -172,6 +172,12 @@ class TConvProofGenerator : protected EnvObj, public ProofGenerator
                       const std::vector<Node>& args,
                       bool isPre = false,
                       uint32_t tctx = 0);
+  /** Same as above, with a theory rewrite step */
+  void addTheoryRewriteStep(Node t,
+                            Node s,
+                            ProofRewriteRule id,
+                            bool isPre = false,
+                            uint32_t tctx = 0);
   /** Has rewrite step for term t */
   bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
   /**

diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp
@@ -181,7 +181,7 @@ void LazyCDProof::addLazyStep(Node expected,
     }
     Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
                           << " set (trusted) step " << idNull << "\n";
-    Node tid = mkTrustId(idNull);
+    Node tid = mkTrustId(nodeManager(), idNull);
     addStep(expected, ProofRule::TRUST, {}, {tid, expected});
     return;
   }

diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp
@@ -74,7 +74,7 @@ void LazyTreeProofGenerator::setCurrentTrust(size_t objectId,
                                              Node proven)
 {
   std::vector<Node> newArgs;
-  newArgs.push_back(mkTrustId(tid));
+  newArgs.push_back(mkTrustId(nodeManager(), tid));
   newArgs.push_back(proven);
   newArgs.insert(newArgs.end(), args.begin(), args.end());
   setCurrent(objectId, ProofRule::TRUST, premise, newArgs, proven);

diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp
@@ -50,10 +50,9 @@ std::ostream& operator<<(std::ostream& out, MethodId id)
   return out;
 }
 
-Node mkMethodId(MethodId id)
+Node mkMethodId(NodeManager* nm, MethodId id)
 {
-  return NodeManager::currentNM()->mkConstInt(
-      Rational(static_cast<uint32_t>(id)));
+  return nm->mkConstInt(Rational(static_cast<uint32_t>(id)));
 }
 
 bool getMethodId(TNode n, MethodId& i)
@@ -98,7 +97,8 @@ bool getMethodIds(const std::vector<Node>& args,
   return true;
 }
 
-void addMethodIds(std::vector<Node>& args,
+void addMethodIds(NodeManager* nm,
+                  std::vector<Node>& args,
                   MethodId ids,
                   MethodId ida,
                   MethodId idr)
@@ -107,15 +107,15 @@ void addMethodIds(std::vector<Node>& args,
   bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
   if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply)
   {
-    args.push_back(mkMethodId(ids));
+    args.push_back(mkMethodId(nm, ids));
   }
   if (ndefApply || ndefRewriter)
   {
-    args.push_back(mkMethodId(ida));
+    args.push_back(mkMethodId(nm, ida));
   }
   if (ndefRewriter)
   {
-    args.push_back(mkMethodId(idr));
+    args.push_back(mkMethodId(nm, idr));
   }
 }
 

diff --git a/src/proof/method_id.h b/src/proof/method_id.h
@@ -84,7 +84,7 @@ const char* toString(MethodId id);
 /** Write a rewriter id to out */
 std::ostream& operator<<(std::ostream& out, MethodId id);
 /** Make a method id node */
-Node mkMethodId(MethodId id);
+Node mkMethodId(NodeManager* nm, MethodId id);
 
 /** get a method identifier from a node, return false if we fail */
 bool getMethodId(TNode n, MethodId& i);
@@ -102,7 +102,8 @@ bool getMethodIds(const std::vector<Node>& args,
  * Add method identifiers ids, ida and idr as nodes to args. This does not add
  * ids, ida or idr if their values are the default ones.
  */
-void addMethodIds(std::vector<Node>& args,
+void addMethodIds(NodeManager* nm,
+                  std::vector<Node>& args,
                   MethodId ids,
                   MethodId ida,
                   MethodId idr);

diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp
@@ -267,7 +267,7 @@ bool CDProof::addTrustedStep(Node expected,
                              CDPOverwrite opolicy)
 {
   std::vector<Node> sargs;
-  sargs.push_back(mkTrustId(id));
+  sargs.push_back(mkTrustId(nodeManager(), id));
   sargs.push_back(expected);
   sargs.insert(sargs.end(), args.begin(), args.end());
   return addStep(

diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp
@@ -272,7 +272,8 @@ ProofRule getCongRule(const Node& n, std::vector<Node>& args)
       break;
   }
   // Add the arguments
-  args.push_back(ProofRuleChecker::mkKindNode(k));
+  NodeManager* nm = NodeManager::currentNM();
+  args.push_back(ProofRuleChecker::mkKindNode(nm, k));
   if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
   {
     args.push_back(n.getOperator());

diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
@@ -68,7 +68,7 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkTrustedNode(
     const Node& conc)
 {
   std::vector<Node> sargs;
-  sargs.push_back(mkTrustId(id));
+  sargs.push_back(mkTrustId(NodeManager::currentNM(), id));
   sargs.push_back(conc);
   sargs.insert(sargs.end(), args.begin(), args.end());
   return mkNode(ProofRule::TRUST, children, sargs);

diff --git a/src/proof/proof_rule_checker.cpp b/src/proof/proof_rule_checker.cpp
@@ -63,15 +63,14 @@ bool ProofRuleChecker::getKind(TNode n, Kind& k)
   return true;
 }
 
-Node ProofRuleChecker::mkKindNode(Kind k)
+Node ProofRuleChecker::mkKindNode(NodeManager* nm, Kind k)
 {
   if (k == Kind::UNDEFINED_KIND)
   {
     // UNDEFINED_KIND is negative, hence return null to avoid cast
     return Node::null();
   }
-  return NodeManager::currentNM()->mkConstInt(
-      Rational(static_cast<uint32_t>(k)));
+  return nm->mkConstInt(Rational(static_cast<uint32_t>(k)));
 }
 
 NodeManager* ProofRuleChecker::nodeManager() const { return d_nm; }

diff --git a/src/proof/proof_rule_checker.h b/src/proof/proof_rule_checker.h
@@ -63,7 +63,7 @@ class ProofRuleChecker
   /** get a Kind from a node, return false if we fail */
   static bool getKind(TNode n, Kind& k);
   /** Make a Kind into a node */
-  static Node mkKindNode(Kind k);
+  static Node mkKindNode(NodeManager* nm, Kind k);
 
   /** Register all rules owned by this rule checker into pc. */
   virtual void registerTo(ProofChecker* pc) {}

diff --git a/src/proof/proof_step_buffer.cpp b/src/proof/proof_step_buffer.cpp
@@ -126,7 +126,7 @@ bool ProofStepBuffer::addTrustedStep(TrustId id,
                                      Node conc)
 {
   std::vector<Node> sargs;
-  sargs.push_back(mkTrustId(id));
+  sargs.push_back(mkTrustId(NodeManager::currentNM(), id));
   sargs.push_back(conc);
   sargs.insert(sargs.end(), args.begin(), args.end());
   return addStep(ProofRule::TRUST, children, sargs, conc);

diff --git a/src/proof/resolution_proofs_util.cpp b/src/proof/resolution_proofs_util.cpp
@@ -64,7 +64,8 @@ std::ostream& operator<<(std::ostream& out, CrowdingLitInfo info)
   return out;
 }
 
-Node eliminateCrowdingLits(bool reorderPremises,
+Node eliminateCrowdingLits(NodeManager* nm,
+                           bool reorderPremises,
                            const std::vector<Node>& clauseLits,
                            const std::vector<Node>& targetClauseLits,
                            const std::vector<Node>& children,
@@ -76,7 +77,6 @@ Node eliminateCrowdingLits(bool reorderPremises,
   Trace("crowding-lits") << "Clause lits: " << clauseLits << "\n";
   Trace("crowding-lits") << "Target lits: " << targetClauseLits << "\n\n";
   std::vector<Node> newChildren{children}, newArgs{args};
-  NodeManager* nm = NodeManager::currentNM();
   Node trueNode = nm->mkConst(true);
   // get crowding lits and the position of the last clause that includes
   // them. The factoring step must be added after the last inclusion and before

diff --git a/src/proof/resolution_proofs_util.h b/src/proof/resolution_proofs_util.h
@@ -107,7 +107,8 @@ namespace proof {
  * @return The resulting node of transforming MACRO_RESOLUTION into
  * CHAIN_RESOLUTION according to the above idea.
  */
-Node eliminateCrowdingLits(bool reorderPremises,
+Node eliminateCrowdingLits(NodeManager* nm,
+                           bool reorderPremises,
                            const std::vector<Node>& clauseLits,
                            const std::vector<Node>& targetClauseLits,
                            const std::vector<Node>& children,

diff --git a/src/proof/rewrite_proof_generator.cpp b/src/proof/rewrite_proof_generator.cpp
@@ -24,7 +24,11 @@ RewriteProofGenerator::RewriteProofGenerator(Env& env, MethodId id)
     : EnvObj(env), ProofGenerator(), d_id(id)
 {
   // initialize the proof args
-  addMethodIds(d_pargs, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL, d_id);
+  addMethodIds(nodeManager(),
+               d_pargs,
+               MethodId::SB_DEFAULT,
+               MethodId::SBA_SEQUENTIAL,
+               d_id);
 }
 RewriteProofGenerator::~RewriteProofGenerator() {}
 

diff --git a/src/proof/subtype_elim_proof_converter.cpp b/src/proof/subtype_elim_proof_converter.cpp
@@ -254,7 +254,7 @@ bool SubtypeElimConverterCallback::prove(const Node& src,
   Node csrc = nm->mkNode(src.getKind(), conv[0], conv[1]);
   if (tgt.getKind() == Kind::EQUAL)
   {
-    Node nk = ProofRuleChecker::mkKindNode(Kind::TO_REAL);
+    Node nk = ProofRuleChecker::mkKindNode(nm, Kind::TO_REAL);
     cdp->addStep(csrc, ProofRule::CONG, {src}, {nk});
     Trace("pf-subtype-elim") << "...via " << csrc << std::endl;
     if (csrc != tgt)
@@ -295,7 +295,7 @@ bool SubtypeElimConverterCallback::prove(const Node& src,
     if (csrc != tgt)
     {
       Node congEq = csrc.eqNode(tgt);
-      Node nk = ProofRuleChecker::mkKindNode(csrc.getKind());
+      Node nk = ProofRuleChecker::mkKindNode(nm, csrc.getKind());
       cdp->addStep(congEq, ProofRule::CONG, {convEq[0], convEq[1]}, {nk});
       cdp->addStep(fullEq, ProofRule::TRANS, {rewriteEq, congEq}, {});
     }