src/cmuBdd/bddsupport.c File Reference

#include "bddint.h"

Include dependency graph for bddsupport.c:

Functions
static int	cmu_bdd_depends_on_step (cmu_bdd_manager bddm, bdd f, bdd_index_type var_index, int mark)
int	cmu_bdd_depends_on (cmu_bdd_manager bddm, bdd f, bdd var)
static void	bdd_unmark_nodes (cmu_bdd_manager bddm, bdd f)
static bdd *	cmu_bdd_support_step (cmu_bdd_manager bddm, bdd f, bdd *support)
void	cmu_bdd_support (cmu_bdd_manager bddm, bdd f, bdd *support)

Function Documentation

static void bdd_unmark_nodes	(	cmu_bdd_manager	bddm,
		bdd	f
	)			`[static]`

Definition at line 52 of file bddsupport.c.

00053 {
00054   bdd temp;
00055 
00056   BDD_SETUP(f);
00057   if (!BDD_MARK(f) || BDD_IS_CONST(f))
00058     return;
00059   BDD_MARK(f)=0;
00060   temp=BDD_IF(bddm, f);
00061   {
00062     BDD_SETUP(temp);
00063     BDD_MARK(temp)=0;
00064   }
00065   bdd_unmark_nodes(bddm, BDD_THEN(f));
00066   bdd_unmark_nodes(bddm, BDD_ELSE(f));
00067 }

int cmu_bdd_depends_on	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	var
	)

Definition at line 32 of file bddsupport.c.

00033 {
00034   if (bdd_check_arguments(2, f, var))
00035     {
00036       BDD_SETUP(var);
00037       if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
00038         {
00039           cmu_bdd_warning("cmu_bdd_depends_on: second argument is not a positive variable");
00040           if (BDD_IS_CONST(var))
00041             return (1);
00042         }
00043       (void)cmu_bdd_depends_on_step(bddm, f, BDD_INDEX(bddm, var), 1);
00044       return (cmu_bdd_depends_on_step(bddm, f, BDD_INDEX(bddm, var), 0));
00045     }
00046   return (0);
00047 }

static int cmu_bdd_depends_on_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd_index_type	var_index,
		int	mark
	)			`[static]`

Definition at line 9 of file bddsupport.c.

00010 {
00011   bdd_index_type f_index;
00012 
00013   BDD_SETUP(f);
00014   f_index=BDD_INDEX(bddm, f);
00015   if (f_index > var_index)
00016     return (0);
00017   if (f_index == var_index)
00018     return (1);
00019   if (BDD_MARK(f) == mark)
00020     return (0);
00021   BDD_MARK(f)=mark;
00022   if (cmu_bdd_depends_on_step(bddm, BDD_THEN(f), var_index, mark))
00023     return (1);
00024   return (cmu_bdd_depends_on_step(bddm, BDD_ELSE(f), var_index, mark));
00025 }

void cmu_bdd_support	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd *	support
	)

Definition at line 99 of file bddsupport.c.

00100 {
00101   bdd *end;
00102 
00103   if (bdd_check_arguments(1, f))
00104     {
00105       end=cmu_bdd_support_step(bddm, f, support);
00106       *end=0;
00107       bdd_unmark_nodes(bddm, f);
00108     }
00109   else
00110     *support=0;
00111 }

static bdd* cmu_bdd_support_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd *	support
	)			`[static]`

Definition at line 72 of file bddsupport.c.

00073 {
00074   bdd temp;
00075 
00076   BDD_SETUP(f);
00077   if (BDD_MARK(f) || BDD_IS_CONST(f))
00078     return (support);
00079   temp=BDD_IF(bddm, f);
00080   {
00081     BDD_SETUP(temp);
00082     if (!BDD_MARK(temp))
00083       {
00084         BDD_MARK(temp)=1;
00085         *support=temp;
00086         ++support;
00087       }
00088   }
00089   BDD_MARK(f)=1;
00090   support=cmu_bdd_support_step(bddm, BDD_THEN(f), support);
00091   return (cmu_bdd_support_step(bddm, BDD_ELSE(f), support));
00092 }

src/cmuBdd/bddsupport.c File Reference

Functions

Function Documentation