diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-05 15:36:50 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-05 15:36:50 -0800 |
| commit | 3d31caa30e094d337a4919b3d1e6ba9259e461b8 (patch) | |
| tree | e99bc99c2ce450f7d0c4fa8c0938b24e886af996 | |
| parent | a2e78ec8dd5e935b6ef166154be7ee35bffc6d32 (diff) | |
Enable -Wsuggest-override by default. (#1643)
Adds missing override keywords.
100 files changed, 1491 insertions, 1139 deletions
diff --git a/configure.ac b/configure.ac index ef12e4825..5dd8ae691 100644 --- a/configure.ac +++ b/configure.ac @@ -950,6 +950,7 @@ CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE]) CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES]) CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED]) CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE]) +CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE]) CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING]) AC_SUBST([WERROR]) AC_SUBST([WNO_CONVERSION_NULL]) @@ -957,8 +958,11 @@ AC_SUBST([WNO_TAUTOLOGICAL_COMPARE]) AC_SUBST([WNO_PARENTHESES]) AC_SUBST([WNO_UNINITIALIZED]) AC_SUBST([WNO_UNUSED_VARIABLE]) +AC_SUBST([W_SUGGEST_OVERRIDE]) AC_SUBST([FNO_STRICT_ALIASING]) +CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}" + # On Mac, we have to fix the visibility of standard library symbols. # Otherwise, exported template instantiations---even though explicitly # CVC4_PUBLIC, can be generated as symbols with internal-only linkage. diff --git a/src/base/output.h b/src/base/output.h index cdc0ac27f..b7f743e56 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -51,7 +51,7 @@ public: * stream. Perhaps this is not so critical, but recommended; this * way the output stream looks like it's functioning, in a non-error * state. */ - int overflow(int c) { return c; } + int overflow(int c) override { return c; } };/* class null_streambuf */ /** A null stream-buffer singleton */ diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 82aa90891..14832679d 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -111,11 +111,13 @@ class CDOhash_map : public ContextObj { CDOhash_map* d_prev; CDOhash_map* d_next; - virtual ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* save(ContextMemoryManager* pCMM) override + { return new(pCMM) CDOhash_map(*this); } - virtual void restore(ContextObj* data) { + void restore(ContextObj* data) override + { CDOhash_map* p = static_cast<CDOhash_map*>(data); if(d_map != NULL) { if(p->d_map == NULL) { @@ -279,14 +281,10 @@ class CDHashMap : public ContextObj { Context* d_context; // Nothing to save; the elements take care of themselves - virtual ContextObj* save(ContextMemoryManager* pCMM) { - Unreachable(); - } + ContextObj* save(ContextMemoryManager* pCMM) override { Unreachable(); } // Similarly, nothing to restore - virtual void restore(ContextObj* data) { - Unreachable(); - } + void restore(ContextObj* data) override { Unreachable(); } // no copy or assignment CDHashMap(const CDHashMap&) CVC4_UNDEFINED; diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index db679c1f7..9211ff7da 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -221,7 +221,8 @@ private: * restored on a pop). The saved information is allocated using the * ContextMemoryManager. */ - ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* save(ContextMemoryManager* pCMM) override + { ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this); Debug("CDInsertHashMap") << "save " << this << " at level " << this->getContext()->getLevel() @@ -237,23 +238,25 @@ protected: * of new pushFront calls have happened since saving. * The d_insertMap is untouched and d_pushFronts is also kept. */ - void restore(ContextObj* data) { - Debug("CDInsertHashMap") << "restore " << this - << " level " << this->getContext()->getLevel() - << " data == " << data - << " d_insertMap == " << this->d_insertMap << std::endl; - size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size; - size_t oldPushFronts = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts; - Assert(oldPushFronts <= d_pushFronts); - - // The size to restore to. - size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts); - d_insertMap->pop_to_size(restoreSize); - d_size = restoreSize; - Assert(d_insertMap->size() == d_size); - Debug("CDInsertHashMap") << "restore " << this - << " level " << this->getContext()->getLevel() - << " size back to " << this->d_size << std::endl; + void restore(ContextObj* data) override + { + Debug("CDInsertHashMap") + << "restore " << this << " level " << this->getContext()->getLevel() + << " data == " << data << " d_insertMap == " << this->d_insertMap + << std::endl; + size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size; + size_t oldPushFronts = + ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts; + Assert(oldPushFronts <= d_pushFronts); + + // The size to restore to. + size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts); + d_insertMap->pop_to_size(restoreSize); + d_size = restoreSize; + Assert(d_insertMap->size() == d_size); + Debug("CDInsertHashMap") + << "restore " << this << " level " << this->getContext()->getLevel() + << " size back to " << this->d_size << std::endl; } public: diff --git a/src/context/cdlist.h b/src/context/cdlist.h index aeb6567a3..e5f9f2dda 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -165,7 +165,8 @@ private: * restored on a pop). The saved information is allocated using the * ContextMemoryManager. */ - ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* save(ContextMemoryManager* pCMM) override + { ContextObj* data = new(pCMM) CDList<T, CleanUp, Allocator>(*this); Debug("cdlist") << "save " << this << " at level " << this->getContext()->getLevel() @@ -182,17 +183,17 @@ protected: * restores the previous size. Note that the list pointer and the * allocated size are not changed. */ - void restore(ContextObj* data) { - Debug("cdlist") << "restore " << this - << " level " << this->getContext()->getLevel() - << " data == " << data - << " call dtor == " << this->d_callDestructor - << " d_list == " << this->d_list << std::endl; - truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size); - Debug("cdlist") << "restore " << this - << " level " << this->getContext()->getLevel() - << " size back to " << this->d_size - << " sizeAlloc at " << this->d_sizeAlloc << std::endl; + void restore(ContextObj* data) override + { + Debug("cdlist") << "restore " << this << " level " + << this->getContext()->getLevel() << " data == " << data + << " call dtor == " << this->d_callDestructor + << " d_list == " << this->d_list << std::endl; + truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size); + Debug("cdlist") << "restore " << this << " level " + << this->getContext()->getLevel() << " size back to " + << this->d_size << " sizeAlloc at " << this->d_sizeAlloc + << std::endl; } /** diff --git a/src/context/cdo.h b/src/context/cdo.h index 3142fe8ef..bac9eb360 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -57,7 +57,8 @@ protected: * current data to a copy using the copy constructor. Memory is allocated * using the ContextMemoryManager. */ - virtual ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* save(ContextMemoryManager* pCMM) override + { Debug("context") << "save cdo " << this; ContextObj* p = new(pCMM) CDO<T>(*this); Debug("context") << " to " << p << std::endl; @@ -68,7 +69,8 @@ protected: * Implementation of mandatory ContextObj method restore: simply copies the * saved data back from the saved copy using operator= for T. */ - virtual void restore(ContextObj* pContextObj) { + void restore(ContextObj* pContextObj) override + { //Debug("context") << "restore cdo " << this; CDO<T>* p = static_cast<CDO<T>*>(pContextObj); d_data = p->d_data; diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index 1df985b48..305e2de77 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -60,7 +60,8 @@ protected: /** Implementation of mandatory ContextObj method save: * We assume that the base class do the job inside their copy constructor. */ - ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* save(ContextMemoryManager* pCMM) override + { ContextObj* data = new(pCMM) CDQueue<T, CleanUp, Allocator>(*this); // We save the d_size in d_lastsave and we should never destruct below this // indices before the corresponding restore. @@ -80,7 +81,8 @@ protected: * restores the previous size, iter and lastsave indices. Note that * the list pointer and the allocated size are not changed. */ - void restore(ContextObj* data) { + void restore(ContextObj* data) override + { CDQueue<T, CleanUp, Allocator>* qdata = static_cast<CDQueue<T, CleanUp, Allocator>*>(data); d_iter = qdata->d_iter; d_lastsave = qdata->d_lastsave; diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h index bbd71f8cd..771cea960 100644 --- a/src/context/cdtrail_hashmap.h +++ b/src/context/cdtrail_hashmap.h @@ -394,7 +394,8 @@ private: * the current sizes to a copy using the copy constructor, * The saved information is allocated using the ContextMemoryManager. */ - ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* save(ContextMemoryManager* pCMM) override + { ContextObj* data = new(pCMM) CDTrailHashMap<Key, Data, HashFcn>(*this); Debug("CDTrailHashMap") << "save " << this << " at level " << this->getContext()->getLevel() @@ -409,20 +410,23 @@ protected: * restores the previous size. Note that the list pointer and the * allocated size are not changed. */ - void restore(ContextObj* data) { - Debug("CDTrailHashMap") << "restore " << this - << " level " << this->getContext()->getLevel() - << " data == " << data - << " d_trailMap == " << this->d_trailMap << std::endl; - size_t oldSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_trailSize; - d_trailMap->pop_to_size(oldSize); - d_trailSize = oldSize; - Assert(d_trailMap->trailSize() == d_trailSize); - - d_prevTrailSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_prevTrailSize; - Debug("CDTrailHashMap") << "restore " << this - << " level " << this->getContext()->getLevel() - << " size back to " << this->d_trailSize << std::endl; + void restore(ContextObj* data) override + { + Debug("CDTrailHashMap") << "restore " << this << " level " + << this->getContext()->getLevel() + << " data == " << data + << " d_trailMap == " << this->d_trailMap + << std::endl; + size_t oldSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_trailSize; + d_trailMap->pop_to_size(oldSize); + d_trailSize = oldSize; + Assert(d_trailMap->trailSize() == d_trailSize); + + d_prevTrailSize = + ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_prevTrailSize; + Debug("CDTrailHashMap") << "restore " << this << " level " + << this->getContext()->getLevel() << " size back to " + << this->d_trailSize << std::endl; } /** diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 25334b777..9b1033c86 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -55,8 +55,7 @@ public: DecisionStrategy(de, c) { } - - bool needIteSkolemMap() { return true; } + bool needIteSkolemMap() override { return true; } virtual void addAssertions(const std::vector<Node> &assertions, unsigned assertionsEnd, diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 210ab4d5c..47cccfbe5 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -117,13 +117,13 @@ public: ~JustificationHeuristic(); - prop::SatLiteral getNext(bool &stopSearch); + prop::SatLiteral getNext(bool &stopSearch) override; void addAssertions(const std::vector<Node> &assertions, unsigned assertionsEnd, - IteSkolemMap iteSkolemMap); + IteSkolemMap iteSkolemMap) override; -private: + private: /* getNext with an option to specify threshold */ prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold); diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h index bdfe5a487..2f2c48ada 100644 --- a/src/expr/node_manager_listeners.h +++ b/src/expr/node_manager_listeners.h @@ -28,7 +28,8 @@ namespace expr { class TlimitListener : public Listener { public: TlimitListener(ResourceManager* rm) : d_rm(rm) {} - virtual void notify(); + void notify() override; + private: ResourceManager* d_rm; }; @@ -36,7 +37,8 @@ class TlimitListener : public Listener { class TlimitPerListener : public Listener { public: TlimitPerListener(ResourceManager* rm) : d_rm(rm) {} - virtual void notify(); + void notify() override; + private: ResourceManager* d_rm; }; @@ -44,7 +46,8 @@ class TlimitPerListener : public Listener { class RlimitListener : public Listener { public: RlimitListener(ResourceManager* rm) : d_rm(rm) {} - virtual void notify(); + void notify() override; + private: ResourceManager* d_rm; }; @@ -52,7 +55,8 @@ class RlimitListener : public Listener { class RlimitPerListener : public Listener { public: RlimitPerListener(ResourceManager* rm) : d_rm(rm) {} - virtual void notify(); + void notify() override; + private: ResourceManager* d_rm; }; diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am index 8db3d664c..aec9fa634 100644 --- a/src/lib/Makefile.am +++ b/src/lib/Makefile.am @@ -3,6 +3,10 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) +# This is a workaround for now to fix some warnings related to unsupported +# compiler flags since we are compiling C code here. CXXFLAGS is set via +# configure, however, we should actually set AM_CXXFLAGS. +CXXFLAGS = $(AM_CXXFLAGS) noinst_LTLIBRARIES = libreplacements.la diff --git a/src/options/argument_extender_implementation.h b/src/options/argument_extender_implementation.h index 859a88b3e..efcd55cae 100644 --- a/src/options/argument_extender_implementation.h +++ b/src/options/argument_extender_implementation.h @@ -50,39 +50,39 @@ class ArgumentExtenderImplementation : public ArgumentExtender { * Preconditions: * - argc and argv are non-null. */ - void getArguments(int* argc, char*** argv) const; + void getArguments(int* argc, char*** argv) const override; /** Returns the number of arguments that are . */ - size_t numArguments() const; + size_t numArguments() const override; /** * Inserts a copy of element into the front of the arguments list. * Preconditions: element is non-null and 0 terminated. */ - void pushFrontArgument(const char* element); + void pushFrontArgument(const char* element) override; /** * Inserts a copy of element into the back of the arguments list. * Preconditions: element is non-null and 0 terminated. */ - void pushBackArgument(const char* element); + void pushBackArgument(const char* element) override; /** Removes the front of the arguments list.*/ - void popFrontArgument(); + void popFrontArgument() override; /** Adds a new preemption to the arguments list. */ - void pushBackPreemption(const char* element); + void pushBackPreemption(const char* element) override; /** * Moves all of the preemptions into the front of the arguments * list. */ - void movePreemptionsToArguments(); + void movePreemptionsToArguments() override; /** Returns true iff there is a pending preemption.*/ - bool hasPreemptions() const; + bool hasPreemptions() const override; -private: + private: typedef std::list< char* > CharPointerList; diff --git a/src/parser/parser.h b/src/parser/parser.h index 7f64b9580..949c56605 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -794,7 +794,7 @@ public: public: ExprStream(Parser* parser) : d_parser(parser) {} ~ExprStream() { delete d_parser; } - Expr nextExpr() { return d_parser->nextExpression(); } + Expr nextExpr() override { return d_parser->nextExpression(); } };/* class Parser::ExprStream */ //------------------------ operator overloading diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index 49a4b8000..1c15df5d3 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -103,7 +103,7 @@ public: */ void addTheory(Theory theory); - bool logicIsSet(); + bool logicIsSet() override; /** * Sets the logic for the current benchmark. Declares any logic and theory symbols. diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 94bc03235..71aa32492 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -84,12 +84,12 @@ public: bool isTheoryEnabled(Theory theory) const; - bool logicIsSet(); - + bool logicIsSet() override; + /** * Returns the expression that name should be interpreted as. */ - virtual Expr getExpressionForNameAndType(const std::string& name, Type t); + Expr getExpressionForNameAndType(const std::string& name, Type t) override; /** Make function defined by a define-fun(s)-rec command. * @@ -135,7 +135,7 @@ public: std::vector<Expr>& bvs, bool bindingLevel = false); - void reset(); + void reset() override; void resetAssertions(); diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 0a44f45c0..677952bf7 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -67,7 +67,7 @@ protected: public: ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine); - virtual void registerTerm(Expr term); + void registerTerm(Expr term) override; }; class LFSCArithProof : public ArithProof { @@ -75,13 +75,21 @@ public: LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine) : ArithProof(arith, 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); + 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; }; diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 99ad956a5..779624df0 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -85,7 +85,7 @@ public: std::string skolemToLiteral(Expr skolem); - virtual void registerTerm(Expr term); + void registerTerm(Expr term) override; }; class LFSCArrayProof : public ArrayProof { @@ -94,15 +94,23 @@ public: : ArrayProof(arrays, 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 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; }; diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 69f9e774b..b5487a352 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -110,7 +110,7 @@ public: void registerTermBB(Expr term); void registerAtomBB(Expr atom, Expr atom_bb); - virtual void registerTerm(Expr term); + void registerTerm(Expr term) override; virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; @@ -143,22 +143,37 @@ public: LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) :BitVectorProof(bv, proofEngine) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); - virtual void printOwnedSort(Type type, std::ostream& os); - virtual void printTermBitblasting(Expr term, std::ostream& os); - virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap); - virtual void printAtomBitblastingToFalse(Expr term, 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); - virtual void printBitblasting(std::ostream& os, std::ostream& paren); - 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, const ProofLetMap &globalLetMap); - void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); + void printOwnedTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) override; + void printOwnedSort(Type type, std::ostream& os) override; + void printTermBitblasting(Expr term, std::ostream& os) override; + void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override; + void printAtomBitblastingToFalse(Expr term, 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; + void printBitblasting(std::ostream& os, std::ostream& paren) override; + void printResolutionProof(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) override; + void calculateAtomsInBitblastingProof() override; + const std::set<Node>* getAtomsInBitblastingProof() override; + void printConstantDisequalityProof(std::ostream& os, + Expr c1, + Expr c2, + const ProofLetMap& globalLetMap) override; + void printRewriteProof(std::ostream& os, + const Node& n1, + const Node& n2) override; }; }/* CVC4 namespace */ diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index a0d7096c0..9087817b3 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -171,20 +171,20 @@ public: void printAtomMapping(const std::set<Node>& atoms, std::ostream& os, - std::ostream& paren); + std::ostream& paren) override; void printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren, - ProofLetMap &letMap); + ProofLetMap& letMap) override; void printClause(const prop::SatClause& clause, std::ostream& os, - std::ostream& paren); + std::ostream& paren) override; void printCnfProofForClause(ClauseId id, const prop::SatClause* clause, std::ostream& os, - std::ostream& paren); + std::ostream& paren) override; };/* class LFSCCnfProof */ } /* CVC4 namespace */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 4ed2360c2..19a8d30cf 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -396,13 +396,15 @@ class LFSCSatProof : public TSatProof<SatSolver> { LFSCSatProof(SatSolver* solver, context::Context* context, const std::string& name, bool checkRes = false) : TSatProof<SatSolver>(solver, context, name, checkRes) {} - virtual void printResolution(ClauseId id, std::ostream& out, - std::ostream& paren); - virtual void printResolutions(std::ostream& out, std::ostream& paren); - virtual void printResolutionEmptyClause(std::ostream& out, - std::ostream& paren); - virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, - std::ostream& paren); + void printResolution(ClauseId id, + std::ostream& out, + std::ostream& paren) override; + void printResolutions(std::ostream& out, std::ostream& paren) override; + void printResolutionEmptyClause(std::ostream& out, + std::ostream& paren) override; + void printAssumptionsResolution(ClauseId id, + std::ostream& out, + std::ostream& paren) override; }; /* class LFSCSatProof */ template <class Solver> diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 15ac533b7..4e599f570 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -163,23 +163,32 @@ public: LFSCTheoryProofEngine() : TheoryProofEngine() {} - void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map); + void printTheoryTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) override; - void registerTermsFromAssertions(); + void registerTermsFromAssertions() override; void printSortDeclarations(std::ostream& os, std::ostream& paren); void printTermDeclarations(std::ostream& os, std::ostream& paren); - virtual void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map); - virtual void printLetTerm(Expr term, std::ostream& os); - virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map); - virtual void printAssertions(std::ostream& os, std::ostream& paren); - virtual void printLemmaRewrites(NodePairSet& rewrites, 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); - virtual void printTheoryLemmas(const IdToSatClause& lemmas, - std::ostream& os, + void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map); + void printLetTerm(Expr term, std::ostream& os) override; + void printBoundTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) override; + void printAssertions(std::ostream& os, std::ostream& paren) override; + void printLemmaRewrites(NodePairSet& rewrites, + std::ostream& os, + std::ostream& paren); + void printDeferredDeclarations(std::ostream& os, + std::ostream& paren) override; + void printAliasingDeclarations(std::ostream& os, std::ostream& paren, - ProofLetMap& map); - virtual void printSort(Type type, std::ostream& os); + const ProofLetMap& globalLetMap) override; + void printTheoryLemmas(const IdToSatClause& lemmas, + std::ostream& os, + std::ostream& paren, + ProofLetMap& map) override; + void printSort(Type type, std::ostream& os) override; void performExtraRegistrations(); @@ -307,16 +316,7 @@ protected: public: BooleanProof(TheoryProofEngine* proofEngine); - virtual void registerTerm(Expr term); - - 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, 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; - virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0; + void registerTerm(Expr term) override; }; class LFSCBooleanProof : public BooleanProof { @@ -324,16 +324,27 @@ public: LFSCBooleanProof(TheoryProofEngine* proofEngine) : BooleanProof(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); + 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); - void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); + bool printsAsBool(const Node& n) override; + void printConstantDisequalityProof(std::ostream& os, + Expr c1, + Expr c2, + const ProofLetMap& globalLetMap) override; }; } /* CVC4 namespace */ 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; }; diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 7dd708ca2..4395cdf6d 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -37,13 +37,16 @@ class BVMinisatSatSolver : public BVSatSolverInterface, public: MinisatNotify(BVSatSolverInterface::Notify* notify) : d_notify(notify) {} - bool notify(BVMinisat::Lit lit) + bool notify(BVMinisat::Lit lit) override { return d_notify->notify(toSatLiteral(lit)); } - void notify(BVMinisat::vec<BVMinisat::Lit>& clause); - void spendResource(unsigned amount) { d_notify->spendResource(amount); } - void safePoint(unsigned amount) { d_notify->safePoint(amount); } + void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override; + void spendResource(unsigned amount) override + { + d_notify->spendResource(amount); + } + void safePoint(unsigned amount) override { d_notify->safePoint(amount); } }; BVMinisat::SimpSolver* d_minisat; @@ -54,45 +57,46 @@ class BVMinisatSatSolver : public BVSatSolverInterface, context::CDO<unsigned> d_lastPropagation; protected: - - void contextNotifyPop(); + void contextNotifyPop() override; public: BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = ""); virtual ~BVMinisatSatSolver(); - void setNotify(Notify* notify); + void setNotify(Notify* notify) override; - ClauseId addClause(SatClause& clause, bool removable); + ClauseId addClause(SatClause& clause, bool removable) override; - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override + { Unreachable("Minisat does not support native XOR reasoning"); } - - SatValue propagate(); - SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); + SatValue propagate() override; - SatVariable trueVar() { return d_minisat->trueVar(); } - SatVariable falseVar() { return d_minisat->falseVar(); } + SatVariable newVar(bool isTheoryAtom = false, + bool preRegister = false, + bool canErase = true) override; - void markUnremovable(SatLiteral lit); + SatVariable trueVar() override { return d_minisat->trueVar(); } + SatVariable falseVar() override { return d_minisat->falseVar(); } - void interrupt(); + void markUnremovable(SatLiteral lit) override; - SatValue solve(); - SatValue solve(long unsigned int&); - bool ok() const; - void getUnsatCore(SatClause& unsatCore); + void interrupt() override; - SatValue value(SatLiteral l); - SatValue modelValue(SatLiteral l); + SatValue solve() override; + SatValue solve(long unsigned int&) override; + bool ok() const override; + void getUnsatCore(SatClause& unsatCore) override; + + SatValue value(SatLiteral l) override; + SatValue modelValue(SatLiteral l) override; void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); - unsigned getAssertionLevel() const; - + unsigned getAssertionLevel() const override; // helper methods for converting from the internal Minisat representation @@ -103,17 +107,17 @@ public: static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); static void toSatClause (const BVMinisat::Clause& clause, SatClause& sat_clause); - void addMarkerLiteral(SatLiteral lit); + void addMarkerLiteral(SatLiteral lit) override; - void explain(SatLiteral lit, std::vector<SatLiteral>& explanation); + void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) override; - SatValue assertAssumption(SatLiteral lit, bool propagate); + SatValue assertAssumption(SatLiteral lit, bool propagate) override; - void popAssumption(); - - void setProofLog( BitVectorProof * bvp ); + void popAssumption() override; -private: + void setProofLog(BitVectorProof* bvp) override; + + private: /* Disable the default constructor. */ BVMinisatSatSolver() CVC4_UNDEFINED; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 9854bf77d..246bb7152 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -69,8 +69,7 @@ class SimpSolver : public Solver { // Memory managment: // - virtual void garbageCollect(); - + void garbageCollect() override; // Generate a (possibly simplified) DIMACS file: // diff --git a/src/prop/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h index 12321cba2..698035b7c 100644 --- a/src/prop/bvminisat/utils/Options.h +++ b/src/prop/bvminisat/utils/Options.h @@ -135,42 +135,58 @@ class DoubleOption : public Option operator double& (void) { return value; } DoubleOption& operator=(double x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; + bool parse(const char* str) override + { + const char* span = str; - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; - - char* end; - double tmp = strtod(span, &end); - - if (end == NULL) - return false; - else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; - // fprintf(stderr, "READ VALUE: %g\n", value); + char* end; + double tmp = strtod(span, &end); - return true; + if (end == NULL) + return false; + else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp <= range.begin + && (!range.begin_inclusive || tmp != range.begin)) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + // fprintf(stderr, "READ VALUE: %g\n", value); + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", - name, type_name, - range.begin_inclusive ? '[' : '(', - range.begin, - range.end, - range.end_inclusive ? ']' : ')', - value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, + " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", + name, + type_name, + range.begin_inclusive ? '[' : '(', + range.begin, + range.end, + range.end_inclusive ? ']' : ')', + value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -193,47 +209,60 @@ class IntOption : public Option operator int32_t& (void) { return value; } IntOption& operator= (int32_t x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + bool parse(const char* str) override + { + const char* span = str; - char* end; - int32_t tmp = strtol(span, &end, 10); - - if (end == NULL) - return false; - else if (tmp > range.end){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp < range.begin){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; + char* end; + int32_t tmp = strtol(span, &end, 10); - return true; + if (end == NULL) + return false; + else if (tmp > range.end) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp < range.begin) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT32_MIN) - fprintf(stderr, "imin"); - else - fprintf(stderr, "%4d", range.begin); - - fprintf(stderr, " .. "); - if (range.end == INT32_MAX) - fprintf(stderr, "imax"); - else - fprintf(stderr, "%4d", range.end); - - fprintf(stderr, "] (default: %d)\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-12s = %-8s [", name, type_name); + if (range.begin == INT32_MIN) + fprintf(stderr, "imin"); + else + fprintf(stderr, "%4d", range.begin); + + fprintf(stderr, " .. "); + if (range.end == INT32_MAX) + fprintf(stderr, "imax"); + else + fprintf(stderr, "%4d", range.end); + + fprintf(stderr, "] (default: %d)\n", value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -255,47 +284,60 @@ class Int64Option : public Option operator int64_t& (void) { return value; } Int64Option& operator= (int64_t x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + bool parse(const char* str) override + { + const char* span = str; - char* end; - int64_t tmp = strtoll(span, &end, 10); - - if (end == NULL) - return false; - else if (tmp > range.end){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp < range.begin){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; + char* end; + int64_t tmp = strtoll(span, &end, 10); - return true; + if (end == NULL) + return false; + else if (tmp > range.end) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp < range.begin) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT64_MIN) - fprintf(stderr, "imin"); - else - fprintf(stderr, "%4" PRIi64, range.begin); - - fprintf(stderr, " .. "); - if (range.end == INT64_MAX) - fprintf(stderr, "imax"); - else - fprintf(stderr, "%4" PRIi64, range.end); - - fprintf(stderr, "] (default: %" PRIi64")\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-12s = %-8s [", name, type_name); + if (range.begin == INT64_MIN) + fprintf(stderr, "imin"); + else + fprintf(stderr, "%4" PRIi64, range.begin); + + fprintf(stderr, " .. "); + if (range.end == INT64_MAX) + fprintf(stderr, "imax"); + else + fprintf(stderr, "%4" PRIi64, range.end); + + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; #endif @@ -315,22 +357,25 @@ class StringOption : public Option operator const char*& (void) { return value; } StringOption& operator= (const char* x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; + bool parse(const char* str) override + { + const char* span = str; - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = span; - return true; + value = span; + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-10s = %8s\n", name, type_name); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-10s = %8s\n", name, type_name); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -351,33 +396,37 @@ class BoolOption : public Option operator bool& (void) { return value; } BoolOption& operator=(bool b) { value = b; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (match(span, "-")){ - bool b = !match(span, "no-"); + bool parse(const char* str) override + { + const char* span = str; + + if (match(span, "-")) + { + bool b = !match(span, "no-"); - if (strcmp(span, name) == 0){ - value = b; - return true; } + if (strcmp(span, name) == 0) + { + value = b; + return true; } + } - return false; + return false; } - virtual void help (bool verbose = false){ + void help(bool verbose = false) override + { + fprintf(stderr, " -%s, -no-%s", name, name); - fprintf(stderr, " -%s, -no-%s", name, name); + for (uint32_t i = 0; i < 32 - strlen(name) * 2; i++) fprintf(stderr, " "); - for (uint32_t i = 0; i < 32 - strlen(name)*2; i++) - fprintf(stderr, " "); - - fprintf(stderr, " "); - fprintf(stderr, "(default: %s)\n", value ? "on" : "off"); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + fprintf(stderr, " "); + fprintf(stderr, "(default: %s)\n", value ? "on" : "off"); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 80f8742a3..174263be0 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -286,8 +286,11 @@ class TseitinCnfStream : public CnfStream { * @param removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool removable, bool negated, - ProofRule rule, TNode from = TNode::null()); + void convertAndAssert(TNode node, + bool removable, + bool negated, + ProofRule rule, + TNode from = TNode::null()) override; private: /** @@ -328,7 +331,7 @@ class TseitinCnfStream : public CnfStream { */ SatLiteral toCNF(TNode node, bool negated = false); - void ensureLiteral(TNode n, bool noPreregistration = false); + void ensureLiteral(TNode n, bool noPreregistration = false) override; }; /* class TseitinCnfStream */ diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index ca179fbc8..58e02179c 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -39,45 +39,48 @@ public: static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); - void initialize(context::Context* context, TheoryProxy* theoryProxy); + void initialize(context::Context* context, TheoryProxy* theoryProxy) override; - ClauseId addClause(SatClause& clause, bool removable); - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + ClauseId addClause(SatClause& clause, bool removable) override; + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override + { Unreachable("Minisat does not support native XOR reasoning"); } - SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); - SatVariable trueVar() { return d_minisat->trueVar(); } - SatVariable falseVar() { return d_minisat->falseVar(); } + SatVariable newVar(bool isTheoryAtom, + bool preRegister, + bool canErase) override; + SatVariable trueVar() override { return d_minisat->trueVar(); } + SatVariable falseVar() override { return d_minisat->falseVar(); } - SatValue solve(); - SatValue solve(long unsigned int&); + SatValue solve() override; + SatValue solve(long unsigned int&) override; - bool ok() const; - - void interrupt(); + bool ok() const override; - SatValue value(SatLiteral l); + void interrupt() override; - SatValue modelValue(SatLiteral l); + SatValue value(SatLiteral l) override; - bool properExplanation(SatLiteral lit, SatLiteral expl) const; + SatValue modelValue(SatLiteral l) override; + + bool properExplanation(SatLiteral lit, SatLiteral expl) const override; /** Incremental interface */ - unsigned getAssertionLevel() const; + unsigned getAssertionLevel() const override; - void push(); + void push() override; - void pop(); + void pop() override; - void requirePhase(SatLiteral lit); + void requirePhase(SatLiteral lit) override; - bool flipDecision(); + bool flipDecision() override; - bool isDecision(SatVariable decn) const; + bool isDecision(SatVariable decn) const override; -private: + private: /** The SatSolver used */ Minisat::SimpSolver* d_minisat; diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index a995c1357..335075f09 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -74,8 +74,7 @@ class SimpSolver : public Solver { // Memory managment: // - virtual void garbageCollect(); - + void garbageCollect() override; // Generate a (possibly simplified) DIMACS file: // diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h index 0577cbbd0..9bddd2b23 100644 --- a/src/prop/minisat/utils/Options.h +++ b/src/prop/minisat/utils/Options.h @@ -135,42 +135,58 @@ class DoubleOption : public Option operator double& (void) { return value; } DoubleOption& operator=(double x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; + bool parse(const char* str) override + { + const char* span = str; - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; - - char* end; - double tmp = strtod(span, &end); - - if (end == NULL) - return false; - else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; - // fprintf(stderr, "READ VALUE: %g\n", value); + char* end; + double tmp = strtod(span, &end); - return true; + if (end == NULL) + return false; + else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp <= range.begin + && (!range.begin_inclusive || tmp != range.begin)) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + // fprintf(stderr, "READ VALUE: %g\n", value); + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", - name, type_name, - range.begin_inclusive ? '[' : '(', - range.begin, - range.end, - range.end_inclusive ? ']' : ')', - value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, + " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", + name, + type_name, + range.begin_inclusive ? '[' : '(', + range.begin, + range.end, + range.end_inclusive ? ']' : ')', + value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -193,47 +209,60 @@ class IntOption : public Option operator int32_t& (void) { return value; } IntOption& operator= (int32_t x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + bool parse(const char* str) override + { + const char* span = str; - char* end; - int32_t tmp = strtol(span, &end, 10); - - if (end == NULL) - return false; - else if (tmp > range.end){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp < range.begin){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; + char* end; + int32_t tmp = strtol(span, &end, 10); - return true; + if (end == NULL) + return false; + else if (tmp > range.end) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp < range.begin) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT32_MIN) - fprintf(stderr, "imin"); - else - fprintf(stderr, "%4d", range.begin); - - fprintf(stderr, " .. "); - if (range.end == INT32_MAX) - fprintf(stderr, "imax"); - else - fprintf(stderr, "%4d", range.end); - - fprintf(stderr, "] (default: %d)\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-12s = %-8s [", name, type_name); + if (range.begin == INT32_MIN) + fprintf(stderr, "imin"); + else + fprintf(stderr, "%4d", range.begin); + + fprintf(stderr, " .. "); + if (range.end == INT32_MAX) + fprintf(stderr, "imax"); + else + fprintf(stderr, "%4d", range.end); + + fprintf(stderr, "] (default: %d)\n", value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -255,47 +284,60 @@ class Int64Option : public Option operator int64_t& (void) { return value; } Int64Option& operator= (int64_t x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + bool parse(const char* str) override + { + const char* span = str; - char* end; - int64_t tmp = strtoll(span, &end, 10); - - if (end == NULL) - return false; - else if (tmp > range.end){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp < range.begin){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; + char* end; + int64_t tmp = strtoll(span, &end, 10); - return true; + if (end == NULL) + return false; + else if (tmp > range.end) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp < range.begin) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT64_MIN) - fprintf(stderr, "imin"); - else - fprintf(stderr, "%4" PRIi64, range.begin); - - fprintf(stderr, " .. "); - if (range.end == INT64_MAX) - fprintf(stderr, "imax"); - else - fprintf(stderr, "%4" PRIi64, range.end); - - fprintf(stderr, "] (default: %" PRIi64")\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-12s = %-8s [", name, type_name); + if (range.begin == INT64_MIN) + fprintf(stderr, "imin"); + else + fprintf(stderr, "%4" PRIi64, range.begin); + + fprintf(stderr, " .. "); + if (range.end == INT64_MAX) + fprintf(stderr, "imax"); + else + fprintf(stderr, "%4" PRIi64, range.end); + + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; #endif @@ -315,22 +357,25 @@ class StringOption : public Option operator const char*& (void) { return value; } StringOption& operator= (const char* x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; + bool parse(const char* str) override + { + const char* span = str; - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = span; - return true; + value = span; + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-10s = %8s\n", name, type_name); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-10s = %8s\n", name, type_name); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -351,33 +396,37 @@ class BoolOption : public Option operator bool& (void) { return value; } BoolOption& operator=(bool b) { value = b; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (match(span, "-")){ - bool b = !match(span, "no-"); + bool parse(const char* str) override + { + const char* span = str; + + if (match(span, "-")) + { + bool b = !match(span, "no-"); - if (strcmp(span, name) == 0){ - value = b; - return true; } + if (strcmp(span, name) == 0) + { + value = b; + return true; } + } - return false; + return false; } - virtual void help (bool verbose = false){ + void help(bool verbose = false) override + { + fprintf(stderr, " -%s, -no-%s", name, name); - fprintf(stderr, " -%s, -no-%s", name, name); + for (uint32_t i = 0; i < 32 - strlen(name) * 2; i++) fprintf(stderr, " "); - for (uint32_t i = 0; i < 32 - strlen(name)*2; i++) - fprintf(stderr, " "); - - fprintf(stderr, " "); - fprintf(stderr, "(default: %s)\n", value ? "on" : "off"); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + fprintf(stderr, " "); + fprintf(stderr, "(default: %s)\n", value ? "on" : "off"); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; diff --git a/src/prop/registrar.h b/src/prop/registrar.h index ec774e979..9735aa43d 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -35,7 +35,7 @@ public: class NullRegistrar : public Registrar { public: - void preRegister(Node n) {} + void preRegister(Node n) override {} };/* class NullRegistrar */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 7be5305ad..4dc95e060 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -137,10 +137,6 @@ public: virtual void popAssumption() = 0; - virtual bool ok() const = 0; - - virtual void setProofLog( BitVectorProof * bvp ) {} - };/* class BVSatSolverInterface */ @@ -159,8 +155,6 @@ public: virtual bool flipDecision() = 0; virtual bool isDecision(SatVariable decn) const = 0; - - virtual bool ok() const = 0; };/* class DPLLSatSolverInterface */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index 3114821b3..f2566d35c 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -79,7 +79,8 @@ class SetToDefaultSourceListener : public Listener { SetToDefaultSourceListener(ManagedOstream* managedOstream) : d_managedOstream(managedOstream){} - virtual void notify() { + void notify() override + { d_managedOstream->set(d_managedOstream->defaultSource()); } @@ -97,15 +98,15 @@ class ManagedDumpOStream : public ManagedOstream { ManagedDumpOStream(){} ~ManagedDumpOStream(); - virtual const char* getName() const { return "dump-to"; } - virtual std::string defaultSource() const; + const char* getName() const override { return "dump-to"; } + std::string defaultSource() const override; protected: /** Initializes an output stream. Not necessarily managed. */ - virtual void initialize(std::ostream* outStream); + void initialize(std::ostream* outStream) override; /** Adds special cases to an ostreamopener. */ - virtual void addSpecialCases(OstreamOpener* opener) const; + void addSpecialCases(OstreamOpener* opener) const override; };/* class ManagedDumpOStream */ /** @@ -120,15 +121,15 @@ class ManagedRegularOutputChannel : public ManagedOstream { /** Assumes Options are in scope. */ ~ManagedRegularOutputChannel(); - virtual const char* getName() const { return "regular-output-channel"; } - virtual std::string defaultSource() const; + const char* getName() const override { return "regular-output-channel"; } + std::string defaultSource() const override; protected: /** Initializes an output stream. Not necessarily managed. */ - virtual void initialize(std::ostream* outStream); + void initialize(std::ostream* outStream) override; /** Adds special cases to an ostreamopener. */ - virtual void addSpecialCases(OstreamOpener* opener) const; + void addSpecialCases(OstreamOpener* opener) const override; };/* class ManagedRegularOutputChannel */ @@ -144,15 +145,15 @@ class ManagedDiagnosticOutputChannel : public ManagedOstream { /** Assumes Options are in scope. */ ~ManagedDiagnosticOutputChannel(); - virtual const char* getName() const { return "diagnostic-output-channel"; } - virtual std::string defaultSource() const; + const char* getName() const override { return "diagnostic-output-channel"; } + std::string defaultSource() const override; protected: /** Initializes an output stream. Not necessarily managed. */ - virtual void initialize(std::ostream* outStream); + void initialize(std::ostream* outStream) override; /** Adds special cases to an ostreamopener. */ - virtual void addSpecialCases(OstreamOpener* opener) const; + void addSpecialCases(OstreamOpener* opener) const override; };/* class ManagedRegularOutputChannel */ /** This controls the memory associated with replay-log. */ @@ -162,15 +163,15 @@ class ManagedReplayLogOstream : public ManagedOstream { ~ManagedReplayLogOstream(); std::ostream* getReplayLog() const { return d_replayLog; } - virtual const char* getName() const { return "replay-log"; } - virtual std::string defaultSource() const; + const char* getName() const override { return "replay-log"; } + std::string defaultSource() const override; protected: /** Initializes an output stream. Not necessarily managed. */ - virtual void initialize(std::ostream* outStream); + void initialize(std::ostream* outStream) override; /** Adds special cases to an ostreamopener. */ - virtual void addSpecialCases(OstreamOpener* opener) const; + void addSpecialCases(OstreamOpener* opener) const override; private: std::ostream* d_replayLog; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6e90ab152..74d6c1b10 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -298,7 +298,8 @@ struct SmtEngineStatistics { class SoftResourceOutListener : public Listener { public: SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { + void notify() override + { SmtScope scope(d_smt); Assert(smt::smtEngineInScope()); d_smt->interrupt(); @@ -311,7 +312,8 @@ class SoftResourceOutListener : public Listener { class HardResourceOutListener : public Listener { public: HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { + void notify() override + { SmtScope scope(d_smt); theory::Rewriter::clearCaches(); } @@ -322,7 +324,8 @@ class HardResourceOutListener : public Listener { class SetLogicListener : public Listener { public: SetLogicListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { + void notify() override + { LogicInfo inOptions(options::forceLogicString()); d_smt->setLogic(inOptions); } @@ -333,9 +336,8 @@ class SetLogicListener : public Listener { class BeforeSearchListener : public Listener { public: BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { - d_smt->beforeSearch(); - } + void notify() override { d_smt->beforeSearch(); } + private: SmtEngine* d_smt; }; /* class BeforeSearchListener */ @@ -346,7 +348,8 @@ class UseTheoryListListener : public Listener { : d_theoryEngine(theoryEngine) {} - void notify() { + void notify() override + { std::stringstream commaList(options::useTheoryList()); std::string token; @@ -375,7 +378,8 @@ class UseTheoryListListener : public Listener { class SetDefaultExprDepthListener : public Listener { public: - virtual void notify() { + void notify() override + { int depth = options::defaultExprDepth(); Debug.getStream() << expr::ExprSetDepth(depth); Trace.getStream() << expr::ExprSetDepth(depth); @@ -389,7 +393,8 @@ class SetDefaultExprDepthListener : public Listener { class SetDefaultExprDagListener : public Listener { public: - virtual void notify() { + void notify() override + { int dag = options::defaultDagThresh(); Debug.getStream() << expr::ExprDag(dag); Trace.getStream() << expr::ExprDag(dag); @@ -403,7 +408,8 @@ class SetDefaultExprDagListener : public Listener { class SetPrintExprTypesListener : public Listener { public: - virtual void notify() { + void notify() override + { bool value = options::printExprTypes(); Debug.getStream() << expr::ExprPrintTypes(value); Trace.getStream() << expr::ExprPrintTypes(value); @@ -417,7 +423,8 @@ class SetPrintExprTypesListener : public Listener { class DumpModeListener : public Listener { public: - virtual void notify() { + void notify() override + { const std::string& value = options::dumpModeString(); Dump.setDumpFromString(value); } @@ -425,7 +432,8 @@ class DumpModeListener : public Listener { class PrintSuccessListener : public Listener { public: - virtual void notify() { + void notify() override + { bool value = options::printSuccess(); Debug.getStream() << Command::printsuccess(value); Trace.getStream() << Command::printsuccess(value); @@ -748,7 +756,8 @@ public: d_resourceManager->spendResource(amount); } - void nmNotifyNewSort(TypeNode tn, uint32_t flags) { + void nmNotifyNewSort(TypeNode tn, uint32_t flags) override + { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType()); @@ -757,19 +766,22 @@ public: } } - void nmNotifyNewSortConstructor(TypeNode tn) { + void nmNotifyNewSortConstructor(TypeNode tn) override + { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), tn.getAttribute(expr::SortArityAttr()), tn.toType()); d_smt.addToModelCommandAndDump(c); } - void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) { + void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override + { DatatypeDeclarationCommand c(dtts); d_smt.addToModelCommandAndDump(c); } - void nmNotifyNewVar(TNode n, uint32_t flags) { + void nmNotifyNewVar(TNode n, uint32_t flags) override + { DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType()); @@ -781,11 +793,12 @@ public: } } - void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { + void nmNotifyNewSkolem(TNode n, + const std::string& comment, + uint32_t flags) override + { string id = n.getAttribute(expr::VarNameAttr()); - DeclareFunctionCommand c(id, - n.toExpr(), - n.getType().toType()); + DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType()); if(Dump.isOn("skolems") && comment != "") { Dump("skolems") << CommentCommand(id + " is " + comment); } @@ -797,7 +810,7 @@ public: } } - void nmNotifyDeleteNode(TNode n) {} + void nmNotifyDeleteNode(TNode n) override {} Node applySubstitutions(TNode node) const { return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index ce4504279..a161985de 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -73,50 +73,50 @@ public: class OptionsErrOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return *(options::err()); } - virtual void set(std::ostream* setTo) { return options::err.set(setTo); } + std::ostream& get() override { return *(options::err()); } + void set(std::ostream* setTo) override { return options::err.set(setTo); } }; /* class OptionsErrOstreamUpdate */ class DumpOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return Dump.getStream(); } - virtual void set(std::ostream* setTo) { Dump.setStream(setTo); } + std::ostream& get() override { return Dump.getStream(); } + void set(std::ostream* setTo) override { Dump.setStream(setTo); } }; /* class DumpOstreamUpdate */ class DebugOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return Debug.getStream(); } - virtual void set(std::ostream* setTo) { Debug.setStream(setTo); } + std::ostream& get() override { return Debug.getStream(); } + void set(std::ostream* setTo) override { Debug.setStream(setTo); } }; /* class DebugOstreamUpdate */ class WarningOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return Warning.getStream(); } - virtual void set(std::ostream* setTo) { Warning.setStream(setTo); } + std::ostream& get() override { return Warning.getStream(); } + void set(std::ostream* setTo) override { Warning.setStream(setTo); } }; /* class WarningOstreamUpdate */ class MessageOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return Message.getStream(); } - virtual void set(std::ostream* setTo) { Message.setStream(setTo); } + std::ostream& get() override { return Message.getStream(); } + void set(std::ostream* setTo) override { Message.setStream(setTo); } }; /* class MessageOstreamUpdate */ class NoticeOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return Notice.getStream(); } - virtual void set(std::ostream* setTo) { Notice.setStream(setTo); } + std::ostream& get() override { return Notice.getStream(); } + void set(std::ostream* setTo) override { Notice.setStream(setTo); } }; /* class NoticeOstreamUpdate */ class ChatOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return Chat.getStream(); } - virtual void set(std::ostream* setTo) { Chat.setStream(setTo); } + std::ostream& get() override { return Chat.getStream(); } + void set(std::ostream* setTo) override { Chat.setStream(setTo); } }; /* class ChatOstreamUpdate */ class TraceOstreamUpdate : public OstreamUpdate { public: - virtual std::ostream& get() { return Trace.getStream(); } - virtual void set(std::ostream* setTo) { Trace.setStream(setTo); } + std::ostream& get() override { return Trace.getStream(); } + void set(std::ostream* setTo) override { Trace.setStream(setTo); } }; /* class TraceOstreamUpdate */ }/* CVC4 namespace */ diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 73798f94c..fa65214e7 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -67,11 +67,9 @@ public: Result::Sat attempt(const ApproximateSimplex::Solution& sol); - Result::Sat findModel(bool exactResult){ - Unreachable(); - } + Result::Sat findModel(bool exactResult) override { Unreachable(); } -private: + private: bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const; bool processSignals(){ diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 3710ac5c0..f84550dcc 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -73,7 +73,7 @@ private: TheoryArithPrivate& d_arith; public: SetupLiteralCallBack(TheoryArithPrivate& ta); - void operator()(TNode lit); + void operator()(TNode lit) override; }; class DeltaComputeCallback : public RationalCallBack { @@ -81,7 +81,7 @@ private: const TheoryArithPrivate& d_ta; public: DeltaComputeCallback(const TheoryArithPrivate& ta); - Rational operator()() const; + Rational operator()() const override; }; class BasicVarModelUpdateCallBack : public ArithVarCallBack{ @@ -89,7 +89,7 @@ private: TheoryArithPrivate& d_ta; public: BasicVarModelUpdateCallBack(TheoryArithPrivate& ta); - void operator()(ArithVar x); + void operator()(ArithVar x) override; }; class TempVarMalloc : public ArithVarMalloc { @@ -97,8 +97,8 @@ private: TheoryArithPrivate& d_ta; public: TempVarMalloc(TheoryArithPrivate& ta); - ArithVar request(); - void release(ArithVar v); + ArithVar request() override; + void release(ArithVar v) override; }; class RaiseConflict { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 228f29838..5085dc841 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -61,17 +61,20 @@ private: public: ArithCongruenceNotify(ArithCongruenceManager& acm); - bool eqNotifyTriggerEquality(TNode equality, bool value); + bool eqNotifyTriggerEquality(TNode equality, bool value) override; - bool eqNotifyTriggerPredicate(TNode predicate, bool value); + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override; - void eqNotifyConstantTermMerge(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2); - void eqNotifyPostMerge(TNode t1, TNode t2); - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + void eqNotifyNewClass(TNode t) override; + void eqNotifyPreMerge(TNode t1, TNode t2) override; + void eqNotifyPostMerge(TNode t1, TNode t2) override; + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; }; ArithCongruenceNotify d_notify; diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 2911592c7..10d18170e 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -63,7 +63,8 @@ class DualSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult) { + Result::Sat findModel(bool exactResult) override + { return dualFindModel(exactResult); } diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index c4f996f9f..a93fa88e8 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -66,7 +66,7 @@ class FCSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult); + Result::Sat findModel(bool exactResult) override; // other error variables are dropping WitnessImprovement dualLikeImproveError(ArithVar evar); diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index c2fa99e31..0f2862a72 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -588,13 +588,16 @@ private: LinearEqualityModule* d_linEq; public: TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {} - void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){ + void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override + { d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn); } - void multiplyRow(RowIndex ridx, int sgn){ + void multiplyRow(RowIndex ridx, int sgn) override + { d_linEq->trackingMultiplyRow(ridx, sgn); } - bool canUseRow(RowIndex ridx) const { + bool canUseRow(RowIndex ridx) const override + { ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx); return d_linEq->basicIsTracked(basic); } @@ -746,7 +749,8 @@ private: LinearEqualityModule* d_mod; public: UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){} - void operator()(ArithVar v, const BoundsInfo& bi){ + void operator()(ArithVar v, const BoundsInfo& bi) override + { d_mod->includeBoundUpdate(v, bi); } }; diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 2e0a1ebb2..eda5b9dac 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -48,9 +48,9 @@ public: class NoEffectCCCB : public CoefficientChangeCallback { public: - void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn); - void multiplyRow(RowIndex ridx, int Sgn); - bool canUseRow(RowIndex ridx) const; + void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override; + void multiplyRow(RowIndex ridx, int Sgn) override; + bool canUseRow(RowIndex ridx) const override; }; template<class T> diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 5f2233b3f..54a47ac4d 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -66,7 +66,7 @@ class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure { public: SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult); + Result::Sat findModel(bool exactResult) override; // other error variables are dropping WitnessImprovement dualLikeImproveError(ArithVar evar); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index caf466c0c..70cb574a8 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -277,7 +277,8 @@ class TheoryArrays : public Theory { public: NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl; // Just forward to arrays if (value) { @@ -287,7 +288,8 @@ class TheoryArrays : public Theory { } } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; // Just forward to arrays if (value) { @@ -297,7 +299,11 @@ class TheoryArrays : public Theory { } } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { if (t1.getType().isArray()) { @@ -318,19 +324,21 @@ class TheoryArrays : public Theory { return true; } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_arrays.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) { } - void eqNotifyPreMerge(TNode t1, TNode t2) { } - void eqNotifyPostMerge(TNode t1, TNode t2) { + void eqNotifyNewClass(TNode t) override {} + void eqNotifyPreMerge(TNode t1, TNode t2) override {} + void eqNotifyPostMerge(TNode t1, TNode t2) override + { if (t1.getType().isArray()) { d_arrays.mergeArrays(t1, t2); } } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} }; /** The notify class for d_equalityEngine */ @@ -386,10 +394,12 @@ class TheoryArrays : public Theory { context::Context* d_satContext; context::Context* d_contextToPop; protected: - void contextNotifyPop() { - if (d_contextToPop->getLevel() > d_satContext->getLevel()) { - d_contextToPop->pop(); - } + void contextNotifyPop() override + { + if (d_contextToPop->getLevel() > d_satContext->getLevel()) + { + d_contextToPop->pop(); + } } public: ContextPopper(context::Context* context, context::Context* contextToPop) diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 78e01f690..7c60505a5 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -79,10 +79,11 @@ private: class DataClearer : context::ContextNotifyObj { T& d_data; protected: - void contextNotifyPop() { - Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data " - << "(size was " << d_data.size() << ")" << std::endl; - d_data.clear(); + void contextNotifyPop() override + { + Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data " + << "(size was " << d_data.size() << ")" << std::endl; + d_data.clear(); } public: DataClearer(context::Context* context, T& data) : diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 9d5966628..cd9a9f904 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -33,11 +33,11 @@ public: : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {} - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; //void check(Effort); - - std::string identify() const { return std::string("TheoryBool"); } + + std::string identify() const override { return std::string("TheoryBool"); } };/* class TheoryBool */ }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index cfc59272c..14a38660b 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -31,7 +31,7 @@ public: OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {} - std::string identify() const { return std::string("TheoryBuiltin"); } + std::string identify() const override { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ }/* CVC4::theory::builtin namespace */ diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 1dc2d8b1e..3bb701fdf 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -169,15 +169,15 @@ class TLazyBitblaster : public TBitblaster<Node> { void addAtom(TNode atom); bool hasValue(TNode a); - Node getModelFromSatSolver(TNode a, bool fullModel); + Node getModelFromSatSolver(TNode a, bool fullModel) override; -public: - void bbTerm(TNode node, Bits& bits); - void bbAtom(TNode node); - Node getBBAtom(TNode atom) const; - void storeBBAtom(TNode atom, Node atom_bb); - void storeBBTerm(TNode node, const Bits& bits); - bool hasBBAtom(TNode atom) const; + public: + void bbTerm(TNode node, Bits& bits) override; + void bbAtom(TNode node) override; + Node getBBAtom(TNode atom) const override; + void storeBBAtom(TNode atom, Node atom_bb) override; + void storeBBTerm(TNode node, const Bits& bits) override; + bool hasBBAtom(TNode atom) const override; TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); ~TLazyBitblaster(); @@ -219,7 +219,7 @@ public: * * @param var */ - void makeVariable(TNode var, Bits& bits); + void makeVariable(TNode var, Bits& bits) override; bool isSharedTerm(TNode node); uint64_t computeAtomWeight(TNode node, NodeSet& seen); @@ -274,7 +274,7 @@ class EagerBitblaster : public TBitblaster<Node> { // This is either an MinisatEmptyNotify or NULL. MinisatEmptyNotify* d_notify; - Node getModelFromSatSolver(TNode a, bool fullModel); + Node getModelFromSatSolver(TNode a, bool fullModel) override; bool isSharedTerm(TNode node); public: @@ -282,14 +282,14 @@ public: ~EagerBitblaster(); void addAtom(TNode atom); - void makeVariable(TNode node, Bits& bits); - void bbTerm(TNode node, Bits& bits); - void bbAtom(TNode node); - Node getBBAtom(TNode node) const; - bool hasBBAtom(TNode atom) const; + void makeVariable(TNode node, Bits& bits) override; + void bbTerm(TNode node, Bits& bits) override; + void bbAtom(TNode node) override; + Node getBBAtom(TNode node) const override; + bool hasBBAtom(TNode atom) const override; void bbFormula(TNode formula); - void storeBBAtom(TNode atom, Node atom_bb); - void storeBBTerm(TNode node, const Bits& bits); + void storeBBAtom(TNode atom, Node atom_bb) override; + void storeBBTerm(TNode node, const Bits& bits) override; bool assertToSat(TNode node, bool propagate = true); bool solve(); @@ -303,7 +303,7 @@ public: BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {} - void preRegister(Node n); + void preRegister(Node n) override; }; /* class Registrar */ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { @@ -322,9 +322,9 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { void addAtom(TNode atom); void simplifyAig(); - void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb); - Abc_Obj_t* getBBAtom(TNode atom) const; - bool hasBBAtom(TNode atom) const; + void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override; + Abc_Obj_t* getBBAtom(TNode atom) const override; + bool hasBBAtom(TNode atom) const override; void cacheAig(TNode node, Abc_Obj_t* aig); bool hasAig(TNode node); Abc_Obj_t* getAig(TNode node); @@ -332,14 +332,18 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { bool hasInput(TNode input); void convertToCnfAndAssert(); void assertToSatSolver(Cnf_Dat_t* pCnf); - Node getModelFromSatSolver(TNode a, bool fullModel) { Unreachable(); } -public: + Node getModelFromSatSolver(TNode a, bool fullModel) override + { + Unreachable(); + } + + public: AigBitblaster(); ~AigBitblaster(); - void makeVariable(TNode node, Bits& bits); - void bbTerm(TNode node, Bits& bits); - void bbAtom(TNode node); + void makeVariable(TNode node, Bits& bits) override; + void bbTerm(TNode node, Bits& bits) override; + void bbAtom(TNode node) override; Abc_Obj_t* bbFormula(TNode formula); bool solve(TNode query); static Abc_Aig_t* currentAigM(); diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 30270b3c3..deba84631 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -201,11 +201,9 @@ class InequalityGraph : public context::ContextNotifyObj{ Node makeDiseqSplitLemma(TNode diseq); /** Backtracking mechanisms **/ std::vector<std::pair<TermId, InequalityEdge> > d_undoStack; - context::CDO<unsigned> d_undoStackIndex; - - void contextNotifyPop() { - backtrack(); - } + context::CDO<unsigned> d_undoStackIndex; + + void contextNotifyPop() override { backtrack(); } void backtrack(); diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 0534c0f17..c963f15d7 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -224,16 +224,19 @@ public: AlgebraicSolver(context::Context* c, TheoryBV* bv); ~AlgebraicSolver(); - void preRegister(TNode node) {} - bool check(Theory::Effort e); - void explain(TNode literal, std::vector<TNode>& assumptions) {Unreachable("AlgebraicSolver does not propagate.\n");} - EqualityStatus getEqualityStatus(TNode a, TNode b); - bool collectModelInfo(TheoryModel* m, bool fullModel); - Node getModelValue(TNode node); - bool isComplete(); - virtual void assertFact(TNode fact); + void preRegister(TNode node) override {} + bool check(Theory::Effort e) override; + void explain(TNode literal, std::vector<TNode>& assumptions) override + { + Unreachable("AlgebraicSolver does not propagate.\n"); + } + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + bool collectModelInfo(TheoryModel* m, bool fullModel) override; + Node getModelValue(TNode node) override; + bool isComplete() override; + void assertFact(TNode fact) override; }; -} -} -} +} // namespace bv +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 5927feddc..f88810fca 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -65,17 +65,17 @@ public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); - void preRegister(TNode node); - bool check(Theory::Effort e); - void explain(TNode literal, std::vector<TNode>& assumptions); - EqualityStatus getEqualityStatus(TNode a, TNode b); - bool collectModelInfo(TheoryModel* m, bool fullModel); - Node getModelValue(TNode node); - bool isComplete() { return true; } + void preRegister(TNode node) override; + bool check(Theory::Effort e) override; + void explain(TNode literal, std::vector<TNode>& assumptions) override; + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + bool collectModelInfo(TheoryModel* m, bool fullModel) override; + Node getModelValue(TNode node) override; + bool isComplete() override { return true; } void bitblastQueue(); void setAbstraction(AbstractionModule* module); uint64_t computeAtomWeight(TNode atom); - void setProofLog( BitVectorProof * bvp ); + void setProofLog(BitVectorProof* bvp) override; }; } /* namespace CVC4::theory::bv */ diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 6cc6253ff..05c9535c3 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -53,14 +53,17 @@ class CoreSolver : public SubtheorySolver { public: NotifyClass(CoreSolver& solver): d_solver(solver) {} - bool eqNotifyTriggerEquality(TNode equality, bool value); - bool eqNotifyTriggerPredicate(TNode predicate, bool value); - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); - void eqNotifyConstantTermMerge(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2) { } - void eqNotifyPostMerge(TNode t1, TNode t2) { } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + bool eqNotifyTriggerEquality(TNode equality, bool value) override; + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override; + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + void eqNotifyNewClass(TNode t) override; + void eqNotifyPreMerge(TNode t1, TNode t2) override {} + void eqNotifyPostMerge(TNode t1, TNode t2) override {} + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} }; @@ -100,17 +103,19 @@ class CoreSolver : public SubtheorySolver { public: CoreSolver(context::Context* c, TheoryBV* bv); ~CoreSolver(); - bool isComplete() { return d_isComplete; } + bool isComplete() override { return d_isComplete; } void setMasterEqualityEngine(eq::EqualityEngine* eq); - void preRegister(TNode node); - bool check(Theory::Effort e); - void explain(TNode literal, std::vector<TNode>& assumptions); - bool collectModelInfo(TheoryModel* m, bool fullModel); - Node getModelValue(TNode var); - void addSharedTerm(TNode t) { + void preRegister(TNode node) override; + bool check(Theory::Effort e) override; + void explain(TNode literal, std::vector<TNode>& assumptions) override; + bool collectModelInfo(TheoryModel* m, bool fullModel) override; + Node getModelValue(TNode var) override; + void addSharedTerm(TNode t) override + { d_equalityEngine.addTriggerTerm(t, THEORY_BV); } - EqualityStatus getEqualityStatus(TNode a, TNode b) { + EqualityStatus getEqualityStatus(TNode a, TNode b) override + { if (d_equalityEngine.areEqual(a, b)) { // The terms are implied to be equal return EQUALITY_TRUE; diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index be0492125..620cd075b 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -65,15 +65,15 @@ public: d_statistics() {} - bool check(Theory::Effort e); - void propagate(Theory::Effort e); - void explain(TNode literal, std::vector<TNode>& assumptions); - bool isComplete() { return d_isComplete; } - bool collectModelInfo(TheoryModel* m, bool fullModel); - Node getModelValue(TNode var); - EqualityStatus getEqualityStatus(TNode a, TNode b); - void assertFact(TNode fact); - void preRegister(TNode node); + bool check(Theory::Effort e) override; + void propagate(Theory::Effort e) override; + void explain(TNode literal, std::vector<TNode>& assumptions) override; + bool isComplete() override { return d_isComplete; } + bool collectModelInfo(TheoryModel* m, bool fullModel) override; + Node getModelValue(TNode var) override; + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + void assertFact(TNode fact) override; + void preRegister(TNode node) override; }; } diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index 718121499..dd65fc08f 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -42,20 +42,21 @@ public: d_bits(0) { } - Node operator*() { + Node operator*() override + { if(d_bits != d_bits.modByPow2(d_size)) { throw NoMoreValuesException(getType()); } return utils::mkConst(d_size, d_bits); } - BitVectorEnumerator& operator++() + BitVectorEnumerator& operator++() override { d_bits += 1; return *this; } - bool isFinished() { return d_bits != d_bits.modByPow2(d_size); } + bool isFinished() override { return d_bits != d_bits.modByPow2(d_size); } };/* BitVectorEnumerator */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 8052df59a..a27fd5543 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -64,7 +64,8 @@ class TheoryDatatypes : public Theory { TheoryDatatypes& d_dt; public: NotifyClass(TheoryDatatypes& dt): d_dt(dt) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { Debug("dt") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; if (value) { return d_dt.propagate(equality); @@ -73,7 +74,8 @@ class TheoryDatatypes : public Theory { return d_dt.propagate(equality.notNode()); } } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { return d_dt.propagate(predicate); @@ -81,7 +83,11 @@ class TheoryDatatypes : public Theory { return d_dt.propagate(predicate.notNode()); } } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_dt.propagate(t1.eqNode(t2)); @@ -89,23 +95,28 @@ class TheoryDatatypes : public Theory { return d_dt.propagate(t1.eqNode(t2).notNode()); } } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { Debug("dt") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_dt.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) { + void eqNotifyNewClass(TNode t) override + { Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; d_dt.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) { + void eqNotifyPreMerge(TNode t1, TNode t2) override + { Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl; d_dt.eqNotifyPreMerge(t1, t2); } - void eqNotifyPostMerge(TNode t1, TNode t2) { + void eqNotifyPostMerge(TNode t1, TNode t2) override + { Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl; d_dt.eqNotifyPostMerge(t1, t2); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override + { Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl; d_dt.eqNotifyDisequal(t1, t2, reason); } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ca80546b8..688c6e600 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -62,15 +62,17 @@ class TheoryFp : public Theory { public: NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {} - bool eqNotifyTriggerEquality(TNode equality, bool value); - bool eqNotifyTriggerPredicate(TNode predicate, bool value); - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, - bool value); - void eqNotifyConstantTermMerge(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t) {} - void eqNotifyPreMerge(TNode t1, TNode t2) {} - void eqNotifyPostMerge(TNode t1, TNode t2) {} - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) override; + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override; + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + void eqNotifyNewClass(TNode t) override {} + void eqNotifyPreMerge(TNode t1, TNode t2) override {} + void eqNotifyPostMerge(TNode t1, TNode t2) override {} + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} }; friend NotifyClass; diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h index 625770869..7b05fc890 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -48,13 +48,13 @@ public: Valuation valuation, const LogicInfo& logicInfo); /** Pre-processing of input atoms */ - Node ppRewrite(TNode atom); + Node ppRewrite(TNode atom) override; /** Check the assertions for satisfiability */ - void check(Effort effort); + void check(Effort effort) override; /** Identity string */ - std::string identify() const { return "THEORY_IDL"; } + std::string identify() const override { return "THEORY_IDL"; } };/* class TheoryIdl */ diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index bf8b99f1c..6967c6c42 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -40,12 +40,12 @@ public: bool pconnected = true ); /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e); + void check(Theory::Effort e, QEffort quant_e) override; /* Called for new quantifiers */ - void registerQuantifier( Node q ) {} - void assertNode( Node n ) {} + void registerQuantifier(Node q) override {} + void assertNode(Node n) override {} /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "QuantAntiSkolem"; } + std::string identify() const override { return "QuantAntiSkolem"; } private: typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 03983fe1a..c12890b83 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -748,11 +748,11 @@ public: bool useModelValue(CegInstantiator* ci, SolvedForm& sf, Node pv, - CegInstEffort effort) + CegInstEffort effort) override { return true; } - std::string identify() const { return "ModelValue"; } + std::string identify() const override { return "ModelValue"; } }; /** instantiator preprocess diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp index e6e64201e..bb210edcc 100644 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp @@ -934,11 +934,13 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery } ~CegInstantiatorBvInverterQuery() {} /** return the model value of n */ - Node getModelValue( Node n ) { - return d_ci->getModelValue( n ); - } + Node getModelValue(Node n) override { return d_ci->getModelValue(n); } /** get bound variable of type tn */ - Node getBoundVariable(TypeNode tn) { return d_ci->getBoundVariable(tn); } + Node getBoundVariable(TypeNode tn) override + { + return d_ci->getBoundVariable(tn); + } + protected: // pointer to class that is able to query model values CegInstantiator * d_ci; diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h index b9c7e2024..eee6747ec 100644 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h @@ -33,57 +33,56 @@ class ArithInstantiator : public Instantiator { public: ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~ArithInstantiator(){} - virtual void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - virtual bool hasProcessEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override { return true; } - virtual bool processEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector<TermProperties>& term_props, - std::vector<Node>& terms, - CegInstEffort effort) override; - virtual bool hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override + bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + CegInstEffort effort) override; + bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override { return true; } - virtual Node hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - CegInstEffort effort) override; - virtual bool processAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - Node lit, - Node alit, - CegInstEffort effort) override; - virtual bool processAssertions(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - virtual bool needsPostProcessInstantiationForVariable( - CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - virtual bool postProcessInstantiationForVariable( - CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort, - std::vector<Node>& lemmas) override; - virtual std::string identify() const override { return "Arith"; } + Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) override; + bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) override; + bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + bool needsPostProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + bool postProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort, + std::vector<Node>& lemmas) override; + std::string identify() const override { return "Arith"; } + private: Node d_vts_sym[2]; std::vector<Node> d_mbp_bounds[2]; @@ -113,29 +112,30 @@ class DtInstantiator : public Instantiator { public: DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~DtInstantiator(){} - virtual void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - virtual bool processEqualTerms(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector<Node>& eqc, - CegInstEffort effort) override; - virtual bool hasProcessEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + CegInstEffort effort) override; + bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override { return true; } - virtual bool processEquality(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector<TermProperties>& term_props, - std::vector<Node>& terms, - CegInstEffort effort) override; - virtual std::string identify() const override { return "Dt"; } + bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + CegInstEffort effort) override; + std::string identify() const override { return "Dt"; } + private: Node solve_dt(Node v, Node a, Node b, Node sa, Node sb); }; @@ -146,22 +146,23 @@ class EprInstantiator : public Instantiator { public: EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} virtual ~EprInstantiator(){} - virtual void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - virtual bool processEqualTerm(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - TermProperties& pv_prop, - Node n, - CegInstEffort effort) override; - virtual bool processEqualTerms(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - std::vector<Node>& eqc, - CegInstEffort effort) override; - virtual std::string identify() const override { return "Epr"; } + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + bool processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + CegInstEffort effort) override; + bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + CegInstEffort effort) override; + std::string identify() const override { return "Epr"; } + private: std::vector<Node> d_equal_terms; void computeMatchScore(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 3443d2c4d..2bc86ef4e 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -103,16 +103,16 @@ class InstStrategyCbqi : public QuantifiersModule { /** whether to do CBQI for quantifier q */ bool doCbqi( Node q ); /** process functions */ - bool needsCheck( Theory::Effort e ); - QEffort needsModel(Theory::Effort e); - void reset_round( Theory::Effort e ); - void check(Theory::Effort e, QEffort quant_e); - bool checkComplete(); - bool checkCompleteFor( Node q ); - void preRegisterQuantifier( Node q ); - void registerQuantifier( Node q ); + bool needsCheck(Theory::Effort e) override; + QEffort needsModel(Theory::Effort e) override; + void reset_round(Theory::Effort e) override; + void check(Theory::Effort e, QEffort quant_e) override; + bool checkComplete() override; + bool checkCompleteFor(Node q) override; + void preRegisterQuantifier(Node q) override; + void registerQuantifier(Node q) override; /** get next decision request */ - Node getNextDecisionRequest( unsigned& priority ); + Node getNextDecisionRequest(unsigned& priority) override; }; //generalized counterexample guided quantifier instantiation @@ -123,9 +123,9 @@ class CegqiOutputInstStrategy : public CegqiOutput { public: CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} InstStrategyCegqi * d_out; - bool doAddInstantiation( std::vector< Node >& subs ); - bool isEligibleForInstantiation( Node n ); - bool addLemma( Node lem ); + bool doAddInstantiation(std::vector<Node>& subs) override; + bool isEligibleForInstantiation(Node n) override; + bool addLemma(Node lem) override; }; class InstStrategyCegqi : public InstStrategyCbqi { diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 85a7d3eb4..764379e76 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -237,14 +237,35 @@ private: ConjectureGenerator& d_sg; public: NotifyClass(ConjectureGenerator& sg): d_sg(sg) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { } - void eqNotifyNewClass(TNode t) { d_sg.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) { d_sg.eqNotifyPreMerge(t1, t2); } - void eqNotifyPostMerge(TNode t1, TNode t2) { d_sg.eqNotifyPostMerge(t1, t2); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_sg.eqNotifyDisequal(t1, t2, reason); } + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { + return true; + } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { + return true; + } + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { + return true; + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {} + void eqNotifyNewClass(TNode t) override { d_sg.eqNotifyNewClass(t); } + void eqNotifyPreMerge(TNode t1, TNode t2) override + { + d_sg.eqNotifyPreMerge(t1, t2); + } + void eqNotifyPostMerge(TNode t1, TNode t2) override + { + d_sg.eqNotifyPostMerge(t1, t2); + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override + { + d_sg.eqNotifyDisequal(t1, t2, reason); + } };/* class ConjectureGenerator::NotifyClass */ /** The notify class */ NotifyClass d_notify; @@ -401,18 +422,18 @@ public: ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ); /* needs check */ - bool needsCheck( Theory::Effort e ); + bool needsCheck(Theory::Effort e) override; /* reset at a round */ - void reset_round( Theory::Effort e ); + void reset_round(Theory::Effort e) override; /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e); + void check(Theory::Effort e, QEffort quant_e) override; /* Called for new quantifiers */ - void registerQuantifier( Node q ); - void assertNode( Node n ); + void registerQuantifier(Node q) override; + void assertNode(Node n) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "ConjectureGenerator"; } -//options -private: + std::string identify() const override { return "ConjectureGenerator"; } + // options + private: bool optReqDistinctVarPatterns(); bool optFilterUnknown(); int optFilterScoreThreshold(); diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 41fec5e5f..85bb09086 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger * Extends Trigger::addInstantiations to also send * lemmas based on addHoTypeMatchPredicateLemmas. */ - virtual int addInstantiations() override; + int addInstantiations() override; protected: /** diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 8f11dfedf..eba49fa9a 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -40,9 +40,10 @@ private: /** counter for quantifiers */ std::map< Node, int > d_counter; /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); -public: + void processResetInstantiationRound(Theory::Effort effort) override; + int process(Node f, Theory::Effort effort, int e) override; + + public: InstStrategyUserPatterns( QuantifiersEngine* ie ) : InstStrategy( ie ){} ~InstStrategyUserPatterns(){} @@ -54,7 +55,7 @@ public: /** get user pattern */ inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; } /** identify */ - std::string identify() const { return std::string("UserPatterns"); } + std::string identify() const override { return std::string("UserPatterns"); } };/* class InstStrategyUserPatterns */ class InstStrategyAutoGenTriggers : public InstStrategy { @@ -89,16 +90,16 @@ private: std::map< Node, Node > d_pat_to_mpat; private: /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - int process( Node q, Theory::Effort effort, int e ); - /** generate triggers */ - void generateTriggers( Node q ); - void addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ); - void addTrigger( inst::Trigger * tr, Node f ); - /** has user patterns */ - bool hasUserPatterns( Node q ); - /** has user patterns */ - std::map< Node, bool > d_hasUserPatterns; + void processResetInstantiationRound(Theory::Effort effort) override; + int process(Node q, Theory::Effort effort, int e) override; + /** generate triggers */ + void generateTriggers(Node q); + void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat); + void addTrigger(inst::Trigger* tr, Node f); + /** has user patterns */ + bool hasUserPatterns(Node q); + /** has user patterns */ + std::map<Node, bool> d_hasUserPatterns; public: InstStrategyAutoGenTriggers( QuantifiersEngine* qe ); ~InstStrategyAutoGenTriggers(){} @@ -106,7 +107,10 @@ public: /** get auto-generated trigger */ inst::Trigger* getAutoGenTrigger( Node q ); /** identify */ - std::string identify() const { return std::string("AutoGenTriggers"); } + std::string identify() const override + { + return std::string("AutoGenTriggers"); + } /** add pattern */ void addUserNoPattern( Node q, Node pat ); };/* class InstStrategyAutoGenTriggers */ diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 18b5ea19c..32ddb19ed 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -76,19 +76,19 @@ class InstantiationEngine : public QuantifiersModule { public: InstantiationEngine(QuantifiersEngine* qe); ~InstantiationEngine(); - void presolve(); - bool needsCheck(Theory::Effort e); - void reset_round(Theory::Effort e); - void check(Theory::Effort e, QEffort quant_e); - bool checkCompleteFor(Node q); - void preRegisterQuantifier(Node q); - void registerQuantifier(Node q); + void presolve() override; + bool needsCheck(Theory::Effort e) override; + void reset_round(Theory::Effort e) override; + void check(Theory::Effort e, QEffort quant_e) override; + bool checkCompleteFor(Node q) override; + void preRegisterQuantifier(Node q) override; + void registerQuantifier(Node q) override; Node explain(TNode n) { return Node::null(); } /** add user pattern */ void addUserPattern(Node q, Node pat); void addUserNoPattern(Node q, Node pat); /** Identify this module */ - std::string identify() const { return "InstEngine"; } + std::string identify() const override { return "InstEngine"; } }; /* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 0048cc14f..0b28f53c6 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -50,26 +50,26 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe); virtual ~EqualityQueryQuantifiersEngine(); /** reset */ - virtual bool reset(Theory::Effort e); + bool reset(Theory::Effort e) override; /* Called for new quantifiers */ - virtual void registerQuantifier(Node q) {} + void registerQuantifier(Node q) override {} /** identify */ - virtual std::string identify() const { return "EqualityQueryQE"; } + std::string identify() const override { return "EqualityQueryQE"; } /** does the equality engine have term a */ - bool hasTerm(Node a); + bool hasTerm(Node a) override; /** get the representative of a */ - Node getRepresentative(Node a); + Node getRepresentative(Node a) override; /** are a and b equal? */ - bool areEqual(Node a, Node b); + bool areEqual(Node a, Node b) override; /** are a and b disequal? */ - bool areDisequal(Node a, Node b); + bool areDisequal(Node a, Node b) override; /** get equality engine * This may either be the master equality engine or the model's equality * engine. */ - eq::EqualityEngine* getEngine(); + eq::EqualityEngine* getEngine() override; /** get list of members in the equivalence class of a */ - void getEquivalenceClass(Node a, std::vector<Node>& eqc); + void getEquivalenceClass(Node a, std::vector<Node>& eqc) override; /** get congruent term * If possible, returns a term n such that: * (1) n is a term in the equality engine from getEngine(). @@ -80,7 +80,7 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery * Notice that f should be a "match operator", returned by * TermDb::getMatchOperator. */ - TNode getCongruentTerm(Node f, std::vector<TNode>& args); + TNode getCongruentTerm(Node f, std::vector<TNode>& args) override; /** gets the current best representative in the equivalence * class of a, based on some heuristic. Currently, the default heuristic * chooses terms that were previously chosen as representatives diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index f33151b4d..db2f97b16 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -67,19 +67,19 @@ class QRepBoundExt : public RepBoundExt QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {} virtual ~QRepBoundExt() {} /** set bound */ - virtual RepSetIterator::RsiEnumType setBound( - Node owner, unsigned i, std::vector<Node>& elements) override; + RepSetIterator::RsiEnumType setBound(Node owner, + unsigned i, + std::vector<Node>& elements) override; /** reset index */ - virtual bool resetIndex(RepSetIterator* rsi, - Node owner, - unsigned i, - bool initial, - std::vector<Node>& elements) override; + bool resetIndex(RepSetIterator* rsi, + Node owner, + unsigned i, + bool initial, + std::vector<Node>& elements) override; /** initialize representative set for type */ - virtual bool initializeRepresentativesForType(TypeNode tn) override; + bool initializeRepresentativesForType(TypeNode tn) override; /** get variable order */ - virtual bool getVariableOrder(Node owner, - std::vector<unsigned>& varOrder) override; + bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override; private: /** quantifiers engine associated with this bound */ @@ -215,11 +215,11 @@ private: public: FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); - FirstOrderModelIG * asFirstOrderModelIG() { return this; } + FirstOrderModelIG* asFirstOrderModelIG() override { return this; } // initialize the model - void processInitialize( bool ispre ); + void processInitialize(bool ispre) override; //for initialize model - void processInitializeModelForTerm( Node n ); + void processInitializeModelForTerm(Node n) override; /** reset evaluation */ void resetEvaluate(); /** evaluate functions */ diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 99d77a8e7..3e990067a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -102,10 +102,10 @@ private: context::CDO< bool > d_has_range; context::CDO< int > d_curr_range; IntBoolMap d_ranges_proxied; - void initialize(); - void assertNode(Node n); - Node getNextDecisionRequest(); - bool proxyCurrentRange(); + void initialize() override; + void assertNode(Node n) override; + Node getNextDecisionRequest() override; + bool proxyCurrentRange() override; }; private: //information for minimizing ranges @@ -142,14 +142,14 @@ private: public: BoundedIntegers( context::Context* c, QuantifiersEngine* qe ); virtual ~BoundedIntegers(); - - void presolve(); - bool needsCheck( Theory::Effort e ); - void check(Theory::Effort e, QEffort quant_e); - void registerQuantifier( Node q ); - void preRegisterQuantifier( Node q ); - void assertNode( Node n ); - Node getNextDecisionRequest( unsigned& priority ); + + void presolve() override; + bool needsCheck(Theory::Effort e) override; + void check(Theory::Effort e, QEffort quant_e) override; + void registerQuantifier(Node q) override; + void preRegisterQuantifier(Node q) override; + void assertNode(Node n) override; + Node getNextDecisionRequest(unsigned& priority) override; bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); } unsigned getBoundVarType( Node q, Node v ); unsigned getNumBoundVars( Node q ) { return d_set[q].size(); } @@ -171,7 +171,7 @@ public: bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ); /** Identify this module */ - std::string identify() const { return "BoundedIntegers"; } + std::string identify() const override { return "BoundedIntegers"; } }; } diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 732f8be07..a64c33303 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -138,13 +138,15 @@ public: void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); - int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + int doExhaustiveInstantiation(FirstOrderModel* fm, + Node f, + int effort) override; Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); - /** process build model */ - bool preProcessBuildModel(TheoryModel* m); - bool processBuildModel(TheoryModel* m); + /** process build model */ + bool preProcessBuildModel(TheoryModel* m) override; + bool processBuildModel(TheoryModel* m) override; bool useSimpleModels(); };/* class FullModelChecker */ diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 4eb592b3e..5af1e3451 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -31,7 +31,8 @@ class QModelBuilder : public TheoryEngineModelBuilder protected: //quantifiers engine QuantifiersEngine* d_qe; - bool preProcessBuildModel(TheoryModel* m); //must call preProcessBuildModelStd + // must call preProcessBuildModelStd + bool preProcessBuildModel(TheoryModel* m) override; bool preProcessBuildModelStd(TheoryModel* m); /** number of lemmas generated while building model */ unsigned d_addedLemmas; @@ -49,7 +50,7 @@ public: /** exist instantiation ? */ virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } //debug model - virtual void debugModel( TheoryModel* m ); + void debugModel(TheoryModel* m) override; //statistics unsigned getNumAddedLemmas() { return d_addedLemmas; } unsigned getNumTriedLemmas() { return d_triedLemmas; } @@ -87,7 +88,7 @@ class QModelBuilderIG : public QModelBuilder //whether inst gen was done bool d_didInstGen; /** process build model */ - virtual bool processBuildModel( TheoryModel* m ); + bool processBuildModel(TheoryModel* m) override; protected: //reset @@ -143,7 +144,9 @@ class QModelBuilderIG : public QModelBuilder // is quantifier active? bool isQuantifierActive( Node f ); //do exhaustive instantiation - int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ); + int doExhaustiveInstantiation(FirstOrderModel* fm, + Node f, + int effort) override; //temporary stats int d_numQuantSat; diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index 090374744..6412ea81b 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -49,18 +49,18 @@ public: ModelEngine( context::Context* c, QuantifiersEngine* qe ); virtual ~ModelEngine(); public: - bool needsCheck( Theory::Effort e ); - QEffort needsModel(Theory::Effort e); - void reset_round( Theory::Effort e ); - void check(Theory::Effort e, QEffort quant_e); - bool checkComplete(); - bool checkCompleteFor( Node q ); - void registerQuantifier( Node f ); - void assertNode( Node f ); - Node explain(TNode n){ return Node::null(); } - void debugPrint( const char* c ); - /** Identify this module */ - std::string identify() const { return "ModelEngine"; } + bool needsCheck(Theory::Effort e) override; + QEffort needsModel(Theory::Effort e) override; + void reset_round(Theory::Effort e) override; + void check(Theory::Effort e, QEffort quant_e) override; + bool checkComplete() override; + bool checkCompleteFor(Node q) override; + void registerQuantifier(Node f) override; + void assertNode(Node f) override; + Node explain(TNode n) { return Node::null(); } + void debugPrint(const char* c); + /** Identify this module */ + std::string identify() const override { return "ModelEngine"; } };/* class ModelEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h index 48de4f36c..157eb57fd 100644 --- a/src/theory/quantifiers/fun_def_engine.h +++ b/src/theory/quantifiers/fun_def_engine.h @@ -38,17 +38,17 @@ public: ~FunDefEngine(){} /* whether this module needs to check this round */ - bool needsCheck( Theory::Effort e ); + bool needsCheck(Theory::Effort e) override; /* reset at a round */ - void reset_round( Theory::Effort e ); + void reset_round(Theory::Effort e) override; /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e); + void check(Theory::Effort e, QEffort quant_e) override; /* Called for new quantifiers */ - void registerQuantifier( Node q ); + void registerQuantifier(Node q) override; /** called for everything that gets asserted */ - void assertNode( Node n ); + void assertNode(Node n) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "FunDefEngine"; } + std::string identify() const override { return "FunDefEngine"; } }; diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 7f485750a..e0c72c9fa 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -39,28 +39,29 @@ public: EqualityQueryInstProp( QuantifiersEngine* qe ); ~EqualityQueryInstProp(){}; /** reset */ - virtual bool reset(Theory::Effort e); + bool reset(Theory::Effort e) override; /* Called for new quantifiers */ - virtual void registerQuantifier(Node q) {} + void registerQuantifier(Node q) override {} /** identify */ - virtual std::string identify() const { return "EqualityQueryInstProp"; } + std::string identify() const override { return "EqualityQueryInstProp"; } /** extends engine */ - bool extendsEngine() { return true; } + bool extendsEngine() override { return true; } /** contains term */ - bool hasTerm( Node a ); + bool hasTerm(Node a) override; /** get the representative of the equivalence class of a */ - Node getRepresentative( Node a ); + Node getRepresentative(Node a) override; /** returns true if a and b are equal in the current context */ - bool areEqual( Node a, Node b ); + bool areEqual(Node a, Node b) override; /** returns true is a and b are disequal in the current context */ - bool areDisequal( Node a, Node b ); + bool areDisequal(Node a, Node b) override; /** get the equality engine associated with this query */ - eq::EqualityEngine* getEngine(); + eq::EqualityEngine* getEngine() override; /** get the equivalence class of a */ - void getEquivalenceClass( Node a, std::vector< Node >& eqc ); + void getEquivalenceClass(Node a, std::vector<Node>& eqc) override; /** get congruent term */ - TNode getCongruentTerm( Node f, std::vector< TNode >& args ); -public: + TNode getCongruentTerm(Node f, std::vector<TNode>& args) override; + + public: /** get the representative of the equivalence class of a, with explanation */ Node getRepresentativeExp( Node a, std::vector< Node >& exp ); /** returns true if a and b are equal in the current context */ @@ -114,15 +115,15 @@ private: InstPropagator& d_ip; public: InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {} - virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e, - Node q, - Node lem, - std::vector<Node>& terms, - Node body) + bool notifyInstantiation(QuantifiersModule::QEffort quant_e, + Node q, + Node lem, + std::vector<Node>& terms, + Node body) override { return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); } - virtual void filterInstantiations() { d_ip.filterInstantiations(); } + void filterInstantiations() override { d_ip.filterInstantiations(); } }; InstantiationNotifyInstPropagator d_notify; /** notify instantiation method */ @@ -173,11 +174,11 @@ public: InstPropagator( QuantifiersEngine* qe ); ~InstPropagator(){} /** reset */ - virtual bool reset(Theory::Effort e) override; + bool reset(Theory::Effort e) override; /* Called for new quantifiers */ - virtual void registerQuantifier(Node q) override {} + void registerQuantifier(Node q) override {} /** identify */ - virtual std::string identify() const override { return "InstPropagator"; } + std::string identify() const override { return "InstPropagator"; } /** get the notify mechanism */ InstantiationNotify* getInstantiationNotify() { return &d_notify; } }; diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index d1973eadb..18a06dc3d 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -93,13 +93,13 @@ class Instantiate : public QuantifiersUtil ~Instantiate(); /** reset */ - virtual bool reset(Theory::Effort e) override; + bool reset(Theory::Effort e) override; /** register quantifier */ - virtual void registerQuantifier(Node q) override; + void registerQuantifier(Node q) override; /** identify */ - virtual std::string identify() const override { return "Instantiate"; } + std::string identify() const override { return "Instantiate"; } /** check incomplete */ - virtual bool checkComplete() override; + bool checkComplete() override; //--------------------------------------notify objects /** add instantiation notify diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 3b19b8d55..76a781e1c 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -56,22 +56,21 @@ private: public: LtePartialInst( QuantifiersEngine * qe, context::Context* c ); /** determine whether this quantified formula will be reduced */ - void preRegisterQuantifier( Node q ); + void preRegisterQuantifier(Node q) override; /** was invoked */ bool wasInvoked() { return d_wasInvoked; } /* whether this module needs to check this round */ - bool needsCheck( Theory::Effort e ); + bool needsCheck(Theory::Effort e) override; /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e); + void check(Theory::Effort e, QEffort quant_e) override; /* Called for new quantifiers */ - void registerQuantifier( Node q ) {} + void registerQuantifier(Node q) override {} /* check complete */ - bool checkComplete() { return !d_wasInvoked; } - void assertNode( Node n ) {} + bool checkComplete() override { return !d_wasInvoked; } + void assertNode(Node n) override {} /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "LtePartialInst"; } - + std::string identify() const override { return "LtePartialInst"; } }; } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 3448e967b..77ea530ae 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -238,10 +238,11 @@ public: QuantConflictFind( QuantifiersEngine * qe, context::Context* c ); /** register quantifier */ - void registerQuantifier( Node q ); -public: + void registerQuantifier(Node q) override; + + public: /** assert quantifier */ - void assertNode( Node q ); + void assertNode(Node q) override; /** new node */ void newEqClass( Node n ); /** merge */ @@ -249,11 +250,11 @@ public: /** assert disequal */ void assertDisequal( Node a, Node b ); /** needs check */ - bool needsCheck( Theory::Effort level ); + bool needsCheck(Theory::Effort level) override; /** reset round */ - void reset_round( Theory::Effort level ); + void reset_round(Theory::Effort level) override; /** check */ - void check(Theory::Effort level, QEffort quant_e); + void check(Theory::Effort level, QEffort quant_e) override; private: bool d_needs_computeRelEqr; @@ -277,7 +278,7 @@ public: }; Statistics d_statistics; /** Identify this module */ - std::string identify() const { return "QcfEngine"; } + std::string identify() const override { return "QcfEngine"; } }; std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e); diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h index 47adddd9e..aa201bbc3 100644 --- a/src/theory/quantifiers/quant_equality_engine.h +++ b/src/theory/quantifiers/quant_equality_engine.h @@ -37,14 +37,38 @@ private: QuantEqualityEngine& d_qee; public: NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_qee.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) { d_qee.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) { d_qee.eqNotifyPreMerge(t1, t2); } - void eqNotifyPostMerge(TNode t1, TNode t2) { d_qee.eqNotifyPostMerge(t1, t2); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_qee.eqNotifyDisequal(t1, t2, reason); } + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { + return true; + } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { + return true; + } + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { + return true; + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { + d_qee.conflict(t1, t2); + } + void eqNotifyNewClass(TNode t) override { d_qee.eqNotifyNewClass(t); } + void eqNotifyPreMerge(TNode t1, TNode t2) override + { + d_qee.eqNotifyPreMerge(t1, t2); + } + void eqNotifyPostMerge(TNode t1, TNode t2) override + { + d_qee.eqNotifyPostMerge(t1, t2); + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override + { + d_qee.eqNotifyDisequal(t1, t2, reason); + } };/* class ConjectureGenerator::NotifyClass */ /** The notify class */ NotifyClass d_notify; @@ -75,17 +99,17 @@ public: QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ); /* whether this module needs to check this round */ - bool needsCheck( Theory::Effort e ); + bool needsCheck(Theory::Effort e) override; /* reset at a round */ - void reset_round( Theory::Effort e ); + void reset_round(Theory::Effort e) override; /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e); + void check(Theory::Effort e, QEffort quant_e) override; /* Called for new quantifiers */ - void registerQuantifier( Node q ); + void registerQuantifier(Node q) override; /** called for everything that gets asserted */ - void assertNode( Node n ); + void assertNode(Node n) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "QuantEqualityEngine"; } + std::string identify() const override { return "QuantEqualityEngine"; } /** queries */ bool areUnivDisequal( TNode n1, TNode n2 ); bool areUnivEqual( TNode n1, TNode n2 ); diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 3182df34b..0650b1c42 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -42,11 +42,11 @@ class QuantRelevance : public QuantifiersUtil QuantRelevance(bool cr) : d_computeRel(cr) {} ~QuantRelevance() {} /** reset */ - virtual bool reset(Theory::Effort e) override { return true; } + bool reset(Theory::Effort e) override { return true; } /** register quantifier */ - virtual void registerQuantifier(Node q) override; + void registerQuantifier(Node q) override; /** identify */ - virtual std::string identify() const override { return "QuantRelevance"; } + std::string identify() const override { return "QuantRelevance"; } /** set relevance of symbol s to r */ void setRelevance(Node s, int r); /** get relevance of symbol s */ diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 644583f04..1ea57433a 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -34,18 +34,18 @@ private: public: QuantDSplit( QuantifiersEngine * qe, context::Context* c ); /** determine whether this quantified formula will be reduced */ - void preRegisterQuantifier( Node q ); - + void preRegisterQuantifier(Node q) override; + /* whether this module needs to check this round */ - bool needsCheck( Theory::Effort e ); + bool needsCheck(Theory::Effort e) override; /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e); + void check(Theory::Effort e, QEffort quant_e) override; /* Called for new quantifiers */ - void registerQuantifier( Node q ) {} - void assertNode( Node n ) {} - bool checkCompleteFor( Node q ); + void registerQuantifier(Node q) override {} + void assertNode(Node n) override {} + bool checkCompleteFor(Node q) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "QuantDSplit"; } + std::string identify() const override { return "QuantDSplit"; } }; } diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 112530788..a138e4e21 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -43,11 +43,11 @@ class RelevantDomain : public QuantifiersUtil RelevantDomain(QuantifiersEngine* qe); virtual ~RelevantDomain(); /** Reset. */ - virtual bool reset(Theory::Effort e) override; + bool reset(Theory::Effort e) override; /** Register the quantified formula q */ - virtual void registerQuantifier(Node q) override; + void registerQuantifier(Node q) override; /** identify */ - virtual std::string identify() const override { return "RelevantDomain"; } + std::string identify() const override { return "RelevantDomain"; } /** Compute the relevant domain */ void compute(); /** Relevant domain representation. diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 2253ac1da..03cf0c996 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -50,13 +50,13 @@ private: public: RewriteEngine( context::Context* c, QuantifiersEngine* qe ); - bool needsCheck( Theory::Effort e ); - void check(Theory::Effort e, QEffort quant_e); - void registerQuantifier( Node f ); - void assertNode( Node n ); - bool checkCompleteFor( Node q ); + bool needsCheck(Theory::Effort e) override; + void check(Theory::Effort e, QEffort quant_e) override; + void registerQuantifier(Node f) override; + void assertNode(Node n) override; + bool checkCompleteFor(Node q) override; /** Identify this module */ - std::string identify() const { return "RewriteEngine"; } + std::string identify() const override { return "RewriteEngine"; } }; } diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h index 1b1d5e44b..e461a08d5 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h @@ -40,31 +40,31 @@ public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); ~CegInstantiation(); public: - bool needsCheck( Theory::Effort e ); - QEffort needsModel(Theory::Effort e); - /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e); - /* Called for new quantifiers */ - void registerQuantifier( Node q ); - /** get the next decision request */ - Node getNextDecisionRequest( unsigned& priority ); - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const { return "CegInstantiation"; } - /** print solution for synthesis conjectures */ - void printSynthSolution( std::ostream& out ); - /** get synth solutions - * - * This function adds entries to sol_map that map functions-to-synthesize - * with their solutions, for all active conjectures (currently just the one - * assigned to d_conj). This should be called immediately after the solver - * answers unsat for sygus input. - * - * For details on what is added to sol_map, see - * CegConjecture::getSynthSolutions. - */ - void getSynthSolutions(std::map<Node, Node>& sol_map); - /** preregister assertion (before rewrite) */ - void preregisterAssertion( Node n ); + bool needsCheck(Theory::Effort e) override; + QEffort needsModel(Theory::Effort e) override; + /* Call during quantifier engine's check */ + void check(Theory::Effort e, QEffort quant_e) override; + /* Called for new quantifiers */ + void registerQuantifier(Node q) override; + /** get the next decision request */ + Node getNextDecisionRequest(unsigned& priority) override; + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const override { return "CegInstantiation"; } + /** print solution for synthesis conjectures */ + void printSynthSolution(std::ostream& out); + /** get synth solutions + * + * This function adds entries to sol_map that map functions-to-synthesize + * with their solutions, for all active conjectures (currently just the one + * assigned to d_conj). This should be called immediately after the solver + * answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * CegConjecture::getSynthSolutions. + */ + void getSynthSolutions(std::map<Node, Node>& sol_map); + /** preregister assertion (before rewrite) */ + void preregisterAssertion(Node n); public: class Statistics { public: diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index abdbef708..70ba2c283 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -37,9 +37,9 @@ public: CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} virtual ~CegqiOutputSingleInv() {} CegConjectureSingleInv * d_out; - bool doAddInstantiation( std::vector< Node >& subs ); - bool isEligibleForInstantiation( Node n ); - bool addLemma( Node lem ); + bool doAddInstantiation(std::vector<Node>& subs) override; + bool isEligibleForInstantiation(Node n) override; + bool addLemma(Node lem) override; }; class DetTrace { diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index a43e38719..9e357f928 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -112,7 +112,7 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest protected: /** does d_conj{ d_var -> nvn } still rewrite to d_result? */ - bool invariant(TermDbSygus* tds, Node nvn, Node x); + bool invariant(TermDbSygus* tds, Node nvn, Node x) override; private: /** the formula we are evaluating */ @@ -170,7 +170,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest protected: /** checks whether the analog of nvn still rewrites to d_bvr */ - bool invariant(TermDbSygus* tds, Node nvn, Node x); + bool invariant(TermDbSygus* tds, Node nvn, Node x) override; private: /** the conjecture associated with the enumerator d_enum */ @@ -202,7 +202,7 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest protected: /** checks whether nvn involves division by zero. */ - bool invariant(TermDbSygus* tds, Node nvn, Node x); + bool invariant(TermDbSygus* tds, Node nvn, Node x) override; }; /** NegContainsSygusInvarianceTest @@ -254,7 +254,7 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest protected: /** checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i. */ - bool invariant(TermDbSygus* tds, Node nvn, Node x); + bool invariant(TermDbSygus* tds, Node nvn, Node x) override; private: /** The enumerator whose value we are considering in this invariance test */ diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 06576d6ce..eba1a87b1 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -176,7 +176,7 @@ class SygusSampler : public LazyTrieEvaluator std::vector<Node>& vars, std::vector<Node>& pt); /** evaluate n on sample point index */ - Node evaluate(Node n, unsigned index); + Node evaluate(Node n, unsigned index) override; /** * Returns the index of a sample point such that the evaluation of a and b * diverge, or -1 if no such sample point exists. @@ -367,7 +367,7 @@ class SygusSamplerExt : public SygusSampler * from the set of all previous input/output pairs based on the * d_drewrite utility. */ - virtual Node registerTerm(Node n, bool forceKeep = false) override; + Node registerTerm(Node n, bool forceKeep = false) override; private: /** dynamic rewriter class */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index de766cc2a..e440e68e9 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -141,11 +141,11 @@ class TermDb : public QuantifiersUtil { /** presolve (called once per user check-sat) */ void presolve(); /** reset (calculate which terms are active) */ - virtual bool reset(Theory::Effort effort) override; + bool reset(Theory::Effort effort) override; /** register quantified formula */ - virtual void registerQuantifier(Node q) override; + void registerQuantifier(Node q) override; /** identify */ - virtual std::string identify() const override { return "TermDb"; } + std::string identify() const override { return "TermDb"; } /** get number of operators */ unsigned getNumOperators(); /** get operator at index i */ diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 83d9d7940..bb02b1d6a 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -117,11 +117,11 @@ public: Node d_one; /** reset */ - virtual bool reset(Theory::Effort e) override { return true; } + bool reset(Theory::Effort e) override { return true; } /** register quantifier */ - virtual void registerQuantifier(Node q) override; + void registerQuantifier(Node q) override; /** identify */ - virtual std::string identify() const override { return "TermUtil"; } + std::string identify() const override { return "TermUtil"; } // for inst constant private: /** map from universal quantifiers to the list of variables */ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 7468d2778..9f3134f84 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -135,7 +135,7 @@ class TheorySep : public Theory { public: NotifyClass(TheorySep& sep) : d_sep(sep) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) + bool eqNotifyTriggerEquality(TNode equality, bool value) override { Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " @@ -151,7 +151,7 @@ class TheorySep : public Theory { } } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override { Unreachable(); } @@ -159,7 +159,7 @@ class TheorySep : public Theory { bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, - bool value) + bool value) override { Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 @@ -176,23 +176,23 @@ class TheorySep : public Theory { return true; } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override { Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_sep.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) {} - void eqNotifyPreMerge(TNode t1, TNode t2) + void eqNotifyNewClass(TNode t) override {} + void eqNotifyPreMerge(TNode t1, TNode t2) override { d_sep.eqNotifyPreMerge(t1, t2); } - void eqNotifyPostMerge(TNode t1, TNode t2) + void eqNotifyPostMerge(TNode t1, TNode t2) override { d_sep.eqNotifyPostMerge(t1, t2); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {} + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} }; /** The notify class for d_equalityEngine */ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index bd63ff43d..b57f208bd 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -253,14 +253,17 @@ private: public: NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {} - bool eqNotifyTriggerEquality(TNode equality, bool value); - bool eqNotifyTriggerPredicate(TNode predicate, bool value); - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); - void eqNotifyConstantTermMerge(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2); - void eqNotifyPostMerge(TNode t1, TNode t2); - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + bool eqNotifyTriggerEquality(TNode equality, bool value) override; + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override; + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + void eqNotifyNewClass(TNode t) override; + void eqNotifyPreMerge(TNode t1, TNode t2) override; + void eqNotifyPostMerge(TNode t1, TNode t2) override; + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; } d_notify; /** Equality engine */ diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 5ca625751..bc4db97ee 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -78,28 +78,35 @@ private: SharedTermsDatabase& d_sharedTerms; public: EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { d_sharedTerms.propagateEquality(equality, value); return true; } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { Unreachable(); return true; } - bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { + bool eqNotifyTriggerTermEquality(theory::TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value); } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { d_sharedTerms.conflict(t1, t2, true); } - void eqNotifyNewClass(TNode t) { } - void eqNotifyPreMerge(TNode t1, TNode t2) { } - void eqNotifyPostMerge(TNode t1, TNode t2) { } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + void eqNotifyNewClass(TNode t) override {} + void eqNotifyPreMerge(TNode t1, TNode t2) override {} + void eqNotifyPostMerge(TNode t1, TNode t2) override {} + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} }; /** The notify class for d_equalityEngine */ @@ -245,9 +252,7 @@ protected: /** * This method gets called on backtracks from the context manager. */ - void contextNotifyPop() { - backtrack(); - } + void contextNotifyPop() override { backtrack(); } }; } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index e07cc6b5e..5dbbb93d6 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -81,7 +81,8 @@ class TheoryStrings : public Theory { TheoryStrings& d_str; public: NotifyClass(TheoryStrings& t_str): d_str(t_str) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; if (value) { return d_str.propagate(equality); @@ -90,7 +91,8 @@ class TheoryStrings : public Theory { return d_str.propagate(equality.notNode()); } } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { return d_str.propagate(predicate); @@ -98,7 +100,11 @@ class TheoryStrings : public Theory { return d_str.propagate(predicate.notNode()); } } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_str.propagate(t1.eqNode(t2)); @@ -106,23 +112,28 @@ class TheoryStrings : public Theory { return d_str.propagate(t1.eqNode(t2).notNode()); } } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_str.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) { + void eqNotifyNewClass(TNode t) override + { Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; d_str.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) { + void eqNotifyPreMerge(TNode t1, TNode t2) override + { Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; d_str.eqNotifyPreMerge(t1, t2); } - void eqNotifyPostMerge(TNode t1, TNode t2) { + void eqNotifyPostMerge(TNode t1, TNode t2) override + { Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; d_str.eqNotifyPostMerge(t1, t2); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override + { Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; d_str.eqNotifyDisequal(t1, t2, reason); } diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index cca39a62e..2a2531887 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -76,9 +76,8 @@ private: class CacheInvalidator : public context::ContextNotifyObj { bool& d_cacheInvalidated; protected: - void contextNotifyPop() { - d_cacheInvalidated = true; - } + void contextNotifyPop() override { d_cacheInvalidated = true; } + public: CacheInvalidator(context::Context* context, bool& cacheInvalidated) : context::ContextNotifyObj(context), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7bc95b097..04e3c5697 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -157,14 +157,35 @@ class TheoryEngine { TheoryEngine& d_te; public: NotifyClass(TheoryEngine& te): d_te(te) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } - bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { return true; } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) {} - void eqNotifyNewClass(TNode t) { d_te.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) { d_te.eqNotifyPreMerge(t1, t2); } - void eqNotifyPostMerge(TNode t1, TNode t2) { d_te.eqNotifyPostMerge(t1, t2); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_te.eqNotifyDisequal(t1, t2, reason); } + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { + return true; + } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { + return true; + } + bool eqNotifyTriggerTermEquality(theory::TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { + return true; + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {} + void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); } + void eqNotifyPreMerge(TNode t1, TNode t2) override + { + d_te.eqNotifyPreMerge(t1, t2); + } + void eqNotifyPostMerge(TNode t1, TNode t2) override + { + d_te.eqNotifyPostMerge(t1, t2); + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override + { + d_te.eqNotifyDisequal(t1, t2, reason); + } };/* class TheoryEngine::NotifyClass */ NotifyClass d_masterEENotify; diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index bb74569b7..5b4a2d983 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -67,7 +67,7 @@ class TheoryEngineModelBuilder : public ModelBuilder * builder in steps (2) or (5), for instance, if the model we * are building fails to satisfy a quantified formula. */ - virtual bool buildModel(Model* m) override; + bool buildModel(Model* m) override; /** Debug check model. * * This throws an assertion failure if the model diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h index df576a694..2514ccce0 100644 --- a/src/theory/theory_registrar.h +++ b/src/theory/theory_registrar.h @@ -37,9 +37,7 @@ public: TheoryRegistrar(TheoryEngine* te) : d_theoryEngine(te) { } - void preRegister(Node n) { - d_theoryEngine->preRegister(n); - } + void preRegister(Node n) override { d_theoryEngine->preRegister(n); } };/* class TheoryRegistrar */ diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 7ca4a6140..736a65ade 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -84,7 +84,10 @@ public: TypeEnumeratorInterface(type) { } - TypeEnumeratorInterface* clone() const { return new T(static_cast<const T&>(*this)); } + TypeEnumeratorInterface* clone() const override + { + return new T(static_cast<const T&>(*this)); + } };/* class TypeEnumeratorBase */ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index a89e55312..2d757cb28 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -131,14 +131,26 @@ public: */ class EqualityEngineNotifyNone : public EqualityEngineNotify { public: - bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { } - void eqNotifyNewClass(TNode t) { } - void eqNotifyPreMerge(TNode t1, TNode t2) { } - void eqNotifyPostMerge(TNode t1, TNode t2) { } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { + return true; + } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { + return true; + } + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { + return true; + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {} + void eqNotifyNewClass(TNode t) override {} + void eqNotifyPreMerge(TNode t1, TNode t2) override {} + void eqNotifyPostMerge(TNode t1, TNode t2) override {} + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} };/* class EqualityEngineNotifyNone */ /** @@ -538,9 +550,7 @@ private: /** * This method gets called on backtracks from the context manager. */ - void contextNotifyPop() { - backtrack(); - } + void contextNotifyPop() override { backtrack(); } /** * Constructor initialization stuff. diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 6fde4a9af..bac03c34c 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -55,7 +55,8 @@ public: public: NotifyClass(TheoryUF& uf): d_uf(uf) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; if (value) { return d_uf.propagate(equality); @@ -65,7 +66,8 @@ public: } } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { return d_uf.propagate(predicate); @@ -74,7 +76,11 @@ public: } } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_uf.propagate(t1.eqNode(t2)); @@ -83,27 +89,32 @@ public: } } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) { + void eqNotifyNewClass(TNode t) override + { Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; d_uf.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) { + void eqNotifyPreMerge(TNode t1, TNode t2) override + { Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.eqNotifyPreMerge(t1, t2); } - void eqNotifyPostMerge(TNode t1, TNode t2) { + void eqNotifyPostMerge(TNode t1, TNode t2) override + { Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.eqNotifyPostMerge(t1, t2); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override + { Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl; d_uf.eqNotifyDisequal(t1, t2, reason); } diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 73a545185..b0ce5698a 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -228,21 +228,21 @@ public: virtual const T& getDataRef() const = 0; /** Flush the value of the statistic to the given output stream. */ - void flushInformation(std::ostream& out) const { + void flushInformation(std::ostream& out) const override + { if(__CVC4_USE_STATISTICS) { out << getData(); } } - virtual void safeFlushInformation(int fd) const { + void safeFlushInformation(int fd) const override + { if (__CVC4_USE_STATISTICS) { safe_print<T>(fd, getDataRef()); } } - SExpr getValue() const { - return mkSExpr(getData()); - } + SExpr getValue() const override { return mkSExpr(getData()); } };/* class ReadOnlyDataStat<T> */ @@ -315,17 +315,18 @@ public: } /** Set this reference statistic to refer to the given data cell. */ - void setData(const T& t) { + void setData(const T& t) override + { if(__CVC4_USE_STATISTICS) { d_data = &t; } } /** Get the value of the referenced data cell. */ - virtual T getData() const { return *d_data; } + T getData() const override { return *d_data; } /** Get a reference to the value of the referenced data cell. */ - virtual const T& getDataRef() const { return *d_data; } + const T& getDataRef() const override { return *d_data; } };/* class ReferenceStat<T> */ @@ -349,7 +350,8 @@ public: } /** Set the underlying data value to the given value. */ - void setData(const T& t) { + void setData(const T& t) override + { if(__CVC4_USE_STATISTICS) { d_data = t; } @@ -364,10 +366,10 @@ public: } /** Get the underlying data value. */ - virtual T getData() const { return d_data; } + T getData() const override { return d_data; } /** Get a reference to the underlying data value. */ - virtual const T& getDataRef() const { return d_data; } + const T& getDataRef() const override { return d_data; } };/* class BackedStat<T> */ @@ -406,21 +408,20 @@ public: } /** Get the data of the underlying (wrapped) statistic. */ - virtual T getData() const { return d_stat.getData(); } + T getData() const override { return d_stat.getData(); } /** Get a reference to the data of the underlying (wrapped) statistic. */ - virtual const T& getDataRef() const { return d_stat.getDataRef(); } + const T& getDataRef() const override { return d_stat.getDataRef(); } - virtual void safeFlushInformation(int fd) const { + void safeFlushInformation(int fd) const override + { // ReadOnlyDataStat uses getDataRef() to get the information to print, // which might not be appropriate for all wrapped statistics. Delegate the // printing to the wrapped statistic instead. d_stat.safeFlushInformation(fd); } - SExpr getValue() const { - return d_stat.getValue(); - } + SExpr getValue() const override { return d_stat.getValue(); } };/* class WrappedStat<T> */ @@ -474,9 +475,7 @@ public: } } - SExpr getValue() const { - return SExpr(Integer(d_data)); - } + SExpr getValue() const override { return SExpr(Integer(d_data)); } };/* class IntStat */ @@ -489,17 +488,17 @@ public: Stat(name), d_sized(sized) {} ~SizeStat() {} - void flushInformation(std::ostream& out) const { + void flushInformation(std::ostream& out) const override + { out << d_sized.size(); } - void safeFlushInformation(int fd) const { + void safeFlushInformation(int fd) const override + { safe_print<uint64_t>(fd, d_sized.size()); } - SExpr getValue() const { - return SExpr(Integer(d_sized.size())); - } + SExpr getValue() const override { return SExpr(Integer(d_sized.size())); } };/* class SizeStat */ @@ -538,7 +537,8 @@ public: } } - SExpr getValue() const { + SExpr getValue() const override + { std::stringstream ss; ss << std::fixed << std::setprecision(8) << d_data; return SExpr(Rational::fromDecimal(ss.str())); @@ -560,19 +560,19 @@ public: SExprStat(const std::string& name, const SExpr& init) : Stat(name), d_data(init){} - virtual void flushInformation(std::ostream& out) const { + void flushInformation(std::ostream& out) const override + { out << d_data << std::endl; } - virtual void safeFlushInformation(int fd) const { + void safeFlushInformation(int fd) const override + { // SExprStat is only used in statistics.cpp in copyFrom, which we cannot // do in a signal handler anyway. safe_print(fd, "<unsupported>"); } - SExpr getValue() const { - return d_data; - } + SExpr getValue() const override { return d_data; } };/* class SExprStat */ @@ -587,7 +587,8 @@ public: HistogramStat(const std::string& name) : Stat(name) {} ~HistogramStat() {} - void flushInformation(std::ostream& out) const{ + void flushInformation(std::ostream& out) const override + { if(__CVC4_USE_STATISTICS) { typename Histogram::const_iterator i = d_hist.begin(); typename Histogram::const_iterator end = d_hist.end(); @@ -605,7 +606,8 @@ public: } } - virtual void safeFlushInformation(int fd) const { + void safeFlushInformation(int fd) const override + { if (__CVC4_USE_STATISTICS) { typename Histogram::const_iterator i = d_hist.begin(); typename Histogram::const_iterator end = d_hist.end(); @@ -665,18 +667,17 @@ public: * Set the name of this statistic registry, used as prefix during * output. (This version overrides StatisticsBase::setPrefix().) */ - void setPrefix(const std::string& name) { - d_prefix = d_name = name; - } + void setPrefix(const std::string& name) override { d_prefix = d_name = name; } /** Overridden to avoid the name being printed */ - void flushStat(std::ostream &out) const; + void flushStat(std::ostream& out) const override; - virtual void flushInformation(std::ostream& out) const; + void flushInformation(std::ostream& out) const override; - virtual void safeFlushInformation(int fd) const; + void safeFlushInformation(int fd) const override; - SExpr getValue() const { + SExpr getValue() const override + { std::vector<SExpr> v; for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { std::vector<SExpr> w; @@ -734,9 +735,10 @@ public: /** If the timer is currently running */ bool running() const; - virtual timespec getData() const; + timespec getData() const override; - virtual void safeFlushInformation(int fd) const { + void safeFlushInformation(int fd) const override + { // Overwrite the implementation in the superclass because we cannot use // getDataRef(): it might return stale data if the timer is currently // running. @@ -744,7 +746,7 @@ public: safe_print<timespec>(fd, data); } - SExpr getValue() const; + SExpr getValue() const override; };/* class TimerStat */ |