From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 29 Jun 2018 18:39:59 +0000 (-0500)
Subject: Use evaluator in sygus sampler. (#2117)
X-Git-Tag: cvc5-1.0.0~4932
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5d5bd50528ee63683078fd16fe5df7c1b9c6f2fa;p=cvc5.git

Use evaluator in sygus sampler. (#2117)

* Use evaluator for sygus sampler.

* Format
---

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 8da65e4ca..e07f73540 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -448,13 +448,19 @@ void SygusSampler::addSamplePoint(std::vector<Node>& pt)
 Node SygusSampler::evaluate(Node n, unsigned index)
 {
   Assert(index < d_samples.size());
-  // just a substitution
+  // 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())
+  {
+    Trace("sygus-sample-ev") << ev << std::endl;
+    return ev;
+  }
+  // substitution + rewrite
   std::vector<Node>& pt = d_samples[index];
-  Node ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end());
-  Trace("sygus-sample-ev-debug") << "Rewrite : " << ev << std::endl;
+  ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end());
   ev = Rewriter::rewrite(ev);
-  Trace("sygus-sample-ev") << "( " << n << ", " << index << " ) -> " << ev
-                           << std::endl;
+  Trace("sygus-sample-ev") << ev << std::endl;
   return ev;
 }
 
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index d323b36bd..290a8b17d 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -18,6 +18,7 @@
 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
 
 #include <map>
+#include "theory/evaluator.h"
 #include "theory/quantifiers/dynamic_rewrite.h"
 #include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -156,6 +157,8 @@ class SygusSampler : public LazyTrieEvaluator
   TermEnumeration d_tenum;
   /** samples */
   std::vector<std::vector<Node> > d_samples;
+  /** evaluator class */
+  Evaluator d_eval;
   /** data structure to check duplication of sample points */
   class PtTrie
   {