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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Saig_ManStatesAreEqual (sat_solver *pSat, Vec_Int_t *vState, int nRegs, int i, int k)
 DECLARATIONS ///. More...
 
int Saig_ManAddUniqueness (sat_solver *pSat, Vec_Int_t *vState, int nRegs, int i, int k, int *pnSatVarNum, int *pnClauses, int fVerbose)
 
int Saig_ManInduction (Aig_Man_t *p, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose)
 

Function Documentation

int Saig_ManAddUniqueness ( sat_solver pSat,
Vec_Int_t vState,
int  nRegs,
int  i,
int  k,
int *  pnSatVarNum,
int *  pnClauses,
int  fVerbose 
)

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

Synopsis [Add uniqueness constraint.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file saigInd.c.

92 {
93  int * pStateI = (int *)Vec_IntArray(vState) + nRegs * i;
94  int * pStateK = (int *)Vec_IntArray(vState) + nRegs * k;
95  int v, iVars, nSatVarsOld, RetValue, * pClause;
96  assert( i && k && i < k );
97  assert( nRegs * k <= Vec_IntSize(vState) );
98  // check if the states are available
99  for ( v = 0; v < nRegs; v++ )
100  if ( pStateI[v] >= 0 && pStateK[v] == -1 )
101  {
102  if ( fVerbose )
103  printf( "Cannot constrain an incomplete state.\n" );
104  return 0;
105  }
106  // add XORs
107  nSatVarsOld = *pnSatVarNum;
108  for ( v = 0; v < nRegs; v++ )
109  if ( pStateI[v] >= 0 )
110  {
111  *pnClauses += 4;
112  RetValue = Cnf_DataAddXorClause( pSat, pStateI[v], pStateK[v], (*pnSatVarNum)++ );
113  if ( RetValue == 0 )
114  {
115  if ( fVerbose )
116  printf( "SAT solver became UNSAT after adding a uniqueness constraint.\n" );
117  return 1;
118  }
119  }
120  // add OR clause
121  (*pnClauses)++;
122  iVars = 0;
123  pClause = ABC_ALLOC( int, nRegs );
124  for ( v = nSatVarsOld; v < *pnSatVarNum; v++ )
125  pClause[iVars++] = toLitCond( v, 0 );
126  assert( iVars <= nRegs );
127  RetValue = sat_solver_addclause( pSat, pClause, pClause + iVars );
128  ABC_FREE( pClause );
129  if ( RetValue == 0 )
130  {
131  if ( fVerbose )
132  printf( "SAT solver became UNSAT after adding a uniqueness constraint.\n" );
133  return 1;
134  }
135  return 0;
136 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static lit toLitCond(int v, int c)
Definition: satVec.h:143
int Cnf_DataAddXorClause(void *pSat, int iVarA, int iVarB, int iVarC)
Definition: cnfMan.c:688
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define assert(ex)
Definition: util_old.h:213
int Saig_ManInduction ( Aig_Man_t p,
int  nTimeOut,
int  nFramesMax,
int  nConfMax,
int  fUnique,
int  fUniqueAll,
int  fGetCex,
int  fVerbose,
int  fVeryVerbose 
)

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

Synopsis [Performs induction by unrolling timeframes backward.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file saigInd.c.

150 {
151  sat_solver * pSat;
152  Aig_Man_t * pAigPart = NULL;
153  Cnf_Dat_t * pCnfPart = NULL;
154  Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL;
155  Vec_Ptr_t * vTop, * vBot;
156  Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
157  int i, k, f, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
158  int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
159  abctime clk, nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock() : 0;
160  assert( fUnique == 0 || fUniqueAll == 0 );
161  assert( Saig_ManPoNum(p) == 1 );
162  Aig_ManSetCioIds( p );
163 
164  // start the top by including the PO
165  vBot = Vec_PtrAlloc( 100 );
166  vTop = Vec_PtrAlloc( 100 );
167  vState = Vec_IntAlloc( 1000 );
168  Vec_PtrPush( vTop, Aig_ManCo(p, 0) );
169  // start the array of CNF variables
170  vTopVarNums = Vec_IntAlloc( 100 );
171  // start the solver
172  pSat = sat_solver_new();
173  sat_solver_setnvars( pSat, 1000 );
174 
175  // set runtime limit
176  if ( nTimeToStop )
177  sat_solver_set_runtime_limit( pSat, nTimeToStop );
178 
179  // iterate backward unrolling
180  RetValue = -1;
181  nSatVarNum = 0;
182  if ( fVerbose )
183  printf( "Induction parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
184  for ( f = 0; ; f++ )
185  {
186  if ( f > 0 )
187  {
188  Aig_ManStop( pAigPart );
189  Cnf_DataFree( pCnfPart );
190  }
191  clk = Abc_Clock();
192  // get the bottom
193  Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
194  // derive AIG for the part between top and bottom
195  pAigPart = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
196  // convert it into CNF
197  pCnfPart = Cnf_Derive( pAigPart, Aig_ManCoNum(pAigPart) );
198  Cnf_DataLift( pCnfPart, nSatVarNum );
199  nSatVarNum += pCnfPart->nVars;
200  nClauses += pCnfPart->nClauses;
201 
202  // remember top frame var IDs
203  if ( fGetCex && vTopVarIds == NULL )
204  {
205  vTopVarIds = Vec_IntStartFull( Aig_ManCiNum(p) );
206  Aig_ManForEachCi( p, pObjPi, i )
207  {
208  if ( pObjPi->pData == NULL )
209  continue;
210  pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
211  assert( Aig_ObjIsCi(pObjPiCopy) );
212  if ( Saig_ObjIsPi(p, pObjPi) )
213  Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
214  else if ( Saig_ObjIsLo(p, pObjPi) )
215  Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
216  else assert( 0 );
217  }
218  }
219 
220  // stitch variables of top and bot
221  assert( Aig_ManCoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) );
222  Aig_ManForEachCo( pAigPart, pObjPo, i )
223  {
224  if ( i == 0 )
225  {
226  // do not perform inductive strengthening
227 // if ( f > 0 )
228 // continue;
229  // add topmost literal
230  Lits[0] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], f>0 );
231  if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
232  assert( 0 );
233  nClauses++;
234  continue;
235  }
236  Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 0 );
237  Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 1 );
238  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
239  assert( 0 );
240  Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 1 );
241  Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 0 );
242  if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
243  assert( 0 );
244  nClauses += 2;
245  }
246  // add CNF to the SAT solver
247  for ( i = 0; i < pCnfPart->nClauses; i++ )
248  if ( !sat_solver_addclause( pSat, pCnfPart->pClauses[i], pCnfPart->pClauses[i+1] ) )
249  break;
250  if ( i < pCnfPart->nClauses )
251  {
252 // printf( "SAT solver became UNSAT after adding clauses.\n" );
253  RetValue = 1;
254  break;
255  }
256 
257  // create new set of POs to derive new top
258  Vec_PtrClear( vTop );
259  Vec_PtrPush( vTop, Aig_ManCo(p, 0) );
260  Vec_IntClear( vTopVarNums );
261  nOldSize = Vec_IntSize(vState);
262  Vec_IntFillExtra( vState, nOldSize + Aig_ManRegNum(p), -1 );
263  Vec_PtrForEachEntry( Aig_Obj_t *, vBot, pObjPi, i )
264  {
265  assert( Aig_ObjIsCi(pObjPi) );
266  if ( Saig_ObjIsLo(p, pObjPi) )
267  {
268  pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
269  assert( pObjPiCopy != NULL );
270  Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObjPi) );
271  Vec_IntPush( vTopVarNums, pCnfPart->pVarNums[pObjPiCopy->Id] );
272 
273  iReg = pObjPi->CioId - Saig_ManPiNum(p);
274  assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
275  Vec_IntWriteEntry( vState, nOldSize+iReg, pCnfPart->pVarNums[pObjPiCopy->Id] );
276  }
277  }
278  assert( Vec_IntSize(vState)%Aig_ManRegNum(p) == 0 );
279  iLast = Vec_IntSize(vState)/Aig_ManRegNum(p);
280  if ( fUniqueAll )
281  {
282  for ( i = 1; i < iLast-1; i++ )
283  {
284  nConstrs++;
285  if ( fVeryVerbose )
286  printf( "Adding constaint for state %2d and state %2d.\n", i, iLast-1 );
287  if ( Saig_ManAddUniqueness( pSat, vState, Aig_ManRegNum(p), i, iLast-1, &nSatVarNum, &nClauses, fVerbose ) )
288  break;
289  }
290  if ( i < iLast-1 )
291  {
292  RetValue = 1;
293  break;
294  }
295  }
296 
297 nextrun:
298  fAdded = 0;
299  // run the SAT solver
300  nConfPrev = pSat->stats.conflicts;
301  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, 0, 0, 0 );
302  if ( fVerbose )
303  {
304  printf( "Frame %4d : PI =%5d. PO =%5d. AIG =%5d. Var =%7d. Clau =%7d. Conf =%7d. ",
305  f, Aig_ManCiNum(pAigPart), Aig_ManCoNum(pAigPart), Aig_ManNodeNum(pAigPart),
306  nSatVarNum, nClauses, (int)pSat->stats.conflicts-nConfPrev );
307  ABC_PRT( "Time", Abc_Clock() - clk );
308  }
309  if ( status == l_Undef )
310  break;
311  if ( status == l_False )
312  {
313  RetValue = 1;
314  break;
315  }
316  assert( status == l_True );
317  // the problem is SAT - add more clauses
318  if ( fVeryVerbose )
319  {
320  Vec_IntForEachEntry( vState, iReg, i )
321  {
322  if ( i && (i % Aig_ManRegNum(p)) == 0 )
323  printf( "\n" );
324  if ( (i % Aig_ManRegNum(p)) == 0 )
325  printf( " State %3d : ", i/Aig_ManRegNum(p) );
326  printf( "%c", (iReg >= 0) ? ('0' + sat_solver_var_value(pSat, iReg)) : 'x' );
327  }
328  printf( "\n" );
329  }
330  if ( nFramesMax && f == nFramesMax - 1 )
331  {
332  // derive counter-example
333  assert( status == l_True );
334  if ( fGetCex )
335  {
336  int VarNum, iBit = 0;
337  Abc_Cex_t * pCex = Abc_CexAlloc( Aig_ManRegNum(p)-1, Saig_ManPiNum(p), 1 );
338  pCex->iFrame = 0;
339  pCex->iPo = 0;
340  Vec_IntForEachEntryStart( vTopVarIds, VarNum, i, 1 )
341  {
342  if ( VarNum >= 0 && sat_solver_var_value( pSat, VarNum ) )
343  Abc_InfoSetBit( pCex->pData, iBit );
344  iBit++;
345  }
346  assert( iBit == pCex->nBits );
347  Abc_CexFree( p->pSeqModel );
348  p->pSeqModel = pCex;
349  }
350  break;
351  }
352  if ( fUnique )
353  {
354  for ( i = 1; i < iLast; i++ )
355  {
356  for ( k = i+1; k < iLast; k++ )
357  {
358  if ( !Saig_ManStatesAreEqual( pSat, vState, Aig_ManRegNum(p), i, k ) )
359  continue;
360  nConstrs++;
361  fAdded = 1;
362  if ( fVeryVerbose )
363  printf( "Adding constaint for state %2d and state %2d.\n", i, k );
364  if ( Saig_ManAddUniqueness( pSat, vState, Aig_ManRegNum(p), i, k, &nSatVarNum, &nClauses, fVerbose ) )
365  break;
366  }
367  if ( k < iLast )
368  break;
369  }
370  if ( i < iLast )
371  {
372  RetValue = 1;
373  break;
374  }
375  }
376  if ( fAdded )
377  goto nextrun;
378  }
379  if ( fVerbose )
380  {
381  if ( nTimeToStop && Abc_Clock() >= nTimeToStop )
382  printf( "Timeout (%d sec) was reached during iteration %d.\n", nTimeOut, f+1 );
383  else if ( status == l_Undef )
384  printf( "Conflict limit (%d) was reached during iteration %d.\n", nConfMax, f+1 );
385  else if ( fUnique || fUniqueAll )
386  printf( "Completed %d interations and added %d uniqueness constraints.\n", f+1, nConstrs );
387  else
388  printf( "Completed %d interations.\n", f+1 );
389  }
390  // cleanup
391  sat_solver_delete( pSat );
392  Aig_ManStop( pAigPart );
393  Cnf_DataFree( pCnfPart );
394  Vec_IntFree( vTopVarNums );
395  Vec_PtrFree( vTop );
396  Vec_PtrFree( vBot );
397  Vec_IntFree( vState );
398  Vec_IntFreeP( &vTopVarIds );
399  return RetValue;
400 }
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
int CioId
Definition: aig.h:73
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
static void Vec_IntFillExtra(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:376
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
#define l_Undef
Definition: SolverTypes.h:86
int nClauses
Definition: cnf.h:61
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
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
void * pData
Definition: aig.h:87
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
void Aig_SupportNodes(Aig_Man_t *p, Aig_Obj_t **ppObjs, int nObjs, Vec_Ptr_t *vSupp)
Definition: aigDfs.c:854
#define l_True
Definition: SolverTypes.h:84
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
stats_t stats
Definition: satSolver.h:156
Definition: cnf.h:56
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int Saig_ManAddUniqueness(sat_solver *pSat, Vec_Int_t *vState, int nRegs, int i, int k, int *pnSatVarNum, int *pnClauses, int fVerbose)
Definition: saigInd.c:91
int ** pClauses
Definition: cnf.h:62
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition: aigUtil.c:965
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
void Cnf_DataLift(Cnf_Dat_t *p, int nVarsPlus)
Definition: cnfMan.c:205
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
ABC_INT64_T conflicts
Definition: satVec.h:154
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define ABC_PRT(a, t)
Definition: abc_global.h:220
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
ABC_NAMESPACE_IMPL_START int Saig_ManStatesAreEqual(sat_solver *pSat, Vec_Int_t *vState, int nRegs, int i, int k)
DECLARATIONS ///.
Definition: saigInd.c:48
#define assert(ex)
Definition: util_old.h:213
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Id
Definition: aig.h:85
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_Man_t * Aig_ManDupSimpleDfsPart(Aig_Man_t *p, Vec_Ptr_t *vPis, Vec_Ptr_t *vCos)
Definition: aigDup.c:240
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
ABC_NAMESPACE_IMPL_START int Saig_ManStatesAreEqual ( sat_solver pSat,
Vec_Int_t vState,
int  nRegs,
int  i,
int  k 
)

DECLARATIONS ///.

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

FileName [saigLoc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [K-step induction for one property only.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Returns 1 if two state are equal.]

Description [Array vState contains indexes of CNF variables for each flop in the first N time frames (0 < i < k, i < N, k < N).]

SideEffects []

SeeAlso []

Definition at line 48 of file saigInd.c.

49 {
50  int * pStateI = (int *)Vec_IntArray(vState) + nRegs * i;
51  int * pStateK = (int *)Vec_IntArray(vState) + nRegs * k;
52  int v;
53  assert( i && k && i < k );
54  assert( nRegs * k <= Vec_IntSize(vState) );
55  // check if the states are available
56  for ( v = 0; v < nRegs; v++ )
57  if ( pStateI[v] >= 0 && pStateK[v] == -1 )
58  return 0;
59 /*
60  printf( "\nchecking uniqueness\n" );
61  printf( "%3d : ", i );
62  for ( v = 0; v < nRegs; v++ )
63  printf( "%d", sat_solver_var_value(pSat, pStateI[v]) );
64  printf( "\n" );
65 
66  printf( "%3d : ", k );
67  for ( v = 0; v < nRegs; v++ )
68  printf( "%d", sat_solver_var_value(pSat, pStateK[v]) );
69  printf( "\n" );
70 */
71  for ( v = 0; v < nRegs; v++ )
72  if ( pStateI[v] >= 0 )
73  {
74  if ( sat_solver_var_value(pSat, pStateI[v]) != sat_solver_var_value(pSat, pStateK[v]) )
75  return 0;
76  }
77  return 1;
78 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213