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 |
|
#include "expr/emptyset.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace sets { |
26 |
|
|
27 |
|
class NormalForm { |
28 |
|
public: |
29 |
|
/** |
30 |
|
* Constructs a set of the form: |
31 |
|
* (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) |
32 |
|
* from the set { c1 ... cn }, also handles empty set case, which is why |
33 |
|
* setType is passed to this method. |
34 |
|
*/ |
35 |
|
template <bool ref_count> |
36 |
579 |
static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements, |
37 |
|
TypeNode setType) |
38 |
|
{ |
39 |
|
typedef typename std::set<NodeTemplate<ref_count> >::const_iterator |
40 |
|
ElementsIterator; |
41 |
579 |
NodeManager* nm = NodeManager::currentNM(); |
42 |
579 |
if (elements.size() == 0) |
43 |
|
{ |
44 |
37 |
return nm->mkConst(EmptySet(setType)); |
45 |
|
} |
46 |
|
else |
47 |
|
{ |
48 |
1084 |
TypeNode elementType = setType.getSetElementType(); |
49 |
542 |
ElementsIterator it = elements.begin(); |
50 |
1084 |
Node cur = nm->mkSingleton(elementType, *it); |
51 |
3608 |
while (++it != elements.end()) |
52 |
|
{ |
53 |
3066 |
Node singleton = nm->mkSingleton(elementType, *it); |
54 |
1533 |
cur = nm->mkNode(kind::UNION, singleton, cur); |
55 |
|
} |
56 |
542 |
return cur; |
57 |
|
} |
58 |
|
} |
59 |
|
|
60 |
|
/** |
61 |
|
* Returns true if n is considered a to be a (canonical) constant set value. |
62 |
|
* A canonical set value is one whose AST is: |
63 |
|
* (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) |
64 |
|
* where c1 ... cn are constants and the node identifier of these constants |
65 |
|
* are such that: |
66 |
|
* c1 > ... > cn. |
67 |
|
* Also handles the corner cases of empty set and singleton set. |
68 |
|
*/ |
69 |
3108 |
static bool checkNormalConstant(TNode n) { |
70 |
6216 |
Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :" |
71 |
3108 |
<< std::endl; |
72 |
3108 |
if (n.getKind() == kind::EMPTYSET) { |
73 |
|
return true; |
74 |
3108 |
} else if (n.getKind() == kind::SINGLETON) { |
75 |
|
return n[0].isConst(); |
76 |
3108 |
} else if (n.getKind() == kind::UNION) { |
77 |
|
// assuming (union {SmallestNodeID} ... (union {BiggerNodeId} ... |
78 |
|
|
79 |
3261 |
Node orig = n; |
80 |
3261 |
TNode prvs; |
81 |
|
// check intermediate nodes |
82 |
15120 |
while (n.getKind() == kind::UNION) |
83 |
|
{ |
84 |
7740 |
if (n[0].getKind() != kind::SINGLETON || !n[0][0].isConst()) |
85 |
|
{ |
86 |
|
// not a constant |
87 |
3090 |
Trace("sets-isconst") << "sets::isConst: " << orig << " not due to " |
88 |
1545 |
<< n[0] << std::endl; |
89 |
1545 |
return false; |
90 |
|
} |
91 |
12390 |
Debug("sets-checknormal") |
92 |
12390 |
<< "[sets-checknormal] element = " << n[0][0] << " " |
93 |
6195 |
<< n[0][0].getId() << std::endl; |
94 |
6195 |
if (!prvs.isNull() && n[0][0] >= prvs) |
95 |
|
{ |
96 |
378 |
Trace("sets-isconst") |
97 |
378 |
<< "sets::isConst: " << orig << " not due to compare " << n[0][0] |
98 |
189 |
<< std::endl; |
99 |
189 |
return false; |
100 |
|
} |
101 |
6006 |
prvs = n[0][0]; |
102 |
6006 |
n = n[1]; |
103 |
|
} |
104 |
|
|
105 |
|
// check SmallestNodeID is smallest |
106 |
1374 |
if (n.getKind() != kind::SINGLETON || !n[0].isConst()) |
107 |
|
{ |
108 |
164 |
Trace("sets-isconst") << "sets::isConst: " << orig |
109 |
82 |
<< " not due to final " << n << std::endl; |
110 |
82 |
return false; |
111 |
|
} |
112 |
2584 |
Debug("sets-checknormal") |
113 |
2584 |
<< "[sets-checknormal] lst element = " << n[0] << " " |
114 |
1292 |
<< n[0].getId() << std::endl; |
115 |
|
// compare last ID |
116 |
1292 |
if (n[0] < prvs) |
117 |
|
{ |
118 |
1139 |
return true; |
119 |
|
} |
120 |
306 |
Trace("sets-isconst") |
121 |
306 |
<< "sets::isConst: " << orig << " not due to compare final " << n[0] |
122 |
153 |
<< std::endl; |
123 |
|
} |
124 |
153 |
return false; |
125 |
|
} |
126 |
|
|
127 |
|
/** |
128 |
|
* Converts a set term to a std::set of its elements. This expects a set of |
129 |
|
* the form: |
130 |
|
* (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) |
131 |
|
* Also handles the corner cases of empty set and singleton set. |
132 |
|
*/ |
133 |
1193 |
static std::set<Node> getElementsFromNormalConstant(TNode n) { |
134 |
1193 |
Assert(n.isConst()); |
135 |
1193 |
std::set<Node> ret; |
136 |
1193 |
if (n.getKind() == kind::EMPTYSET) { |
137 |
63 |
return ret; |
138 |
|
} |
139 |
5028 |
while (n.getKind() == kind::UNION) { |
140 |
1949 |
Assert(n[0].getKind() == kind::SINGLETON); |
141 |
1949 |
ret.insert(ret.begin(), n[0][0]); |
142 |
1949 |
n = n[1]; |
143 |
|
} |
144 |
1130 |
Assert(n.getKind() == kind::SINGLETON); |
145 |
1130 |
ret.insert(n[0]); |
146 |
1130 |
return ret; |
147 |
|
} |
148 |
|
|
149 |
2093 |
static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){ |
150 |
2093 |
if( index>=els.size() ){ |
151 |
240 |
return NodeManager::currentNM()->mkConst(EmptySet(tn)); |
152 |
1853 |
}else if( index==els.size()-1 ){ |
153 |
1252 |
return els[index]; |
154 |
|
}else{ |
155 |
601 |
return NodeManager::currentNM()->mkNode( k, els[index], mkBop( k, els, tn, index+1 ) ); |
156 |
|
} |
157 |
|
} |
158 |
|
|
159 |
|
}; |
160 |
|
} |
161 |
|
} |
162 |
|
} // namespace cvc5 |
163 |
|
|
164 |
|
#endif |