CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
binary_functional_enumeratort Class Reference

Enumerator that enumerates binary functional expressions. More...

#include <expr_enumerator.h>

+ Inheritance diagram for binary_functional_enumeratort:
+ Collaboration diagram for binary_functional_enumeratort:

Public Member Functions

 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)
 
 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)
 
 binary_functional_enumeratort (const irep_idt &op, const enumerator_baset &enumerator_1, const enumerator_baset &enumerator_2, const namespacet &ns)
 
bool is_commutative (const irep_idt &op) const
 
bool is_equivalence_class_representation (const expr_listt &exprs) const override
 Determine whether a tuple of expressions is the representation of some equivalence class.
 
- Public Member Functions inherited from non_leaf_enumeratort
 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.
 
- 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

exprt instantiate (const expr_listt &exprs) const override
 Combine a list of sub-expressions to construct the top-level expression.
 

Protected Attributes

const bool is_exchangeable = false
 
const irep_idt & op_id
 
- Protected Attributes inherited from non_leaf_enumeratort
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

Enumerator that enumerates binary functional expressions.

Definition at line 216 of file expr_enumerator.h.

Constructor & Destructor Documentation

◆ binary_functional_enumeratort() [1/3]

binary_functional_enumeratort::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 
)
inline

Definition at line 219 of file expr_enumerator.h.

◆ binary_functional_enumeratort() [2/3]

binary_functional_enumeratort::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 
)
inline

Definition at line 232 of file expr_enumerator.h.

◆ binary_functional_enumeratort() [3/3]

binary_functional_enumeratort::binary_functional_enumeratort ( const irep_idt &  op,
const enumerator_baset &  enumerator_1,
const enumerator_baset &  enumerator_2,
const namespacet &  ns 
)
inline

Definition at line 248 of file expr_enumerator.h.

Member Function Documentation

◆ instantiate()

exprt binary_functional_enumeratort::instantiate ( const expr_listt &  exprs) const
overrideprotectedvirtual

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

Implements non_leaf_enumeratort.

Definition at line 372 of file expr_enumerator.cpp.

◆ is_commutative()

bool binary_functional_enumeratort::is_commutative ( const irep_idt &  op) const

Definition at line 288 of file expr_enumerator.cpp.

◆ is_equivalence_class_representation()

bool binary_functional_enumeratort::is_equivalence_class_representation ( const expr_listt &  exprs) const
overridevirtual

Determine whether a tuple of expressions is the representation of some equivalence class.

We are not sure if exprs is represented by some other tuple.

Reimplemented from non_leaf_enumeratort.

Definition at line 296 of file expr_enumerator.cpp.

Member Data Documentation

◆ is_exchangeable

const bool binary_functional_enumeratort::is_exchangeable = false
protected

Definition at line 274 of file expr_enumerator.h.

◆ op_id

const irep_idt& binary_functional_enumeratort::op_id
protected

Definition at line 276 of file expr_enumerator.h.

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