From: Andrew Reynolds Date: Thu, 1 Feb 2018 18:13:54 +0000 (-0600) Subject: Use sygus to synthesize/verify rewrite rules (#1547) X-Git-Tag: cvc5-1.0.0~5340 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dbd1797f64216ba9eb598579de27cc45814e1db4;p=cvc5.git Use sygus to synthesize/verify rewrite rules (#1547) --- diff --git a/src/Makefile.am b/src/Makefile.am index a6c58e281..4720186f4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -465,6 +465,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus_grammar_norm.h \ theory/quantifiers/sygus_process_conj.cpp \ theory/quantifiers/sygus_process_conj.h \ + theory/quantifiers/sygus_sampler.cpp \ + theory/quantifiers/sygus_sampler.h \ theory/quantifiers/symmetry_breaking.cpp \ theory/quantifiers/symmetry_breaking.h \ theory/quantifiers/term_database.cpp \ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index c6eb1cd5e..9d717c0ba 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -295,9 +295,17 @@ option sygusCRefEval --sygus-cref-eval bool :default true option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true use min explain for direct evaluation of refinement lemmas for conflict analysis -option sygusStream --sygus-stream bool :default false +option sygusStream --sygus-stream bool :read-write :default false enumerate a stream of solutions instead of terminating after the first one +# internal uses of sygus +option sygusRewSynth --sygus-rr-synth bool :default false + use sygus to enumerate candidate rewrite rules via sampling +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 + # CEGQI applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 11c226ee4..0c8723ff6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1885,6 +1885,11 @@ void SmtEngine::setDefaults() { if( !options::instNoEntail.wasSetByUser() ){ options::instNoEntail.set( false ); } + if (options::sygusRewSynth()) + { + // rewrite rule synthesis implies that sygus stream must be true + options::sygusStream.set(true); + } if (options::sygusStream()) { // PBE and streaming modes are incompatible diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index b06c96e68..7c3ab71d8 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -808,7 +808,38 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, Trace("sygus-sb-exc") << " ......programs " << prev_bv << " and " << bv << " rewrite to " << bvr << "." << std::endl; } } - + + if (options::sygusRewVerify()) + { + // add to the sampler database object + std::map::iterator its = + d_sampler.find(a); + if (its == d_sampler.end()) + { + d_sampler[a].initialize(d_tds, a, options::sygusSamples()); + its = d_sampler.find(a); + } + Node sample_ret = its->second.registerTerm(bv); + d_cache[a].d_search_val_sample[nv] = sample_ret; + if (itsv != d_cache[a].d_search_val[tn].end()) + { + // if the analog of this term and another term were rewritten to the + // same term, then they should be equivalent under examples. + Node prev = itsv->second; + Node prev_sample_ret = d_cache[a].d_search_val_sample[prev]; + if (sample_ret != prev_sample_ret) + { + Node prev_bv = d_tds->sygusToBuiltin(prev, tn); + // we have detected unsoundness in the rewriter + Options& nodeManagerOptions = + NodeManager::currentNM()->getOptions(); + std::ostream* out = nodeManagerOptions.getOut(); + (*out) << "(unsound-rewrite " << prev_bv << " " << bv << ")" + << std::endl; + } + } + } + if( !bad_val_bvr.isNull() ){ Node bad_val = nv; Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr]; diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 099b45fec..1162f767f 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -30,6 +30,7 @@ #include "expr/datatype.h" #include "expr/node.h" #include "theory/quantifiers/ce_guided_conjecture.h" +#include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers/term_database.h" namespace CVC4 { @@ -80,14 +81,34 @@ private: SearchCache(){} std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_search_terms; std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_sb_lemmas; - // search values + /** search value + * + * For each sygus type, a map from a builtin term to a sygus term for that + * type that we encountered during the search whose analog rewrites to that + * term. The range of this map can be updated if we later encounter a sygus + * term that also rewrites to the builtin value but has a smaller term size. + */ std::map< TypeNode, std::map< Node, Node > > d_search_val; + /** the size of terms in the range of d_search val. */ std::map< TypeNode, std::map< Node, unsigned > > d_search_val_sz; - std::map< TypeNode, std::map< Node, Node > > d_search_val_b; + /** search value sample + * + * This is used for the sygusRewVerify() option. For each sygus term we + * register in this cache, this stores the value returned by calling + * SygusSample::registerTerm(...) on its analog. + */ + std::map d_search_val_sample; + /** For each term, whether this cache has processed that term */ std::map< Node, bool > d_search_val_proc; }; // anchor -> cache std::map< Node, SearchCache > d_cache; + /** a sygus sampler object for each anchor + * + * This is used for the sygusRewVerify() option to verify the correctness of + * the rewriter. + */ + std::map d_sampler; Node d_null; void assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ); // register search term diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 378b26eef..74d5cef47 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -435,6 +435,12 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& std::stringstream ss; Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv); Trace("cegqi-engine") << ss.str() << " "; + if (Trace.isOn("cegqi-engine-rr")) + { + Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); + bv = Rewriter::rewrite(bv); + Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + } } Assert( !nv.isNull() ); } @@ -628,6 +634,63 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol); } out << ")" << std::endl; + + if (status != 0 && options::sygusRewSynth()) + { + TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); + std::map::iterator its = d_sampler.find(prog); + if (its == d_sampler.end()) + { + d_sampler[prog].initialize(sygusDb, prog, options::sygusSamples()); + its = d_sampler.find(prog); + } + Node solb = sygusDb->sygusToBuiltin(sol, prog.getType()); + Node eq_sol = its->second.registerTerm(solb); + // eq_sol is a candidate solution that is equivalent to sol + if (eq_sol != solb) + { + // one of eq_sol or solb must be ordered + bool eqor = its->second.isOrdered(eq_sol); + bool sor = its->second.isOrdered(solb); + bool outputRewrite = false; + if (eqor || sor) + { + outputRewrite = true; + // if only one is ordered, then the ordered one must contain the + // free variables of the other + if (!eqor) + { + outputRewrite = its->second.containsFreeVariables(solb, eq_sol); + } + else if (!sor) + { + outputRewrite = its->second.containsFreeVariables(eq_sol, solb); + } + } + + if (outputRewrite) + { + // 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; + // if the previous value stored was unordered, but this is + // ordered, we prefer this one. Thus, we force its addition to the + // sampler database. + if (!eqor) + { + its->second.registerTerm(solb, true); + } + } + else + { + Trace("sygus-synth-rr") + << "Alpha equivalent candidate rewrite : " << eq_sol << " " + << solb << std::endl; + } + } + } } } } diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h index 0f000bba5..e57b545e6 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.h +++ b/src/theory/quantifiers/ce_guided_conjecture.h @@ -24,6 +24,7 @@ #include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/sygus_grammar_cons.h" #include "theory/quantifiers/sygus_process_conj.h" +#include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -197,6 +198,12 @@ private: /** the guard for non-syntax-guided synthesis */ Node d_nsg_guard; //-------------------------------- end non-syntax guided (deprecated) + /** sygus sampler objects for each program variable + * + * This is used for the sygusRewSynth() option to synthesize new candidate + * rewrite rules. + */ + std::map d_sampler; }; } /* namespace CVC4::theory::quantifiers */ diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp new file mode 100644 index 000000000..b5e63a6ab --- /dev/null +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -0,0 +1,355 @@ +/********************* */ +/*! \file sygus_sampler.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus_sampler + **/ + +#include "theory/quantifiers/sygus_sampler.h" + +#include "util/bitvector.h" +#include "util/random.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +Node LazyTrie::add(Node n, + LazyTrieEvaluator* ev, + unsigned index, + unsigned ntotal, + bool forceKeep) +{ + LazyTrie* lt = this; + while (lt != NULL) + { + if (index == ntotal) + { + // lazy child holds the leaf data + if (lt->d_lazy_child.isNull() || forceKeep) + { + lt->d_lazy_child = n; + } + return lt->d_lazy_child; + } + std::vector ex; + if (lt->d_children.empty()) + { + if (lt->d_lazy_child.isNull()) + { + // no one has been here, we are done + lt->d_lazy_child = n; + return lt->d_lazy_child; + } + // evaluate the lazy child + Node e_lc = ev->evaluate(lt->d_lazy_child, index); + // store at next level + lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child; + // replace + lt->d_lazy_child = Node::null(); + } + // recurse + Node e = ev->evaluate(n, index); + lt = <->d_children[e]; + index = index + 1; + } + return Node::null(); +} + +SygusSampler::SygusSampler() : d_tds(nullptr), d_is_valid(false) {} + +void SygusSampler::initialize(TermDbSygus* tds, Node f, unsigned nsamples) +{ + d_tds = tds; + d_is_valid = true; + d_ftn = f.getType(); + Assert(d_ftn.isDatatype()); + const Datatype& dt = static_cast(d_ftn.toType()).getDatatype(); + Assert(dt.isSygus()); + + Trace("sygus-sample") << "Register sampler for " << f << std::endl; + + d_var_index.clear(); + d_type_vars.clear(); + std::vector types; + // get the sygus variable list + Node var_list = Node::fromExpr(dt.getSygusVarList()); + if (!var_list.isNull()) + { + for (const Node& sv : var_list) + { + TypeNode svt = sv.getType(); + d_var_index[sv] = d_type_vars[svt].size(); + d_type_vars[svt].push_back(sv); + types.push_back(svt); + Trace("sygus-sample") << " var #" << types.size() << " : " << sv << " : " + << svt << std::endl; + } + } + + d_samples.clear(); + 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]); + if (r.isNull()) + { + Trace("sygus-sample") << "INVALID"; + d_is_valid = false; + } + Trace("sygus-sample") << r << " "; + sample_pt.push_back(r); + } + Trace("sygus-sample") << std::endl; + d_samples.push_back(sample_pt); + } + + d_trie.clear(); +} + +Node SygusSampler::registerTerm(Node n, bool forceKeep) +{ + if (d_is_valid) + { + return d_trie.add(n, this, 0, d_samples.size(), forceKeep); + } + return n; +} + +bool SygusSampler::isContiguous(Node n) +{ + // compute free variables in n + std::vector fvs; + computeFreeVariables(n, fvs); + // compute contiguous condition + for (const std::pair >& p : d_type_vars) + { + bool foundNotFv = false; + for (const Node& v : p.second) + { + bool hasFv = std::find(fvs.begin(), fvs.end(), v) != fvs.end(); + if (!hasFv) + { + foundNotFv = true; + } + else if (foundNotFv) + { + return false; + } + } + } + return true; +} + +void SygusSampler::computeFreeVariables(Node n, std::vector& fvs) +{ + std::unordered_set visited; + std::unordered_set::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar()) + { + if (d_var_index.find(cur) != d_var_index.end()) + { + fvs.push_back(cur); + } + } + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); +} + +bool SygusSampler::isOrdered(Node n) +{ + // compute free variables in n for each type + std::map > fvs; + + std::unordered_set visited; + std::unordered_set::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar()) + { + std::map::iterator itv = d_var_index.find(cur); + if (itv != d_var_index.end()) + { + TypeNode tn = cur.getType(); + // if this variable is out of order + if (itv->second != fvs[tn].size()) + { + return false; + } + fvs[tn].push_back(cur); + } + } + for (unsigned j = 0, nchildren = cur.getNumChildren(); j < nchildren; j++) + { + visit.push_back(cur[(nchildren - j) - 1]); + } + } + } while (!visit.empty()); + return true; +} + +bool SygusSampler::containsFreeVariables(Node a, Node b) +{ + // compute free variables in a + std::vector fvs; + computeFreeVariables(a, fvs); + + std::unordered_set visited; + std::unordered_set::iterator it; + std::vector visit; + TNode cur; + visit.push_back(b); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar()) + { + if (std::find(fvs.begin(), fvs.end(), cur) == fvs.end()) + { + return false; + } + } + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + return true; +} + +Node SygusSampler::evaluate(Node n, unsigned index) +{ + Assert(index < d_samples.size()); + Node ev = d_tds->evaluateBuiltin(d_ftn, n, d_samples[index]); + Trace("sygus-sample-ev") << "( " << n << ", " << index << " ) -> " << ev + << std::endl; + return ev; +} + +Node SygusSampler::getRandomValue(TypeNode tn) +{ + NodeManager* nm = NodeManager::currentNM(); + if (tn.isBoolean()) + { + return nm->mkConst(Random::getRandom().pickWithProb(0.5)); + } + else if (tn.isBitVector()) + { + unsigned sz = tn.getBitVectorSize(); + std::stringstream ss; + for (unsigned i = 0; i < sz; i++) + { + ss << (Random::getRandom().pickWithProb(0.5) ? "1" : "0"); + } + return nm->mkConst(BitVector(ss.str(), 2)); + } + else if (tn.isString() || tn.isInteger()) + { + std::vector vec; + double ext_freq = .5; + unsigned base = 10; + while (Random::getRandom().pickWithProb(ext_freq)) + { + // add a digit + vec.push_back(Random::getRandom().pick(0, base)); + } + if (tn.isString()) + { + return nm->mkConst(String(vec)); + } + else if (tn.isInteger()) + { + Rational baser(base); + Rational curr(1); + std::vector sum; + for (unsigned j = 0, size = vec.size(); j < size; j++) + { + Node digit = nm->mkConst(Rational(vec[j]) * curr); + sum.push_back(digit); + curr = curr * baser; + } + Node ret; + if (sum.empty()) + { + ret = nm->mkConst(Rational(0)); + } + else if (sum.size() == 1) + { + ret = sum[0]; + } + else + { + ret = nm->mkNode(kind::PLUS, sum); + } + + if (Random::getRandom().pickWithProb(0.5)) + { + // negative + ret = nm->mkNode(kind::UMINUS, ret); + } + ret = Rewriter::rewrite(ret); + Assert(ret.isConst()); + return ret; + } + } + else if (tn.isReal()) + { + Node s = getRandomValue(nm->integerType()); + Node r = getRandomValue(nm->integerType()); + if (!s.isNull() && !r.isNull()) + { + Rational sr = s.getConst(); + Rational rr = s.getConst(); + if (rr.sgn() == 0) + { + return s; + } + else + { + return nm->mkConst(sr / rr); + } + } + } + return Node::null(); +} + +} /* 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 new file mode 100644 index 000000000..897931649 --- /dev/null +++ b/src/theory/quantifiers/sygus_sampler.h @@ -0,0 +1,237 @@ +/********************* */ +/*! \file sygus_sampler.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus_sampler + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H + +#include +#include "theory/quantifiers/term_database_sygus.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** abstract evaluator class + * + * This class is used for the LazyTrie data structure below. + */ +class LazyTrieEvaluator +{ + public: + virtual Node evaluate(Node n, unsigned index) = 0; +}; + +/** LazyTrie + * + * This is a trie where terms are added in a lazy fashion. This data structure + * is useful, for instance, when we are only interested in when two terms + * map to the same node in the trie but we need not care about computing + * exactly where they are. + * + * In other words, when a term n is added to this trie, we do not insist + * that n is placed at the maximal depth of the trie. Instead, we place n at a + * minimal depth node that has no children. In this case we say n is partially + * evaluated in this trie. + * + * This class relies on an abstract evaluator interface above, which evaluates + * nodes for indices. + * + * For example, say we have terms a, b, c and an evaluator ev where: + * ev->evaluate( a, 0,1,2 ) = 0, 5, 6 + * ev->evaluate( b, 0,1,2 ) = 1, 3, 0 + * ev->evaluate( c, 0,1,2 ) = 1, 3, 2 + * After adding a to the trie, we get: + * root: a + * After adding b to the resulting trie, we get: + * root: null + * d_children[0]: a + * d_children[1]: b + * After adding c to the resulting trie, we get: + * root: null + * d_children[0]: a + * d_children[1]: null + * d_children[3]: null + * d_children[0] : b + * d_children[2] : c + * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ). + */ +class LazyTrie +{ + public: + LazyTrie() {} + ~LazyTrie() {} + /** the data at this node, which may be partially evaluated */ + Node d_lazy_child; + /** the children of this node */ + std::map d_children; + /** clear the trie */ + void clear() { d_children.clear(); } + /** add n to the trie + * + * This function returns a node that is mapped to the same node in the trie + * if one exists, or n otherwise. + * + * ev is an evaluator which determines where n is placed in the trie + * index is the depth of this node + * ntotal is the maximal depth of the trie + * forceKeep is whether we wish to force that n is chosen as a representative + */ + Node add(Node n, + LazyTrieEvaluator* ev, + unsigned index, + unsigned ntotal, + bool forceKeep); +}; + +/** SygusSampler + * + * This class can be used to test whether two expressions are equivalent + * by random sampling. We use this class for the following options: + * + * sygus-rr-synth: synthesize candidate rewrite rules by finding two terms + * t1 and t2 do not rewrite to the same term, but are identical when considering + * a set of sample points, and + * + * sygus-rr-verify: detect unsound rewrite rules by finding two terms t1 and + * t2 that rewrite to the same term, but not identical when considering a set + * of sample points. + * + * To use this class: + * (1) Call initialize( tds, f, nsamples) where f is sygus datatype term. + * (2) For terms n1....nm enumerated that correspond to builtin analog of sygus + * term f, we call registerTerm( n1 )....registerTerm( nm ). It may be the case + * that registerTerm( ni ) returns nj for some j < i. In this case, we have that + * ni and nj are equivalent under the sample points in this class. + * + * For example, say the grammar for f is: + * A = 0 | 1 | x | y | A+A | ite( B, A, A ) + * B = A <= A + * If we call intialize( tds, f, 5 ), this class will generate 5 random sample + * points for (x,y), say (0,0), (1,1), (0,1), (1,0), (2,2). The return values + * of successive calls to registerTerm are listed below. + * registerTerm( 0 ) -> 0 + * registerTerm( x ) -> x + * registerTerm( x+y ) -> x+y + * registerTerm( y+x ) -> x+y + * registerTerm( x+ite(x <= 1+1, 0, y ) ) -> x + * Notice that the number of sample points can be configured for the above + * options using sygus-samples=N. + */ +class SygusSampler : public LazyTrieEvaluator +{ + public: + SygusSampler(); + virtual ~SygusSampler() {} + /** initialize + * + * tds : reference to a sygus database, + * f : a term of some SyGuS datatype type whose (builtin) values we will be + * testing, + * nsamples : number of sample points this class will test. + */ + void initialize(TermDbSygus* tds, Node f, unsigned nsamples); + /** register term n with this sampler database + * + * forceKeep is whether we wish to force that n is chosen as a representative + * value in the trie. + */ + Node registerTerm(Node n, bool forceKeep = false); + /** is contiguous + * + * This returns whether n's free variables (terms occurring in the range of + * d_type_vars) are a prefix of the list of variables in d_type_vars for each + * type. For instance, if d_type_vars[Int] = { x, y }, then 0, x, x+y, y+x are + * contiguous but y is not. This is useful for excluding terms from + * consideration that are alpha-equivalent to others. + */ + bool isContiguous(Node n); + /** is ordered + * + * This returns whether n's free variables are in order with respect to + * variables in d_type_vars for each type. For instance, if + * d_type_vars[Int] = { x, y }, then 0, x, x+y are ordered but y and y+x + * are not. + */ + bool isOrdered(Node n); + /** contains free variables + * + * Returns true if all free variables of a are contained in b. Free variables + * are those that occur in the range d_type_vars. + */ + bool containsFreeVariables(Node a, Node b); + /** evaluate n on sample point index */ + Node evaluate(Node n, unsigned index); + + private: + /** sygus term database of d_qe */ + TermDbSygus* d_tds; + /** samples */ + std::vector > d_samples; + /** type of nodes we will be registering with this class */ + TypeNode d_ftn; + /** type variables + * + * For each type, a list of variables in the grammar we are considering, for + * that type. These typically correspond to the arguments of the + * function-to-synthesize whose grammar we are considering. + */ + std::map > d_type_vars; + /** + * A map all variables in the grammar we are considering to their index in + * d_type_vars. + */ + std::map d_var_index; + /** constants + * + * For each type, a list of constants in the grammar we are considering, for + * that type. + */ + std::map > d_type_consts; + /** the lazy trie */ + LazyTrie d_trie; + /** is this sampler valid? + * + * A sampler can be invalid if sample points cannot be generated for a type + * of an argument to function f. + */ + bool d_is_valid; + /** + * Compute the variables from the domain of d_var_index that occur in n, + * store these in the vector fvs. + */ + void computeFreeVariables(Node n, std::vector& fvs); + /** get random value for a type + * + * Returns a random value for the given type based on the random number + * generator. Currently, supported types: + * + * Bool, Bitvector : returns a random value in the range of that type. + * Int, String : returns a random string of values in (base 10) of random + * 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); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */