1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Enumerator for uninterpreted sorts and functions. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/builtin/type_enumerator.h" |
17 |
|
|
18 |
|
#include "theory/builtin/theory_builtin_rewriter.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace theory { |
22 |
|
namespace builtin { |
23 |
|
|
24 |
3009 |
UninterpretedSortEnumerator::UninterpretedSortEnumerator( |
25 |
3009 |
TypeNode type, TypeEnumeratorProperties* tep) |
26 |
3009 |
: TypeEnumeratorBase<UninterpretedSortEnumerator>(type), d_count(0) |
27 |
|
{ |
28 |
3009 |
Assert(type.getKind() == kind::SORT_TYPE); |
29 |
3009 |
d_has_fixed_bound = false; |
30 |
3009 |
Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl; |
31 |
3009 |
if (tep && tep->d_fixed_usort_card) |
32 |
|
{ |
33 |
2198 |
d_has_fixed_bound = true; |
34 |
2198 |
std::map<TypeNode, Integer>::iterator it = tep->d_fixed_card.find(type); |
35 |
2198 |
if (it != tep->d_fixed_card.end()) |
36 |
|
{ |
37 |
2198 |
d_fixed_bound = it->second; |
38 |
|
} |
39 |
|
else |
40 |
|
{ |
41 |
|
d_fixed_bound = Integer(1); |
42 |
|
} |
43 |
2198 |
Trace("uf-type-enum") << "...fixed bound : " << d_fixed_bound << std::endl; |
44 |
|
} |
45 |
3009 |
} |
46 |
|
|
47 |
18783 |
Node UninterpretedSortEnumerator::operator*() |
48 |
|
{ |
49 |
18783 |
if (isFinished()) |
50 |
|
{ |
51 |
2070 |
throw NoMoreValuesException(getType()); |
52 |
|
} |
53 |
|
return NodeManager::currentNM()->mkConst( |
54 |
16713 |
UninterpretedConstant(getType(), d_count)); |
55 |
|
} |
56 |
|
|
57 |
6835 |
UninterpretedSortEnumerator& UninterpretedSortEnumerator::operator++() |
58 |
|
{ |
59 |
6835 |
d_count += 1; |
60 |
6835 |
return *this; |
61 |
|
} |
62 |
|
|
63 |
44203 |
bool UninterpretedSortEnumerator::isFinished() |
64 |
|
{ |
65 |
44203 |
if (d_has_fixed_bound) |
66 |
|
{ |
67 |
32851 |
return d_count >= d_fixed_bound; |
68 |
|
} |
69 |
11352 |
return false; |
70 |
|
} |
71 |
|
|
72 |
|
} // namespace builtin |
73 |
|
} // namespace theory |
74 |
31137 |
} // namespace cvc5 |