diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-29 13:39:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-29 13:39:59 -0500 |
| commit | 5d5bd50528ee63683078fd16fe5df7c1b9c6f2fa (patch) | |
| tree | 661dfa25ae81129171e2d556fbf334666878eb45 | |
| parent | 021e7ebaf808f4496609685cccab4eae8eb04d38 (diff) | |
Use evaluator in sygus sampler. (#2117)
* Use evaluator for sygus sampler.
* Format
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 16 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 3 |
2 files changed, 14 insertions, 5 deletions
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 { |