diff options
author | Guy <katz911@gmail.com> | 2016-04-03 15:58:58 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-04-03 15:58:58 -0700 |
commit | 29df9622b570ce843756e05a3ef248de04d2a5c3 (patch) | |
tree | 6577c5eec908571f2ee0fb262c12b3612f0c3118 /src/proof/uf_proof.cpp | |
parent | cd5cc65fed2c850100a6f00067d102b48d262742 (diff) |
Removed the theory-specific merge reason types. Instead, added a mechanism for dynamically allocating these tags upon request.
Diffstat (limited to 'src/proof/uf_proof.cpp')
-rw-r--r-- | src/proof/uf_proof.cpp | 82 |
1 files changed, 0 insertions, 82 deletions
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 6a6f8d906..e728e9e49 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -615,88 +615,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E return n1; } - case theory::eq::MERGED_ARRAYS_ROW: { - Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW encountered in UF_PROOF" << std::endl; - Unreachable(); - - Debug("pf::uf") << "row lemma: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - TNode t1, t2, t3, t4; - Node ret; - if(pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0].getKind() == kind::STORE && - pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0] == pf->d_node[1][0][0] && - pf->d_node[0][1] == pf->d_node[1][1]) { - t2 = pf->d_node[1][0][1]; - t3 = pf->d_node[1][1]; - t1 = pf->d_node[0][0]; - t4 = pf->d_node[1][0][2]; - ret = pf->d_node[1].eqNode(pf->d_node[0]); - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; - } else { - Assert(pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0].getKind() == kind::STORE && - pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0] == pf->d_node[0][0][0] && - pf->d_node[1][1] == pf->d_node[0][1]); - t2 = pf->d_node[0][0][1]; - t3 = pf->d_node[0][1]; - t1 = pf->d_node[1][0]; - t4 = pf->d_node[0][0][2]; - ret = pf->d_node; - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; - } - out << "(row _ _ "; - tp->printTerm(t2.toExpr(), out, map); - out << " "; - tp->printTerm(t3.toExpr(), out, map); - out << " "; - tp->printTerm(t1.toExpr(), out, map); - out << " "; - tp->printTerm(t4.toExpr(), out, map); - out << " " << ProofManager::getLitName(t2.eqNode(t3)) << ")"; - return ret; - } - - case theory::eq::MERGED_ARRAYS_ROW1: { - Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW1 encountered in UF_PROOF" << std::endl; - Unreachable(); - - Debug("pf::uf") << "row1 lemma: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - TNode t1, t2, t3; - Node ret; - if(pf->d_node[1].getKind() == kind::SELECT && - pf->d_node[1][0].getKind() == kind::STORE && - pf->d_node[1][0][1] == pf->d_node[1][1] && - pf->d_node[1][0][2] == pf->d_node[0]) { - t1 = pf->d_node[1][0][0]; - t2 = pf->d_node[1][0][1]; - t3 = pf->d_node[0]; - ret = pf->d_node[1].eqNode(pf->d_node[0]); - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; - } else { - Assert(pf->d_node[0].getKind() == kind::SELECT && - pf->d_node[0][0].getKind() == kind::STORE && - pf->d_node[0][0][1] == pf->d_node[0][1] && - pf->d_node[0][0][2] == pf->d_node[1]); - t1 = pf->d_node[0][0][0]; - t2 = pf->d_node[0][0][1]; - t3 = pf->d_node[1]; - ret = pf->d_node; - Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; - } - out << "(row1 _ _ "; - tp->printTerm(t1.toExpr(), out, map); - out << " "; - tp->printTerm(t2.toExpr(), out, map); - out << " "; - tp->printTerm(t3.toExpr(), out, map); - out << ")"; - return ret; - } - default: Assert(!pf->d_node.isNull()); Assert(pf->d_children.empty()); |