glu-2.2: src/cmuBdd/bddrelprod.c Source File

00001 /* BDD relational product routine */
00002 
00003 
00004 #include "bddint.h"
00005 
00006 
00007 static
00008 bdd
00009 cmu_bdd_rel_prod_step(cmu_bdd_manager bddm, bdd f, bdd g, long op, var_assoc vars)
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 }
00061 
00062 
00063 /* cmu_bdd_rel_prod(bddm, f, g) returns the BDD for "f and g" with those */
00064 /* variables which are associated with something in the current */
00065 /* variable association quantified out. */
00066 
00067 bdd
00068 cmu_bdd_rel_prod(cmu_bdd_manager bddm, bdd f, bdd g)
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 }