1 /********************* */
4 ** Original author: Andrew Reynolds
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 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 Implementation of representative set
15 #include "theory/rep_set.h"
16 #include "theory/type_enumerator.h"
17 #include "theory/quantifiers/bounded_integers.h"
21 using namespace CVC4::kind
;
22 using namespace CVC4::context
;
23 using namespace CVC4::theory
;
27 d_type_complete
.clear();
31 int RepSet::getNumRepresentatives( TypeNode tn
) const{
32 std::map
< TypeNode
, std::vector
< Node
> >::const_iterator it
= d_type_reps
.find( tn
);
33 if( it
!=d_type_reps
.end() ){
34 return (int)it
->second
.size();
40 void RepSet::add( Node n
){
41 TypeNode t
= n
.getType();
42 d_tmap
[ n
] = (int)d_type_reps
[t
].size();
43 d_type_reps
[t
].push_back( n
);
46 int RepSet::getIndexFor( Node n
) const {
47 std::map
< Node
, int >::const_iterator it
= d_tmap
.find( n
);
48 if( it
!=d_tmap
.end() ){
55 void RepSet::complete( TypeNode t
){
56 if( d_type_complete
.find( t
)==d_type_complete
.end() ){
57 d_type_complete
[t
] = true;
59 while( !te
.isFinished() ){
61 if( std::find( d_type_reps
[t
].begin(), d_type_reps
[t
].end(), n
)==d_type_reps
[t
].end() ){
66 for( size_t i
=0; i
<d_type_reps
[t
].size(); i
++ ){
67 Trace("reps-complete") << d_type_reps
[t
][i
] << " ";
69 Trace("reps-complete") << std::endl
;
73 void RepSet::toStream(std::ostream
& out
){
75 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= d_type_reps
.begin(); it
!= d_type_reps
.end(); ++it
){
76 out
<< it
->first
<< " : " << std::endl
;
77 for( int i
=0; i
<(int)it
->second
.size(); i
++ ){
78 out
<< " " << i
<< ": " << it
->second
[i
] << std::endl
;
82 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= d_type_reps
.begin(); it
!= d_type_reps
.end(); ++it
){
83 if( !it
->first
.isFunction() && !it
->first
.isPredicate() ){
84 out
<< "(" << it
->first
<< " " << it
->second
.size();
86 for( int i
=0; i
<(int)it
->second
.size(); i
++ ){
87 if( i
>0 ){ out
<< " "; }
91 out
<< ")" << std::endl
;
98 RepSetIterator::RepSetIterator( QuantifiersEngine
* qe
, RepSet
* rs
) : d_qe(qe
), d_rep_set( rs
){
102 int RepSetIterator::domainSize( int i
) {
104 if( d_enum_type
[i
]==ENUM_DOMAIN_ELEMENTS
){
105 return d_domain
[i
].size();
107 return d_domain
[i
][0];
111 bool RepSetIterator::setQuantifier( Node f
){
112 Trace("rsi") << "Make rsi for " << f
<< std::endl
;
113 Assert( d_types
.empty() );
115 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
116 d_types
.push_back( f
[0][i
].getType() );
122 bool RepSetIterator::setFunctionDomain( Node op
){
123 Trace("rsi") << "Make rsi for " << op
<< std::endl
;
124 Assert( d_types
.empty() );
125 TypeNode tn
= op
.getType();
126 for( size_t i
=0; i
<tn
.getNumChildren()-1; i
++ ){
127 d_types
.push_back( tn
[i
] );
133 bool RepSetIterator::initialize(){
134 for( size_t i
=0; i
<d_types
.size(); i
++ ){
135 d_index
.push_back( 0 );
136 //store default index order
137 d_index_order
.push_back( i
);
139 //store default domain
140 d_domain
.push_back( RepDomain() );
141 TypeNode tn
= d_types
[i
];
144 if( !d_rep_set
->hasType( tn
) ){
145 Node var
= NodeManager::currentNM()->mkSkolem( "repSet_$$", tn
, "is a variable created by the RepSetIterator" );
146 Trace("mkVar") << "RepSetIterator:: Make variable " << var
<< " : " << tn
<< std::endl
;
147 d_rep_set
->add( var
);
149 }else if( tn
.isInteger() ){
150 //check if it is bound
151 if( d_owner
.getKind()==FORALL
&& d_qe
&& d_qe
->getBoundedIntegers() ){
152 if( d_qe
->getBoundedIntegers()->isBoundVar( d_owner
, d_owner
[0][i
] ) ){
153 Trace("bound-int-rsi") << "Rep set iterator: variable #" << i
<< " is bounded integer." << std::endl
;
154 d_enum_type
.push_back( ENUM_RANGE
);
157 Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl
;
161 Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl
;
164 }else if( tn
.isReal() ){
165 Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn
<< std::endl
;
167 //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
168 }else if( tn
.getCardinality().isFinite() && tn
.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
169 d_rep_set
->complete( tn
);
171 Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn
<< std::endl
;
175 d_enum_type
.push_back( ENUM_DOMAIN_ELEMENTS
);
176 if( d_rep_set
->hasType( tn
) ){
177 for( size_t j
=0; j
<d_rep_set
->d_type_reps
[tn
].size(); j
++ ){
178 d_domain
[i
].push_back( j
);
185 //must set a variable index order
186 if (d_owner
.getKind()==FORALL
&& d_qe
&& d_qe
->getBoundedIntegers()) {
187 Trace("bound-int-rsi") << "Calculating variable order..." << std::endl
;
188 std::vector
< int > varOrder
;
189 for( unsigned i
=0; i
<d_qe
->getBoundedIntegers()->getNumBoundVars(d_owner
); i
++ ){
190 varOrder
.push_back(d_qe
->getBoundedIntegers()->getBoundVarNum(d_owner
,i
));
192 for( unsigned i
=0; i
<d_owner
[0].getNumChildren(); i
++) {
193 if( !d_qe
->getBoundedIntegers()->isBoundVar(d_owner
, d_owner
[0][i
])) {
194 varOrder
.push_back(i
);
197 Trace("bound-int-rsi") << "Variable order : ";
198 for( unsigned i
=0; i
<varOrder
.size(); i
++) {
199 Trace("bound-int-rsi") << varOrder
[i
] << " ";
201 Trace("bound-int-rsi") << std::endl
;
202 std::vector
< int > indexOrder
;
203 indexOrder
.resize(varOrder
.size());
204 for( unsigned i
=0; i
<varOrder
.size(); i
++){
205 indexOrder
[varOrder
[i
]] = i
;
207 Trace("bound-int-rsi") << "Will use index order : ";
208 for( unsigned i
=0; i
<indexOrder
.size(); i
++) {
209 Trace("bound-int-rsi") << indexOrder
[i
] << " ";
211 Trace("bound-int-rsi") << std::endl
;
212 setIndexOrder(indexOrder
);
214 for (unsigned i
=0; i
<d_index
.size(); i
++) {
215 if (!resetIndex(i
, true)){
222 void RepSetIterator::setIndexOrder( std::vector
< int >& indexOrder
){
223 d_index_order
.clear();
224 d_index_order
.insert( d_index_order
.begin(), indexOrder
.begin(), indexOrder
.end() );
225 //make the d_var_order mapping
226 for( int i
=0; i
<(int)d_index_order
.size(); i
++ ){
227 d_var_order
[d_index_order
[i
]] = i
;
231 void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
233 d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
234 //we are done if a domain is empty
235 for( int i=0; i<(int)d_domain.size(); i++ ){
236 if( d_domain[i].empty() ){
242 bool RepSetIterator::resetIndex( int i
, bool initial
) {
244 int ii
= d_index_order
[i
];
245 Trace("bound-int-rsi") << "Reset " << i
<< " " << ii
<< " " << initial
<< std::endl
;
246 //determine the current range
247 if( d_enum_type
[ii
]==ENUM_RANGE
){
248 if( initial
|| !d_qe
->getBoundedIntegers()->isGroundRange( d_owner
, d_owner
[0][ii
] ) ){
249 Trace("bound-int-rsi") << "Getting range of " << d_owner
[0][ii
] << std::endl
;
251 d_qe
->getBoundedIntegers()->getBoundValues( d_owner
, d_owner
[0][ii
], this, l
, u
);
252 if( l
.isNull() || u
.isNull() ){
253 //failed, abort the iterator
257 Trace("bound-int-rsi") << "Can limit bounds of " << d_owner
[0][ii
] << " to " << l
<< "..." << u
<< std::endl
;
258 Node range
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS
, u
, l
) );
259 Node ra
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ
, range
, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
260 d_domain
[ii
].clear();
261 d_lower_bounds
[ii
] = l
;
262 if( ra
==NodeManager::currentNM()->mkConst(true) ){
263 long rr
= range
.getConst
<Rational
>().getNumerator().getLong()+1;
264 Trace("bound-int-rsi") << "Actual bound range is " << rr
<< std::endl
;
265 d_domain
[ii
].push_back( (int)rr
);
267 Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner
[0][ii
] << "." << std::endl
;
269 d_domain
[ii
].push_back( 0 );
273 Trace("bound-int-rsi") << d_owner
[0][ii
] << " has ground range, skip." << std::endl
;
279 void RepSetIterator::increment2( int counter
){
280 Assert( !isFinished() );
281 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
282 counter
= (int)d_index
.size()-1;
286 Trace("rsi-debug") << "domain size of " << counter
<< " is " << domainSize(counter
) << std::endl
;
288 while( counter
>=0 && d_index
[counter
]>=(int)(domainSize(counter
)-1) ){
291 Trace("rsi-debug") << "domain size of " << counter
<< " is " << domainSize(counter
) << std::endl
;
298 bool emptyDomain
= false;
299 for( int i
=(int)d_index
.size()-1; i
>counter
; i
-- ){
302 }else if( domainSize(i
)<=0 ){
307 Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl
;
313 void RepSetIterator::increment(){
315 increment2( (int)d_index
.size()-1 );
319 bool RepSetIterator::isFinished(){
320 return d_index
.empty();
323 Node
RepSetIterator::getTerm( int i
){
324 int index
= d_index_order
[i
];
325 if( d_enum_type
[index
]==ENUM_DOMAIN_ELEMENTS
){
326 TypeNode tn
= d_types
[index
];
327 Assert( d_rep_set
->d_type_reps
.find( tn
)!=d_rep_set
->d_type_reps
.end() );
328 return d_rep_set
->d_type_reps
[tn
][d_domain
[index
][d_index
[index
]]];
330 Trace("rsi-debug") << index
<< " " << d_lower_bounds
[index
] << " " << d_index
[index
] << std::endl
;
331 Node t
= NodeManager::currentNM()->mkNode(PLUS
, d_lower_bounds
[index
],
332 NodeManager::currentNM()->mkConst( Rational(d_index
[index
]) ) );
333 t
= Rewriter::rewrite( t
);
338 void RepSetIterator::debugPrint( const char* c
){
339 for( int i
=0; i
<(int)d_index
.size(); i
++ ){
340 Debug( c
) << i
<< " : " << d_index
[i
] << " : " << getTerm( i
) << std::endl
;
344 void RepSetIterator::debugPrintSmall( const char* c
){
345 Debug( c
) << "RI: ";
346 for( int i
=0; i
<(int)d_index
.size(); i
++ ){
347 Debug( c
) << d_index
[i
] << ": " << getTerm( i
) << " ";
349 Debug( c
) << std::endl
;