Add floating-point support in evaluatoreval_fp

Currently, the operations implemented by the FloatingPoint class are
fairly slow, so it is not always beneficial to use the Evaluator as
opposed to the rewriter because the rewriter does more aggressive
caching. Thus, the evaluator is disabled by default for floating-point
logics. Note that this commit also adds a check for the --sygus-eval-opt
flag in SygusSampler::evaluate() (previously, it was always used in that
method).

1 files changed, 14 insertions, 7 deletions

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index b1b21a53e..0ed7cea12 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -451,16 +451,23 @@ void SygusSampler::addSamplePoint(std::vector<Node>& pt)
 Node SygusSampler::evaluate(Node n, unsigned index)
 {
   Assert(index < d_samples.size());
-  // use efficient rewrite for substitution + rewrite
-  Node ev = d_eval.eval(n, d_vars, d_samples[index]);
-  Trace("sygus-sample-ev") << "Evaluate ( " << n << ", " << index << " ) -> ";
-  if (!ev.isNull())
+
+  std::vector<Node>& pt = d_samples[index];
+
+  Node ev;
+  if (options::sygusEvalOpt())
   {
-    Trace("sygus-sample-ev") << ev << std::endl;
-    return ev;
+  // use efficient rewrite for substitution + rewrite
+    ev = d_eval.eval(n, d_vars, pt);
+    Trace("sygus-sample-ev") << "Evaluate ( " << n << ", " << index << " ) -> ";
+    if (!ev.isNull())
+    {
+      Trace("sygus-sample-ev") << ev << std::endl;
+      return ev;
+    }
   }
+
   // substitution + rewrite
-  std::vector<Node>& pt = d_samples[index];
   ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end());
   ev = Rewriter::rewrite(ev);
   Trace("sygus-sample-ev") << ev << std::endl;