From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 5 Jul 2018 03:23:19 +0000 (+0100)
Subject: Minor changes to sygus-rr utilities to support floating point rewrites (#2148)
X-Git-Tag: cvc5-1.0.0~4912
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc8cbd0728630db5a3bc566a9cd627bcb122dda2;p=cvc5.git

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 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