From 5035105b8d3ca8d260581581ca2beccf9ead3354 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 4 Feb 2018 12:46:05 -0600 Subject: [PATCH] Sample based on sygus grammar by default (#1558) --- src/options/quantifiers_options | 2 + src/theory/quantifiers/sygus_sampler.cpp | 187 +++++++++++++++++- src/theory/quantifiers/sygus_sampler.h | 53 ++++- .../quantifiers/term_database_sygus.cpp | 6 + src/theory/quantifiers/term_database_sygus.h | 84 ++++++-- 5 files changed, 307 insertions(+), 25 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 34af81033..c58313390 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -308,6 +308,8 @@ option sygusRewVerify --sygus-rr-verify bool :default false use sygus to verify the correctness of rewrite rules via sampling option sygusSamples --sygus-samples=N int :read-write :default 100 :read-write number of points to consider when doing sygus rewriter sample testing +option sygusSampleGrammar --sygus-sample-grammar bool :default true + when applicable, use grammar for choosing sample points # CEGQI applied to general quantified formulas option cbqi --cbqi bool :read-write :default false diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 0b8f390f3..82720dd5e 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus_sampler.h" +#include "options/quantifiers_options.h" #include "util/bitvector.h" #include "util/random.h" @@ -80,6 +81,9 @@ void SygusSampler::initialize(TypeNode tn, d_var_index[sv] = d_type_vars[svt].size(); d_type_vars[svt].push_back(sv); } + d_rvalue_cindices.clear(); + d_rvalue_null_cindices.clear(); + d_var_sygus_types.clear(); initializeSamples(nsamples); } @@ -109,6 +113,10 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples) d_type_vars[svt].push_back(sv); } } + d_rvalue_cindices.clear(); + d_rvalue_null_cindices.clear(); + d_var_sygus_types.clear(); + registerSygusType(d_ftn); initializeSamples(nsamples); } @@ -123,28 +131,90 @@ void SygusSampler::initializeSamples(unsigned nsamples) Trace("sygus-sample") << " var #" << types.size() << " : " << v << " : " << vt << std::endl; } + std::map >::iterator> sts; + if (options::sygusSampleGrammar()) + { + for (unsigned j = 0, size = types.size(); j < size; j++) + { + sts[j] = d_var_sygus_types.find(d_vars[j]); + } + } + + unsigned nduplicates = 0; for (unsigned i = 0; i < nsamples; i++) { std::vector sample_pt; - Trace("sygus-sample") << "Sample point #" << i << " : "; for (unsigned j = 0, size = types.size(); j < size; j++) { - Node r = getRandomValue(types[j]); + Node v = d_vars[j]; + Node r; + if (options::sygusSampleGrammar()) + { + // choose a random start sygus type, if possible + if (sts[j] != d_var_sygus_types.end()) + { + unsigned ntypes = sts[j]->second.size(); + Assert(ntypes > 0); + unsigned index = Random::getRandom().pick(0, ntypes - 1); + if (index < ntypes) + { + // currently hard coded to 0.0, 0.5 + r = getSygusRandomValue(sts[j]->second[index], 0.0, 0.5); + } + } + } if (r.isNull()) { - Trace("sygus-sample") << "INVALID"; - d_is_valid = false; + r = getRandomValue(types[j]); + if (r.isNull()) + { + d_is_valid = false; + } } - Trace("sygus-sample") << r << " "; sample_pt.push_back(r); } - Trace("sygus-sample") << std::endl; - d_samples.push_back(sample_pt); + if (d_samples_trie.add(sample_pt)) + { + if (Trace.isOn("sygus-sample")) + { + Trace("sygus-sample") << "Sample point #" << i << " : "; + for (const Node& r : sample_pt) + { + Trace("sygus-sample") << r << " "; + } + Trace("sygus-sample") << std::endl; + } + d_samples.push_back(sample_pt); + } + else + { + i--; + nduplicates++; + if (nduplicates == nsamples * 10) + { + Trace("sygus-sample") + << "...WARNING: excessive duplicates, cut off sampling at " << i + << "/" << nsamples << " points." << std::endl; + break; + } + } } d_trie.clear(); } +bool SygusSampler::PtTrie::add(std::vector& pt) +{ + PtTrie* curr = this; + for (unsigned i = 0, size = pt.size(); i < size; i++) + { + curr = &(curr->d_children[pt[i]]); + } + bool retVal = curr->d_children.empty(); + curr = &(curr->d_children[Node::null()]); + return retVal; +} + Node SygusSampler::registerTerm(Node n, bool forceKeep) { if (d_is_valid) @@ -389,6 +459,109 @@ Node SygusSampler::getRandomValue(TypeNode tn) return Node::null(); } +Node SygusSampler::getSygusRandomValue(TypeNode tn, + double rchance, + double rinc, + unsigned depth) +{ + Assert(tn.isDatatype()); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Assert(dt.isSygus()); + Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end()); + Trace("sygus-sample-grammar") << "Sygus random value " << tn + << ", depth = " << depth + << ", rchance = " << rchance << std::endl; + // check if we terminate on this call + // we refuse to enumerate terms of 10+ depth as a hard limit + bool terminate = Random::getRandom().pickWithProb(rchance) || depth >= 10; + // if we terminate, only nullary constructors can be chosen + std::vector& cindices = + terminate ? d_rvalue_null_cindices[tn] : d_rvalue_cindices[tn]; + unsigned ncons = cindices.size(); + // select a random constructor, or random value when index=ncons. + unsigned index = Random::getRandom().pick(0, ncons); + Trace("sygus-sample-grammar") << "Random index 0..." << ncons + << " was : " << index << std::endl; + if (index < ncons) + { + Trace("sygus-sample-grammar") << "Recurse constructor index #" << index + << std::endl; + unsigned cindex = cindices[index]; + Assert(cindex < dt.getNumConstructors()); + const DatatypeConstructor& dtc = dt[cindex]; + // more likely to terminate in recursive calls + double rchance_new = rchance + (1.0 - rchance) * rinc; + std::map pre; + bool success = true; + // generate random values for all arguments + for (unsigned i = 0, nargs = dtc.getNumArgs(); i < nargs; i++) + { + TypeNode tnc = d_tds->getArgType(dtc, i); + Node c = getSygusRandomValue(tnc, rchance_new, rinc, depth + 1); + if (c.isNull()) + { + success = false; + Trace("sygus-sample-grammar") << "...fail." << std::endl; + break; + } + Trace("sygus-sample-grammar") << " child #" << i << " : " << c + << std::endl; + pre[i] = c; + } + if (success) + { + Trace("sygus-sample-grammar") << "mkGeneric" << std::endl; + Node ret = d_tds->mkGeneric(dt, cindex, pre); + Trace("sygus-sample-grammar") << "...returned " << ret << std::endl; + ret = Rewriter::rewrite(ret); + Trace("sygus-sample-grammar") << "...after rewrite " << ret << std::endl; + Assert(ret.isConst()); + return ret; + } + } + Trace("sygus-sample-grammar") << "...resort to random value" << std::endl; + // if we did not generate based on the grammar, pick a random value + return getRandomValue(TypeNode::fromType(dt.getSygusType())); +} + +// recursion depth bounded by number of types in grammar (small) +void SygusSampler::registerSygusType(TypeNode tn) +{ + if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end()) + { + d_rvalue_cindices[tn].clear(); + Assert(tn.isDatatype()); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Assert(dt.isSygus()); + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + const DatatypeConstructor& dtc = dt[i]; + Node sop = Node::fromExpr(dtc.getSygusOp()); + bool isVar = std::find(d_vars.begin(), d_vars.end(), sop) != d_vars.end(); + if (isVar) + { + // if it is a variable, add it to the list of sygus types for that var + d_var_sygus_types[sop].push_back(tn); + } + else + { + // otherwise, it is a constructor for sygus random value + d_rvalue_cindices[tn].push_back(i); + if (dtc.getNumArgs() == 0) + { + d_rvalue_null_cindices[tn].push_back(i); + } + } + // recurse on all subfields + for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++) + { + TypeNode tnc = d_tds->getArgType(dtc, j); + registerSygusType(tnc); + } + } + } +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 09f4124fe..02b60d155 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -194,6 +194,19 @@ class SygusSampler : public LazyTrieEvaluator TermDbSygus* d_tds; /** samples */ std::vector > d_samples; + /** data structure to check duplication of sample points */ + class PtTrie + { + public: + /** add pt to this trie, returns true if pt is not a duplicate. */ + bool add(std::vector& pt); + + private: + /** the children of this node */ + std::map d_children; + }; + /** a trie for samples */ + PtTrie d_samples_trie; /** type of nodes we will be registering with this class */ TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ @@ -246,11 +259,45 @@ class SygusSampler : public LazyTrieEvaluator * length, currently by a repeated coin flip. * Real : returns the division of two random integers, where the denominator * is omitted if it is zero. - * - * TODO (#1549): improve this function. Can use the grammar to generate - * interesting sample points. */ Node getRandomValue(TypeNode tn); + /** get sygus random value + * + * Returns a random value based on the sygus type tn. The return value is + * a constant in the analog type of tn. This function chooses either to + * return a random value, or otherwise will construct a constant based on + * a random constructor of tn whose builtin operator is not a variable. + * + * rchance: the chance that the call to this function will be forbidden + * from making recursive calls and instead must return a value based on + * a nullary constructor of tn or based on getRandomValue above. + * rinc: the percentage to increment rchance on recursive calls. + * + * For example, consider the grammar: + * A -> x | y | 0 | 1 | +( A, A ) | ite( B, A, A ) + * B -> A = A + * If we call this function on A and rchance is 0.0, there are five evenly + * chosen possibilities, either we return a random value via getRandomValue + * above, or we choose one of the four non-variable constructors of A. + * Say we choose ite, then we recursively call this function for + * B, A, and A, which return constants c1, c2, and c3. Then, this function + * returns the rewritten form of ite( c1, c2, c3 ). + * If on the other hand, rchance was 0.5 and rand() < 0.5. Then, we force + * this call to terminate by either selecting a random value via + * getRandomValue, 0 or 1. + */ + Node getSygusRandomValue(TypeNode tn, + double rchance, + double rinc, + unsigned depth = 0); + /** map from sygus types to non-variable constructors */ + std::map > d_rvalue_cindices; + /** map from sygus types to non-variable nullary constructors */ + std::map > d_rvalue_null_cindices; + /** map from variables to sygus types that include them */ + std::map > d_var_sygus_types; + /** register sygus type, intializes the above two data structures */ + void registerSygusType(TypeNode tn); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index 87bfa1901..7d7cc624e 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -147,6 +147,12 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int return ret; } +Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map& pre) +{ + std::map var_count; + return mkGeneric(dt, c, var_count, pre); +} + Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { Assert( n.getType()==tn ); Assert( tn.isDatatype() ); diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h index 586ef0777..af1ef50b6 100644 --- a/src/theory/quantifiers/term_database_sygus.h +++ b/src/theory/quantifiers/term_database_sygus.h @@ -68,6 +68,56 @@ class TermDbSygus { SygusExplain* getExplain() { return d_syexp.get(); } /** get the extended rewrite utility */ ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); } + //-----------------------------conversion from sygus to builtin + /** get free variable + * + * This class caches a list of free variables for each type, which are + * used, for instance, for constructing canonical forms of terms with free + * variables. This function returns the i^th free variable for type tn. + * If useSygusType is true, then this function returns a variable of the + * analog type for sygus type tn (see d_fv for details). + */ + TNode getFreeVar(TypeNode tn, int i, bool useSygusType = false); + /** get free variable and increment + * + * This function returns the next free variable for type tn, and increments + * the counter in var_count for that type. + */ + TNode getFreeVarInc(TypeNode tn, + std::map& var_count, + bool useSygusType = false); + /** returns true if n is a cached free variable (in d_fv). */ + bool isFreeVar(Node n) { return d_fv_stype.find(n) != d_fv_stype.end(); } + /** returns the index of n in the free variable cache (d_fv). */ + int getVarNum(Node n) { return d_fv_num[n]; } + /** returns true if n has a cached free variable (in d_fv). */ + bool hasFreeVar(Node n); + /** make generic + * + * This function returns a builtin term f( t1, ..., tn ) where f is the + * builtin op of the sygus datatype constructor specified by arguments + * dt and c. The mapping pre maps child indices to the term for that index + * in the term we are constructing. That is, for each i = 1,...,n: + * If i is in the domain of pre, then ti = pre[i]. + * If i is not in the domain of pre, then ti = d_fv[1][ var_count[Ti ] ], + * and var_count[Ti] is incremented. + */ + Node mkGeneric(const Datatype& dt, + int c, + std::map& var_count, + std::map& pre); + /** same as above, but with empty var_count */ + Node mkGeneric(const Datatype& dt, int c, std::map& pre); + /** sygus to builtin + * + * Given a sygus datatype term n of type tn, this function returns its analog, + * that is, the term that n encodes. + */ + Node sygusToBuiltin(Node n, TypeNode tn); + /** same as above, but without tn */ + Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); } + //-----------------------------end conversion from sygus to builtin + private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -88,23 +138,31 @@ class TermDbSygus { */ std::map d_enum_to_active_guard; + //-----------------------------conversion from sygus to builtin + /** cache for sygusToBuiltin */ + std::map > d_sygus_to_builtin; + /** a cache of fresh variables for each type + * + * We store two versions of this list: + * index 0: mapping from builtin types to fresh variables of that type, + * index 1: mapping from sygus types to fresh varaibles of the type they + * encode. + */ + std::map > d_fv[2]; + /** Maps free variables to the domain type they are associated with in d_fv */ + std::map d_fv_stype; + /** Maps free variables to their index in d_fv. */ + std::map d_fv_num; + /** recursive helper for hasFreeVar, visited stores nodes we have visited. */ + bool hasFreeVar(Node n, std::map& visited); + //-----------------------------end conversion from sygus to builtin + // TODO :issue #1235 : below here needs refactor public: Node d_true; Node d_false; - private: - std::map< TypeNode, std::vector< Node > > d_fv[2]; - std::map< Node, TypeNode > d_fv_stype; - std::map< Node, int > d_fv_num; - bool hasFreeVar( Node n, std::map< Node, bool >& visited ); -public: - TNode getFreeVar( TypeNode tn, int i, bool useSygusType = false ); - TNode getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType = false ); - bool isFreeVar( Node n ) { return d_fv_stype.find( n )!=d_fv_stype.end(); } - int getVarNum( Node n ) { return d_fv_num[n]; } - bool hasFreeVar( Node n ); private: void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ); bool involvesDivByZero( Node n, std::map< Node, bool >& visited ); @@ -122,7 +180,6 @@ private: std::map > d_semantic_skolem; // normalized map std::map > d_normalized; - std::map > d_sygus_to_builtin; // grammar information // root -> type -> _ std::map > d_min_type_depth; @@ -165,9 +222,6 @@ private: bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ); TypeNode getSygusTypeForVar( Node v ); - Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); - Node sygusToBuiltin( Node n, TypeNode tn ); - Node sygusToBuiltin( Node n ) { return sygusToBuiltin( n, n.getType() ); } Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ); Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); Node getNormalized(TypeNode t, Node prog); -- 2.30.2