src/cmuBdd/bddapply.c File Reference

#include "bddint.h"

Include dependency graph for bddapply.c:

Functions
static bdd	bdd_apply2_step (cmu_bdd_manager bddm, bdd(terminal_fn)(cmu_bdd_manager, bdd , bdd *, pointer), long op, bdd f, bdd g, pointer env)
bdd	bdd_apply2 (cmu_bdd_manager bddm, bdd(terminal_fn)(cmu_bdd_manager, bdd , bdd *, pointer), bdd f, bdd g, pointer env)
static bdd	bdd_apply1_step (cmu_bdd_manager bddm, bdd(terminal_fn)(cmu_bdd_manager, bdd , pointer), long op, bdd f, pointer env)
bdd	bdd_apply1 (cmu_bdd_manager bddm, bdd(terminal_fn)(cmu_bdd_manager, bdd , pointer), bdd f, pointer env)

Function Documentation

bdd bdd_apply1	(	cmu_bdd_manager	bddm,
		bdd()(cmu_bdd_manager, bdd , pointer)	terminal_fn,
		bdd	f,
		pointer	env
	)

Definition at line 87 of file bddapply.c.

00088 {
00089   long op;
00090 
00091   if (bdd_check_arguments(1, f))
00092     {
00093       FIREWALL(bddm);
00094       op=bddm->temp_op--;
00095       RETURN_BDD(bdd_apply1_step(bddm, terminal_fn, op, f, env));
00096     }
00097   return ((bdd)0);
00098 }

static bdd bdd_apply1_step	(	cmu_bdd_manager	bddm,
		bdd()(cmu_bdd_manager, bdd , pointer)	terminal_fn,
		long	op,
		bdd	f,
		pointer	env
	)			`[static]`

Definition at line 62 of file bddapply.c.

00063 {
00064   bdd temp1, temp2;
00065   bdd result;
00066 
00067   if ((result=(*terminal_fn)(bddm, &f, env)))
00068     {
00069       BDD_SETUP(result);
00070       BDD_TEMP_INCREFS(result);
00071       return (result);
00072     }
00073   if (bdd_lookup_in_cache1(bddm, op, f, &result))
00074     return (result);
00075   {
00076     BDD_SETUP(f);
00077     temp1=bdd_apply1_step(bddm, terminal_fn, op, BDD_THEN(f), env);
00078     temp2=bdd_apply1_step(bddm, terminal_fn, op, BDD_ELSE(f), env);
00079     result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
00080     bdd_insert_in_cache1(bddm, op, f, result);
00081     return (result);
00082   }
00083 }

bdd bdd_apply2	(	cmu_bdd_manager	bddm,
		bdd()(cmu_bdd_manager, bdd , bdd *, pointer)	terminal_fn,
		bdd	f,
		bdd	g,
		pointer	env
	)

Definition at line 46 of file bddapply.c.

00047 {
00048   long op;
00049 
00050   if (bdd_check_arguments(2, f, g))
00051     {
00052       FIREWALL(bddm);
00053       op=bddm->temp_op--;
00054       RETURN_BDD(bdd_apply2_step(bddm, terminal_fn, op, f, g, env));
00055     }
00056   return ((bdd)0);
00057 }

static bdd bdd_apply2_step	(	cmu_bdd_manager	bddm,
		bdd()(cmu_bdd_manager, bdd , bdd *, pointer)	terminal_fn,
		long	op,
		bdd	f,
		bdd	g,
		pointer	env
	)			`[static]`

Definition at line 9 of file bddapply.c.

00015 {
00016   bdd_indexindex_type top_indexindex;
00017   bdd f1, f2;
00018   bdd g1, g2;
00019   bdd temp1, temp2;
00020   bdd result;
00021 
00022   if ((result=(*terminal_fn)(bddm, &f, &g, env)))
00023     {
00024       BDD_SETUP(result);
00025       BDD_TEMP_INCREFS(result);
00026       return (result);
00027     }
00028   if (bdd_lookup_in_cache2(bddm, op, f, g, &result))
00029     return (result);
00030   {
00031     BDD_SETUP(f);
00032     BDD_SETUP(g);
00033     BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00034     BDD_COFACTOR(top_indexindex, f, f1, f2);
00035     BDD_COFACTOR(top_indexindex, g, g1, g2);
00036     temp1=bdd_apply2_step(bddm, terminal_fn, op, f1, g1, env);
00037     temp2=bdd_apply2_step(bddm, terminal_fn, op, f2, g2, env);
00038     result=bdd_find(bddm, top_indexindex, temp1, temp2);
00039     bdd_insert_in_cache2(bddm, op, f, g, result);
00040     return (result);
00041   }
00042 }

src/cmuBdd/bddapply.c File Reference

Functions

Function Documentation