cprover
|
Enumerator that enumerates binary functional expressions. More...
#include <expr_enumerator.h>
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 |
![]() | |
const std::size_t | arity |
const enumeratorst | sub_enumerators |
const std::function< bool(const partitiont &) | is_good_partition ) |
![]() | |
const namespacet & | ns |
Enumerator that enumerates binary functional expressions.
Definition at line 215 of file expr_enumerator.h.
|
inline |
Definition at line 218 of file expr_enumerator.h.
|
inline |
Definition at line 231 of file expr_enumerator.h.
|
inline |
Definition at line 247 of file expr_enumerator.h.
|
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.
Definition at line 288 of file expr_enumerator.cpp.
|
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.
Definition at line 273 of file expr_enumerator.h.
Definition at line 275 of file expr_enumerator.h.