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, 198 deletions

diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h
deleted file mode 100644
index c0b368e6e..000000000
--- a/src/theory/eager_proof_generator.h
+++ /dev/null
@@ -1,198 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Alex Ozdemir, Gereon Kremer
- *
- * 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.
- * ****************************************************************************
- *
- * The eager proof generator class.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__THEORY__EAGER_PROOF_GENERATOR_H
-#define CVC5__THEORY__EAGER_PROOF_GENERATOR_H
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_rule.h"
-#include "theory/trust_node.h"
-
-namespace cvc5 {
-
-class ProofNode;
-class ProofNodeManager;
-
-namespace theory {
-
-/**
- * An eager proof generator, with explicit proof caching.
- *
- * The intended use of this class is to store proofs for lemmas and conflicts
- * at the time they are sent out on the ProofOutputChannel. This means that the
- * getProofForConflict and getProofForLemma methods are lookups in a
- * (user-context depedent) map, the field d_proofs below.
- *
- * In detail, the method setProofForConflict(conf, pf) should be called prior to
- * calling ProofOutputChannel(TrustNode(conf,X)), where X is this generator.
- * Similarly for setProofForLemma.
- *
- * The intended usage of this class in combination with OutputChannel is
- * the following:
- * //-----------------------------------------------------------
- *   class MyEagerProofGenerator : public EagerProofGenerator
- *   {
- *     public:
- *      TrustNode getProvenConflictByMethodX(...)
- *      {
- *        // construct a conflict
- *        Node conf = [construct conflict];
- *        // construct a proof for conf
- *        std::shared_ptr<ProofNode> pf = [construct the proof for conf];
- *        // wrap the conflict in a trust node
- *        return mkTrustNode(conf,pf);
- *      }
- *   };
- *   // [1] Make objects given user context u and output channel out.
- *
- *   MyEagerProofGenerator epg(u);
- *   OutputChannel out;
- *
- *   // [2] Assume epg realizes there is a conflict. We have it store the proof
- *   // internally and return the conflict node paired with epg.
- *
- *   TrustNode pconf = epg.getProvenConflictByMethodX(...);
- *
- *   // [3] Send the conflict on the output channel.
- *
- *   out.trustedConflict(pconf);
- *
- *   // [4] The trust node has information about what is proven and who can
- *   // prove it, where this association is valid in the remainder of the user
- *   // context.
- *
- *   Node conf = pconf.getProven();
- *   ProofGenerator * pg = pconf.getGenerator();
- *   std::shared_ptr<ProofNode> pf = pg->getProofForConflict(conf);
- * //-----------------------------------------------------------
- * In other words, the proof generator epg is responsible for creating and
- * storing the proof internally, and the proof output channel is responsible for
- * maintaining the map that epg is who to ask for the proof of the conflict.
- */
-class EagerProofGenerator : public ProofGenerator
-{
-  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
-
- public:
-  EagerProofGenerator(ProofNodeManager* pnm,
-                      context::Context* c = nullptr,
-                      std::string name = "EagerProofGenerator");
-  ~EagerProofGenerator() {}
-  /** Get the proof for formula f. */
-  std::shared_ptr<ProofNode> getProofFor(Node f) override;
-  /** Can we give the proof for formula f? */
-  bool hasProofFor(Node f) override;
-  /**
-   * Set proof for fact f, called when pf is a proof of f.
-   *
-   * @param f The fact proven by pf,
-   * @param pf The proof to store in this class.
-   */
-  void setProofFor(Node f, std::shared_ptr<ProofNode> pf);
-  /**
-   * Make trust node: wrap n in a trust node with this generator, and have it
-   * store the proof pf to lemma or conflict n.
-   *
-   * @param n The proven node,
-   * @param pf The proof of n,
-   * @param isConflict Whether the returned trust node is a conflict (otherwise
-   * it is a lemma),
-   * @return The trust node corresponding to the fact that this generator has
-   * a proof of n.
-   */
-  TrustNode mkTrustNode(Node n,
-                        std::shared_ptr<ProofNode> pf,
-                        bool isConflict = false);
-  /**
-   * Make trust node from a single step proof. This is a convenience function
-   * that avoids the need to explictly construct ProofNode by the caller.
-   *
-   * @param conc The conclusion of the rule,
-   * @param id The rule of the proof concluding conc
-   * @param exp The explanation (premises) to the proof concluding conc,
-   * @param args The arguments to the proof concluding conc,
-   * @param isConflict Whether the returned trust node is a conflict (otherwise
-   * it is a lemma),
-   * @return The trust node corresponding to the fact that this generator has
-   * a proof of (exp => conc), or of conc if exp is empty.
-   */
-  TrustNode mkTrustNode(Node conc,
-                        PfRule id,
-                        const std::vector<Node>& exp,
-                        const std::vector<Node>& args,
-                        bool isConflict = false);
-  /**
-   * Make trust node: wrap `exp => n` in a trust node with this generator, and
-   * have it store the proof `pf` too.
-   *
-   * @param n The implication
-   * @param exp A conjunction of literals that imply it
-   * @param pf The proof of exp => n,
-   * @return The trust node corresponding to the fact that this generator has
-   * a proof of exp => n.
-   */
-  TrustNode mkTrustedPropagation(Node n,
-                                 Node exp,
-                                 std::shared_ptr<ProofNode> pf);
-  /**
-   * Make trust node: `a = b` as a Rewrite trust node
-   *
-   * @param a the original
-   * @param b what is rewrites to
-   * @param pf The proof of a = b,
-   * @return The trust node corresponding to the fact that this generator has
-   * a proof of a = b
-   */
-  TrustNode mkTrustedRewrite(
-      Node a, Node b, std::shared_ptr<ProofNode> pf);
-  //--------------------------------------- common proofs
-  /**
-   * This returns the trust node corresponding to the splitting lemma
-   * (or f (not f)) and this generator. The method registers its proof in the
-   * map maintained by this class.
-   */
-  TrustNode mkTrustNodeSplit(Node f);
-  //--------------------------------------- end common proofs
-  /** identify */
-  std::string identify() const override;
-
- protected:
-  /** Set that pf is the proof for conflict conf */
-  void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf);
-  /** Set that pf is the proof for lemma lem */
-  void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf);
-  /** Set that pf is the proof for explained propagation */
-  void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf);
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
-  /** Name identifier */
-  std::string d_name;
-  /** A dummy context used by this class if none is provided */
-  context::Context d_context;
-  /**
-   * A user-context-dependent map from lemmas and conflicts to proofs provided
-   * by calls to setProofForConflict and setProofForLemma above.
-   */
-  NodeProofNodeMap d_proofs;
-};
-
-}  // namespace theory
-}  // namespace cvc5
-
-#endif /* CVC5__THEORY__PROOF_GENERATOR_H */