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 |
1067 |
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 |
1067 |
NodeManager* nm = NodeManager::currentNM(); |
42 |
1067 |
if (elements.size() == 0) |
43 |
|
{ |
44 |
86 |
return nm->mkConst(EmptySet(setType)); |
45 |
|
} |
46 |
|
else |
47 |
|
{ |
48 |
1962 |
TypeNode elementType = setType.getSetElementType(); |
49 |
981 |
ElementsIterator it = elements.begin(); |
50 |
1962 |
Node cur = nm->mkSingleton(elementType, *it); |
51 |
6179 |
while (++it != elements.end()) |
52 |
|
{ |
53 |
5198 |
Node singleton = nm->mkSingleton(elementType, *it); |
54 |
2599 |
cur = nm->mkNode(kind::UNION, singleton, cur); |
55 |
|
} |
56 |
981 |
return cur; |
57 |
|
} |
58 |
|
} |
59 |
|
|
60 |
|
/** |
61 |
|
* Returns true if n is considered 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 |
5561 |
static bool checkNormalConstant(TNode n) { |
70 |
11122 |
Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :" |
71 |
5561 |
<< std::endl; |
72 |
5561 |
if (n.getKind() == kind::EMPTYSET) { |
73 |
|
return true; |
74 |
5561 |
} else if (n.getKind() == kind::SINGLETON) { |
75 |
|
return n[0].isConst(); |
76 |
5561 |
} else if (n.getKind() == kind::UNION) { |
77 |
|
// assuming (union {SmallestNodeID} ... (union {BiggerNodeId} ... |
78 |
|
|
79 |
5841 |
Node orig = n; |
80 |
5841 |
TNode prvs; |
81 |
|
// check intermediate nodes |
82 |
21181 |
while (n.getKind() == kind::UNION) |
83 |
|
{ |
84 |
11286 |
if (n[0].getKind() != kind::SINGLETON || !n[0][0].isConst()) |
85 |
|
{ |
86 |
|
// not a constant |
87 |
5840 |
Trace("sets-isconst") << "sets::isConst: " << orig << " not due to " |
88 |
2920 |
<< n[0] << std::endl; |
89 |
2920 |
return false; |
90 |
|
} |
91 |
16732 |
Debug("sets-checknormal") |
92 |
16732 |
<< "[sets-checknormal] element = " << n[0][0] << " " |
93 |
8366 |
<< n[0][0].getId() << std::endl; |
94 |
8366 |
if (!prvs.isNull() && n[0][0] >= prvs) |
95 |
|
{ |
96 |
1112 |
Trace("sets-isconst") |
97 |
1112 |
<< "sets::isConst: " << orig << " not due to compare " << n[0][0] |
98 |
556 |
<< std::endl; |
99 |
556 |
return false; |
100 |
|
} |
101 |
7810 |
prvs = n[0][0]; |
102 |
7810 |
n = n[1]; |
103 |
|
} |
104 |
|
|
105 |
|
// check SmallestNodeID is smallest |
106 |
2085 |
if (n.getKind() != kind::SINGLETON || !n[0].isConst()) |
107 |
|
{ |
108 |
450 |
Trace("sets-isconst") << "sets::isConst: " << orig |
109 |
225 |
<< " not due to final " << n << std::endl; |
110 |
225 |
return false; |
111 |
|
} |
112 |
3720 |
Debug("sets-checknormal") |
113 |
3720 |
<< "[sets-checknormal] lst element = " << n[0] << " " |
114 |
1860 |
<< n[0].getId() << std::endl; |
115 |
|
// compare last ID |
116 |
1860 |
if (n[0] < prvs) |
117 |
|
{ |
118 |
1580 |
return true; |
119 |
|
} |
120 |
560 |
Trace("sets-isconst") |
121 |
560 |
<< "sets::isConst: " << orig << " not due to compare final " << n[0] |
122 |
280 |
<< std::endl; |
123 |
|
} |
124 |
280 |
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 |
2220 |
static std::set<Node> getElementsFromNormalConstant(TNode n) { |
134 |
2220 |
Assert(n.isConst()); |
135 |
2220 |
std::set<Node> ret; |
136 |
2220 |
if (n.getKind() == kind::EMPTYSET) { |
137 |
106 |
return ret; |
138 |
|
} |
139 |
7350 |
while (n.getKind() == kind::UNION) { |
140 |
2618 |
Assert(n[0].getKind() == kind::SINGLETON); |
141 |
2618 |
ret.insert(ret.begin(), n[0][0]); |
142 |
2618 |
n = n[1]; |
143 |
|
} |
144 |
2114 |
Assert(n.getKind() == kind::SINGLETON); |
145 |
2114 |
ret.insert(n[0]); |
146 |
2114 |
return ret; |
147 |
|
} |
148 |
|
|
149 |
14778 |
static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){ |
150 |
14778 |
if( index>=els.size() ){ |
151 |
667 |
return NodeManager::currentNM()->mkConst(EmptySet(tn)); |
152 |
14111 |
}else if( index==els.size()-1 ){ |
153 |
11463 |
return els[index]; |
154 |
|
}else{ |
155 |
2648 |
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 |