diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/proof/bitvector_proof.cpp | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
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.
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
| -rw-r--r-- | src/proof/bitvector_proof.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
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";} |