1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Mathias Preiner, Fabian Wolff
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
19 #define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
22 #include "theory/evaluator.h"
23 #include "theory/quantifiers/lazy_trie.h"
24 #include "theory/quantifiers/sygus/term_database_sygus.h"
25 #include "theory/quantifiers/term_enumeration.h"
29 namespace quantifiers
{
33 * This class can be used to test whether two expressions are equivalent
34 * by random sampling. We use this class for the following options:
36 * sygus-rr-synth: synthesize candidate rewrite rules by finding two terms
37 * t1 and t2 do not rewrite to the same term, but are identical when considering
38 * a set of sample points, and
40 * sygus-rr-verify: detect unsound rewrite rules by finding two terms t1 and
41 * t2 that rewrite to the same term, but not identical when considering a set
45 * (1) Call initialize( tds, f, nsamples) where f is sygus datatype term.
46 * (2) For terms n1....nm enumerated that correspond to builtin analog of sygus
47 * term f, we call registerTerm( n1 )....registerTerm( nm ). It may be the case
48 * that registerTerm( ni ) returns nj for some j < i. In this case, we have that
49 * ni and nj are equivalent under the sample points in this class.
51 * For example, say the grammar for f is:
52 * A = 0 | 1 | x | y | A+A | ite( B, A, A )
54 * If we call initialize( tds, f, 5 ), this class will generate 5 random sample
55 * points for (x,y), say (0,0), (1,1), (0,1), (1,0), (2,2). The return values
56 * of successive calls to registerTerm are listed below.
57 * registerTerm( 0 ) -> 0
58 * registerTerm( x ) -> x
59 * registerTerm( x+y ) -> x+y
60 * registerTerm( y+x ) -> x+y
61 * registerTerm( x+ite(x <= 1+1, 0, y ) ) -> x
62 * Notice that the number of sample points can be configured for the above
63 * options using sygus-samples=N.
65 class SygusSampler
: public LazyTrieEvaluator
69 ~SygusSampler() override
{}
73 * tn : the return type of terms we will be testing with this class,
74 * vars : the variables we are testing substitutions for,
75 * nsamples : number of sample points this class will test,
76 * unique_type_ids : if this is set to true, then we consider each variable
77 * in vars to have a unique "type id". A type id is a finer-grained notion of
78 * type that is used to determine when a rewrite rule is redundant.
80 virtual void initialize(TypeNode tn
,
81 const std::vector
<Node
>& vars
,
83 bool unique_type_ids
= false);
86 * qe : pointer to quantifiers engine,
87 * f : a term of some SyGuS datatype type whose values we will be
88 * testing under the free variables in the grammar of f,
89 * nsamples : number of sample points this class will test,
90 * useSygusType : whether we will register terms with this sampler that have
91 * the same type as f. If this flag is false, then we will be registering
92 * terms of the analog of the type of f, that is, the builtin type that
93 * f's type encodes in the deep embedding.
95 virtual void initializeSygus(TermDbSygus
* tds
,
99 /** register term n with this sampler database
101 * forceKeep is whether we wish to force that n is chosen as a representative
104 virtual Node
registerTerm(Node n
, bool forceKeep
= false);
105 /** get number of sample points */
106 unsigned getNumSamplePoints() const { return d_samples
.size(); }
107 /** get variables, adds d_vars to vars */
108 void getVariables(std::vector
<Node
>& vars
) const;
111 * Appends sample point #index to the vector pt, d_vars to vars.
113 void getSamplePoint(unsigned index
,
114 std::vector
<Node
>& pt
);
115 /** Add pt to the set of sample points considered by this sampler */
116 void addSamplePoint(std::vector
<Node
>& pt
);
117 /** evaluate n on sample point index */
118 Node
evaluate(Node n
, unsigned index
) override
;
120 * Compute the variables from the domain of d_var_index that occur in n,
121 * store these in the vector fvs.
123 void computeFreeVariables(Node n
, std::vector
<Node
>& fvs
);
125 * Returns the index of a sample point such that the evaluation of a and b
126 * diverge, or -1 if no such sample point exists.
128 int getDiffSamplePointIndex(Node a
, Node b
);
130 //--------------------------queries about terms
133 * This returns whether n's free variables (terms occurring in the range of
134 * d_type_vars) are a prefix of the list of variables in d_type_vars for each
135 * type id. For instance, if d_type_vars[id] = { x, y } for some id, then
136 * 0, x, x+y, y+x are contiguous but y is not. This is useful for excluding
137 * terms from consideration that are alpha-equivalent to others.
139 bool isContiguous(Node n
);
142 * This returns whether n's free variables are in order with respect to
143 * variables in d_type_vars for each type. For instance, if
144 * d_type_vars[id] = { x, y } for some id, then 0, x, x+y are ordered but
147 bool isOrdered(Node n
);
150 * This returns whether n contains at most one occurrence of each free
151 * variable. For example, x, x+y are linear, but x+x, (x-y)+y, (x+0)+(x+0) are
154 bool isLinear(Node n
);
157 * This returns false if !isOrdered(n) and checkOrder is true or !isLinear(n)
158 * if checkLinear is true, or false otherwise.
160 bool checkVariables(Node n
, bool checkOrder
, bool checkLinear
);
161 /** contains free variables
163 * Returns true if the free variables of b are a subset of those in a, where
164 * we require a strict subset if strict is true. Free variables are those that
165 * occur in the range d_type_vars.
167 bool containsFreeVariables(Node a
, Node b
, bool strict
= false);
168 //--------------------------end queries about terms
171 * Check whether bv and bvr are equivalent on all sample points, print
172 * an error if not. Used with --sygus-rr-verify.
174 * @param bv The original term
175 * @param bvr The rewritten form of bvr
176 * @param out The output stream to write if the rewrite was unsound.
178 void checkEquivalent(Node bv
, Node bvr
, std::ostream
& out
);
181 /** sygus term database of d_qe */
183 /** term enumerator object (used for random sampling) */
184 TermEnumeration d_tenum
;
186 std::vector
<std::vector
<Node
> > d_samples
;
187 /** evaluator class */
189 /** data structure to check duplication of sample points */
193 /** add pt to this trie, returns true if pt is not a duplicate. */
194 bool add(std::vector
<Node
>& pt
);
197 /** the children of this node */
198 std::map
<Node
, PtTrie
> d_children
;
200 /** a trie for samples */
201 PtTrie d_samples_trie
;
202 /** the sygus type for this sampler (if applicable). */
204 /** whether we are registering terms of sygus types with this sampler */
205 bool d_use_sygus_type
;
207 * For each (sygus) type, a map from builtin terms to the sygus term they
210 std::map
<TypeNode
, std::map
<Node
, Node
> > d_builtin_to_sygus
;
211 /** all variables we are sampling values for */
212 std::vector
<Node
> d_vars
;
215 * We group variables according to "type ids". Two variables have the same
216 * type id if they have indistinguishable status according to this sampler.
217 * This is a finer-grained grouping than types. For example, two variables
218 * of the same type may have different type ids if they occur as constructors
219 * of a different set of sygus types in the grammar we are considering.
220 * For instance, we assign x and y different type ids in this grammar:
224 * Type ids are computed for each variable in d_vars during initialize(...).
226 * For each type id, a list of variables in the grammar we are considering,
227 * for that type. These typically correspond to the arguments of the
228 * function-to-synthesize whose grammar we are considering.
230 std::map
<unsigned, std::vector
<Node
> > d_type_vars
;
232 * A map all variables in the grammar we are considering to their index in
235 std::map
<Node
, unsigned> d_var_index
;
236 /** Map from variables to the id (the domain of d_type_vars). */
237 std::map
<Node
, unsigned> d_type_ids
;
240 * For each type, a list of constants in the grammar we are considering, for
243 std::map
<TypeNode
, std::vector
<Node
> > d_type_consts
;
244 /** a lazy trie for each type
246 * This stores the evaluation of all terms registered to this class.
248 * Notice if we are registering sygus terms with this class, then terms
249 * are grouped into this trie according to their sygus type, and not their
250 * builtin type. For example, for grammar:
252 * B -> x | 0 | 1 | B+B
253 * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class,
254 * then x+0 is registered to d_trie[B] and x is registered to d_trie[A],
255 * and no rewrite rule is reported. The reason for this is that otherwise
256 * we would end up reporting many useless rewrites since the same builtin
257 * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()).
259 std::map
<TypeNode
, LazyTrie
> d_trie
;
260 /** is this sampler valid?
262 * A sampler can be invalid if sample points cannot be generated for a type
263 * of an argument to function f.
266 /** initialize samples
268 * Adds nsamples sample points to d_samples.
270 void initializeSamples(unsigned nsamples
);
271 /** get random value for a type
273 * Returns a random value for the given type based on the random number
274 * generator. Currently, supported types:
276 * Bool, Bitvector : returns a random value in the range of that type.
277 * Int, String : returns a random string of values in (base 10) of random
278 * length, currently by a repeated coin flip.
279 * Real : returns the division of two random integers, where the denominator
280 * is omitted if it is zero.
282 Node
getRandomValue(TypeNode tn
);
283 /** get sygus random value
285 * Returns a random value based on the sygus type tn. The return value is
286 * a constant in the analog type of tn. This function chooses either to
287 * return a random value, or otherwise will construct a constant based on
288 * a random constructor of tn whose builtin operator is not a variable.
290 * rchance: the chance that the call to this function will be forbidden
291 * from making recursive calls and instead must return a value based on
292 * a nullary constructor of tn or based on getRandomValue above.
293 * rinc: the percentage to increment rchance on recursive calls.
295 * For example, consider the grammar:
296 * A -> x | y | 0 | 1 | +( A, A ) | ite( B, A, A )
298 * If we call this function on A and rchance is 0.0, there are five evenly
299 * chosen possibilities, either we return a random value via getRandomValue
300 * above, or we choose one of the four non-variable constructors of A.
301 * Say we choose ite, then we recursively call this function for
302 * B, A, and A, which return constants c1, c2, and c3. Then, this function
303 * returns the rewritten form of ite( c1, c2, c3 ).
304 * If on the other hand, rchance was 0.5 and rand() < 0.5. Then, we force
305 * this call to terminate by either selecting a random value via
306 * getRandomValue, 0 or 1.
308 Node
getSygusRandomValue(TypeNode tn
,
312 /** map from sygus types to non-variable constructors */
313 std::map
<TypeNode
, std::vector
<unsigned> > d_rvalue_cindices
;
314 /** map from sygus types to non-variable nullary constructors */
315 std::map
<TypeNode
, std::vector
<unsigned> > d_rvalue_null_cindices
;
316 /** the random string alphabet */
317 std::vector
<unsigned> d_rstring_alphabet
;
318 /** map from variables to sygus types that include them */
319 std::map
<Node
, std::vector
<TypeNode
> > d_var_sygus_types
;
320 /** map from constants to sygus types that include them */
321 std::map
<Node
, std::vector
<TypeNode
> > d_const_sygus_types
;
322 /** register sygus type, initializes the above two data structures */
323 void registerSygusType(TypeNode tn
);
326 } // namespace quantifiers
327 } // namespace theory
330 #endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */