Fix warnings in src/proof

Fix warning due to `ProofLetCount` being defined as `struct` in
`proof_utils.h` and `class` in `proof.h`. Fix warnings due to different
number of arguments of `printConstantDisequalityProof()` and
`printTheoryLemmaProof()` in subclasses.

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 3c96f7cf39a242e99bc148133cdc584df4aa54f3..49e0e8e2f16728d37c88375e3889076662cee3e2 100644 (file)
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -1054,7 +1054,7 @@ bool LFSCBitVectorProof::hasAlias(Expr expr) {
   return d_assignedAliases.find(expr) != d_assignedAliases.end();
 }
 
-void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
   Assert (c1.isConst());
   Assert (c2.isConst());
   Assert (utils::getSize(c1) == utils::getSize(c2));

diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index f897749452d8ee8667586e8573a86a91099f381c..6b952e35cf3a78cc5b20763dbf5cd95f9ad1c4a9 100644 (file)
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -157,7 +157,7 @@ public:
   virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
   void calculateAtomsInBitblastingProof();
   const std::set<Node>* getAtomsInBitblastingProof();
-  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
   void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 };
 

diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index 546d419fccb03877d251c685d8087788b1726802..b172217d86fbee7e4bc59518c2256934f4192c0e 100644 (file)
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -33,7 +33,8 @@ typedef std::pair<Node, Node> NodePair;
 typedef std::set<NodePair> NodePairSet;
 
 
-struct ProofLetCount {
+class ProofLetCount {
+public:
   static unsigned counter;
   static void resetCounter() { counter = 0; }
   static unsigned newId() { return ++counter; }

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index eae8a68dffbd67b56e357a1bae109c226b7ed04f..8aefaae45f406367abfa0689acf8133c3586d1ad 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1167,7 +1167,8 @@ void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream&
 
 void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                              std::ostream& os,
-                                             std::ostream& paren) {
+                                             std::ostream& paren,
+                                             const ProofLetMap& map) {
   Unreachable("No boolean lemmas yet!");
 }
 

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index c622fabee7532dfd614c2d27d9a7e9795c3774dd..80a737580206c498c986f56f422aa3a114444069 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -308,7 +308,7 @@ public:
   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
 
   virtual void printOwnedSort(Type type, std::ostream& os) = 0;
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0;
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) = 0;
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
@@ -322,7 +322,7 @@ public:
   {}
   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);