1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Haniel Barbosa, Mathias Preiner |
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 simple symmetry breaking for sygus. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/datatypes/sygus_simple_sym.h" |
17 |
|
|
18 |
|
#include "expr/dtype_cons.h" |
19 |
|
#include "theory/quantifiers/term_util.h" |
20 |
|
|
21 |
|
using namespace std; |
22 |
|
using namespace cvc5::kind; |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace datatypes { |
27 |
|
|
28 |
1529 |
SygusSimpleSymBreak::SygusSimpleSymBreak(quantifiers::TermDbSygus* tds) |
29 |
1529 |
: d_tds(tds) |
30 |
|
{ |
31 |
1529 |
} |
32 |
|
|
33 |
|
/** Requirement trie |
34 |
|
* |
35 |
|
* This class is used to make queries about sygus grammars, including what |
36 |
|
* constructors they contain, and their types. |
37 |
|
* |
38 |
|
* As a simple example, consider the trie: |
39 |
|
* root: |
40 |
|
* d_req_kind = PLUS |
41 |
|
* d_children[0]: |
42 |
|
* d_req_type = A |
43 |
|
* d_children[1]: |
44 |
|
* d_req_type = A |
45 |
|
* This trie is satisfied by sygus types that have a constructor whose builtin |
46 |
|
* kind is PLUS and whose argument types are both A. |
47 |
|
*/ |
48 |
7087 |
class ReqTrie |
49 |
|
{ |
50 |
|
public: |
51 |
7087 |
ReqTrie() : d_req_kind(UNDEFINED_KIND) {} |
52 |
|
/** the children of this node */ |
53 |
|
std::map<unsigned, ReqTrie> d_children; |
54 |
|
/** the (builtin) kind required by this node */ |
55 |
|
Kind d_req_kind; |
56 |
|
/** the type that this node is required to be */ |
57 |
|
TypeNode d_req_type; |
58 |
|
/** the constant required by this node */ |
59 |
|
Node d_req_const; |
60 |
|
/** print this trie */ |
61 |
4261 |
void print(const char* c, int indent = 0) |
62 |
|
{ |
63 |
4261 |
if (d_req_kind != UNDEFINED_KIND) |
64 |
|
{ |
65 |
1665 |
Trace(c) << d_req_kind << " "; |
66 |
|
} |
67 |
2596 |
else if (!d_req_type.isNull()) |
68 |
|
{ |
69 |
2584 |
Trace(c) << d_req_type; |
70 |
|
} |
71 |
12 |
else if (!d_req_const.isNull()) |
72 |
|
{ |
73 |
12 |
Trace(c) << d_req_const; |
74 |
|
} |
75 |
|
else |
76 |
|
{ |
77 |
|
Trace(c) << "_"; |
78 |
|
} |
79 |
4261 |
Trace(c) << std::endl; |
80 |
7814 |
for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin(); |
81 |
7814 |
it != d_children.end(); |
82 |
|
++it) |
83 |
|
{ |
84 |
8990 |
for (int i = 0; i <= indent; i++) |
85 |
|
{ |
86 |
5437 |
Trace(c) << " "; |
87 |
|
} |
88 |
3553 |
Trace(c) << it->first << " : "; |
89 |
3553 |
it->second.print(c, indent + 1); |
90 |
|
} |
91 |
4261 |
} |
92 |
|
/** |
93 |
|
* Are the requirements of this trie satisfied by sygus type tn? |
94 |
|
* tdb is a reference to the sygus term database. |
95 |
|
*/ |
96 |
4168 |
bool satisfiedBy(quantifiers::TermDbSygus* tdb, TypeNode tn) |
97 |
|
{ |
98 |
4168 |
if (!d_req_const.isNull()) |
99 |
|
{ |
100 |
12 |
quantifiers::SygusTypeInfo& sti = tdb->getTypeInfo(tn); |
101 |
12 |
if (!sti.hasConst(d_req_const)) |
102 |
|
{ |
103 |
2 |
return false; |
104 |
|
} |
105 |
|
} |
106 |
4166 |
if (!d_req_type.isNull()) |
107 |
|
{ |
108 |
4948 |
Trace("sygus-sb-debug") |
109 |
2474 |
<< "- check if " << tn << " is type " << d_req_type << std::endl; |
110 |
2474 |
if (tn != d_req_type) |
111 |
|
{ |
112 |
14 |
return false; |
113 |
|
} |
114 |
|
} |
115 |
4152 |
if (d_req_kind != UNDEFINED_KIND) |
116 |
|
{ |
117 |
3252 |
Trace("sygus-sb-debug") |
118 |
1626 |
<< "- check if " << tn << " has " << d_req_kind << std::endl; |
119 |
3185 |
std::vector<TypeNode> argts; |
120 |
1626 |
if (tdb->canConstructKind(tn, d_req_kind, argts)) |
121 |
|
{ |
122 |
4963 |
for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin(); |
123 |
4963 |
it != d_children.end(); |
124 |
|
++it) |
125 |
|
{ |
126 |
3404 |
if (it->first < argts.size()) |
127 |
|
{ |
128 |
6782 |
TypeNode tnc = argts[it->first]; |
129 |
3404 |
if (!it->second.satisfiedBy(tdb, tnc)) |
130 |
|
{ |
131 |
26 |
return false; |
132 |
|
} |
133 |
|
} |
134 |
|
else |
135 |
|
{ |
136 |
|
return false; |
137 |
|
} |
138 |
|
} |
139 |
|
} |
140 |
|
else |
141 |
|
{ |
142 |
41 |
return false; |
143 |
|
} |
144 |
|
} |
145 |
4085 |
return true; |
146 |
|
} |
147 |
|
/** is this the empty (trivially satisfied) trie? */ |
148 |
7074 |
bool empty() |
149 |
|
{ |
150 |
13388 |
return d_req_kind == UNDEFINED_KIND && d_req_const.isNull() |
151 |
13388 |
&& d_req_type.isNull() && d_children.empty(); |
152 |
|
} |
153 |
|
}; |
154 |
|
|
155 |
2810 |
bool SygusSimpleSymBreak::considerArgKind( |
156 |
|
TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg) |
157 |
|
{ |
158 |
2810 |
const DType& pdt = tnp.getDType(); |
159 |
2810 |
const DType& dt = tn.getDType(); |
160 |
2810 |
quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn); |
161 |
2810 |
quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp); |
162 |
2810 |
Assert(ti.hasKind(k)); |
163 |
2810 |
Assert(pti.hasKind(pk)); |
164 |
5620 |
Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk |
165 |
2810 |
<< ", arg = " << arg << " in " << tnp << "?" |
166 |
2810 |
<< std::endl; |
167 |
2810 |
int c = ti.getKindConsNum(k); |
168 |
2810 |
int pc = pti.getKindConsNum(pk); |
169 |
|
// check for associativity |
170 |
2810 |
if (k == pk && quantifiers::TermUtil::isAssoc(k)) |
171 |
|
{ |
172 |
|
// if the operator is associative, then a repeated occurrence should only |
173 |
|
// occur in the leftmost argument position |
174 |
238 |
int firstArg = getFirstArgOccurrence(pdt[pc], tn); |
175 |
238 |
Assert(firstArg != -1); |
176 |
238 |
if (arg == firstArg) |
177 |
|
{ |
178 |
120 |
return true; |
179 |
|
} |
180 |
|
// the argument types of the child must be the parent's type |
181 |
344 |
for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++) |
182 |
|
{ |
183 |
457 |
TypeNode type = dt[c].getArgType(i); |
184 |
231 |
if (type != tnp) |
185 |
|
{ |
186 |
5 |
return true; |
187 |
|
} |
188 |
|
} |
189 |
226 |
Trace("sygus-sb-simple") |
190 |
113 |
<< " sb-simple : do not consider " << k << " at child arg " << arg |
191 |
113 |
<< " of " << k |
192 |
113 |
<< " since it is associative, with first arg = " << firstArg |
193 |
113 |
<< std::endl; |
194 |
113 |
return false; |
195 |
|
} |
196 |
|
// describes the shape of an alternate term to construct |
197 |
|
// we check whether this term is in the sygus grammar below |
198 |
5144 |
ReqTrie rt; |
199 |
2572 |
Assert(rt.empty()); |
200 |
|
|
201 |
|
// construct rt by cases |
202 |
2572 |
if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG) |
203 |
|
{ |
204 |
|
// negation normal form |
205 |
141 |
if (pk == k) |
206 |
|
{ |
207 |
23 |
rt.d_req_type = dt[c].getArgType(0); |
208 |
|
} |
209 |
|
else |
210 |
|
{ |
211 |
118 |
Kind reqk = UNDEFINED_KIND; // required kind for all children |
212 |
236 |
std::map<unsigned, Kind> reqkc; // required kind for some children |
213 |
118 |
if (pk == NOT) |
214 |
|
{ |
215 |
81 |
if (k == AND) |
216 |
|
{ |
217 |
19 |
rt.d_req_kind = OR; |
218 |
19 |
reqk = NOT; |
219 |
|
} |
220 |
62 |
else if (k == OR) |
221 |
|
{ |
222 |
18 |
rt.d_req_kind = AND; |
223 |
18 |
reqk = NOT; |
224 |
|
} |
225 |
44 |
else if (k == EQUAL) |
226 |
|
{ |
227 |
17 |
rt.d_req_kind = XOR; |
228 |
|
} |
229 |
27 |
else if (k == XOR) |
230 |
|
{ |
231 |
2 |
rt.d_req_kind = EQUAL; |
232 |
|
} |
233 |
25 |
else if (k == ITE) |
234 |
|
{ |
235 |
1 |
rt.d_req_kind = ITE; |
236 |
1 |
reqkc[1] = NOT; |
237 |
1 |
reqkc[2] = NOT; |
238 |
1 |
rt.d_children[0].d_req_type = dt[c].getArgType(0); |
239 |
|
} |
240 |
24 |
else if (k == LEQ || k == GT) |
241 |
|
{ |
242 |
|
// (not (~ x y)) -----> (~ (+ y 1) x) |
243 |
12 |
rt.d_req_kind = k; |
244 |
12 |
rt.d_children[0].d_req_kind = PLUS; |
245 |
12 |
rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1); |
246 |
24 |
rt.d_children[0].d_children[1].d_req_const = |
247 |
36 |
NodeManager::currentNM()->mkConst(Rational(1)); |
248 |
12 |
rt.d_children[1].d_req_type = dt[c].getArgType(0); |
249 |
|
} |
250 |
12 |
else if (k == LT || k == GEQ) |
251 |
|
{ |
252 |
|
// (not (~ x y)) -----> (~ y (+ x 1)) |
253 |
|
rt.d_req_kind = k; |
254 |
|
rt.d_children[0].d_req_type = dt[c].getArgType(1); |
255 |
|
rt.d_children[1].d_req_kind = PLUS; |
256 |
|
rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0); |
257 |
|
rt.d_children[1].d_children[1].d_req_const = |
258 |
|
NodeManager::currentNM()->mkConst(Rational(1)); |
259 |
|
} |
260 |
|
} |
261 |
37 |
else if (pk == BITVECTOR_NOT) |
262 |
|
{ |
263 |
22 |
if (k == BITVECTOR_AND) |
264 |
|
{ |
265 |
2 |
rt.d_req_kind = BITVECTOR_OR; |
266 |
2 |
reqk = BITVECTOR_NOT; |
267 |
|
} |
268 |
20 |
else if (k == BITVECTOR_OR) |
269 |
|
{ |
270 |
2 |
rt.d_req_kind = BITVECTOR_AND; |
271 |
2 |
reqk = BITVECTOR_NOT; |
272 |
|
} |
273 |
18 |
else if (k == BITVECTOR_XNOR) |
274 |
|
{ |
275 |
|
rt.d_req_kind = BITVECTOR_XOR; |
276 |
|
} |
277 |
18 |
else if (k == BITVECTOR_XOR) |
278 |
|
{ |
279 |
2 |
rt.d_req_kind = BITVECTOR_XNOR; |
280 |
|
} |
281 |
|
} |
282 |
15 |
else if (pk == UMINUS) |
283 |
|
{ |
284 |
|
if (k == PLUS) |
285 |
|
{ |
286 |
|
rt.d_req_kind = PLUS; |
287 |
|
reqk = UMINUS; |
288 |
|
} |
289 |
|
} |
290 |
15 |
else if (pk == BITVECTOR_NEG) |
291 |
|
{ |
292 |
15 |
if (k == PLUS) |
293 |
|
{ |
294 |
|
rt.d_req_kind = PLUS; |
295 |
|
reqk = BITVECTOR_NEG; |
296 |
|
} |
297 |
|
} |
298 |
118 |
if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty())) |
299 |
|
{ |
300 |
42 |
int pcr = pti.getKindConsNum(rt.d_req_kind); |
301 |
42 |
if (pcr != -1) |
302 |
|
{ |
303 |
39 |
Assert(pcr < static_cast<int>(pdt.getNumConstructors())); |
304 |
|
// must have same number of arguments |
305 |
39 |
if (pdt[pcr].getNumArgs() == dt[c].getNumArgs()) |
306 |
|
{ |
307 |
118 |
for (unsigned i = 0, nargs = pdt[pcr].getNumArgs(); i < nargs; i++) |
308 |
|
{ |
309 |
79 |
Kind rk = reqk; |
310 |
79 |
if (reqk == UNDEFINED_KIND) |
311 |
|
{ |
312 |
3 |
std::map<unsigned, Kind>::iterator itr = reqkc.find(i); |
313 |
3 |
if (itr != reqkc.end()) |
314 |
|
{ |
315 |
2 |
rk = itr->second; |
316 |
|
} |
317 |
|
} |
318 |
79 |
if (rk != UNDEFINED_KIND) |
319 |
|
{ |
320 |
78 |
rt.d_children[i].d_req_kind = rk; |
321 |
78 |
rt.d_children[i].d_children[0].d_req_type = dt[c].getArgType(i); |
322 |
|
} |
323 |
|
} |
324 |
|
} |
325 |
|
} |
326 |
|
} |
327 |
141 |
} |
328 |
|
} |
329 |
2431 |
else if (k == MINUS || k == BITVECTOR_SUB) |
330 |
|
{ |
331 |
350 |
if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ |
332 |
156 |
|| pk == LT || pk == GEQ || pk == GT) |
333 |
|
{ |
334 |
194 |
int oarg = arg == 0 ? 1 : 0; |
335 |
|
// (~ x (- y z)) ----> (~ (+ x z) y) |
336 |
|
// (~ (- y z) x) ----> (~ y (+ x z)) |
337 |
194 |
rt.d_req_kind = pk; |
338 |
194 |
rt.d_children[arg].d_req_type = dt[c].getArgType(0); |
339 |
194 |
rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_ADD; |
340 |
194 |
rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg); |
341 |
194 |
rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1); |
342 |
|
} |
343 |
156 |
else if (pk == PLUS || pk == BITVECTOR_ADD) |
344 |
|
{ |
345 |
|
// (+ x (- y z)) -----> (- (+ x y) z) |
346 |
|
// (+ (- y z) x) -----> (- (+ x y) z) |
347 |
70 |
rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB; |
348 |
70 |
int oarg = arg == 0 ? 1 : 0; |
349 |
70 |
rt.d_children[0].d_req_kind = pk; |
350 |
70 |
rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg); |
351 |
70 |
rt.d_children[0].d_children[1].d_req_type = dt[c].getArgType(0); |
352 |
70 |
rt.d_children[1].d_req_type = dt[c].getArgType(1); |
353 |
350 |
} |
354 |
|
} |
355 |
2081 |
else if (k == ITE) |
356 |
|
{ |
357 |
388 |
if (pk != ITE) |
358 |
|
{ |
359 |
|
// (o X (ite y z w) X') -----> (ite y (o X z X') (o X w X')) |
360 |
313 |
rt.d_req_kind = ITE; |
361 |
313 |
rt.d_children[0].d_req_type = dt[c].getArgType(0); |
362 |
313 |
unsigned n_args = pdt[pc].getNumArgs(); |
363 |
939 |
for (unsigned r = 1; r <= 2; r++) |
364 |
|
{ |
365 |
626 |
rt.d_children[r].d_req_kind = pk; |
366 |
1880 |
for (unsigned q = 0; q < n_args; q++) |
367 |
|
{ |
368 |
1254 |
if ((int)q == arg) |
369 |
|
{ |
370 |
626 |
rt.d_children[r].d_children[q].d_req_type = dt[c].getArgType(r); |
371 |
|
} |
372 |
|
else |
373 |
|
{ |
374 |
628 |
rt.d_children[r].d_children[q].d_req_type = pdt[pc].getArgType(q); |
375 |
|
} |
376 |
|
} |
377 |
|
} |
378 |
|
// this increases term size but is probably a good idea |
379 |
|
} |
380 |
|
} |
381 |
1693 |
else if (k == NOT) |
382 |
|
{ |
383 |
141 |
if (pk == ITE) |
384 |
|
{ |
385 |
|
// (ite (not y) z w) -----> (ite y w z) |
386 |
33 |
rt.d_req_kind = ITE; |
387 |
33 |
rt.d_children[0].d_req_type = dt[c].getArgType(0); |
388 |
33 |
rt.d_children[1].d_req_type = pdt[pc].getArgType(2); |
389 |
33 |
rt.d_children[2].d_req_type = pdt[pc].getArgType(1); |
390 |
|
} |
391 |
|
} |
392 |
5144 |
Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk |
393 |
2572 |
<< ", arg = " << arg << "?" << std::endl; |
394 |
2572 |
if (!rt.empty()) |
395 |
|
{ |
396 |
708 |
rt.print("sygus-sb-debug"); |
397 |
|
// check if it meets the requirements |
398 |
708 |
if (rt.satisfiedBy(d_tds, tnp)) |
399 |
|
{ |
400 |
651 |
Trace("sygus-sb-debug") << "...success!" << std::endl; |
401 |
1302 |
Trace("sygus-sb-simple") |
402 |
651 |
<< " sb-simple : do not consider " << k << " as arg " << arg |
403 |
651 |
<< " of " << pk << std::endl; |
404 |
|
// do not need to consider the kind in the search since there are ways to |
405 |
|
// construct equivalent terms |
406 |
651 |
return false; |
407 |
|
} |
408 |
|
else |
409 |
|
{ |
410 |
57 |
Trace("sygus-sb-debug") << "...failed." << std::endl; |
411 |
|
} |
412 |
57 |
Trace("sygus-sb-debug") << std::endl; |
413 |
|
} |
414 |
|
// must consider this kind in the search |
415 |
1921 |
return true; |
416 |
|
} |
417 |
|
|
418 |
1207 |
bool SygusSimpleSymBreak::considerConst( |
419 |
|
TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg) |
420 |
|
{ |
421 |
1207 |
const DType& pdt = tnp.getDType(); |
422 |
|
// child grammar-independent |
423 |
1207 |
if (!considerConst(pdt, tnp, c, pk, arg)) |
424 |
|
{ |
425 |
357 |
return false; |
426 |
|
} |
427 |
|
// this can probably be made child grammar independent |
428 |
850 |
quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn); |
429 |
850 |
quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp); |
430 |
850 |
int pc = pti.getKindConsNum(pk); |
431 |
850 |
if (pdt[pc].getNumArgs() == 2) |
432 |
|
{ |
433 |
|
Kind ok; |
434 |
|
int offset; |
435 |
667 |
if (quantifiers::TermUtil::hasOffsetArg(pk, arg, offset, ok)) |
436 |
|
{ |
437 |
56 |
Trace("sygus-sb-simple-debug") |
438 |
28 |
<< pk << " has offset arg " << ok << " " << offset << std::endl; |
439 |
28 |
int ok_arg = pti.getKindConsNum(ok); |
440 |
28 |
if (ok_arg != -1) |
441 |
|
{ |
442 |
8 |
Trace("sygus-sb-simple-debug") |
443 |
4 |
<< "...at argument " << ok_arg << std::endl; |
444 |
|
// other operator be the same type |
445 |
4 |
if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg])) |
446 |
|
{ |
447 |
|
int status; |
448 |
|
Node co = quantifiers::TermUtil::mkTypeValueOffset( |
449 |
6 |
c.getType(), c, offset, status); |
450 |
8 |
Trace("sygus-sb-simple-debug") |
451 |
4 |
<< c << " with offset " << offset << " is " << co |
452 |
4 |
<< ", status=" << status << std::endl; |
453 |
4 |
if (status == 0 && !co.isNull()) |
454 |
|
{ |
455 |
4 |
if (ti.hasConst(co)) |
456 |
|
{ |
457 |
4 |
Trace("sygus-sb-simple") |
458 |
2 |
<< " sb-simple : by offset reasoning, do not consider const " |
459 |
2 |
<< c; |
460 |
4 |
Trace("sygus-sb-simple") |
461 |
2 |
<< " as arg " << arg << " of " << pk << " since we can use " |
462 |
2 |
<< co << " under " << ok << " " << std::endl; |
463 |
2 |
return false; |
464 |
|
} |
465 |
|
} |
466 |
|
} |
467 |
|
} |
468 |
|
} |
469 |
|
} |
470 |
848 |
return true; |
471 |
|
} |
472 |
|
|
473 |
1207 |
bool SygusSimpleSymBreak::considerConst( |
474 |
|
const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg) |
475 |
|
{ |
476 |
1207 |
quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp); |
477 |
1207 |
Assert(pti.hasKind(pk)); |
478 |
1207 |
int pc = pti.getKindConsNum(pk); |
479 |
1207 |
bool ret = true; |
480 |
2414 |
Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk |
481 |
1207 |
<< ", arg = " << arg << "?" << std::endl; |
482 |
1207 |
if (quantifiers::TermUtil::isIdempotentArg(c, pk, arg)) |
483 |
|
{ |
484 |
195 |
if (pdt[pc].getNumArgs() == 2) |
485 |
|
{ |
486 |
195 |
int oarg = arg == 0 ? 1 : 0; |
487 |
390 |
TypeNode otn = pdt[pc].getArgType(oarg); |
488 |
195 |
if (otn == tnp) |
489 |
|
{ |
490 |
348 |
Trace("sygus-sb-simple") |
491 |
174 |
<< " sb-simple : " << c << " is idempotent arg " << arg << " of " |
492 |
174 |
<< pk << "..." << std::endl; |
493 |
174 |
ret = false; |
494 |
|
} |
495 |
|
} |
496 |
|
} |
497 |
|
else |
498 |
|
{ |
499 |
2024 |
Node sc = quantifiers::TermUtil::isSingularArg(c, pk, arg); |
500 |
1012 |
if (!sc.isNull()) |
501 |
|
{ |
502 |
141 |
if (pti.hasConst(sc)) |
503 |
|
{ |
504 |
254 |
Trace("sygus-sb-simple") |
505 |
127 |
<< " sb-simple : " << c << " is singular arg " << arg << " of " |
506 |
127 |
<< pk << ", evaluating to " << sc << "..." << std::endl; |
507 |
127 |
ret = false; |
508 |
|
} |
509 |
|
} |
510 |
|
} |
511 |
1207 |
if (ret) |
512 |
|
{ |
513 |
1812 |
ReqTrie rt; |
514 |
906 |
Assert(rt.empty()); |
515 |
1812 |
Node max_c = quantifiers::TermUtil::mkTypeMaxValue(c.getType()); |
516 |
1812 |
Node zero_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 0); |
517 |
1812 |
Node one_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 1); |
518 |
906 |
if (pk == XOR || pk == BITVECTOR_XOR) |
519 |
|
{ |
520 |
8 |
if (c == max_c) |
521 |
|
{ |
522 |
|
rt.d_req_kind = pk == XOR ? NOT : BITVECTOR_NOT; |
523 |
|
} |
524 |
|
} |
525 |
902 |
else if (pk == ITE) |
526 |
|
{ |
527 |
170 |
if (arg == 0) |
528 |
|
{ |
529 |
56 |
if (c == max_c) |
530 |
|
{ |
531 |
28 |
rt.d_children[1].d_req_type = tnp; |
532 |
|
} |
533 |
28 |
else if (c == zero_c) |
534 |
|
{ |
535 |
28 |
rt.d_children[2].d_req_type = tnp; |
536 |
|
} |
537 |
|
} |
538 |
|
} |
539 |
732 |
else if (pk == STRING_SUBSTR) |
540 |
|
{ |
541 |
|
if (c == one_c && arg == 2) |
542 |
|
{ |
543 |
|
rt.d_req_kind = STRING_CHARAT; |
544 |
|
rt.d_children[0].d_req_type = pdt[pc].getArgType(0); |
545 |
|
rt.d_children[1].d_req_type = pdt[pc].getArgType(1); |
546 |
|
} |
547 |
|
} |
548 |
906 |
if (!rt.empty()) |
549 |
|
{ |
550 |
|
// check if satisfied |
551 |
56 |
if (rt.satisfiedBy(d_tds, tnp)) |
552 |
|
{ |
553 |
112 |
Trace("sygus-sb-simple") << " sb-simple : do not consider const " << c |
554 |
56 |
<< " as arg " << arg << " of " << pk; |
555 |
56 |
Trace("sygus-sb-simple") << " in " << pdt.getName() << std::endl; |
556 |
|
// do not need to consider the constant in the search since there are |
557 |
|
// ways to construct equivalent terms |
558 |
56 |
ret = false; |
559 |
|
} |
560 |
|
} |
561 |
|
} |
562 |
1207 |
return ret; |
563 |
|
} |
564 |
|
|
565 |
2597 |
int SygusSimpleSymBreak::solveForArgument(TypeNode tn, |
566 |
|
unsigned cindex, |
567 |
|
unsigned arg) |
568 |
|
{ |
569 |
|
// we currently do not solve for arguments |
570 |
2597 |
return -1; |
571 |
|
} |
572 |
|
|
573 |
238 |
int SygusSimpleSymBreak::getFirstArgOccurrence(const DTypeConstructor& c, |
574 |
|
TypeNode tn) |
575 |
|
{ |
576 |
238 |
for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++) |
577 |
|
{ |
578 |
238 |
if (c.getArgType(i) == tn) |
579 |
|
{ |
580 |
238 |
return i; |
581 |
|
} |
582 |
|
} |
583 |
|
return -1; |
584 |
|
} |
585 |
|
|
586 |
|
} // namespace datatypes |
587 |
|
} // namespace theory |
588 |
28191 |
} // namespace cvc5 |