From a131d4b4cf086f27c4c62d4b012862c75153033e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 26 Jul 2018 14:27:37 -0500 Subject: [PATCH] Fix a few issues in the sygus sampler related to evaluation (#2215) --- src/theory/evaluator.cpp | 5 +++++ src/theory/quantifiers/sygus_sampler.cpp | 4 ++++ 2 files changed, 9 insertions(+) diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index ca2140ed5..dd40ace8a 100644 --- 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 b1b21a53e..6808f2a6e 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -451,6 +451,8 @@ void SygusSampler::addSamplePoint(std::vector& 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& pt = d_samples[index]; ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end()); -- 2.30.2