ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraZddTrunc.c File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/st/st.h"
#include "bdd/cudd/cuddInt.h"
Include dependency graph for extraZddTrunc.c:

Go to the source code of this file.

Classes

struct  Vec_Int_t_
 

Macros

#define TEST_VAR_MAX   10
 
#define TEST_SET_MAX   10
 

Typedefs

typedef struct Vec_Int_t_ Vec_Int_t
 

Functions

void Extra_zddTruncate_rec (DdManager *dd, DdNode *zFunc, double *pVarProbs, double ProbLimit, double ProbThis, Vec_Int_t *vSubset, Vec_Int_t *vResult)
 
int * Extra_zddTruncate (DdManager *dd, DdNode *zFunc, double *pVarProbs, double ProbLimit)
 
DdNode * Extra_zddVariable (DdManager *dd, int iVar)
 
DdNode * Extra_zddCreateSubsets (DdManager *dd, int pSubsets[][TEST_VAR_MAX+1], int nSubsets)
 
void Extra_zddPrintSubsets (int *pSubsets)
 
void Extra_zddTruncateTest ()
 

Macro Definition Documentation

◆ TEST_SET_MAX

#define TEST_SET_MAX   10

Definition at line 35 of file extraZddTrunc.c.

◆ TEST_VAR_MAX

#define TEST_VAR_MAX   10

CFile****************************************************************

FileName [extraZddTrunc.c]

PackageName [extra]

Synopsis [Procedure to truncate a ZDD using variable probabilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - September 1, 2003.]

Revision [

Id
extraZddTrunc.c,v 1.0 2003/05/21 18:03:50 alanmi Exp

]

Definition at line 34 of file extraZddTrunc.c.

Typedef Documentation

◆ Vec_Int_t

typedef struct Vec_Int_t_ Vec_Int_t

AutomaticStart

Definition at line 66 of file extraZddTrunc.c.

Function Documentation

◆ Extra_zddCreateSubsets()

DdNode * Extra_zddCreateSubsets ( DdManager * dd,
int pSubsets[][TEST_VAR_MAX+1],
int nSubsets )

Function********************************************************************

Synopsis [Creates ZDD representing a given set of subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file extraZddTrunc.c.

245{
246 int i, k;
247 DdNode * zOne, * zVar, * zRes, * zTemp;
248 zRes = Cudd_ReadZero(dd); Cudd_Ref( zRes );
249 for ( i = 0; i < nSubsets; i++ )
250 {
251 zOne = Cudd_ReadOne(dd); Cudd_Ref( zOne );
252 for ( k = 0; pSubsets[i][k] != -1; k++ )
253 {
254 assert( pSubsets[i][k] < TEST_VAR_MAX );
255 zVar = Extra_zddVariable( dd, pSubsets[i][k] );
256 zOne = Cudd_zddUnateProduct( dd, zTemp = zOne, zVar ); Cudd_Ref( zOne );
257 Cudd_RecursiveDerefZdd( dd, zTemp );
258 }
259 zRes = Cudd_zddUnion( dd, zRes, zOne ); Cudd_Ref( zRes );
260 Cudd_RecursiveDerefZdd( dd, zOne );
261 }
262 Cudd_Deref( zRes );
263 return zRes;
264}
#define TEST_VAR_MAX
DdNode * Extra_zddVariable(DdManager *dd, int iVar)
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Extra_zddPrintSubsets()

void Extra_zddPrintSubsets ( int * pSubsets)

Function********************************************************************

Synopsis [Prints a set of subsets represented using as an array.]

Description []

SideEffects []

SeeAlso []

Definition at line 277 of file extraZddTrunc.c.

278{
279 int i, k, Counter = 0;
280 printf( "The set contains %d subsets:\n", pSubsets[0] );
281 for ( i = k = 0; i < pSubsets[0]; i++ )
282 {
283 printf( "Subset %3d : {", Counter );
284 for ( k++; pSubsets[k] != -1; k++ )
285 printf( " %d", pSubsets[k] );
286 printf( " }\n" );
287 Counter++;
288 }
289}
Here is the caller graph for this function:

◆ Extra_zddTruncate()

int * Extra_zddTruncate ( DdManager * dd,
DdNode * zFunc,
double * pVarProbs,
double ProbLimit )

Definition at line 185 of file extraZddTrunc.c.

190{
191 Vec_Int_t * vSubset, * vResult;
192 int i, sizeZ = Cudd_ReadZddSize(dd);
193 int * pResult;
194 // check that probabilities are reasonable
195 assert( ProbLimit > 0 && ProbLimit <= 1 );
196 for ( i = 0; i < sizeZ; i++ )
197 assert( pVarProbs[i] > 0 && pVarProbs[i] <= 1 );
198 // enumerate assignments satisfying the probability limit
199 vSubset = Vec_IntAlloc( sizeZ );
200 vResult = Vec_IntAlloc( 10 * sizeZ );
201 Vec_IntPush( vResult, 0 );
202 Extra_zddTruncate_rec( dd, zFunc, pVarProbs, ProbLimit, 1, vSubset, vResult );
203 Vec_IntFree( vSubset );
204 pResult = Vec_IntReleaseArray( vResult );
205 Vec_IntFree( vResult );
206 return pResult;
207} // end of Extra_zddTruncate
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
void Extra_zddTruncate_rec(DdManager *dd, DdNode *zFunc, double *pVarProbs, double ProbLimit, double ProbThis, Vec_Int_t *vSubset, Vec_Int_t *vResult)
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Extra_zddTruncate_rec()

void Extra_zddTruncate_rec ( DdManager * dd,
DdNode * zFunc,
double * pVarProbs,
double ProbLimit,
double ProbThis,
Vec_Int_t * vSubset,
Vec_Int_t * vResult )

AutomaticEnd Function********************************************************************

Synopsis [Compute the set of subsets whose probability is more than ProbLimit.]

Description [The resulting array has the following form: The first integer entry is the number of resulting subsets. The following integer entries in the array contain as many subsets. Each subset is an array of integers followed by -1. See how subsets are printed in the included test procedure below.]

SideEffects []

SeeAlso []

Definition at line 155 of file extraZddTrunc.c.

163{
164 // quit if probability of the path is less then the limit
165 if ( ProbThis < ProbLimit )
166 return;
167 // quit if there is no subsets
168 if ( zFunc == Cudd_ReadZero(dd) )
169 return;
170 // quit and save a new subset if there is one
171 if ( zFunc == Cudd_ReadOne(dd) )
172 {
173 Vec_IntAddToEntry( vResult, 0, 1 );
174 Vec_IntAppend( vResult, vSubset );
175 Vec_IntPush( vResult, -1 );
176 return;
177 }
178 // call recursively for the set without the given variable
179 Extra_zddTruncate_rec( dd, cuddE(zFunc), pVarProbs, ProbLimit, ProbThis, vSubset, vResult );
180 // call recursively for the set with the given variable
181 Vec_IntPush( vSubset, Cudd_NodeReadIndex(zFunc) );
182 Extra_zddTruncate_rec( dd, cuddT(zFunc), pVarProbs, ProbLimit, ProbThis * pVarProbs[Cudd_NodeReadIndex(zFunc)], vSubset, vResult );
183 Vec_IntPop( vSubset );
184}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Extra_zddTruncateTest()

void Extra_zddTruncateTest ( )

Function********************************************************************

Synopsis [Testbench for the above truncation procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 302 of file extraZddTrunc.c.

303{
304 // input data
305 int nSubsets = 5;
306 int pSubsets[TEST_SET_MAX][TEST_VAR_MAX+1] = { {0, 3, 5, -1}, {1, 2, 3, 6, 9, -1}, {1, 5, 7, 8, -1}, {2, 4, -1}, {0, 5, 6, 9, -1} };
307 // varible probabilities
308 double pVarProbs[TEST_VAR_MAX] = { 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1 };
309 double ProbLimit = 0.001;
310 // output data
311 int * pOutput;
312 // start the manager and create ZDD representing the input subsets
313 DdManager * dd = Cudd_Init( 0, TEST_VAR_MAX, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS , 0 );
314 DdNode * zFunc = Extra_zddCreateSubsets( dd, pSubsets, nSubsets ); Cudd_Ref( zFunc );
315 assert( nSubsets <= TEST_SET_MAX );
316 // print the input ZDD
317 printf( "The initial ZDD representing %d subsets:\n", nSubsets );
318 Cudd_zddPrintMinterm( dd, zFunc );
319 // compute the result of truncation
320 pOutput = Extra_zddTruncate( dd, zFunc, pVarProbs, ProbLimit );
321 // print the resulting ZDD
322 printf( "The resulting ZDD representing %d subsets:\n", pOutput[0] );
323 // print the resulting subsets
324 Extra_zddPrintSubsets( pOutput );
325 // cleanup
326 ABC_FREE( pOutput );
327 Cudd_RecursiveDerefZdd( dd, zFunc );
328 Cudd_Quit( dd );
329}
#define ABC_FREE(obj)
Definition abc_global.h:267
DdNode * Extra_zddCreateSubsets(DdManager *dd, int pSubsets[][TEST_VAR_MAX+1], int nSubsets)
int * Extra_zddTruncate(DdManager *dd, DdNode *zFunc, double *pVarProbs, double ProbLimit)
#define TEST_SET_MAX
void Extra_zddPrintSubsets(int *pSubsets)
Here is the call graph for this function:

◆ Extra_zddVariable()

DdNode * Extra_zddVariable ( DdManager * dd,
int iVar )

Function*************************************************************

Synopsis [Creates the combination composed of a single ZDD variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file extraZddTrunc.c.

221{
222 DdNode * zRes;
223 do {
224 dd->reordered = 0;
225 zRes = cuddZddGetNode( dd, iVar, Cudd_ReadOne(dd), Cudd_ReadZero(dd) );
226 } while (dd->reordered == 1);
227 return zRes;
228}
Here is the caller graph for this function: