1 /********************* */
2 /*! \file rr_candidate_generator.cpp
4 ** Original author: ajreynol
5 ** Major contributors: bobot
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 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 Implementation of rr candidate generator class
17 #include "theory/rewriterules/rr_candidate_generator.h"
18 #include "theory/theory_engine.h"
19 #include "theory/uf/theory_uf.h"
20 #include "theory/quantifiers/term_database.h"
24 using namespace CVC4::kind
;
25 using namespace CVC4::context
;
26 using namespace CVC4::theory
;
27 using namespace CVC4::theory::rrinst
;
29 GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine
* qe
){
30 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
31 if(qe
->getInstantiator(i
) != NULL
)
32 d_can_gen
[i
] = qe
->getInstantiator(i
)->getRRCanGenClasses();
33 else d_can_gen
[i
] = NULL
;
37 GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){
38 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
43 void GenericCandidateGeneratorClasses::resetInstantiationRound(){
44 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
45 if(d_can_gen
[i
] != NULL
) d_can_gen
[i
]->resetInstantiationRound();
47 d_can_gen_id
=THEORY_FIRST
;
50 void GenericCandidateGeneratorClasses::reset(TNode eqc
){
52 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
53 if(d_can_gen
[i
] != NULL
) d_can_gen
[i
]->reset(eqc
);
55 d_can_gen_id
=THEORY_FIRST
;
59 TNode
GenericCandidateGeneratorClasses::getNextCandidate(){
60 Assert(THEORY_FIRST
<= d_can_gen_id
&& d_can_gen_id
<= THEORY_LAST
);
62 if(d_can_gen_id
== THEORY_LAST
) return TNode::null();
63 /** Try with this theory */
64 TNode cand
= d_can_gen
[d_can_gen_id
]->getNextCandidate();
65 if( !cand
.isNull() ) return cand
;
67 return getNextCandidate();
70 void GenericCandidateGeneratorClasses::lookForNextTheory(){
71 do{ /* look for the next available generator */
73 } while( d_can_gen_id
< THEORY_LAST
&& d_can_gen
[d_can_gen_id
] == NULL
);
76 GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine
* qe
): d_qe(qe
) {
77 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
78 if(d_qe
->getInstantiator(i
) != NULL
)
79 d_can_gen
[i
] = d_qe
->getInstantiator(i
)->getRRCanGenClass();
80 else d_can_gen
[i
] = NULL
;
84 GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){
85 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
90 void GenericCandidateGeneratorClass::resetInstantiationRound(){
91 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
92 if(d_can_gen
[i
] != NULL
) d_can_gen
[i
]->resetInstantiationRound();
94 d_can_gen_id
=THEORY_FIRST
;
97 void GenericCandidateGeneratorClass::reset(TNode eqc
){
98 for(TheoryId i
= THEORY_FIRST
; i
< theory::THEORY_LAST
; ++i
){
99 if(d_can_gen
[i
] != NULL
) d_can_gen
[i
]->reset(eqc
);
101 d_can_gen_id
=THEORY_FIRST
;
106 TNode
GenericCandidateGeneratorClass::getNextCandidate(){
107 Assert(THEORY_FIRST
<= d_can_gen_id
&& d_can_gen_id
<= THEORY_LAST
);
109 if(d_can_gen_id
== THEORY_LAST
) return TNode::null();
110 /** Try with this theory */
111 TNode cand
= d_can_gen
[d_can_gen_id
]->getNextCandidate();
112 if( !cand
.isNull() ) return cand
;
114 return getNextCandidate();
117 void GenericCandidateGeneratorClass::lookForNextTheory(){
118 do{ /* look for the next available generator, where the element is */
121 d_can_gen_id
< THEORY_LAST
&&
122 (d_can_gen
[d_can_gen_id
] == NULL
||
123 !d_qe
->getInstantiator( d_can_gen_id
)->hasTerm( d_node
))