From 8bfab32eed06973d53ce8ae066a9a26d4ae8a489 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Fri, 3 Jun 2016 14:27:00 -0700
Subject: [PATCH] Better infrastructure for proving constant disequality. Added
 support for the BV case

---
 proofs/signatures/th_bv.plf   | 19 +++++++++++++++++++
 src/proof/bitvector_proof.cpp | 30 ++++++++++++++++++++++++++++++
 src/proof/bitvector_proof.h   |  1 +
 src/proof/theory_proof.cpp    | 22 ++++++++++++++++------
 src/proof/theory_proof.h      |  6 ++++++
 5 files changed, 72 insertions(+), 6 deletions(-)

diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf
index 7f478d823..6012e052a 100644
--- a/proofs/signatures/th_bv.plf
+++ b/proofs/signatures/th_bv.plf
@@ -49,6 +49,25 @@
 	 (! v bv
 	    (term (BitVec n)))))
 
+(program bv_constants_are_disequal ((x bv) (y bv)) formula
+  (match x
+      (bvn (fail formula))
+      ((bvc bx x')
+        (match y
+          (bvn (fail formula))
+          ((bvc by y') (match bx
+                             (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true))))
+                             (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y'))))
+          ))
+      ))
+))
+
+(declare bv_disequal_constants
+	 (! n mpz
+	 (! x bv
+	 (! y bv
+	 (! c (^ (bv_constants_are_disequal x y) true)
+  	   (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y)))))))))
 
 ; a bv variable
 (declare var_bv type)
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 */
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4e5e98541..5ea754e08 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -147,6 +147,7 @@ public:
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printBitblasting(std::ostream& os, std::ostream& paren);
   virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
 };
 
 }/* CVC4 namespace */
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index eaf21846b..fe67ec94d 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -114,13 +114,11 @@ void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryI
 }
 
 void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
-  LetMap emptyMap;
+  Assert(c1.isConst());
+  Assert(c2.isConst());
 
-  os << "(trust_f (not (= _ ";
-  printBoundTerm(c1, os, emptyMap);
-  os << " ";
-  printBoundTerm(c2, os, emptyMap);
-  os << ")))";
+  Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2));
+  getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2);
 }
 
 void TheoryProofEngine::registerTerm(Expr term) {
@@ -1100,4 +1098,16 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Unreachable("No boolean lemmas yet!");
 }
 
+void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+  // By default, we just print a trust statement. Specific theories can implement
+  // better proofs.
+  LetMap emptyMap;
+
+  os << "(trust_f (not (= _ ";
+  d_proofEngine->printBoundTerm(c1, os, emptyMap);
+  os << " ";
+  d_proofEngine->printBoundTerm(c2, os, emptyMap);
+  os << ")))";
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index c8c776ec9..352cc1b53 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -315,6 +315,12 @@ public:
    * @param term
    */
   virtual void registerTerm(Expr term) = 0;
+  /**
+   * Print a proof for the disequality of two constants that belong to this theory.
+   *
+   * @param term
+   */
+  virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
 
   virtual void treatBoolsAsFormulas(bool value) {}
 };
-- 
2.30.2