src/cmuBdd/bddcmp.c File Reference

#include "bddint.h"

Include dependency graph for bddcmp.c:

Functions
static int	bdd_fraction_compare (cmu_bdd_manager bddm, bdd f, bdd g)
static int	cmu_bdd_compare_step (cmu_bdd_manager bddm, bdd f, bdd g, bdd_indexindex_type v_indexindex, long op)
int	cmu_bdd_compare_temp (cmu_bdd_manager bddm, bdd f, bdd g, bdd v)
int	cmu_bdd_compare (cmu_bdd_manager bddm, bdd f, bdd g, bdd v)

Function Documentation

static int bdd_fraction_compare	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)			`[static]`

Definition at line 9 of file bddcmp.c.

00010 {
00011   double f_frac, g_frac;
00012 
00013   bddm->op_cache.cache_level++;
00014   f_frac=cmu_bdd_satisfying_fraction_step(bddm, f);
00015   g_frac=cmu_bdd_satisfying_fraction_step(bddm, g);
00016   bddm->op_cache.cache_level--;
00017   if (f_frac < g_frac)
00018     return (-1);
00019   if (f_frac > g_frac)
00020     return (1);
00021   return (0);
00022 }

int cmu_bdd_compare	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g,
		bdd	v
	)

Definition at line 70 of file bddcmp.c.

00071 {
00072   if (bdd_check_arguments(3, f, g, v))
00073     {
00074       BDD_SETUP(v);
00075       if (cmu_bdd_type_aux(bddm, v) != BDD_TYPE_POSVAR)
00076         {
00077           cmu_bdd_warning("cmu_bdd_compare: third argument is not a positive variable");
00078           return (0);
00079         }
00080       return (cmu_bdd_compare_step(bddm, f, g, BDD_INDEXINDEX(v), OP_CMPTO+BDD_INDEXINDEX(v)));
00081     }
00082   return (0);
00083 }

static int cmu_bdd_compare_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g,
		bdd_indexindex_type	v_indexindex,
		long	op
	)			`[static]`

Definition at line 27 of file bddcmp.c.

00028 {
00029   bdd f1, f2;
00030   bdd g1, g2;
00031   bdd_indexindex_type top_indexindex;
00032   INT_PTR result;
00033 
00034   BDD_SETUP(f);
00035   BDD_SETUP(g);
00036   if (f == g)
00037     return (0);
00038   if (BDD_IS_CONST(f) || BDD_IS_CONST(g))
00039     {
00040       if (f == BDD_ZERO(bddm) || g == BDD_ONE(bddm))
00041         return (-1);
00042       return (1);
00043     }
00044   if (bdd_lookup_in_cache2d(bddm, op, f, g, &result))
00045     return ((int)result);
00046   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00047   if (bddm->indexes[top_indexindex] > bddm->indexes[v_indexindex])
00048     result=bdd_fraction_compare(bddm, f, g);
00049   else
00050     {
00051       BDD_COFACTOR(top_indexindex, f, f1, f2);
00052       BDD_COFACTOR(top_indexindex, g, g1, g2);
00053       if (!(result=cmu_bdd_compare_step(bddm, f2, g2, v_indexindex, op)))
00054         result=cmu_bdd_compare_step(bddm, f1, g1, v_indexindex, op);
00055     }
00056   bdd_insert_in_cache2d(bddm, op, f, g, result);
00057   return ((int)result);
00058 }

int cmu_bdd_compare_temp	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g,
		bdd	v
	)

Definition at line 62 of file bddcmp.c.

00063 {
00064   BDD_SETUP(v);
00065   return (cmu_bdd_compare_step(bddm, f, g, BDD_INDEXINDEX(v), OP_CMPTO+BDD_INDEXINDEX(v)));
00066 }

src/cmuBdd/bddcmp.c File Reference

Functions

Function Documentation