Diagram manager for Binary Decision Diagrams. More...

#include <core.hpp>

Inheritance diagram for teddy::bdd_manager:

Public Member Functions
	bdd_manager (int32 varCount, int64 nodePoolSize, std::vector< int32 > order=default_oder())
	Initializes BDD manager.

	bdd_manager (int32 varCount, int64 nodePoolSize, int64 overflowNodePoolSize, std::vector< int32 > order=default_oder())
	Initializes BDD manager.

Public Member Functions inherited from teddy::diagram_manager< void, degrees::fixed< 2 >, domains::fixed< 2 > >
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< 2 >, domains::fixed< 2 > >
using	diagram_t = diagram< void, degrees::fixed< 2 > >
	Alias for the diagram type used in the functions of this manager.

Protected Types inherited from teddy::diagram_manager< void, degrees::fixed< 2 >, domains::fixed< 2 > >
using	node_t = typename diagram< void, degrees::fixed< 2 > >::node_t

using	son_container = typename node_t::son_container

Protected Member Functions inherited from teddy::diagram_manager< void, degrees::fixed< 2 >, domains::fixed< 2 > >
	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< 2 >, domains::fixed< 2 > >
node_manager< void, degrees::fixed< 2 >, domains::fixed< 2 > >	nodes_

Detailed Description

Diagram manager for Binary Decision Diagrams.

Constructor & Destructor Documentation

◆ bdd_manager() [1/2]

teddy::bdd_manager::bdd_manager	(	int32	varCount,
		int64	nodePoolSize,
		std::vector< int32 >	order = `default_oder()`
	)

inline

Initializes BDD manager.

Parameters

varCount	Number of variables.
nodePoolSize	Size of the main node pool.
order	Order of variables. Variables are ordered by their indices by default.

◆ bdd_manager() [2/2]

teddy::bdd_manager::bdd_manager	(	int32	varCount,
		int64	nodePoolSize,
		int64	overflowNodePoolSize,
		std::vector< int32 >	order = `default_oder()`
	)