From 1f4b954a2cc7667a56a3007fa75c125fba93ed23 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 2 Mar 2017 14:45:21 -0600 Subject: Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. --- src/proof/bitvector_proof.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/proof/bitvector_proof.cpp') 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().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";} -- cgit v1.2.3