A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes. More...

#include "miniBDD.h"
#include <cassert>
#include <iostream>

Include dependency graph for miniBDD.cpp:

Classes
class	mini_bdd_applyt

class	restrictt

Macros
#define	forall_nodes(it)

Functions
bool	equal_fkt (bool x, bool y)

bool	xor_fkt (bool x, bool y)

bool	and_fkt (bool x, bool y)

bool	or_fkt (bool x, bool y)

mini_bddt	restrict (const mini_bddt &u, unsigned var, const bool value)

mini_bddt	exists (const mini_bddt &u, const unsigned var)

mini_bddt	substitute (const mini_bddt &t, unsigned var, const mini_bddt &tp)

void	cubes (const mini_bddt &u, const std::string &path, std::string &result)

std::string	cubes (const mini_bddt &u)

bool	OneSat (const mini_bddt &v, std::map< unsigned, bool > &assignment)

Detailed Description

A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes.

Definition in file miniBDD.cpp.

Macro Definition Documentation

◆ forall_nodes

#define forall_nodes ( it )

Value:

for(nodest::const_iterator it=nodes.begin(); \

it!=nodes.end(); it++)

Definition at line 20 of file miniBDD.cpp.

Referenced by mini_bdd_mgrt::DumpDot(), mini_bdd_mgrt::DumpTable(), and mini_bdd_mgrt::DumpTikZ().

Function Documentation

◆ and_fkt()

bool and_fkt	(	bool	x,
		bool	y
	)

Definition at line 386 of file miniBDD.cpp.

◆ cubes() [1/2]

void cubes	(	const mini_bddt &	u,
		const std::string &	path,
		std::string &	result
	)

Definition at line 566 of file miniBDD.cpp.

References mini_bddt::high(), mini_bddt::is_false(), mini_bddt::is_true(), mini_bddt::low(), mini_bdd_nodet::mgr, mini_bddt::node, mini_bddt::var(), and mini_bdd_mgrt::var_table.

Referenced by cubes().

◆ cubes() [2/2]

std::string cubes ( const mini_bddt & u )

Definition at line 591 of file miniBDD.cpp.

References cubes(), mini_bddt::is_false(), and mini_bddt::is_true().

◆ equal_fkt()

bool equal_fkt	(	bool	x,
		bool	y
	)

Definition at line 359 of file miniBDD.cpp.

Referenced by mini_bddt::operator==().

◆ exists()

mini_bddt exists	(	const mini_bddt &	u,
		const unsigned	var
	)

Definition at line 549 of file miniBDD.cpp.

References restrict().

◆ OneSat()

bool OneSat	(	const mini_bddt &	v,
		std::map< unsigned, bool > &	assignment
	)

Definition at line 605 of file miniBDD.cpp.

References mini_bddt::high(), mini_bddt::is_false(), mini_bddt::is_true(), mini_bddt::low(), OneSat(), and mini_bddt::var().

Referenced by OneSat().

◆ or_fkt()

bool or_fkt	(	bool	x,
		bool	y
	)

Definition at line 396 of file miniBDD.cpp.

Referenced by mini_bddt::operator|().

◆ restrict()

mini_bddt restrict	(	const mini_bddt &	u,
		unsigned	var,
		const bool	value
	)

Definition at line 544 of file miniBDD.cpp.

Referenced by exists(), main(), and substitute().

◆ substitute()

mini_bddt substitute	(	const mini_bddt &	t,
		unsigned	var,
		const mini_bddt &	tp
	)

Definition at line 556 of file miniBDD.cpp.