1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mudathir Mohamed, Andres Noetzli |
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 |
|
* [[ Add one-line brief description here ]] |
13 |
|
* |
14 |
|
* [[ Add lengthier description here ]] |
15 |
|
* \todo document this file |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "theory/sep/theory_sep_rewriter.h" |
19 |
|
|
20 |
|
#include "expr/attribute.h" |
21 |
|
#include "expr/emptyset.h" |
22 |
|
#include "options/sep_options.h" |
23 |
|
#include "theory/quantifiers/quant_util.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
namespace theory { |
27 |
|
namespace sep { |
28 |
|
|
29 |
399 |
void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){ |
30 |
399 |
Assert(n.getKind() == kind::SEP_STAR); |
31 |
798 |
Node tr = NodeManager::currentNM()->mkConst( true ); |
32 |
1351 |
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
33 |
952 |
if( n[i].getKind()==kind::SEP_EMP ){ |
34 |
14 |
s_children.push_back( n[i] ); |
35 |
938 |
}else if( n[i].getKind()==kind::SEP_STAR ){ |
36 |
19 |
getStarChildren( n[i], s_children, ns_children ); |
37 |
919 |
}else if( n[i].getKind()==kind::SEP_PTO ){ |
38 |
677 |
s_children.push_back( n[i] ); |
39 |
|
}else{ |
40 |
484 |
std::vector< Node > temp_s_children; |
41 |
242 |
getAndChildren( n[i], temp_s_children, ns_children ); |
42 |
484 |
Node to_add; |
43 |
242 |
if( temp_s_children.size()==0 ){ |
44 |
60 |
if( std::find( s_children.begin(), s_children.end(), tr )==s_children.end() ){ |
45 |
59 |
to_add = tr; |
46 |
|
} |
47 |
182 |
}else if( temp_s_children.size()==1 ){ |
48 |
182 |
to_add = temp_s_children[0]; |
49 |
|
}else{ |
50 |
|
to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children ); |
51 |
|
} |
52 |
242 |
if( !to_add.isNull() ){ |
53 |
|
//flatten star |
54 |
241 |
if( to_add.getKind()==kind::SEP_STAR ){ |
55 |
|
getStarChildren( to_add, s_children, ns_children ); |
56 |
241 |
}else if( to_add.getKind()!=kind::SEP_EMP || s_children.empty() ){ //remove sep emp |
57 |
225 |
s_children.push_back( to_add ); |
58 |
|
} |
59 |
|
} |
60 |
|
} |
61 |
|
} |
62 |
399 |
} |
63 |
|
|
64 |
282 |
void TheorySepRewriter::getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ) { |
65 |
282 |
if( n.getKind()==kind::AND ){ |
66 |
60 |
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
67 |
40 |
getAndChildren( n[i], s_children, ns_children ); |
68 |
|
} |
69 |
|
}else{ |
70 |
524 |
std::map< Node, bool > visited; |
71 |
262 |
if( isSpatial( n, visited ) ){ |
72 |
182 |
if( std::find( s_children.begin(), s_children.end(), n )==s_children.end() ){ |
73 |
182 |
s_children.push_back( n ); |
74 |
|
} |
75 |
|
}else{ |
76 |
80 |
if( std::find( ns_children.begin(), ns_children.end(), n )==ns_children.end() ){ |
77 |
80 |
if( n!=NodeManager::currentNM()->mkConst(true) ){ |
78 |
22 |
ns_children.push_back( n ); |
79 |
|
} |
80 |
|
} |
81 |
|
} |
82 |
|
} |
83 |
282 |
} |
84 |
|
|
85 |
469 |
bool TheorySepRewriter::isSpatial( Node n, std::map< Node, bool >& visited ) { |
86 |
469 |
if( visited.find( n )==visited.end() ){ |
87 |
469 |
visited[n] = true; |
88 |
469 |
if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP || n.getKind()==kind::SEP_LABEL ){ |
89 |
182 |
return true; |
90 |
287 |
}else if( n.getType().isBoolean() ){ |
91 |
288 |
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
92 |
207 |
if( isSpatial( n[i], visited ) ){ |
93 |
162 |
return true; |
94 |
|
} |
95 |
|
} |
96 |
|
} |
97 |
|
} |
98 |
125 |
return false; |
99 |
|
} |
100 |
|
|
101 |
2993 |
RewriteResponse TheorySepRewriter::postRewrite(TNode node) { |
102 |
2993 |
Trace("sep-postrewrite") << "Sep::postRewrite start " << node << std::endl; |
103 |
5986 |
Node retNode = node; |
104 |
2993 |
switch (node.getKind()) { |
105 |
1537 |
case kind::SEP_LABEL: { |
106 |
1537 |
if( node[0].getKind()==kind::SEP_PTO ){ |
107 |
|
// TODO(project##230): Find a safe type for the singleton operator |
108 |
2252 |
Node s = NodeManager::currentNM()->mkSingleton(node[0][0].getType(), |
109 |
4504 |
node[0][0]); |
110 |
1126 |
if( node[1]!=s ){ |
111 |
1028 |
Node c1 = node[1].eqNode( s ); |
112 |
1028 |
Node c2 = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, node[0][0], node[0][1] ), s ); |
113 |
514 |
retNode = NodeManager::currentNM()->mkNode( kind::AND, c1, c2 ); |
114 |
|
} |
115 |
|
} |
116 |
1537 |
if( node[0].getKind()==kind::SEP_EMP ){ |
117 |
129 |
retNode = node[1].eqNode( |
118 |
86 |
NodeManager::currentNM()->mkConst(EmptySet(node[1].getType()))); |
119 |
|
} |
120 |
1537 |
break; |
121 |
|
} |
122 |
698 |
case kind::SEP_PTO: { |
123 |
698 |
break; |
124 |
|
} |
125 |
380 |
case kind::SEP_STAR: { |
126 |
|
//flatten |
127 |
760 |
std::vector< Node > s_children; |
128 |
760 |
std::vector< Node > ns_children; |
129 |
380 |
getStarChildren( node, s_children, ns_children ); |
130 |
380 |
if( !s_children.empty() ){ |
131 |
760 |
Node schild; |
132 |
380 |
if( s_children.size()==1 ) { |
133 |
9 |
schild = s_children[0]; |
134 |
|
}else{ |
135 |
371 |
schild = NodeManager::currentNM()->mkNode( kind::SEP_STAR, s_children ); |
136 |
|
} |
137 |
380 |
ns_children.push_back( schild ); |
138 |
|
} |
139 |
380 |
Assert(!ns_children.empty()); |
140 |
380 |
if( ns_children.size()==1 ){ |
141 |
367 |
retNode = ns_children[0]; |
142 |
|
}else{ |
143 |
13 |
retNode = NodeManager::currentNM()->mkNode( kind::AND, ns_children ); |
144 |
|
} |
145 |
380 |
break; |
146 |
|
} |
147 |
|
case kind::EQUAL: { |
148 |
|
if(node[0] == node[1]) { |
149 |
|
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); |
150 |
|
} |
151 |
|
else if (node[0].isConst() && node[1].isConst()) { |
152 |
|
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); |
153 |
|
} |
154 |
|
if (node[0] > node[1]) { |
155 |
|
Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); |
156 |
|
return RewriteResponse(REWRITE_DONE, newNode); |
157 |
|
} |
158 |
|
break; |
159 |
|
} |
160 |
378 |
default: |
161 |
378 |
break; |
162 |
|
} |
163 |
2993 |
if( node!=retNode ){ |
164 |
589 |
Trace("sep-rewrite") << "Sep::rewrite : " << node << " -> " << retNode << std::endl; |
165 |
|
} |
166 |
2993 |
return RewriteResponse(node==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); |
167 |
|
} |
168 |
|
|
169 |
|
} // namespace sep |
170 |
|
} // namespace theory |
171 |
29280 |
} // namespace cvc5 |