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).
partitiont	from_bits_to_partition (std::size_t v, std::size_t n)
	Construct partition of n elements from a bit vector v.
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.

widen_bitvector()

static std::pair< const exprt, const exprt > widen_bitvector ( const exprt &  lhs, const exprt &  rhs  )

static

Definition at line 321 of file expr_enumerator.cpp.