non_leaf_enumeratort Class Reference

Non-leaf enumerator enumerates expressions of form f(a_1, a_2, ..., a_n) where a_i's are sub-expressions enumerated by sub-enumerators. More...

#include <expr_enumerator.h>

Inheritance diagram for non_leaf_enumeratort:

Collaboration diagram for non_leaf_enumeratort:

Public Member Functions
	non_leaf_enumeratort (const enumeratorst &enumerators, const std::function< bool(const partitiont &)> partition_check, const namespacet &ns)
	non_leaf_enumeratort (const enumeratorst &enumerators, const namespacet &ns)
	As default: no optimization. partition_check Accept all partitions.
expr_sett	enumerate (const std::size_t size) const override
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 each enumerator in the list.
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 bool	is_equivalence_class_representation (const expr_listt &es) const
	As default, keep all expression tuples.
Public Member Functions inherited from enumerator_baset
	enumerator_baset (const namespacet &ns)
	enumerator_baset (const enumerator_baset &other)=delete
enumerator_baset &	operator= (const enumerator_baset &other)=delete
virtual	~enumerator_baset ()=default

Protected Member Functions
virtual exprt	instantiate (const expr_listt &exprs) const =0
	Combine a list of sub-expressions to construct the top-level expression.

Protected Attributes
const std::size_t	arity
const enumeratorst	sub_enumerators
const std::function< bool(const partitiont &)>	is_good_partition
Protected Attributes inherited from enumerator_baset
const namespacet &	ns

Detailed Description

Non-leaf enumerator enumerates expressions of form f(a_1, a_2, ..., a_n) where a_i's are sub-expressions enumerated by sub-enumerators.

Definition at line 154 of file expr_enumerator.h.

Constructor & Destructor Documentation

non_leaf_enumeratort() [1/2]

non_leaf_enumeratort::non_leaf_enumeratort ( const enumeratorst &  enumerators, const std::function< bool(const partitiont &)>  partition_check, const namespacet &  ns  )

inline

Parameters

enumerators	a list of enumerator (e_1,...,e_n), where a_i in the expressions enumerated by this enumerator can be enumerated by the enumerator e_i.
partition_check	an optional function checking whether a partition can be safely discarded.
ns	namespace used by simplify_expr.

Definition at line 163 of file expr_enumerator.h.

non_leaf_enumeratort() [2/2]

non_leaf_enumeratort::non_leaf_enumeratort ( const enumeratorst &  enumerators, const namespacet &  ns  )

inline

As default: no optimization. partition_check Accept all partitions.

Definition at line 177 of file expr_enumerator.h.

Member Function Documentation

cartesian_product_of_enumerators()

std::set< expr_listt > non_leaf_enumeratort::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 each enumerator in the list.

Current enumerator is the last enumerator. Add all expressions enumerated by it_enumerators to result.

First compute the Cartesian product of enumerators after it_enumerators. And then append the expressions enumerated by the it_enumerators to every list in the Cartesian product.

Definition at line 57 of file expr_enumerator.cpp.

enumerate()

expr_sett non_leaf_enumeratort::enumerate ( const std::size_t  size ) const

overridevirtual

Implements enumerator_baset.

Definition at line 24 of file expr_enumerator.cpp.

get_partitions()

std::list< partitiont > non_leaf_enumeratort::get_partitions	(	const std::size_t	n,
		const std::size_t	k
	)		const

Enumerate all partitions of n into k components.

Order of partitions is considered relevant.

Definition at line 234 of file expr_enumerator.cpp.

instantiate()

virtual exprt non_leaf_enumeratort::instantiate ( const expr_listt &  exprs ) const

protectedpure virtual

Combine a list of sub-expressions to construct the top-level expression.

Implemented in binary_functional_enumeratort.

is_equivalence_class_representation()

virtual bool non_leaf_enumeratort::is_equivalence_class_representation ( const expr_listt &  es ) const

inlinevirtual

As default, keep all expression tuples.

Reimplemented in binary_functional_enumeratort.

Definition at line 201 of file expr_enumerator.h.

Member Data Documentation

arity

const std::size_t non_leaf_enumeratort::arity

protected

Definition at line 210 of file expr_enumerator.h.

is_good_partition

const std::function<bool(const partitiont &)> non_leaf_enumeratort::is_good_partition

protected

Definition at line 212 of file expr_enumerator.h.

sub_enumerators

const enumeratorst non_leaf_enumeratort::sub_enumerators

protected

Definition at line 211 of file expr_enumerator.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/goto-synthesizer/expr_enumerator.h
• /home/runner/work/cbmc/cbmc/src/goto-synthesizer/expr_enumerator.cpp