Avoiding cyclic redundant steps

6 files changed, 29 insertions, 6 deletions

diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp
index 60c224e61..c16b2cdbc 100644
--- a/src/expr/proof_step_buffer.cpp
+++ b/src/expr/proof_step_buffer.cpp
@@ -81,6 +81,15 @@ void ProofStepBuffer::addStep(PfRule id,
       std::pair<Node, ProofStep>(expected, ProofStep(id, children, args)));
 }
 
+void ProofStepBuffer::popStep()
+{
+  Assert (!d_steps.empty());
+  if (!d_steps.empty())
+  {
+    d_steps.pop_back();
+  }
+}
+
 size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); }
 
 const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index 56dc113e1..db07f8649 100644
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -68,6 +68,8 @@ class ProofStepBuffer
                const std::vector<Node>& children,
                const std::vector<Node>& args,
                Node expected);
+  /** pop step */
+  void popStep();
   /** Get num steps */
   size_t getNumSteps() const;
   /** Get steps */
diff --git a/src/theory/proof_engine_output_channel.cpp b/src/theory/proof_engine_output_channel.cpp
index f16033bb8..f377b60ee 100644
--- a/src/theory/proof_engine_output_channel.cpp
+++ b/src/theory/proof_engine_output_channel.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/proof_engine_output_channel.h"
 
+#include "expr/lazy_proof.h"
+
 namespace CVC4 {
 namespace theory {
 
diff --git a/src/theory/proof_engine_output_channel.h b/src/theory/proof_engine_output_channel.h
index fc1eb2fd4..69b9e86ed 100644
--- a/src/theory/proof_engine_output_channel.h
+++ b/src/theory/proof_engine_output_channel.h
@@ -18,13 +18,13 @@
 #define CVC4__THEORY__PROOF_ENGINE_OUTPUT_CHANNEL_H
 
 #include "context/cdhashmap.h"
-#include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/proof_node.h"
-#include "theory/eager_proof_generator.h"
 #include "theory/engine_output_channel.h"
 
 namespace CVC4 {
+  
+class LazyCDProof;
+
 namespace theory {
 
 /**
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index cb781db25..9a73b9390 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -224,8 +224,13 @@ Node InferProofCons::convert(Inference infer,
                             ps.d_children.begin(),
                             ps.d_children.begin() + mainEqIndex);
         std::vector<Node> argsSRew;
-        Node mainEqSRew =
-            d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, argsSRew);
+        Node mainEqSRew = 
+              d_psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, argsSRew);
+        if (mainEqSRew==mainEq)
+        {
+          // not necessary
+          d_psb.popStep();
+        }
         Trace("strings-ipc-core")
             << "Main equality after subs+rewrite " << mainEqSRew << std::endl;
         // now, apply CONCAT_EQ to get the remainder
@@ -238,8 +243,14 @@ Node InferProofCons::convert(Inference infer,
             << "Main equality after CONCAT_EQ " << mainEqCeq << std::endl;
         if (mainEqCeq.isNull() || mainEqCeq.getKind() != EQUAL)
         {
+          // fail
           break;
         }
+        else if (mainEqCeq==mainEqSRew)
+        {
+          // not necessary
+          d_psb.popStep();
+        }
         // Now, mainEqCeq is an equality t ++ ... == s ++ ... where the
         // inference involved t and s.
         if (infer == Inference::N_ENDPOINT_EQ
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index 9566318b9..7bb817379 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {