bdd.c File Reference

#include "tarski.h"

Go to the source code of this file.

Functions
bdd_t *	nodeComputeBdd (F aNode)
int	test_bdd ()
int	bdd_print_dot (bdd_t *aBdd)
int	bdd_print_recur (bdd_t *aBdd, st_table *processedTable)
int	bdd_cmp (char *aBdd, char *bBdd)
int	bdd_hash (char *aBdd, int modulus)
Variables
bdd_manager *	bddMgr = 0
st_table *	nodeToBdd = ( st_table * ) 0
st_table *	indexToName = ( st_table * ) 0

---

Function Documentation

int bdd_cmp (  char *  aBdd, char *  bBdd )

Function******************************************************************** Synopsis [Compare function for bdd_t] Description [Compare function for bdd_t] SideEffects [] SeeAlso [] Definition at line 267 of file bdd.c. Referenced by bdd_print_dot().

int bdd_hash (  char *  aBdd, int  modulus )

Function******************************************************************** Synopsis [Hash function for bdd_t] Description [Hash function for bdd_t] SideEffects [] SeeAlso [] Definition at line 302 of file bdd.c. Referenced by bdd_print_dot().

int bdd_print_dot (  bdd_t *  aBdd  )

Function******************************************************************** Synopsis [Print a bdd in dot format] Description [Print a bdd in dot format] SideEffects [] SeeAlso [] Definition at line 169 of file bdd.c. References bdd_cmp(), bdd_hash(), and bdd_print_recur().

int bdd_print_recur (  bdd_t *  aBdd, st_table *  processedTable )

Function******************************************************************** Synopsis [Print each bdd node one at a time] Description [Print each bdd node one at a time. There's no chance a GC will take place in this routine, so we can key off of the bdd_node field.] SideEffects [] SeeAlso [] Definition at line 199 of file bdd.c. References indexToName. Referenced by bdd_print_dot().

bdd_t* nodeComputeBdd (  F  aNode  )

Function******************************************************************** Synopsis [Create a Bdd for the given formula node. Tree rooted at node is assumed to consist solely of Boolean nodes. Returns a freshly allocated bdd_t, caller is responsible for freeing.] Description [Create a Bdd for the given formula node. Tree rooted at node is assumed to consist solely of Boolean nodes. Returns a freshly allocated bdd_t, caller is responsible for freeing. Proceeds recursively - recursion stops at PIs and registers, with which we associate bdd variables. Right now, we don't do any ordering, just tack new variables on at the end, let the reordering figure out orders. We associate F nodes with bdd_t's and therefore even in the presence of garbage collection and reordering, wherein the bdd_node field changes for the bdd_t's we are safe, since the manager will automatically update these fields.] Definition at line 62 of file bdd.c. References And_c, bddMgr, FALSE_c, Iff_c, indexToName, F::lchild(), node_cmp(), node_hash(), node_test_is_boolean(), nodeToBdd, Not_c, Or_c, F::raw, F::rchild(), TRUE_c, and F::type().

int test_bdd (   )

Function******************************************************************** Synopsis [Test the bdd routines] Description [Test the bdd routines] Definition at line 129 of file bdd.c. References build_fs(), nodeGetSupport(), and cube::nodeToValue.

---

Variable Documentation

bdd_manager* bddMgr = 0

AutomaticEnd************************************************************** Definition at line 28 of file bdd.c. Referenced by nodeComputeBdd().

st_table* indexToName = ( st_table * ) 0

Definition at line 30 of file bdd.c. Referenced by bdd_print_recur(), and nodeComputeBdd().

st_table* nodeToBdd = ( st_table * ) 0

Definition at line 29 of file bdd.c. Referenced by nodeComputeBdd().

---