miniBDD.h File Reference

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

#include <list>
#include <map>
#include <stack>
#include <string>
#include <vector>
#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 596 of file miniBDD.cpp.

exists()

mini_bddt exists	(	const mini_bddt &	u,
		unsigned	var
	)

Definition at line 556 of file miniBDD.cpp.

OneSat()

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

Definition at line 610 of file miniBDD.cpp.

restrict()

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

Definition at line 551 of file miniBDD.cpp.

substitute()

mini_bddt substitute	(	const mini_bddt &	where,
		unsigned	var,
		const mini_bddt &	by_what
	)

Definition at line 562 of file miniBDD.cpp.