diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ambqi_builder.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/candidate_generator.h | 63 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.h | 430 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 42 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_equality_engine.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 1 |
14 files changed, 310 insertions, 301 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 89cd8b6a8..c451f0489 100644 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -89,11 +89,13 @@ private: bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ); public: AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ); - ~AbsMbqiBuilder() throw() {} + //process build model - bool processBuildModel(TheoryModel* m); + bool processBuildModel(TheoryModel* m) override; //do exhaustive instantiation - int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ); + int doExhaustiveInstantiation(FirstOrderModel* fm, + Node q, + int effort) override; }; } diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index dd71ef56e..4662d7c4c 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -61,25 +61,26 @@ public: /** candidate generator queue (for manual candidate generation) */ class CandidateGeneratorQueue : public CandidateGenerator { -private: + private: std::vector< Node > d_candidates; int d_candidate_index; -public: + + public: CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){} - ~CandidateGeneratorQueue() throw() {} - void addCandidate( Node n ); + void addCandidate(Node n) override; - void resetInstantiationRound(){} - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override {} + void reset(Node eqc) override; + Node getNextCandidate() override; };/* class CandidateGeneratorQueue */ //the default generator class CandidateGeneratorQE : public CandidateGenerator { friend class CandidateGeneratorQEDisequal; -private: + + private: //operator you are looking for Node d_op; //the equality class iterator @@ -102,56 +103,56 @@ private: bool isLegalOpCandidate( Node n ); Node d_n; std::map< Node, bool > d_exclude_eqc; -public: + + public: CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ); - ~CandidateGeneratorQE() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; void excludeEqc( Node r ) { d_exclude_eqc[r] = true; } bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); } }; class CandidateGeneratorQELitEq : public CandidateGenerator { -private: + private: //the equality classes iterator eq::EqClassesIterator d_eq; //equality you are trying to match equalities for Node d_match_pattern; Node d_match_gterm; bool d_do_mgt; -public: + + public: CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQELitEq() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; }; class CandidateGeneratorQELitDeq : public CandidateGenerator { -private: + private: //the equality class iterator for false eq::EqClassIterator d_eqc_false; //equality you are trying to match disequalities for Node d_match_pattern; //type of disequality TypeNode d_match_pattern_type; -public: + + public: CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQELitDeq() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; }; class CandidateGeneratorQEAll : public CandidateGenerator { -private: + private: //the equality classes iterator eq::EqClassesIterator d_eq; //equality you are trying to match equalities for @@ -162,13 +163,13 @@ private: unsigned d_index; //first time bool d_firstTime; -public: + + public: CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); - ~CandidateGeneratorQEAll() throw() {} - void resetInstantiationRound(); - void reset( Node eqc ); - Node getNextCandidate(); + void resetInstantiationRound() override; + void reset(Node eqc) override; + Node getNextCandidate() override; }; }/* CVC4::theory::inst namespace */ diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index fa74795c3..85a7d3eb4 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -399,7 +399,7 @@ private: //information about ground equivalence classes unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); public: ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ); - ~ConjectureGenerator() throw() {} + /* needs check */ bool needsCheck( Theory::Effort e ); /* reset at a round */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 6749a8c0d..e7070b469 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -836,7 +836,8 @@ FirstOrderModel(qe, c, name){ } -FirstOrderModelFmc::~FirstOrderModelFmc() throw() { +FirstOrderModelFmc::~FirstOrderModelFmc() +{ for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) { delete (*i).second; } @@ -1004,7 +1005,8 @@ FirstOrderModel(qe, c, name) { } -FirstOrderModelAbs::~FirstOrderModelAbs() throw() { +FirstOrderModelAbs::~FirstOrderModelAbs() +{ for(std::map<Node, AbsDef*>::iterator i = d_models.begin(); i != d_models.end(); ++i) { delete (*i).second; } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 57582a856..0c4b6b7a4 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -93,7 +93,7 @@ class FirstOrderModel : public TheoryModel { public: FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name); - virtual ~FirstOrderModel() throw() {} + virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; } virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; } @@ -214,7 +214,7 @@ private: //the following functions are for evaluating quantifier bodies public: FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); - ~FirstOrderModelIG() throw() {} + FirstOrderModelIG * asFirstOrderModelIG() { return this; } // initialize the model void processInitialize( bool ispre ); @@ -257,7 +257,7 @@ private: void processInitializeModelForTerm(Node n); public: FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); - virtual ~FirstOrderModelFmc() throw(); + ~FirstOrderModelFmc() override; FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } // initialize the model void processInitialize( bool ispre ); @@ -277,24 +277,26 @@ class AbsDef; class FirstOrderModelAbs : public FirstOrderModel { -public: + public: std::map< Node, AbsDef * > d_models; std::map< Node, bool > d_models_valid; std::map< TNode, unsigned > d_rep_id; std::map< TypeNode, unsigned > d_domain; std::map< Node, std::vector< int > > d_var_order; std::map< Node, std::map< int, int > > d_var_index; -private: + + private: /** get current model value */ - void processInitializeModelForTerm(Node n); - void processInitializeQuantifier( Node q ); + void processInitializeModelForTerm(Node n) override; + void processInitializeQuantifier(Node q) override; void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ); TNode getUsedRepresentative( TNode n ); -public: + + public: FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); - ~FirstOrderModelAbs() throw(); - FirstOrderModelAbs * asFirstOrderModelAbs() { return this; } - void processInitialize( bool ispre ); + ~FirstOrderModelAbs() override; + FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; } + void processInitialize(bool ispre) override; unsigned getRepresentativeId( TNode n ); bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); } Node getFunctionValue(Node op, const char* argPrefix ); diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index c5d005969..f6d16dc03 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -134,7 +134,6 @@ private: Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: FullModelChecker( context::Context* c, QuantifiersEngine* qe ); - ~FullModelChecker() throw() {} void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 884ed29f5..46ae8aa84 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -59,7 +59,8 @@ InstMatchGenerator::InstMatchGenerator() { d_independent_gen = false; } -InstMatchGenerator::~InstMatchGenerator() throw() { +InstMatchGenerator::~InstMatchGenerator() +{ for( unsigned i=0; i<d_children.size(); i++ ){ delete d_children[i]; } @@ -692,10 +693,6 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vecto } } -InstMatchGeneratorMultiLinear::~InstMatchGeneratorMultiLinear() throw() { - -} - int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){ for( unsigned i=0; i<d_children.size(); i++ ){ if( !d_children[i]->reset( Node::null(), qe ) ){ @@ -814,7 +811,8 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q, } } -InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() { +InstMatchGeneratorMulti::~InstMatchGeneratorMulti() +{ for( unsigned i=0; i<d_children.size(); i++ ){ delete d_children[i]; } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 95faf0279..fc913c7cf 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -191,231 +191,231 @@ class CandidateGenerator; * ground terms not in the equivalence class of b. */ class InstMatchGenerator : public IMGenerator { -public: - /** destructor */ - virtual ~InstMatchGenerator() throw(); + public: + /** destructor */ + ~InstMatchGenerator() override; - /** Reset instantiation round. */ - void resetInstantiationRound(QuantifiersEngine* qe) override; - /** Reset. */ - bool reset(Node eqc, QuantifiersEngine* qe) override; - /** Get the next match. */ - int getNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent) override; - /** Add instantiations. */ - int addInstantiations(Node q, - QuantifiersEngine* qe, - Trigger* tparent) override; + /** Reset instantiation round. */ + void resetInstantiationRound(QuantifiersEngine* qe) override; + /** Reset. */ + bool reset(Node eqc, QuantifiersEngine* qe) override; + /** Get the next match. */ + int getNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent) override; + /** Add instantiations. */ + int addInstantiations(Node q, + QuantifiersEngine* qe, + Trigger* tparent) override; - /** set active add flag (true by default) - * - * If active add is true, we call sendInstantiation in calls to getNextMatch, - * instead of returning the match. This is necessary so that we can ensure - * policies that are dependent upon knowing when instantiations are - * successfully added to the output channel through - * Instantiate::addInstantiation(...). - */ - void setActiveAdd(bool val); - /** Get active score for this inst match generator - * - * See Trigger::getActiveScore for details. + /** set active add flag (true by default) + * + * If active add is true, we call sendInstantiation in calls to getNextMatch, + * instead of returning the match. This is necessary so that we can ensure + * policies that are dependent upon knowing when instantiations are + * successfully added to the output channel through + * Instantiate::addInstantiation(...). */ - int getActiveScore(QuantifiersEngine* qe); - /** exclude match - * - * Exclude matching d_match_pattern with Node n on subsequent calls to - * getNextMatch. + void setActiveAdd(bool val); + /** Get active score for this inst match generator + * + * See Trigger::getActiveScore for details. + */ + int getActiveScore(QuantifiersEngine* qe); + /** exclude match + * + * Exclude matching d_match_pattern with Node n on subsequent calls to + * getNextMatch. + */ + void excludeMatch(Node n) { d_curr_exclude_match[n] = true; } + /** Get current match. + * Returns the term we are currently matching. + */ + Node getCurrentMatch() { return d_curr_matched; } + /** set that this match generator is independent + * + * A match generator is indepndent when this generator fails to produce a + * match in a call to getNextMatch, the overall matching fails. */ - void excludeMatch(Node n) { d_curr_exclude_match[n] = true; } - /** Get current match. - * Returns the term we are currently matching. + void setIndependent() { d_independent_gen = true; } + //-------------------------------construction of inst match generators + /** mkInstMatchGenerator for single triggers, calls the method below */ + static InstMatchGenerator* mkInstMatchGenerator(Node q, + Node pat, + QuantifiersEngine* qe); + /** mkInstMatchGenerator for the multi trigger case + * + * This linked list of InstMatchGenerator classes with one + * InstMatchGeneratorMultiLinear at the head and a list of trailing + * InstMatchGenerators corresponding to each unique subterm of pats with + * free variables. */ - Node getCurrentMatch() { return d_curr_matched; } - /** set that this match generator is independent + static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q, + std::vector<Node>& pats, + QuantifiersEngine* qe); + /** mkInstMatchGenerator * - * A match generator is indepndent when this generator fails to produce a - * match in a call to getNextMatch, the overall matching fails. - */ - void setIndependent() { d_independent_gen = true; } - //-------------------------------construction of inst match generators - /** mkInstMatchGenerator for single triggers, calls the method below */ - static InstMatchGenerator* mkInstMatchGenerator(Node q, - Node pat, - QuantifiersEngine* qe); - /** mkInstMatchGenerator for the multi trigger case - * - * This linked list of InstMatchGenerator classes with one - * InstMatchGeneratorMultiLinear at the head and a list of trailing - * InstMatchGenerators corresponding to each unique subterm of pats with - * free variables. - */ - static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q, - std::vector<Node>& pats, - QuantifiersEngine* qe); - /** mkInstMatchGenerator - * - * This generates a linked list of InstMatchGenerators for each unique - * subterm of pats with free variables. - * - * q is the quantified formula associated with the generator we are making - * pats is a set of terms we are making InstMatchGenerator nodes for - * qe is a pointer to the quantifiers engine (used for querying necessary - * information during initialization) pat_map_init maps from terms to - * generators we have already made for them. - * - * It calls initialize(...) for all InstMatchGenerators generated by this call. - */ - static InstMatchGenerator* mkInstMatchGenerator( - Node q, - std::vector<Node>& pats, - QuantifiersEngine* qe, - std::map<Node, InstMatchGenerator*>& pat_map_init); - //-------------------------------end construction of inst match generators - -protected: - /** constructors + * This generates a linked list of InstMatchGenerators for each unique + * subterm of pats with free variables. * - * These are intentionally private, and are called during linked list - * construction in mkInstMatchGenerator. - */ - InstMatchGenerator(Node pat); - InstMatchGenerator(); - /** The pattern we are producing matches for. + * q is the quantified formula associated with the generator we are making + * pats is a set of terms we are making InstMatchGenerator nodes for + * qe is a pointer to the quantifiers engine (used for querying necessary + * information during initialization) pat_map_init maps from terms to + * generators we have already made for them. * - * This term and d_match_pattern can be different since this - * term may involve information regarding phase and (dis)equality entailment, - * or other special cases of Triggers. - * - * For example, for the trigger for P( x ) = false, which matches P( x ) with - * P( t ) in the equivalence class of false, - * P( x ) = false is d_pattern - * P( x ) is d_match_pattern - * Another example, for pure theory triggers like head( x ), we have - * head( x ) is d_pattern - * x is d_match_pattern - * since head( x ) can match any (List) datatype term x. - * - * If null, this is a multi trigger that is merging matches from d_children, - * which is used in InstMatchGeneratorMulti. - */ - Node d_pattern; - /** The match pattern - * This is the term that is matched against ground terms, - * see examples above. - */ - Node d_match_pattern; - /** The current term we are matching. */ - Node d_curr_matched; - /** do we need to call reset on this generator? */ - bool d_needsReset; - /** candidate generator - * This is the back-end utility for InstMatchGenerator. - * It generates a stream of candidate terms to match against d_match_pattern - * below, dependending upon what kind of term we are matching - * (e.g. a matchable term, a variable, a relation, etc.). + * It calls initialize(...) for all InstMatchGenerators generated by this call. */ - CandidateGenerator* d_cg; - /** children generators - * These match generators correspond to the children of the term - * we are matching with this generator. - * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ] - * in the example (EX1) above. - */ - std::vector<InstMatchGenerator*> d_children; - /** for each child, the index in the term - * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ] - * in the example (EX1) above, indicating it is the 2nd child - * of the term. + static InstMatchGenerator* mkInstMatchGenerator( + Node q, + std::vector<Node>& pats, + QuantifiersEngine* qe, + std::map<Node, InstMatchGenerator*>& pat_map_init); + //-------------------------------end construction of inst match generators + + protected: + /** constructors + * + * These are intentionally private, and are called during linked list + * construction in mkInstMatchGenerator. */ - std::vector<int> d_children_index; - /** children types + InstMatchGenerator(Node pat); + InstMatchGenerator(); + /** The pattern we are producing matches for. + * + * This term and d_match_pattern can be different since this + * term may involve information regarding phase and (dis)equality entailment, + * or other special cases of Triggers. * - * If d_match_pattern is an instantiation constant, then this is a singleton - * vector containing the variable number of the d_match_pattern itself. - * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each - * index i, d_children[i] stores the type of node ti is, where: - * >= 0 : variable (indicates its number), - * -1 : ground term, - * -2 : child term. - */ - std::vector<int> d_children_types; - /** The next generator in the linked list - * that this generator is a part of. - */ - InstMatchGenerator* d_next; - /** The equivalence class we are currently matching in. */ - Node d_eq_class; - /** If non-null, then this is a relational trigger of the form x ~ - * d_eq_class_rel. */ - Node d_eq_class_rel; - /** Excluded matches - * Stores the terms we are not allowed to match. - * These can for instance be specified by the smt2 - * extended syntax (! ... :no-pattern). - */ - std::map<Node, bool> d_curr_exclude_match; - /** Current first candidate - * Used in a key fail-quickly optimization which generates - * the first candidate term to match during reset(). - */ - Node d_curr_first_candidate; - /** Indepdendent generate - * If this flag is true, failures to match should be cached. - */ - bool d_independent_gen; - /** active add flag, described above. */ - bool d_active_add; - /** cached value of d_match_pattern.getType() */ - TypeNode d_match_pattern_type; - /** the match operator for d_match_pattern + * For example, for the trigger for P( x ) = false, which matches P( x ) with + * P( t ) in the equivalence class of false, + * P( x ) = false is d_pattern + * P( x ) is d_match_pattern + * Another example, for pure theory triggers like head( x ), we have + * head( x ) is d_pattern + * x is d_match_pattern + * since head( x ) can match any (List) datatype term x. * - * See TermDatabase::getMatchOperator for details on match operators. + * If null, this is a multi trigger that is merging matches from d_children, + * which is used in InstMatchGeneratorMulti. */ - Node d_match_pattern_op; - /** get the match against ground term or formula t. - * - * d_match_pattern and t should have the same shape, that is, - * their match operator (see TermDatabase::getMatchOperator) is the same. - * only valid for use where !d_match_pattern.isNull(). + Node d_pattern; + /** The match pattern + * This is the term that is matched against ground terms, + * see examples above. + */ + Node d_match_pattern; + /** The current term we are matching. */ + Node d_curr_matched; + /** do we need to call reset on this generator? */ + bool d_needsReset; + /** candidate generator + * This is the back-end utility for InstMatchGenerator. + * It generates a stream of candidate terms to match against d_match_pattern + * below, dependending upon what kind of term we are matching + * (e.g. a matchable term, a variable, a relation, etc.). + */ + CandidateGenerator* d_cg; + /** children generators + * These match generators correspond to the children of the term + * we are matching with this generator. + * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ] + * in the example (EX1) above. + */ + std::vector<InstMatchGenerator*> d_children; + /** for each child, the index in the term + * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ] + * in the example (EX1) above, indicating it is the 2nd child + * of the term. + */ + std::vector<int> d_children_index; + /** children types + * + * If d_match_pattern is an instantiation constant, then this is a singleton + * vector containing the variable number of the d_match_pattern itself. + * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each + * index i, d_children[i] stores the type of node ti is, where: + * >= 0 : variable (indicates its number), + * -1 : ground term, + * -2 : child term. + */ + std::vector<int> d_children_types; + /** The next generator in the linked list + * that this generator is a part of. + */ + InstMatchGenerator* d_next; + /** The equivalence class we are currently matching in. */ + Node d_eq_class; + /** If non-null, then this is a relational trigger of the form x ~ + * d_eq_class_rel. */ + Node d_eq_class_rel; + /** Excluded matches + * Stores the terms we are not allowed to match. + * These can for instance be specified by the smt2 + * extended syntax (! ... :no-pattern). */ - int getMatch( - Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent); - /** Initialize this generator. - * - * q is the quantified formula associated with this generator. - * - * This constructs the appropriate information about what - * patterns we are matching and children generators. - * - * It may construct new (child) generators needed to implement - * the matching algorithm for this term. For each new generator - * constructed in this way, it adds them to gens. + std::map<Node, bool> d_curr_exclude_match; + /** Current first candidate + * Used in a key fail-quickly optimization which generates + * the first candidate term to match during reset(). */ - void initialize(Node q, - QuantifiersEngine* qe, - std::vector<InstMatchGenerator*>& gens); - /** Continue next match - * - * This is called during getNextMatch when the current generator in the linked - * list succesfully satisfies its matching constraint. This function either - * calls getNextMatch of the next element in the linked list, or finalizes the - * match (calling sendInstantiation(...) if active add is true, or returning a - * value >0 if active add is false). Its return value has the same semantics - * as getNextMatch. - */ - int continueNextMatch(Node q, - InstMatch& m, - QuantifiersEngine* qe, - Trigger* tparent); - /** Get inst match generator - * - * Gets the InstMatchGenerator that implements the - * appropriate matching algorithm for n within q - * within a linked list of InstMatchGenerators. + Node d_curr_first_candidate; + /** Indepdendent generate + * If this flag is true, failures to match should be cached. */ - static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); + bool d_independent_gen; + /** active add flag, described above. */ + bool d_active_add; + /** cached value of d_match_pattern.getType() */ + TypeNode d_match_pattern_type; + /** the match operator for d_match_pattern + * + * See TermDatabase::getMatchOperator for details on match operators. + */ + Node d_match_pattern_op; + /** get the match against ground term or formula t. + * + * d_match_pattern and t should have the same shape, that is, + * their match operator (see TermDatabase::getMatchOperator) is the same. + * only valid for use where !d_match_pattern.isNull(). + */ + int getMatch( + Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent); + /** Initialize this generator. + * + * q is the quantified formula associated with this generator. + * + * This constructs the appropriate information about what + * patterns we are matching and children generators. + * + * It may construct new (child) generators needed to implement + * the matching algorithm for this term. For each new generator + * constructed in this way, it adds them to gens. + */ + void initialize(Node q, + QuantifiersEngine* qe, + std::vector<InstMatchGenerator*>& gens); + /** Continue next match + * + * This is called during getNextMatch when the current generator in the linked + * list succesfully satisfies its matching constraint. This function either + * calls getNextMatch of the next element in the linked list, or finalizes the + * match (calling sendInstantiation(...) if active add is true, or returning a + * value >0 if active add is false). Its return value has the same semantics + * as getNextMatch. + */ + int continueNextMatch(Node q, + InstMatch& m, + QuantifiersEngine* qe, + Trigger* tparent); + /** Get inst match generator + * + * Gets the InstMatchGenerator that implements the + * appropriate matching algorithm for n within q + * within a linked list of InstMatchGenerators. + */ + static InstMatchGenerator* getInstMatchGenerator(Node q, Node n); };/* class InstMatchGenerator */ /** match generator for Boolean term ITEs @@ -424,7 +424,7 @@ protected: class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { public: VarMatchGeneratorBooleanTerm( Node var, Node comp ); - virtual ~VarMatchGeneratorBooleanTerm() throw() {} + /** Reset */ bool reset(Node eqc, QuantifiersEngine* qe) override { @@ -451,7 +451,7 @@ public: class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: VarMatchGeneratorTermSubs( Node var, Node subs ); - virtual ~VarMatchGeneratorTermSubs() throw() {} + /** Reset */ bool reset(Node eqc, QuantifiersEngine* qe) override { @@ -515,9 +515,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator { friend class InstMatchGenerator; public: - /** destructor */ - virtual ~InstMatchGeneratorMultiLinear() throw(); - /** Reset. */ bool reset(Node eqc, QuantifiersEngine* qe) override; /** Get the next match. */ @@ -552,7 +549,7 @@ class InstMatchGeneratorMulti : public IMGenerator { std::vector<Node>& pats, QuantifiersEngine* qe); /** destructor */ - virtual ~InstMatchGeneratorMulti() throw(); + ~InstMatchGeneratorMulti() override; /** Reset instantiation round. */ void resetInstantiationRound(QuantifiersEngine* qe) override; @@ -641,8 +638,7 @@ class InstMatchGeneratorSimple : public IMGenerator { public: /** constructors */ InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe); - /** destructor */ - ~InstMatchGeneratorSimple() throw() {} + /** Reset instantiation round. */ void resetInstantiationRound(QuantifiersEngine* qe) override; /** Add instantiations. */ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index bd2b8e78e..70dc9c4e9 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -48,8 +48,6 @@ d_nested_qe_waitlist_proc( qe->getUserContext() ) d_qid_count = 0; } -InstStrategyCbqi::~InstStrategyCbqi() throw(){} - bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } @@ -673,7 +671,8 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) d_check_vts_lemma_lc = false; } -InstStrategyCegqi::~InstStrategyCegqi() throw () { +InstStrategyCegqi::~InstStrategyCegqi() +{ delete d_out; for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(), diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 0b23de10d..c2520a973 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -35,7 +35,8 @@ namespace quantifiers { class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; -protected: + + protected: bool d_cbqi_set_quant_inactive; bool d_incomplete_check; /** whether we have added cbqi lemma */ @@ -64,7 +65,8 @@ protected: /** process functions */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; virtual void process( Node q, Theory::Effort effort, int e ) = 0; -protected: + + protected: //for identification uint64_t d_qid_count; //nested qe map @@ -90,12 +92,14 @@ protected: NodeIntMap d_nested_qe_waitlist_size; NodeIntMap d_nested_qe_waitlist_proc; std::map< Node, std::vector< Node > > d_nested_qe_waitlist; -public: + + public: //do nested quantifier elimination Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ); -public: + + public: InstStrategyCbqi( QuantifiersEngine * qe ); - ~InstStrategyCbqi() throw(); + /** whether to do CBQI for quantifier q */ bool doCbqi( Node q ); /** process functions */ @@ -138,7 +142,7 @@ protected: void registerCounterexampleLemma( Node q, Node lem ); public: InstStrategyCegqi( QuantifiersEngine * qe ); - ~InstStrategyCegqi() throw(); + ~InstStrategyCegqi() override; bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 73e2937ab..511aebf3b 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -38,7 +38,7 @@ protected: unsigned d_triedLemmas; public: QModelBuilder( context::Context* c, QuantifiersEngine* qe ); - virtual ~QModelBuilder() throw() {} + //do exhaustive instantiation // 0 : failed, but resorting to true exhaustive instantiation may work // >0 : success @@ -77,7 +77,8 @@ public: class QModelBuilderIG : public QModelBuilder { typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; -protected: + + protected: BoolMap d_basisNoMatch; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; @@ -87,7 +88,8 @@ protected: bool d_didInstGen; /** process build model */ virtual bool processBuildModel( TheoryModel* m ); -protected: + + protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; //initialize quantifiers, return number of lemmas produced @@ -100,20 +102,23 @@ protected: virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0; //theory-specific build models virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0; -protected: + + protected: //map from quantifiers to if are SAT //std::map< Node, bool > d_quant_sat; //which quantifiers have been initialized std::map< Node, bool > d_quant_basis_match_added; //map from quantifiers to model basis match std::map< Node, InstMatch > d_quant_basis_match; -protected: //helper functions + + protected: // helper functions /** term has constant definition */ bool hasConstantDefinition( Node n ); -public: + + public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); - virtual ~QModelBuilderIG() throw() {} -public: + + public: /** statistics class */ class Statistics { public: @@ -152,8 +157,8 @@ public: class QModelBuilderDefault : public QModelBuilderIG { -private: ///information for (old) InstGen - //map from quantifiers to their selection literals + private: /// information for (old) InstGen + // map from quantifiers to their selection literals std::map< Node, Node > d_quant_selection_lit; std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates; //map from quantifiers to their selection literal terms @@ -164,20 +169,23 @@ private: ///information for (old) InstGen std::map< Node, std::vector< Node > > d_op_selection_terms; //get selection score int getSelectionScore( std::vector< Node >& uf_terms ); -protected: + + protected: //reset - void reset( FirstOrderModel* fm ); + void reset(FirstOrderModel* fm) override; //analyze quantifier - void analyzeQuantifier( FirstOrderModel* fm, Node f ); + void analyzeQuantifier(FirstOrderModel* fm, Node f) override; //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen( FirstOrderModel* fm, Node f ); + int doInstGen(FirstOrderModel* fm, Node f) override; //theory-specific build models void constructModelUf( FirstOrderModel* fm, Node op ); -protected: + + protected: std::map< Node, QuantPhaseReq > d_phase_reqs; -public: + + public: QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} - ~QModelBuilderDefault() throw() {} + //options bool optReconsiderFuncConstants() { return true; } //has inst gen diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index f4d0e8e43..3448e967b 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -236,7 +236,7 @@ private: //for equivalence classes bool areMatchDisequal( TNode n1, TNode n2 ); public: QuantConflictFind( QuantifiersEngine * qe, context::Context* c ); - ~QuantConflictFind() throw() {} + /** register quantifier */ void registerQuantifier( Node q ); public: diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h index d2e9ec77b..47adddd9e 100644 --- a/src/theory/quantifiers/quant_equality_engine.h +++ b/src/theory/quantifiers/quant_equality_engine.h @@ -73,7 +73,6 @@ private: TNode getUnivRepresentativeInternal( TNode n ); public: QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ); - virtual ~QuantEqualityEngine() throw (){} /* whether this module needs to check this round */ bool needsCheck( Theory::Effort e ); diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index d56e7c730..cfca96259 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -49,7 +49,6 @@ private: int checkRewriteRule( Node f, Theory::Effort e ); public: RewriteEngine( context::Context* c, QuantifiersEngine* qe ); - ~RewriteEngine() throw() {} bool needsCheck( Theory::Effort e ); void check(Theory::Effort e, QEffort quant_e); |