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 /src/theory | |
parent | a2e78ec8dd5e935b6ef166154be7ee35bffc6d32 (diff) |
Enable -Wsuggest-override by default. (#1643)
Adds missing override keywords.
Diffstat (limited to 'src/theory')
64 files changed, 694 insertions, 534 deletions
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); } |