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.

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;