Fix warnings in proof code (#1850)

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 2052adeac69b32efc30dde8964351d7b8ac0305e..6ca27352bf25d729cb41fc123226be00627e6e99 100644 (file)
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -63,7 +63,7 @@ protected:
   ExprSet d_declarations; // all the variable/function declarations
 
   bool d_realMode;
-  theory::TheoryId getTheoryId();
+  theory::TheoryId getTheoryId() override;
 
  public:
   ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine);

diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index ea865f9d801063d11e55f3d61e2d26d6de3f5f25..c62af75b824baf75924998a84e371d2e1c1084e6 100644 (file)
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -79,7 +79,7 @@ protected:
   ExprSet d_declarations; // all the variable/function declarations
   ExprSet d_skolemDeclarations; // all the skolem variable declarations
   std::map<Expr, std::string> d_skolemToLiteral;
-  theory::TheoryId getTheoryId();
+  theory::TheoryId getTheoryId() override;
 
  public:
   ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine);

diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index a41d5d515c706c729234adc48127cef213ecdf44..93e8dfb46c387e352b7ca4cd260fe12842db41d2 100644 (file)
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -83,7 +83,7 @@ protected:
 
   std::map<Expr,std::string> d_constantLetMap;
   bool d_useConstantLetification;
-  theory::TheoryId getTheoryId();
+  theory::TheoryId getTheoryId() override;
   context::Context d_fakeContext;
 public:
   BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 34f3a92ecfd6aac4f629db950265f6a8b4546127..d6181423f26f84f69b347d472eeff844036bd3c1 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1264,7 +1264,7 @@ void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node
   os << "))";
 }
 
-inline bool TheoryProof::match(TNode n1, TNode n2)
+bool TheoryProof::match(TNode n1, TNode n2)
 {
   theory::TheoryId theoryId = this->getTheoryId();
   ProofManager* pm = ProofManager::currentPM();

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index efe05bce80629a844258e75a32f985d06a56a957..b49929be5b7bf751e27224645fd08f913dd390bb 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -242,7 +242,7 @@ protected:
   }
 
   // congrence matching term helper
-  inline bool match(TNode n1, TNode n2);
+  bool match(TNode n1, TNode n2);
 
   /**
    * Helper function for ProofUF::toStreamRecLFSC and
@@ -363,7 +363,7 @@ protected:
 class BooleanProof : public TheoryProof {
 protected:
   ExprSet d_declarations; // all the boolean variables
-  theory::TheoryId getTheoryId();
+  theory::TheoryId getTheoryId() override;
 
  public:
   BooleanProof(TheoryProofEngine* proofEngine);

diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index a4e4cff0b2036f242b83ff682b94dde451f7aaa9..c8dae9cff213d7d337ac675bd0b4f3dad49b7f91 100644 (file)
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -62,7 +62,7 @@ class UFProof : public TheoryProof {
 protected:
   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
   ExprSet d_declarations; // all the variable/function declarations
-  theory::TheoryId getTheoryId();
+  theory::TheoryId getTheoryId() override;
 
  public:
   UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);