abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
ifSat.c File Reference
#include "if.h"
#include "sat/bsat/satSolver.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void * If_ManSatBuildXY (int nLutSize)
 DECLARATIONS ///. More...
 
void * If_ManSatBuildXYZ (int nLutSize)
 
void If_ManSatUnbuild (void *p)
 
static word If_ManSat6ComposeLut4 (int t, word f[4], int k)
 
word If_ManSat6Truth (word uBound, word uFree, int *pBSet, int nBSet, int *pSSet, int nSSet, int *pFSet, int nFSet)
 
int If_ManSatCheckXY (void *pSat, int nLutSize, word *pTruth, int nVars, unsigned uSet, word *pTBound, word *pTFree, Vec_Int_t *vLits)
 
unsigned If_ManSatCheckXYall_int (void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
 
unsigned If_ManSatCheckXYall (void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
 
void If_ManSatTest2 ()
 
void If_ManSatTest3 ()
 

Function Documentation

static word If_ManSat6ComposeLut4 ( int  t,
word  f[4],
int  k 
)
static

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

Synopsis [Verification for 6-input function.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file ifSat.c.

103 {
104  int m, v, nMints = (1 << k);
105  word c, r = 0;
106  assert( k <= 4 );
107  for ( m = 0; m < nMints; m++ )
108  {
109  if ( !((t >> m) & 1) )
110  continue;
111  c = ~(word)0;
112  for ( v = 0; v < k; v++ )
113  c &= ((m >> v) & 1) ? f[v] : ~f[v];
114  r |= c;
115  }
116  return r;
117 }
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
assert
#define assert(ex)
Definition: util_old.h:213
word If_ManSat6Truth ( word  uBound,
word  uFree,
int *  pBSet,
int  nBSet,
int *  pSSet,
int  nSSet,
int *  pFSet,
int  nFSet 
)

Definition at line 118 of file ifSat.c.

119 {
120  word r, q, f[4];
121  int i, k = 0;
122  // bound set vars
123  for ( i = 0; i < nSSet; i++ )
124  f[k++] = s_Truths6[pSSet[i]];
125  for ( i = 0; i < nBSet; i++ )
126  f[k++] = s_Truths6[pBSet[i]];
127  q = If_ManSat6ComposeLut4( (int)(uBound & 0xffff), f, k );
128  // free set vars
129  k = 0;
130  f[k++] = q;
131  for ( i = 0; i < nSSet; i++ )
132  f[k++] = s_Truths6[pSSet[i]];
133  for ( i = 0; i < nFSet; i++ )
134  f[k++] = s_Truths6[pFSet[i]];
135  r = If_ManSat6ComposeLut4( (int)(uFree & 0xffff), f, k );
136  return r;
137 }
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
If_ManSat6ComposeLut4
static word If_ManSat6ComposeLut4(int t, word f[4], int k)
Definition: ifSat.c:102
ABC_NAMESPACE_IMPL_START void* If_ManSatBuildXY ( int  nLutSize)

DECLARATIONS ///.

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

FileName [ifSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [FPGA mapping based on priority cuts.]

Synopsis [SAT-based evaluation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 21, 2006.]

Revision [

Id:
ifSat.c,v 1.00 2006/11/21 00:00:00 alanmi Exp

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

Synopsis [Builds SAT instance for the given structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ifSat.c.

46 {
47  int nMintsL = (1 << nLutSize);
48  int nMintsF = (1 << (2 * nLutSize - 1));
49  int nVars = 2 * nMintsL + nMintsF;
50  int iVarP0 = 0; // LUT0 parameters (total nMintsL)
51  int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
52  int m,iVarM = 2 * nMintsL; // MUX vars (total nMintsF)
53  sat_solver * p = sat_solver_new();
54  sat_solver_setnvars( p, nVars );
55  for ( m = 0; m < nMintsF; m++ )
56  sat_solver_add_mux( p,
57  iVarP0 + m % nMintsL,
58  iVarP1 + 2 * (m / nMintsL) + 1,
59  iVarP1 + 2 * (m / nMintsL),
60  iVarM + m );
61  return p;
62 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_add_mux
static int sat_solver_add_mux(sat_solver *pSat, int iVarC, int iVarT, int iVarE, int iVarZ)
Definition: satSolver.h:377
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
sat_solver_t
Definition: satSolver.h:91
void* If_ManSatBuildXYZ ( int  nLutSize)

Definition at line 63 of file ifSat.c.

64 {
65  int nMintsL = (1 << nLutSize);
66  int nMintsF = (1 << (3 * nLutSize - 2));
67  int nVars = 3 * nMintsL + nMintsF;
68  int iVarP0 = 0; // LUT0 parameters (total nMintsL)
69  int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
70  int iVarP2 = 2 * nMintsL; // LUT2 parameters (total nMintsL)
71  int m,iVarM = 3 * nMintsL; // MUX vars (total nMintsF)
72  sat_solver * p = sat_solver_new();
73  sat_solver_setnvars( p, nVars );
74  for ( m = 0; m < nMintsF; m++ )
75  sat_solver_add_mux41( p,
76  iVarP0 + m % nMintsL,
77  iVarP1 + (m >> nLutSize) % nMintsL,
78  iVarP2 + 4 * (m >> (2 * nLutSize)) + 0,
79  iVarP2 + 4 * (m >> (2 * nLutSize)) + 1,
80  iVarP2 + 4 * (m >> (2 * nLutSize)) + 2,
81  iVarP2 + 4 * (m >> (2 * nLutSize)) + 3,
82  iVarM + m );
83  return p;
84 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
sat_solver_t
Definition: satSolver.h:91
sat_solver_add_mux41
static int sat_solver_add_mux41(sat_solver *pSat, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3, int iVarZ)
Definition: satSolver.h:423
int If_ManSatCheckXY ( void *  pSat,
int  nLutSize,
word *  pTruth,
int  nVars,
unsigned  uSet,
word *  pTBound,
word *  pTFree,
Vec_Int_t *  vLits 
)

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

Synopsis [Returns config string for the given truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file ifSat.c.

151 {
152  sat_solver * p = (sat_solver *)pSat;
153  int iBSet, nBSet = 0, pBSet[IF_MAX_FUNC_LUTSIZE];
154  int iSSet, nSSet = 0, pSSet[IF_MAX_FUNC_LUTSIZE];
155  int iFSet, nFSet = 0, pFSet[IF_MAX_FUNC_LUTSIZE];
156  int nMintsL = (1 << nLutSize);
157  int nMintsF = (1 << (2 * nLutSize - 1));
158  int v, Value, m, mNew, nMintsFNew, nMintsLNew;
159  word Res;
160  // collect variable sets
161  Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet );
162  assert( nBSet + nSSet + nFSet == nVars );
163  // check variable bounds
164  assert( nSSet + nBSet <= nLutSize );
165  assert( nLutSize + nSSet + nFSet <= 2*nLutSize - 1 );
166  nMintsFNew = (1 << (nLutSize + nSSet + nFSet));
167  // remap minterms
168  Vec_IntFill( vLits, nMintsF, -1 );
169  for ( m = 0; m < (1 << nVars); m++ )
170  {
171  mNew = iBSet = iSSet = iFSet = 0;
172  for ( v = 0; v < nVars; v++ )
173  {
174  Value = ((uSet >> (v << 1)) & 3);
175  if ( Value == 0 ) // FS
176  {
177  if ( ((m >> v) & 1) )
178  mNew |= 1 << (nLutSize + nSSet + iFSet), pFSet[iFSet] = v;
179  iFSet++;
180  }
181  else if ( Value == 1 ) // BS
182  {
183  if ( ((m >> v) & 1) )
184  mNew |= 1 << (nSSet + iBSet), pBSet[iBSet] = v;
185  iBSet++;
186  }
187  else if ( Value == 3 ) // SS
188  {
189  if ( ((m >> v) & 1) )
190  {
191  mNew |= 1 << iSSet;
192  mNew |= 1 << (nLutSize + iSSet);
193  pSSet[iSSet] = v;
194  }
195  iSSet++;
196  }
197  else assert( Value == 0 );
198  }
199  assert( iBSet == nBSet && iFSet == nFSet );
200  assert( Vec_IntEntry(vLits, mNew) == -1 );
201  Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
202  }
203  // find assumptions
204  v = 0;
205  Vec_IntForEachEntry( vLits, Value, m )
206  {
207 // printf( "%d", (Value >= 0) ? Value : 2 );
208  if ( Value >= 0 )
209  Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
210  }
211  Vec_IntShrink( vLits, v );
212 // printf( " %d\n", Vec_IntSize(vLits) );
213  // run SAT solver
214  Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
215  if ( Value != l_True )
216  return 0;
217  if ( pTBound && pTFree )
218  {
219  // collect config
220  assert( nSSet + nBSet <= nLutSize );
221  *pTBound = 0;
222  nMintsLNew = (1 << (nSSet + nBSet));
223  for ( m = 0; m < nMintsLNew; m++ )
224  if ( sat_solver_var_value(p, m) )
225  Abc_TtSetBit( pTBound, m );
226  *pTBound = Abc_Tt6Stretch( *pTBound, nSSet + nBSet );
227  // collect configs
228  assert( nSSet + nFSet + 1 <= nLutSize );
229  *pTFree = 0;
230  nMintsLNew = (1 << (1 + nSSet + nFSet));
231  for ( m = 0; m < nMintsLNew; m++ )
232  if ( sat_solver_var_value(p, nMintsL+m) )
233  Abc_TtSetBit( pTFree, m );
234  *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet );
235  if ( nVars != 6 || nLutSize != 4 )
236  return 1;
237  // verify the result
238  Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet );
239  if ( pTruth[0] != Res )
240  {
241  Dau_DsdPrintFromTruth( pTruth, nVars );
242  Dau_DsdPrintFromTruth( &Res, nVars );
243  Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
244  Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
245  printf( "Verification failed!\n" );
246  }
247  }
248  return 1;
249 }
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_solve
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition: dauDsd.c:1968
l_True
#define l_True
Definition: SolverTypes.h:84
Abc_TtSetBit
static void Abc_TtSetBit(word *p, int i)
Definition: utilTruth.h:150
Abc_TtGetBit
static int Abc_TtGetBit(word *p, int i)
MACRO DEFINITIONS ///.
Definition: utilTruth.h:149
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
If_ManSat6Truth
word If_ManSat6Truth(word uBound, word uFree, int *pBSet, int nBSet, int *pSSet, int nSSet, int *pFSet, int nFSet)
Definition: ifSat.c:118
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
IF_MAX_FUNC_LUTSIZE
#define IF_MAX_FUNC_LUTSIZE
Definition: if.h:54
Dau_DecSortSet
void Dau_DecSortSet(unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
Definition: dauNonDsd.c:371
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
unsigned If_ManSatCheckXYall ( void *  pSat,
int  nLutSize,
word *  pTruth,
int  nVars,
Vec_Int_t *  vLits 
)

Definition at line 476 of file ifSat.c.

477 {
478  unsigned uSet = If_ManSatCheckXYall_int( pSat, nLutSize, pTruth, nVars, vLits );
479 // Dau_DecPrintSet( uSet, nVars, 1 );
480  return uSet;
481 }
If_ManSatCheckXYall_int
unsigned If_ManSatCheckXYall_int(void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
Definition: ifSat.c:262
unsigned If_ManSatCheckXYall_int ( void *  pSat,
int  nLutSize,
word *  pTruth,
int  nVars,
Vec_Int_t *  vLits 
)

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

Synopsis [Returns config string for the given truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file ifSat.c.

263 {
264  unsigned uSet = 0;
265  int nTotal = 2 * nLutSize - 1;
266  int nShared = nTotal - nVars;
267  int i[6], s[4];
268  assert( nLutSize >= 2 && nLutSize <= 6 );
269  assert( nLutSize < nVars && nVars <= nTotal );
270  assert( nShared >= 0 && nShared < nLutSize - 1 );
271  if ( nLutSize == 2 )
272  {
273  assert( nShared == 0 );
274  for ( i[0] = 0; i[0] < nVars; i[0]++ )
275  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
276  {
277  uSet = (1 << (2*i[0])) | (1 << (2*i[1]));
278  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
279  return uSet;
280  }
281  }
282  else if ( nLutSize == 3 )
283  {
284  for ( i[0] = 0; i[0] < nVars; i[0]++ )
285  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
286  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
287  {
288  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
289  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
290  return uSet;
291  }
292  if ( nShared < 1 )
293  return 0;
294  for ( i[0] = 0; i[0] < nVars; i[0]++ )
295  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
296  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
297  {
298  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2]));
299  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
300  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
301  return uSet | (3 << (2*i[s[0]]));
302  }
303  }
304  else if ( nLutSize == 4 )
305  {
306  for ( i[0] = 0; i[0] < nVars; i[0]++ )
307  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
308  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
309  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
310  {
311  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
312  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
313  return uSet;
314  }
315  if ( nShared < 1 )
316  return 0;
317  for ( i[0] = 0; i[0] < nVars; i[0]++ )
318  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
319  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
320  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
321  {
322  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
323  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
324  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
325  return uSet | (3 << (2*i[s[0]]));
326  }
327  if ( nShared < 2 )
328  return 0;
329  for ( i[0] = 0; i[0] < nVars; i[0]++ )
330  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
331  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
332  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
333  {
334  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3]));
335  {
336  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
337  for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
338  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
339  return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
340  }
341  }
342  }
343  else if ( nLutSize == 5 )
344  {
345  for ( i[0] = 0; i[0] < nVars; i[0]++ )
346  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
347  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
348  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
349  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
350  {
351  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
352  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
353  return uSet;
354  }
355  if ( nShared < 1 )
356  return 0;
357  for ( i[0] = 0; i[0] < nVars; i[0]++ )
358  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
359  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
360  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
361  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
362  {
363  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
364  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
365  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
366  return uSet | (3 << (2*i[s[0]]));
367  }
368  if ( nShared < 2 )
369  return 0;
370  for ( i[0] = 0; i[0] < nVars; i[0]++ )
371  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
372  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
373  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
374  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
375  {
376  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
377  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
378  for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
379  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
380  return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
381  }
382  if ( nShared < 3 )
383  return 0;
384  for ( i[0] = 0; i[0] < nVars; i[0]++ )
385  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
386  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
387  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
388  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
389  {
390  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
391  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
392  for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
393  for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
394  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
395  return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
396  }
397  }
398  else if ( nLutSize == 6 )
399  {
400  for ( i[0] = 0; i[0] < nVars; i[0]++ )
401  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
402  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
403  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
404  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
405  for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
406  {
407  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
408  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet, NULL, NULL, vLits) )
409  return uSet;
410  }
411  if ( nShared < 1 )
412  return 0;
413  for ( i[0] = 0; i[0] < nVars; i[0]++ )
414  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
415  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
416  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
417  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
418  for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
419  {
420  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
421  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
422  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])), NULL, NULL, vLits) )
423  return uSet | (3 << (2*i[s[0]]));
424  }
425  if ( nShared < 2 )
426  return 0;
427  for ( i[0] = 0; i[0] < nVars; i[0]++ )
428  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
429  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
430  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
431  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
432  for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
433  {
434  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
435  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
436  for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
437  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])), NULL, NULL, vLits) )
438  return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]]));
439  }
440  if ( nShared < 3 )
441  return 0;
442  for ( i[0] = 0; i[0] < nVars; i[0]++ )
443  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
444  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
445  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
446  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
447  for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
448  {
449  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
450  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
451  for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
452  for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
453  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])), NULL, NULL, vLits) )
454  return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]]));
455  }
456  if ( nShared < 4 )
457  return 0;
458  for ( i[0] = 0; i[0] < nVars; i[0]++ )
459  for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
460  for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
461  for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
462  for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
463  for ( i[5] = i[4]+1; i[5] < nVars; i[5]++ )
464  {
465  uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])) | (1 << (2*i[5]));
466  for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
467  for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
468  for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
469  for ( s[3] = s[1]+1; s[3] < nLutSize; s[3]++ )
470  if ( If_ManSatCheckXY(pSat, nLutSize, pTruth, nVars, uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]])), NULL, NULL, vLits) )
471  return uSet | (3 << (2*i[s[0]])) | (3 << (2*i[s[1]])) | (3 << (2*i[s[2]])) | (3 << (2*i[s[3]]));
472  }
473  }
474  return 0;
475 }
If_ManSatCheckXY
int If_ManSatCheckXY(void *pSat, int nLutSize, word *pTruth, int nVars, unsigned uSet, word *pTBound, word *pTFree, Vec_Int_t *vLits)
Definition: ifSat.c:150
assert
#define assert(ex)
Definition: util_old.h:213
nTotal
int nTotal
DECLARATIONS ///.
Definition: cutTruth.c:37
void If_ManSatTest2 ( )

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

Synopsis [Test procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 494 of file ifSat.c.

495 {
496  int nVars = 6;
497  int nLutSize = 4;
498  sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
499 // char * pDsd = "(abcdefg)";
500 // char * pDsd = "([a!bc]d!e)";
501  char * pDsd = "0123456789ABCDEF{abcdef}";
502  word * pTruth = Dau_DsdToTruth( pDsd, nVars );
503  word uBound, uFree;
504  Vec_Int_t * vLits = Vec_IntAlloc( 100 );
505 // unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
506 // unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
507  unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
508  int RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
509  assert( RetValue );
510 
511 // Abc_TtPrintBinary( pTruth, nVars );
512 // Abc_TtPrintBinary( &uBound, nLutSize );
513 // Abc_TtPrintBinary( &uFree, nLutSize );
514 
515  Dau_DsdPrintFromTruth( pTruth, nVars );
516  Dau_DsdPrintFromTruth( &uBound, nLutSize );
517  Dau_DsdPrintFromTruth( &uFree, nLutSize );
518  sat_solver_delete(p);
519  Vec_IntFree( vLits );
520 }
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
If_ManSatBuildXY
ABC_NAMESPACE_IMPL_START void * If_ManSatBuildXY(int nLutSize)
DECLARATIONS ///.
Definition: ifSat.c:45
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition: dauDsd.c:1968
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition: dauDsd.c:609
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
If_ManSatCheckXY
int If_ManSatCheckXY(void *pSat, int nLutSize, word *pTruth, int nVars, unsigned uSet, word *pTBound, word *pTFree, Vec_Int_t *vLits)
Definition: ifSat.c:150
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void If_ManSatTest3 ( )

Definition at line 521 of file ifSat.c.

522 {
523  int nVars = 6;
524  int nLutSize = 4;
525  sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
526 // char * pDsd = "(abcdefg)";
527 // char * pDsd = "([a!bc]d!e)";
528  char * pDsd = "0123456789ABCDEF{abcdef}";
529  word * pTruth = Dau_DsdToTruth( pDsd, nVars );
530  Vec_Int_t * vLits = Vec_IntAlloc( 100 );
531 // unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
532 // unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
533  unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
534  uSet = If_ManSatCheckXYall( p, nLutSize, pTruth, nVars, vLits );
535  Dau_DecPrintSet( uSet, nVars, 1 );
536 
537  sat_solver_delete(p);
538  Vec_IntFree( vLits );
539 }
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
If_ManSatBuildXY
ABC_NAMESPACE_IMPL_START void * If_ManSatBuildXY(int nLutSize)
DECLARATIONS ///.
Definition: ifSat.c:45
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition: dauDsd.c:609
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
Dau_DecPrintSet
void Dau_DecPrintSet(unsigned set, int nVars, int fNewLine)
Definition: dauNonDsd.c:390
If_ManSatCheckXYall
unsigned If_ManSatCheckXYall(void *pSat, int nLutSize, word *pTruth, int nVars, Vec_Int_t *vLits)
Definition: ifSat.c:476
sat_solver_t
Definition: satSolver.h:91
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void If_ManSatUnbuild ( void *  p)

Definition at line 85 of file ifSat.c.

86 {
87  if ( p )
88  sat_solver_delete( (sat_solver *)p );
89 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
sat_solver_t
Definition: satSolver.h:91