(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.

2 files changed, 271 insertions, 93 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 89091d309..3f44e592e 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -18,6 +18,7 @@
 #include <vector>
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/proof_options.h"
 #include "proof/proof_manager.h"
 
@@ -26,44 +27,51 @@ using namespace std;
 namespace CVC4 {
 
 RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
-    : d_tfCache(u), d_skolem_cache(u)
+    : d_tfCache(u),
+      d_skolem_cache(u),
+      d_pnm(nullptr),
+      d_tpg(nullptr),
+      d_lp(nullptr)
 {
 }
 
 RemoveTermFormulas::~RemoveTermFormulas() {}
 
-void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
+theory::TrustNode RemoveTermFormulas::run(
+    Node assertion,
+    std::vector<theory::TrustNode>& newAsserts,
+    std::vector<Node>& newSkolems,
+    bool reportDeps)
 {
-  size_t n = output.size();
-  for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
-    // Do this in two steps to avoid Node problems(?)
-    // Appears related to bug 512, splitting this into two lines
-    // fixes the bug on clang on Mac OS
-    Node itesRemoved = run(output[i], output, iteSkolemMap, false, false);
-    // In some calling contexts, not necessary to report dependence information.
-    if (reportDeps &&
-        (options::unsatCores() || options::fewerPreprocessingHoles())) {
-      // new assertions have a dependence on the node
-      PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
-      while(n < output.size()) {
-        PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
-        ++n;
-      }
+  Node itesRemoved = run(assertion, newAsserts, newSkolems, false, false);
+  // In some calling contexts, not necessary to report dependence information.
+  if (reportDeps
+      && (options::unsatCores() || options::fewerPreprocessingHoles()))
+  {
+    // new assertions have a dependence on the node
+    PROOF(ProofManager::currentPM()->addDependence(itesRemoved, assertion);)
+    unsigned n = 0;
+    while (n < newAsserts.size())
+    {
+      PROOF(ProofManager::currentPM()->addDependence(newAsserts[n].getProven(),
+                                                     assertion);)
+      ++n;
     }
-    output[i] = itesRemoved;
   }
+  // The rewriting of assertion can be justified by the term conversion proof
+  // generator d_tpg.
+  return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
 }
 
-Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
-                    IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) {
+Node RemoveTermFormulas::run(TNode node,
+                             std::vector<theory::TrustNode>& output,
+                             std::vector<Node>& newSkolems,
+                             bool inQuant,
+                             bool inTerm)
+{
   // Current node
   Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl;
 
-  //if(node.isVar() || node.isConst()){
-  //   (options::biasedITERemoval() && !containsTermITE(node))){
-  //if(node.isVar()){
-  //  return Node(node);
-  //}
   if( node.getKind()==kind::INST_PATTERN_LIST ){
     return Node(node);
   }
@@ -84,6 +92,8 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   TypeNode nodeType = node.getType();
   Node skolem;
   Node newAssertion;
+  // the exists form of the assertion
+  ProofGenerator* newAssertionPg = nullptr;
   // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled
   // in the "non-variable Boolean term within term" case below.
   if (node.getKind() == kind::ITE && !nodeType.isBoolean())
@@ -96,15 +106,39 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
       if (skolem.isNull())
       {
         // Make the skolem to represent the ITE
-        skolem = nodeManager->mkSkolem(
+        SkolemManager* sm = nodeManager->getSkolemManager();
+        skolem = sm->mkPurifySkolem(
+            node,
             "termITE",
-            nodeType,
             "a variable introduced due to term-level ITE removal");
         d_skolem_cache.insert(node, skolem);
 
         // The new assertion
         newAssertion = nodeManager->mkNode(
             kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
+
+        // we justify it internally
+        if (isProofEnabled())
+        {
+          // ---------------------- REMOVE_TERM_FORMULA_AXIOM
+          // (ite node[0]
+          //      (= node node[1])            ------------- MACRO_SR_PRED_INTRO
+          //      (= node node[2]))           node = skolem
+          // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
+          // (ite node[0] (= skolem node[1]) (= skolem node[2]))
+          //
+          // Note that the MACRO_SR_PRED_INTRO step holds due to conversion
+          // of skolem into its witness form, which is node.
+          Node axiom = getAxiomFor(node);
+          d_lp->addStep(axiom, PfRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node});
+          Node eq = node.eqNode(skolem);
+          d_lp->addStep(eq, PfRule::MACRO_SR_PRED_INTRO, {}, {eq});
+          d_lp->addStep(newAssertion,
+                        PfRule::MACRO_SR_PRED_TRANSFORM,
+                        {axiom, eq},
+                        {newAssertion});
+          newAssertionPg = d_lp.get();
+        }
       }
     }
   }
@@ -117,9 +151,10 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
       if (skolem.isNull())
       {
         // Make the skolem to represent the lambda
-        skolem = nodeManager->mkSkolem(
+        SkolemManager* sm = nodeManager->getSkolemManager();
+        skolem = sm->mkPurifySkolem(
+            node,
             "lambdaF",
-            nodeType,
             "a function introduced due to term-level lambda removal");
         d_skolem_cache.insert(node, skolem);
 
@@ -135,6 +170,15 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
         children.push_back(skolem_app.eqNode(node[1]));
         // axiom defining skolem
         newAssertion = nodeManager->mkNode(kind::FORALL, children);
+
+        // Lambda lifting is trivial to justify, hence we don't set a proof
+        // generator here. In particular, replacing the skolem introduced
+        // here with its original lambda ensures the new assertion rewrites
+        // to true.
+        // For example, if (lambda y. t[y]) has skolem k, then this lemma is:
+        //   forall x. k(x)=t[x]
+        // whose witness form rewrites
+        //   forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true
       }
     }
   }
@@ -148,10 +192,12 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
       skolem = getSkolemForNode(node);
       if (skolem.isNull())
       {
-        // Make the skolem to witness the choice
-        skolem = nodeManager->mkSkolem(
+        // Make the skolem to witness the choice, which notice is handled
+        // as a special case within SkolemManager::mkPurifySkolem.
+        SkolemManager* sm = nodeManager->getSkolemManager();
+        skolem = sm->mkPurifySkolem(
+            node,
             "witnessK",
-            nodeType,
             "a skolem introduced due to term-level witness removal");
         d_skolem_cache.insert(node, skolem);
 
@@ -160,6 +206,27 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
         // The new assertion is the assumption that the body
         // of the witness operator holds for the Skolem
         newAssertion = node[1].substitute(node[0][0], skolem);
+
+        // Get the proof generator, if one exists, which was responsible for
+        // constructing this witness term. This may not exist, in which case
+        // the witness term was trivial to justify. This is the case e.g. for
+        // purification witness terms.
+        if (isProofEnabled())
+        {
+          Node existsAssertion =
+              nodeManager->mkNode(kind::EXISTS, node[0], node[1]);
+          // -------------------- from skolem manager
+          // (exists x. node[1])
+          // -------------------- SKOLEMIZE
+          // node[1] * { x -> skolem }
+          ProofGenerator* expg = sm->getProofGenerator(existsAssertion);
+          if (expg != nullptr)
+          {
+            d_lp->addLazyStep(existsAssertion, expg);
+          }
+          d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {});
+          newAssertionPg = d_lp.get();
+        }
       }
     }
   }
@@ -175,12 +242,23 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
       // Skolems introduced for Boolean formulas appearing in terms have a
       // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled
       // properly in theory combination. We must use this kind here instead of a
-      // generic skolem.
-      skolem = nodeManager->mkBooleanTermVariable();
+      // generic skolem. Notice that the name/comment are currently ignored
+      // within SkolemManager::mkPurifySkolem, since BOOLEAN_TERM_VARIABLE
+      // variables cannot be given names.
+      SkolemManager* sm = nodeManager->getSkolemManager();
+      skolem = sm->mkPurifySkolem(
+          node,
+          "btvK",
+          "a Boolean term variable introduced during term formula removal",
+          NodeManager::SKOLEM_BOOL_TERM_VAR);
       d_skolem_cache.insert(node, skolem);
 
       // The new assertion
       newAssertion = skolem.eqNode(node);
+
+      // Boolean term removal is trivial to justify, hence we don't set a proof
+      // generator here. It is trivial to justify since it is an instance of
+      // purification, which is justified by conversion to witness forms.
     }
   }
 
@@ -192,15 +270,43 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
     // if the skolem was introduced in this call
     if (!newAssertion.isNull())
     {
+      // if proofs are enabled
+      if (isProofEnabled())
+      {
+        // justify the introduction of the skolem
+        // ------------------- MACRO_SR_PRED_INTRO
+        // t = witness x. x=t
+        // The above step is trivial, since the skolems introduced above are
+        // all purification skolems. We record this equality in the term
+        // conversion proof generator.
+        d_tpg->addRewriteStep(node,
+                              skolem,
+                              PfRule::MACRO_SR_PRED_INTRO,
+                              {},
+                              {node.eqNode(skolem)});
+        // justify the axiom that defines the skolem, if not already done so
+        if (newAssertionPg == nullptr)
+        {
+          // Should have trivial justification if not yet provided. This is the
+          // case of lambda lifting and Boolean term removal.
+          // ---------------- MACRO_SR_PRED_INTRO
+          // newAssertion
+          d_lp->addStep(
+              newAssertion, PfRule::MACRO_SR_PRED_INTRO, {}, {newAssertion});
+        }
+      }
       Debug("ite") << "*** term formula removal introduced " << skolem
                    << " for " << node << std::endl;
 
       // Remove ITEs from the new assertion, rewrite it and push it to the
       // output
-      newAssertion = run(newAssertion, output, iteSkolemMap, false, false);
+      newAssertion = run(newAssertion, output, newSkolems, false, false);
+
+      theory::TrustNode trna =
+          theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
 
-      iteSkolemMap[skolem] = output.size();
-      output.push_back(newAssertion);
+      output.push_back(trna);
+      newSkolems.push_back(skolem);
     }
 
     // The representation is now the skolem
@@ -225,7 +331,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   }
   // Remove the ITEs from the children
   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-    Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm);
+    Node newChild = run(*it, output, newSkolems, inQuant, inTerm);
     somethingChanged |= (newChild != *it);
     newChildren.push_back(newChild);
   }
@@ -305,4 +411,27 @@ bool RemoveTermFormulas::hasNestedTermChildren( TNode node ) {
          // dont' worry about FORALL or EXISTS (handled separately)
 }
 
+Node RemoveTermFormulas::getAxiomFor(Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Kind k = n.getKind();
+  if (k == kind::ITE)
+  {
+    return nm->mkNode(kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2]));
+  }
+  return Node::null();
+}
+
+void RemoveTermFormulas::setProofChecker(ProofChecker* pc)
+{
+  if (d_tpg == nullptr)
+  {
+    d_pnm.reset(new ProofNodeManager(pc));
+    d_tpg.reset(new TConvProofGenerator(d_pnm.get()));
+    d_lp.reset(new LazyCDProof(d_pnm.get()));
+  }
+}
+
+bool RemoveTermFormulas::isProofEnabled() const { return d_pnm != nullptr; }
+
 }/* CVC4 namespace */
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 */