Minor changes to sygus-rr utilities to support floating point rewrites (#2148)

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index ebd10c5852c07af51483533532b9133e097e7935..5ae0e83b2090c10e2c1cd5afed0d51d31561b5bb 100644 (file)
--- 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