From: guykatzz <katz911@gmail.com>
Date: Thu, 9 Mar 2017 22:46:33 +0000 (-0800)
Subject: bug fix
X-Git-Tag: cvc5-1.0.0~5895
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58df458f5c5c8d318254f8d6b3b43b42883445d8;p=cvc5.git

bug fix
---

diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 6d04c3004..38428dd1e 100644
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -80,6 +80,30 @@
   (! f formula
     (term Bool)))
 
+(declare true_preds_equal
+  (! x1 (term Bool)
+  (! x2 (term Bool)
+  (! u1 (th_holds (p_app x1))
+  (! u2 (th_holds (p_app x2))
+    (th_holds (= Bool x1 x2)))))))
+
+(declare false_preds_equal
+  (! x1 (term Bool)
+  (! x2 (term Bool)
+  (! u1 (th_holds (not (p_app x1)))
+  (! u2 (th_holds (not (p_app x2)))
+    (th_holds (= Bool x1 x2)))))))
+
+(declare pred_refl_pos
+  (! x1 (term Bool)
+  (! u1 (th_holds (p_app x1))
+    (th_holds (= Bool x1 x1)))))
+
+(declare pred_refl_neg
+  (! x1 (term Bool)
+  (! u1 (th_holds (not (p_app x1)))
+    (th_holds (= Bool x1 x1)))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
 ; CNF Clausification
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index d3da2bcdb..c38fa1403 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -644,12 +644,50 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
           Unreachable();
         }
       } else {
-        // Both n1 and n2 are predicates. Don't know what to do...
-        Unreachable();
+        // Both n1 and n2 are predicates.
+        // We want to prove b1 = b2, and we know that ((b1), (b2)) or ((not b1), (not b2))
+        Debug("gk::temp") << "Two-predicate case. pf->d_node = " << pf->d_node
+                          << ", n1 = " << n1 << ", n2 = " << n2 << std::endl;
+
+        if (n1.getKind() == kind::NOT) {
+          Assert(n2.getKind() == kind::NOT);
+          Assert(pf->d_node[0] == n1[0] || pf->d_node[0] == n2[0]);
+          Assert(pf->d_node[1] == n1[0] || pf->d_node[1] == n2[0]);
+          Assert(n1[0].getKind() == kind::BOOLEAN_TERM_VARIABLE);
+          Assert(n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE);
+
+          if (pf->d_node[0] == n1[0]) {
+            ss << "(false_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") ";
+            ss << "(pred_refl_neg _ " << ss2.str() << ")";
+          } else {
+            ss << "(false_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") ";
+            ss << "(pred_refl_neg _ " << ss1.str() << ")";
+          }
+          n1 = pf->d_node;
+
+        } else if (n1.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
+          Assert(n2.getKind() == kind::BOOLEAN_TERM_VARIABLE);
+          Assert(pf->d_node[0] == n1 || pf->d_node[0] == n2);
+          Assert(pf->d_node[1] == n1 || pf->d_node[2] == n2);
+
+          if (pf->d_node[0] == n1) {
+            ss << "(true_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") ";
+            ss << "(pred_refl_pos _ " << ss2.str() << ")";
+          } else {
+            ss << "(true_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") ";
+            ss << "(pred_refl_pos _ " << ss1.str() << ")";
+          }
+          n1 = pf->d_node;
+
+        } else {
+
+          Unreachable();
+        }
       }
 
       ss << ")";
     }
+
     out << ss.str();
     Debug("pf::uf") << "\n++ trans proof done, have proven " << n1 << std::endl;
     return n1;