Merge branch 'master' into regDisableProofs

6 files changed, 251 insertions, 49 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index be8aaea9b..0a45c6790 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -32,9 +32,13 @@ const char* toString(PfRule id)
     case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
     case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
+    case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
+    //================================================= Trusted rules
     case PfRule::PREPROCESS: return "PREPROCESS";
+    case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
+    case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
+    case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
     case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
-    case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
     //================================================= Boolean rules
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index a83e043bf..59c406d28 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -174,29 +174,35 @@ enum class PfRule : uint32_t
   THEORY_REWRITE,
 
   //================================================= Processing rules
-  // ======== Preprocess (trusted)
+  // ======== Remove Term Formulas Axiom
+  // Children: none
+  // Arguments: (t)
+  // ---------------------------------------------------------------
+  // Conclusion: RemoveTermFormulas::getAxiomFor(t).
+  REMOVE_TERM_FORMULA_AXIOM,
+
+  //================================================= Trusted rules
+  // The rules in this section have the signature of a "trusted rule":
+  //
   // Children: none
   // Arguments: (F)
   // ---------------------------------------------------------------
   // Conclusion: F
+  //
   // where F is an equality of the form t = t' where t was replaced by t'
   // based on some preprocessing pass, or otherwise F was added as a new
   // assertion by some preprocessing pass.
   PREPROCESS,
-  // ======== Witness axiom (trusted)
-  // Children: none
-  // Arguments: (F)
-  // ---------------------------------------------------------------
-  // Conclusion: F
+  // where F was added as a new assertion by some preprocessing pass.
+  PREPROCESS_LEMMA,
+  // where F is an equality of the form t = Theory::ppRewrite(t) for some
+  // theory. Notice this is a "trusted" rule.
+  THEORY_PREPROCESS,
+  // where F was added as a new assertion by theory preprocessing.
+  THEORY_PREPROCESS_LEMMA,
   // where F is an existential (exists ((x T)) (P x)) used for introducing
   // a witness term (witness ((x T)) (P x)).
   WITNESS_AXIOM,
-  // ======== Remove Term Formulas Axiom
-  // Children: none
-  // Arguments: (t)
-  // ---------------------------------------------------------------
-  // Conclusion: RemoveTermFormulas::getAxiomFor(t).
-  REMOVE_TERM_FORMULA_AXIOM,
 
   //================================================= Boolean rules
   // ======== Split
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 05c17dedf..7521d116e 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -61,9 +61,13 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
   pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
   pc->registerChecker(PfRule::THEORY_REWRITE, this);
-  pc->registerChecker(PfRule::PREPROCESS, this);
-  pc->registerChecker(PfRule::WITNESS_AXIOM, this);
   pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this);
+  // trusted rules
+  pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2);
+  pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2);
+  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2);
+  pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 2);
+  pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2);
 }
 
 Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite)
@@ -330,7 +334,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Assert(args.size() == 1);
     return RemoveTermFormulas::getAxiomFor(args[0]);
   }
-  else if (id == PfRule::PREPROCESS || id == PfRule::WITNESS_AXIOM)
+  else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA
+           || id == PfRule::THEORY_PREPROCESS
+           || id == PfRule::THEORY_PREPROCESS_LEMMA
+           || id == PfRule::WITNESS_AXIOM)
   {
     Assert(children.empty());
     Assert(args.size() == 1);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e86a09112..f8694e760 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -980,7 +980,13 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
 void TheoryEngine::preprocessStart() { d_tpp.clearCache(); }
 
 Node TheoryEngine::preprocess(TNode assertion) {
-  return d_tpp.theoryPreprocess(assertion);
+  TrustNode trn = d_tpp.theoryPreprocess(assertion);
+  if (trn.isNull())
+  {
+    // no change
+    return assertion;
+  }
+  return trn.getNode();
 }
 
 void TheoryEngine::notifyPreprocessedAssertions(
@@ -1633,6 +1639,12 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   std::vector<Node> newSkolems;
   TrustNode tlemma = d_tpp.preprocess(node, newLemmas, newSkolems, preprocess);
 
+  // !!!!!!! temporary, until this method is fully updated from proof-new
+  if (tlemma.isNull())
+  {
+    tlemma = TrustNode::mkTrustLemma(node);
+  }
+
   // must use an assertion pipeline due to decision engine below
   AssertionPipeline lemmas;
   // make the assertion pipeline
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 328c65fcb..6e569508b 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/theory_preprocessor.h"
 
+#include "expr/lazy_proof.h"
+#include "expr/skolem_manager.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -24,31 +26,90 @@ namespace CVC4 {
 namespace theory {
 
 TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
-                                       RemoveTermFormulas& tfr)
+                                       RemoveTermFormulas& tfr,
+                                       ProofNodeManager* pnm)
     : d_engine(engine),
       d_logicInfo(engine.getLogicInfo()),
       d_ppCache(),
-      d_tfr(tfr)
+      d_tfr(tfr),
+      d_pfContext(),
+      d_tpg(pnm ? new TConvProofGenerator(
+                      pnm,
+                      &d_pfContext,
+                      TConvPolicy::FIXPOINT,
+                      TConvCachePolicy::NEVER,
+                      "TheoryPreprocessor::TConvProofGenerator")
+                : nullptr),
+      d_lp(pnm ? new LazyCDProof(pnm,
+                                 nullptr,
+                                 &d_pfContext,
+                                 "TheoryPreprocessor::LazyCDProof")
+               : nullptr)
 {
+  if (isProofEnabled())
+  {
+    // enable proofs in the term formula remover
+    d_tfr.setProofNodeManager(pnm);
+    // push the proof context, since proof steps may be cleared on calls to
+    // clearCache() below.
+    d_pfContext.push();
+  }
 }
 
 TheoryPreprocessor::~TheoryPreprocessor() {}
 
-void TheoryPreprocessor::clearCache() { d_ppCache.clear(); }
+void TheoryPreprocessor::clearCache()
+{
+  d_ppCache.clear();
+  // clear proofs from d_tpg and d_lp using internal push/pop context
+  if (isProofEnabled())
+  {
+    d_pfContext.pop();
+    d_pfContext.push();
+  }
+}
 
 TrustNode TheoryPreprocessor::preprocess(TNode node,
                                          std::vector<TrustNode>& newLemmas,
                                          std::vector<Node>& newSkolems,
                                          bool doTheoryPreprocess)
 {
+  // In this method, all rewriting steps of node are stored in d_tpg.
+
+  Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: start " << node
+                           << std::endl;
   // Run theory preprocessing, maybe
-  Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node);
+  Node ppNode = node;
+  if (doTheoryPreprocess)
+  {
+    // run theory preprocessing
+    TrustNode tpp = theoryPreprocess(node);
+    ppNode = tpp.getNode();
+  }
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: after preprocessing " << ppNode
+      << std::endl;
 
   // Remove the ITEs
   Trace("te-tform-rm") << "Remove term formulas from " << ppNode << 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 (isProofEnabled())
+  {
+    // if we rewrote
+    if (retNode != ppNode)
+    {
+      // should always have provided a proof generator, or else term formula
+      // removal and this class do not agree on whether proofs are enabled.
+      Assert(ttfr.getGenerator() != nullptr);
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (term formula removal) "
+          << ppNode << " -> " << retNode << std::endl;
+      // store as a rewrite in d_tpg
+      d_tpg->addRewriteStep(ppNode, retNode, ttfr.getGenerator());
+    }
+  }
 
   if (Debug.isOn("lemma-ites"))
   {
@@ -62,14 +123,25 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     }
     Debug("lemma-ites") << endl;
   }
-
-  retNode = Rewriter::rewrite(retNode);
+  // Rewrite the main node, we rewrite and store the proof step, if necessary,
+  // in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: rewrite returned node " << retNode
+      << std::endl;
+  retNode = rewriteWithProof(retNode);
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: after rewriting is " << retNode
+      << std::endl;
 
   // now, rewrite the lemmas
+  Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: process lemmas"
+                           << std::endl;
   for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
   {
     // get the trust node to process
     TrustNode trn = newLemmas[i];
+    trn.debugCheckClosed(
+        "tpp-proof-debug", "TheoryPreprocessor::lemma_new_initial", false);
     Assert(trn.getKind() == TrustNodeKind::LEMMA);
     Node assertion = trn.getNode();
     // rewrite, which is independent of d_tpg, since additional lemmas
@@ -77,11 +149,37 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     Node rewritten = Rewriter::rewrite(assertion);
     if (assertion != rewritten)
     {
-      // not tracking proofs, just make new
-      newLemmas[i] = TrustNode::mkTrustLemma(rewritten, nullptr);
+      if (isProofEnabled())
+      {
+        Assert(d_lp != nullptr);
+        // store in the lazy proof
+        d_lp->addLazyStep(assertion,
+                          trn.getGenerator(),
+                          true,
+                          "TheoryPreprocessor::rewrite_lemma_new",
+                          false,
+                          PfRule::THEORY_PREPROCESS_LEMMA);
+        d_lp->addStep(rewritten,
+                      PfRule::MACRO_SR_PRED_TRANSFORM,
+                      {assertion},
+                      {rewritten});
+      }
+      newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get());
     }
+    Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
+    newLemmas[i].debugCheckClosed("tpp-proof-debug",
+                                  "TheoryPreprocessor::lemma_new");
   }
-  return TrustNode::mkTrustRewrite(node, retNode, nullptr);
+  if (node == retNode)
+  {
+    // no change
+    return TrustNode::null();
+  }
+  Trace("tpp-proof-debug") << "Preprocessed: " << node << " " << retNode
+                           << std::endl;
+  TrustNode tret = TrustNode::mkTrustRewrite(node, retNode, d_tpg.get());
+  tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret");
+  return tret;
 }
 
 struct preprocess_stack_element
@@ -91,7 +189,7 @@ struct preprocess_stack_element
   preprocess_stack_element(TNode n) : node(n), children_added(false) {}
 };
 
-Node TheoryPreprocessor::theoryPreprocess(TNode assertion)
+TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
 {
   Trace("theory::preprocess")
       << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
@@ -158,7 +256,7 @@ Node TheoryPreprocessor::theoryPreprocess(TNode assertion)
       Node result = builder;
       if (result != current)
       {
-        result = Rewriter::rewrite(result);
+        result = rewriteWithProof(result);
       }
       Debug("theory::internal")
           << "TheoryPreprocessor::theoryPreprocess(" << assertion
@@ -196,9 +294,9 @@ Node TheoryPreprocessor::theoryPreprocess(TNode assertion)
       }
     }
   }
-
   // Return the substituted version
-  return d_ppCache[assertion];
+  Node res = d_ppCache[assertion];
+  return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get());
 }
 
 // Recursively traverse a term and call the theory rewriter on its sub-terms
@@ -212,18 +310,13 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
   unsigned nc = term.getNumChildren();
   if (nc == 0)
   {
-    TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
-    return trn.isNull() ? Node(term) : trn.getNode();
+    return preprocessWithProof(term);
   }
   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
 
-  Node newTerm;
+  Node newTerm = term;
   // do not rewrite inside quantifiers
-  if (term.isClosure())
-  {
-    newTerm = Rewriter::rewrite(term);
-  }
-  else
+  if (!term.isClosure())
   {
     NodeBuilder<> newNode(term.getKind());
     if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
@@ -235,18 +328,75 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
     {
       newNode << ppTheoryRewrite(term[i]);
     }
-    newTerm = Rewriter::rewrite(Node(newNode));
-  }
-  TrustNode trn = d_engine.theoryOf(newTerm)->ppRewrite(newTerm);
-  Node newTerm2 = trn.isNull() ? newTerm : trn.getNode();
-  if (newTerm != newTerm2)
-  {
-    newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
+    newTerm = Node(newNode);
   }
+  newTerm = rewriteWithProof(newTerm);
+  newTerm = preprocessWithProof(newTerm);
   d_ppCache[term] = newTerm;
   Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
   return newTerm;
 }
 
+Node TheoryPreprocessor::rewriteWithProof(Node term)
+{
+  Node termr = Rewriter::rewrite(term);
+  // store rewrite step if tracking proofs and it rewrites
+  if (isProofEnabled())
+  {
+    // may rewrite the same term more than once, thus check hasRewriteStep
+    if (termr != term)
+    {
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> "
+          << termr << std::endl;
+      d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
+    }
+  }
+  return termr;
+}
+
+Node TheoryPreprocessor::preprocessWithProof(Node term)
+{
+  // Important that it is in rewritten form, to ensure that the rewrite steps
+  // recorded in d_tpg are functional. In other words, there should not
+  // be steps from the same term to multiple rewritten forms, which would be
+  // the case if we registered a preprocessing step for a non-rewritten term.
+  Assert(term == Rewriter::rewrite(term));
+  // call ppRewrite for the given theory
+  TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
+  if (trn.isNull())
+  {
+    // no change, return original term
+    return term;
+  }
+  Node termr = trn.getNode();
+  Assert(term != termr);
+  if (isProofEnabled())
+  {
+    if (trn.getGenerator() != nullptr)
+    {
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (generator) " << term << " -> "
+          << termr << std::endl;
+      trn.debugCheckClosed("tpp-proof-debug",
+                           "TheoryPreprocessor::preprocessWithProof");
+      d_tpg->addRewriteStep(term, termr, trn.getGenerator());
+    }
+    else
+    {
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (trusted) " << term << " -> "
+          << termr << std::endl;
+      // small step trust
+      d_tpg->addRewriteStep(
+          term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)});
+    }
+  }
+  termr = rewriteWithProof(termr);
+  return ppTheoryRewrite(termr);
+}
+
+bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 2f3813e68..95236ded3 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -19,15 +19,16 @@
 
 #include <unordered_map>
 
+#include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "preprocessing/assertion_pipeline.h"
+#include "expr/term_conversion_proof_generator.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 
 class LogicInfo;
 class TheoryEngine;
 class RemoveTermFormulas;
-class LazyCDProof;
 
 namespace theory {
 
@@ -40,7 +41,9 @@ class TheoryPreprocessor
 
  public:
   /** Constructs a theory preprocessor */
-  TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr);
+  TheoryPreprocessor(TheoryEngine& engine,
+                     RemoveTermFormulas& tfr,
+                     ProofNodeManager* pnm = nullptr);
   /** Destroys a theory preprocessor */
   ~TheoryPreprocessor();
   /** Clear the cache of this class */
@@ -69,7 +72,7 @@ class TheoryPreprocessor
    * the formula.  This is only called on input assertions, after ITEs
    * have been removed.
    */
-  Node theoryPreprocess(TNode node);
+  TrustNode theoryPreprocess(TNode node);
 
  private:
   /** Reference to owning theory engine */
@@ -80,8 +83,28 @@ class TheoryPreprocessor
   NodeMap d_ppCache;
   /** The term formula remover */
   RemoveTermFormulas& d_tfr;
+  /** The context for the proof generator below */
+  context::Context d_pfContext;
+  /** A term conversion proof generator */
+  std::unique_ptr<TConvProofGenerator> d_tpg;
+  /** A lazy proof, for additional lemmas. */
+  std::unique_ptr<LazyCDProof> d_lp;
   /** Helper for theoryPreprocess */
   Node ppTheoryRewrite(TNode term);
+  /**
+   * Rewrite with proof, which stores a REWRITE step in d_tpg if necessary
+   * and returns the rewritten form of term.
+   */
+  Node rewriteWithProof(Node term);
+  /**
+   * Preprocess with proof, which calls the appropriate ppRewrite method,
+   * stores the corresponding rewrite step in d_tpg if necessary and returns
+   * the preprocessed and rewritten form of term. It should be the case that
+   * term is already in rewritten form.
+   */
+  Node preprocessWithProof(Node term);
+  /** Proofs enabled */
+  bool isProofEnabled() const;
 };
 
 }  // namespace theory