teddy::ifmdd_manager< M > Class Template Reference

Diagram manager (integer) Multi-valued Decision Diagrams (iMDDs) More...

#include <core.hpp>

Inheritance diagram for teddy::ifmdd_manager< M >:

Public Member Functions
	ifmdd_manager (int32 varCount, int64 nodePoolSize, std::vector< int32 > domains, std::vector< int32 > order=default_oder())
	Initializes ifMDD manager.
	ifmdd_manager (int32 varCount, int64 nodePoolSize, int64 overflowNodePoolSize, std::vector< int32 > domains, std::vector< int32 > order=default_oder())
	Initializes ifMDD manager.
Public Member Functions inherited from teddy::diagram_manager< void, degrees::fixed< M >, domains::mixed >
auto	constant (int32 val) -> diagram_t
	Creates diagram representing constant function.
auto	variable (int32 index) -> diagram_t
	Creates diagram representing function of single variable.
auto	variable_not (int32 index) -> utils::second_t< Foo, diagram_t >
	Creates BDD representing function of complemented variable.
auto	operator() (int32 index) -> diagram_t
	Creates diagram representing function of single variable.
auto	variables (std::initializer_list< T > indices) -> std::vector< diagram_t >
	Creates vector of diagrams representing single variables.
auto	variables (I first, S last) -> std::vector< diagram_t >
	Creates vector of diagrams representing functions of single variables.
auto	variables (Is const &indices) -> std::vector< diagram_t >
	Creates vector of diagrams representing single variables.
auto	from_vector (I first, S last) -> diagram_t
	Creates diagram from a truth vector of a function.
auto	from_vector (R &&vector) -> diagram_t
	Creates diagram from a truth vector of a function.
auto	to_vector (diagram_t const &diagram) const -> std::vector< int32 >
	Creates truth vector from the diagram.
auto	to_vector_g (diagram_t const &diagram, O out) const -> void
	Creates truth vector from the diagram.
auto	from_pla (pla_file const &file, fold_type foldType=fold_type::Tree) -> utils::second_t< Foo, std::vector< diagram_t > >
	Creates BDDs defined by PLA file.
auto	from_expression_tree (Node const &root) -> diagram_t
	Creates diagram from an expression tree (AST).
auto	apply (diagram_t const &lhs, diagram_t const &rhs) -> diagram_t
	Merges two diagrams using given binary operation.
auto	apply_n (Diagram const &... diagrams) -> diagram_t
	TODO.
auto	left_fold (R const &diagrams) -> diagram_t
	Merges diagams in the range using the apply function and binary operation.
auto	left_fold (I first, S last) -> diagram_t
	Merges diagams in the range using the apply function and binary operation.
auto	tree_fold (R &diagrams) -> diagram_t
	Merges diagams in the range using the apply function and binary operation.
auto	tree_fold (I first, S last) -> diagram_t
	Merges diagams in the range using the apply function and binary operation.
auto	evaluate (diagram_t const &diagram, Vars const &values) const -> int32
	Evaluates value of the function represented by the diagram.
auto	satisfy_count (int32 value, diagram_t const &diagram) -> int64
	Calculates number of variable assignments for which the functions evaluates to certain value.
auto	satisfy_one (int32 value, diagram_t const &diagram) -> std::optional< Vars >
	Finds variable assignment for which diagram evaluates to value.
auto	satisfy_all (int32 value, diagram_t const &diagram) const -> std::vector< Vars >
	Enumerates all elements of the satisfying set.
auto	satisfy_all_g (int32 value, diagram_t const &diagram, O out) const -> void
	Enumerates all elements of the satisfying set.
auto	satisfy_all_g (int32 const value, diagram_t const &diagram, OutputIt out) const -> void
auto	get_cofactor (diagram_t const &diagram, int32 varIndex, int32 varValue) -> diagram_t
	Calculates cofactor of the functions.
auto	get_cofactor (diagram_t const &diagram, std::vector< var_cofactor > const &vars) -> diagram_t
auto	transform (diagram_t const &diagram, F transformer) -> diagram_t
	Transforms values of the function.
auto	negate (diagram_t const &diagram) -> utils::second_t< Foo, diagram_t >
	Negates Boolean function.
auto	get_dependency_set (diagram_t const &diagram) const -> std::vector< int32 >
	Enumerates indices of variables that the function depends on.
auto	get_dependency_set_g (diagram_t const &diagram, O out) const -> void
	Enumerates indices of variables that the function depends on.
auto	reduce (diagram_t const &diagram) -> diagram_t
	Reduces diagrams to its canonical form.
auto	get_node_count () const -> int64
	Returns number of nodes that are currently used by the manager.
auto	get_node_count (diagram_t const &diagram) const -> int64
	Returns number of nodes in the diagram including terminal nodes.
auto	to_dot_graph (std::ostream &out) const -> void
	Prints dot representation of the graph.
auto	to_dot_graph (std::ostream &out, diagram_t const &diagram) const -> void
	Prints dot representation of the diagram.
auto	force_gc () -> void
	Runs garbage collection.
auto	force_reorder () -> void
	Runs variable reordering heuristic.
auto	clear_cache () -> void
	Clears apply cache.
auto	get_var_count () const -> int32
	Returns number of variables for this manager set in the constructor.
auto	get_order () const -> std::vector< int32 > const &
	Returns current order of variables.
auto	get_domains () const -> std::vector< int32 >
	Return domains of variables.
auto	set_cache_ratio (double ratio) -> void
	Sets the relative cache size w.r.t the number of nodes.
auto	set_gc_ratio (double ratio) -> void
	Sets ratio used to determine new node pool allocation.
auto	set_auto_reorder (bool doReorder) -> void
	Enables or disables automatic variable reordering.
	diagram_manager (diagram_manager &&) noexcept=default
	diagram_manager (diagram_manager const &)=delete
auto	operator= (diagram_manager &&) noexcept -> diagram_manager &=default
auto	operator= (diagram_manager const &) -> diagram_manager &=delete

Additional Inherited Members
Public Types inherited from teddy::diagram_manager< void, degrees::fixed< M >, domains::mixed >
using	diagram_t = diagram< void, degrees::fixed< M > >
	Alias for the diagram type used in the functions of this manager.
Protected Types inherited from teddy::diagram_manager< void, degrees::fixed< M >, domains::mixed >
using	node_t = typename diagram< void, degrees::fixed< M > >::node_t
using	son_container = typename node_t::son_container
Protected Member Functions inherited from teddy::diagram_manager< void, degrees::fixed< M >, domains::mixed >
	diagram_manager (int32 varCount, int64 nodePoolSize, int64 extraNodePoolSize, std::vector< int32 > order)
	Initializes diagram manager.
	diagram_manager (int32 varCount, int64 nodePoolSize, int64 extraNodePoolSize, domains::mixed domain, std::vector< int32 > order)
	Initializes diagram manager.
Protected Attributes inherited from teddy::diagram_manager< void, degrees::fixed< M >, domains::mixed >
node_manager< void, degrees::fixed< M >, domains::mixed >	nodes_

Detailed Description

template<int32 M>
class teddy::ifmdd_manager< M >

Diagram manager (integer) Multi-valued Decision Diagrams (iMDDs)

Unlike mdd_manager variables in ifMDDs can have different domains. However, node representation is the same since the maximal number of sons is known at compile time. Note that some memory might be allocated but unused because each node allocates space for PMax sons regardles of its domain.

Template Parameters

M	maximum of the sizes of domains of variables

Constructor & Destructor Documentation

ifmdd_manager() [1/2]

template<int32 M>

teddy::ifmdd_manager< M >::ifmdd_manager	(	int32	varCount,
		int64	nodePoolSize,
		std::vector< int32 >	domains,
		std::vector< int32 >	order = default_oder()
	)

Initializes ifMDD manager.

Parameters

varCount	Number of variables
nodePoolSize	Size of the main node pool
domains	Domains of variables Number at index i is the domain of i-th variable.
order	Order of variables. Variables are ordered by their indices by default

ifmdd_manager() [2/2]

template<int32 PMax>

teddy::ifmdd_manager< PMax >::ifmdd_manager	(	int32	varCount,
		int64	nodePoolSize,
		int64	overflowNodePoolSize,
		std::vector< int32 >	domains,
		std::vector< int32 >	order = default_oder()
	)

Initializes ifMDD manager.

Parameters

varCount	Number of variables
nodePoolSize	Size of the main node pool
overflowNodePoolSize	Size of the additional node pools
domains	Domains of variables Number at index i is the domain of i-th variable.
order	Order of variables. Variables are ordered by their indices by default

---

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

• core.hpp