abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Typedefs | Functions
kitCloud.c File Reference
#include "kit.h"

Go to the source code of this file.

Data Structures

struct  Kit_Mux_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Kit_Mux_t_ 		Kit_Mux_t
 DECLARATIONS ///. More...
 

Functions

static int Kit_Mux2Int (Kit_Mux_t m)
 
static Kit_Mux_t Kit_Int2Mux (int m)
 
CloudNode * Kit_TruthToCloud5_rec (CloudManager *dd, unsigned uTruth, int nVars, int nVarsAll)
 FUNCTION DEFINITIONS ///. More...
 
CloudNode * Kit_TruthToCloud_rec (CloudManager *dd, unsigned *pTruth, int nVars, int nVarsAll)
 
CloudNode * Kit_TruthToCloud (CloudManager *dd, unsigned *pTruth, int nVars)
 
int Kit_CreateCloud (CloudManager *dd, CloudNode *pFunc, Vec_Int_t *vNodes)
 
int Kit_CreateCloudFromTruth (CloudManager *dd, unsigned *pTruth, int nVars, Vec_Int_t *vNodes)
 
unsigned * Kit_CloudToTruth (Vec_Int_t *vNodes, int nVars, Vec_Ptr_t *vStore, int fInv)
 
unsigned * Kit_TruthCompose (CloudManager *dd, unsigned *pTruth, int nVars, unsigned **pInputs, int nVarsAll, Vec_Ptr_t *vStore, Vec_Int_t *vNodes)
 
void Kit_TruthCofSupports (Vec_Int_t *vBddDir, Vec_Int_t *vBddInv, int nVars, Vec_Int_t *vMemory, unsigned *puSupps)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t

DECLARATIONS ///.

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

FileName [kitCloud.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures using BDD package CLOUD.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:
kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

]

Definition at line 31 of file kitCloud.c.

Function Documentation

unsigned* Kit_CloudToTruth ( Vec_Int_t *  vNodes,
int  nVars,
Vec_Ptr_t *  vStore,
int  fInv 
)

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

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file kitCloud.c.

230 {
231  unsigned * pThis, * pFan0, * pFan1;
232  Kit_Mux_t Mux;
233  int i, Entry;
234  assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
235  pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
236  Kit_TruthFill( pThis, nVars );
237  Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
238  {
239  Mux = Kit_Int2Mux(Entry);
240  assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );
241  pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
242  pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
243  pThis = (unsigned *)Vec_PtrEntry( vStore, i );
244  Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
245  }
246  // complement the result
247  if ( Mux.i )
248  Kit_TruthNot( pThis, pThis, nVars );
249  return pThis;
250 }
Kit_TruthFill
static void Kit_TruthFill(unsigned *pOut, int nVars)
Definition: kit.h:367
Kit_TruthMuxVarPhase
void Kit_TruthMuxVarPhase(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
Definition: kitTruth.c:1125
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Kit_Mux_t
typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
DECLARATIONS ///.
Definition: kitCloud.c:31
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Kit_Int2Mux
static Kit_Mux_t Kit_Int2Mux(int m)
Definition: kitCloud.c:42
assert
#define assert(ex)
Definition: util_old.h:213
int Kit_CreateCloud ( CloudManager *  dd,
CloudNode *  pFunc,
Vec_Int_t *  vNodes 
)

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

Synopsis [Transforms the array of BDDs into the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file kitCloud.c.

168 {
169  Kit_Mux_t Mux;
170  int nNodes, i;
171  // collect BDD nodes
172  nNodes = Cloud_DagCollect( dd, pFunc );
173  if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
174  return 0;
175  assert( nNodes == Cloud_DagSize( dd, pFunc ) );
176  assert( nNodes < dd->nNodesLimit );
177  Vec_IntClear( vNodes );
178  Vec_IntPush( vNodes, 0 ); // const1 node
179  dd->ppNodes[0]->s = 0;
180  for ( i = 1; i < nNodes; i++ )
181  {
182  dd->ppNodes[i]->s = i;
183  Mux.v = dd->ppNodes[i]->v;
184  Mux.t = dd->ppNodes[i]->t->s;
185  Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
186  Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e);
187  Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
188  // put the MUX into the array
189  Vec_IntPush( vNodes, Kit_Mux2Int(Mux) );
190  }
191  assert( Vec_IntSize(vNodes) == nNodes );
192  // reset signatures
193  for ( i = 0; i < nNodes; i++ )
194  dd->ppNodes[i]->s = dd->nSignCur;
195  return 1;
196 }
Cloud_IsComplement
#define Cloud_IsComplement(p)
Definition: cloud.h:188
Cloud_Regular
#define Cloud_Regular(p)
Definition: cloud.h:185
Kit_Mux_t
typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
DECLARATIONS ///.
Definition: kitCloud.c:31
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Kit_Mux2Int
static int Kit_Mux2Int(Kit_Mux_t m)
Definition: kitCloud.c:41
Cloud_DagSize
int Cloud_DagSize(CloudManager *dd, CloudNode *n)
Definition: cloud.c:721
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Cloud_DagCollect
int Cloud_DagCollect(CloudManager *dd, CloudNode *n)
Definition: cloud.c:772
int Kit_CreateCloudFromTruth ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars,
Vec_Int_t *  vNodes 
)

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

Synopsis [Transforms the array of BDDs into the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file kitCloud.c.

210 {
211  CloudNode * pFunc;
212  Cloud_Restart( dd );
213  pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
214  Vec_IntClear( vNodes );
215  return Kit_CreateCloud( dd, pFunc, vNodes );
216 }
Kit_CreateCloud
int Kit_CreateCloud(CloudManager *dd, CloudNode *pFunc, Vec_Int_t *vNodes)
Definition: kitCloud.c:167
Cloud_Restart
void Cloud_Restart(CloudManager *dd)
Definition: cloud.c:166
Kit_TruthToCloud
CloudNode * Kit_TruthToCloud(CloudManager *dd, unsigned *pTruth, int nVars)
Definition: kitCloud.c:148
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static Kit_Mux_t Kit_Int2Mux ( int  m)
inlinestatic

Definition at line 42 of file kitCloud.c.

42 { union { Kit_Mux_t x; int y; } v; v.y = m; return v.x; }
Kit_Mux_t
typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
DECLARATIONS ///.
Definition: kitCloud.c:31
static int Kit_Mux2Int ( Kit_Mux_t  m)
inlinestatic

Definition at line 41 of file kitCloud.c.

41 { union { Kit_Mux_t x; int y; } v; v.x = m; return v.y; }
Kit_Mux_t
typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
DECLARATIONS ///.
Definition: kitCloud.c:31
void Kit_TruthCofSupports ( Vec_Int_t *  vBddDir,
Vec_Int_t *  vBddInv,
int  nVars,
Vec_Int_t *  vMemory,
unsigned *  puSupps 
)

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file kitCloud.c.

311 {
312  Kit_Mux_t Mux;
313  unsigned * puSuppAll;
314  unsigned * pThis = NULL; // Suppress "might be used uninitialized"
315  unsigned * pFan0, * pFan1;
316  int i, v, Var, Entry, nSupps;
317  nSupps = 2 * nVars;
318 
319  // extend storage
320  if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
321  Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
322  puSuppAll = (unsigned *)Vec_IntArray( vMemory );
323  // clear storage for the const node
324  memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
325  // compute supports from nodes
326  Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
327  {
328  Mux = Kit_Int2Mux(Entry);
329  Var = nVars - 1 - Mux.v;
330  pFan0 = puSuppAll + nSupps * Mux.e;
331  pFan1 = puSuppAll + nSupps * Mux.t;
332  pThis = puSuppAll + nSupps * i;
333  for ( v = 0; v < nSupps; v++ )
334  pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
335  assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
336  assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
337  pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
338  pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
339  }
340  // copy the result
341  memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
342  // compute the inverse
343 
344  // extend storage
345  if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
346  Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
347  puSuppAll = (unsigned *)Vec_IntArray( vMemory );
348  // clear storage for the const node
349  memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
350  // compute supports from nodes
351  Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
352  {
353  Mux = Kit_Int2Mux(Entry);
354 // Var = nVars - 1 - Mux.v;
355  Var = Mux.v;
356  pFan0 = puSuppAll + nSupps * Mux.e;
357  pFan1 = puSuppAll + nSupps * Mux.t;
358  pThis = puSuppAll + nSupps * i;
359  for ( v = 0; v < nSupps; v++ )
360  pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
361  assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
362  assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
363  pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
364  pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
365  }
366 
367  // merge supports
368  for ( Var = 0; Var < nSupps; Var++ )
369  puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
370 }
memset
char * memset()
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
memcpy
char * memcpy()
Kit_Mux_t
typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
DECLARATIONS ///.
Definition: kitCloud.c:31
Vec_IntGrow
static void Vec_IntGrow(Vec_Int_t *p, int nCapMin)
Definition: bblif.c:336
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Kit_Int2Mux
static Kit_Mux_t Kit_Int2Mux(int m)
Definition: kitCloud.c:42
Minisat::Var
int Var
Definition: SolverTypes.h:42
assert
#define assert(ex)
Definition: util_old.h:213
Kit_BitMask
static unsigned Kit_BitMask(int nBits)
Definition: kit.h:225
unsigned* Kit_TruthCompose ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars,
unsigned **  pInputs,
int  nVarsAll,
Vec_Ptr_t *  vStore,
Vec_Int_t *  vNodes 
)

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

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file kitCloud.c.

265 {
266  CloudNode * pFunc;
267  unsigned * pThis, * pFan0, * pFan1;
268  Kit_Mux_t Mux;
269  int i, Entry, RetValue;
270  // derive BDD from truth table
271  Cloud_Restart( dd );
272  pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
273  // convert it into nodes
274  RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
275  if ( RetValue == 0 )
276  printf( "Kit_TruthCompose(): Internal failure!!!\n" );
277  // verify the result
278 // pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
279 // if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
280 // printf( "Failed!\n" );
281  // compute truth table from the BDD
282  assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
283  pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
284  Kit_TruthFill( pThis, nVarsAll );
285  Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
286  {
287  Mux = Kit_Int2Mux(Entry);
288  pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
289  pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
290  pThis = (unsigned *)Vec_PtrEntry( vStore, i );
291  Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
292  }
293  // complement the result
294  if ( Mux.i )
295  Kit_TruthNot( pThis, pThis, nVarsAll );
296  return pThis;
297 }
Kit_CreateCloud
int Kit_CreateCloud(CloudManager *dd, CloudNode *pFunc, Vec_Int_t *vNodes)
Definition: kitCloud.c:167
Kit_TruthFill
static void Kit_TruthFill(unsigned *pOut, int nVars)
Definition: kit.h:367
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cloud_Restart
void Cloud_Restart(CloudManager *dd)
Definition: cloud.c:166
Kit_Mux_t
typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
DECLARATIONS ///.
Definition: kitCloud.c:31
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Kit_TruthToCloud
CloudNode * Kit_TruthToCloud(CloudManager *dd, unsigned *pTruth, int nVars)
Definition: kitCloud.c:148
Kit_TruthMuxPhase
static void Kit_TruthMuxPhase(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, unsigned *pCtrl, int nVars, int fComp0)
Definition: kit.h:463
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Kit_Int2Mux
static Kit_Mux_t Kit_Int2Mux(int m)
Definition: kitCloud.c:42
assert
#define assert(ex)
Definition: util_old.h:213
CloudNode* Kit_TruthToCloud ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars 
)

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file kitCloud.c.

149 {
150  CloudNode * pRes;
151  pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
152 // printf( "%d/%d ", Count, Cloud_DagSize(dd, pRes) );
153  return pRes;
154 }
Kit_TruthToCloud_rec
CloudNode * Kit_TruthToCloud_rec(CloudManager *dd, unsigned *pTruth, int nVars, int nVarsAll)
Definition: kitCloud.c:109
CloudNode* Kit_TruthToCloud5_rec ( CloudManager *  dd,
unsigned  uTruth,
int  nVars,
int  nVarsAll 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Derive BDD from the truth table for 5 variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 59 of file kitCloud.c.

60 {
61  static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
62  CloudNode * pCof0, * pCof1;
63  unsigned uCof0, uCof1;
64  assert( nVars <= 5 );
65  if ( uTruth == 0 )
66  return dd->zero;
67  if ( uTruth == ~0 )
68  return dd->one;
69  if ( nVars == 1 )
70  {
71  if ( uTruth == uVars[0] )
72  return dd->vars[nVarsAll-1];
73  if ( uTruth == ~uVars[0] )
74  return Cloud_Not(dd->vars[nVarsAll-1]);
75  assert( 0 );
76  }
77 // Count++;
78  assert( nVars > 1 );
79  uCof0 = uTruth & ~uVars[nVars-1];
80  uCof1 = uTruth & uVars[nVars-1];
81  uCof0 |= uCof0 << (1<<(nVars-1));
82  uCof1 |= uCof1 >> (1<<(nVars-1));
83  if ( uCof0 == uCof1 )
84  return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
85  if ( uCof0 == ~uCof1 )
86  {
87  pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
88  pCof1 = Cloud_Not( pCof0 );
89  }
90  else
91  {
92  pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
93  pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
94  }
95  return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
96 }
Cloud_Not
#define Cloud_Not(p)
Definition: cloud.h:186
Cloud_MakeNode
CloudNode * Cloud_MakeNode(CloudManager *dd, CloudVar v, CloudNode *t, CloudNode *e)
Definition: cloud.c:254
Kit_TruthToCloud5_rec
CloudNode * Kit_TruthToCloud5_rec(CloudManager *dd, unsigned uTruth, int nVars, int nVarsAll)
FUNCTION DEFINITIONS ///.
Definition: kitCloud.c:59
assert
#define assert(ex)
Definition: util_old.h:213
CloudNode* Kit_TruthToCloud_rec ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars,
int  nVarsAll 
)

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file kitCloud.c.

110 {
111  CloudNode * pCof0, * pCof1;
112  unsigned * pTruth0, * pTruth1;
113  if ( nVars <= 5 )
114  return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
115  if ( Kit_TruthIsConst0(pTruth, nVars) )
116  return dd->zero;
117  if ( Kit_TruthIsConst1(pTruth, nVars) )
118  return dd->one;
119 // Count++;
120  pTruth0 = pTruth;
121  pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
122  if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
123  return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
124  if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
125  {
126  pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
127  pCof1 = Cloud_Not( pCof0 );
128  }
129  else
130  {
131  pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
132  pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
133  }
134  return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
135 }
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
Cloud_Not
#define Cloud_Not(p)
Definition: cloud.h:186
Kit_TruthIsEqual
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Kit_TruthIsConst1
static int Kit_TruthIsConst1(unsigned *pIn, int nVars)
Definition: kit.h:323
Cloud_MakeNode
CloudNode * Cloud_MakeNode(CloudManager *dd, CloudVar v, CloudNode *t, CloudNode *e)
Definition: cloud.c:254
Kit_TruthToCloud_rec
CloudNode * Kit_TruthToCloud_rec(CloudManager *dd, unsigned *pTruth, int nVars, int nVarsAll)
Definition: kitCloud.c:109
Kit_TruthIsOpposite
static int Kit_TruthIsOpposite(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:290
Kit_TruthToCloud5_rec
CloudNode * Kit_TruthToCloud5_rec(CloudManager *dd, unsigned uTruth, int nVars, int nVarsAll)
FUNCTION DEFINITIONS ///.
Definition: kitCloud.c:59