Better infrastructure for proving constant disequality.

Added support for the BV case

1 files changed, 16 insertions, 6 deletions

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