diff options
author | Tim King <taking@cs.nyu.edu> | 2018-02-06 15:55:40 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-06 15:55:40 -0800 |
commit | b258ebd1cb08252f8cf7f317c08eadbe1fb8e8fe (patch) | |
tree | ad5a36fc8bad0c95ef7e9538314e81ce683c2cee /src/theory/arrays | |
parent | af20fc43b48217ebc402ad0def388e7a21b49c47 (diff) |
Resolving warnings from -Winconsistent-missing-override on clang. (#1563)
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 77 |
1 files changed, 32 insertions, 45 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 24c286e92..caf466c0c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -143,9 +143,9 @@ class TheoryArrays : public Theory { std::string name = ""); ~TheoryArrays(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - std::string identify() const { return std::string("TheoryArrays"); } + std::string identify() const override { return std::string("TheoryArrays"); } ///////////////////////////////////////////////////////////////////////////// // PREPROCESSING @@ -174,17 +174,15 @@ class TheoryArrays : public Theory { bool ppDisequal(TNode a, TNode b); Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck); - public: - - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); + public: + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + Node ppRewrite(TNode atom) override; ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// - private: - + private: /** Literals to propagate */ context::CDList<Node> d_literalsToPropagate; @@ -204,19 +202,17 @@ class TheoryArrays : public Theory { /** Helper for preRegisterTerm, also used internally */ void preRegisterTermInternal(TNode n); - public: - - void preRegisterTerm(TNode n); - void propagate(Effort e); + public: + void preRegisterTerm(TNode n) override; + void propagate(Effort e) override; Node explain(TNode n, eq::EqProof* proof); - Node explain(TNode n); + Node explain(TNode n) override; ///////////////////////////////////////////////////////////////////////////// // SHARING ///////////////////////////////////////////////////////////////////////////// - private: - + private: class MayEqualNotifyClass { public: bool notify(TNode propagation) { return true; } @@ -232,46 +228,40 @@ class TheoryArrays : public Theory { // Helper for computeCareGraph void checkPair(TNode r1, TNode r2); - public: - - void addSharedTerm(TNode t); - EqualityStatus getEqualityStatus(TNode a, TNode b); - void computeCareGraph(); + public: + void addSharedTerm(TNode t) override; + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + void computeCareGraph() override; bool isShared(TNode t) - { return (d_sharedArrays.find(t) != d_sharedArrays.end()); } - + { + return (d_sharedArrays.find(t) != d_sharedArrays.end()); + } ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - private: - - public: - bool collectModelInfo(TheoryModel* m) override; - - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// + public: + bool collectModelInfo(TheoryModel* m) override; - private: - public: + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// - Node getNextDecisionRequest( unsigned& priority ); + public: + Node getNextDecisionRequest(unsigned& priority) override; - void presolve(); - void shutdown() { } + void presolve() override; + void shutdown() override {} ///////////////////////////////////////////////////////////////////////////// // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// - public: - - void check(Effort e); - - private: + public: + void check(Effort e) override; + private: TNode weakEquivGetRep(TNode node); TNode weakEquivGetRepIndex(TNode node, TNode index); void visitAllLeaves(TNode reason, std::vector<TNode>& conjunctions); @@ -454,11 +444,8 @@ class TheoryArrays : public Theory { /** An equality-engine callback for proof reconstruction */ ArrayProofReconstruction d_proofReconstruction; - public: - - eq::EqualityEngine* getEqualityEngine() { - return &d_equalityEngine; - } + public: + eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } };/* class TheoryArrays */ |