miniBDD.h File Reference

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

#include <cassert>
#include <list>
#include <vector>
#include <map>
#include <string>
#include <stack>
#include "miniBDD.inc"

Include dependency graph for miniBDD.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	mini_bddt
class	mini_bdd_nodet
class	mini_bdd_mgrt
struct	mini_bdd_mgrt::var_table_entryt
struct	mini_bdd_mgrt::reverse_keyt

Functions
mini_bddt	restrict (const mini_bddt &u, unsigned var, const bool value)
mini_bddt	exists (const mini_bddt &u, unsigned var)
mini_bddt	substitute (const mini_bddt &where, unsigned var, const mini_bddt &by_what)
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.

Small BDD implementation.

Author

Daniel Kroening kroen.nosp@m.ing@.nosp@m.kroen.nosp@m.ing..nosp@m.com

Date

Mon Sep 28 00:00:00 BST 2009

Definition in file miniBDD.h.

Function Documentation

cubes()

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().

exists()

mini_bddt exists	(	const mini_bddt &	u,
		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().

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 &	where,
		unsigned	var,
		const mini_bddt &	by_what
	)

Definition at line 556 of file miniBDD.cpp.

References restrict().