1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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/rep_set.h"
18 #include "theory/type_enumerator.h"
21 using namespace CVC4::kind
;
28 d_type_complete
.clear();
30 d_values_to_terms
.clear();
33 bool RepSet::hasRep(TypeNode tn
, Node n
) const
35 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
37 if( it
==d_type_reps
.end() ){
40 return std::find( it
->second
.begin(), it
->second
.end(), n
)!=it
->second
.end();
44 size_t RepSet::getNumRepresentatives(TypeNode tn
) const
46 const std::vector
<Node
>* reps
= getTypeRepsOrNull(tn
);
47 return (reps
!= nullptr) ? reps
->size() : 0;
50 Node
RepSet::getRepresentative(TypeNode tn
, unsigned i
) const
52 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
54 Assert(it
!= d_type_reps
.end());
55 Assert(i
< it
->second
.size());
59 const std::vector
<Node
>* RepSet::getTypeRepsOrNull(TypeNode tn
) const
61 auto it
= d_type_reps
.find(tn
);
62 if (it
== d_type_reps
.end())
71 bool containsStoreAll(Node n
, std::unordered_set
<Node
, NodeHashFunction
>& cache
)
73 if( std::find( cache
.begin(), cache
.end(), n
)==cache
.end() ){
75 if( n
.getKind()==STORE_ALL
){
78 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
79 if( containsStoreAll( n
[i
], cache
) ){
90 void RepSet::add( TypeNode tn
, Node n
){
91 //for now, do not add array constants FIXME
93 std::unordered_set
<Node
, NodeHashFunction
> cache
;
94 if( containsStoreAll( n
, cache
) ){
98 Trace("rsi-debug") << "Add rep #" << d_type_reps
[tn
].size() << " for " << tn
<< " : " << n
<< std::endl
;
99 Assert(n
.getType().isSubtypeOf(tn
));
100 d_tmap
[ n
] = (int)d_type_reps
[tn
].size();
101 d_type_reps
[tn
].push_back( n
);
104 int RepSet::getIndexFor( Node n
) const {
105 std::map
< Node
, int >::const_iterator it
= d_tmap
.find( n
);
106 if( it
!=d_tmap
.end() ){
113 bool RepSet::complete( TypeNode t
){
114 std::map
< TypeNode
, bool >::iterator it
= d_type_complete
.find( t
);
115 if( it
==d_type_complete
.end() ){
116 //remove all previous
117 for( unsigned i
=0; i
<d_type_reps
[t
].size(); i
++ ){
118 d_tmap
.erase( d_type_reps
[t
][i
] );
120 d_type_reps
[t
].clear();
121 //now complete the type
122 d_type_complete
[t
] = true;
123 TypeEnumerator
te(t
);
124 while( !te
.isFinished() ){
126 if( std::find( d_type_reps
[t
].begin(), d_type_reps
[t
].end(), n
)==d_type_reps
[t
].end() ){
131 for( size_t i
=0; i
<d_type_reps
[t
].size(); i
++ ){
132 Trace("reps-complete") << d_type_reps
[t
][i
] << " ";
134 Trace("reps-complete") << std::endl
;
141 Node
RepSet::getTermForRepresentative(Node n
) const
143 std::map
<Node
, Node
>::const_iterator it
= d_values_to_terms
.find(n
);
144 if (it
!= d_values_to_terms
.end())
154 void RepSet::setTermForRepresentative(Node n
, Node t
)
156 d_values_to_terms
[n
] = t
;
159 Node
RepSet::getDomainValue(TypeNode tn
, const std::vector
<Node
>& exclude
) const
161 std::map
<TypeNode
, std::vector
<Node
> >::const_iterator it
=
162 d_type_reps
.find(tn
);
163 if (it
!= d_type_reps
.end())
165 // try to find a pre-existing arbitrary element
166 for (size_t i
= 0; i
< it
->second
.size(); i
++)
168 if (std::find(exclude
.begin(), exclude
.end(), it
->second
[i
])
171 return it
->second
[i
];
178 void RepSet::toStream(std::ostream
& out
){
179 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator it
= d_type_reps
.begin(); it
!= d_type_reps
.end(); ++it
){
180 if( !it
->first
.isFunction() && !it
->first
.isPredicate() ){
181 out
<< "(" << it
->first
<< " " << it
->second
.size();
183 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
184 if( i
>0 ){ out
<< " "; }
185 out
<< it
->second
[i
];
188 out
<< ")" << std::endl
;
193 RepSetIterator::RepSetIterator(const RepSet
* rs
, RepBoundExt
* rext
)
194 : d_rs(rs
), d_rext(rext
), d_incomplete(false)
198 unsigned RepSetIterator::domainSize(unsigned i
)
200 unsigned v
= d_var_order
[i
];
201 return d_domain_elements
[v
].size();
204 TypeNode
RepSetIterator::getTypeOf(unsigned i
) const { return d_types
[i
]; }
206 bool RepSetIterator::setQuantifier(Node q
)
208 Trace("rsi") << "Make rsi for quantified formula " << q
<< std::endl
;
209 Assert(d_types
.empty());
211 for (size_t i
= 0; i
< q
[0].getNumChildren(); i
++)
213 d_types
.push_back(q
[0][i
].getType());
219 bool RepSetIterator::setFunctionDomain(Node op
)
221 Trace("rsi") << "Make rsi for function " << op
<< std::endl
;
222 Assert(d_types
.empty());
223 TypeNode tn
= op
.getType();
224 for( size_t i
=0; i
<tn
.getNumChildren()-1; i
++ ){
225 d_types
.push_back( tn
[i
] );
231 bool RepSetIterator::initialize()
233 Trace("rsi") << "Initialize rep set iterator..." << std::endl
;
234 for( unsigned v
=0; v
<d_types
.size(); v
++ ){
235 d_index
.push_back( 0 );
236 //store default index order
237 d_index_order
.push_back( v
);
239 //store default domain
240 //d_domain.push_back( RepDomain() );
241 d_domain_elements
.push_back( std::vector
< Node
>() );
242 TypeNode tn
= d_types
[v
];
243 Trace("rsi") << "Var #" << v
<< " is type " << tn
<< "..." << std::endl
;
245 bool setEnum
= false;
246 //check if it is externally bound
249 inc
= !d_rext
->initializeRepresentativesForType(tn
);
250 RsiEnumType rsiet
= d_rext
->setBound(d_owner
, v
, d_domain_elements
[v
]);
251 if (rsiet
!= ENUM_INVALID
)
253 d_enum_type
.push_back(rsiet
);
260 Trace("fmf-incomplete") << "Incomplete because of quantification of type "
265 //if we have yet to determine the type of enumeration
268 if (d_rs
->hasType(tn
))
270 d_enum_type
.push_back( ENUM_DEFAULT
);
271 if (const auto* type_reps
= d_rs
->getTypeRepsOrNull(tn
))
273 std::vector
<Node
>& v_domain_elements
= d_domain_elements
[v
];
274 v_domain_elements
.insert(v_domain_elements
.end(),
275 type_reps
->begin(), type_reps
->end());
278 Assert(d_incomplete
);
286 std::vector
<unsigned> varOrder
;
287 if (d_rext
->getVariableOrder(d_owner
, varOrder
))
289 if (Trace
.isOn("bound-int-rsi"))
291 Trace("bound-int-rsi") << "Variable order : ";
292 for (unsigned i
= 0; i
< varOrder
.size(); i
++)
294 Trace("bound-int-rsi") << varOrder
[i
] << " ";
296 Trace("bound-int-rsi") << std::endl
;
298 std::vector
<unsigned> indexOrder
;
299 indexOrder
.resize(varOrder
.size());
300 for (unsigned i
= 0; i
< varOrder
.size(); i
++)
302 Assert(varOrder
[i
] < indexOrder
.size());
303 indexOrder
[varOrder
[i
]] = i
;
305 if (Trace
.isOn("bound-int-rsi"))
307 Trace("bound-int-rsi") << "Will use index order : ";
308 for (unsigned i
= 0; i
< indexOrder
.size(); i
++)
310 Trace("bound-int-rsi") << indexOrder
[i
] << " ";
312 Trace("bound-int-rsi") << std::endl
;
314 setIndexOrder(indexOrder
);
317 //now reset the indices
318 do_reset_increment( -1, true );
322 void RepSetIterator::setIndexOrder(std::vector
<unsigned>& indexOrder
)
324 d_index_order
.clear();
325 d_index_order
.insert( d_index_order
.begin(), indexOrder
.begin(), indexOrder
.end() );
326 //make the d_var_order mapping
327 for( unsigned i
=0; i
<d_index_order
.size(); i
++ ){
328 d_var_order
[d_index_order
[i
]] = i
;
332 int RepSetIterator::resetIndex(unsigned i
, bool initial
)
335 unsigned v
= d_var_order
[i
];
336 Trace("bound-int-rsi") << "Reset " << i
<< ", var order = " << v
<< ", initial = " << initial
<< std::endl
;
339 if (!d_rext
->resetIndex(this, d_owner
, v
, initial
, d_domain_elements
[v
]))
344 return d_domain_elements
[v
].empty() ? 0 : 1;
347 int RepSetIterator::incrementAtIndex(int i
)
349 Assert(!isFinished());
350 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
351 i
= (int)d_index
.size()-1;
353 Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i
<< std::endl
;
356 Trace("rsi-debug") << "domain size of " << i
<< " is " << domainSize(i
) << std::endl
;
358 while( i
>=0 && d_index
[i
]>=(int)(domainSize(i
)-1) ){
361 Trace("rsi-debug") << "domain size of " << i
<< " is " << domainSize(i
) << std::endl
;
365 Trace("rsi-debug") << "increment failed" << std::endl
;
369 Trace("rsi-debug") << "increment " << i
<< std::endl
;
371 return do_reset_increment( i
);
375 int RepSetIterator::do_reset_increment( int i
, bool initial
) {
376 Trace("rsi-debug") << "RepSetIterator::do_reset_increment: " << i
377 << ", initial=" << initial
<< std::endl
;
378 for( unsigned ii
=(i
+1); ii
<d_index
.size(); ii
++ ){
379 bool emptyDomain
= false;
380 int ri_res
= resetIndex( ii
, initial
);
386 }else if( ri_res
==0 ){
389 //force next iteration if currently an empty domain
392 Trace("rsi-debug") << "This is an empty domain (index " << ii
<< ")."
396 // increment at the previous index
397 return incrementAtIndex(ii
- 1);
401 // this is the first index, we are done
407 Trace("rsi-debug") << "Finished, return " << i
<< std::endl
;
411 int RepSetIterator::increment(){
413 return incrementAtIndex(d_index
.size() - 1);
419 bool RepSetIterator::isFinished() const { return d_index
.empty(); }
421 Node
RepSetIterator::getCurrentTerm(unsigned i
, bool valTerm
) const
423 unsigned ii
= d_index_order
[i
];
424 unsigned curr
= d_index
[ii
];
425 Trace("rsi-debug") << "rsi : get term " << i
426 << ", index order = " << d_index_order
[i
] << std::endl
;
427 Trace("rsi-debug") << "rsi : curr = " << curr
<< " / "
428 << d_domain_elements
[i
].size() << std::endl
;
429 Assert(0 <= curr
&& curr
< d_domain_elements
[i
].size());
430 Node t
= d_domain_elements
[i
][curr
];
433 Node tt
= d_rs
->getTermForRepresentative(t
);
442 void RepSetIterator::getCurrentTerms(std::vector
<Node
>& terms
) const
444 for (unsigned i
= 0, size
= d_index_order
.size(); i
< size
; i
++)
446 terms
.push_back(getCurrentTerm(i
));
450 void RepSetIterator::debugPrint( const char* c
){
451 for( unsigned v
=0; v
<d_index
.size(); v
++ ){
452 Debug( c
) << v
<< " : " << getCurrentTerm( v
) << std::endl
;
456 void RepSetIterator::debugPrintSmall( const char* c
){
457 Debug( c
) << "RI: ";
458 for( unsigned v
=0; v
<d_index
.size(); v
++ ){
459 Debug( c
) << v
<< ": " << getCurrentTerm( v
) << " ";
461 Debug( c
) << std::endl
;
464 } /* CVC4::theory namespace */
465 } /* CVC4 namespace */