59 const enumeratorst::const_iterator &it_enumerators,
61 const partitiont::const_iterator &it_partition)
const
64 std::distance(it_enumerators, enumerators.end()) ==
65 std::distance(it_partition, partition.end()),
66 "Partition should have the same size as enumerators.");
68 std::set<expr_listt> result;
70 if(std::next(it_enumerators) == enumerators.end())
74 for(
const auto &e : enumerators.back()->enumerate(*it_partition))
86 std::next(it_enumerators),
88 std::next(it_partition)))
90 for(
const auto &elem : (*it_enumerators)->enumerate(*it_partition))
93 new_tuple.emplace_front(elem);
94 result.insert(new_tuple);
101 std::list<partitiont>
104 std::list<partitiont> result;
110 std::vector<std::size_t> cuts;
118 cuts.emplace_back(0);
119 cuts.emplace_back(n - k + 1);
120 for(std::size_t i = 0; i < k - 1; i++)
122 cuts.emplace_back(n - k + 2 + i);
132 for(std::size_t i = 1; i < k + 1; i++)
134 new_partition.emplace_back(cuts[i] - cuts[i - 1]);
152 std::size_t rightmost_to_move = 0;
153 for(std::size_t i = 1; i < k; i++)
155 if(cuts[i] - cuts[i - 1] > 1)
157 rightmost_to_move = i;
165 cuts[rightmost_to_move] = cuts[rightmost_to_move] - 1;
168 if(rightmost_to_move == 0)
177 std::size_t accum = 1;
178 for(std::size_t i = k - 1; i > rightmost_to_move; i--)
184 result.emplace_back(new_partition);
192 const std::size_t length =
sizeof(std::size_t) * CHAR_BIT;
193 std::vector<std::size_t> result;
196 std::size_t curr_pos = length;
201 result.insert(result.begin(), curr_pos);
219 const std::vector<std::size_t> ones_pos =
get_ones_pos(v);
221 INVARIANT(ones_pos.size() >= 1,
"There should be at least one bit set in v");
225 for(std::size_t i = 1; i < ones_pos.size(); i++)
227 result.emplace_back(ones_pos[i] - ones_pos[i - 1]);
229 result.emplace_back(n - ones_pos[ones_pos.size() - 1]);
236 const std::size_t k)
const
243 const std::size_t length =
sizeof(std::size_t) * CHAR_BIT;
262 for(
size_t i = 0; i < k - 1; i++)
269 v = v << (length - n);
270 end = end << (length - k);
272 std::list<partitiont> result;
280 std::size_t t = (v | (v - 1)) + 1;
281 v = t | ((((t & -t) / (v & -v)) >> 1) - 1);
290 return op_id == ID_equal ||
op_id == ID_plus ||
op_id == ID_notequal ||
299 std::stringstream left, right;
300 left <<
format(exprs.front());
301 right <<
format(exprs.back());
320 static std::pair<const exprt, const exprt>
326 (lhs.
type().
id() == ID_unsignedbv || lhs.
type().
id() == ID_signedbv) &&
327 (rhs.
type().
id() == ID_unsignedbv || rhs.
type().
id() == ID_signedbv))
329 const auto &lhs_type = type_try_dynamic_cast<bitvector_typet>(lhs.
type());
330 const auto &rhs_type = type_try_dynamic_cast<bitvector_typet>(rhs.
type());
333 if(lhs_type->get_width() == rhs_type->get_width())
335 if((lhs.
type().
id() == ID_unsignedbv || rhs.
type().
id() == ID_unsignedbv))
337 return std::pair<const exprt, const exprt>(
345 return std::pair<const exprt, const exprt>(
354 if(lhs_type->get_width() > rhs_type->get_width())
356 return std::pair<const exprt, const exprt>(
361 return std::pair<const exprt, const exprt>(
368 return std::pair<const exprt, const exprt>(lhs, rhs);
376 "number of arguments should be 2: " +
integer2string(exprs.size()));
381 if(
op_id == ID_equal)
382 return equal_exprt(operands.first, operands.second);
383 if(
op_id == ID_notequal)
394 return and_exprt(exprs.front(), exprs.back());
396 return or_exprt(exprs.front(), exprs.back());
398 return plus_exprt(operands.first, operands.second);
399 if(
op_id == ID_minus)
400 return minus_exprt(operands.first, operands.second);
410 for(
const auto &e : enumerator->enumerate(size))
424 return actual_enumerator.
enumerate(size);
432 INVARIANT(ret.second,
"Duplicated non-terminals");
436 const std::string &
id,
441 ret.second,
"Cannot attach enumerators to a non-existing nonterminal.");
std::list< exprt > expr_listt
Pre-defined bitvector types.
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
A base class for binary expressions.
const bool is_exchangeable
bool is_equivalence_class_representation(const expr_listt &exprs) const override
Determine whether a tuple of expressions is the representation of some equivalence class.
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.
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.
Base class for all expressions.
typet & type()
Return the type of the expression.
Binary greater than operator expression.
Binary greater than or equal operator expression.
const irep_idt & id() const
expr_sett enumerate(const std::size_t size) const override
Enumerate expressions in the set of leaf_exprs.
const expr_sett leaf_exprs
Binary less than operator expression.
Binary less than or equal operator expression.
expr_sett enumerate(const std::size_t size) const override
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.
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.
The plus expression Associativity is not specified.
Placeholders for actual enumerators, which represent nonterminals.
const enumerator_factoryt & factory
expr_sett enumerate(const std::size_t size) const override
const std::string identifier
Fixed-width bit-vector with two's complement interpretation.
static exprt conditional_cast(const exprt &expr, const typet &type)
Fixed-width bit-vector with unsigned binary interpretation.
std::unordered_set< exprt, irep_hash > expr_sett
std::list< partitiont > get_partitions_long(const std::size_t n, const std::size_t k)
static std::pair< const exprt, const exprt > widen_bitvector(const exprt &lhs, const exprt &rhs)
partitiont from_bits_to_partition(std::size_t v, std::size_t n)
Construct partition of n elements from a bit vector v.
std::vector< std::size_t > get_ones_pos(std::size_t v)
Compute all positions of ones in the bit vector v (1-indexed).
std::list< const enumerator_baset * > enumeratorst
std::list< std::size_t > partitiont
const std::string integer2string(const mp_integer &n, unsigned base)
exprt simplify_expr(exprt src, const namespacet &ns)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.