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