(proof-new) Proof production for term formula removal (#4687)

This adds proof support in the term formula removal pass.

It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.

1 files changed, 104 insertions, 55 deletions

diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 9ec12cb12..d4c22b78b 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -23,8 +23,12 @@
 
 #include "context/cdinsert_hashmap.h"
 #include "context/context.h"
+#include "expr/lazy_proof.h"
 #include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "smt/dump.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/trust_node.h"
 #include "util/bool.h"
 #include "util/hash.h"
 
@@ -33,6 +37,89 @@ namespace CVC4 {
 typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
 class RemoveTermFormulas {
+ public:
+  RemoveTermFormulas(context::UserContext* u);
+  ~RemoveTermFormulas();
+
+  /**
+   * By introducing skolem variables, this function removes all occurrences of:
+   * (1) term ITEs,
+   * (2) terms of type Boolean that are not Boolean term variables,
+   * (3) lambdas, and
+   * (4) Hilbert choice expressions.
+   * from assertions.
+   * All additional assertions are pushed into assertions. iteSkolemMap
+   * contains a map from introduced skolem variables to the index in
+   * assertions containing the new definition created in conjunction
+   * with that skolem variable.
+   *
+   * As an example of (1):
+   *   f( (ite C 0 1)) = 2
+   * becomes
+   *   f( k ) = 2 ^ ite( C, k=0, k=1 )
+   *
+   * As an example of (2):
+   *   g( (and C1 C2) ) = 3
+   * becomes
+   *   g( k ) = 3 ^ ( k <=> (and C1 C2) )
+   *
+   * As an example of (3):
+   *   (lambda x. t[x]) = f
+   * becomes
+   *   (forall x. k(x) = t[x]) ^ k = f
+   * where k is a fresh skolem function.
+   * This is sometimes called "lambda lifting"
+   *
+   * As an example of (4):
+   *   (witness x. P( x ) ) = t
+   * becomes
+   *   P( k ) ^ k = t
+   * where k is a fresh skolem constant.
+   *
+   * With reportDeps true, report reasoning dependences to the proof
+   * manager (for unsat cores).
+   *
+   * @param assertion The assertion to remove term formulas from
+   * @param newAsserts The new assertions corresponding to axioms for newly
+   * introduced skolems.
+   * @param newSkolems The skolems corresponding to each of the newAsserts.
+   * @param reportDeps Used for unsat cores in the old proof infrastructure.
+   * @return a trust node of kind TrustNodeKind::REWRITE whose
+   * right hand side is assertion after removing term formulas, and the proof
+   * generator (if provided) that can prove the equivalence.
+   */
+  theory::TrustNode run(Node assertion,
+                        std::vector<theory::TrustNode>& newAsserts,
+                        std::vector<Node>& newSkolems,
+                        bool reportDeps = false);
+
+  /**
+   * Substitute under node using pre-existing cache.  Do not remove
+   * any ITEs not seen during previous runs.
+   */
+  Node replace(TNode node, bool inQuant = false, bool inTerm = false) const;
+
+  /** Returns true if e contains a term ite. */
+  bool containsTermITE(TNode e) const;
+
+  /** Garbage collects non-context dependent data-structures. */
+  void garbageCollect();
+
+  /**
+   * Set proof checker, which signals this class to enable proofs using the
+   * given checker.
+   */
+  void setProofChecker(ProofChecker* pc);
+
+  /**
+   * Get axiom for term n. This returns the axiom that this class uses to
+   * eliminate the term n, which is determined by its top-most symbol. For
+   * example, if n is (ite n1 n2 n3), this returns the formula:
+   *   (ite n1 (= (ite n1 n2 n3) n2) (= (ite n1 n2 n3) n3))
+   */
+  static Node getAxiomFor(Node n);
+
+ private:
   typedef context::
       CDInsertHashMap<std::pair<Node, int>,
                       Node,
@@ -77,50 +164,18 @@ class RemoveTermFormulas {
   inline Node getSkolemForNode(Node node) const;
 
   static bool hasNestedTermChildren( TNode node );
-public:
-
-  RemoveTermFormulas(context::UserContext* u);
-  ~RemoveTermFormulas();
 
+  /** A proof node manager */
+  std::unique_ptr<ProofNodeManager> d_pnm;
   /**
-   * By introducing skolem variables, this function removes all occurrences of:
-   * (1) term ITEs,
-   * (2) terms of type Boolean that are not Boolean term variables,
-   * (3) lambdas, and
-   * (4) Hilbert choice expressions.
-   * from assertions.
-   * All additional assertions are pushed into assertions. iteSkolemMap
-   * contains a map from introduced skolem variables to the index in
-   * assertions containing the new definition created in conjunction
-   * with that skolem variable.
-   *
-   * As an example of (1):
-   *   f( (ite C 0 1)) = 2
-   * becomes
-   *   f( k ) = 2 ^ ite( C, k=0, k=1 )
-   *
-   * As an example of (2):
-   *   g( (and C1 C2) ) = 3
-   * becomes
-   *   g( k ) = 3 ^ ( k <=> (and C1 C2) )
-   *
-   * As an example of (3):
-   *   (lambda x. t[x]) = f
-   * becomes
-   *   (forall x. k(x) = t[x]) ^ k = f
-   * where k is a fresh skolem function.
-   * This is sometimes called "lambda lifting"
-   *
-   * As an example of (4):
-   *   (witness x. P( x ) ) = t
-   * becomes
-   *   P( k ) ^ k = t
-   * where k is a fresh skolem constant.
-   *
-   * With reportDeps true, report reasoning dependences to the proof
-   * manager (for unsat cores).
+   * A proof generator for the term conversion.
    */
-  void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
+  std::unique_ptr<TConvProofGenerator> d_tpg;
+  /**
+   * A proof generator for skolems we introduce that are based on axioms that
+   * this class is responsible for.
+   */
+  std::unique_ptr<LazyCDProof> d_lp;
 
   /**
    * Removes terms of the form (1), (2), (3) described above from node.
@@ -133,20 +188,14 @@ public:
    * inTerm is whether we are are processing node in a "term" position, that is, it is a subterm
    *        of a parent term that is not a Boolean connective.
    */
-  Node run(TNode node, std::vector<Node>& additionalAssertions,
-           IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm);
-
-  /**
-   * Substitute under node using pre-existing cache.  Do not remove
-   * any ITEs not seen during previous runs.
-   */
-  Node replace(TNode node, bool inQuant = false, bool inTerm = false) const;
-
-  /** Returns true if e contains a term ite. */
-  bool containsTermITE(TNode e) const;
-
-  /** Garbage collects non-context dependent data-structures. */
-  void garbageCollect();
+  Node run(TNode node,
+           std::vector<theory::TrustNode>& newAsserts,
+           std::vector<Node>& newSkolems,
+           bool inQuant,
+           bool inTerm);
+
+  /** Whether proofs are enabled */
+  bool isProofEnabled() const;
 };/* class RemoveTTE */
 
 }/* CVC4 namespace */