From: Chao Wang (Wangc@colorado.edu)
Date: Sun Sep 21 2003 - 20:59:02 MDT
> I am using Cudd in conjunction with the Bmc package of Vis, to implement
> a hybrid symbolic/sat-based model checking method.
Nice work!
> So, my problem is the
> following: given a BDD node, I would like to know the CNF variable
> corresponding to the "label variable" (index) of the node. Is there an
> easy way of doing this?
Here is my way of doing it, (not necessarily the best solution):
(1) Get the bddId of the BDD node,
(2) Get the bAig node name corresponding to that bddId,
(3) Once you have the bAig node name, and the time-frame, you can look up
its cnfIndex.
The tricky part might be Step (2). Here is my function for it.
/**Function********************************************************************
Synopsis [return the baigName of a bddid]
SideEffects [The caller should free the returned char *.
We assume that MDD and MAIG shares the same naming convention.]
SeeAlso []
******************************************************************************/
char *
XXX_BddIdToBaigName(
mdd_manager *mddManager,
int bddid)
{
array_t *mvar_list = mdd_ret_mvar_list(mddManager);
array_t *bvar_list = mdd_ret_bvar_list(mddManager);
bvar_type bv;
mvar_type mv;
int mddid, index, id;
char *nodeName;
char baigName[1024];
// 1. from bddid, get mddid and the index of this bddid in the mddid
bv = array_fetch(bvar_type, bvar_list, bddid);
mddid = bv.mvar_id;
mv = array_fetch(mvar_type, mvar_list, mddid);
arrayForEachItem(int, mv.bvars, index, id) {
if (id == bddid)
break;
}
assert(index <= mv.encode_length -1);
// 2. assumptions: (1) mv.name = nodeName,
// (2) index is the same for MDD and MAIG
nodeName = mv.name;
// 3. the baigEdge_t's name is ("%s_%d",nodeName,index)
sprintf(baigName, "%s_%d", nodeName, index);
return util_strsav(baigName);
}
-------------
Chao
This archive was generated by hypermail 2.1.7 : Sun Sep 21 2003 - 21:00:46 MDT