diff options
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 3fe426f15..b2d6fdecf 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -1000,4 +1000,34 @@ bool LFSCBitVectorProof::hasAlias(Expr expr) { return d_assignedAliases.find(expr) != d_assignedAliases.end(); } +void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + Assert (c1.isConst()); + Assert (c2.isConst()); + Assert (utils::getSize(c1) == utils::getSize(c2)); + + os << "(bv_disequal_constants " << utils::getSize(c1) << " "; + + std::ostringstream paren; + + for (int i = utils::getSize(c1) - 1; i >= 0; --i) { + os << "(bvc "; + os << (utils::getBit(c1, i) ? "b1" : "b0") << " "; + paren << ")"; + } + os << "bvn"; + os << paren.str(); + + os << " "; + + for (int i = utils::getSize(c2) - 1; i >= 0; --i) { + os << "(bvc "; + os << (utils::getBit(c2, i) ? "b1" : "b0") << " "; + + } + os << "bvn"; + os << paren.str(); + + os << ")"; +} + } /* namespace CVC4 */ |