diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:30 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:36 -0500 |
commit | f65b945119341ae8afa69bd0b7dc005c9fcc768b (patch) | |
tree | c264125578d3b8edd752740701789f7b1e4e26bb /src/theory/quantifiers/candidate_generator.h | |
parent | 53c301aa808218abe725014e01bddc19fe11a116 (diff) |
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
Diffstat (limited to 'src/theory/quantifiers/candidate_generator.h')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.h | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 18ef6a086..4fc6969fc 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -33,8 +33,10 @@ namespace inst { /** base class for generating candidates for matching */ class CandidateGenerator { +protected: + QuantifiersEngine* d_qe; public: - CandidateGenerator(){} + CandidateGenerator( QuantifiersEngine* qe ) : d_qe( qe ){} virtual ~CandidateGenerator(){} /** Get candidates functions. These set up a context to get all match candidates. @@ -54,7 +56,7 @@ public: virtual void resetInstantiationRound() = 0; public: /** legal candidate */ - static bool isLegalCandidate( Node n ); + bool isLegalCandidate( Node n ); };/* class CandidateGenerator */ /** candidate generator queue (for manual candidate generation) */ @@ -63,7 +65,7 @@ private: std::vector< Node > d_candidates; int d_candidate_index; public: - CandidateGeneratorQueue() : d_candidate_index( 0 ){} + CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){} ~CandidateGeneratorQueue() throw() {} void addCandidate( Node n ); @@ -80,8 +82,6 @@ class CandidateGeneratorQE : public CandidateGenerator private: //operator you are looking for Node d_op; - //instantiator pointer - QuantifiersEngine* d_qe; //the equality class iterator unsigned d_op_arity; std::vector< quantifiers::TermArgTrie* > d_tindex; @@ -122,8 +122,6 @@ private: Node d_match_pattern; Node d_match_gterm; bool d_do_mgt; - //einstantiator pointer - QuantifiersEngine* d_qe; public: CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); ~CandidateGeneratorQELitEq() throw() {} @@ -142,8 +140,6 @@ private: Node d_match_pattern; //type of disequality TypeNode d_match_pattern_type; - //einstantiator pointer - QuantifiersEngine* d_qe; public: CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); ~CandidateGeneratorQELitDeq() throw() {} @@ -161,8 +157,6 @@ private: //equality you are trying to match equalities for Node d_match_pattern; TypeNode d_match_pattern_type; - //einstantiator pointer - QuantifiersEngine* d_qe; // quantifier/index for the variable we are matching Node d_f; unsigned d_index; |