cprover
miniBDD.cpp File Reference

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:

Go to the source code of this file.

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.

References mini_bddt::operator &().

§ cubes() [1/2]

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

§ 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 
)

§ 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.

References restrict().

§ xor_fkt()

bool xor_fkt ( bool  x,
bool  y 
)

Definition at line 369 of file miniBDD.cpp.

Referenced by mini_bddt::operator^().