(proof-new) Fixes for theory preprocessing proofs (#5171)

This fixes several subtle issues with theory preprocessing.

The main fix is to ensure proofs are correct for cases where the theory preprocessor applies either with or without theory preprocessing (calling Theory::ppRewrite on subterms) enabled, see argument doTheoryPreprocess of preprocess. If disabled, it applies term formula removal and rewriting only. This is required for processing lemmas that are marked as "do not preprocess", which is an optimization, but is also necessary since theory combination may e.g. split on equality that was solved during ppRewrite. The solution is to use 2 separate term conversion sequences for these 2 cases.

It also fixes an issue where preprocessing is term-context-sensitive: terms underneath quantifiers are treated differently. This is now handled by a new TermContext callback "InQuantTermContext".

diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index 6974e211464b2435add9b1bf1b62455b84064d60..67da6d842a281771ad2ebe1edeea3d91ac6e0c57 100644 (file)
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -69,6 +69,22 @@ bool RtfTermContext::hasNestedTermChildren(TNode t)
          && k != kind::BITVECTOR_EAGER_ATOM;
 }
 
+uint32_t InQuantTermContext::initialValue() const { return 0; }
+
+uint32_t InQuantTermContext::computeValue(TNode t,
+                                          uint32_t tval,
+                                          size_t index) const
+{
+  return t.isClosure() ? 1 : tval;
+}
+
+uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; }
+
+bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant)
+{
+  return val == 1;
+}
+
 uint32_t PolarityTermContext::initialValue() const
 {
   // by default, we have true polarity

diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index ec7b488f92e23d89947906a4429f06b1a08f9c9b..b0ce03e481f9e3ec24f12865c260ca15313b258e 100644 (file)
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -92,6 +92,24 @@ class RtfTermContext : public TermContext
   static bool hasNestedTermChildren(TNode t);
 };
 
+/**
+ * Simpler version of above that only computes whether we are inside a
+ * quantifier.
+ */
+class InQuantTermContext : public TermContext
+{
+ public:
+  InQuantTermContext() {}
+  /** The initial value: not beneath a quantifier. */
+  uint32_t initialValue() const override;
+  /** Compute the value of the index^th child of t whose hash is tval */
+  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
+  /** get hash value from the flags */
+  static uint32_t getValue(bool inQuant);
+  /** get flags from the hash value */
+  static bool inQuant(uint32_t val, bool& inQuant);
+};
+
 /**
  * Polarity term context.
  *

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 5034119e8f01626650d1041bf04652515f490804..cf7c00e2b4d49a63fe3417d608dd530d45b377d4 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -552,6 +552,11 @@ void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm)
   }
 }
 
+ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
+{
+  return d_tpg.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 30972c1cc39ab463b14501f7c52e15752adbe93e..25dcd02955c263f9a4f0b4435c0544a91adba75c 100644 (file)
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -107,10 +107,18 @@ class RemoveTermFormulas {
 
   /**
    * Set proof node manager, which signals this class to enable proofs using the
-   * given checker.
+   * given proof node manager.
    */
   void setProofNodeManager(ProofNodeManager* pnm);
 
+  /**
+   * Get proof generator that is responsible for all proofs for removing term
+   * formulas from nodes. When proofs are enabled, the returned trust node
+   * of the run method use this proof generator (the trust nodes in newAsserts
+   * do not use this generator).
+   */
+  ProofGenerator* getTConvProofGenerator();
+
   /**
    * 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

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 049598dbbc2425682645f9af6fef2d47c1477190..80b824ca0234563f6c0c3a879fa0bd88930b270a 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -38,8 +38,17 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
                       &d_pfContext,
                       TConvPolicy::FIXPOINT,
                       TConvCachePolicy::NEVER,
-                      "TheoryPreprocessor::TConvProofGenerator")
+                      "TheoryPreprocessor::preprocess_rewrite",
+                      &d_iqtc)
                 : nullptr),
+      d_tspg(nullptr),
+      d_tpgRew(pnm ? new TConvProofGenerator(pnm,
+                                             &d_pfContext,
+                                             TConvPolicy::FIXPOINT,
+                                             TConvCachePolicy::NEVER,
+                                             "TheoryPreprocessor::rewrite")
+                   : nullptr),
+      d_tspgNoPp(nullptr),
       d_lp(pnm ? new LazyCDProof(pnm,
                                  nullptr,
                                  &d_pfContext,
@@ -53,6 +62,26 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
     // push the proof context, since proof steps may be cleared on calls to
     // clearCache() below.
     d_pfContext.push();
+    // Make the main term conversion sequence generator, which tracks up to
+    // three conversions made in succession:
+    // (1) theory preprocessing+rewriting
+    // (2) term formula removal
+    // (3) rewriting
+    // Steps (1) and (3) use a common term conversion generator.
+    std::vector<ProofGenerator*> ts;
+    ts.push_back(d_tpg.get());
+    ts.push_back(d_tfr.getTConvProofGenerator());
+    ts.push_back(d_tpg.get());
+    d_tspg.reset(new TConvSeqProofGenerator(
+        pnm, ts, &d_pfContext, "TheoryPreprocessor::sequence"));
+    // Make the "no preprocess" term conversion sequence generator, which
+    // applies only steps (2) and (3), where notice (3) must use the
+    // "pure rewrite" term conversion (d_tpgRew).
+    std::vector<ProofGenerator*> tsNoPp;
+    tsNoPp.push_back(d_tfr.getTConvProofGenerator());
+    tsNoPp.push_back(d_tpgRew.get());
+    d_tspgNoPp.reset(new TConvSeqProofGenerator(
+        pnm, tsNoPp, &d_pfContext, "TheoryPreprocessor::sequence_no_pp"));
   }
 }
 
@@ -60,8 +89,9 @@ TheoryPreprocessor::~TheoryPreprocessor() {}
 
 void TheoryPreprocessor::clearCache()
 {
+  Trace("tpp-proof-debug") << "TheoryPreprocessor::clearCache" << std::endl;
   d_ppCache.clear();
-  // clear proofs from d_tpg and d_lp using internal push/pop context
+  // clear proofs from d_tpg, d_tspg and d_lp using internal push/pop context
   if (isProofEnabled())
   {
     d_pfContext.pop();
@@ -77,6 +107,7 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   // In this method, all rewriting steps of node are stored in d_tpg.
 
   Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: start " << node
+                           << ", doTheoryPreprocess=" << doTheoryPreprocess
                            << std::endl;
   // Run theory preprocessing, maybe
   Node ppNode = node;
@@ -94,22 +125,10 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   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());
-    }
-  }
+  Node rtfNode = ttfr.getNode();
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: rtf returned node " << rtfNode
+      << std::endl;
 
   if (Debug.isOn("lemma-ites"))
   {
@@ -125,13 +144,54 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   }
   // 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);
+  Node retNode = rewriteWithProof(rtfNode);
   Trace("tpp-proof-debug")
       << "TheoryPreprocessor::preprocess: after rewriting is " << retNode
       << std::endl;
+  if (node == retNode)
+  {
+    // no change
+    Assert(newLemmas.empty());
+    return TrustNode::null();
+  }
+
+  // Now, sequence the conversion steps if proofs are enabled.
+  TrustNode tret;
+  if (isProofEnabled())
+  {
+    std::vector<Node> cterms;
+    cterms.push_back(node);
+    if (doTheoryPreprocess)
+    {
+      cterms.push_back(ppNode);
+    }
+    cterms.push_back(rtfNode);
+    cterms.push_back(retNode);
+    // We have that:
+    // node -> ppNode via preprocessing + rewriting (if doTheoryPreprocess)
+    // ppNode -> rtfNode via term formula removal
+    // rtfNode -> retNode via rewriting
+    if (!doTheoryPreprocess)
+    {
+      // If preprocessing is not performed, we cannot use the main sequence
+      // generator, instead we use d_tspgNoPp.
+      // We register the top-level rewrite in the pure rewrite term converter.
+      d_tpgRew->addRewriteStep(
+          rtfNode, retNode, PfRule::REWRITE, {}, {rtfNode});
+      // Now get the trust node from the sequence generator
+      tret = d_tspgNoPp->mkTrustRewriteSequence(cterms);
+    }
+    else
+    {
+      // we wil use the sequence generator
+      tret = d_tspg->mkTrustRewriteSequence(cterms);
+    }
+    tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret");
+  }
+  else
+  {
+    tret = TrustNode::mkTrustRewrite(node, retNode, nullptr);
+  }
 
   // now, rewrite the lemmas
   Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: process lemmas"
@@ -170,15 +230,8 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     newLemmas[i].debugCheckClosed("tpp-proof-debug",
                                   "TheoryPreprocessor::lemma_new");
   }
-  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;
 }
 
@@ -205,7 +258,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
     preprocess_stack_element& stackHead = toVisit.back();
     TNode current = stackHead.node;
 
-    Debug("theory::internal")
+    Trace("theory::preprocess-debug")
         << "TheoryPreprocessor::theoryPreprocess(" << assertion
         << "): processing " << current << endl;
 
@@ -258,7 +311,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
       {
         result = rewriteWithProof(result);
       }
-      Debug("theory::internal")
+      Trace("theory::preprocess-debug")
           << "TheoryPreprocessor::theoryPreprocess(" << assertion
           << "): setting " << current << " -> " << result << endl;
       d_ppCache[current] = result;
@@ -286,7 +339,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
       else
       {
         // No children, so we're done
-        Debug("substitution::internal")
+        Trace("theory::preprocess-debug")
             << "SubstitutionMap::internalSubstitute(" << assertion
             << "): setting " << current << " -> " << current << endl;
         d_ppCache[current] = current;
@@ -349,6 +402,7 @@ Node TheoryPreprocessor::rewriteWithProof(Node term)
       Trace("tpp-proof-debug")
           << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> "
           << termr << std::endl;
+      // always use term context hash 0 (default)
       d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
     }
   }
@@ -380,6 +434,7 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
           << termr << std::endl;
       trn.debugCheckClosed("tpp-proof-debug",
                            "TheoryPreprocessor::preprocessWithProof");
+      // always use term context hash 0 (default)
       d_tpg->addRewriteStep(term, termr, trn.getGenerator());
     }
     else

diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index db43b6828b229c73f78f32d8bae2d3acb0a6dd5e..769d548d97e85faa4ab251d140bfa994b2316dbd 100644 (file)
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -21,6 +21,7 @@
 
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
+#include "expr/tconv_seq_proof_generator.h"
 #include "expr/term_conversion_proof_generator.h"
 #include "theory/trust_node.h"
 
@@ -85,8 +86,31 @@ class TheoryPreprocessor
   RemoveTermFormulas& d_tfr;
   /** The context for the proof generator below */
   context::Context d_pfContext;
-  /** A term conversion proof generator */
+  /** The term context, which computes hash values for term contexts. */
+  InQuantTermContext d_iqtc;
+  /**
+   * A term conversion proof generator storing preprocessing and rewriting
+   * steps.
+   */
   std::unique_ptr<TConvProofGenerator> d_tpg;
+  /**
+   * A term conversion sequence generator, which applies theory preprocessing,
+   * term formula removal, and rewriting in sequence.
+   */
+  std::unique_ptr<TConvSeqProofGenerator> d_tspg;
+  /**
+   * A term conversion proof generator storing rewriting steps, which is used
+   * for calls to preprocess when doTheoryPreprocess is false. We store
+   * (top-level) rewrite steps only. Notice this is intentionally separate
+   * from d_tpg, which interleaves both preprocessing and rewriting.
+   */
+  std::unique_ptr<TConvProofGenerator> d_tpgRew;
+  /**
+   * A term conversion sequence generator, which applies term formula removal
+   * and rewriting in sequence. This is used for reconstruct proofs of
+   * calls to preprocess where doTheoryPreprocess is false.
+   */
+  std::unique_ptr<TConvSeqProofGenerator> d_tspgNoPp;
   /** A lazy proof, for additional lemmas. */
   std::unique_ptr<LazyCDProof> d_lp;
   /** Helper for theoryPreprocess */