diff options
author | guykatzz <katz911@gmail.com> | 2017-03-09 14:46:33 -0800 |
---|---|---|
committer | guykatzz <katz911@gmail.com> | 2017-03-09 14:46:33 -0800 |
commit | 58df458f5c5c8d318254f8d6b3b43b42883445d8 (patch) | |
tree | 8d2854fc47c20acc7233fc32b89b2d0782135d10 /src/proof/uf_proof.cpp | |
parent | 2f287a59e9c775d9087cddd8c72be5169c2706e1 (diff) |
bug fix
Diffstat (limited to 'src/proof/uf_proof.cpp')
-rw-r--r-- | src/proof/uf_proof.cpp | 42 |
1 files changed, 40 insertions, 2 deletions
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; |