cprover
Loading...
Searching...
No Matches
expr_enumerator.h
Go to the documentation of this file.
1/*******************************************************************\
2Module: Enumerator Interface
3Author: Qinheping Hu
4\*******************************************************************/
5
8
9#ifndef CPROVER_GOTO_SYNTHESIZER_EXPR_ENUMERATOR_H
10#define CPROVER_GOTO_SYNTHESIZER_EXPR_ENUMERATOR_H
11
12#include <util/expr.h>
13
14#include <map>
15#include <set>
16
17typedef std::list<exprt> expr_listt;
18typedef std::set<exprt> expr_sett;
19typedef std::list<std::size_t> partitiont;
20
21/*
22 This is the interface of grammar-based enumerators. Users can specify tree
23 grammars, and enumerate expressions derived by the grammars using these
24 enumerators. A tree grammar consists of a finite set of nonterminals and
25 a finite set of productions of the form A -> t where A is some nonterminal,
26 and t is some tree composed from nonterminal symbols and constants.
27
28 In the level of productions, we introduce three classes of enumerators:
29 1. `leaf_enumeratort` enumerates `exprt`-typed expressions. It is used
30 to enumerate leaves of trees derived from the tree grammar.
31 Example:
32 a `leaf_enumeratort` with `leaf_exprs` {0} enumerates expressions derived
33 from the production
34 * -> 0.
35 2. `non_leaf_enumeratort` enumerates expressions recursively built from
36 sub-trees---trees enumerated by sub-enumerators.
37 Example:
38 a `non_leaf_enumeratort` with `sub_enumerators` {A, B} and `op` +
39 enumerates expressions derived from the production
40 * -> A + B.
41 3. `alternatives_enumeratort` enumerates expressions that can be enumerated
42 by any of its `sub_enumerators`
43 Example:
44 a `alternatives_enumeratort` with `sub_enumerators` the enumerators in
45 the Example 1 and 2 enumerates expressions derived from the production
46 * -> 0 | A + B.
47
48 One missing part in the above enumerators is the left-hand-side of
49 productions, it should be a nonterminal symbol associated with a finite set
50 of productions. So we introduce `recursive_enumerator_placeholdert` for
51 nonterminal symbols, and `recursive_enumerator_factoryt` for grammars.
52 Each placeholder has an identifier, and corresponds to a nonterminal in the
53 grammar. Each factory maintains a map from identifier to placeholder, and a
54 map from identifiers to placeholder's productions.
55
56 As an example, to specify a grammar G with two nonterminals A and B, and two
57 productions
58 A -> A + B | 0
59 B -> 1.
60 We need to construct a factory with two placeholders ph_A and ph_b whose
61 identifiers are "A" and "B", respectively.
62 The factory should contain a set {ph_A, ph_B}, and a map
63 {("A", E_A), ("B", E_B)}
64 where the alternatives enumerator E_A is for the production
65 -> A + B | 0
66 and the alternatives enumerator E_B is for the production
67 -> 1 | 2.
68 Note that E_A contains a binary non-leaf enumerator E_plus with
69 sub-enumerators (ph_A, ph_B) and operator `ID_plus`, and a leaf enumerator
70 E_0 with `leaf_exprs` {0}. E_B contains a leaf enumerator E_1 with
71 `leaf_exprs` {1} and a leaf enumerator E_2 with `leaf_exprs` {2}.
72
73 Let [E, n] to be the result of enumeration E.enumerate(n)---expressions with
74 size n enumerated by the enumerator E. To enumerate expressions with size 5
75 in L(A) in the above example, the algorithm works as follow.
76 [ph_A, 5] = [E_A, 5] looking up "A" from `productions_map` of ph_A.factory
77 = [E_plus, 5] \/ [E_0, 5]
78 = [E_plus, 5] \/ {} = [E_plus, 5]
79 [E_0, 5] = {} as leaf enumerator enumerates only expressions with size 1.
80
81 To enumerate [E_plus, 5], we first enumerate expressions from two
82 sub-enumerators E_A and E_B of E_plus, and then combine them using the
83 operator ID_plus. In E_plus, the size of the operator ID_plus is 1, so the
84 sum of sizes of two sub-expressions should be 4. There are three way to
85 partition 4: (3, 1), (2, 2), and (1, 3). So
86 [E_plus, 5] = [E_A, 3]*[E_B, 1] \/ [E_A, 2]*[E_B, 2] \/ [E_A, 1]*[E_B, 3]
87 Note that E_B contain only leaf expressions. Therefore [E_B, 1] = {1, 2}, and
88 [E_B, n] = {} for all n > 1. The * operator is the Cartesian products
89 instantiated with plus operator.
90 [E_plus, 5] = [E_A, 3]*[E_B, 1] \/ [E_A, 2]*[E_B, 2] \/ [E_A, 1]*[E_B, 3]
91 = [E_A, 3]*{1, 2} \/ [E_A, 2]*{} \/ [E_A, 2]*{}
92 = [E_A, 3]*{1, 2} \/ {} \/ {}
93 = [E_A, 3]*{1, 2}
94 = ([E_A, 1]*[E_B, 1])*{1, 2}
95 = ({0}*{1,2})*{1, 2}
96 = {0+1, 0+2}*{1, 2}
97 = {(0+1)+1, (0+2)+1, (0+1)+2, (0+2)+2}
98 So, expressions in L(A) are {(0+1)+1, (0+2)+1, (0+1)+2, (0+2)+2}.
99
100 Why Cartesian products.
101 For a grammar,
102 A -> B + B
103 B -> 1 | 2,
104 the expressions enumerated by B are {1, 2}. To enumerate expressions in L(A).
105 We need to combine sub-expressions {1, 2} into a plus-expression.
106 {1, 2} + {1, 2}
107 Because each nonterminal B can yield either 1 and 2 independently, we have to
108 combine sub-expressions as their cartesian products.
109 {1 + 1, 1 + 2, 2 + 1, 2 + 2}.
110*/
111
114{
115public:
116 explicit enumerator_baset(const namespacet &ns) : ns(ns)
117 {
118 }
119
120 virtual expr_sett enumerate(const std::size_t size) const = 0;
121
122 enumerator_baset(const enumerator_baset &other) = delete;
124
125 virtual ~enumerator_baset() = default;
126
127protected:
129};
130
131typedef std::list<const enumerator_baset *> enumeratorst;
132
136{
137public:
142
144 expr_sett enumerate(const std::size_t size) const override;
145
146protected:
148};
149
154{
155public:
163 const enumeratorst &enumerators,
164 const std::function<bool(const partitiont &)> partition_check,
165 const namespacet &ns)
167 arity(enumerators.size()),
168 sub_enumerators(enumerators),
169 is_good_partition(partition_check)
170 {
171 INVARIANT(
172 arity > 1, "arity should be greater than one for non_leaf_enumeratort");
173 }
174
176 non_leaf_enumeratort(const enumeratorst &enumerators, const namespacet &ns)
178 enumerators,
179 [](const partitiont &) { return true; },
180 ns)
181 {
182 }
183
184 expr_sett enumerate(const std::size_t size) const override;
185
188 std::set<expr_listt> cartesian_product_of_enumerators(
189 const enumeratorst &enumerators,
190 const enumeratorst::const_iterator &it,
191 const partitiont &partition,
192 const partitiont::const_iterator &it_partition) const;
193
196 std::list<partitiont>
197 get_partitions(const std::size_t n, const std::size_t k) const;
198
201 {
202 return true;
203 }
204
205protected:
207 virtual exprt instantiate(const expr_listt &exprs) const = 0;
208
209 const std::size_t arity;
211 const std::function<bool(const partitiont &)> is_good_partition;
212};
213
216{
217public:
219 const irep_idt &op,
220 const enumerator_baset &enumerator_1,
221 const enumerator_baset &enumerator_2,
222 const std::function<bool(const partitiont &)> partition_check,
223 const bool exchangeable,
224 const namespacet &ns)
225 : non_leaf_enumeratort({&enumerator_1, &enumerator_2}, partition_check, ns),
226 is_exchangeable(exchangeable),
227 op_id(op)
228 {
229 }
230
232 const irep_idt &op,
233 const enumerator_baset &enumerator_1,
234 const enumerator_baset &enumerator_2,
235 const std::function<bool(const partitiont &)> partition_check,
236 const namespacet &ns)
238 op,
239 enumerator_1,
240 enumerator_2,
241 partition_check,
242 &enumerator_1 == &enumerator_2,
243 ns)
244 {
245 }
246
248 const irep_idt &op,
249 const enumerator_baset &enumerator_1,
250 const enumerator_baset &enumerator_2,
251 const namespacet &ns)
253 op,
254 enumerator_1,
255 enumerator_2,
256 [](const partitiont &) { return true; },
257 ns)
258 {
259 }
260
261 bool is_commutative(const irep_idt &op) const;
262
265 bool
266 is_equivalence_class_representation(const expr_listt &exprs) const override;
267
268protected:
269 exprt instantiate(const expr_listt &exprs) const override;
270
271 // Whether the two sub-enumerators are exchangeable---they enumerate the same
272 // set of expressions.
273 const bool is_exchangeable = false;
274
276};
277
283{
284public:
286 const enumeratorst &enumerators,
287 const namespacet &ns)
288 : enumerator_baset(ns), sub_enumerators(enumerators)
289 {
290 }
291
292 expr_sett enumerate(const std::size_t size) const override;
293
294protected:
296};
297
299
302{
303public:
305 {
306 }
307
309 void add_placeholder(const recursive_enumerator_placeholdert &placeholder);
310
312 void
313 attach_productions(const std::string &id, const enumeratorst &enumerators);
314
319 std::map<std::string, const enumeratorst> productions_map;
320
321protected:
323
325 std::set<std::string> nonterminal_set;
326};
327
335{
336public:
343 const std::string &id,
344 const namespacet &ns)
346 {
348 }
349
350 expr_sett enumerate(const std::size_t size) const override;
351
352 const std::string identifier;
353
354protected:
356};
357
358#endif // CPROVER_GOTO_SYNTHESIZER_EXPR_ENUMERATOR_H
std::list< exprt > expr_listt
Enumerators that enumerates expressions in the union of enumerated expressions of sub-enumerators.
const enumeratorst sub_enumerators
expr_sett enumerate(const std::size_t size) const override
alternatives_enumeratort(const enumeratorst &enumerators, const namespacet &ns)
Enumerator that enumerates binary functional expressions.
binary_functional_enumeratort(const irep_idt &op, const enumerator_baset &enumerator_1, const enumerator_baset &enumerator_2, const std::function< bool(const partitiont &)> partition_check, const bool exchangeable, const namespacet &ns)
bool is_equivalence_class_representation(const expr_listt &exprs) const override
Determine whether a tuple of expressions is the representation of some equivalence class.
binary_functional_enumeratort(const irep_idt &op, const enumerator_baset &enumerator_1, const enumerator_baset &enumerator_2, const namespacet &ns)
binary_functional_enumeratort(const irep_idt &op, const enumerator_baset &enumerator_1, const enumerator_baset &enumerator_2, const std::function< bool(const partitiont &)> partition_check, const namespacet &ns)
exprt instantiate(const expr_listt &exprs) const override
Combine a list of sub-expressions to construct the top-level expression.
bool is_commutative(const irep_idt &op) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
A base class for expression enumerators.
const namespacet & ns
virtual expr_sett enumerate(const std::size_t size) const =0
enumerator_baset(const namespacet &ns)
enumerator_baset(const enumerator_baset &other)=delete
virtual ~enumerator_baset()=default
enumerator_baset & operator=(const enumerator_baset &other)=delete
Factory for enumerator that can be used to represent a tree grammar.
enumerator_factoryt(const namespacet &ns)
void add_placeholder(const recursive_enumerator_placeholdert &placeholder)
Add a new placeholder/nonterminal to the grammar.
std::set< std::string > nonterminal_set
Set of nonterminals in the grammar.
std::map< std::string, const enumeratorst > productions_map
Map from names of nonterminals to rhs of productions with lhs being them.
void attach_productions(const std::string &id, const enumeratorst &enumerators)
Attach enumerators to the placeholder with id.
const namespacet & ns
Base class for all expressions.
Definition expr.h:56
Enumerator that enumerates leaf expressions from a given list.
expr_sett enumerate(const std::size_t size) const override
Enumerate expressions in the set of leaf_exprs.
leaf_enumeratort(const expr_sett &leaf_exprs, const namespacet &ns)
const expr_sett leaf_exprs
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Non-leaf enumerator enumerates expressions of form f(a_1, a_2, ..., a_n) where a_i's are sub-expressi...
expr_sett enumerate(const std::size_t size) const override
non_leaf_enumeratort(const enumeratorst &enumerators, const namespacet &ns)
As default: no optimization. partition_check Accept all partitions.
const std::size_t arity
std::list< partitiont > get_partitions(const std::size_t n, const std::size_t k) const
Enumerate all partitions of n into k components.
virtual exprt instantiate(const expr_listt &exprs) const =0
Combine a list of sub-expressions to construct the top-level expression.
non_leaf_enumeratort(const enumeratorst &enumerators, const std::function< bool(const partitiont &)> partition_check, const namespacet &ns)
const std::function< bool(const partitiont &)> is_good_partition
const enumeratorst sub_enumerators
std::set< expr_listt > cartesian_product_of_enumerators(const enumeratorst &enumerators, const enumeratorst::const_iterator &it, const partitiont &partition, const partitiont::const_iterator &it_partition) const
Given a list enumerators of enumerators, return the Cartesian product of expressions enumerated by ea...
virtual bool is_equivalence_class_representation(const expr_listt &es) const
As default, keep all expression tuples.
Placeholders for actual enumerators, which represent nonterminals.
const enumerator_factoryt & factory
expr_sett enumerate(const std::size_t size) const override
recursive_enumerator_placeholdert(enumerator_factoryt &factory, const std::string &id, const namespacet &ns)
std::unordered_set< exprt, irep_hash > expr_sett
std::list< exprt > expr_listt
std::set< exprt > expr_sett
std::list< const enumerator_baset * > enumeratorst
std::list< std::size_t > partitiont
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423