src/theory/quantifiers/sygus_sampler.cpp

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