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

4 files changed, 71 insertions, 28 deletions

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 59f405337..817d21fdf 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -15,6 +15,7 @@
 #include "theory/builtin/proof_checker.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/term_formula_removal.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
@@ -61,6 +62,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
   pc->registerChecker(PfRule::THEORY_REWRITE, this);
   pc->registerChecker(PfRule::PREPROCESS, this);
+  pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
 }
 
 Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite)
@@ -321,6 +323,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     }
     return args[0];
   }
+  else if (id == PfRule::REMOVE_TERM_FORMULA_AXIOM)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    return RemoveTermFormulas::getAxiomFor(args[0]);
+  }
   else if (id == PfRule::PREPROCESS)
   {
     Assert(children.empty());
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 70e744acf..9955be850 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1610,10 +1610,25 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                      << CheckSatCommand(n.toExpr());
   }
 
-  // the assertion pipeline storing the lemmas
-  AssertionPipeline lemmas;
   // call preprocessor
-  d_tpp.preprocess(node, lemmas, preprocess);
+  std::vector<TrustNode> newLemmas;
+  std::vector<Node> newSkolems;
+  TrustNode tlemma = d_tpp.preprocess(node, newLemmas, newSkolems, preprocess);
+
+  // must use an assertion pipeline due to decision engine below
+  AssertionPipeline lemmas;
+  // make the assertion pipeline
+  lemmas.push_back(tlemma.getNode());
+  lemmas.updateRealAssertionsEnd();
+  Assert(newSkolems.size() == newLemmas.size());
+  for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
+  {
+    // store skolem mapping here
+    IteSkolemMap& imap = lemmas.getIteSkolemMap();
+    imap[newSkolems[i]] = lemmas.size();
+    lemmas.push_back(newLemmas[i].getNode());
+  }
+
   // assert lemmas to prop engine
   for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
   {
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index b12916b7d..328c65fcb 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -36,41 +36,52 @@ TheoryPreprocessor::~TheoryPreprocessor() {}
 
 void TheoryPreprocessor::clearCache() { d_ppCache.clear(); }
 
-void TheoryPreprocessor::preprocess(TNode node,
-                                    preprocessing::AssertionPipeline& lemmas,
-                                    bool doTheoryPreprocess)
+TrustNode TheoryPreprocessor::preprocess(TNode node,
+                                         std::vector<TrustNode>& newLemmas,
+                                         std::vector<Node>& newSkolems,
+                                         bool doTheoryPreprocess)
 {
   // Run theory preprocessing, maybe
   Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node);
 
   // Remove the ITEs
   Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl;
-  lemmas.push_back(ppNode);
-  lemmas.updateRealAssertionsEnd();
-  d_tfr.run(lemmas.ref(), lemmas.getIteSkolemMap());
-  Trace("te-tform-rm") << "..done " << lemmas[0] << std::endl;
+  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false);
+  Trace("te-tform-rm") << "..done " << ttfr.getNode() << std::endl;
+  Node retNode = ttfr.getNode();
 
   if (Debug.isOn("lemma-ites"))
   {
-    Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
-    Debug("lemma-ites") << " + now have the following " << lemmas.size()
+    Debug("lemma-ites") << "removed ITEs from lemma: " << ttfr.getNode()
+                        << endl;
+    Debug("lemma-ites") << " + now have the following " << newLemmas.size()
                         << " lemma(s):" << endl;
-    for (std::vector<Node>::const_iterator i = lemmas.begin();
-         i != lemmas.end();
-         ++i)
+    for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i)
     {
-      Debug("lemma-ites") << " + " << *i << endl;
+      Debug("lemma-ites") << " + " << newLemmas[i].getNode() << endl;
     }
     Debug("lemma-ites") << endl;
   }
 
+  retNode = Rewriter::rewrite(retNode);
+
   // now, rewrite the lemmas
-  Node retLemma;
-  for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
+  for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
   {
-    Node rewritten = Rewriter::rewrite(lemmas[i]);
-    lemmas.replace(i, rewritten);
+    // get the trust node to process
+    TrustNode trn = newLemmas[i];
+    Assert(trn.getKind() == TrustNodeKind::LEMMA);
+    Node assertion = trn.getNode();
+    // rewrite, which is independent of d_tpg, since additional lemmas
+    // are justified separately.
+    Node rewritten = Rewriter::rewrite(assertion);
+    if (assertion != rewritten)
+    {
+      // not tracking proofs, just make new
+      newLemmas[i] = TrustNode::mkTrustLemma(rewritten, nullptr);
+    }
   }
+  return TrustNode::mkTrustRewrite(node, retNode, nullptr);
 }
 
 struct preprocess_stack_element
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 2488cf162..2f3813e68 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -46,15 +46,24 @@ class TheoryPreprocessor
   /** Clear the cache of this class */
   void clearCache();
   /**
-   * Preprocesses node and stores it along with lemmas generated by
-   * preprocessing into the assertion pipeline lemmas. The (optional) argument
-   * lcp is the proof that stores a proof of all top-level formulas in lemmas,
-   * assuming that lcp initially contains a proof of node. The flag
-   * doTheoryPreprocess is whether we should run theory-specific preprocessing.
+   * Preprocesses the given assertion node. It returns a TrustNode of kind
+   * TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores
+   * additional lemmas in newLemmas, which are trust nodes of kind
+   * TrustNodeKind::LEMMA. These correspond to e.g. lemmas corresponding to ITE
+   * removal. For each lemma in newLemmas, we add the corresponding skolem that
+   * the lemma defines. The flag doTheoryPreprocess is whether we should run
+   * theory-specific preprocessing.
+   *
+   * @param node The assertion to preprocess,
+   * @param newLemmas The lemmas to add to the set of assertions,
+   * @param newSkolems The skolems that newLemmas correspond to,
+   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
+   * @return The trust node corresponding to rewriting node via preprocessing.
    */
-  void preprocess(TNode node,
-                  preprocessing::AssertionPipeline& lemmas,
-                  bool doTheoryPreprocess);
+  TrustNode preprocess(TNode node,
+                       std::vector<TrustNode>& newLemmas,
+                       std::vector<Node>& newSkolems,
+                       bool doTheoryPreprocess);
   /**
    * Runs theory specific preprocessing on the non-Boolean parts of
    * the formula.  This is only called on input assertions, after ITEs