Better infrastructure for proving constant disequality.

Added support for the BV case

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 */