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-2017 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 <unordered_set>
17 #include "theory/quantifiers/bounded_integers.h"
18 #include "theory/quantifiers/first_order_model.h"
19 #include "theory/quantifiers/term_enumeration.h"
20 #include "theory/quantifiers/term_util.h"
21 #include "theory/rep_set.h"
22 #include "theory/type_enumerator.h"
26 using namespace CVC4::kind
;
27 using namespace CVC4::context
;
28 using namespace CVC4::theory
;
32 d_type_complete
.clear();
34 d_values_to_terms
.clear();
37 bool RepSet::hasRep(TypeNode tn
, Node n
) const
39 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
41 if( it
==d_type_reps
.end() ){
44 return std::find( it
->second
.begin(), it
->second
.end(), n
)!=it
->second
.end();
48 unsigned RepSet::getNumRepresentatives(TypeNode tn
) const
50 std::map
< TypeNode
, std::vector
< Node
> >::const_iterator it
= d_type_reps
.find( tn
);
51 if( it
!=d_type_reps
.end() ){
52 return it
->second
.size();
58 Node
RepSet::getRepresentative(TypeNode tn
, unsigned i
) const
60 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
62 Assert(it
!= d_type_reps
.end());
63 Assert(i
< it
->second
.size());
67 bool containsStoreAll(Node n
, std::unordered_set
<Node
, NodeHashFunction
>& cache
)
69 if( std::find( cache
.begin(), cache
.end(), n
)==cache
.end() ){
71 if( n
.getKind()==STORE_ALL
){
74 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
75 if( containsStoreAll( n
[i
], cache
) ){
84 void RepSet::add( TypeNode tn
, Node n
){
85 //for now, do not add array constants FIXME
87 std::unordered_set
<Node
, NodeHashFunction
> cache
;
88 if( containsStoreAll( n
, cache
) ){
92 Trace("rsi-debug") << "Add rep #" << d_type_reps
[tn
].size() << " for " << tn
<< " : " << n
<< std::endl
;
93 Assert( n
.getType().isSubtypeOf( tn
) );
94 d_tmap
[ n
] = (int)d_type_reps
[tn
].size();
95 d_type_reps
[tn
].push_back( n
);
98 int RepSet::getIndexFor( Node n
) const {
99 std::map
< Node
, int >::const_iterator it
= d_tmap
.find( n
);
100 if( it
!=d_tmap
.end() ){
107 bool RepSet::complete( TypeNode t
){
108 std::map
< TypeNode
, bool >::iterator it
= d_type_complete
.find( t
);
109 if( it
==d_type_complete
.end() ){
110 //remove all previous
111 for( unsigned i
=0; i
<d_type_reps
[t
].size(); i
++ ){
112 d_tmap
.erase( d_type_reps
[t
][i
] );
114 d_type_reps
[t
].clear();
115 //now complete the type
116 d_type_complete
[t
] = true;
117 TypeEnumerator
te(t
);
118 while( !te
.isFinished() ){
120 if( std::find( d_type_reps
[t
].begin(), d_type_reps
[t
].end(), n
)==d_type_reps
[t
].end() ){
125 for( size_t i
=0; i
<d_type_reps
[t
].size(); i
++ ){
126 Trace("reps-complete") << d_type_reps
[t
][i
] << " ";
128 Trace("reps-complete") << std::endl
;
135 Node
RepSet::getTermForRepresentative(Node n
) const
137 std::map
<Node
, Node
>::const_iterator it
= d_values_to_terms
.find(n
);
138 if (it
!= d_values_to_terms
.end())
148 void RepSet::setTermForRepresentative(Node n
, Node t
)
150 d_values_to_terms
[n
] = t
;
153 Node
RepSet::getDomainValue(TypeNode tn
, const std::vector
<Node
>& exclude
) const
155 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
156 d_type_reps
.find(tn
);
157 if (it
!= d_type_reps
.end())
159 // try to find a pre-existing arbitrary element
160 for (size_t i
= 0; i
< it
->second
.size(); i
++)
162 if (std::find(exclude
.begin(), exclude
.end(), it
->second
[i
])
165 return it
->second
[i
];
172 void RepSet::toStream(std::ostream
& out
){
173 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= d_type_reps
.begin(); it
!= d_type_reps
.end(); ++it
){
174 if( !it
->first
.isFunction() && !it
->first
.isPredicate() ){
175 out
<< "(" << it
->first
<< " " << it
->second
.size();
177 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
178 if( i
>0 ){ out
<< " "; }
179 out
<< it
->second
[i
];
182 out
<< ")" << std::endl
;
188 RepSetIterator::RepSetIterator( QuantifiersEngine
* qe
, RepSet
* rs
) : d_qe(qe
), d_rep_set( rs
){
189 d_incomplete
= false;
192 int RepSetIterator::domainSize( int i
) {
194 int v
= d_var_order
[i
];
195 return d_domain_elements
[v
].size();
198 bool RepSetIterator::setQuantifier( Node f
, RepBoundExt
* rext
){
199 Trace("rsi") << "Make rsi for " << f
<< std::endl
;
200 Assert( d_types
.empty() );
202 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
203 d_types
.push_back( f
[0][i
].getType() );
206 return initialize( rext
);
209 bool RepSetIterator::setFunctionDomain( Node op
, RepBoundExt
* rext
){
210 Trace("rsi") << "Make rsi for " << op
<< std::endl
;
211 Assert( d_types
.empty() );
212 TypeNode tn
= op
.getType();
213 for( size_t i
=0; i
<tn
.getNumChildren()-1; i
++ ){
214 d_types
.push_back( tn
[i
] );
217 return initialize( rext
);
220 // TODO : as part of #1199, the portions of this
221 // function which modify d_rep_set should be
222 // moved to TheoryModel.
223 bool RepSetIterator::initialize( RepBoundExt
* rext
){
224 Trace("rsi") << "Initialize rep set iterator..." << std::endl
;
225 for( unsigned v
=0; v
<d_types
.size(); v
++ ){
226 d_index
.push_back( 0 );
227 //store default index order
228 d_index_order
.push_back( v
);
230 //store default domain
231 //d_domain.push_back( RepDomain() );
232 d_domain_elements
.push_back( std::vector
< Node
>() );
233 TypeNode tn
= d_types
[v
];
234 Trace("rsi") << "Var #" << v
<< " is type " << tn
<< "..." << std::endl
;
236 //must ensure uninterpreted type is non-empty.
237 if( !d_rep_set
->hasType( tn
) ){
239 // terms in rep_set are now constants which mapped to terms through TheoryModel
240 // thus, should introduce a constant and a term. for now, just a term.
242 //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 );
243 Node var
= d_qe
->getModel()->getSomeDomainElement( tn
);
244 Trace("mkVar") << "RepSetIterator:: Make variable " << var
<< " : " << tn
<< std::endl
;
245 d_rep_set
->add( tn
, var
);
249 //check if it is externally bound
250 if( rext
&& rext
->setBound( d_owner
, v
, tn
, d_domain_elements
[v
] ) ){
251 d_enum_type
.push_back( ENUM_DEFAULT
);
253 //builtin: check if it is bound by bounded integer module
254 }else if( d_owner
.getKind()==FORALL
&& d_qe
&& d_qe
->getBoundedIntegers() ){
255 if( d_qe
->getBoundedIntegers()->isBoundVar( d_owner
, d_owner
[0][v
] ) ){
256 unsigned bvt
= d_qe
->getBoundedIntegers()->getBoundVarType( d_owner
, d_owner
[0][v
] );
257 if( bvt
!=quantifiers::BoundedIntegers::BOUND_FINITE
){
258 d_enum_type
.push_back( ENUM_BOUND_INT
);
261 //will treat in default way
267 if (d_qe
->getTermEnumeration()->mayComplete(tn
))
269 Trace("rsi") << " do complete, since cardinality is small (" << tn
.getCardinality() << ")..." << std::endl
;
270 d_rep_set
->complete( tn
);
271 //must have succeeded
272 Assert( d_rep_set
->hasType( tn
) );
274 Trace("rsi") << " variable cannot be bounded." << std::endl
;
275 Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn
<< std::endl
;
281 //if we have yet to determine the type of enumeration
282 if( d_enum_type
.size()<=v
){
283 if( d_rep_set
->hasType( tn
) ){
284 d_enum_type
.push_back( ENUM_DEFAULT
);
285 for( unsigned j
=0; j
<d_rep_set
->d_type_reps
[tn
].size(); j
++ ){
286 //d_domain[v].push_back( j );
287 d_domain_elements
[v
].push_back( d_rep_set
->d_type_reps
[tn
][j
] );
290 Assert( d_incomplete
);
295 //must set a variable index order based on bounded integers
296 if( d_owner
.getKind()==FORALL
&& d_qe
&& d_qe
->getBoundedIntegers() ){
297 Trace("bound-int-rsi") << "Calculating variable order..." << std::endl
;
298 std::vector
< int > varOrder
;
299 for( unsigned i
=0; i
<d_qe
->getBoundedIntegers()->getNumBoundVars( d_owner
); i
++ ){
300 Node v
= d_qe
->getBoundedIntegers()->getBoundVar( d_owner
, i
);
301 Trace("bound-int-rsi") << " bound var #" << i
<< " is " << v
<< std::endl
;
302 varOrder
.push_back( d_qe
->getTermUtil()->getVariableNum( d_owner
, v
) );
304 for( unsigned i
=0; i
<d_owner
[0].getNumChildren(); i
++) {
305 if( !d_qe
->getBoundedIntegers()->isBoundVar(d_owner
, d_owner
[0][i
])) {
306 varOrder
.push_back(i
);
309 Trace("bound-int-rsi") << "Variable order : ";
310 for( unsigned i
=0; i
<varOrder
.size(); i
++) {
311 Trace("bound-int-rsi") << varOrder
[i
] << " ";
313 Trace("bound-int-rsi") << std::endl
;
314 std::vector
< int > indexOrder
;
315 indexOrder
.resize(varOrder
.size());
316 for( unsigned i
=0; i
<varOrder
.size(); i
++){
317 indexOrder
[varOrder
[i
]] = i
;
319 Trace("bound-int-rsi") << "Will use index order : ";
320 for( unsigned i
=0; i
<indexOrder
.size(); i
++) {
321 Trace("bound-int-rsi") << indexOrder
[i
] << " ";
323 Trace("bound-int-rsi") << std::endl
;
324 setIndexOrder( indexOrder
);
326 //now reset the indices
327 do_reset_increment( -1, true );
331 void RepSetIterator::setIndexOrder( std::vector
< int >& indexOrder
){
332 d_index_order
.clear();
333 d_index_order
.insert( d_index_order
.begin(), indexOrder
.begin(), indexOrder
.end() );
334 //make the d_var_order mapping
335 for( unsigned i
=0; i
<d_index_order
.size(); i
++ ){
336 d_var_order
[d_index_order
[i
]] = i
;
340 int RepSetIterator::resetIndex( int i
, bool initial
) {
342 int v
= d_var_order
[i
];
343 Trace("bound-int-rsi") << "Reset " << i
<< ", var order = " << v
<< ", initial = " << initial
<< std::endl
;
344 if( d_enum_type
[v
]==ENUM_BOUND_INT
){
345 Assert( d_owner
.getKind()==FORALL
);
346 if( !d_qe
->getBoundedIntegers()->getBoundElements( this, initial
, d_owner
, d_owner
[0][v
], d_domain_elements
[v
] ) ){
350 return d_domain_elements
[v
].empty() ? 0 : 1;
353 int RepSetIterator::increment2( int i
){
354 Assert( !isFinished() );
355 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
356 i
= (int)d_index
.size()-1;
360 Trace("rsi-debug") << "domain size of " << i
<< " is " << domainSize(i
) << std::endl
;
362 while( i
>=0 && d_index
[i
]>=(int)(domainSize(i
)-1) ){
365 Trace("rsi-debug") << "domain size of " << i
<< " is " << domainSize(i
) << std::endl
;
372 Trace("rsi-debug") << "increment " << i
<< std::endl
;
374 return do_reset_increment( i
);
378 int RepSetIterator::do_reset_increment( int i
, bool initial
) {
379 bool emptyDomain
= false;
380 for( unsigned ii
=(i
+1); ii
<d_index
.size(); ii
++ ){
381 int ri_res
= resetIndex( ii
, initial
);
387 }else if( ri_res
==0 ){
390 //force next iteration if currently an empty domain
392 d_index
[ii
] = domainSize(ii
)-1;
396 Trace("rsi-debug") << "This is an empty domain, increment." << std::endl
;
403 int RepSetIterator::increment(){
405 return increment2( (int)d_index
.size()-1 );
411 bool RepSetIterator::isFinished(){
412 return d_index
.empty();
415 Node
RepSetIterator::getCurrentTerm( int v
){
416 int ii
= d_index_order
[v
];
417 int curr
= d_index
[ii
];
418 Trace("rsi-debug") << "rsi : get term " << v
<< ", index order = " << d_index_order
[v
] << std::endl
;
419 Trace("rsi-debug") << "rsi : curr = " << curr
<< " / " << d_domain_elements
[v
].size() << std::endl
;
420 Assert( 0<=curr
&& curr
<(int)d_domain_elements
[v
].size() );
421 return d_domain_elements
[v
][curr
];
424 void RepSetIterator::debugPrint( const char* c
){
425 for( unsigned v
=0; v
<d_index
.size(); v
++ ){
426 Debug( c
) << v
<< " : " << getCurrentTerm( v
) << std::endl
;
430 void RepSetIterator::debugPrintSmall( const char* c
){
431 Debug( c
) << "RI: ";
432 for( unsigned v
=0; v
<d_index
.size(); v
++ ){
433 Debug( c
) << v
<< ": " << getCurrentTerm( v
) << " ";
435 Debug( c
) << std::endl
;