Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

1 files changed, 0 insertions, 145 deletions

diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
deleted file mode 100644
index f8d71f703..000000000
--- a/src/expr/proof_node.h
+++ /dev/null
@@ -1,145 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
- *
- * 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.
- * ****************************************************************************
- *
- * Proof node utility.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__EXPR__PROOF_NODE_H
-#define CVC5__EXPR__PROOF_NODE_H
-
-#include <vector>
-
-#include "expr/node.h"
-#include "expr/proof_rule.h"
-
-namespace cvc5 {
-
-class ProofNodeManager;
-class ProofNode;
-
-// Alias for shared pointer to a proof node
-using Pf = std::shared_ptr<ProofNode>;
-
-struct ProofNodeHashFunction
-{
-  inline size_t operator()(std::shared_ptr<ProofNode> pfn) const;
-}; /* struct ProofNodeHashFunction */
-
-/** A node in a proof
- *
- * A ProofNode represents a single step in a proof. It contains:
- * (1) d_id, an identifier indicating the kind of inference,
- * (2) d_children, the child ProofNode objects indicating its premises,
- * (3) d_args, additional arguments used to determine the conclusion,
- * (4) d_proven, cache of the formula that this ProofNode proves.
- *
- * Overall, a ProofNode and its children form a directed acyclic graph.
- *
- * A ProofNode is partially mutable in that (1), (2) and (3) can be
- * modified. A motivating example of when this is useful is when a ProofNode
- * is established to be a "hole" for something to be proven later. On the other
- * hand, (4) is intended to be immutable.
- *
- * The method setValue is private and can be called by objects that manage
- * ProofNode objects in trusted ways that ensure that the node maintains
- * the invariant above. Furthermore, notice that this class is not responsible
- * for setting d_proven; this is done externally by a ProofNodeManager class.
- *
- * Notice that all fields of ProofNode are stored in ***Skolem form***. Their
- * correctness is checked in ***witness form*** (for details on this
- * terminology, see expr/skolem_manager.h). As a simple example, say a
- * theory solver has a term t, and wants to introduce a unit lemma (= k t)
- * where k is a fresh Skolem variable. It creates this variable via:
- *   k = SkolemManager::mkPurifySkolem(t,"k");
- * A checked ProofNode for the fact (= k t) then may have fields:
- *   d_rule := MACRO_SR_PRED_INTRO,
- *   d_children := {},
- *   d_args := {(= k t)}
- *   d_proven := (= k t).
- * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation
- * in theory/builtin/proof_kinds) is in terms of the witness form of the
- * argument:
- *   (= (witness ((z T)) (= z t)) t)
- * which, by that rule's side condition, is such that:
- *   Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true.
- * Notice that the correctness of the rule is justified here by rewriting
- * the witness form of (= k t). The conversion to/from witness form is
- * managed by ProofRuleChecker::check.
- *
- * An external proof checker is expected to formalize the ProofNode only in
- * terms of *witness* forms.
- *
- * However, the rest of cvc5 sees only the *Skolem* form of arguments and
- * conclusions in ProofNode, since this is what is used throughout cvc5.
- */
-class ProofNode
-{
-  friend class ProofNodeManager;
-
- public:
-  ProofNode(PfRule id,
-            const std::vector<std::shared_ptr<ProofNode>>& children,
-            const std::vector<Node>& args);
-  ~ProofNode() {}
-  /** get the rule of this proof node */
-  PfRule getRule() const;
-  /** Get children */
-  const std::vector<std::shared_ptr<ProofNode>>& getChildren() const;
-  /** Get arguments */
-  const std::vector<Node>& getArguments() const;
-  /** get what this node proves, or the null node if this is an invalid proof */
-  Node getResult() const;
-  /**
-   * Returns true if this is a closed proof (i.e. it has no free assumptions).
-   */
-  bool isClosed();
-  /** Print debug on output strem os */
-  void printDebug(std::ostream& os) const;
-
- private:
-  /**
-   * Set value, called to overwrite the contents of this ProofNode with the
-   * given arguments.
-   */
-  void setValue(PfRule id,
-                const std::vector<std::shared_ptr<ProofNode>>& children,
-                const std::vector<Node>& args);
-  /** The proof rule */
-  PfRule d_rule;
-  /** The children of this proof node */
-  std::vector<std::shared_ptr<ProofNode>> d_children;
-  /** arguments of this node */
-  std::vector<Node> d_args;
-  /** The cache of the fact that has been proven, modifiable by ProofChecker */
-  Node d_proven;
-};
-
-inline size_t ProofNodeHashFunction::operator()(
-    std::shared_ptr<ProofNode> pfn) const
-{
-  return pfn->getResult().getId() + static_cast<unsigned>(pfn->getRule());
-}
-
-/**
- * Serializes a given proof node to the given stream.
- *
- * @param out the output stream to use
- * @param pn the proof node to output to the stream
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const ProofNode& pn);
-
-}  // namespace cvc5
-
-#endif /* CVC5__EXPR__PROOF_NODE_H */