From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 3 May 2018 22:34:43 +0000 (-0700)
Subject: Fix warnings in proof code (#1850)
X-Git-Tag: cvc5-1.0.0~5095
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=475a7de39316ee13bd279a090c30c52bc61978ce;p=cvc5.git

Fix warnings in proof code (#1850)
---

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 2052adeac..6ca27352b 100644
--- 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 ea865f9d8..c62af75b8 100644
--- 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 a41d5d515..93e8dfb46 100644
--- 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 34f3a92ec..d6181423f 100644
--- 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 efe05bce8..b49929be5 100644
--- 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 a4e4cff0b..c8dae9cff 100644
--- 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);