1 /********************* */
2 /*! \file sygus_sampler.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Implementation of sygus_sampler
13 **/
14
15 #include "theory/quantifiers/sygus_sampler.h"
16
17 #include "expr/node_algorithm.h"
18 #include "options/base_options.h"
19 #include "options/quantifiers_options.h"
20 #include "printer/printer.h"
21 #include "theory/quantifiers/lazy_trie.h"
22 #include "util/bitvector.h"
23 #include "util/random.h"
24 #include "util/sampler.h"
25
26 namespace CVC4 {
27 namespace theory {
28 namespace quantifiers {
29
SygusSampler()30 SygusSampler::SygusSampler()
31 : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
32 {
33 }
34
initialize(TypeNode tn,const std::vector<Node> & vars,unsigned nsamples,bool unique_type_ids)35 void SygusSampler::initialize(TypeNode tn,
36 const std::vector<Node>& vars,
37 unsigned nsamples,
38 bool unique_type_ids)
39 {
40 d_tds = nullptr;
41 d_use_sygus_type = false;
42 d_is_valid = true;
43 d_ftn = TypeNode::null();
44 d_type_vars.clear();
45 d_vars.clear();
46 d_rvalue_cindices.clear();
47 d_rvalue_null_cindices.clear();
48 d_rstring_alphabet.clear();
49 d_var_sygus_types.clear();
50 d_const_sygus_types.clear();
51 d_vars.insert(d_vars.end(), vars.begin(), vars.end());
52 std::map<TypeNode, unsigned> type_to_type_id;
53 unsigned type_id_counter = 0;
54 for (const Node& sv : d_vars)
55 {
56 TypeNode svt = sv.getType();
57 unsigned tnid = 0;
58 if (unique_type_ids)
59 {
60 tnid = type_id_counter;
61 type_id_counter++;
62 }
63 else
64 {
65 std::map<TypeNode, unsigned>::iterator itt = type_to_type_id.find(svt);
66 if (itt == type_to_type_id.end())
67 {
68 type_to_type_id[svt] = type_id_counter;
69 type_id_counter++;
70 }
71 else
72 {
73 tnid = itt->second;
74 }
75 }
76 Trace("sygus-sample-debug")
77 << "Type id for " << sv << " is " << tnid << std::endl;
78 d_var_index[sv] = d_type_vars[tnid].size();
79 d_type_vars[tnid].push_back(sv);
80 d_type_ids[sv] = tnid;
81 }
82 initializeSamples(nsamples);
83 }
84
initializeSygus(TermDbSygus * tds,Node f,unsigned nsamples,bool useSygusType)85 void SygusSampler::initializeSygus(TermDbSygus* tds,
86 Node f,
87 unsigned nsamples,
88 bool useSygusType)
89 {
90 d_tds = tds;
91 d_use_sygus_type = useSygusType;
92 d_is_valid = true;
93 d_ftn = f.getType();
94 Assert(d_ftn.isDatatype());
95 const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype();
96 Assert(dt.isSygus());
97
98 Trace("sygus-sample") << "Register sampler for " << f << std::endl;
99
100 d_vars.clear();
101 d_type_vars.clear();
102 d_var_index.clear();
103 d_type_vars.clear();
104 d_rvalue_cindices.clear();
105 d_rvalue_null_cindices.clear();
106 d_var_sygus_types.clear();
107 // get the sygus variable list
108 Node var_list = Node::fromExpr(dt.getSygusVarList());
109 if (!var_list.isNull())
110 {
111 for (const Node& sv : var_list)
112 {
113 d_vars.push_back(sv);
114 }
115 }
116 // register sygus type
117 registerSygusType(d_ftn);
118 // Variables are associated with type ids based on the set of sygus types they
119 // appear in.
120 std::map<Node, unsigned> var_to_type_id;
121 unsigned type_id_counter = 0;
122 for (const Node& sv : d_vars)
123 {
124 TypeNode svt = sv.getType();
125 // is it equivalent to a previous variable?
126 for (const std::pair<Node, unsigned>& v : var_to_type_id)
127 {
128 Node svc = v.first;
129 if (svc.getType() == svt)
130 {
131 if (d_var_sygus_types[sv].size() == d_var_sygus_types[svc].size())
132 {
133 bool success = true;
134 for (unsigned t = 0, size = d_var_sygus_types[sv].size(); t < size;
135 t++)
136 {
137 if (d_var_sygus_types[sv][t] != d_var_sygus_types[svc][t])
138 {
139 success = false;
140 break;
141 }
142 }
143 if (success)
144 {
145 var_to_type_id[sv] = var_to_type_id[svc];
146 }
147 }
148 }
149 }
150 if (var_to_type_id.find(sv) == var_to_type_id.end())
151 {
152 var_to_type_id[sv] = type_id_counter;
153 type_id_counter++;
154 }
155 unsigned tnid = var_to_type_id[sv];
156 Trace("sygus-sample-debug")
157 << "Type id for " << sv << " is " << tnid << std::endl;
158 d_var_index[sv] = d_type_vars[tnid].size();
159 d_type_vars[tnid].push_back(sv);
160 d_type_ids[sv] = tnid;
161 }
162
163 initializeSamples(nsamples);
164 }
165
initializeSamples(unsigned nsamples)166 void SygusSampler::initializeSamples(unsigned nsamples)
167 {
168 d_samples.clear();
169 std::vector<TypeNode> types;
170 for (const Node& v : d_vars)
171 {
172 TypeNode vt = v.getType();
173 types.push_back(vt);
174 Trace("sygus-sample") << " var #" << types.size() << " : " << v << " : "
175 << vt << std::endl;
176 }
177 std::map<unsigned, std::map<Node, std::vector<TypeNode> >::iterator> sts;
178 if (options::sygusSampleGrammar())
179 {
180 for (unsigned j = 0, size = types.size(); j < size; j++)
181 {
182 sts[j] = d_var_sygus_types.find(d_vars[j]);
183 }
184 }
185
186 unsigned nduplicates = 0;
187 for (unsigned i = 0; i < nsamples; i++)
188 {
189 std::vector<Node> sample_pt;
190 for (unsigned j = 0, size = types.size(); j < size; j++)
191 {
192 Node v = d_vars[j];
193 Node r;
194 if (options::sygusSampleGrammar())
195 {
196 // choose a random start sygus type, if possible
197 if (sts[j] != d_var_sygus_types.end())
198 {
199 unsigned ntypes = sts[j]->second.size();
200 if(ntypes > 0)
201 {
202 unsigned index = Random::getRandom().pick(0, ntypes - 1);
203 if (index < ntypes)
204 {
205 // currently hard coded to 0.0, 0.5
206 r = getSygusRandomValue(sts[j]->second[index], 0.0, 0.5);
207 }
208 }
209 }
210 }
211 if (r.isNull())
212 {
213 r = getRandomValue(types[j]);
214 if (r.isNull())
215 {
216 d_is_valid = false;
217 }
218 }
219 sample_pt.push_back(r);
220 }
221 if (d_samples_trie.add(sample_pt))
222 {
223 if (Trace.isOn("sygus-sample"))
224 {
225 Trace("sygus-sample") << "Sample point #" << i << " : ";
226 for (const Node& r : sample_pt)
227 {
228 Trace("sygus-sample") << r << " ";
229 }
230 Trace("sygus-sample") << std::endl;
231 }
232 d_samples.push_back(sample_pt);
233 }
234 else
235 {
236 i--;
237 nduplicates++;
238 if (nduplicates == nsamples * 10)
239 {
240 Trace("sygus-sample")
241 << "...WARNING: excessive duplicates, cut off sampling at " << i
242 << "/" << nsamples << " points." << std::endl;
243 break;
244 }
245 }
246 }
247
248 d_trie.clear();
249 }
250
add(std::vector<Node> & pt)251 bool SygusSampler::PtTrie::add(std::vector<Node>& pt)
252 {
253 PtTrie* curr = this;
254 for (unsigned i = 0, size = pt.size(); i < size; i++)
255 {
256 curr = &(curr->d_children[pt[i]]);
257 }
258 bool retVal = curr->d_children.empty();
259 curr = &(curr->d_children[Node::null()]);
260 return retVal;
261 }
262
registerTerm(Node n,bool forceKeep)263 Node SygusSampler::registerTerm(Node n, bool forceKeep)
264 {
265 if (!d_is_valid)
266 {
267 // do nothing
268 return n;
269 }
270 Node bn = n;
271 TypeNode tn = n.getType();
272 // If we are using sygus types, get the builtin analog of n.
273 if (d_use_sygus_type)
274 {
275 bn = d_tds->sygusToBuiltin(n);
276 d_builtin_to_sygus[tn][bn] = n;
277 }
278 // cache based on the (original) type of n
279 Node res = d_trie[tn].add(bn, this, 0, d_samples.size(), forceKeep);
280 // If we are using sygus types, map back to an original.
281 // Notice that d_builtin_to_sygus is not necessarily bijective.
282 if (d_use_sygus_type)
283 {
284 std::map<Node, Node>& bts = d_builtin_to_sygus[tn];
285 Assert(bts.find(res) != bts.end());
286 res = res != bn ? bts[res] : n;
287 }
288 return res;
289 }
290
isContiguous(Node n)291 bool SygusSampler::isContiguous(Node n)
292 {
293 // compute free variables in n
294 std::vector<Node> fvs;
295 computeFreeVariables(n, fvs);
296 // compute contiguous condition
297 for (const std::pair<const unsigned, std::vector<Node> >& p : d_type_vars)
298 {
299 bool foundNotFv = false;
300 for (const Node& v : p.second)
301 {
302 bool hasFv = std::find(fvs.begin(), fvs.end(), v) != fvs.end();
303 if (!hasFv)
304 {
305 foundNotFv = true;
306 }
307 else if (foundNotFv)
308 {
309 return false;
310 }
311 }
312 }
313 return true;
314 }
315
computeFreeVariables(Node n,std::vector<Node> & fvs)316 void SygusSampler::computeFreeVariables(Node n, std::vector<Node>& fvs)
317 {
318 std::unordered_set<TNode, TNodeHashFunction> visited;
319 std::unordered_set<TNode, TNodeHashFunction>::iterator it;
320 std::vector<TNode> visit;
321 TNode cur;
322 visit.push_back(n);
323 do
324 {
325 cur = visit.back();
326 visit.pop_back();
327 if (visited.find(cur) == visited.end())
328 {
329 visited.insert(cur);
330 if (cur.isVar())
331 {
332 if (d_var_index.find(cur) != d_var_index.end())
333 {
334 fvs.push_back(cur);
335 }
336 }
337 for (const Node& cn : cur)
338 {
339 visit.push_back(cn);
340 }
341 }
342 } while (!visit.empty());
343 }
344
isOrdered(Node n)345 bool SygusSampler::isOrdered(Node n) { return checkVariables(n, true, false); }
346
isLinear(Node n)347 bool SygusSampler::isLinear(Node n) { return checkVariables(n, false, true); }
348
checkVariables(Node n,bool checkOrder,bool checkLinear)349 bool SygusSampler::checkVariables(Node n, bool checkOrder, bool checkLinear)
350 {
351 // compute free variables in n for each type
352 std::map<unsigned, std::vector<Node> > fvs;
353
354 std::unordered_set<TNode, TNodeHashFunction> visited;
355 std::unordered_set<TNode, TNodeHashFunction>::iterator it;
356 std::vector<TNode> visit;
357 TNode cur;
358 visit.push_back(n);
359 do
360 {
361 cur = visit.back();
362 visit.pop_back();
363 if (visited.find(cur) == visited.end())
364 {
365 visited.insert(cur);
366 if (cur.isVar())
367 {
368 std::map<Node, unsigned>::iterator itv = d_var_index.find(cur);
369 if (itv != d_var_index.end())
370 {
371 if (checkOrder)
372 {
373 unsigned tnid = d_type_ids[cur];
374 // if this variable is out of order
375 if (itv->second != fvs[tnid].size())
376 {
377 return false;
378 }
379 fvs[tnid].push_back(cur);
380 }
381 if (checkLinear)
382 {
383 if (expr::hasSubtermMulti(n, cur))
384 {
385 return false;
386 }
387 }
388 }
389 }
390 for (unsigned j = 0, nchildren = cur.getNumChildren(); j < nchildren; j++)
391 {
392 visit.push_back(cur[(nchildren - j) - 1]);
393 }
394 }
395 } while (!visit.empty());
396 return true;
397 }
398
containsFreeVariables(Node a,Node b,bool strict)399 bool SygusSampler::containsFreeVariables(Node a, Node b, bool strict)
400 {
401 // compute free variables in a
402 std::vector<Node> fvs;
403 computeFreeVariables(a, fvs);
404 std::vector<Node> fv_found;
405
406 std::unordered_set<TNode, TNodeHashFunction> visited;
407 std::unordered_set<TNode, TNodeHashFunction>::iterator it;
408 std::vector<TNode> visit;
409 TNode cur;
410 visit.push_back(b);
411 do
412 {
413 cur = visit.back();
414 visit.pop_back();
415 if (visited.find(cur) == visited.end())
416 {
417 visited.insert(cur);
418 if (cur.isVar())
419 {
420 if (std::find(fvs.begin(), fvs.end(), cur) == fvs.end())
421 {
422 return false;
423 }
424 else if (strict)
425 {
426 if (fv_found.size() + 1 == fvs.size())
427 {
428 return false;
429 }
430 // cur should only be visited once
431 Assert(std::find(fv_found.begin(), fv_found.end(), cur)
432 == fv_found.end());
433 fv_found.push_back(cur);
434 }
435 }
436 for (const Node& cn : cur)
437 {
438 visit.push_back(cn);
439 }
440 }
441 } while (!visit.empty());
442 return true;
443 }
444
getVariables(std::vector<Node> & vars) const445 void SygusSampler::getVariables(std::vector<Node>& vars) const
446 {
447 vars.insert(vars.end(), d_vars.begin(), d_vars.end());
448 }
449
getSamplePoint(unsigned index,std::vector<Node> & pt)450 void SygusSampler::getSamplePoint(unsigned index,
451 std::vector<Node>& pt)
452 {
453 Assert(index < d_samples.size());
454 std::vector<Node>& spt = d_samples[index];
455 pt.insert(pt.end(), spt.begin(), spt.end());
456 }
457
addSamplePoint(std::vector<Node> & pt)458 void SygusSampler::addSamplePoint(std::vector<Node>& pt)
459 {
460 Assert(pt.size() == d_vars.size());
461 d_samples.push_back(pt);
462 }
463
evaluate(Node n,unsigned index)464 Node SygusSampler::evaluate(Node n, unsigned index)
465 {
466 Assert(index < d_samples.size());
467 // do beta-reductions in n first
468 n = Rewriter::rewrite(n);
469 // use efficient rewrite for substitution + rewrite
470 Node ev = d_eval.eval(n, d_vars, d_samples[index]);
471 Trace("sygus-sample-ev") << "Evaluate ( " << n << ", " << index << " ) -> ";
472 if (!ev.isNull())
473 {
474 Trace("sygus-sample-ev") << ev << std::endl;
475 return ev;
476 }
477 Trace("sygus-sample-ev") << "null" << std::endl;
478 Trace("sygus-sample-ev") << "Rewrite -> ";
479 // substitution + rewrite
480 std::vector<Node>& pt = d_samples[index];
481 ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end());
482 ev = Rewriter::rewrite(ev);
483 Trace("sygus-sample-ev") << ev << std::endl;
484 return ev;
485 }
486
getDiffSamplePointIndex(Node a,Node b)487 int SygusSampler::getDiffSamplePointIndex(Node a, Node b)
488 {
489 for (unsigned i = 0, nsamp = d_samples.size(); i < nsamp; i++)
490 {
491 Node ae = evaluate(a, i);
492 Node be = evaluate(b, i);
493 if (ae != be)
494 {
495 return i;
496 }
497 }
498 return -1;
499 }
500
getRandomValue(TypeNode tn)501 Node SygusSampler::getRandomValue(TypeNode tn)
502 {
503 NodeManager* nm = NodeManager::currentNM();
504 if (tn.isBoolean())
505 {
506 return nm->mkConst(Random::getRandom().pickWithProb(0.5));
507 }
508 else if (tn.isBitVector())
509 {
510 unsigned sz = tn.getBitVectorSize();
511 return nm->mkConst(Sampler::pickBvUniform(sz));
512 }
513 else if (tn.isFloatingPoint())
514 {
515 unsigned e = tn.getFloatingPointExponentSize();
516 unsigned s = tn.getFloatingPointSignificandSize();
517 return nm->mkConst(options::sygusSampleFpUniform()
518 ? Sampler::pickFpUniform(e, s)
519 : Sampler::pickFpBiased(e, s));
520 }
521 else if (tn.isString() || tn.isInteger())
522 {
523 // if string, determine the alphabet
524 if (tn.isString() && d_rstring_alphabet.empty())
525 {
526 Trace("sygus-sample-str-alpha")
527 << "Setting string alphabet..." << std::endl;
528 std::unordered_set<unsigned> alphas;
529 for (const std::pair<const Node, std::vector<TypeNode> >& c :
530 d_const_sygus_types)
531 {
532 if (c.first.getType().isString())
533 {
534 Trace("sygus-sample-str-alpha")
535 << "...have constant " << c.first << std::endl;
536 Assert(c.first.isConst());
537 std::vector<unsigned> svec = c.first.getConst<String>().getVec();
538 for (unsigned ch : svec)
539 {
540 alphas.insert(ch);
541 }
542 }
543 }
544 // can limit to 1 extra characters beyond those in the grammar (2 if
545 // there are none in the grammar)
546 unsigned num_fresh_char = alphas.empty() ? 2 : 1;
547 unsigned fresh_char = 0;
548 for (unsigned i = 0; i < num_fresh_char; i++)
549 {
550 while (alphas.find(fresh_char) != alphas.end())
551 {
552 fresh_char++;
553 }
554 alphas.insert(fresh_char);
555 }
556 Trace("sygus-sample-str-alpha")
557 << "Sygus sampler: limit strings alphabet to : " << std::endl
558 << " ";
559 for (unsigned ch : alphas)
560 {
561 d_rstring_alphabet.push_back(ch);
562 Trace("sygus-sample-str-alpha")
563 << " \"" << String::convertUnsignedIntToChar(ch) << "\"";
564 }
565 Trace("sygus-sample-str-alpha") << std::endl;
566 }
567
568 std::vector<unsigned> vec;
569 double ext_freq = .5;
570 unsigned base = tn.isString() ? d_rstring_alphabet.size() : 10;
571 while (Random::getRandom().pickWithProb(ext_freq))
572 {
573 // add a digit
574 unsigned digit = Random::getRandom().pick(0, base - 1);
575 if (tn.isString())
576 {
577 digit = d_rstring_alphabet[digit];
578 }
579 vec.push_back(digit);
580 }
581 if (tn.isString())
582 {
583 return nm->mkConst(String(vec));
584 }
585 else if (tn.isInteger())
586 {
587 Rational baser(base);
588 Rational curr(1);
589 std::vector<Node> sum;
590 for (unsigned j = 0, size = vec.size(); j < size; j++)
591 {
592 Node digit = nm->mkConst(Rational(vec[j]) * curr);
593 sum.push_back(digit);
594 curr = curr * baser;
595 }
596 Node ret;
597 if (sum.empty())
598 {
599 ret = nm->mkConst(Rational(0));
600 }
601 else if (sum.size() == 1)
602 {
603 ret = sum[0];
604 }
605 else
606 {
607 ret = nm->mkNode(kind::PLUS, sum);
608 }
609
610 if (Random::getRandom().pickWithProb(0.5))
611 {
612 // negative
613 ret = nm->mkNode(kind::UMINUS, ret);
614 }
615 ret = Rewriter::rewrite(ret);
616 Assert(ret.isConst());
617 return ret;
618 }
619 }
620 else if (tn.isReal())
621 {
622 Node s = getRandomValue(nm->integerType());
623 Node r = getRandomValue(nm->integerType());
624 if (!s.isNull() && !r.isNull())
625 {
626 Rational sr = s.getConst<Rational>();
627 Rational rr = r.getConst<Rational>();
628 if (rr.sgn() == 0)
629 {
630 return s;
631 }
632 else
633 {
634 return nm->mkConst(sr / rr);
635 }
636 }
637 }
638 // default: use type enumerator
639 unsigned counter = 0;
640 while (Random::getRandom().pickWithProb(0.5))
641 {
642 counter++;
643 }
644 Node ret = d_tenum.getEnumerateTerm(tn, counter);
645 if (ret.isNull())
646 {
647 // beyond bounds, return the first
648 ret = d_tenum.getEnumerateTerm(tn, 0);
649 }
650 return ret;
651 }
652
getSygusRandomValue(TypeNode tn,double rchance,double rinc,unsigned depth)653 Node SygusSampler::getSygusRandomValue(TypeNode tn,
654 double rchance,
655 double rinc,
656 unsigned depth)
657 {
658 if (!tn.isDatatype())
659 {
660 return getRandomValue(tn);
661 }
662 const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
663 if (!dt.isSygus())
664 {
665 return getRandomValue(tn);
666 }
667 Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end());
668 Trace("sygus-sample-grammar")
669 << "Sygus random value " << tn << ", depth = " << depth
670 << ", rchance = " << rchance << std::endl;
671 // check if we terminate on this call
672 // we refuse to enumerate terms of 10+ depth as a hard limit
673 bool terminate = Random::getRandom().pickWithProb(rchance) || depth >= 10;
674 // if we terminate, only nullary constructors can be chosen
675 std::vector<unsigned>& cindices =
676 terminate ? d_rvalue_null_cindices[tn] : d_rvalue_cindices[tn];
677 unsigned ncons = cindices.size();
678 // select a random constructor, or random value when index=ncons.
679 unsigned index = Random::getRandom().pick(0, ncons);
680 Trace("sygus-sample-grammar")
681 << "Random index 0..." << ncons << " was : " << index << std::endl;
682 if (index < ncons)
683 {
684 Trace("sygus-sample-grammar")
685 << "Recurse constructor index #" << index << std::endl;
686 unsigned cindex = cindices[index];
687 Assert(cindex < dt.getNumConstructors());
688 const DatatypeConstructor& dtc = dt[cindex];
689 // more likely to terminate in recursive calls
690 double rchance_new = rchance + (1.0 - rchance) * rinc;
691 std::map<int, Node> pre;
692 bool success = true;
693 // generate random values for all arguments
694 for (unsigned i = 0, nargs = dtc.getNumArgs(); i < nargs; i++)
695 {
696 TypeNode tnc = d_tds->getArgType(dtc, i);
697 Node c = getSygusRandomValue(tnc, rchance_new, rinc, depth + 1);
698 if (c.isNull())
699 {
700 success = false;
701 Trace("sygus-sample-grammar") << "...fail." << std::endl;
702 break;
703 }
704 Trace("sygus-sample-grammar")
705 << " child #" << i << " : " << c << std::endl;
706 pre[i] = c;
707 }
708 if (success)
709 {
710 Trace("sygus-sample-grammar") << "mkGeneric" << std::endl;
711 Node ret = d_tds->mkGeneric(dt, cindex, pre);
712 Trace("sygus-sample-grammar") << "...returned " << ret << std::endl;
713 ret = Rewriter::rewrite(ret);
714 Trace("sygus-sample-grammar") << "...after rewrite " << ret << std::endl;
715 Assert(ret.isConst());
716 return ret;
717 }
718 }
719 Trace("sygus-sample-grammar") << "...resort to random value" << std::endl;
720 // if we did not generate based on the grammar, pick a random value
721 return getRandomValue(TypeNode::fromType(dt.getSygusType()));
722 }
723
724 // recursion depth bounded by number of types in grammar (small)
registerSygusType(TypeNode tn)725 void SygusSampler::registerSygusType(TypeNode tn)
726 {
727 if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end())
728 {
729 d_rvalue_cindices[tn].clear();
730 if (!tn.isDatatype())
731 {
732 return;
733 }
734 const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
735 if (!dt.isSygus())
736 {
737 return;
738 }
739 for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
740 {
741 const DatatypeConstructor& dtc = dt[i];
742 Node sop = Node::fromExpr(dtc.getSygusOp());
743 bool isVar = std::find(d_vars.begin(), d_vars.end(), sop) != d_vars.end();
744 if (isVar)
745 {
746 // if it is a variable, add it to the list of sygus types for that var
747 d_var_sygus_types[sop].push_back(tn);
748 }
749 else
750 {
751 // otherwise, it is a constructor for sygus random value
752 d_rvalue_cindices[tn].push_back(i);
753 if (dtc.getNumArgs() == 0)
754 {
755 d_rvalue_null_cindices[tn].push_back(i);
756 if (sop.isConst())
757 {
758 d_const_sygus_types[sop].push_back(tn);
759 }
760 }
761 }
762 // recurse on all subfields
763 for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
764 {
765 TypeNode tnc = d_tds->getArgType(dtc, j);
766 registerSygusType(tnc);
767 }
768 }
769 }
770 }
771
checkEquivalent(Node bv,Node bvr)772 void SygusSampler::checkEquivalent(Node bv, Node bvr)
773 {
774 Trace("sygus-rr-verify") << "Testing rewrite rule " << bv << " ---> " << bvr
775 << std::endl;
776
777 // see if they evaluate to same thing on all sample points
778 bool ptDisequal = false;
779 unsigned pt_index = 0;
780 Node bve, bvre;
781 for (unsigned i = 0, npoints = getNumSamplePoints(); i < npoints; i++)
782 {
783 bve = evaluate(bv, i);
784 bvre = evaluate(bvr, i);
785 if (bve != bvre)
786 {
787 ptDisequal = true;
788 pt_index = i;
789 break;
790 }
791 }
792 // bv and bvr should be equivalent under examples
793 if (ptDisequal)
794 {
795 // we have detected unsoundness in the rewriter
796 Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
797 std::ostream* out = nodeManagerOptions.getOut();
798 (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
799 // debugging information
800 (*out) << "; unsound: are not equivalent for : " << std::endl;
801 std::vector<Node> vars;
802 getVariables(vars);
803 std::vector<Node> pt;
804 getSamplePoint(pt_index, pt);
805 Assert(vars.size() == pt.size());
806 for (unsigned i = 0, size = pt.size(); i < size; i++)
807 {
808 (*out) << "; unsound: " << vars[i] << " -> " << pt[i] << std::endl;
809 }
810 Assert(bve != bvre);
811 (*out) << "; unsound: where they evaluate to " << bve << " and " << bvre
812 << std::endl;
813
814 if (options::sygusRewVerifyAbort())
815 {
816 AlwaysAssert(false,
817 "--sygus-rr-verify detected unsoundness in the rewriter!");
818 }
819 }
820 }
821
822 } /* CVC4::theory::quantifiers namespace */
823 } /* CVC4::theory namespace */
824 } /* CVC4 namespace */
825