GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus_sampler.cpp Lines: 368 463 79.5 %
Date: 2021-03-23 Branches: 587 1542 38.1 %

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