1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing 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"
18 #include "theory/quantifiers/term_database.h"
19 #include "theory/quantifiers/first_order_model.h"
23 using namespace CVC4::kind
;
24 using namespace CVC4::context
;
25 using namespace CVC4::theory
;
29 d_type_complete
.clear();
31 d_values_to_terms
.clear();
32 d_type_rlv_rep
.clear();
35 bool RepSet::hasRep( TypeNode tn
, Node n
) {
36 std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= d_type_reps
.find( tn
);
37 if( it
==d_type_reps
.end() ){
40 return std::find( it
->second
.begin(), it
->second
.end(), n
)!=it
->second
.end();
44 int RepSet::getNumRepresentatives( TypeNode tn
) const{
45 std::map
< TypeNode
, std::vector
< Node
> >::const_iterator it
= d_type_reps
.find( tn
);
46 if( it
!=d_type_reps
.end() ){
47 return (int)it
->second
.size();
53 bool containsStoreAll( Node n
, std::vector
< Node
>& cache
){
54 if( std::find( cache
.begin(), cache
.end(), n
)==cache
.end() ){
56 if( n
.getKind()==STORE_ALL
){
59 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
60 if( containsStoreAll( n
[i
], cache
) ){
69 void RepSet::add( TypeNode tn
, Node n
){
70 //for now, do not add array constants FIXME
72 std::vector
< Node
> cache
;
73 if( containsStoreAll( n
, cache
) ){
77 Trace("rsi-debug") << "Add rep #" << d_type_reps
[tn
].size() << " for " << tn
<< " : " << n
<< std::endl
;
78 Assert( n
.getType().isSubtypeOf( tn
) );
79 d_tmap
[ n
] = (int)d_type_reps
[tn
].size();
80 d_type_reps
[tn
].push_back( n
);
83 int RepSet::getIndexFor( Node n
) const {
84 std::map
< Node
, int >::const_iterator it
= d_tmap
.find( n
);
85 if( it
!=d_tmap
.end() ){
92 bool RepSet::complete( TypeNode t
){
93 std::map
< TypeNode
, bool >::iterator it
= d_type_complete
.find( t
);
94 if( it
==d_type_complete
.end() ){
96 for( unsigned i
=0; i
<d_type_reps
[t
].size(); i
++ ){
97 d_tmap
.erase( d_type_reps
[t
][i
] );
99 d_type_reps
[t
].clear();
100 //now complete the type
101 d_type_complete
[t
] = true;
102 TypeEnumerator
te(t
);
103 while( !te
.isFinished() ){
105 if( std::find( d_type_reps
[t
].begin(), d_type_reps
[t
].end(), n
)==d_type_reps
[t
].end() ){
110 for( size_t i
=0; i
<d_type_reps
[t
].size(); i
++ ){
111 Trace("reps-complete") << d_type_reps
[t
][i
] << " ";
113 Trace("reps-complete") << std::endl
;
120 int RepSet::getNumRelevantGroundReps( TypeNode t
) {
121 std::map
< TypeNode
, int >::iterator it
= d_type_rlv_rep
.find( t
);
122 if( it
==d_type_rlv_rep
.end() ){
129 void RepSet::toStream(std::ostream
& out
){
130 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= d_type_reps
.begin(); it
!= d_type_reps
.end(); ++it
){
131 if( !it
->first
.isFunction() && !it
->first
.isPredicate() ){
132 out
<< "(" << it
->first
<< " " << it
->second
.size();
134 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
135 if( i
>0 ){ out
<< " "; }
136 out
<< it
->second
[i
];
139 out
<< ")" << std::endl
;
145 RepSetIterator::RepSetIterator( QuantifiersEngine
* qe
, RepSet
* rs
) : d_qe(qe
), d_rep_set( rs
){
146 d_incomplete
= false;
149 int RepSetIterator::domainSize( int i
) {
151 int v
= d_var_order
[i
];
152 if( d_enum_type
[v
]==ENUM_DOMAIN_ELEMENTS
){
153 return d_domain
[v
].size();
155 return d_domain
[v
][0];
159 bool RepSetIterator::setQuantifier( Node f
){
160 Trace("rsi") << "Make rsi for " << f
<< std::endl
;
161 Assert( d_types
.empty() );
163 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
164 d_types
.push_back( f
[0][i
].getType() );
170 bool RepSetIterator::setFunctionDomain( Node op
){
171 Trace("rsi") << "Make rsi for " << op
<< std::endl
;
172 Assert( d_types
.empty() );
173 TypeNode tn
= op
.getType();
174 for( size_t i
=0; i
<tn
.getNumChildren()-1; i
++ ){
175 d_types
.push_back( tn
[i
] );
181 bool RepSetIterator::initialize(){
182 Trace("rsi") << "Initialize rep set iterator..." << std::endl
;
183 for( unsigned v
=0; v
<d_types
.size(); v
++ ){
184 d_index
.push_back( 0 );
185 //store default index order
186 d_index_order
.push_back( v
);
188 //store default domain
189 d_domain
.push_back( RepDomain() );
190 TypeNode tn
= d_types
[v
];
191 Trace("rsi") << "Var #" << v
<< " is type " << tn
<< "..." << std::endl
;
193 //must ensure uninterpreted type is non-empty.
194 if( !d_rep_set
->hasType( tn
) ){
196 // terms in rep_set are now constants which mapped to terms through TheoryModel
197 // thus, should introduce a constant and a term. for now, just a term.
199 //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
200 Node var
= d_qe
->getModel()->getSomeDomainElement( tn
);
201 Trace("mkVar") << "RepSetIterator:: Make variable " << var
<< " : " << tn
<< std::endl
;
202 d_rep_set
->add( tn
, var
);
206 //check if it is bound by bounded integer module
207 if( d_owner
.getKind()==FORALL
&& d_qe
&& d_qe
->getBoundedIntegers() ){
208 unsigned bvt
= d_qe
->getBoundedIntegers()->getBoundVarType( d_owner
, d_owner
[0][v
] );
209 if( bvt
==quantifiers::BoundedIntegers::BOUND_INT_RANGE
){
210 Trace("rsi") << " variable is bounded integer." << std::endl
;
211 d_enum_type
.push_back( ENUM_INT_RANGE
);
213 }else if( bvt
==quantifiers::BoundedIntegers::BOUND_SET_MEMBER
){
214 Trace("rsi") << " variable is bounded by set membership." << std::endl
;
215 d_enum_type
.push_back( ENUM_SET_MEMBERS
);
220 //check if it is otherwise bound
221 if( d_bounds
[0].find( v
)!=d_bounds
[0].end() && d_bounds
[1].find( v
)!=d_bounds
[1].end() ){
222 Trace("rsi") << " variable is bounded." << std::endl
;
223 d_enum_type
.push_back( ENUM_INT_RANGE
);
224 }else if( d_qe
->getTermDatabase()->mayComplete( tn
) ){
225 Trace("rsi") << " do complete, since cardinality is small (" << tn
.getCardinality() << ")..." << std::endl
;
226 d_rep_set
->complete( tn
);
227 //must have succeeded
228 Assert( d_rep_set
->hasType( tn
) );
230 Trace("rsi") << " variable cannot be bounded." << std::endl
;
231 Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn
<< std::endl
;
236 //if we have yet to determine the type of enumeration
237 if( d_enum_type
.size()<=v
){
238 d_enum_type
.push_back( ENUM_DOMAIN_ELEMENTS
);
239 if( d_rep_set
->hasType( tn
) ){
240 for( unsigned j
=0; j
<d_rep_set
->d_type_reps
[tn
].size(); j
++ ){
241 d_domain
[v
].push_back( j
);
244 Assert( d_incomplete
);
249 //must set a variable index order based on bounded integers
250 if( d_owner
.getKind()==FORALL
&& d_qe
&& d_qe
->getBoundedIntegers() ){
251 Trace("bound-int-rsi") << "Calculating variable order..." << std::endl
;
252 std::vector
< int > varOrder
;
253 for( unsigned i
=0; i
<d_qe
->getBoundedIntegers()->getNumBoundVars( d_owner
); i
++ ){
254 Node v
= d_qe
->getBoundedIntegers()->getBoundVar( d_owner
, i
);
255 Trace("bound-int-rsi") << " bound var #" << i
<< " is " << v
<< std::endl
;
256 varOrder
.push_back( d_qe
->getTermDatabase()->getVariableNum( d_owner
, v
) );
258 for( unsigned i
=0; i
<d_owner
[0].getNumChildren(); i
++) {
259 if( !d_qe
->getBoundedIntegers()->isBoundVar(d_owner
, d_owner
[0][i
])) {
260 varOrder
.push_back(i
);
263 Trace("bound-int-rsi") << "Variable order : ";
264 for( unsigned i
=0; i
<varOrder
.size(); i
++) {
265 Trace("bound-int-rsi") << varOrder
[i
] << " ";
267 Trace("bound-int-rsi") << std::endl
;
268 std::vector
< int > indexOrder
;
269 indexOrder
.resize(varOrder
.size());
270 for( unsigned i
=0; i
<varOrder
.size(); i
++){
271 indexOrder
[varOrder
[i
]] = i
;
273 Trace("bound-int-rsi") << "Will use index order : ";
274 for( unsigned i
=0; i
<indexOrder
.size(); i
++) {
275 Trace("bound-int-rsi") << indexOrder
[i
] << " ";
277 Trace("bound-int-rsi") << std::endl
;
278 setIndexOrder( indexOrder
);
280 //now reset the indices
281 do_reset_increment( -1, true );
285 void RepSetIterator::setIndexOrder( std::vector
< int >& indexOrder
){
286 d_index_order
.clear();
287 d_index_order
.insert( d_index_order
.begin(), indexOrder
.begin(), indexOrder
.end() );
288 //make the d_var_order mapping
289 for( unsigned i
=0; i
<d_index_order
.size(); i
++ ){
290 d_var_order
[d_index_order
[i
]] = i
;
294 int RepSetIterator::resetIndex( int i
, bool initial
) {
296 int v
= d_var_order
[i
];
297 Trace("bound-int-rsi") << "Reset " << i
<< ", var order = " << v
<< ", initial = " << initial
<< std::endl
;
298 //determine the current range
299 if( initial
|| ( d_owner
.getKind()==FORALL
&& d_qe
&& d_qe
->getBoundedIntegers() &&
300 d_qe
->getBoundedIntegers()->isBoundVar( d_owner
, d_owner
[0][v
] ) &&
301 !d_qe
->getBoundedIntegers()->isGroundRange( d_owner
, d_owner
[0][v
] ) ) ){
302 Trace("bound-int-rsi") << "Getting range of " << d_owner
[0][v
] << std::endl
;
303 if( d_enum_type
[v
]==ENUM_INT_RANGE
){
306 if( d_qe
->getBoundedIntegers() ){
307 unsigned bvt
= d_qe
->getBoundedIntegers()->getBoundVarType( d_owner
, d_owner
[0][v
] );
308 if( bvt
==quantifiers::BoundedIntegers::BOUND_INT_RANGE
){
309 d_qe
->getBoundedIntegers()->getBoundValues( d_owner
, d_owner
[0][v
], this, l
, u
);
312 for( unsigned b
=0; b
<2; b
++ ){
313 if( d_bounds
[b
].find(v
)!=d_bounds
[b
].end() ){
314 Trace("bound-int-rsi") << "May further limit bound(" << b
<< ") based on " << d_bounds
[b
][v
] << std::endl
;
315 if( b
==0 && (l
.isNull() || d_bounds
[b
][v
].getConst
<Rational
>() > l
.getConst
<Rational
>()) ){
317 //bound was limited externally, record that the value lower bound is not equal to the term lower bound
318 actual_l
= NodeManager::currentNM()->mkNode( MINUS
, d_bounds
[b
][v
], l
);
321 }else if( b
==1 && (u
.isNull() || d_bounds
[b
][v
].getConst
<Rational
>() <= u
.getConst
<Rational
>()) ){
322 u
= NodeManager::currentNM()->mkNode( MINUS
, d_bounds
[b
][v
],
323 NodeManager::currentNM()->mkConst( Rational(1) ) );
324 u
= Rewriter::rewrite( u
);
329 if( l
.isNull() || u
.isNull() ){
330 //failed, abort the iterator
333 Trace("bound-int-rsi") << "Can limit bounds of " << d_owner
[0][v
] << " to " << l
<< "..." << u
<< std::endl
;
334 Node range
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS
, u
, l
) );
335 Node ra
= Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ
, range
, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
339 if( d_qe
->getBoundedIntegers() && d_qe
->getBoundedIntegers()->isBoundVar( d_owner
, d_owner
[0][v
] ) ){
340 d_qe
->getBoundedIntegers()->getBounds( d_owner
, d_owner
[0][v
], this, tl
, tu
);
342 d_lower_bounds
[v
] = tl
;
343 if( !actual_l
.isNull() ){
344 //if bound was limited externally, must consider the offset
345 d_lower_bounds
[v
] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS
, tl
, actual_l
) );
347 if( ra
==d_qe
->getTermDatabase()->d_true
){
348 long rr
= range
.getConst
<Rational
>().getNumerator().getLong()+1;
349 Trace("bound-int-rsi") << "Actual bound range is " << rr
<< std::endl
;
350 d_domain
[v
].push_back( (int)rr
);
355 Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner
[0][v
] << "." << std::endl
;
359 }else if( d_enum_type
[v
]==ENUM_SET_MEMBERS
){
360 Assert( d_qe
->getBoundedIntegers()->getBoundVarType( d_owner
, d_owner
[0][v
] )==quantifiers::BoundedIntegers::BOUND_SET_MEMBER
);
361 Node srv
= d_qe
->getBoundedIntegers()->getSetRangeValue( d_owner
, d_owner
[0][v
], this );
365 Trace("bound-int-rsi") << "Bounded by set membership : " << srv
<< std::endl
;
367 d_setm_bounds
[v
].clear();
368 if( srv
.getKind()!=EMPTYSET
){
369 //TODO: need term model, not value model
370 while( srv
.getKind()==UNION
){
371 Assert( srv
[1].getKind()==kind::SINGLETON
);
372 d_setm_bounds
[v
].push_back( srv
[1][0] );
375 d_setm_bounds
[v
].push_back( srv
[0] );
376 d_domain
[v
].push_back( d_setm_bounds
[v
].size() );
378 d_domain
[v
].push_back( 0 );
386 int RepSetIterator::increment2( int i
){
387 Assert( !isFinished() );
388 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
389 i
= (int)d_index
.size()-1;
393 Trace("rsi-debug") << "domain size of " << i
<< " is " << domainSize(i
) << std::endl
;
395 while( i
>=0 && d_index
[i
]>=(int)(domainSize(i
)-1) ){
398 Trace("rsi-debug") << "domain size of " << i
<< " is " << domainSize(i
) << std::endl
;
405 Trace("rsi-debug") << "increment " << i
<< std::endl
;
407 return do_reset_increment( i
);
411 int RepSetIterator::do_reset_increment( int i
, bool initial
) {
412 bool emptyDomain
= false;
413 for( unsigned ii
=(i
+1); ii
<d_index
.size(); ii
++ ){
414 int ri_res
= resetIndex( ii
, initial
);
420 }else if( ri_res
==0 ){
423 //force next iteration if currently an empty domain
425 d_index
[ii
] = domainSize(ii
)-1;
429 Trace("rsi-debug") << "This is an empty domain, increment." << std::endl
;
436 int RepSetIterator::increment(){
438 return increment2( (int)d_index
.size()-1 );
444 bool RepSetIterator::isFinished(){
445 return d_index
.empty();
448 Node
RepSetIterator::getCurrentTerm( int v
){
449 Trace("rsi-debug") << "rsi : get term " << v
<< ", index order = " << d_index_order
[v
] << std::endl
;
450 int ii
= d_index_order
[v
];
451 int curr
= d_index
[ii
];
452 if( d_enum_type
[v
]==ENUM_DOMAIN_ELEMENTS
){
453 TypeNode tn
= d_types
[v
];
454 Assert( d_rep_set
->d_type_reps
.find( tn
)!=d_rep_set
->d_type_reps
.end() );
455 Assert( 0<=d_domain
[v
][curr
] && d_domain
[v
][curr
]<(int)d_rep_set
->d_type_reps
[tn
].size() );
456 return d_rep_set
->d_type_reps
[tn
][d_domain
[v
][curr
]];
457 }else if( d_enum_type
[v
]==ENUM_SET_MEMBERS
){
458 Assert( 0<=curr
&& curr
<(int)d_setm_bounds
[v
].size() );
459 return d_setm_bounds
[v
][curr
];
461 Trace("rsi-debug") << "Get, with offset : " << v
<< " " << d_lower_bounds
[v
] << " " << curr
<< std::endl
;
462 Assert( !d_lower_bounds
[v
].isNull() );
463 Node t
= NodeManager::currentNM()->mkNode(PLUS
, d_lower_bounds
[v
], NodeManager::currentNM()->mkConst( Rational(curr
) ) );
464 t
= Rewriter::rewrite( t
);
469 void RepSetIterator::debugPrint( const char* c
){
470 for( unsigned v
=0; v
<d_index
.size(); v
++ ){
471 Debug( c
) << v
<< " : " << getCurrentTerm( v
) << std::endl
;
475 void RepSetIterator::debugPrintSmall( const char* c
){
476 Debug( c
) << "RI: ";
477 for( unsigned v
=0; v
<d_index
.size(); v
++ ){
478 Debug( c
) << v
<< ": " << getCurrentTerm( v
) << " ";
480 Debug( c
) << std::endl
;