diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-27 14:12:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-27 14:12:17 -0500 |
commit | d6c7967cfc7a9f8530f0de50f12f99bfc5f93da7 (patch) | |
tree | 2741c23c2cc42c065dc2aa573e0983e8f10823c1 /src/theory/quantifiers/sygus_sampler.cpp | |
parent | a236ade3242599d4916fd9ee676c2c68c7c004b1 (diff) |
Synthesize candidate-rewrites from standard inputs (#1918)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 65 |
1 files changed, 42 insertions, 23 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index c290c027a..8da65e4ca 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -32,7 +32,8 @@ SygusSampler::SygusSampler() void SygusSampler::initialize(TypeNode tn, std::vector<Node>& vars, - unsigned nsamples) + unsigned nsamples, + bool unique_type_ids) { d_tds = nullptr; d_use_sygus_type = false; @@ -53,15 +54,23 @@ void SygusSampler::initialize(TypeNode tn, { TypeNode svt = sv.getType(); unsigned tnid = 0; - std::map<TypeNode, unsigned>::iterator itt = type_to_type_id.find(svt); - if (itt == type_to_type_id.end()) + if (unique_type_ids) { - type_to_type_id[svt] = type_id_counter; + tnid = type_id_counter; type_id_counter++; } else { - tnid = itt->second; + std::map<TypeNode, unsigned>::iterator itt = type_to_type_id.find(svt); + if (itt == type_to_type_id.end()) + { + type_to_type_id[svt] = type_id_counter; + type_id_counter++; + } + else + { + tnid = itt->second; + } } Trace("sygus-sample-debug") << "Type id for " << sv << " is " << tnid << std::endl; @@ -586,7 +595,7 @@ Node SygusSampler::getRandomValue(TypeNode tn) if (!s.isNull() && !r.isNull()) { Rational sr = s.getConst<Rational>(); - Rational rr = s.getConst<Rational>(); + Rational rr = r.getConst<Rational>(); if (rr.sgn() == 0) { return s; @@ -597,7 +606,19 @@ Node SygusSampler::getRandomValue(TypeNode tn) } } } - return Node::null(); + // default: use type enumerator + unsigned counter = 0; + while (Random::getRandom().pickWithProb(0.5)) + { + counter++; + } + Node ret = d_tenum.getEnumerateTerm(tn, counter); + if (ret.isNull()) + { + // beyond bounds, return the first + ret = d_tenum.getEnumerateTerm(tn, 0); + } + return ret; } Node SygusSampler::getSygusRandomValue(TypeNode tn, @@ -719,28 +740,23 @@ void SygusSampler::registerSygusType(TypeNode tn) } } -SygusSamplerExt::SygusSamplerExt() : d_ssenm(*this) {} +SygusSamplerExt::SygusSamplerExt() : d_drewrite(nullptr), d_ssenm(*this) {} -void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe, - Node f, - unsigned nsamples, - bool useSygusType) +void SygusSamplerExt::initializeSygus(TermDbSygus* tds, + Node f, + unsigned nsamples, + bool useSygusType) { - SygusSampler::initializeSygus( - qe->getTermDatabaseSygus(), f, nsamples, useSygusType); - - // initialize the dynamic rewriter - std::stringstream ss; - ss << f; - if (options::sygusRewSynthFilterCong()) - { - d_drewrite = - std::unique_ptr<DynamicRewriter>(new DynamicRewriter(ss.str(), qe)); - } + SygusSampler::initializeSygus(tds, f, nsamples, useSygusType); d_pairs.clear(); d_match_trie.clear(); } +void SygusSamplerExt::setDynamicRewriter(DynamicRewriter* dr) +{ + d_drewrite = dr; +} + Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) { Node eq_n = SygusSampler::registerTerm(n, forceKeep); @@ -896,6 +912,9 @@ bool SygusSamplerExt::notify(Node s, for (unsigned i = 0, size = vars.size(); i < size; i++) { Trace("sse-match") << " " << vars[i] << " -> " << subs[i] << std::endl; + // TODO (#1923) ensure that we use an internal representation to + // ensure polymorphism is handled correctly + Assert(vars[i].getType().isComparableTo(subs[i].getType())); } } Assert(it != d_pairs.end()); |