diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.cpp | 16 | ||||
-rw-r--r-- | src/proof/array_proof.cpp | 16 | ||||
-rw-r--r-- | src/proof/bitvector_proof.cpp | 10 | ||||
-rw-r--r-- | src/proof/cnf_proof.cpp | 12 | ||||
-rw-r--r-- | src/proof/proof_utils.cpp | 14 | ||||
-rw-r--r-- | src/proof/proof_utils.h | 1 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 19 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 28 |
8 files changed, 68 insertions, 48 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index b7ed0b2ec..0f0c14eb2 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -24,7 +24,7 @@ namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); + return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); } // congrence matching term helper @@ -429,7 +429,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if(n2.getKind() == kind::EQUAL) { if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { // We are in a sequence of identical equalities @@ -487,8 +487,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq } else { // We have a "next node". Use it to guide us. - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || - nodeAfterEqualitySequence.getKind() == kind::IFF); + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { @@ -533,7 +532,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Debug("pf::arith") << "\ndoing trans proof, got n2 " << n2 << "\n"; if(tb == 1) { Debug("pf::arith") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; - Debug("pf::arith") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + Debug("pf::arith") << (n2.getKind() == kind::EQUAL) << "\n"; if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { Debug("pf::arith") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; @@ -549,8 +548,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq } ss << "(trans _ _ _ _ "; - if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && - (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL)) // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { @@ -580,7 +578,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Unreachable(); } Debug("pf::arith") << "++ trans proof[" << i << "], now have " << n1 << std::endl; - } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + } else if(n1.getKind() == kind::EQUAL) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { n1 = n1[1]; @@ -591,7 +589,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq } else { Unreachable(); } - } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + } else if(n2.getKind() == kind::EQUAL) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { n1 = n2[1]; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 32a7c247d..cc60d8c07 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -24,7 +24,7 @@ namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); + return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); } // congrence matching term helper @@ -640,7 +640,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if(n2.getKind() == kind::EQUAL) { if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { // We are in a sequence of identical equalities @@ -701,8 +701,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, nodeAfterEqualitySequence = nodeAfterEqualitySequence[0]; } - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || - nodeAfterEqualitySequence.getKind() == kind::IFF); + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { @@ -747,7 +746,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n"; if(tb == 1) { Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; - Debug("mgdx") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + Debug("mgdx") << (n2.getKind() == kind::EQUAL) << "\n"; if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; @@ -784,8 +783,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ss << "(trans _ _ _ _ "; } - if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && - (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL)) // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { @@ -824,7 +822,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Unreachable(); } Debug("mgd") << "++ trans proof[" << i << "], now have " << n1 << std::endl; - } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + } else if(n1.getKind() == kind::EQUAL) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { n1 = n1[1]; @@ -836,7 +834,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } else { Unreachable(); } - } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + } else if(n2.getKind() == kind::EQUAL) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { n1 = n2[1]; diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index cbe54ff4b..926dae9fd 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -412,7 +412,7 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { } void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) { - std::string op = utils::toLFSCKind(term.getKind()); + std::string op = utils::toLFSCKindTerm(term); std::ostringstream paren; std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : ""; unsigned size = term.getKind() == kind::BITVECTOR_CONCAT? utils::getSize(term) : @@ -431,7 +431,7 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Pr void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; - os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; + os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os << " "; d_proofEngine->printBoundTerm(term[0], os, map); os <<")"; @@ -439,7 +439,7 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const P void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; - os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" "; + os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" "; os << " "; d_proofEngine->printBoundTerm(term[0], os, map); os << " "; @@ -449,7 +449,7 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const Proof void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; - os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; + os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os <<" "; if (term.getKind() == kind::BITVECTOR_REPEAT) { unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount; @@ -872,7 +872,7 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool case kind::EQUAL: { Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; - os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + os << "(bv_bbl_" << utils::toLFSCKindTerm(atom); if (swap) {os << "_swap";} diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index b58ade35e..69b613f28 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -596,16 +596,16 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os << ")"; } } - }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){ + }else if( base_assertion.getKind()==kind::XOR || ( base_assertion.getKind()==kind::EQUAL && base_assertion[0].getType().isBoolean() ) ){ //eliminate negation int num_nots_2 = 0; int num_nots_1 = 0; Kind k; if( !base_pol ){ - if( base_assertion.getKind()==kind::IFF ){ + if( base_assertion.getKind()==kind::EQUAL ){ num_nots_2 = 1; } - k = kind::IFF; + k = kind::EQUAL; }else{ k = base_assertion.getKind(); } @@ -623,7 +623,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, if( i==0 ){ //figure out which way to elim elimNum = child_pol==childPol[child_base] ? 2 : 1; - if( (elimNum==2)==(k==kind::IFF) ){ + if( (elimNum==2)==(k==kind::EQUAL) ){ num_nots_2++; } if( elimNum==1 ){ @@ -651,9 +651,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } Assert( elimNum!=0 ); - os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; + os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; if( !base_pol ){ - os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; + os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; }else{ os_base_n << os_base.str(); } diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp index fe0d42242..3ace236b5 100644 --- a/src/proof/proof_utils.cpp +++ b/src/proof/proof_utils.cpp @@ -41,7 +41,6 @@ std::string toLFSCKind(Kind kind) { case kind::AND: return "and"; case kind::XOR: return "xor"; case kind::EQUAL: return "="; - case kind::IFF: return "iff"; case kind::IMPLIES: return "impl"; case kind::NOT: return "not"; @@ -123,5 +122,18 @@ std::string toLFSCKind(Kind kind) { } } +std::string toLFSCKindTerm(Expr node) { + Kind k = node.getKind(); + if( k==kind::EQUAL ){ + if( node[0].getType().isBoolean() ){ + return "iff"; + }else{ + return "="; + } + }else{ + return toLFSCKind( k ); + } +} + } /* namespace CVC4::utils */ } /* namespace CVC4 */ diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index b172217d8..a7590451d 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -88,6 +88,7 @@ typedef std::vector<LetOrderElement> Bindings; namespace utils { std::string toLFSCKind(Kind kind); +std::string toLFSCKindTerm(Expr node); inline unsigned getExtractHigh(Expr node) { return node.getOperator().getConst<BitVectorExtract>().high; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 1912dbada..156c90e47 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -856,9 +856,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro case kind::EQUAL: os << "("; - os << "= "; - printSort(term[0].getType(), os); - os << " "; + if( term[0].getType().isBoolean() ){ + os << "iff "; + }else{ + os << "= "; + printSort(term[0].getType(), os); + os << " "; + } printBoundTerm(term[0], os, map); os << " "; printBoundTerm(term[1], os, map); @@ -912,6 +916,12 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro // LFSC doesn't allow declarations with variable numbers of // arguments, so we have to flatten chained operators, like =. Kind op = term.getOperator().getConst<Chain>().getOperator(); + std::string op_str; + if( op==kind::EQUAL && term[0].getType().isBoolean() ){ + op_str = "iff"; + }else{ + op_str = utils::toLFSCKind(op); + } size_t n = term.getNumChildren(); std::ostringstream paren; for(size_t i = 1; i < n; ++i) { @@ -919,7 +929,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro os << "(" << utils::toLFSCKind(kind::AND) << " "; paren << ")"; } - os << "(" << utils::toLFSCKind(op) << " "; + os << "(" << op_str << " "; printBoundTerm(term[i - 1], os, map); os << " "; printBoundTerm(term[i], os, map); @@ -1096,7 +1106,6 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe // If letification is off or there were 2 children, same treatment as the other cases. // (No break is intentional). case kind::XOR: - case kind::IFF: case kind::IMPLIES: case kind::NOT: // print the Boolean operators diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 27f351102..41262051c 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -24,7 +24,7 @@ namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); + return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); } // congrence matching term helper @@ -472,7 +472,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if(n2.getKind() == kind::EQUAL) { if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { // We are in a sequence of identical equalities @@ -530,8 +530,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else { // We have a "next node". Use it to guide us. - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || - nodeAfterEqualitySequence.getKind() == kind::IFF); + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { @@ -576,7 +575,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Debug("pf::uf") << "\ndoing trans proof, got n2 " << n2 << "\n"; if(tb == 1) { Debug("pf::uf") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; - Debug("pf::uf") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + Debug("pf::uf") << (n2.getKind() == kind::EQUAL) << "\n"; if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { Debug("pf::uf") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; @@ -592,8 +591,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } ss << "(trans _ _ _ _ "; - if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && - (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL) // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { @@ -623,24 +621,24 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Unreachable(); } Debug("pf::uf") << "++ trans proof[" << i << "], now have " << n1 << std::endl; - } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + } else if(n1.getKind() == kind::EQUAL) { // 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].eqNode(NodeManager::currentNM()->mkConst(true)); 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].eqNode(NodeManager::currentNM()->mkConst(true)); ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; } else { Unreachable(); } - } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + } else if(n2.getKind() == kind::EQUAL) { // 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].eqNode(NodeManager::currentNM()->mkConst(true)); 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].eqNode(NodeManager::currentNM()->mkConst(true)); ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; } else { Unreachable(); @@ -707,6 +705,10 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& os << term; return; } + if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) { + os << "(p_app " << term << ")"; + return; + } Assert (term.getKind() == kind::APPLY_UF); d_proofEngine->treatBoolsAsFormulas(false); |