From b258ebd1cb08252f8cf7f317c08eadbe1fb8e8fe Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 6 Feb 2018 15:55:40 -0800 Subject: Resolving warnings from -Winconsistent-missing-override on clang. (#1563) --- src/theory/arith/theory_arith.h | 52 ++++---- src/theory/arrays/theory_arrays.h | 77 +++++------- src/theory/bv/theory_bv.h | 43 ++++--- src/theory/datatypes/theory_datatypes.h | 54 +++++---- src/theory/fp/theory_fp.h | 16 +-- src/theory/quantifiers/ceg_t_instantiator.h | 65 +++++----- src/theory/quantifiers/first_order_model.h | 12 +- src/theory/quantifiers/inst_match_generator.h | 2 +- src/theory/quantifiers/inst_strategy_cbqi.h | 17 +-- src/theory/quantifiers/model_builder.h | 7 +- src/theory/quantifiers/theory_quantifiers.h | 52 ++++---- src/theory/sep/theory_sep.h | 144 ++++++++++++---------- src/theory/sets/theory_sets.h | 32 ++--- src/theory/strings/theory_strings.h | 167 +++++++++++++++----------- src/theory/theory_model.h | 10 +- src/theory/uf/theory_uf.h | 34 +++--- 16 files changed, 421 insertions(+), 363 deletions(-) diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1c10bde0d..4f3a13b4d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -48,41 +48,47 @@ public: /** * Does non-context dependent setup for a node connected to a theory. */ - void preRegisterTerm(TNode n); + void preRegisterTerm(TNode n) override; - Node expandDefinition(LogicRequest &logicRequest, Node node); + Node expandDefinition(LogicRequest& logicRequest, Node node) override; - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - void check(Effort e); - bool needsCheckLastEffort(); - void propagate(Effort e); - Node explain(TNode n); - bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); - bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ); + void check(Effort e) override; + bool needsCheckLastEffort() override; + void propagate(Effort e) override; + Node explain(TNode n) override; + bool getCurrentSubstitution(int effort, + std::vector& vars, + std::vector& subs, + std::map >& exp) override; + bool isExtfReduced(int effort, + Node n, + Node on, + std::vector& exp) override; bool collectModelInfo(TheoryModel* m) override; - void shutdown(){ } + void shutdown() override {} - void presolve(); - void notifyRestart(); - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); - void ppStaticLearn(TNode in, NodeBuilder<>& learned); + void presolve() override; + void notifyRestart() override; + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + Node ppRewrite(TNode atom) override; + void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; - std::string identify() const { return std::string("TheoryArith"); } + std::string identify() const override { return std::string("TheoryArith"); } - EqualityStatus getEqualityStatus(TNode a, TNode b); + EqualityStatus getEqualityStatus(TNode a, TNode b) override; - void addSharedTerm(TNode n); + void addSharedTerm(TNode n) override; - Node getModelValue(TNode var); + Node getModelValue(TNode var) override; - - std::pair entailmentCheck(TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* out); + std::pair entailmentCheck( + TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out) override; };/* class TheoryArith */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 24c286e92..caf466c0c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -143,9 +143,9 @@ class TheoryArrays : public Theory { std::string name = ""); ~TheoryArrays(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - std::string identify() const { return std::string("TheoryArrays"); } + std::string identify() const override { return std::string("TheoryArrays"); } ///////////////////////////////////////////////////////////////////////////// // PREPROCESSING @@ -174,17 +174,15 @@ class TheoryArrays : public Theory { bool ppDisequal(TNode a, TNode b); Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck); - public: - - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); + public: + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + Node ppRewrite(TNode atom) override; ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// - private: - + private: /** Literals to propagate */ context::CDList d_literalsToPropagate; @@ -204,19 +202,17 @@ class TheoryArrays : public Theory { /** Helper for preRegisterTerm, also used internally */ void preRegisterTermInternal(TNode n); - public: - - void preRegisterTerm(TNode n); - void propagate(Effort e); + public: + void preRegisterTerm(TNode n) override; + void propagate(Effort e) override; Node explain(TNode n, eq::EqProof* proof); - Node explain(TNode n); + Node explain(TNode n) override; ///////////////////////////////////////////////////////////////////////////// // SHARING ///////////////////////////////////////////////////////////////////////////// - private: - + private: class MayEqualNotifyClass { public: bool notify(TNode propagation) { return true; } @@ -232,46 +228,40 @@ class TheoryArrays : public Theory { // Helper for computeCareGraph void checkPair(TNode r1, TNode r2); - public: - - void addSharedTerm(TNode t); - EqualityStatus getEqualityStatus(TNode a, TNode b); - void computeCareGraph(); + public: + void addSharedTerm(TNode t) override; + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + void computeCareGraph() override; bool isShared(TNode t) - { return (d_sharedArrays.find(t) != d_sharedArrays.end()); } - + { + return (d_sharedArrays.find(t) != d_sharedArrays.end()); + } ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - private: - - public: - bool collectModelInfo(TheoryModel* m) override; - - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// + public: + bool collectModelInfo(TheoryModel* m) override; - private: - public: + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// - Node getNextDecisionRequest( unsigned& priority ); + public: + Node getNextDecisionRequest(unsigned& priority) override; - void presolve(); - void shutdown() { } + void presolve() override; + void shutdown() override {} ///////////////////////////////////////////////////////////////////////////// // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// - public: - - void check(Effort e); - - private: + public: + void check(Effort e) override; + private: TNode weakEquivGetRep(TNode node); TNode weakEquivGetRepIndex(TNode node, TNode index); void visitAllLeaves(TNode reason, std::vector& conjunctions); @@ -454,11 +444,8 @@ class TheoryArrays : public Theory { /** An equality-engine callback for proof reconstruction */ ArrayProofReconstruction d_proofReconstruction; - public: - - eq::EqualityEngine* getEqualityEngine() { - return &d_equalityEngine; - } + public: + eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } };/* class TheoryArrays */ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8cefe03b2..1992c0ae3 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -64,40 +64,43 @@ public: ~TheoryBV(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - Node expandDefinition(LogicRequest &logicRequest, Node node); + Node expandDefinition(LogicRequest& logicRequest, Node node) override; void mkAckermanizationAssertions(std::vector& assertions); - void preRegisterTerm(TNode n); + void preRegisterTerm(TNode n) override; - void check(Effort e); - - bool needsCheckLastEffort(); + void check(Effort e) override; + + bool needsCheckLastEffort() override; - void propagate(Effort e); + void propagate(Effort e) override; - Node explain(TNode n); + Node explain(TNode n) override; bool collectModelInfo(TheoryModel* m) override; - std::string identify() const { return std::string("TheoryBV"); } + std::string identify() const override { return std::string("TheoryBV"); } /** equality engine */ - eq::EqualityEngine * getEqualityEngine(); - bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); - int getReduction( int effort, Node n, Node& nr ); - - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + eq::EqualityEngine* getEqualityEngine() override; + bool getCurrentSubstitution(int effort, + std::vector& vars, + std::vector& subs, + std::map >& exp) override; + int getReduction(int effort, Node n, Node& nr) override; + + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void enableCoreTheorySlicer(); - Node ppRewrite(TNode t); + Node ppRewrite(TNode t) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned); + void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; - void presolve(); + void presolve() override; bool applyAbstraction(const std::vector& assertions, std::vector& new_assertions); @@ -206,13 +209,13 @@ private: */ void explain(TNode literal, std::vector& assumptions); - void addSharedTerm(TNode t); + void addSharedTerm(TNode t) override; bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } - EqualityStatus getEqualityStatus(TNode a, TNode b); + EqualityStatus getEqualityStatus(TNode a, TNode b) override; - Node getModelValue(TNode var); + Node getModelValue(TNode var) override; inline std::string indent() { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index a3001d042..8052df59a 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -220,21 +220,21 @@ private: /** get eqc constructor */ TNode getEqcConstructor( TNode r ); -protected: + protected: void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ); /** compute care graph */ - void computeCareGraph(); + void computeCareGraph() override; -public: + public: TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryDatatypes(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; /** propagate */ - void propagate(Effort effort); + void propagate(Effort effort) override; /** propagate */ bool propagate(TNode literal); /** explain */ @@ -242,7 +242,7 @@ public: void explainEquality( TNode a, TNode b, bool polarity, std::vector& assumptions ); void explainPredicate( TNode p, bool polarity, std::vector& assumptions ); void explain( TNode literal, std::vector& assumptions ); - Node explain( TNode literal ); + Node explain(TNode literal) override; Node explain( std::vector< Node >& lits ); /** Conflict when merging two constants */ void conflict(TNode a, TNode b); @@ -255,26 +255,36 @@ public: /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - void check(Effort e); - bool needsCheckLastEffort(); - void preRegisterTerm(TNode n); - void finishInit(); - Node expandDefinition(LogicRequest &logicRequest, Node n); - Node ppRewrite(TNode n); - void presolve(); - void addSharedTerm(TNode t); - EqualityStatus getEqualityStatus(TNode a, TNode b); + void check(Effort e) override; + bool needsCheckLastEffort() override; + void preRegisterTerm(TNode n) override; + void finishInit() override; + Node expandDefinition(LogicRequest& logicRequest, Node n) override; + Node ppRewrite(TNode n) override; + void presolve() override; + void addSharedTerm(TNode t) override; + EqualityStatus getEqualityStatus(TNode a, TNode b) override; bool collectModelInfo(TheoryModel* m) override; - void shutdown() { } - std::string identify() const { return std::string("TheoryDatatypes"); } + void shutdown() override {} + std::string identify() const override + { + return std::string("TheoryDatatypes"); + } /** equality engine */ - eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; } - bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); + eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } + bool getCurrentSubstitution(int effort, + std::vector& vars, + std::vector& subs, + std::map >& exp) override; /** debug print */ void printModelDebug( const char* c ); /** entailment check */ - virtual std::pair entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); -private: + std::pair entailmentCheck( + TNode lit, + const EntailmentCheckParameters* params = NULL, + EntailmentCheckSideEffects* out = NULL) override; + + private: /** add tester to equivalence class info */ void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg ); /** add selector to equivalence class info */ @@ -325,7 +335,7 @@ private: SygusSymBreakNew* d_sygus_sym_break; public: - Node getNextDecisionRequest( unsigned& priority ); + Node getNextDecisionRequest(unsigned& priority) override; };/* class TheoryDatatypes */ }/* CVC4::theory::datatypes namespace */ diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 614cbff46..ca80546b8 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -38,21 +38,21 @@ class TheoryFp : public Theory { TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); - Node expandDefinition(LogicRequest& lr, Node node); + Node expandDefinition(LogicRequest& lr, Node node) override; - void preRegisterTerm(TNode node); - void addSharedTerm(TNode node); + void preRegisterTerm(TNode node) override; + void addSharedTerm(TNode node) override; - void check(Effort); + void check(Effort) override; - Node getModelValue(TNode var); + Node getModelValue(TNode var) override; bool collectModelInfo(TheoryModel* m) override; - std::string identify() const { return "THEORY_FP"; } + std::string identify() const override { return "THEORY_FP"; } - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - Node explain(TNode n); + Node explain(TNode n) override; protected: /** Equality engine */ diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index a607909cc..95295d214 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -187,43 +187,44 @@ class EprInstantiator : public Instantiator { class BvInstantiator : public Instantiator { public: BvInstantiator(QuantifiersEngine* qe, TypeNode tn); - virtual ~BvInstantiator(); - virtual void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - virtual bool hasProcessAssertion(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override + ~BvInstantiator() override; + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + 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; + 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; /** use model value * * We allow model values if we have not already tried an assertion, * and only at levels below full if cbqiFullEffort is false. */ - virtual bool useModelValue(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) override; - virtual std::string identify() const { return "Bv"; } + bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + std::string identify() const override { return "Bv"; } + private: // point to the bv inverter class BvInverter * d_inverter; @@ -281,7 +282,7 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess { public: BvInstantiatorPreprocess() {} - virtual ~BvInstantiatorPreprocess() {} + ~BvInstantiatorPreprocess() override {} /** register counterexample lemma * * This method modifies the contents of lems based on the extract terms @@ -308,8 +309,8 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess * since the added equalities ensure we are able to construct the proper * solved forms for variables in t and for the intermediate variables above. */ - virtual void registerCounterexampleLemma(std::vector& lems, - std::vector& ce_vars) override; + void registerCounterexampleLemma(std::vector& lems, + std::vector& ce_vars) override; private: /** collect extracts diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 0c4b6b7a4..f33151b4d 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -248,19 +248,21 @@ class Def; class FirstOrderModelFmc : public FirstOrderModel { friend class FullModelChecker; -private: + + private: /** models for UF */ std::map d_models; std::map d_type_star; Node intervalOp; /** get current model value */ - void processInitializeModelForTerm(Node n); -public: + void processInitializeModelForTerm(Node n) override; + + public: FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); ~FirstOrderModelFmc() override; - FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } + FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; } // initialize the model - void processInitialize( bool ispre ); + void processInitialize(bool ispre) override; Node getFunctionValue(Node op, const char* argPrefix ); bool isStar(Node n); diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index fc913c7cf..1903a0f95 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -222,7 +222,7 @@ class InstMatchGenerator : public IMGenerator { * * See Trigger::getActiveScore for details. */ - int getActiveScore(QuantifiersEngine* qe); + int getActiveScore(QuantifiersEngine* qe) override; /** exclude match * * Exclude matching d_match_pattern with Node n on subsequent calls to diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index c2520a973..26591c678 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -129,18 +129,19 @@ public: }; class InstStrategyCegqi : public InstStrategyCbqi { -protected: + protected: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; Node d_small_const; Node d_curr_quant; bool d_check_vts_lemma_lc; /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); - void process( Node f, Theory::Effort effort, int e ); + void processResetInstantiationRound(Theory::Effort effort) override; + void process(Node f, Theory::Effort effort, int e) override; /** register ce lemma */ - void registerCounterexampleLemma( Node q, Node lem ); -public: + void registerCounterexampleLemma(Node q, Node lem) override; + + public: InstStrategyCegqi( QuantifiersEngine * qe ); ~InstStrategyCegqi() override; @@ -148,14 +149,14 @@ public: bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); /** identify */ - std::string identify() const { return std::string("Cegqi"); } + std::string identify() const override { return std::string("Cegqi"); } //get instantiator for quantifier CegInstantiator * getInstantiator( Node q ); //register quantifier - void registerQuantifier( Node q ); + void registerQuantifier(Node q) override; //presolve - void presolve(); + void presolve() override; }; } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 511aebf3b..4eb592b3e 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -178,7 +178,7 @@ class QModelBuilderDefault : public QModelBuilderIG //do InstGen techniques for quantifier, return number of lemmas produced int doInstGen(FirstOrderModel* fm, Node f) override; //theory-specific build models - void constructModelUf( FirstOrderModel* fm, Node op ); + void constructModelUf(FirstOrderModel* fm, Node op) override; protected: std::map< Node, QuantPhaseReq > d_phase_reqs; @@ -189,7 +189,10 @@ class QModelBuilderDefault : public QModelBuilderIG //options bool optReconsiderFuncConstants() { return true; } //has inst gen - bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); } + bool hasInstGen(Node f) override + { + return !d_quant_selection_lit[f].isNull(); + } }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 295a39464..4f87f6aae 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -33,37 +33,47 @@ namespace theory { namespace quantifiers { class TheoryQuantifiers : public Theory { -private: - typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - /** number of instantiations */ - int d_numInstantiations; - int d_baseDecLevel; -private: - void computeCareGraph(); - -public: + public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryQuantifiers(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); - void addSharedTerm(TNode t); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; + void addSharedTerm(TNode t) override; void notifyEq(TNode lhs, TNode rhs); - void preRegisterTerm(TNode n); - void presolve(); - void ppNotifyAssertions(const std::vector& assertions); - void check(Effort e); - Node getNextDecisionRequest( unsigned& priority ); + void preRegisterTerm(TNode n) override; + void presolve() override; + void ppNotifyAssertions(const std::vector& assertions) override; + void check(Effort e) override; + Node getNextDecisionRequest(unsigned& priority) override; Node getValue(TNode n); bool collectModelInfo(TheoryModel* m) override; - void shutdown() { } - std::string identify() const { return std::string("TheoryQuantifiers"); } - void setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value); - bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; } -private: + void shutdown() override {} + std::string identify() const override + { + return std::string("TheoryQuantifiers"); + } + void setUserAttribute(const std::string& attr, + Node n, + std::vector node_values, + std::string str_value) override; + bool ppDontRewriteSubterm(TNode atom) override + { + return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; + } + + private: void assertUniversal( Node n ); void assertExistential( Node n ); + void computeCareGraph() override; + + using BoolMap = context::CDHashMap; + + /** number of instantiations */ + int d_numInstantiations; + int d_baseDecLevel; + };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 65f076631..7468d2778 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -43,7 +43,7 @@ class TheorySep : public Theory { // MISC ///////////////////////////////////////////////////////////////////////////// - private: + private: /** all lemmas sent */ NodeSet d_lemmas_produced_c; @@ -62,119 +62,137 @@ class TheorySep : public Theory { std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict, bool pol, bool hasPol, bool underSpatial ); - public: - + public: TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheorySep(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - std::string identify() const { return std::string("TheorySep"); } + std::string identify() const override { return std::string("TheorySep"); } ///////////////////////////////////////////////////////////////////////////// // PREPROCESSING ///////////////////////////////////////////////////////////////////////////// - public: - - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); + public: + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; + Node ppRewrite(TNode atom) override; - void ppNotifyAssertions(const std::vector& assertions); + void ppNotifyAssertions(const std::vector& assertions) override; ///////////////////////////////////////////////////////////////////////////// // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// - private: - + private: /** Should be called to propagate the literal. */ bool propagate(TNode literal); /** Explain why this literal is true by adding assumptions */ void explain(TNode literal, std::vector& assumptions); - public: + public: + void propagate(Effort e) override; + Node explain(TNode n) override; - void propagate(Effort e); - Node explain(TNode n); - - public: - - void addSharedTerm(TNode t); - EqualityStatus getEqualityStatus(TNode a, TNode b); - void computeCareGraph(); + public: + void addSharedTerm(TNode t) override; + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + void computeCareGraph() override; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - public: - bool collectModelInfo(TheoryModel* m) override; - void postProcessModel(TheoryModel* m); - - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// + public: + bool collectModelInfo(TheoryModel* m) override; + void postProcessModel(TheoryModel* m) override; - private: - public: + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// - Node getNextDecisionRequest( unsigned& priority ); + public: + Node getNextDecisionRequest(unsigned& priority) override; - void presolve(); - void shutdown() { } + void presolve() override; + void shutdown() override {} ///////////////////////////////////////////////////////////////////////////// // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// - public: - - void check(Effort e); + public: + void check(Effort e) override; - bool needsCheckLastEffort(); + bool needsCheckLastEffort() override; - private: - - // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module - class NotifyClass : public eq::EqualityEngineNotify { + private: + // NotifyClass: template helper class for d_equalityEngine - handles + // call-back from congruence closure module + class NotifyClass : public eq::EqualityEngineNotify + { TheorySep& d_sep; - public: - NotifyClass(TheorySep& sep): d_sep(sep) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl; + public: + NotifyClass(TheorySep& sep) : d_sep(sep) {} + + bool eqNotifyTriggerEquality(TNode equality, bool value) + { + Debug("sep::propagate") + << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " + << (value ? "true" : "false") << ")" << std::endl; // Just forward to sep - if (value) { + if (value) + { return d_sep.propagate(equality); - } else { + } + else + { return d_sep.propagate(equality.notNode()); } } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + bool eqNotifyTriggerPredicate(TNode predicate, bool value) + { Unreachable(); } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; - if (value) { + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) + { + Debug("sep::propagate") + << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 + << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) + { // Propagate equality between shared terms return d_sep.propagate(t1.eqNode(t2)); - } else { + } + else + { return d_sep.propagate(t1.eqNode(t2).notNode()); } return true; } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + void eqNotifyConstantTermMerge(TNode t1, TNode t2) + { + Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 + << ", " << t2 << ")" << std::endl; d_sep.conflict(t1, t2); } - void eqNotifyNewClass(TNode t) { } - void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); } - void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + void eqNotifyNewClass(TNode t) {} + void eqNotifyPreMerge(TNode t1, TNode t2) + { + d_sep.eqNotifyPreMerge(t1, t2); + } + void eqNotifyPostMerge(TNode t1, TNode t2) + { + d_sep.eqNotifyPostMerge(t1, t2); + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {} }; /** The notify class for d_equalityEngine */ @@ -289,7 +307,8 @@ class TheorySep : public Theory { void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ); Node mkUnion( TypeNode tn, std::vector< Node >& locs ); -private: + + private: Node getRepresentative( Node t ); bool hasTerm( Node a ); bool areEqual( Node a, Node b ); @@ -299,10 +318,9 @@ private: void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false ); void doPendingFacts(); -public: - eq::EqualityEngine* getEqualityEngine() { - return &d_equalityEngine; - } + + public: + eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } void initializeBounds(); };/* class TheorySep */ diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 1f0fbdd1f..a246903a1 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -46,36 +46,36 @@ public: ~TheorySets(); - void addSharedTerm(TNode); + void addSharedTerm(TNode) override; - void check(Effort); - - bool needsCheckLastEffort(); + void check(Effort) override; + + bool needsCheckLastEffort() override; bool collectModelInfo(TheoryModel* m) override; - void computeCareGraph(); + void computeCareGraph() override; + + Node explain(TNode) override; - Node explain(TNode); + EqualityStatus getEqualityStatus(TNode a, TNode b) override; - EqualityStatus getEqualityStatus(TNode a, TNode b); + Node getModelValue(TNode) override; - Node getModelValue(TNode); + std::string identify() const override { return "THEORY_SETS"; } - std::string identify() const { return "THEORY_SETS"; } + void preRegisterTerm(TNode node) override; - void preRegisterTerm(TNode node); + Node expandDefinition(LogicRequest& logicRequest, Node n) override; - Node expandDefinition(LogicRequest &logicRequest, Node n); + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + void presolve() override; - void presolve(); + void propagate(Effort) override; - void propagate(Effort); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - void setMasterEqualityEngine(eq::EqualityEngine* eq); - bool isEntailed( Node n, bool pol ); };/* class TheorySets */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index f07057444..e07cc6b5e 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -54,25 +54,28 @@ class TheoryStrings : public Theory { typedef context::CDHashMap NodeNodeMap; typedef context::CDHashSet NodeSet; -public: + public: TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryStrings(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - std::string identify() const { return std::string("TheoryStrings"); } + std::string identify() const override { return std::string("TheoryStrings"); } -public: - void propagate(Effort e); + public: + void propagate(Effort e) override; bool propagate(TNode literal); void explain( TNode literal, std::vector& assumptions ); - Node explain( TNode literal ); - eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; } - bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); - int getReduction( int effort, Node n, Node& nr ); - + Node explain(TNode literal) override; + eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } + bool getCurrentSubstitution(int effort, + std::vector& vars, + std::vector& subs, + std::map >& exp) override; + int getReduction(int effort, Node n, Node& nr) override; + // NotifyClass for equality engine class NotifyClass : public eq::EqualityEngineNotify { TheoryStrings& d_str; @@ -213,24 +216,24 @@ private: ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// -public: - bool collectModelInfo(TheoryModel* m) override; + public: + bool collectModelInfo(TheoryModel* m) override; - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// -public: - void presolve(); - void shutdown() { } + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// + public: + void presolve() override; + void shutdown() override {} ///////////////////////////////////////////////////////////////////////////// // MAIN SOLVER ///////////////////////////////////////////////////////////////////////////// -private: - void addSharedTerm(TNode n); - EqualityStatus getEqualityStatus(TNode a, TNode b); + private: + void addSharedTerm(TNode n) override; + EqualityStatus getEqualityStatus(TNode a, TNode b) override; -private: + private: class EqcInfo { public: EqcInfo( context::Context* c ); @@ -367,17 +370,18 @@ private: //cardinality check void checkCardinality(); -private: + private: void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); -public: + + public: /** preregister term */ - void preRegisterTerm(TNode n); + void preRegisterTerm(TNode n) override; /** Expand definition */ - Node expandDefinition(LogicRequest &logicRequest, Node n); + Node expandDefinition(LogicRequest& logicRequest, Node n) override; /** Check at effort e */ - void check(Effort e); + void check(Effort e) override; /** needs check last effort */ - bool needsCheckLastEffort(); + bool needsCheckLastEffort() override; /** Conflict when merging two constants */ void conflict(TNode a, TNode b); /** called when a new equivalence class is created */ @@ -389,39 +393,48 @@ public: /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); /** get preprocess */ - StringsPreprocess * getPreprocess() { return &d_preproc; } -protected: + StringsPreprocess* getPreprocess() { return &d_preproc; } + + protected: /** compute care graph */ - void computeCareGraph(); + void computeCareGraph() override; - //do pending merges + // do pending merges void assertPendingFact(Node atom, bool polarity, Node exp); void doPendingFacts(); void doPendingLemmas(); bool hasProcessed(); - void addToExplanation( Node a, Node b, std::vector< Node >& exp ); - void addToExplanation( Node lit, std::vector< Node >& exp ); - - //register term - void registerTerm( Node n, int effort ); - //send lemma - void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false ); - void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false ); - void sendLemma( Node ant, Node conc, const char * c ); - void sendInfer( Node eq_exp, Node eq, const char * c ); + void addToExplanation(Node a, Node b, std::vector& exp); + void addToExplanation(Node lit, std::vector& exp); + + // register term + void registerTerm(Node n, int effort); + // send lemma + void sendInference(std::vector& exp, + std::vector& exp_n, + Node eq, + const char* c, + bool asLemma = false); + void sendInference(std::vector& exp, + Node eq, + const char* c, + bool asLemma = false); + void sendLemma(Node ant, Node conc, const char* c); + void sendInfer(Node eq_exp, Node eq, const char* c); bool sendSplit(Node a, Node b, const char* c, bool preq = true); - void sendLengthLemma( Node n ); + void sendLengthLemma(Node n); /** mkConcat **/ - inline Node mkConcat( Node n1, Node n2 ); - inline Node mkConcat( Node n1, Node n2, Node n3 ); - inline Node mkConcat( const std::vector< Node >& c ); - inline Node mkLength( Node n ); - //mkSkolem - enum { + inline Node mkConcat(Node n1, Node n2); + inline Node mkConcat(Node n1, Node n2, Node n3); + inline Node mkConcat(const std::vector& c); + inline Node mkLength(Node n); + // mkSkolem + enum + { sk_id_c_spt, sk_id_vc_spt, sk_id_vc_bin_spt, - sk_id_v_spt, + sk_id_v_spt, sk_id_c_spt_rev, sk_id_vc_spt_rev, sk_id_vc_bin_spt_rev, @@ -434,30 +447,36 @@ protected: sk_id_deq_y, sk_id_deq_z, }; - std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache; - Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 ); - inline Node mkSkolemS(const char * c, int isLenSplit = 0); - void registerNonEmptySkolem( Node sk ); - //inline Node mkSkolemI(const char * c); + std::map > > d_skolem_cache; + Node mkSkolemCached( + Node a, Node b, int id, const char* c, int isLenSplit = 0); + inline Node mkSkolemS(const char* c, int isLenSplit = 0); + void registerNonEmptySkolem(Node sk); + // inline Node mkSkolemI(const char * c); /** mkExplain **/ - Node mkExplain( std::vector< Node >& a ); - Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); + Node mkExplain(std::vector& a); + Node mkExplain(std::vector& a, std::vector& an); /** mkAnd **/ - Node mkAnd( std::vector< Node >& a ); + Node mkAnd(std::vector& a); /** get concat vector */ - void getConcatVec( Node n, std::vector< Node >& c ); + void getConcatVec(Node n, std::vector& c); - //get equivalence classes - void getEquivalenceClasses( std::vector< Node >& eqcs ); + // get equivalence classes + void getEquivalenceClasses(std::vector& eqcs); - //separate into collections with equal length - void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); - void printConcat( std::vector< Node >& n, const char * c ); + // separate into collections with equal length + void separateByLength(std::vector& n, + std::vector >& col, + std::vector& lts); + void printConcat(std::vector& n, const char* c); - void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc ); + void inferSubstitutionProxyVars(Node n, + std::vector& vars, + std::vector& subs, + std::vector& unproc); // Symbolic Regular Expression -private: + private: // regular expression memberships NodeList d_regexp_memberships; NodeSet d_regexp_ucached; @@ -492,18 +511,20 @@ private: // Finite Model Finding -private: + private: NodeSet d_input_vars; context::CDO< Node > d_input_var_lsum; context::CDHashMap< int, Node > d_cardinality_lits; context::CDO< int > d_curr_cardinality; -public: + + public: //for finite model finding - Node getNextDecisionRequest( unsigned& priority ); - //ppRewrite - Node ppRewrite(TNode atom); -public: -/** statistics class */ + Node getNextDecisionRequest(unsigned& priority) override; + // ppRewrite + Node ppRewrite(TNode atom) override; + + public: + /** statistics class */ class Statistics { public: IntStat d_splits; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 934a09a8e..1f9fd92d4 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -162,13 +162,13 @@ public: */ Node getValue(TNode n, bool useDontCares = false) const; /** get comments */ - void getComments(std::ostream& out) const; + void getComments(std::ostream& out) const override; //---------------------------- separation logic /** set the heap and value sep.nil is equal to */ void setHeapModel(Node h, Node neq); /** get the heap and value sep.nil is equal to */ - bool getHeapModel(Expr& h, Expr& neq) const; + bool getHeapModel(Expr& h, Expr& neq) const override; //---------------------------- end separation logic /** get the representative set object */ @@ -176,11 +176,11 @@ public: /** get the representative set object (FIXME: remove this, see #1199) */ RepSet* getRepSetPtr() { return &d_rep_set; } /** return whether this node is a don't-care */ - bool isDontCare(Expr expr) const; + bool isDontCare(Expr expr) const override; /** get value function for Exprs. */ - Expr getValue( Expr expr ) const; + Expr getValue(Expr expr) const override; /** get cardinality for sort */ - Cardinality getCardinality( Type t ) const; + Cardinality getCardinality(Type t) const override; /** print representative debug function */ void printRepresentativeDebug( const char* c, Node r ); /** print representative function */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 269aa63db..6fde4a9af 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -234,34 +234,30 @@ public: ~TheoryUF(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); - void finishInit(); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; + void finishInit() override; - void check(Effort); - Node expandDefinition(LogicRequest &logicRequest, Node node); - void preRegisterTerm(TNode term); - Node explain(TNode n); + void check(Effort) override; + Node expandDefinition(LogicRequest& logicRequest, Node node) override; + void preRegisterTerm(TNode term) override; + Node explain(TNode n) override; bool collectModelInfo(TheoryModel* m) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned); - void presolve(); + void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + void presolve() override; - void addSharedTerm(TNode n); - void computeCareGraph(); + void addSharedTerm(TNode n) override; + void computeCareGraph() override; - void propagate(Effort effort); - Node getNextDecisionRequest( unsigned& priority ); + void propagate(Effort effort) override; + Node getNextDecisionRequest(unsigned& priority) override; - EqualityStatus getEqualityStatus(TNode a, TNode b); + EqualityStatus getEqualityStatus(TNode a, TNode b) override; - std::string identify() const { - return "THEORY_UF"; - } + std::string identify() const override { return "THEORY_UF"; } - eq::EqualityEngine* getEqualityEngine() { - return &d_equalityEngine; - } + eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } StrongSolverTheoryUF* getStrongSolver() { return d_thss; -- cgit v1.2.3