expr_enumerator.cpp File Reference
#include "expr_enumerator.h"#include <util/bitvector_types.h>#include <util/format_expr.h>#include <util/simplify_expr.h>#include <util/std_expr.h>#include <climits>
Include dependency graph for expr_enumerator.cpp:Go to the source code of this file.
Functions | |
| std::list< partitiont > | get_partitions_long (const std::size_t n, const std::size_t k) |
| std::vector< std::size_t > | get_ones_pos (std::size_t v) |
Compute all positions of ones in the bit vector v (1-indexed). More... | |
| partitiont | from_bits_to_partition (std::size_t v, std::size_t n) |
Construct partition of n elements from a bit vector v. More... | |
| static std::pair< const exprt, const exprt > | widen_bitvector (const exprt &lhs, const exprt &rhs) |
Function Documentation
◆ from_bits_to_partition()
| partitiont from_bits_to_partition | ( | std::size_t | v, |
| std::size_t | n | ||
| ) |
Construct partition of n elements from a bit vector v.
For a bit vector with ones at positions (computed by get_ones_pos) (ones[0], ones[1], ..., ones[k-2]), the corresponding partition is (ones[0], ones[1]-ones[0], ..., ones[k-2]-ones[k-3], n-ones[k-2]).
Definition at line 217 of file expr_enumerator.cpp.
◆ get_ones_pos()
| std::vector<std::size_t> get_ones_pos | ( | std::size_t | v | ) |
Compute all positions of ones in the bit vector v (1-indexed).
Definition at line 190 of file expr_enumerator.cpp.
◆ get_partitions_long()
| std::list<partitiont> get_partitions_long | ( | const std::size_t | n, |
| const std::size_t | k | ||
| ) |
Definition at line 102 of file expr_enumerator.cpp.
