1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
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 |
|
* Implementation of techniques for sygus explanations. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/sygus/sygus_explain.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "smt/logic_exception.h" |
21 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
22 |
|
#include "theory/quantifiers/sygus/sygus_invariance.h" |
23 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
24 |
|
|
25 |
|
using namespace cvc5::kind; |
26 |
|
using namespace std; |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace quantifiers { |
31 |
|
|
32 |
61660 |
void TermRecBuild::addTerm(Node n) |
33 |
|
{ |
34 |
61660 |
d_term.push_back(n); |
35 |
123320 |
std::vector<Node> currc; |
36 |
61660 |
d_kind.push_back(n.getKind()); |
37 |
61660 |
if (n.getMetaKind() == kind::metakind::PARAMETERIZED) |
38 |
|
{ |
39 |
61636 |
currc.push_back(n.getOperator()); |
40 |
61636 |
d_has_op.push_back(true); |
41 |
|
} |
42 |
|
else |
43 |
|
{ |
44 |
24 |
d_has_op.push_back(false); |
45 |
|
} |
46 |
111713 |
for (unsigned i = 0; i < n.getNumChildren(); i++) |
47 |
|
{ |
48 |
50053 |
currc.push_back(n[i]); |
49 |
|
} |
50 |
61660 |
d_children.push_back(currc); |
51 |
61660 |
} |
52 |
|
|
53 |
13804 |
void TermRecBuild::init(Node n) |
54 |
|
{ |
55 |
13804 |
Assert(d_term.empty()); |
56 |
13804 |
addTerm(n); |
57 |
13804 |
} |
58 |
|
|
59 |
47856 |
void TermRecBuild::push(unsigned p) |
60 |
|
{ |
61 |
47856 |
Assert(!d_term.empty()); |
62 |
47856 |
unsigned curr = d_term.size() - 1; |
63 |
47856 |
Assert(d_pos.size() == curr); |
64 |
47856 |
Assert(d_pos.size() + 1 == d_children.size()); |
65 |
47856 |
Assert(p < d_term[curr].getNumChildren()); |
66 |
47856 |
addTerm(d_term[curr][p]); |
67 |
47856 |
d_pos.push_back(p); |
68 |
47856 |
} |
69 |
|
|
70 |
47856 |
void TermRecBuild::pop() |
71 |
|
{ |
72 |
47856 |
Assert(!d_pos.empty()); |
73 |
47856 |
d_pos.pop_back(); |
74 |
47856 |
d_kind.pop_back(); |
75 |
47856 |
d_has_op.pop_back(); |
76 |
47856 |
d_children.pop_back(); |
77 |
47856 |
d_term.pop_back(); |
78 |
47856 |
} |
79 |
|
|
80 |
97866 |
void TermRecBuild::replaceChild(unsigned i, Node r) |
81 |
|
{ |
82 |
97866 |
Assert(!d_term.empty()); |
83 |
97866 |
unsigned curr = d_term.size() - 1; |
84 |
97866 |
unsigned o = d_has_op[curr] ? 1 : 0; |
85 |
97866 |
d_children[curr][i + o] = r; |
86 |
97866 |
} |
87 |
|
|
88 |
|
Node TermRecBuild::getChild(unsigned i) |
89 |
|
{ |
90 |
|
unsigned curr = d_term.size() - 1; |
91 |
|
unsigned o = d_has_op[curr] ? 1 : 0; |
92 |
|
return d_children[curr][i + o]; |
93 |
|
} |
94 |
|
|
95 |
83276 |
Node TermRecBuild::build(unsigned d) |
96 |
|
{ |
97 |
83276 |
Assert(d_pos.size() + 1 == d_term.size()); |
98 |
83276 |
Assert(d < d_term.size()); |
99 |
83276 |
int p = d < d_pos.size() ? d_pos[d] : -2; |
100 |
166552 |
std::vector<Node> children; |
101 |
83276 |
unsigned o = d_has_op[d] ? 1 : 0; |
102 |
334288 |
for (unsigned i = 0; i < d_children[d].size(); i++) |
103 |
|
{ |
104 |
502024 |
Node nc; |
105 |
251012 |
if (p + o == i) |
106 |
|
{ |
107 |
33266 |
nc = build(d + 1); |
108 |
|
} |
109 |
|
else |
110 |
|
{ |
111 |
217746 |
nc = d_children[d][i]; |
112 |
|
} |
113 |
251012 |
children.push_back(nc); |
114 |
|
} |
115 |
166552 |
return NodeManager::currentNM()->mkNode(d_kind[d], children); |
116 |
|
} |
117 |
|
|
118 |
26984 |
void SygusExplain::getExplanationForEquality(Node n, |
119 |
|
Node vn, |
120 |
|
std::vector<Node>& exp) |
121 |
|
{ |
122 |
53968 |
std::map<unsigned, bool> cexc; |
123 |
26984 |
getExplanationForEquality(n, vn, exp, cexc); |
124 |
26984 |
} |
125 |
|
|
126 |
27216 |
void SygusExplain::getExplanationForEquality(Node n, |
127 |
|
Node vn, |
128 |
|
std::vector<Node>& exp, |
129 |
|
std::map<unsigned, bool>& cexc) |
130 |
|
{ |
131 |
|
// since builtin types occur in grammar, types are comparable but not |
132 |
|
// necessarily equal |
133 |
27216 |
Assert(n.getType().isComparableTo(n.getType())); |
134 |
27216 |
if (n == vn) |
135 |
|
{ |
136 |
377 |
return; |
137 |
|
} |
138 |
54055 |
TypeNode tn = n.getType(); |
139 |
27216 |
if (!tn.isDatatype()) |
140 |
|
{ |
141 |
|
// sygus datatype fields that are not sygus datatypes are treated as |
142 |
|
// abstractions only, hence we disregard this field |
143 |
377 |
return; |
144 |
|
} |
145 |
26839 |
Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); |
146 |
26839 |
const DType& dt = tn.getDType(); |
147 |
26839 |
int i = datatypes::utils::indexOf(vn.getOperator()); |
148 |
53678 |
Node tst = datatypes::utils::mkTester(n, i, dt); |
149 |
26839 |
exp.push_back(tst); |
150 |
44886 |
for (unsigned j = 0; j < vn.getNumChildren(); j++) |
151 |
|
{ |
152 |
18047 |
if (cexc.find(j) == cexc.end()) |
153 |
|
{ |
154 |
|
Node sel = NodeManager::currentNM()->mkNode( |
155 |
36094 |
kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n); |
156 |
18047 |
getExplanationForEquality(sel, vn[j], exp); |
157 |
|
} |
158 |
|
} |
159 |
|
} |
160 |
|
|
161 |
232 |
Node SygusExplain::getExplanationForEquality(Node n, Node vn) |
162 |
|
{ |
163 |
464 |
std::map<unsigned, bool> cexc; |
164 |
464 |
return getExplanationForEquality(n, vn, cexc); |
165 |
|
} |
166 |
|
|
167 |
232 |
Node SygusExplain::getExplanationForEquality(Node n, |
168 |
|
Node vn, |
169 |
|
std::map<unsigned, bool>& cexc) |
170 |
|
{ |
171 |
464 |
std::vector<Node> exp; |
172 |
232 |
getExplanationForEquality(n, vn, exp, cexc); |
173 |
232 |
Assert(!exp.empty()); |
174 |
339 |
return exp.size() == 1 ? exp[0] |
175 |
571 |
: NodeManager::currentNM()->mkNode(kind::AND, exp); |
176 |
|
} |
177 |
|
|
178 |
|
// we have ( n = vn => eval( n ) = bvr ) ^ vn != vnr , returns exp such that exp |
179 |
|
// => ( eval( n ) = bvr ^ vn != vnr ) |
180 |
61660 |
void SygusExplain::getExplanationFor(TermRecBuild& trb, |
181 |
|
Node n, |
182 |
|
Node vn, |
183 |
|
std::vector<Node>& exp, |
184 |
|
std::map<TypeNode, int>& var_count, |
185 |
|
SygusInvarianceTest& et, |
186 |
|
Node vnr, |
187 |
|
Node& vnr_exp, |
188 |
|
int& sz) |
189 |
|
{ |
190 |
61660 |
Assert(vnr.isNull() || vn != vnr); |
191 |
61660 |
Assert(n.getType().isComparableTo(vn.getType())); |
192 |
123253 |
TypeNode ntn = n.getType(); |
193 |
61660 |
if (!ntn.isDatatype()) |
194 |
|
{ |
195 |
|
// SyGuS datatype fields that are not sygus datatypes are treated as |
196 |
|
// abstractions only, hence we disregard this field. It is important |
197 |
|
// that users of this method pay special attention to any constants, |
198 |
|
// otherwise the explanation n.eqNode(vn) is necessary here. For example, |
199 |
|
// any lemma schema that blocks the current value of an enumerator should |
200 |
|
// not make any assumptions about the value of the arguments of its any |
201 |
|
// constant constructors, since their explanation is not included here. |
202 |
67 |
return; |
203 |
|
} |
204 |
61593 |
Assert(vn.getKind() == APPLY_CONSTRUCTOR); |
205 |
61593 |
Assert(vnr.isNull() || vnr.getKind() == APPLY_CONSTRUCTOR); |
206 |
123186 |
std::map<unsigned, bool> cexc; |
207 |
|
// for each child, |
208 |
|
// check whether replacing that child by a fresh variable |
209 |
|
// also satisfies the invariance test. |
210 |
111603 |
for (unsigned i = 0; i < vn.getNumChildren(); i++) |
211 |
|
{ |
212 |
100020 |
TypeNode xtn = vn[i].getType(); |
213 |
100020 |
Node x = d_tdb->getFreeVarInc(xtn, var_count); |
214 |
50010 |
trb.replaceChild(i, x); |
215 |
100020 |
Node nvn = trb.build(); |
216 |
50010 |
Assert(nvn.getKind() == kind::APPLY_CONSTRUCTOR); |
217 |
50010 |
if (et.is_invariant(d_tdb, nvn, x)) |
218 |
|
{ |
219 |
2154 |
cexc[i] = true; |
220 |
|
// we are tracking term size if positive |
221 |
2154 |
if (sz >= 0) |
222 |
|
{ |
223 |
216 |
int s = d_tdb->getSygusTermSize(vn[i]); |
224 |
216 |
sz = sz - s; |
225 |
|
} |
226 |
|
} |
227 |
|
else |
228 |
|
{ |
229 |
|
// revert |
230 |
47856 |
trb.replaceChild(i, vn[i]); |
231 |
|
} |
232 |
|
} |
233 |
61593 |
const DType& dt = ntn.getDType(); |
234 |
61593 |
int cindex = datatypes::utils::indexOf(vn.getOperator()); |
235 |
61593 |
Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); |
236 |
123186 |
Node tst = datatypes::utils::mkTester(n, cindex, dt); |
237 |
61593 |
exp.push_back(tst); |
238 |
|
// if the operator of vn is different than vnr, then disunification obligation |
239 |
|
// is met |
240 |
61593 |
if (!vnr.isNull()) |
241 |
|
{ |
242 |
3100 |
if (vnr.getOperator() != vn.getOperator()) |
243 |
|
{ |
244 |
1692 |
vnr = Node::null(); |
245 |
1692 |
vnr_exp = NodeManager::currentNM()->mkConst(true); |
246 |
|
} |
247 |
|
} |
248 |
111603 |
for (unsigned i = 0; i < vn.getNumChildren(); i++) |
249 |
|
{ |
250 |
|
Node sel = NodeManager::currentNM()->mkNode( |
251 |
100020 |
kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n); |
252 |
100020 |
Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]); |
253 |
50010 |
if (cexc.find(i) == cexc.end()) |
254 |
|
{ |
255 |
47856 |
trb.push(i); |
256 |
95712 |
Node vnr_exp_c; |
257 |
47856 |
getExplanationFor( |
258 |
|
trb, sel, vn[i], exp, var_count, et, vnr_c, vnr_exp_c, sz); |
259 |
47856 |
trb.pop(); |
260 |
47856 |
if (!vnr_c.isNull()) |
261 |
|
{ |
262 |
1405 |
Assert(!vnr_exp_c.isNull()); |
263 |
1405 |
if (vnr_exp_c.isConst() || vnr_exp.isNull()) |
264 |
|
{ |
265 |
|
// recursively satisfied the disunification obligation |
266 |
1405 |
if (vnr_exp_c.isConst()) |
267 |
|
{ |
268 |
|
// was successful, don't consider further |
269 |
1405 |
vnr = Node::null(); |
270 |
|
} |
271 |
1405 |
vnr_exp = vnr_exp_c; |
272 |
|
} |
273 |
|
} |
274 |
|
} |
275 |
|
else |
276 |
|
{ |
277 |
|
// if excluded, we may need to add the explanation for this |
278 |
2154 |
if (vnr_exp.isNull() && !vnr_c.isNull()) |
279 |
|
{ |
280 |
4 |
vnr_exp = getExplanationForEquality(sel, vnr[i]); |
281 |
|
} |
282 |
|
} |
283 |
|
} |
284 |
|
} |
285 |
|
|
286 |
|
void SygusExplain::getExplanationFor(Node n, |
287 |
|
Node vn, |
288 |
|
std::vector<Node>& exp, |
289 |
|
SygusInvarianceTest& et, |
290 |
|
Node vnr, |
291 |
|
unsigned& sz) |
292 |
|
{ |
293 |
|
std::map<TypeNode, int> var_count; |
294 |
|
return getExplanationFor(n, vn, exp, et, vnr, var_count, sz); |
295 |
|
} |
296 |
|
|
297 |
1695 |
void SygusExplain::getExplanationFor(Node n, |
298 |
|
Node vn, |
299 |
|
std::vector<Node>& exp, |
300 |
|
SygusInvarianceTest& et, |
301 |
|
Node vnr, |
302 |
|
std::map<TypeNode, int>& var_count, |
303 |
|
unsigned& sz) |
304 |
|
{ |
305 |
|
// naive : |
306 |
|
// return getExplanationForEquality( n, vn, exp ); |
307 |
|
|
308 |
|
// set up the recursion object; |
309 |
3390 |
TermRecBuild trb; |
310 |
1695 |
trb.init(vn); |
311 |
3390 |
Node vnr_exp; |
312 |
1695 |
int sz_use = sz; |
313 |
1695 |
getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz_use); |
314 |
1695 |
Assert(sz_use >= 0); |
315 |
1695 |
sz = sz_use; |
316 |
1695 |
Assert(vnr.isNull() || !vnr_exp.isNull()); |
317 |
1695 |
if (!vnr_exp.isNull() && !vnr_exp.isConst()) |
318 |
|
{ |
319 |
3 |
exp.push_back(vnr_exp.negate()); |
320 |
|
} |
321 |
1695 |
} |
322 |
|
|
323 |
7454 |
void SygusExplain::getExplanationFor(Node n, |
324 |
|
Node vn, |
325 |
|
std::vector<Node>& exp, |
326 |
|
SygusInvarianceTest& et, |
327 |
|
bool strict) |
328 |
|
{ |
329 |
14908 |
std::map<TypeNode, int> var_count; |
330 |
7454 |
getExplanationFor(n, vn, exp, et, var_count, strict); |
331 |
7454 |
} |
332 |
|
|
333 |
14572 |
void SygusExplain::getExplanationFor(Node n, |
334 |
|
Node vn, |
335 |
|
std::vector<Node>& exp, |
336 |
|
SygusInvarianceTest& et, |
337 |
|
std::map<TypeNode, int>& var_count, |
338 |
|
bool strict) |
339 |
|
{ |
340 |
14572 |
if (!strict) |
341 |
|
{ |
342 |
|
// check if it is invariant over the entire node |
343 |
11773 |
TypeNode vtn = vn.getType(); |
344 |
11773 |
Node x = d_tdb->getFreeVarInc(vtn, var_count); |
345 |
7118 |
if (et.is_invariant(d_tdb, x, x)) |
346 |
|
{ |
347 |
2463 |
return; |
348 |
|
} |
349 |
4655 |
var_count[vtn]--; |
350 |
|
} |
351 |
12109 |
int sz = -1; |
352 |
24218 |
TermRecBuild trb; |
353 |
12109 |
trb.init(vn); |
354 |
24218 |
Node vnr; |
355 |
24218 |
Node vnr_exp; |
356 |
12109 |
getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz); |
357 |
|
} |
358 |
|
|
359 |
|
} // namespace quantifiers |
360 |
|
} // namespace theory |
361 |
28194 |
} // namespace cvc5 |