diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-01 12:13:54 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-01 12:13:54 -0600 |
commit | dbd1797f64216ba9eb598579de27cc45814e1db4 (patch) | |
tree | da47015c59c728ada2b7034900267609a00ecb12 /src/theory/quantifiers/sygus_sampler.h | |
parent | 2e4eba43ffa4dd938b7e1153cc42216a42e8ce04 (diff) |
Use sygus to synthesize/verify rewrite rules (#1547)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 237 |
1 files changed, 237 insertions, 0 deletions
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 <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 */ |