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 8da65e4cad74f6bb07681aeed3db3438a9ea3788..e07f735407439f58d489de11670c4b086f9e860e 100644 (file)
--- 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 d323b36bd26f43b802e399a93058955eb14d4e62..290a8b17dc056f01f4e2849570c80e1f9cc476d7 100644 (file)
--- 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
   {