1 /********************* */
2 /*! \file candidate_generator.h
4 ** Original author: ajreynol
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Theory uf candidate generator
17 #include "cvc4_private.h"
19 #ifndef __CVC4__CANDIDATE_GENERATOR_H
20 #define __CVC4__CANDIDATE_GENERATOR_H
22 #include "theory/theory.h"
23 #include "theory/uf/equality_engine.h"
28 class QuantifiersEngine
;
32 /** base class for generating candidates for matching */
33 class CandidateGenerator
{
35 CandidateGenerator(){}
36 ~CandidateGenerator(){}
38 /** Get candidates functions. These set up a context to get all match candidates.
41 Node cand = cg->getNextCandidate();
43 }while( !cand.isNull() );
45 eqc is the equivalence class you are searching in
47 virtual void reset( Node eqc
) = 0;
48 virtual Node
getNextCandidate() = 0;
49 /** add candidate to list of nodes returned by this generator */
50 virtual void addCandidate( Node n
) {}
51 /** call this at the beginning of each instantiation round */
52 virtual void resetInstantiationRound() = 0;
54 /** legal candidate */
55 static bool isLegalCandidate( Node n
);
56 };/* class CandidateGenerator */
58 /** candidate generator queue (for manual candidate generation) */
59 class CandidateGeneratorQueue
: public CandidateGenerator
{
61 std::vector
< Node
> d_candidates
;
62 int d_candidate_index
;
64 CandidateGeneratorQueue() : d_candidate_index( 0 ){}
65 ~CandidateGeneratorQueue(){}
67 void addCandidate( Node n
);
69 void resetInstantiationRound(){}
70 void reset( Node eqc
);
71 Node
getNextCandidate();
72 };/* class CandidateGeneratorQueue */
74 class CandidateGeneratorQEDisequal
;
78 class CandidateGeneratorQE
: public CandidateGenerator
80 friend class CandidateGeneratorQEDisequal
;
82 //operator you are looking for
84 //instantiator pointer
85 QuantifiersEngine
* d_qe
;
86 //the equality class iterator
87 eq::EqClassIterator d_eqc
;
89 int d_term_iter_limit
;
93 CandidateGeneratorQE( QuantifiersEngine
* qe
, Node op
);
94 ~CandidateGeneratorQE(){}
96 void resetInstantiationRound();
97 void reset( Node eqc
);
98 Node
getNextCandidate();
103 class CandidateGeneratorQE
: public CandidateGenerator
105 friend class CandidateGeneratorQEDisequal
;
107 //operator you are looking for
109 //instantiator pointer
110 QuantifiersEngine
* d_qe
;
111 //the equality class iterator
112 std::vector
< Node
> d_eqc
;
114 int d_term_iter_limit
;
115 bool d_using_term_db
;
117 CandidateGeneratorQE( QuantifiersEngine
* qe
, Node op
);
118 ~CandidateGeneratorQE(){}
120 void resetInstantiationRound();
121 void reset( Node eqc
);
122 Node
getNextCandidate();
127 //class CandidateGeneratorQEDisequal : public CandidateGenerator
130 // //equivalence class
132 // //equivalence class info
133 // EqClassInfo* d_eci;
134 // //equivalence class iterator
135 // EqClassInfo::BoolMap::const_iterator d_eqci_iter;
136 // //instantiator pointer
137 // QuantifiersEngine* d_qe;
139 // CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc );
140 // ~CandidateGeneratorQEDisequal(){}
142 // void resetInstantiationRound();
143 // void reset( Node eqc ); //should be what you want to be disequal from
144 // Node getNextCandidate();
147 class CandidateGeneratorQELitEq
: public CandidateGenerator
150 //the equality classes iterator
151 eq::EqClassesIterator d_eq
;
152 //equality you are trying to match equalities for
153 Node d_match_pattern
;
154 //einstantiator pointer
155 QuantifiersEngine
* d_qe
;
157 CandidateGeneratorQELitEq( QuantifiersEngine
* qe
, Node mpat
);
158 ~CandidateGeneratorQELitEq(){}
160 void resetInstantiationRound();
161 void reset( Node eqc
);
162 Node
getNextCandidate();
165 class CandidateGeneratorQELitDeq
: public CandidateGenerator
168 //the equality class iterator for false
169 eq::EqClassIterator d_eqc_false
;
170 //equality you are trying to match disequalities for
171 Node d_match_pattern
;
172 //einstantiator pointer
173 QuantifiersEngine
* d_qe
;
175 CandidateGeneratorQELitDeq( QuantifiersEngine
* qe
, Node mpat
);
176 ~CandidateGeneratorQELitDeq(){}
178 void resetInstantiationRound();
179 void reset( Node eqc
);
180 Node
getNextCandidate();
183 }/* CVC4::theory::inst namespace */
184 }/* CVC4::theory namespace */
185 }/* CVC4 namespace */
187 #endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */