From 30398e8552bd372264d99743d39b826e1a2b53be Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Mar 2018 11:59:42 -0600 Subject: [PATCH] Print candidate rewrites in terms of original grammar (#1635) --- src/theory/datatypes/datatypes_sygus.cpp | 3 +- .../sygus/ce_guided_conjecture.cpp | 25 ++++++++----- src/theory/quantifiers/sygus_sampler.cpp | 37 ++++++++++++++++--- src/theory/quantifiers/sygus_sampler.h | 22 +++++++++-- 4 files changed, 66 insertions(+), 21 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 728cd8135..6f533bfe0 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -794,7 +794,8 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, d_sampler[a].find(tn); if (its == d_sampler[a].end()) { - d_sampler[a][tn].initializeSygus(d_tds, nv, options::sygusSamples()); + d_sampler[a][tn].initializeSygus( + d_tds, nv, options::sygusSamples(), false); its = d_sampler[a].find(tn); } Node bvr_sample_ret; diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index f2a1c334c..ac0982c4e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -620,29 +620,34 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation if (its == d_sampler.end()) { d_sampler[prog].initializeSygusExt( - d_qe, prog, options::sygusSamples()); + d_qe, prog, options::sygusSamples(), true); its = d_sampler.find(prog); } - Node solb = sygusDb->sygusToBuiltin(sol, prog.getType()); - Node eq_sol = its->second.registerTerm(solb); + Node eq_sol = its->second.registerTerm(sol); // eq_sol is a candidate solution that is equivalent to sol - if (eq_sol != solb) + if (eq_sol != sol) { ++(cei->d_statistics.d_candidate_rewrites); if (!eq_sol.isNull()) { - // Terms solb and eq_sol are equivalent under sample points but do - // not rewrite to the same term. Hence, this indicates a candidate - // rewrite. - out << "(candidate-rewrite " << solb << " " << eq_sol << ")" - << std::endl; + // The analog of terms sol and eq_sol are equivalent under sample + // points but do not rewrite to the same term. Hence, this indicates + // a candidate rewrite. + Printer* p = Printer::getPrinter(options::outputLanguage()); + out << "(candidate-rewrite "; + p->toStreamSygus(out, sol); + out << " "; + p->toStreamSygus(out, eq_sol); + out << ")" << std::endl; ++(cei->d_statistics.d_candidate_rewrites_print); // debugging information if (Trace.isOn("sygus-rr-debug")) { ExtendedRewriter* er = sygusDb->getExtRewriter(); + Node solb = sygusDb->sygusToBuiltin(sol); Node solbr = er->extendedRewrite(solb); - Node eq_solr = er->extendedRewrite(eq_sol); + Node eq_solb = sygusDb->sygusToBuiltin(eq_sol); + Node eq_solr = er->extendedRewrite(eq_solb); Trace("sygus-rr-debug") << "; candidate #1 ext-rewrites to: " << solbr << std::endl; Trace("sygus-rr-debug") diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index fa0478ac7..0b9254818 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -64,13 +64,17 @@ Node LazyTrie::add(Node n, return Node::null(); } -SygusSampler::SygusSampler() : d_tds(nullptr), d_is_valid(false) {} +SygusSampler::SygusSampler() + : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false) +{ +} void SygusSampler::initialize(TypeNode tn, std::vector& vars, unsigned nsamples) { d_tds = nullptr; + d_use_sygus_type = false; d_is_valid = true; d_tn = tn; d_ftn = TypeNode::null(); @@ -105,9 +109,13 @@ void SygusSampler::initialize(TypeNode tn, initializeSamples(nsamples); } -void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples) +void SygusSampler::initializeSygus(TermDbSygus* tds, + Node f, + unsigned nsamples, + bool useSygusType) { d_tds = tds; + d_use_sygus_type = useSygusType; d_is_valid = true; d_ftn = f.getType(); Assert(d_ftn.isDatatype()); @@ -282,8 +290,23 @@ Node SygusSampler::registerTerm(Node n, bool forceKeep) { if (d_is_valid) { - Assert(n.getType() == d_tn); - return d_trie.add(n, this, 0, d_samples.size(), forceKeep); + Node bn = n; + // if this is a sygus type, get its builtin analog + if (d_use_sygus_type) + { + Assert(!d_ftn.isNull()); + bn = d_tds->sygusToBuiltin(n); + bn = Rewriter::rewrite(bn); + d_builtin_to_sygus[bn] = n; + } + Assert(bn.getType() == d_tn); + Node res = d_trie.add(bn, this, 0, d_samples.size(), forceKeep); + if (d_use_sygus_type) + { + Assert(d_builtin_to_sygus.find(res) == d_builtin_to_sygus.end()); + res = res != bn ? d_builtin_to_sygus[res] : n; + } + return res; } return n; } @@ -645,9 +668,11 @@ void SygusSampler::registerSygusType(TypeNode tn) void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe, Node f, - unsigned nsamples) + unsigned nsamples, + bool useSygusType) { - SygusSampler::initializeSygus(qe->getTermDatabaseSygus(), f, nsamples); + SygusSampler::initializeSygus( + qe->getTermDatabaseSygus(), f, nsamples, useSygusType); // initialize the dynamic rewriter std::stringstream ss; diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index abc9232af..5fcfc1c93 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -148,11 +148,18 @@ class SygusSampler : public LazyTrieEvaluator /** initialize sygus * * tds : pointer to sygus database, - * f : a term of some SyGuS datatype type whose (builtin) values we will be + * f : a term of some SyGuS datatype type whose values we will be * testing under the free variables in the grammar of f, - * nsamples : number of sample points this class will test. + * nsamples : number of sample points this class will test, + * useSygusType : whether we will register terms with this sampler that have + * the same type as f. If this flag is false, then we will be registering + * terms of the analog of the type of f, that is, the builtin type that + * f's type encodes in the deep embedding. */ - void initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples); + void initializeSygus(TermDbSygus* tds, + Node f, + unsigned nsamples, + bool useSygusType); /** register term n with this sampler database * * forceKeep is whether we wish to force that n is chosen as a representative @@ -222,6 +229,10 @@ class SygusSampler : public LazyTrieEvaluator TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; + /** whether we are registering terms of type d_ftn */ + bool d_use_sygus_type; + /** map from builtin terms to the sygus term they correspond to */ + std::map d_builtin_to_sygus; /** all variables we are sampling values for */ std::vector d_vars; /** type variables @@ -329,7 +340,10 @@ class SygusSamplerExt : public SygusSampler { public: /** initialize extended */ - void initializeSygusExt(QuantifiersEngine* qe, Node f, unsigned nsamples); + void initializeSygusExt(QuantifiersEngine* qe, + Node f, + unsigned nsamples, + bool useSygusType); /** register term n with this sampler database * * This returns either null, or a term ret with the same guarantees as -- 2.30.2