Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)

This changes an annotation of a step of rewriting from "post" to "pre" in the theory preprocessor.
Fixes #6754.

diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp
index 3635f3deac4c2e54f7dcd0e8f9df537fc1fcb856..1c4e2de5d2796f8ad472f32160156a31c9b4289c 100644 (file)
--- a/src/proof/conv_proof_generator.cpp
+++ b/src/proof/conv_proof_generator.cpp
@@ -213,7 +213,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
 
       if (debugTraceEnabled)
       {
-        Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl;
+        Trace("tconv-pf-gen-debug") << "Rewrite steps:" << std::endl;
         for (size_t r = 0; r < 2; r++)
         {
           const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
@@ -233,7 +233,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
   std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
   Trace("tconv-pf-gen") << "... success" << std::endl;
   Assert(pfn != nullptr);
-  Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
+  Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
   return pfn;
 }
 
@@ -251,7 +251,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
   }
   std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
   Assert(pfn != nullptr);
-  Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
+  Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
   return pfn;
 }
 

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 230c2342407f2d58baf1b045088a6c124c6c25b0..53c90c88a88ba635a1658d0670c6cea25e520303 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -310,9 +310,14 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
         rtfNode = ttfr.getNode();
         registerTrustedRewrite(ttfr, d_tpgRtf.get(), true);
       }
-      // Finish the conversion by rewriting. This is registered as a
-      // post-rewrite, since it is the last step applied for theory atoms.
-      Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), false);
+      // Finish the conversion by rewriting. Notice that we must consider this a
+      // pre-rewrite since we do not recursively register the rewriting steps
+      // of subterms of rtfNode. For example, if this step rewrites
+      // (not A) ---> B, then if registered a pre-rewrite, it will apply when
+      // reconstructing proofs via d_tpgRtf. However, if it is a post-rewrite
+      // it will fail to apply if another call to this class registers A -> C,
+      // in which case (not C) will be returned instead of B (see issue 6754).
+      Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), true);
       d_rtfCache[current] = retNode;
       continue;
     }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 63d34ebe1d5092e17de1021e08f64e9db62cd280..da67705f57b6a2d2f189555419ebba95cee737a3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -794,6 +794,7 @@ set(regress_0_tests
   regress0/preprocess/circuit-prop.smt2
   regress0/preprocess/issue5729-rewritten-assertions.smt2
   regress0/preprocess/issue5943-non-clausal-simp.smt2
+  regress0/preprocess/issue6754-tpp.smt2
   regress0/preprocess/preprocess_00.cvc
   regress0/preprocess/preprocess_01.cvc
   regress0/preprocess/preprocess_02.cvc

diff --git a/test/regress/regress0/preprocess/issue6754-tpp.smt2 b/test/regress/regress0/preprocess/issue6754-tpp.smt2
new file mode 100644 (file)
index 0000000..9d34429
--- /dev/null
+++ b/test/regress/regress0/preprocess/issue6754-tpp.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () Bool)
+(assert (> (mod (ite a 0 1) 2) 1))
+(check-sat)