Fix a few issues in the sygus sampler related to evaluation (#2215)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index ca2140ed59dae9c31de34a1715daee4f0a9e535b..dd40ace8a07e3b3bfadcddf56e8987905a40efc0 100644 (file)
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -193,6 +193,11 @@ EvalResult Evaluator::evalInternal(TNode n,
         // Lambdas are evaluated in a recursive fashion because each evaluation
         // requires different substitutions
         results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals);
+        if (results[currNode].d_tag == EvalResult::INVALID)
+        {
+          // evaluation was invalid, we fail
+          return results[currNode];
+        }
         continue;
       }
 

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index b1b21a53e809a5ca4f02d541a8cd1aea812dd137..6808f2a6e13cf4e20821871ab7e436b58cf32fc7 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -451,6 +451,8 @@ void SygusSampler::addSamplePoint(std::vector<Node>& pt)
 Node SygusSampler::evaluate(Node n, unsigned index)
 {
   Assert(index < d_samples.size());
+  // do beta-reductions in n first
+  n = Rewriter::rewrite(n);
   // use efficient rewrite for substitution + rewrite
   Node ev = d_eval.eval(n, d_vars, d_samples[index]);
   Trace("sygus-sample-ev") << "Evaluate ( " << n << ", " << index << " ) -> ";
@@ -459,6 +461,8 @@ Node SygusSampler::evaluate(Node n, unsigned index)
     Trace("sygus-sample-ev") << ev << std::endl;
     return ev;
   }
+  Trace("sygus-sample-ev") << "null" << std::endl;
+  Trace("sygus-sample-ev") << "Rewrite -> ";
   // substitution + rewrite
   std::vector<Node>& pt = d_samples[index];
   ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end());