1 /********************* */
2 /*! \file candidate_generator.h
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Theory uf candidate generator
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
18 #define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
20 #include "theory/theory.h"
21 #include "theory/uf/equality_engine.h"
26 class QuantifiersEngine
;
30 /** base class for generating candidates for matching */
31 class CandidateGenerator
{
33 CandidateGenerator(){}
34 ~CandidateGenerator(){}
36 /** Get candidates functions. These set up a context to get all match candidates.
39 Node cand = cg->getNextCandidate();
41 }while( !cand.isNull() );
43 eqc is the equivalence class you are searching in
45 virtual void reset( Node eqc
) = 0;
46 virtual Node
getNextCandidate() = 0;
47 /** add candidate to list of nodes returned by this generator */
48 virtual void addCandidate( Node n
) {}
49 /** call this at the beginning of each instantiation round */
50 virtual void resetInstantiationRound() = 0;
52 /** legal candidate */
53 static bool isLegalCandidate( Node n
);
54 };/* class CandidateGenerator */
56 /** candidate generator queue (for manual candidate generation) */
57 class CandidateGeneratorQueue
: public CandidateGenerator
{
59 std::vector
< Node
> d_candidates
;
60 int d_candidate_index
;
62 CandidateGeneratorQueue() : d_candidate_index( 0 ){}
63 ~CandidateGeneratorQueue(){}
65 void addCandidate( Node n
);
67 void resetInstantiationRound(){}
68 void reset( Node eqc
);
69 Node
getNextCandidate();
70 };/* class CandidateGeneratorQueue */
72 //the default generator
73 class CandidateGeneratorQE
: public CandidateGenerator
75 friend class CandidateGeneratorQEDisequal
;
77 //operator you are looking for
79 //instantiator pointer
80 QuantifiersEngine
* d_qe
;
81 //the equality class iterator
82 eq::EqClassIterator d_eqc_iter
;
83 //std::vector< Node > d_eqc;
85 int d_term_iter_limit
;
93 bool isLegalOpCandidate( Node n
);
96 CandidateGeneratorQE( QuantifiersEngine
* qe
, Node op
);
97 ~CandidateGeneratorQE(){}
99 void resetInstantiationRound();
100 void reset( Node eqc
);
101 Node
getNextCandidate();
104 class CandidateGeneratorQELitEq
: public CandidateGenerator
107 //the equality classes iterator
108 eq::EqClassesIterator d_eq
;
109 //equality you are trying to match equalities for
110 Node d_match_pattern
;
111 //einstantiator pointer
112 QuantifiersEngine
* d_qe
;
114 CandidateGeneratorQELitEq( QuantifiersEngine
* qe
, Node mpat
);
115 ~CandidateGeneratorQELitEq(){}
117 void resetInstantiationRound();
118 void reset( Node eqc
);
119 Node
getNextCandidate();
122 class CandidateGeneratorQELitDeq
: public CandidateGenerator
125 //the equality class iterator for false
126 eq::EqClassIterator d_eqc_false
;
127 //equality you are trying to match disequalities for
128 Node d_match_pattern
;
129 //einstantiator pointer
130 QuantifiersEngine
* d_qe
;
132 CandidateGeneratorQELitDeq( QuantifiersEngine
* qe
, Node mpat
);
133 ~CandidateGeneratorQELitDeq(){}
135 void resetInstantiationRound();
136 void reset( Node eqc
);
137 Node
getNextCandidate();
140 class CandidateGeneratorQEAll
: public CandidateGenerator
143 //the equality classes iterator
144 eq::EqClassesIterator d_eq
;
145 //equality you are trying to match equalities for
146 Node d_match_pattern
;
147 TypeNode d_match_pattern_type
;
148 //einstantiator pointer
149 QuantifiersEngine
* d_qe
;
150 // quantifier/index for the variable we are matching
154 CandidateGeneratorQEAll( QuantifiersEngine
* qe
, Node mpat
);
155 ~CandidateGeneratorQEAll(){}
157 void resetInstantiationRound();
158 void reset( Node eqc
);
159 Node
getNextCandidate();
162 }/* CVC4::theory::inst namespace */
163 }/* CVC4::theory namespace */
164 }/* CVC4 namespace */
166 #endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */