src/cmuBdd/bddrelprod.c File Reference

#include "bddint.h"

Include dependency graph for bddrelprod.c:

Functions
static bdd	cmu_bdd_rel_prod_step (cmu_bdd_manager bddm, bdd f, bdd g, long op, var_assoc vars)
bdd	cmu_bdd_rel_prod (cmu_bdd_manager bddm, bdd f, bdd g)

Function Documentation

bdd cmu_bdd_rel_prod	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 68 of file bddrelprod.c.

00069 {
00070   long op;
00071 
00072   if (bdd_check_arguments(2, f, g))
00073     {
00074       FIREWALL(bddm);
00075       if (bddm->curr_assoc_id == -1)
00076         {
00077           op=bddm->temp_op--;
00078           /* We decrement the temporary opcode once more because */
00079           /* cmu_bdd_rel_prod may call cmu_bdd_exists_temp, and we don't */
00080           /* want to generate new temporary opcodes for each such */
00081           /* call.  Instead, we pass op-1 to cmu_bdd_exists_temp, and */
00082           /* have it use this opcode for caching. */
00083           bddm->temp_op--;
00084         }
00085       else
00086         op=OP_RELPROD+bddm->curr_assoc_id;
00087       RETURN_BDD(cmu_bdd_rel_prod_step(bddm, f, g, op, bddm->curr_assoc));
00088     }
00089   return ((bdd)0);
00090 }

static bdd cmu_bdd_rel_prod_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g,
		long	op,
		var_assoc	vars
	)			`[static]`

Definition at line 9 of file bddrelprod.c.

00010 {
00011   bdd_indexindex_type top_indexindex;
00012   bdd f1, f2;
00013   bdd g1, g2;
00014   bdd temp1, temp2;
00015   bdd result;
00016   int quantifying;
00017 
00018   BDD_SETUP(f);
00019   BDD_SETUP(g);
00020   if (BDD_IS_CONST(f) || BDD_IS_CONST(g))
00021     {
00022       if (f == BDD_ZERO(bddm) || g == BDD_ZERO(bddm))
00023         return (BDD_ZERO(bddm));
00024       if (f == BDD_ONE(bddm))
00025         return (cmu_bdd_exists_temp(bddm, g, op-1));
00026       return (cmu_bdd_exists_temp(bddm, f, op-1));
00027     }
00028   if ((long)BDD_INDEX(bddm, f) > vars->last && (long)BDD_INDEX(bddm, g) > vars->last)
00029     return (cmu_bdd_ite_step(bddm, f, g, BDD_ZERO(bddm)));
00030   /* Put in canonical order. */
00031   if (BDD_OUT_OF_ORDER(f, g))
00032     BDD_SWAP(f, g);
00033   if (bdd_lookup_in_cache2(bddm, op, f, g, &result))
00034     return (result);
00035   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00036   quantifying=(vars->assoc[top_indexindex] != 0);
00037   BDD_COFACTOR(top_indexindex, f, f1, f2);
00038   BDD_COFACTOR(top_indexindex, g, g1, g2);
00039   temp1=cmu_bdd_rel_prod_step(bddm, f1, g1, op, vars);
00040   if (quantifying && temp1 == BDD_ONE(bddm))
00041     result=temp1;
00042   else
00043     {
00044       temp2=cmu_bdd_rel_prod_step(bddm, f2, g2, op, vars);
00045       if (quantifying)
00046         {
00047           BDD_SETUP(temp1);
00048           BDD_SETUP(temp2);
00049           bddm->op_cache.cache_level++;
00050           result=cmu_bdd_ite_step(bddm, temp1, BDD_ONE(bddm), temp2);
00051           BDD_TEMP_DECREFS(temp1);
00052           BDD_TEMP_DECREFS(temp2);
00053           bddm->op_cache.cache_level--;
00054         }
00055       else
00056         result=bdd_find(bddm, top_indexindex, temp1, temp2);
00057     }
00058   bdd_insert_in_cache2(bddm, op, f, g, result);
00059   return (result);
00060 }

src/cmuBdd/bddrelprod.c File Reference

Functions

Function Documentation