diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/proof/uf_proof.cpp | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/proof/uf_proof.cpp')
-rw-r--r-- | src/proof/uf_proof.cpp | 103 |
1 files changed, 27 insertions, 76 deletions
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index bc409901c..32ca122b0 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -86,16 +86,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E pf->debug_print("pf::uf"); Debug("pf::uf") << std::endl; - if (tb == 0) { - // Special case: false was an input, so the proof is just "false". - if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY && - pf->d_node == NodeManager::currentNM()->mkConst(false)) { - out << "(clausify_false "; - out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode()); - out << ")" << std::endl; - return Node(); - } - + if(tb == 0) { Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS); Assert(!pf->d_node.isNull()); Assert(pf->d_children.size() >= 2); @@ -199,71 +190,42 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ++i; } } - - bool disequalityFound = (neg >= 0); - if (!disequalityFound) { - Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl; - Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl; - Assert(pf->d_node.getKind() == kind::EQUAL); - Assert(pf->d_node.getNumChildren() == 2); - Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst()); - } + Assert(neg >= 0); Node n1; std::stringstream ss; + //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; - - if(!disequalityFound || subTrans.d_children.size() >= 2) { + if(pf->d_children.size() > 2) { n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); } else { n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; } - Debug("pf::uf") << "\nhave proven: " << n1 << std::endl; - + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); out << "(clausify_false (contra _ "; + Debug("pf::uf") << "\nhave proven: " << n1 << std::endl; + Debug("pf::uf") << "n2 is " << n2[0] << std::endl; - if (disequalityFound) { - Node n2 = pf->d_children[neg]->d_node; - Assert(n2.getKind() == kind::NOT); - Debug("pf::uf") << "n2 is " << n2[0] << std::endl; - - if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } - if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; } - - if(n2[0].getKind() == kind::APPLY_UF) { - out << "(trans _ _ _ _ "; + if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; } - if (n1[0] == n2[0]) { - out << "(symm _ _ _ "; - out << ss.str(); - out << ") "; - } else { - Assert(n1[1] == n2[0]); - out << ss.str(); - } - out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; + if(n2[0].getKind() == kind::APPLY_UF) { + out << "(trans _ _ _ _ "; + out << "(symm _ _ _ "; + out << ss.str(); + out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; + } else { + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + if(n1[1] == n2[0][0]) { + out << "(symm _ _ _ " << ss.str() << ")"; } else { - Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); - if(n1[1] == n2[0][0]) { - out << "(symm _ _ _ " << ss.str() << ")"; - } else { - out << ss.str(); - } - out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + out << ss.str(); } - } else { - Node n2 = pf->d_node; - Assert(n2.getKind() == kind::EQUAL); - Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); - - out << ss.str(); - out << " "; - ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr()); - out << "))" << std::endl; + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; } - return Node(); } @@ -622,10 +584,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { - n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[1]; ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; } else if(n1[1] == n2) { - n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[0]; ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; } else { Unreachable(); @@ -633,16 +595,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { - n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[1]; ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; } else if(n2[1] == n1) { - n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[0]; ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; } else { Unreachable(); } } else { - // Both n1 and n2 are predicates. Don't know what to do... + // Both n1 and n2 are prediacates. Don't know what to do... Unreachable(); } @@ -705,7 +667,6 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) } Assert (term.getKind() == kind::APPLY_UF); - d_proofEngine->treatBoolsAsFormulas(false); if(term.getType().isBoolean()) { os << "(p_app "; @@ -722,7 +683,6 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) if(term.getType().isBoolean()) { os << ")"; } - d_proofEngine->treatBoolsAsFormulas(true); } void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { @@ -754,8 +714,6 @@ void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { // declaring the terms - Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl; - for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { Expr term = *it; @@ -771,8 +729,7 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { os << "(arrow"; for (unsigned i = 0; i < args.size(); i++) { Type arg_type = args[i]; - os << " "; - d_proofEngine->printSort(arg_type, os); + os << " " << arg_type; if (i < args.size() - 2) { os << " (arrow"; fparen << ")"; @@ -785,16 +742,10 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { } paren << ")"; } - - Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl; } void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { // Nothing to do here at this point. } -void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { - // Nothing to do here at this point. -} - } /* namespace CVC4 */ |