diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-05 04:23:19 +0100 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-04 20:23:19 -0700 |
commit | dc8cbd0728630db5a3bc566a9cd627bcb122dda2 (patch) | |
tree | 5ea1a400ae8bb14b5a374bd1a379fddfb1456806 /src | |
parent | 801d53f9e048e6e4906ec098e076e256820eccc8 (diff) |
Minor changes to sygus-rr utilities to support floating point rewrites (#2148)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index ebd10c585..5ae0e83b2 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -197,12 +197,14 @@ void SygusSampler::initializeSamples(unsigned nsamples) if (sts[j] != d_var_sygus_types.end()) { unsigned ntypes = sts[j]->second.size(); - Assert(ntypes > 0); - unsigned index = Random::getRandom().pick(0, ntypes - 1); - if (index < ntypes) + if(ntypes > 0) { - // currently hard coded to 0.0, 0.5 - r = getSygusRandomValue(sts[j]->second[index], 0.0, 0.5); + unsigned index = Random::getRandom().pick(0, ntypes - 1); + if (index < ntypes) + { + // currently hard coded to 0.0, 0.5 + r = getSygusRandomValue(sts[j]->second[index], 0.0, 0.5); + } } } } @@ -495,6 +497,15 @@ Node SygusSampler::getRandomValue(TypeNode tn) } return nm->mkConst(BitVector(ss.str(), 2)); } + else if (tn.isFloatingPoint() ) + { + // extremely naive uniform generation of floating points + unsigned e = tn.getFloatingPointExponentSize(); + unsigned s = tn.getFloatingPointSignificandSize(); + TypeNode bvt = nm->mkBitVectorType(e+s); + Node bvc = getRandomValue(bvt); + return nm->mkConst(FloatingPoint(e,s,bvc.getConst<BitVector>())); + } else if (tn.isString() || tn.isInteger()) { // if string, determine the alphabet |