diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-05 18:59:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-05 18:59:13 -0600 |
| commit | 4ada10b0e9b0ccd96e8bf620690e6888e617c2fb (patch) | |
| tree | 8beb5839622eb5b1a44100d3e6bb97174652c847 /src/theory/quantifiers/sygus_sampler.cpp | |
| parent | 66a7932c7d4bd986665a041293ed23f8f58570f4 (diff) | |
Statically eliminate redundant sygus constructors (#1560)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 82720dd5e..f824cd6f7 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -468,9 +468,9 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn, const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); Assert(dt.isSygus()); Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end()); - Trace("sygus-sample-grammar") << "Sygus random value " << tn - << ", depth = " << depth - << ", rchance = " << rchance << std::endl; + Trace("sygus-sample-grammar") + << "Sygus random value " << tn << ", depth = " << depth + << ", rchance = " << rchance << std::endl; // check if we terminate on this call // we refuse to enumerate terms of 10+ depth as a hard limit bool terminate = Random::getRandom().pickWithProb(rchance) || depth >= 10; @@ -480,12 +480,12 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn, unsigned ncons = cindices.size(); // select a random constructor, or random value when index=ncons. unsigned index = Random::getRandom().pick(0, ncons); - Trace("sygus-sample-grammar") << "Random index 0..." << ncons - << " was : " << index << std::endl; + Trace("sygus-sample-grammar") + << "Random index 0..." << ncons << " was : " << index << std::endl; if (index < ncons) { - Trace("sygus-sample-grammar") << "Recurse constructor index #" << index - << std::endl; + Trace("sygus-sample-grammar") + << "Recurse constructor index #" << index << std::endl; unsigned cindex = cindices[index]; Assert(cindex < dt.getNumConstructors()); const DatatypeConstructor& dtc = dt[cindex]; @@ -504,8 +504,8 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn, Trace("sygus-sample-grammar") << "...fail." << std::endl; break; } - Trace("sygus-sample-grammar") << " child #" << i << " : " << c - << std::endl; + Trace("sygus-sample-grammar") + << " child #" << i << " : " << c << std::endl; pre[i] = c; } if (success) |