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 \
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
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
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<Node, quantifiers::SygusSampler>::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];
#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 {
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<Node, Node> 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<Node, quantifiers::SygusSampler> d_sampler;
Node d_null;
void assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas );
// register search term
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() );
}
Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
}
out << ")" << std::endl;
+
+ if (status != 0 && options::sygusRewSynth())
+ {
+ TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+ std::map<Node, SygusSampler>::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;
+ }
+ }
+ }
}
}
}
#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 {
/** 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<Node, SygusSampler> d_sampler;
};
} /* namespace CVC4::theory::quantifiers */
--- /dev/null
+/********************* */
+/*! \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<Node> 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<DatatypeType>(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<TypeNode> 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<Node> 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<Node> fvs;
+ computeFreeVariables(n, fvs);
+ // compute contiguous condition
+ for (const std::pair<const TypeNode, std::vector<Node> >& 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<Node>& fvs)
+{
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> 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<TypeNode, std::vector<Node> > fvs;
+
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> 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<Node, unsigned>::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<Node> fvs;
+ computeFreeVariables(a, fvs);
+
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> 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<unsigned> 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<Node> 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>();
+ Rational rr = s.getConst<Rational>();
+ if (rr.sgn() == 0)
+ {
+ return s;
+ }
+ else
+ {
+ return nm->mkConst(sr / rr);
+ }
+ }
+ }
+ return Node::null();
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \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 <map>
+#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<Node, LazyTrie> 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<std::vector<Node> > 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<TypeNode, std::vector<Node> > d_type_vars;
+ /**
+ * A map all variables in the grammar we are considering to their index in
+ * d_type_vars.
+ */
+ std::map<Node, unsigned> d_var_index;
+ /** constants
+ *
+ * For each type, a list of constants in the grammar we are considering, for
+ * that type.
+ */
+ std::map<TypeNode, std::vector<Node> > 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<Node>& 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 */
projects / cvc5.git / commitdiff