diff options
Diffstat (limited to 'src/theory/quantifiers')
31 files changed, 377 insertions, 319 deletions
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 */ |