abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
dauNonDsd.c File Reference
#include "dauInt.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Dau_DecCheckSetTop5 (word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
 DECLARATIONS ///. More...
 
int Dau_DecCheckSetTop6 (word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
 
static int Dau_DecCheckSetTop (word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
 
static void Dau_DecGetMinterm (word *p, int g, int nVarsS, int uMaskAll)
 
static int Dau_DecCheckSet5 (word *p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word *pCof0, word *pCof1, word *pDec)
 
static int Dau_DecCheckSet6 (word *p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word *pCof0, word *pCof1, word *pDec)
 
static int Dau_DecCheckSetAny (word *p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word *pCof0, word *pCof1, word *pDec)
 
int Dau_DecCheckSetTopOld (word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word **pCof0, word **pCof1, word **pDec)
 
static unsigned Dau_DecCreateSet (int *pVarsB, int sizeB, int maskS)
 
static int Dau_DecSetHas01 (unsigned Mask)
 
static int Dau_DecSetIsContained (Vec_Int_t *vSets, unsigned New)
 
void Dau_DecSortSet (unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
 
void Dau_DecPrintSet (unsigned set, int nVars, int fNewLine)
 
unsigned Dau_DecReadSet (char *pStr)
 
void Dau_DecPrintSets (Vec_Int_t *vSets, int nVars)
 
void Dau_DecMoveFreeToLSB (word *p, int nVars, int *V2P, int *P2V, int maskB, int sizeB)
 
Vec_Int_t * Dau_DecFindSets_int (word *pInit, int nVars, int *pSched[16])
 
Vec_Int_t * Dau_DecFindSets (word *pInit, int nVars)
 
void Dau_DecFindSetsTest2 ()
 
void Dau_DecVarReplace (char *pStr, int *pPerm, int nVars)
 
int Dau_DecDecomposeSet (word *pInit, int nVars, unsigned uSet, word *pComp, word *pDec, int *pPermC, int *pPermD, int *pnVarsC, int *pnVarsD, int *pnVarsS)
 
int Dau_DecVerify (word *pInit, int nVars, char *pDsdC, char *pDsdD)
 
int Dau_DecPerform6 (word *p, int nVars, unsigned uSet)
 
int Dau_DecPerform (word *pInit, int nVars, unsigned uSet)
 
void Dau_DecTrySets (word *pInit, int nVars, int fVerbose)
 
void Dau_DecFindSetsTest3 ()
 
void Dau_DecFindSetsTest ()
 

Function Documentation

static int Dau_DecCheckSet5 ( word *  p,
int  nVars,
int  nVarsF,
int  uMaskAll,
int  uMaskValue,
word *  pCof0,
word *  pCof1,
word *  pDec 
)
inlinestatic

Definition at line 213 of file dauNonDsd.c.

214 {
215  int fFound0 = 0, fFound1 = 0;
216  int g, gMax = (1 << (nVars - nVarsF));
217  int Shift = 6 - nVarsF, Mask = (1 << Shift) - 1;
218  word Mask2 = (((word)1) << (1 << nVarsF)) - 1;
219  word Cof0 = 0, Cof1 = 0, Value;
220  assert( nVarsF >= 1 && nVarsF <= 5 );
221  if ( pDec ) *pDec = 0;
222  for ( g = 0; g < gMax; g++ )
223  if ( (g & uMaskAll) == uMaskValue ) // this minterm g matches shared variable minterm uMaskValue
224  {
225  Value = (p[g>>Shift] >> ((g&Mask)<<nVarsF)) & Mask2;
226  if ( !fFound0 )
227  Cof0 = Value, fFound0 = 1;
228  else if ( Cof0 == Value )
229  continue;
230  else if ( !fFound1 )
231  {
232  Cof1 = Value, fFound1 = 1;
233  if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
234  }
235  else if ( Cof1 == Value )
236  {
237  if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
238  continue;
239  }
240  else
241  return 0;
242  }
243  if ( pCof0 )
244  {
245  assert( fFound0 );
246  Cof1 = fFound1 ? Cof1 : Cof0;
247  *pCof0 = Abc_Tt6Stretch( Cof0, nVarsF );
248  *pCof1 = Abc_Tt6Stretch( Cof1, nVarsF );
249  }
250  return 1;
251 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dau_DecGetMinterm
static void Dau_DecGetMinterm(word *p, int g, int nVarsS, int uMaskAll)
Definition: dauNonDsd.c:200
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
assert
#define assert(ex)
Definition: util_old.h:213
static int Dau_DecCheckSet6 ( word *  p,
int  nVars,
int  nVarsF,
int  uMaskAll,
int  uMaskValue,
word *  pCof0,
word *  pCof1,
word *  pDec 
)
inlinestatic

Definition at line 252 of file dauNonDsd.c.

253 {
254  int fFound0 = 0, fFound1 = 0;
255  int g, gMax = (1 << (nVars - nVarsF));
256  int nWords = Abc_TtWordNum(nVarsF);
257  word * Cof0 = NULL, * Cof1 = NULL;
258  assert( nVarsF >= 6 && nVarsF <= nVars - 2 );
259  if ( pDec ) *pDec = 0;
260  for ( g = 0; g < gMax; g++ )
261  if ( (g & uMaskAll) == uMaskValue )
262  {
263  if ( !fFound0 )
264  Cof0 = p + g * nWords, fFound0 = 1;
265  else if ( !memcmp(Cof0, p + g * nWords, sizeof(word) * nWords) )
266  continue;
267  else if ( !fFound1 )
268  {
269  Cof1 = p + g * nWords, fFound1 = 1;
270  if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
271  }
272  else if ( !memcmp(Cof1, p + g * nWords, sizeof(word) * nWords) )
273  {
274  if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
275  continue;
276  }
277  else
278  return 0;
279  }
280  if ( pCof0 )
281  {
282  assert( fFound0 );
283  Cof1 = fFound1 ? Cof1 : Cof0;
284  memcpy( pCof0, Cof0, sizeof(word) * nWords );
285  memcpy( pCof1, Cof1, sizeof(word) * nWords );
286  }
287  return 1;
288 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dau_DecGetMinterm
static void Dau_DecGetMinterm(word *p, int g, int nVarsS, int uMaskAll)
Definition: dauNonDsd.c:200
memcpy
char * memcpy()
nWords
int nWords
Definition: abcNpn.c:127
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
memcmp
int memcmp()
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
assert
#define assert(ex)
Definition: util_old.h:213
static int Dau_DecCheckSetAny ( word *  p,
int  nVars,
int  nVarsF,
int  uMaskAll,
int  uMaskValue,
word *  pCof0,
word *  pCof1,
word *  pDec 
)
inlinestatic

Definition at line 289 of file dauNonDsd.c.

290 {
291  assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
292  if ( nVarsF < 6 )
293  return Dau_DecCheckSet5( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
294  else
295  return Dau_DecCheckSet6( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
296 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dau_DecCheckSet5
static int Dau_DecCheckSet5(word *p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word *pCof0, word *pCof1, word *pDec)
Definition: dauNonDsd.c:213
Dau_DecCheckSet6
static int Dau_DecCheckSet6(word *p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word *pCof0, word *pCof1, word *pDec)
Definition: dauNonDsd.c:252
assert
#define assert(ex)
Definition: util_old.h:213
static int Dau_DecCheckSetTop ( word *  p,
int  nVars,
int  nVarsF,
int  nVarsB,
int  nVarsS,
int  uMaskS,
int *  pSched,
word *  pDec,
word *  pComp 
)
inlinestatic

Definition at line 181 of file dauNonDsd.c.

182 {
183  if ( nVarsF < 6 )
184  return Dau_DecCheckSetTop5( p, nVars, nVarsF, nVarsB, nVarsS, uMaskS, pSched, pDec, pComp );
185  else
186  return Dau_DecCheckSetTop6( p, nVars, nVarsF, nVarsB, nVarsS, uMaskS, pSched, pDec, pComp );
187 }
Dau_DecCheckSetTop6
int Dau_DecCheckSetTop6(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
Definition: dauNonDsd.c:116
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dau_DecCheckSetTop5
ABC_NAMESPACE_IMPL_START int Dau_DecCheckSetTop5(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
DECLARATIONS ///.
Definition: dauNonDsd.c:46
ABC_NAMESPACE_IMPL_START int Dau_DecCheckSetTop5 ( word *  p,
int  nVars,
int  nVarsF,
int  nVarsB,
int  nVarsS,
int  uMaskS,
int *  pSched,
word *  pDec,
word *  pComp 
)

DECLARATIONS ///.

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

FileName [dauNonDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware unmapping.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
dauNonDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Checks decomposability with given variable set.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file dauNonDsd.c.

47 {
48  word Cof[2][64], Value;
49  word MaskFF = (((word)1) << (1 << nVarsF)) - 1;
50  int ShiftF = 6 - nVarsF, MaskF = (1 << ShiftF) - 1;
51  int pVarsS[16], pVarsB[16];
52  int nMints = (1 << nVarsB);
53  int nMintsB = (1 <<(nVarsB-nVarsS));
54  int nMintsS = (1 << nVarsS);
55  int s, b, v, m, Mint, MintB, MintS;
56  assert( nVars == nVarsB + nVarsF );
57  assert( nVars <= 16 );
58  assert( nVarsS <= 6 );
59  assert( nVarsF >= 1 && nVarsF <= 5 );
60  // collect bound/shared variables
61  for ( s = b = v = 0; v < nVarsB; v++ )
62  if ( (uMaskS >> v) & 1 )
63  pVarsB[v] = -1, pVarsS[v] = s++;
64  else
65  pVarsS[v] = -1, pVarsB[v] = b++;
66  assert( s == nVarsS );
67  assert( b == nVarsB-nVarsS );
68  // clean minterm storage
69  for ( s = 0; s < nMintsS; s++ )
70  Cof[0][s] = Cof[1][s] = ~(word)0;
71  // iterate through bound set minters
72  for ( MintS = MintB = Mint = m = 0; m < nMints; m++ )
73  {
74  // find minterm value
75  Value = (p[Mint>>ShiftF] >> ((Mint&MaskF)<<nVarsF)) & MaskFF;
76  // check if this cof already appeared
77  if ( !~Cof[0][MintS] || Cof[0][MintS] == Value )
78  Cof[0][MintS] = Value;
79  else if ( !~Cof[1][MintS] || Cof[1][MintS] == Value )
80  {
81  Cof[1][MintS] = Value;
82  if ( pDec )
83  {
84  int iMintB = MintS * nMintsB + MintB;
85  pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63));
86  }
87  }
88  else
89  return 0;
90  // find next minterm
91  v = pSched[m];
92  Mint ^= (1 << v);
93  if ( (uMaskS >> v) & 1 ) // shared variable
94  MintS ^= (1 << pVarsS[v]);
95  else
96  MintB ^= (1 << pVarsB[v]);
97  }
98  // create composition function
99  if ( pComp )
100  {
101  for ( s = 0; s < nMintsS; s++ )
102  {
103  pComp[s>>ShiftF] |= (Cof[0][s] << ((s&MaskF) << nVarsF));
104  if ( ~Cof[1][s] )
105  pComp[(s+nMintsS)>>ShiftF] |= (Cof[1][s] << (((s+nMintsS)&MaskF) << nVarsF));
106  else
107  pComp[(s+nMintsS)>>ShiftF] |= (Cof[0][s] << (((s+nMintsS)&MaskF) << nVarsF));
108  }
109  if ( nVarsF + nVarsS + 1 < 6 )
110  pComp[0] = Abc_Tt6Stretch( pComp[0], nVarsF + nVarsS + 1 );
111  }
112  if ( pDec && nVarsB < 6 )
113  pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB );
114  return 1;
115 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
assert
#define assert(ex)
Definition: util_old.h:213
int Dau_DecCheckSetTop6 ( word *  p,
int  nVars,
int  nVarsF,
int  nVarsB,
int  nVarsS,
int  uMaskS,
int *  pSched,
word *  pDec,
word *  pComp 
)

Definition at line 116 of file dauNonDsd.c.

117 {
118  word * Cof[2][64];
119  int nWordsF = Abc_TtWordNum(nVarsF);
120  int pVarsS[16], pVarsB[16];
121  int nMints = (1 << nVarsB);
122  int nMintsB = (1 <<(nVarsB-nVarsS));
123  int nMintsS = (1 << nVarsS);
124  int s, b, v, m, Mint, MintB, MintS;
125  assert( nVars == nVarsB + nVarsF );
126  assert( nVars <= 16 );
127  assert( nVarsS <= 6 );
128  assert( nVarsF >= 6 );
129  // collect bound/shared variables
130  for ( s = b = v = 0; v < nVarsB; v++ )
131  if ( (uMaskS >> v) & 1 )
132  pVarsB[v] = -1, pVarsS[v] = s++;
133  else
134  pVarsS[v] = -1, pVarsB[v] = b++;
135  assert( s == nVarsS );
136  assert( b == nVarsB-nVarsS );
137  // clean minterm storage
138  for ( s = 0; s < nMintsS; s++ )
139  Cof[0][s] = Cof[1][s] = NULL;
140  // iterate through bound set minters
141  for ( MintS = MintB = Mint = m = 0; m < nMints; m++ )
142  {
143  // check if this cof already appeared
144  if ( !Cof[0][MintS] || !memcmp(Cof[0][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) )
145  Cof[0][MintS] = p + Mint * nWordsF;
146  else if ( !Cof[1][MintS] || !memcmp(Cof[1][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) )
147  {
148  Cof[1][MintS] = p + Mint * nWordsF;
149  if ( pDec )
150  {
151  int iMintB = MintS * nMintsB + MintB;
152  pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63));
153  }
154  }
155  else
156  return 0;
157  // find next minterm
158  v = pSched[m];
159  Mint ^= (1 << v);
160  if ( (uMaskS >> v) & 1 ) // shared variable
161  MintS ^= (1 << pVarsS[v]);
162  else
163  MintB ^= (1 << pVarsB[v]);
164  }
165  // create composition function
166  if ( pComp )
167  {
168  for ( s = 0; s < nMintsS; s++ )
169  {
170  memcpy( pComp + s * nWordsF, Cof[0][s], sizeof(word) * nWordsF );
171  if ( Cof[1][s] )
172  memcpy( pComp + (s+nMintsS) * nWordsF, Cof[1][s], sizeof(word) * nWordsF );
173  else
174  memcpy( pComp + (s+nMintsS) * nWordsF, Cof[0][s], sizeof(word) * nWordsF );
175  }
176  }
177  if ( pDec && nVarsB < 6 )
178  pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB );
179  return 1;
180 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
memcpy
char * memcpy()
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
memcmp
int memcmp()
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
assert
#define assert(ex)
Definition: util_old.h:213
int Dau_DecCheckSetTopOld ( word *  p,
int  nVars,
int  nVarsF,
int  nVarsB,
int  nVarsS,
int  maskS,
word **  pCof0,
word **  pCof1,
word **  pDec 
)

Definition at line 297 of file dauNonDsd.c.

298 {
299  int i, pVarsS[16];
300  int v, m, mMax = (1 << nVarsS), uMaskValue;
301  assert( nVars >= 3 && nVars <= 16 );
302  assert( nVars == nVarsF + nVarsB );
303  assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
304  assert( nVarsB >= 2 && nVarsB <= nVars - 1 );
305  assert( nVarsS >= 0 && nVarsS <= nVarsB - 2 );
306  if ( nVarsS == 0 )
307  return Dau_DecCheckSetAny( p, nVars, nVarsF, 0, 0, pCof0? pCof0[0] : 0, pCof1? pCof1[0] : 0, pDec? pDec[0] : 0 );
308  // collect shared variables
309  assert( maskS > 0 && maskS < (1 << nVarsB) );
310  for ( i = 0, v = 0; v < nVarsB; v++ )
311  if ( (maskS >> v) & 1 )
312  pVarsS[i++] = v;
313  assert( i == nVarsS );
314  // go through shared set minterms
315  for ( m = 0; m < mMax; m++ )
316  {
317  // generate share set mask
318  uMaskValue = 0;
319  for ( v = 0; v < nVarsS; v++ )
320  if ( (m >> v) & 1 )
321  uMaskValue |= (1 << pVarsS[v]);
322  assert( (maskS & uMaskValue) == uMaskValue );
323  // check decomposition
324  if ( !Dau_DecCheckSetAny( p, nVars, nVarsF, maskS, uMaskValue, pCof0? pCof0[m] : 0, pCof1? pCof1[m] : 0, pDec? pDec[m] : 0 ) )
325  return 0;
326  }
327  return 1;
328 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dau_DecCheckSetAny
static int Dau_DecCheckSetAny(word *p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word *pCof0, word *pCof1, word *pDec)
Definition: dauNonDsd.c:289
assert
#define assert(ex)
Definition: util_old.h:213
static unsigned Dau_DecCreateSet ( int *  pVarsB,
int  sizeB,
int  maskS 
)
inlinestatic

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

Synopsis [Variable sets.]

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file dauNonDsd.c.

343 {
344  unsigned uSet = 0; int v;
345  for ( v = 0; v < sizeB; v++ )
346  {
347  uSet |= (1 << (pVarsB[v] << 1));
348  if ( (maskS >> v) & 1 )
349  uSet |= (1 << ((pVarsB[v] << 1)+1));
350  }
351  return uSet;
352 }
int Dau_DecDecomposeSet ( word *  pInit,
int  nVars,
unsigned  uSet,
word *  pComp,
word *  pDec,
int *  pPermC,
int *  pPermD,
int *  pnVarsC,
int *  pnVarsD,
int *  pnVarsS 
)

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

Synopsis [Decomposes with the given bound-set.]

Description []

SideEffects []

SeeAlso []

Definition at line 579 of file dauNonDsd.c.

580 {
581  word p[1<<13], Cof[64], Cof0[64], Cof1[64], Decs[64];
582  word * pCof0[64], * pCof1[64], * pDecs[64], MintC, MintD;
583  int V2P[16], P2V[16], pVarsU[16], pVarsS[16], pVarsF[16];
584  int nVarsU = 0, nVarsS = 0, nVarsF = 0;
585  int nWords = Abc_TtWordNum(nVars);
586  int v, d, c, Status, nDecs;
587  assert( nVars <= 16 );
588  for ( v = 0; v < nVars; v++ )
589  V2P[v] = P2V[v] = v;
590  memcpy( p, pInit, sizeof(word) * nWords );
591  // sort variables
592  for ( v = 0; v < nVars; v++ )
593  {
594  int Value = (uSet >> (v<<1)) & 3;
595  if ( Value == 0 )
596  pVarsF[nVarsF++] = v;
597  else if ( Value == 1 )
598  pVarsU[nVarsU++] = v;
599  else if ( Value == 3 )
600  pVarsS[nVarsS++] = v;
601  else assert(0);
602  }
603  assert( nVarsS >= 0 && nVarsS <= 6 );
604  assert( nVarsF + nVarsS + 1 <= 6 );
605  assert( nVarsU + nVarsS <= 6 );
606  // init space for decomposition functions
607  nDecs = (1 << nVarsS);
608  for ( d = 0; d < nDecs; d++ )
609  {
610  pCof0[d] = Cof0 + d;
611  pCof1[d] = Cof1 + d;
612  pDecs[d] = Decs + d;
613  }
614  // permute variables
615  c = 0;
616  for ( v = 0; v < nVarsF; v++ )
617  Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsF[v], c++ );
618  for ( v = 0; v < nVarsS; v++ )
619  Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsS[v], c++ );
620  for ( v = 0; v < nVarsU; v++ )
621  Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsU[v], c++ );
622  assert( c == nVars );
623  // check decomposition
624  Status = Dau_DecCheckSetTopOld( p, nVars, nVarsF, nVarsS+nVarsU, nVarsS, Abc_InfoMask(nVarsS), pCof0, pCof1, pDecs );
625  if ( !Status )
626  return 0;
627  // compute cofactors
628  assert( nVarsF + nVarsS < 6 );
629  for ( d = 0; d < nDecs; d++ )
630  {
631  Cof[d] = (pCof1[d][0] & s_Truths6[nVarsF + nVarsS]) | (pCof0[d][0] & ~s_Truths6[nVarsF + nVarsS]);
632  pDecs[d][0] = Abc_Tt6Stretch( pDecs[d][0], nVarsU );
633  }
634  // compute the resulting functions
635  pComp[0] = 0;
636  pDec[0] = 0;
637  for ( d = 0; d < nDecs; d++ )
638  {
639  // compute minterms for composition/decomposition function
640  MintC = MintD = ~((word)0);
641  for ( v = 0; v < nVarsS; v++ )
642  {
643  MintC &= ((d >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
644  MintD &= ((d >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
645  }
646  // derive functions
647  pComp[0] |= MintC & Cof[d];
648  pDec[0] |= MintD & pDecs[d][0];
649  }
650  // derive variable permutations
651  if ( pPermC )
652  {
653  for ( v = 0; v < nVarsF; v++ )
654  pPermC[v] = pVarsF[v];
655  for ( v = 0; v < nVarsS; v++ )
656  pPermC[nVarsF+v] = pVarsS[v];
657  pPermC[nVarsF + nVarsS] = nVars;
658  }
659  if ( pPermD )
660  {
661  for ( v = 0; v < nVarsU; v++ )
662  pPermD[v] = pVarsU[v];
663  for ( v = 0; v < nVarsS; v++ )
664  pPermD[nVarsU+v] = pVarsS[v];
665  }
666  if ( pnVarsC )
667  *pnVarsC = nVarsF + nVarsS + 1;
668  if ( pnVarsD )
669  *pnVarsD = nVarsU + nVarsS;
670  if ( pnVarsS )
671  *pnVarsS = nVarsS;
672  return 1;
673 }
Abc_InfoMask
static unsigned Abc_InfoMask(int nVar)
Definition: abc_global.h:261
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dau_DecCheckSetTopOld
int Dau_DecCheckSetTopOld(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word **pCof0, word **pCof1, word **pDec)
Definition: dauNonDsd.c:297
memcpy
char * memcpy()
nWords
int nWords
Definition: abcNpn.c:127
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
assert
#define assert(ex)
Definition: util_old.h:213
Abc_TtMoveVar
static void Abc_TtMoveVar(word *pF, int nVars, int *V2P, int *P2V, int v, int p)
Definition: utilTruth.h:1277
Vec_Int_t* Dau_DecFindSets ( word *  pInit,
int  nVars 
)

Definition at line 516 of file dauNonDsd.c.

517 {
518  Vec_Int_t * vSets;
519  int v, * pSched[16] = {NULL};
520  for ( v = 2; v < nVars; v++ )
521  pSched[v] = Extra_GreyCodeSchedule( v );
522  vSets = Dau_DecFindSets_int( pInit, nVars, pSched );
523  for ( v = 2; v < nVars; v++ )
524  ABC_FREE( pSched[v] );
525  return vSets;
526 }
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition: extraUtilMisc.c:2169
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Dau_DecFindSets_int
Vec_Int_t * Dau_DecFindSets_int(word *pInit, int nVars, int *pSched[16])
Definition: dauNonDsd.c:462
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Vec_Int_t* Dau_DecFindSets_int ( word *  pInit,
int  nVars,
int *  pSched[16] 
)

Definition at line 462 of file dauNonDsd.c.

463 {
464  Vec_Int_t * vSets = Vec_IntAlloc( 32 );
465  int V2P[16], P2V[16], pVarsB[16];
466  int Limit = (1 << nVars);
467  int c, v, sizeB, sizeS, maskB, maskS;
468  unsigned setMixed;
469  word p[1<<10];
470  memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
471  for ( v = 0; v < nVars; v++ )
472  assert( Abc_TtHasVar( p, nVars, v ) );
473  // initialize permutation
474  for ( v = 0; v < nVars; v++ )
475  V2P[v] = P2V[v] = v;
476  // iterate through bound sets of each size in increasing order
477  for ( sizeB = 2; sizeB < nVars; sizeB++ ) // bound set size
478  for ( maskB = 0; maskB < Limit; maskB++ ) // bound set
479  if ( Abc_TtBitCount16(maskB) == sizeB )
480  {
481  // permute variables to have bound set on top
482  Dau_DecMoveFreeToLSB( p, nVars, V2P, P2V, maskB, sizeB );
483  // collect bound set vars on levels nVars-sizeB to nVars-1
484  for ( c = 0; c < sizeB; c++ )
485  pVarsB[c] = P2V[nVars-sizeB+c];
486  // check disjoint
487 // if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, 0, 0, NULL, NULL, NULL) )
488  if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, 0, 0, pSched[sizeB], NULL, NULL) )
489  {
490  Vec_IntPush( vSets, Dau_DecCreateSet(pVarsB, sizeB, 0) );
491  continue;
492  }
493  if ( sizeB == 2 )
494  continue;
495  // iterate through shared sets of each size in the increasing order
496  for ( sizeS = 1; sizeS <= sizeB - 2; sizeS++ ) // shared set size
497  if ( sizeS <= 3 )
498 // sizeS = 1;
499  for ( maskS = 0; maskS < (1 << sizeB); maskS++ ) // shared set
500  if ( Abc_TtBitCount16(maskS) == sizeS )
501  {
502  setMixed = Dau_DecCreateSet( pVarsB, sizeB, maskS );
503 // printf( "Considering %10d ", setMixed );
504 // Dau_DecPrintSet( setMixed, nVars );
505  // check if it exists
506  if ( Dau_DecSetIsContained(vSets, setMixed) )
507  continue;
508  // check if it can be added
509 // if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, NULL, NULL, NULL) )
510  if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, pSched[sizeB], NULL, NULL) )
511  Vec_IntPush( vSets, setMixed );
512  }
513  }
514  return vSets;
515 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
memcpy
char * memcpy()
Abc_TtBitCount16
static int Abc_TtBitCount16(int i)
Definition: utilTruth.h:127
Dau_DecCreateSet
static unsigned Dau_DecCreateSet(int *pVarsB, int sizeB, int maskS)
Definition: dauNonDsd.c:342
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_TtHasVar
static int Abc_TtHasVar(word *t, int nVars, int iVar)
Definition: utilTruth.h:953
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Dau_DecSetIsContained
static int Dau_DecSetIsContained(Vec_Int_t *vSets, unsigned New)
Definition: dauNonDsd.c:357
Dau_DecCheckSetTop
static int Dau_DecCheckSetTop(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
Definition: dauNonDsd.c:181
assert
#define assert(ex)
Definition: util_old.h:213
Dau_DecMoveFreeToLSB
void Dau_DecMoveFreeToLSB(word *p, int nVars, int *V2P, int *P2V, int maskB, int sizeB)
Definition: dauNonDsd.c:454
void Dau_DecFindSetsTest ( )

Definition at line 877 of file dauNonDsd.c.

878 {
879  int nVars = 6;
880 // word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
881 // word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
882 // word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
883 // word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
884 // word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
885 // word t = ABC_CONST(0x00000000901FFFFF); // some funct
886  word t = ABC_CONST(0x000030F00D0D3FFF); // some funct
887 // word t = ABC_CONST(0x00000000690006FF); // some funct
888 // word t = ABC_CONST(0x7000F80007FF0FFF); // some funct
889 // word t = ABC_CONST(0x4133CB334133CB33); // some funct 5 var
890 // word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
891 // word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
892 // word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
893  Dau_DecTrySets( &t, nVars, 1 );
894 }
Dau_DecTrySets
void Dau_DecTrySets(word *pInit, int nVars, int fVerbose)
Definition: dauNonDsd.c:831
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
void Dau_DecFindSetsTest2 ( )

Definition at line 527 of file dauNonDsd.c.

528 {
529  Vec_Int_t * vSets;
530  word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
531  word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
532  word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
533 // word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
534 // word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
535 // word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
536 // word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
537 // word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
538  int nVars = 5;
539 
540  vSets = Dau_DecFindSets( &t, nVars );
541  Dau_DecPrintSets( vSets, nVars );
542  Vec_IntFree( vSets );
543 }
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
a1
#define a1
Definition: extraBdd.h:80
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Dau_DecPrintSets
void Dau_DecPrintSets(Vec_Int_t *vSets, int nVars)
Definition: dauNonDsd.c:434
Dau_DecFindSets
Vec_Int_t * Dau_DecFindSets(word *pInit, int nVars)
Definition: dauNonDsd.c:516
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
a0
#define a0
Definition: extraBdd.h:79
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void Dau_DecFindSetsTest3 ( )

Definition at line 863 of file dauNonDsd.c.

864 {
865  word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
866  word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
867  word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
868 // word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
869  int nVars = 6;
870  char * pStr = "Bcd";
871 // char * pStr = "Abcd";
872 // char * pStr = "ab";
873  unsigned uSet = Dau_DecReadSet( pStr );
874  Dau_DecPerform6( &t, nVars, uSet );
875 }
a1
#define a1
Definition: extraBdd.h:80
Dau_DecPerform6
int Dau_DecPerform6(word *p, int nVars, unsigned uSet)
Definition: dauNonDsd.c:714
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
a0
#define a0
Definition: extraBdd.h:79
Dau_DecReadSet
unsigned Dau_DecReadSet(char *pStr)
Definition: dauNonDsd.c:421
static void Dau_DecGetMinterm ( word *  p,
int  g,
int  nVarsS,
int  uMaskAll 
)
inlinestatic

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

Synopsis [Checks decomposability with given BS variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file dauNonDsd.c.

201 {
202  int m, c, v;
203  for ( m = c = v = 0; v < nVarsS; v++ )
204  if ( !((uMaskAll >> v) & 1) ) // not shared bound set variable
205  {
206  if ( (g >> v) & 1 )
207  m |= (1 << c);
208  c++;
209  }
210  assert( c >= 2 );
211  p[m>>6] |= (((word)1)<<(m & 63));
212 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
assert
#define assert(ex)
Definition: util_old.h:213
void Dau_DecMoveFreeToLSB ( word *  p,
int  nVars,
int *  V2P,
int *  P2V,
int  maskB,
int  sizeB 
)

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

Synopsis [Find decomposable bound-sets of the given function.]

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file dauNonDsd.c.

455 {
456  int v, c = 0;
457  for ( v = 0; v < nVars; v++ )
458  if ( !((maskB >> v) & 1) )
459  Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
460  assert( c == nVars - sizeB );
461 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
assert
#define assert(ex)
Definition: util_old.h:213
Abc_TtMoveVar
static void Abc_TtMoveVar(word *pF, int nVars, int *V2P, int *P2V, int v, int p)
Definition: utilTruth.h:1277
int Dau_DecPerform ( word *  pInit,
int  nVars,
unsigned  uSet 
)

Definition at line 771 of file dauNonDsd.c.

772 {
773  word p[1<<10], pDec[1<<10], pComp[1<<10]; // at most 2^10 words
774  char pDsdC[5000], pDsdD[5000]; // at most 2^12 hex digits
775  int nVarsU, nVarsS, nVarsF, nVarsC = 0, nVarsD = 0;
776  int V2P[16], P2V[16], pPermC[16], pPermD[16], * pSched;
777  int v, i, status, ResC, ResD;
778  int nWords = Abc_TtWordNum(nVars);
779  assert( nVars <= 16 );
780  // backup the function
781  memcpy( p, pInit, sizeof(word) * nWords );
782  // get variable numbers
783  Dau_DecSortSet( uSet, nVars, &nVarsU, &nVarsS, &nVarsF );
784  // permute function and order variables
785  for ( v = 0; v < nVars; v++ )
786  V2P[v] = P2V[v] = v;
787  for ( i = v = 0; v < nVars; v++ )
788  if ( ((uSet >> (v<<1)) & 3) == 0 ) // free first
789  Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v;
790  for ( v = 0; v < nVars; v++ )
791  if ( ((uSet >> (v<<1)) & 3) == 3 ) // share second
792  Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v;
793  pPermC[nVarsC++] = nVars;
794  for ( v = 0; v < nVars; v++ )
795  if ( ((uSet >> (v<<1)) & 3) == 1 ) // unique last
796  Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermD[nVarsD++] = v;
797  for ( v = 0; v < nVarsS; v++ )
798  pPermD[nVarsD++] = pPermC[nVarsF+v];
799  assert( nVarsD == nVarsU + nVarsS );
800  assert( nVarsC == nVarsF + nVarsS + 1 );
801  assert( i == nVars );
802  // decompose
803  pSched = Extra_GreyCodeSchedule( nVarsU + nVarsS );
804  memset( pDec, 0, sizeof(word) * Abc_TtWordNum(nVarsD) );
805  memset( pComp, 0, sizeof(word) * Abc_TtWordNum(nVarsC) );
806  status = Dau_DecCheckSetTop( p, nVars, nVarsF, nVarsU + nVarsS, nVarsS, nVarsS ? Abc_InfoMask(nVarsS) : 0, pSched, pDec, pComp );
807  ABC_FREE( pSched );
808  if ( !status )
809  {
810  printf( " Decomposition does not exist\n" );
811  return 0;
812  }
813 // Dau_DsdPrintFromTruth( stdout, pC, nVars+1 ); //printf( "\n" );
814 // Dau_DsdPrintFromTruth( stdout, pD, nVars ); //printf( "\n" );
815 // Kit_DsdPrintFromTruth( (unsigned *)pComp, 6 ); printf( "\n" );
816 // Kit_DsdPrintFromTruth( (unsigned *)pDec, 6 ); printf( "\n" );
817  // decompose
818  ResC = Dau_DsdDecompose( pComp, nVarsC, 0, 1, pDsdC );
819  ResD = Dau_DsdDecompose( pDec, nVarsD, 0, 1, pDsdD );
820  // replace variables
821  Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
822  Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
823  // report
824  printf( " " );
825  printf( "%3d : ", 0 );
826  printf( "%24s ", pDsdD );
827  printf( "%24s ", pDsdC );
828  Dau_DecVerify( pInit, nVars, pDsdC, pDsdD );
829  return 1;
830 }
memset
char * memset()
Abc_InfoMask
static unsigned Abc_InfoMask(int nVar)
Definition: abc_global.h:261
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition: extraUtilMisc.c:2169
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
memcpy
char * memcpy()
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition: dauDsd.c:1912
nWords
int nWords
Definition: abcNpn.c:127
Dau_DecSortSet
void Dau_DecSortSet(unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
Definition: dauNonDsd.c:371
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Dau_DecVerify
int Dau_DecVerify(word *pInit, int nVars, char *pDsdC, char *pDsdD)
Definition: dauNonDsd.c:687
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Dau_DecCheckSetTop
static int Dau_DecCheckSetTop(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
Definition: dauNonDsd.c:181
assert
#define assert(ex)
Definition: util_old.h:213
Abc_TtMoveVar
static void Abc_TtMoveVar(word *pF, int nVars, int *V2P, int *P2V, int v, int p)
Definition: utilTruth.h:1277
Dau_DecVarReplace
void Dau_DecVarReplace(char *pStr, int *pPerm, int nVars)
Definition: dauNonDsd.c:557
int Dau_DecPerform6 ( word *  p,
int  nVars,
unsigned  uSet 
)

Definition at line 714 of file dauNonDsd.c.

715 {
716  word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD;
717  char pDsdC[1000], pDsdD[1000];
718  int pPermC[16], pPermD[16];
719  int nVarsC, nVarsD, nVarsS, nVarsU, nVarsF, nPairs;
720  int i, m, v, status, ResC, ResD, Counter = 0;
721  status = Dau_DecDecomposeSet( p, nVars, uSet, &tComp, &tDec0, pPermC, pPermD, &nVarsC, &nVarsD, &nVarsS );
722  if ( !status )
723  {
724  printf( " Decomposition does not exist\n" );
725  return 0;
726  }
727  nVarsU = nVarsD - nVarsS;
728  nVarsF = nVarsC - nVarsS - 1;
729  tComp0 = Abc_Tt6Cofactor0( tComp, nVarsF + nVarsS );
730  tComp1 = Abc_Tt6Cofactor1( tComp, nVarsF + nVarsS );
731  nPairs = 1 << (1 << nVarsS);
732  for ( i = 0; i < nPairs; i++ )
733  {
734  if ( i & 1 )
735  continue;
736  // create miterms with this polarity
737  FuncC = FuncD = 0;
738  for ( m = 0; m < (1 << nVarsS); m++ )
739  {
740  word MintC, MintD;
741  if ( !((i >> m) & 1) )
742  continue;
743  MintC = MintD = ~(word)0;
744  for ( v = 0; v < nVarsS; v++ )
745  {
746  MintC &= ((m >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
747  MintD &= ((m >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
748  }
749  FuncC |= MintC;
750  FuncD |= MintD;
751  }
752  // uncomplement given variables
753  tComp = (~s_Truths6[nVarsF + nVarsS] & ((tComp0 & ~FuncC) | (tComp1 & FuncC))) | (s_Truths6[nVarsF + nVarsS] & ((tComp1 & ~FuncC) | (tComp0 & FuncC)));
754  tDec = tDec0 ^ FuncD;
755  // decompose
756  ResC = Dau_DsdDecompose( &tComp, nVarsC, 0, 1, pDsdC );
757  ResD = Dau_DsdDecompose( &tDec, nVarsD, 0, 1, pDsdD );
758  // replace variables
759  Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
760  Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
761  // report
762 // printf( " " );
763  printf( "%3d : ", Counter++ );
764  printf( "%24s ", pDsdD );
765  printf( "%24s ", pDsdC );
766  Dau_DecVerify( p, nVars, pDsdC, pDsdD );
767  }
768  return 1;
769 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Dau_DecDecomposeSet
int Dau_DecDecomposeSet(word *pInit, int nVars, unsigned uSet, word *pComp, word *pDec, int *pPermC, int *pPermD, int *pnVarsC, int *pnVarsD, int *pnVarsS)
Definition: dauNonDsd.c:579
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition: dauDsd.c:1912
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Dau_DecVerify
int Dau_DecVerify(word *pInit, int nVars, char *pDsdC, char *pDsdD)
Definition: dauNonDsd.c:687
Counter
static int Counter
Definition: extraBddMisc.c:1877
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Dau_DecVarReplace
void Dau_DecVarReplace(char *pStr, int *pPerm, int nVars)
Definition: dauNonDsd.c:557
void Dau_DecPrintSet ( unsigned  set,
int  nVars,
int  fNewLine 
)

Definition at line 390 of file dauNonDsd.c.

391 {
392  int v, Counter = 0;
393  int nUnique = 0, nShared = 0, nFree = 0;
394  Dau_DecSortSet( set, nVars, &nUnique, &nShared, &nFree );
395  printf( "S =%2d D =%2d C =%2d ", nShared, nUnique+nShared, nShared+nFree+1 );
396 
397  printf( "x=" );
398  for ( v = 0; v < nVars; v++ )
399  {
400  int Value = ((set >> (v << 1)) & 3);
401  if ( Value == 1 )
402  printf( "%c", 'a' + v ), Counter++;
403  else if ( Value == 3 )
404  printf( "%c", 'A' + v ), Counter++;
405  else assert( Value == 0 );
406  }
407  printf( " y=x" );
408  for ( v = 0; v < nVars; v++ )
409  {
410  int Value = ((set >> (v << 1)) & 3);
411  if ( Value == 0 )
412  printf( "%c", 'a' + v ), Counter++;
413  else if ( Value == 3 )
414  printf( "%c", 'A' + v ), Counter++;
415  }
416  for ( ; Counter < 15; Counter++ )
417  printf( " " );
418  if ( fNewLine )
419  printf( "\n" );
420 }
Dau_DecSortSet
void Dau_DecSortSet(unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
Definition: dauNonDsd.c:371
Counter
static int Counter
Definition: extraBddMisc.c:1877
assert
#define assert(ex)
Definition: util_old.h:213
void Dau_DecPrintSets ( Vec_Int_t *  vSets,
int  nVars 
)

Definition at line 434 of file dauNonDsd.c.

435 {
436  int i, Entry;
437  printf( "The %d-variable set family contains %d sets:\n", nVars, Vec_IntSize(vSets) );
438  Vec_IntForEachEntry( vSets, Entry, i )
439  Dau_DecPrintSet( (unsigned)Entry, nVars, 1 );
440  printf( "\n" );
441 }
Dau_DecPrintSet
void Dau_DecPrintSet(unsigned set, int nVars, int fNewLine)
Definition: dauNonDsd.c:390
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
unsigned Dau_DecReadSet ( char *  pStr)

Definition at line 421 of file dauNonDsd.c.

422 {
423  unsigned uSet = 0; int v;
424  for ( v = 0; pStr[v]; v++ )
425  {
426  if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
427  uSet |= (1 << ((pStr[v] - 'a') << 1));
428  else if ( pStr[v] >= 'A' && pStr[v] <= 'Z' )
429  uSet |= (1 << ((pStr[v] - 'a') << 1)) | (1 << (((pStr[v] - 'a') << 1)+1));
430  else break;
431  }
432  return uSet;
433 }
static int Dau_DecSetHas01 ( unsigned  Mask)
inlinestatic

Definition at line 353 of file dauNonDsd.c.

354 {
355  return (Mask & ((~Mask) >> 1) & 0x55555555);
356 }
static int Dau_DecSetIsContained ( Vec_Int_t *  vSets,
unsigned  New 
)
inlinestatic

Definition at line 357 of file dauNonDsd.c.

360 {
361  unsigned Old;
362  int i, Entry;
363  Vec_IntForEachEntry( vSets, Entry, i )
364  {
365  Old = (unsigned)Entry;
366  if ( (Old & ~New) == 0 && !Dau_DecSetHas01(~Old & New))
367  return 1;
368  }
369  return 0;
370 }
Dau_DecSetHas01
static int Dau_DecSetHas01(unsigned Mask)
Definition: dauNonDsd.c:353
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Dau_DecSortSet ( unsigned  set,
int  nVars,
int *  pnUnique,
int *  pnShared,
int *  pnFree 
)

Definition at line 371 of file dauNonDsd.c.

372 {
373  int v;
374  int nUnique = 0, nShared = 0, nFree = 0;
375  for ( v = 0; v < nVars; v++ )
376  {
377  int Value = ((set >> (v << 1)) & 3);
378  if ( Value == 1 )
379  nUnique++;
380  else if ( Value == 3 )
381  nShared++;
382  else if ( Value == 0 )
383  nFree++;
384  else assert( 0 );
385  }
386  *pnUnique = nUnique;
387  *pnShared = nShared;
388  *pnFree = nFree;
389 }
assert
#define assert(ex)
Definition: util_old.h:213
void Dau_DecTrySets ( word *  pInit,
int  nVars,
int  fVerbose 
)

Definition at line 831 of file dauNonDsd.c.

832 {
833  Vec_Int_t * vSets;
834  int i, Entry;
835  assert( nVars <= 16 );
836  vSets = Dau_DecFindSets( pInit, nVars );
837  if ( !fVerbose )
838  {
839  Vec_IntFree( vSets );
840  return;
841  }
842  Dau_DsdPrintFromTruth( pInit, nVars );
843  printf( "This %d-variable function has %d decomposable variable sets:\n", nVars, Vec_IntSize(vSets) );
844  Vec_IntForEachEntry( vSets, Entry, i )
845  {
846  unsigned uSet = (unsigned)Entry;
847  printf( "Set %4d : ", i );
848  if ( nVars > 6 )
849  {
850  Dau_DecPrintSet( uSet, nVars, 0 );
851  Dau_DecPerform( pInit, nVars, uSet );
852  }
853  else
854  {
855  Dau_DecPrintSet( uSet, nVars, 1 );
856  Dau_DecPerform6( pInit, nVars, uSet );
857  }
858  }
859  Vec_IntFree( vSets );
860 // printf( "\n" );
861 }
Dau_DecPrintSet
void Dau_DecPrintSet(unsigned set, int nVars, int fNewLine)
Definition: dauNonDsd.c:390
Dau_DecPerform
int Dau_DecPerform(word *pInit, int nVars, unsigned uSet)
Definition: dauNonDsd.c:771
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition: dauDsd.c:1968
Dau_DecPerform6
int Dau_DecPerform6(word *p, int nVars, unsigned uSet)
Definition: dauNonDsd.c:714
Dau_DecFindSets
Vec_Int_t * Dau_DecFindSets(word *pInit, int nVars)
Definition: dauNonDsd.c:516
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Dau_DecVarReplace ( char *  pStr,
int *  pPerm,
int  nVars 
)

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

Synopsis [Replaces variables in the string.]

Description []

SideEffects []

SeeAlso []

Definition at line 557 of file dauNonDsd.c.

558 {
559  int v;
560  for ( v = 0; pStr[v]; v++ )
561  if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
562  {
563  assert( pStr[v] - 'a' < nVars );
564  pStr[v] = 'a' + pPerm[pStr[v] - 'a'];
565  }
566 }
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
assert
#define assert(ex)
Definition: util_old.h:213
int Dau_DecVerify ( word *  pInit,
int  nVars,
char *  pDsdC,
char *  pDsdD 
)

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

Synopsis [Testing procedures.]

Description []

SideEffects []

SeeAlso []

Definition at line 687 of file dauNonDsd.c.

688 {
689  word pC[1<<13], pD[1<<13], pRes[1<<13]; // max = 16
690  int nWordsC = Abc_TtWordNum(nVars+1);
691  int nWordsD = Abc_TtWordNum(nVars);
692  assert( nVars < 16 );
693  memcpy( pC, Dau_DsdToTruth(pDsdC, nVars+1), sizeof(word) * nWordsC );
694  memcpy( pD, Dau_DsdToTruth(pDsdD, nVars), sizeof(word) * nWordsD );
695  if ( nVars >= 6 )
696  {
697  assert( nWordsD >= 1 );
698  assert( nWordsC > 1 );
699  Abc_TtMux( pRes, pD, pC + nWordsD, pC, nWordsD );
700  }
701  else
702  {
703  word pC0 = Abc_Tt6Stretch( pC[0], nVars );
704  word pC1 = Abc_Tt6Stretch( (pC[0] >> (1 << nVars)), nVars );
705  Abc_TtMux( pRes, pD, &pC1, &pC0, nWordsD );
706  }
707  if ( !Abc_TtEqual(pInit, pRes, nWordsD) )
708  printf( " Verification failed" );
709 // else
710 // printf( " Verification successful" );
711  printf( "\n" );
712  return 1;
713 }
memcpy
char * memcpy()
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition: dauDsd.c:609
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Abc_TtMux
static void Abc_TtMux(word *pOut, word *pCtrl, word *pIn1, word *pIn0, int nWords)
Definition: utilTruth.h:263
Abc_TtEqual
static int Abc_TtEqual(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:269
assert
#define assert(ex)
Definition: util_old.h:213