From 8bfab32eed06973d53ce8ae066a9a26d4ae8a489 Mon Sep 17 00:00:00 2001 From: Guy Date: Fri, 3 Jun 2016 14:27:00 -0700 Subject: Better infrastructure for proving constant disequality. Added support for the BV case --- src/proof/bitvector_proof.h | 1 + 1 file changed, 1 insertion(+) (limited to 'src/proof/bitvector_proof.h') 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 */ -- cgit v1.2.3