Update proof namespaces (#6614)

This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.

12 files changed, 235 insertions, 27 deletions

diff --git a/src/proof/conv_seq_proof_generator.cpp b/src/proof/conv_seq_proof_generator.cpp
index 65a7e462b..7b6a06ddd 100644
--- a/src/proof/conv_seq_proof_generator.cpp
+++ b/src/proof/conv_seq_proof_generator.cpp
@@ -122,13 +122,13 @@ std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor(
   return d_pnm->mkTrans(transChildren, f);
 }
 
-theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
+TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
     const std::vector<Node>& cterms)
 {
   Assert(cterms.size() == d_tconvs.size() + 1);
   if (cterms[0] == cterms[cterms.size() - 1])
   {
-    return theory::TrustNode::null();
+    return TrustNode::null();
   }
   bool useThis = false;
   ProofGenerator* pg = nullptr;
@@ -163,8 +163,7 @@ theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
     }
   }
   Assert(pg != nullptr);
-  return theory::TrustNode::mkTrustRewrite(
-      cterms[0], cterms[cterms.size() - 1], pg);
+  return TrustNode::mkTrustRewrite(cterms[0], cterms[cterms.size() - 1], pg);
 }
 
 std::string TConvSeqProofGenerator::identify() const { return d_name; }
diff --git a/src/proof/conv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h
index 8d4417134..ac8663b58 100644
--- a/src/proof/conv_seq_proof_generator.h
+++ b/src/proof/conv_seq_proof_generator.h
@@ -98,7 +98,7 @@ class TConvSeqProofGenerator : public ProofGenerator
    * then we return a trust node proving (= d e) with the 2nd component proof
    * generator, as it alone is capable of proving this equality.
    */
-  theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
+  TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
 
  protected:
   using NodeIndexPairHashFunction =
diff --git a/src/proof/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp
index 34ff4fa75..2a86f982c 100644
--- a/src/proof/eager_proof_generator.cpp
+++ b/src/proof/eager_proof_generator.cpp
@@ -20,7 +20,6 @@
 #include "proof/proof_node_manager.h"
 
 namespace cvc5 {
-namespace theory {
 
 EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
                                          context::Context* c,
@@ -155,5 +154,4 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
 
 std::string EagerProofGenerator::identify() const { return d_name; }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/eager_proof_generator.h b/src/proof/eager_proof_generator.h
index ada48d893..90e2787fd 100644
--- a/src/proof/eager_proof_generator.h
+++ b/src/proof/eager_proof_generator.h
@@ -29,8 +29,6 @@ namespace cvc5 {
 class ProofNode;
 class ProofNodeManager;
 
-namespace theory {
-
 /**
  * An eager proof generator, with explicit proof caching.
  *
@@ -191,7 +189,6 @@ class EagerProofGenerator : public ProofGenerator
   NodeProofNodeMap d_proofs;
 };
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif /* CVC5__PROOF__PROOF_GENERATOR_H */
diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp
index a50b9efd4..225a6c75c 100644
--- a/src/proof/lazy_tree_proof_generator.cpp
+++ b/src/proof/lazy_tree_proof_generator.cpp
@@ -23,7 +23,6 @@
 #include "proof/proof_node_manager.h"
 
 namespace cvc5 {
-namespace theory {
 
 LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm,
                                                const std::string& name)
@@ -142,5 +141,4 @@ std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg)
   return os;
 }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h
index 8b8d344e9..ff5d0ad2e 100644
--- a/src/proof/lazy_tree_proof_generator.h
+++ b/src/proof/lazy_tree_proof_generator.h
@@ -25,7 +25,6 @@
 #include "proof/proof_node_manager.h"
 
 namespace cvc5 {
-namespace theory {
 namespace detail {
 /**
  * A single node in the proof tree created by the LazyTreeProofGenerator.
@@ -217,7 +216,6 @@ class LazyTreeProofGenerator : public ProofGenerator
  */
 std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg);
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif
diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp
new file mode 100644
index 000000000..c5e8458cd
--- /dev/null
+++ b/src/proof/method_id.cpp
@@ -0,0 +1,118 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of method identifier
+ */
+
+#include "proof/method_id.h"
+
+#include "proof/proof_checker.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+
+const char* toString(MethodId id)
+{
+  switch (id)
+  {
+    case MethodId::RW_REWRITE: return "RW_REWRITE";
+    case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
+    case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
+    case MethodId::RW_EVALUATE: return "RW_EVALUATE";
+    case MethodId::RW_IDENTITY: return "RW_IDENTITY";
+    case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
+    case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
+    case MethodId::SB_DEFAULT: return "SB_DEFAULT";
+    case MethodId::SB_LITERAL: return "SB_LITERAL";
+    case MethodId::SB_FORMULA: return "SB_FORMULA";
+    case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL";
+    case MethodId::SBA_SIMUL: return "SBA_SIMUL";
+    case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT";
+    default: return "MethodId::Unknown";
+  };
+}
+
+std::ostream& operator<<(std::ostream& out, MethodId id)
+{
+  out << toString(id);
+  return out;
+}
+
+Node mkMethodId(MethodId id)
+{
+  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
+}
+
+bool getMethodId(TNode n, MethodId& i)
+{
+  uint32_t index;
+  if (!ProofRuleChecker::getUInt32(n, index))
+  {
+    return false;
+  }
+  i = static_cast<MethodId>(index);
+  return true;
+}
+
+bool getMethodIds(const std::vector<Node>& args,
+                  MethodId& ids,
+                  MethodId& ida,
+                  MethodId& idr,
+                  size_t index)
+{
+  ids = MethodId::SB_DEFAULT;
+  ida = MethodId::SBA_SEQUENTIAL;
+  idr = MethodId::RW_REWRITE;
+  for (size_t offset = 0; offset <= 2; offset++)
+  {
+    if (args.size() > index + offset)
+    {
+      MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr);
+      if (!getMethodId(args[index + offset], id))
+      {
+        Trace("builtin-pfcheck")
+            << "Failed to get id from " << args[index + offset] << std::endl;
+        return false;
+      }
+    }
+    else
+    {
+      break;
+    }
+  }
+  Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
+                           << ida << " / " << idr << "\n";
+  return true;
+}
+
+void addMethodIds(std::vector<Node>& args,
+                  MethodId ids,
+                  MethodId ida,
+                  MethodId idr)
+{
+  bool ndefRewriter = (idr != MethodId::RW_REWRITE);
+  bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL);
+  if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply)
+  {
+    args.push_back(mkMethodId(ids));
+  }
+  if (ndefApply || ndefRewriter)
+  {
+    args.push_back(mkMethodId(ida));
+  }
+  if (ndefRewriter)
+  {
+    args.push_back(mkMethodId(idr));
+  }
+}
+
+}  // namespace cvc5
diff --git a/src/proof/method_id.h b/src/proof/method_id.h
new file mode 100644
index 000000000..b353232f4
--- /dev/null
+++ b/src/proof/method_id.h
@@ -0,0 +1,109 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Method identifier enumeration
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__METHOD_ID_H
+#define CVC5__PROOF__METHOD_ID_H
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+/**
+ * Identifiers for rewriters and substitutions, which we abstractly
+ * classify as "methods".  Methods have a unique identifier in the internal
+ * proof calculus implemented by the checker below.
+ *
+ * A "rewriter" is abstractly a method from Node to Node, where the output
+ * is semantically equivalent to the input. The identifiers below list
+ * various methods that have this contract. This identifier is used
+ * in a number of the builtin rules.
+ *
+ * A substitution is a method for turning a formula into a substitution.
+ */
+enum class MethodId : uint32_t
+{
+  //---------------------------- Rewriters
+  // Rewriter::rewrite(n)
+  RW_REWRITE,
+  // d_ext_rew.extendedRewrite(n);
+  RW_EXT_REWRITE,
+  // Rewriter::rewriteExtEquality(n)
+  RW_REWRITE_EQ_EXT,
+  // Evaluator::evaluate(n)
+  RW_EVALUATE,
+  // identity
+  RW_IDENTITY,
+  // theory preRewrite, note this is only intended to be used as an argument
+  // to THEORY_REWRITE in the final proof. It is not implemented in
+  // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
+  RW_REWRITE_THEORY_PRE,
+  // same as above, for theory postRewrite
+  RW_REWRITE_THEORY_POST,
+  //---------------------------- Substitutions
+  // (= x y) is interpreted as x -> y, using Node::substitute
+  SB_DEFAULT,
+  // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
+  SB_LITERAL,
+  // P is interpreted as P -> true using Node::substitute
+  SB_FORMULA,
+  //---------------------------- Substitution applications
+  // multiple substitutions are applied sequentially
+  SBA_SEQUENTIAL,
+  // multiple substitutions are applied simultaneously
+  SBA_SIMUL,
+  // multiple substitutions are applied to fix point
+  SBA_FIXPOINT
+  // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to
+  // y gives:
+  // - f(g(x)) for SBA_SEQUENTIAL
+  // - f(z) for SBA_SIMUL
+  // - f(g(u)) for SBA_FIXPOINT
+  // Notice that SBA_FIXPOINT should provide a terminating rewrite system
+  // as a substitution, or else non-termination will occur during proof
+  // checking.
+};
+/** Converts a rewriter id to a string. */
+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);
+
+/** get a method identifier from a node, return false if we fail */
+bool getMethodId(TNode n, MethodId& i);
+/**
+ * Get method identifiers from args starting at the given index. Store their
+ * values into ids, ida, and idr. This method returns false if args does not
+ * contain valid method identifiers at position index in args.
+ */
+bool getMethodIds(const std::vector<Node>& args,
+                  MethodId& ids,
+                  MethodId& ida,
+                  MethodId& idr,
+                  size_t index);
+/**
+ * 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,
+                  MethodId ids,
+                  MethodId ida,
+                  MethodId idr);
+
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__METHOD_ID_H */
diff --git a/src/proof/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp
index f00c664c8..79e98471d 100644
--- a/src/proof/theory_proof_step_buffer.cpp
+++ b/src/proof/theory_proof_step_buffer.cpp
@@ -20,7 +20,6 @@
 using namespace cvc5::kind;
 
 namespace cvc5 {
-namespace theory {
 
 TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
     : ProofStepBuffer(pc)
@@ -36,7 +35,7 @@ bool TheoryProofStepBuffer::applyEqIntro(Node src,
 {
   std::vector<Node> args;
   args.push_back(src);
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
   if (res.isNull())
   {
@@ -73,7 +72,7 @@ bool TheoryProofStepBuffer::applyPredTransform(Node src,
   // try to prove that tgt rewrites to src
   children.insert(children.end(), exp.begin(), exp.end());
   args.push_back(tgt);
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
   if (res.isNull())
   {
@@ -93,7 +92,7 @@ bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
 {
   std::vector<Node> args;
   args.push_back(tgt);
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
   if (res.isNull())
   {
@@ -113,7 +112,7 @@ Node TheoryProofStepBuffer::applyPredElim(Node src,
   children.push_back(src);
   children.insert(children.end(), exp.begin(), exp.end());
   std::vector<Node> args;
-  builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr);
+  addMethodIds(args, ids, ida, idr);
   Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
   if (CDProof::isSame(src, srcRew))
   {
@@ -236,5 +235,4 @@ Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
   return n;
 }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/theory_proof_step_buffer.h b/src/proof/theory_proof_step_buffer.h
index fc2e25e5a..ac58d3718 100644
--- a/src/proof/theory_proof_step_buffer.h
+++ b/src/proof/theory_proof_step_buffer.h
@@ -25,7 +25,6 @@
 #include "theory/builtin/proof_checker.h"
 
 namespace cvc5 {
-namespace theory {
 /**
  * Class used to speculatively try and buffer a set of proof steps before
  * sending them to a proof object, extended with theory-specfic proof rule
@@ -114,7 +113,6 @@ class TheoryProofStepBuffer : public ProofStepBuffer
   Node elimDoubleNegLit(Node n);
 };
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */
diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp
index d99e6de51..6c5de13c7 100644
--- a/src/proof/trust_node.cpp
+++ b/src/proof/trust_node.cpp
@@ -19,7 +19,6 @@
 #include "proof/proof_generator.h"
 
 namespace cvc5 {
-namespace theory {
 
 const char* toString(TrustNodeKind tnk)
 {
@@ -146,5 +145,4 @@ std::ostream& operator<<(std::ostream& out, TrustNode n)
   return out;
 }
 
-}  // namespace theory
 }  // namespace cvc5
diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h
index 200dececd..8971df1d1 100644
--- a/src/proof/trust_node.h
+++ b/src/proof/trust_node.h
@@ -25,8 +25,6 @@ namespace cvc5 {
 class ProofGenerator;
 class ProofNode;
 
-namespace theory {
-
 /** A kind for trust nodes */
 enum class TrustNodeKind : uint32_t
 {
@@ -172,7 +170,6 @@ class TrustNode
  */
 std::ostream& operator<<(std::ostream& out, TrustNode n);
 
-}  // namespace theory
 }  // namespace cvc5
 
 #endif /* CVC5__PROOF__TRUST_NODE_H */