summaryrefslogtreecommitdiff
path: root/src/proof/uf_proof.h
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-03-05 15:36:50 -0800
committerGitHub <noreply@github.com>2018-03-05 15:36:50 -0800
commit3d31caa30e094d337a4919b3d1e6ba9259e461b8 (patch)
treee99bc99c2ce450f7d0c4fa8c0938b24e886af996 /src/proof/uf_proof.h
parenta2e78ec8dd5e935b6ef166154be7ee35bffc6d32 (diff)
Enable -Wsuggest-override by default. (#1643)
Adds missing override keywords.
Diffstat (limited to 'src/proof/uf_proof.h')
-rw-r--r--src/proof/uf_proof.h35
1 files changed, 23 insertions, 12 deletions
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 1b14bd15f..7aa00cc35 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -66,7 +66,7 @@ protected:
public:
UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
};
class LFSCUFProof : public UFProof {
@@ -74,17 +74,28 @@ public:
LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine)
: UFProof(uf, proofEngine)
{}
- 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, 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);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
-
- bool printsAsBool(const Node &n);
-
- void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
+
+ bool printsAsBool(const Node& n) override;
+
+ void printConstantDisequalityProof(std::ostream& os,
+ Expr c1,
+ Expr c2,
+ const ProofLetMap& globalLetMap) override;
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback