1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed |
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 |
|
* Normal form for set constants. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__SETS__NORMAL_FORM_H |
19 |
|
#define CVC5__THEORY__SETS__NORMAL_FORM_H |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
namespace theory { |
23 |
|
namespace sets { |
24 |
|
|
25 |
|
class NormalForm { |
26 |
|
public: |
27 |
|
/** |
28 |
|
* Constructs a set of the form: |
29 |
|
* (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) |
30 |
|
* from the set { c1 ... cn }, also handles empty set case, which is why |
31 |
|
* setType is passed to this method. |
32 |
|
*/ |
33 |
|
template <bool ref_count> |
34 |
640 |
static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements, |
35 |
|
TypeNode setType) |
36 |
|
{ |
37 |
|
typedef typename std::set<NodeTemplate<ref_count> >::const_iterator |
38 |
|
ElementsIterator; |
39 |
640 |
NodeManager* nm = NodeManager::currentNM(); |
40 |
640 |
if (elements.size() == 0) |
41 |
|
{ |
42 |
43 |
return nm->mkConst(EmptySet(setType)); |
43 |
|
} |
44 |
|
else |
45 |
|
{ |
46 |
1194 |
TypeNode elementType = setType.getSetElementType(); |
47 |
597 |
ElementsIterator it = elements.begin(); |
48 |
1194 |
Node cur = nm->mkSingleton(elementType, *it); |
49 |
3845 |
while (++it != elements.end()) |
50 |
|
{ |
51 |
3248 |
Node singleton = nm->mkSingleton(elementType, *it); |
52 |
1624 |
cur = nm->mkNode(kind::UNION, singleton, cur); |
53 |
|
} |
54 |
597 |
return cur; |
55 |
|
} |
56 |
|
} |
57 |
|
|
58 |
|
/** |
59 |
|
* Returns true if n is considered a to be a (canonical) constant set value. |
60 |
|
* A canonical set value is one whose AST is: |
61 |
|
* (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) |
62 |
|
* where c1 ... cn are constants and the node identifier of these constants |
63 |
|
* are such that: |
64 |
|
* c1 > ... > cn. |
65 |
|
* Also handles the corner cases of empty set and singleton set. |
66 |
|
*/ |
67 |
4175 |
static bool checkNormalConstant(TNode n) { |
68 |
8350 |
Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :" |
69 |
4175 |
<< std::endl; |
70 |
4175 |
if (n.getKind() == kind::EMPTYSET) { |
71 |
|
return true; |
72 |
4175 |
} else if (n.getKind() == kind::SINGLETON) { |
73 |
|
return n[0].isConst(); |
74 |
4175 |
} else if (n.getKind() == kind::UNION) { |
75 |
|
// assuming (union {SmallestNodeID} ... (union {BiggerNodeId} ... |
76 |
|
|
77 |
4365 |
Node orig = n; |
78 |
4365 |
TNode prvs; |
79 |
|
// check intermediate nodes |
80 |
16533 |
while (n.getKind() == kind::UNION) |
81 |
|
{ |
82 |
8862 |
if (n[0].getKind() != kind::SINGLETON || !n[0][0].isConst()) |
83 |
|
{ |
84 |
|
// not a constant |
85 |
4954 |
Trace("sets-isconst") << "sets::isConst: " << orig << " not due to " |
86 |
2477 |
<< n[0] << std::endl; |
87 |
2477 |
return false; |
88 |
|
} |
89 |
12770 |
Debug("sets-checknormal") |
90 |
12770 |
<< "[sets-checknormal] element = " << n[0][0] << " " |
91 |
6385 |
<< n[0][0].getId() << std::endl; |
92 |
6385 |
if (!prvs.isNull() && n[0][0] >= prvs) |
93 |
|
{ |
94 |
412 |
Trace("sets-isconst") |
95 |
412 |
<< "sets::isConst: " << orig << " not due to compare " << n[0][0] |
96 |
206 |
<< std::endl; |
97 |
206 |
return false; |
98 |
|
} |
99 |
6179 |
prvs = n[0][0]; |
100 |
6179 |
n = n[1]; |
101 |
|
} |
102 |
|
|
103 |
|
// check SmallestNodeID is smallest |
104 |
1492 |
if (n.getKind() != kind::SINGLETON || !n[0].isConst()) |
105 |
|
{ |
106 |
186 |
Trace("sets-isconst") << "sets::isConst: " << orig |
107 |
93 |
<< " not due to final " << n << std::endl; |
108 |
93 |
return false; |
109 |
|
} |
110 |
2798 |
Debug("sets-checknormal") |
111 |
2798 |
<< "[sets-checknormal] lst element = " << n[0] << " " |
112 |
1399 |
<< n[0].getId() << std::endl; |
113 |
|
// compare last ID |
114 |
1399 |
if (n[0] < prvs) |
115 |
|
{ |
116 |
1209 |
return true; |
117 |
|
} |
118 |
380 |
Trace("sets-isconst") |
119 |
380 |
<< "sets::isConst: " << orig << " not due to compare final " << n[0] |
120 |
190 |
<< std::endl; |
121 |
|
} |
122 |
190 |
return false; |
123 |
|
} |
124 |
|
|
125 |
|
/** |
126 |
|
* Converts a set term to a std::set of its elements. This expects a set of |
127 |
|
* the form: |
128 |
|
* (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) |
129 |
|
* Also handles the corner cases of empty set and singleton set. |
130 |
|
*/ |
131 |
1338 |
static std::set<Node> getElementsFromNormalConstant(TNode n) { |
132 |
1338 |
Assert(n.isConst()); |
133 |
1338 |
std::set<Node> ret; |
134 |
1338 |
if (n.getKind() == kind::EMPTYSET) { |
135 |
92 |
return ret; |
136 |
|
} |
137 |
5184 |
while (n.getKind() == kind::UNION) { |
138 |
1969 |
Assert(n[0].getKind() == kind::SINGLETON); |
139 |
1969 |
ret.insert(ret.begin(), n[0][0]); |
140 |
1969 |
n = n[1]; |
141 |
|
} |
142 |
1246 |
Assert(n.getKind() == kind::SINGLETON); |
143 |
1246 |
ret.insert(n[0]); |
144 |
1246 |
return ret; |
145 |
|
} |
146 |
|
|
147 |
3907 |
static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){ |
148 |
3907 |
if( index>=els.size() ){ |
149 |
389 |
return NodeManager::currentNM()->mkConst(EmptySet(tn)); |
150 |
3518 |
}else if( index==els.size()-1 ){ |
151 |
2717 |
return els[index]; |
152 |
|
}else{ |
153 |
801 |
return NodeManager::currentNM()->mkNode( k, els[index], mkBop( k, els, tn, index+1 ) ); |
154 |
|
} |
155 |
|
} |
156 |
|
|
157 |
|
}; |
158 |
|
} |
159 |
|
} |
160 |
|
} // namespace cvc5 |
161 |
|
|
162 |
|
#endif |