Better infrastructure for proving constant disequality.

Added support for the BV case

diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf
index 7f478d8231df2b549d7d82a0f04c3b55e94de32a..6012e052a180542c71970ad5306e03967f045aba 100644 (file)
--- 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 3fe426f15a9a81b99c5a5d9d421bcabb1d9ef32c..b2d6fdecf8043f78314bae56c8aad73e7e10fad8 100644 (file)
--- 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 4e5e98541df7663851c697e248c83a7515cecbb2..5ea754e082b5d3c6c98c291cb8f9de32751d3b7d 100644 (file)
--- 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 eaf21846b19ae423a5fe9edf530dad55e8fe8dd5..fe67ec94d68dfa0a606faa6da420393a18b0545f 100644 (file)
--- 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 c8c776ec9ea45c40dc5dea2f2fcc1ff503c1b55d..352cc1b53215a7c9e9d63e7e5b3bc4b20b52d987 100644 (file)
--- 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) {}
 };