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