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

Go to the source code of this file.

Macros

#define KIT_ISOP_MEM_LIMIT   (1<<20)
 DECLARATIONS ///. More...
 

Functions

static unsigned * Kit_TruthIsop_rec (unsigned *puOn, unsigned *puOnDc, int nVars, Kit_Sop_t *pcRes, Vec_Int_t *vStore)
 
static unsigned Kit_TruthIsop5_rec (unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t *pcRes, Vec_Int_t *vStore)
 
int Kit_TruthIsop (unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
 FUNCTION DEFINITIONS ///. More...
 
void Kit_TruthIsopPrintCover (Vec_Int_t *vCover, int nVars, int fCompl)
 
void Kit_TruthIsopPrint (unsigned *puTruth, int nVars, Vec_Int_t *vCover, int fTryBoth)
 

Macro Definition Documentation

#define KIT_ISOP_MEM_LIMIT   (1<<20)

DECLARATIONS ///.

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

FileName [kitIsop.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [ISOP computation based on Morreale's algorithm.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 31 of file kitIsop.c.

Function Documentation

int Kit_TruthIsop ( unsigned *  puTruth,
int  nVars,
Vec_Int_t *  vMemory,
int  fTryBoth 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes ISOP from TT.]

Description [Returns the cover in vMemory. Uses the rest of array in vMemory as an intermediate memory storage. Returns the cover with -1 cubes, if the the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of intermediate data).]

SideEffects []

SeeAlso []

Definition at line 55 of file kitIsop.c.

56 {
57  Kit_Sop_t cRes, * pcRes = &cRes;
58  Kit_Sop_t cRes2, * pcRes2 = &cRes2;
59  unsigned * pResult;
60  int RetValue = 0;
61  assert( nVars >= 0 && nVars <= 16 );
62  // if nVars < 5, make sure it does not depend on those vars
63 // for ( i = nVars; i < 5; i++ )
64 // assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
65  // prepare memory manager
66  Vec_IntClear( vMemory );
67  Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
68  // compute ISOP for the direct polarity
69  pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
70  if ( pcRes->nCubes == -1 )
71  {
72  vMemory->nSize = -1;
73  return -1;
74  }
75  assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
76  if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
77  {
78  vMemory->pArray[0] = 0;
79  Vec_IntShrink( vMemory, pcRes->nCubes );
80  return 0;
81  }
82  if ( fTryBoth )
83  {
84  // compute ISOP for the complemented polarity
85  Kit_TruthNot( puTruth, puTruth, nVars );
86  pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
87  if ( pcRes2->nCubes >= 0 )
88  {
89  assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
90  if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) )
91  {
92  RetValue = 1;
93  pcRes = pcRes2;
94  }
95  }
96  Kit_TruthNot( puTruth, puTruth, nVars );
97  }
98 // printf( "%d ", vMemory->nSize );
99  // move the cover representation to the beginning of the memory buffer
100  memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
101  Vec_IntShrink( vMemory, pcRes->nCubes );
102  return RetValue;
103 }
KIT_ISOP_MEM_LIMIT
#define KIT_ISOP_MEM_LIMIT
DECLARATIONS ///.
Definition: kitIsop.c:31
Kit_TruthIsEqual
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
memmove
char * memmove()
Vec_IntGrow
static void Vec_IntGrow(Vec_Int_t *p, int nCapMin)
Definition: bblif.c:336
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Kit_Sop_t
typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_ Kit_Sop_t
INCLUDES ///.
Definition: kit.h:51
Kit_TruthIsop_rec
static unsigned * Kit_TruthIsop_rec(unsigned *puOn, unsigned *puOnDc, int nVars, Kit_Sop_t *pcRes, Vec_Int_t *vStore)
Definition: kitIsop.c:145
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
unsigned Kit_TruthIsop5_rec ( unsigned  uOn,
unsigned  uOnDc,
int  nVars,
Kit_Sop_t *  pcRes,
Vec_Int_t *  vStore 
)
static

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

Synopsis [Computes ISOP for 5 variables or less.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file kitIsop.c.

273 {
274  unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
275  Kit_Sop_t cRes0, cRes1, cRes2;
276  Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
277  unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
278  int i, k, Var;
279  assert( nVars <= 5 );
280  assert( (uOn & ~uOnDc) == 0 );
281  if ( uOn == 0 )
282  {
283  pcRes->nLits = 0;
284  pcRes->nCubes = 0;
285  pcRes->pCubes = NULL;
286  return 0;
287  }
288  if ( uOnDc == 0xFFFFFFFF )
289  {
290  pcRes->nLits = 0;
291  pcRes->nCubes = 1;
292  pcRes->pCubes = Vec_IntFetch( vStore, 1 );
293  if ( pcRes->pCubes == NULL )
294  {
295  pcRes->nCubes = -1;
296  return 0;
297  }
298  pcRes->pCubes[0] = 0;
299  return 0xFFFFFFFF;
300  }
301  assert( nVars > 0 );
302  // find the topmost var
303  for ( Var = nVars-1; Var >= 0; Var-- )
304  if ( Kit_TruthVarInSupport( &uOn, 5, Var ) ||
305  Kit_TruthVarInSupport( &uOnDc, 5, Var ) )
306  break;
307  assert( Var >= 0 );
308  // cofactor
309  uOn0 = uOn1 = uOn;
310  uOnDc0 = uOnDc1 = uOnDc;
311  Kit_TruthCofactor0( &uOn0, Var + 1, Var );
312  Kit_TruthCofactor1( &uOn1, Var + 1, Var );
313  Kit_TruthCofactor0( &uOnDc0, Var + 1, Var );
314  Kit_TruthCofactor1( &uOnDc1, Var + 1, Var );
315  // solve for cofactors
316  uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
317  if ( pcRes0->nCubes == -1 )
318  {
319  pcRes->nCubes = -1;
320  return 0;
321  }
322  uRes1 = Kit_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
323  if ( pcRes1->nCubes == -1 )
324  {
325  pcRes->nCubes = -1;
326  return 0;
327  }
328  uRes2 = Kit_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
329  if ( pcRes2->nCubes == -1 )
330  {
331  pcRes->nCubes = -1;
332  return 0;
333  }
334  // create the resulting cover
335  pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes;
336  pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
337  pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
338  if ( pcRes->pCubes == NULL )
339  {
340  pcRes->nCubes = -1;
341  return 0;
342  }
343  k = 0;
344  for ( i = 0; i < pcRes0->nCubes; i++ )
345  pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
346  for ( i = 0; i < pcRes1->nCubes; i++ )
347  pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
348  for ( i = 0; i < pcRes2->nCubes; i++ )
349  pcRes->pCubes[k++] = pcRes2->pCubes[i];
350  assert( k == pcRes->nCubes );
351  // derive the final truth table
352  uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
353 // assert( (uOn & ~uRes2) == 0 );
354 // assert( (uRes2 & ~uOnDc) == 0 );
355  return uRes2;
356 }
Kit_TruthCofactor0
void Kit_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:368
Kit_TruthIsop5_rec
static unsigned Kit_TruthIsop5_rec(unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t *pcRes, Vec_Int_t *vStore)
Definition: kitIsop.c:272
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
Kit_TruthCofactor1
void Kit_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:470
Kit_Sop_t
typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_ Kit_Sop_t
INCLUDES ///.
Definition: kit.h:51
Minisat::Var
int Var
Definition: SolverTypes.h:42
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:270
assert
#define assert(ex)
Definition: util_old.h:213
unsigned * Kit_TruthIsop_rec ( unsigned *  puOn,
unsigned *  puOnDc,
int  nVars,
Kit_Sop_t *  pcRes,
Vec_Int_t *  vStore 
)
static

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

Synopsis [Computes ISOP 6 variables or more.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file kitIsop.c.

146 {
147  Kit_Sop_t cRes0, cRes1, cRes2;
148  Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
149  unsigned * puRes0, * puRes1, * puRes2;
150  unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
151  int i, k, Var, nWords, nWordsAll;
152 // assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) );
153  // allocate room for the resulting truth table
154  nWordsAll = Kit_TruthWordNum( nVars );
155  pTemp = Vec_IntFetch( vStore, nWordsAll );
156  if ( pTemp == NULL )
157  {
158  pcRes->nCubes = -1;
159  return NULL;
160  }
161  // check for constants
162  if ( Kit_TruthIsConst0( puOn, nVars ) )
163  {
164  pcRes->nLits = 0;
165  pcRes->nCubes = 0;
166  pcRes->pCubes = NULL;
167  Kit_TruthClear( pTemp, nVars );
168  return pTemp;
169  }
170  if ( Kit_TruthIsConst1( puOnDc, nVars ) )
171  {
172  pcRes->nLits = 0;
173  pcRes->nCubes = 1;
174  pcRes->pCubes = Vec_IntFetch( vStore, 1 );
175  if ( pcRes->pCubes == NULL )
176  {
177  pcRes->nCubes = -1;
178  return NULL;
179  }
180  pcRes->pCubes[0] = 0;
181  Kit_TruthFill( pTemp, nVars );
182  return pTemp;
183  }
184  assert( nVars > 0 );
185  // find the topmost var
186  for ( Var = nVars-1; Var >= 0; Var-- )
187  if ( Kit_TruthVarInSupport( puOn, nVars, Var ) ||
188  Kit_TruthVarInSupport( puOnDc, nVars, Var ) )
189  break;
190  assert( Var >= 0 );
191  // consider a simple case when one-word computation can be used
192  if ( Var < 5 )
193  {
194  unsigned uRes = Kit_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
195  for ( i = 0; i < nWordsAll; i++ )
196  pTemp[i] = uRes;
197  return pTemp;
198  }
199  assert( Var >= 5 );
200  nWords = Kit_TruthWordNum( Var );
201  // cofactor
202  puOn0 = puOn; puOn1 = puOn + nWords;
203  puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords;
204  pTemp0 = pTemp; pTemp1 = pTemp + nWords;
205  // solve for cofactors
206  Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
207  puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
208  if ( pcRes0->nCubes == -1 )
209  {
210  pcRes->nCubes = -1;
211  return NULL;
212  }
213  Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
214  puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
215  if ( pcRes1->nCubes == -1 )
216  {
217  pcRes->nCubes = -1;
218  return NULL;
219  }
220  Kit_TruthSharp( pTemp0, puOn0, puRes0, Var );
221  Kit_TruthSharp( pTemp1, puOn1, puRes1, Var );
222  Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var );
223  Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
224  puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
225  if ( pcRes2->nCubes == -1 )
226  {
227  pcRes->nCubes = -1;
228  return NULL;
229  }
230  // create the resulting cover
231  pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes;
232  pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
233  pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
234  if ( pcRes->pCubes == NULL )
235  {
236  pcRes->nCubes = -1;
237  return NULL;
238  }
239  k = 0;
240  for ( i = 0; i < pcRes0->nCubes; i++ )
241  pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
242  for ( i = 0; i < pcRes1->nCubes; i++ )
243  pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
244  for ( i = 0; i < pcRes2->nCubes; i++ )
245  pcRes->pCubes[k++] = pcRes2->pCubes[i];
246  assert( k == pcRes->nCubes );
247  // create the resulting truth table
248  Kit_TruthOr( pTemp0, puRes0, puRes2, Var );
249  Kit_TruthOr( pTemp1, puRes1, puRes2, Var );
250  // copy the table if needed
251  nWords <<= 1;
252  for ( i = 1; i < nWordsAll/nWords; i++ )
253  for ( k = 0; k < nWords; k++ )
254  pTemp[i*nWords + k] = pTemp[k];
255  // verify in the end
256 // assert( Kit_TruthIsImply( puOn, pTemp, nVars ) );
257 // assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) );
258  return pTemp;
259 }
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
Kit_TruthFill
static void Kit_TruthFill(unsigned *pOut, int nVars)
Definition: kit.h:367
Kit_TruthIsop5_rec
static unsigned Kit_TruthIsop5_rec(unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t *pcRes, Vec_Int_t *vStore)
Definition: kitIsop.c:272
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Vec_IntFetch
static unsigned * Vec_IntFetch(Vec_Int_t *p, int nWords)
Definition: vecInt.h:853
nWords
int nWords
Definition: abcNpn.c:127
Kit_TruthAnd
static void Kit_TruthAnd(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:379
Kit_TruthIsConst1
static int Kit_TruthIsConst1(unsigned *pIn, int nVars)
Definition: kit.h:323
Kit_TruthSharp
static void Kit_TruthSharp(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:397
Kit_Sop_t
typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_ Kit_Sop_t
INCLUDES ///.
Definition: kit.h:51
Kit_TruthIsop_rec
static unsigned * Kit_TruthIsop_rec(unsigned *puOn, unsigned *puOnDc, int nVars, Kit_Sop_t *pcRes, Vec_Int_t *vStore)
Definition: kitIsop.c:145
Minisat::Var
int Var
Definition: SolverTypes.h:42
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition: kitTruth.c:270
assert
#define assert(ex)
Definition: util_old.h:213
Kit_TruthClear
static void Kit_TruthClear(unsigned *pOut, int nVars)
Definition: kit.h:361
Kit_TruthOr
static void Kit_TruthOr(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:385
void Kit_TruthIsopPrint ( unsigned *  puTruth,
int  nVars,
Vec_Int_t *  vCover,
int  fTryBoth 
)

Definition at line 128 of file kitIsop.c.

129 {
130  int fCompl = Kit_TruthIsop( puTruth, nVars, vCover, fTryBoth );
131  Kit_TruthIsopPrintCover( vCover, nVars, fCompl );
132 }
Kit_TruthIsopPrintCover
void Kit_TruthIsopPrintCover(Vec_Int_t *vCover, int nVars, int fCompl)
Definition: kitIsop.c:104
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
void Kit_TruthIsopPrintCover ( Vec_Int_t *  vCover,
int  nVars,
int  fCompl 
)

Definition at line 104 of file kitIsop.c.

105 {
106  int i, k, Entry, Literal;
107  if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
108  {
109  printf( "Constant %d\n", Vec_IntSize(vCover) );
110  return;
111  }
112  Vec_IntForEachEntry( vCover, Entry, i )
113  {
114  for ( k = 0; k < nVars; k++ )
115  {
116  Literal = 3 & (Entry >> (k << 1));
117  if ( Literal == 1 ) // neg literal
118  printf( "0" );
119  else if ( Literal == 2 ) // pos literal
120  printf( "1" );
121  else if ( Literal == 0 )
122  printf( "-" );
123  else assert( 0 );
124  }
125  printf( " %d\n", !fCompl );
126  }
127 }
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54