cprover
Loading...
Searching...
No Matches
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.