abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
int2Core.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [int2Core.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Interpolation engine.]
8 
9  Synopsis [Core procedures.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - Dec 1, 2013.]
16 
17  Revision [$Id: int2Core.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "int2Int.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [This procedure sets default values of interpolation parameters.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
46 {
47  memset( p, 0, sizeof(Int2_ManPars_t) );
48  p->nBTLimit = 0; // limit on the number of conflicts
49  p->nFramesS = 1; // the starting number timeframes
50  p->nFramesMax = 0; // the max number timeframes to unroll
51  p->nSecLimit = 0; // time limit in seconds
52  p->nFramesK = 1; // the number of timeframes to use in induction
53  p->fRewrite = 0; // use additional rewriting to simplify timeframes
54  p->fTransLoop = 0; // add transition into the init state under new PI var
55  p->fDropInvar = 0; // dump inductive invariant into file
56  p->fVerbose = 0; // print verbose statistics
57  p->iFrameMax = -1;
58 }
59 /**Function*************************************************************
60 
61  Synopsis []
62 
63  Description []
64 
65  SideEffects []
66 
67  SeeAlso []
68 
69 ***********************************************************************/
70 Gia_Man_t * Int2_ManUnroll( Gia_Man_t * p, int nFrames )
71 {
72  Gia_Man_t * pFrames, * pTemp;
73  Gia_Obj_t * pObj;
74  int i, f;
75  assert( Gia_ManRegNum(pAig) > 0 );
76  pFrames = Gia_ManStart( Gia_ManObjNum(pAig) );
77  pFrames->pName = Abc_UtilStrsav( pAig->pName );
78  pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
79  Gia_ManHashAlloc( pFrames );
80  Gia_ManConst0(pAig)->Value = 0;
81  for ( f = 0; f < nFrames; f++ )
82  {
83  Gia_ManForEachRo( pAig, pObj, i )
84  pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0;
85  Gia_ManForEachPi( pAig, pObj, i )
86  pObj->Value = Gia_ManAppendCi( pFrames );
87  Gia_ManForEachAnd( pAig, pObj, i )
88  pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
89  Gia_ManForEachRi( pAig, pObj, i )
90  pObj->Value = Gia_ObjFanin0Copy(pObj);
91  }
92  Gia_ManForEachRi( pAig, pObj, i )
93  Gia_ManAppendCo( pFrames, pObj->Value );
94  Gia_ManHashStop( pFrames );
95  pFrames = Gia_ManCleanup( pTemp = pFrames );
96  Gia_ManStop( pTemp );
97  return pFrames;
98 }
100 {
101  Gia_Man_t * pPref, * pNew;
102  sat_solver * pSat;
103  // create subset of the timeframe
104  pPref = Int2_ManUnroll( p, f );
105  // create SAT solver
106  pNew = Jf_ManDeriveCnf( pPref, 0 );
107  pCnf = (Cnf_Dat_t *)pPref->pData; pPref->pData = NULL;
108  Gia_ManStop( pPref );
109  // derive the SAT solver
110  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
111  // collect indexes of CO variables
112  *pvCiMap = Vec_IntAlloc( 100 );
113  Gia_ManForEachPo( pNew, pObj, i )
114  Vec_IntPush( *pvCiMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
115  // cleanup
116  Cnf_DataFree( pCnf );
117  Gia_ManStop( pNew );
118  return pSat;
119 }
120 
121 /**Function*************************************************************
122 
123  Synopsis []
124 
125  Description []
126 
127  SideEffects []
128 
129  SeeAlso []
130 
131 ***********************************************************************/
132 sat_solver * Int2_ManPrepareSuffix( Gia_Man_t * p, Vec_Int_t * vImageOne, Vec_Int_t * vImagesAll, Vec_Int_t ** pvCoMap, Gia_Man_t ** ppSuff )
133 {
134  Gia_Man_t * pSuff, * pNew;
135  Gia_Obj_t * pObj;
136  Cnf_Dat_t * pCnf;
137  sat_solver * pSat;
138  Vec_Int_t * vLits;
139  int i, Lit, Limit;
140  // create subset of the timeframe
141  pSuff = Int2_ManProbToGia( p, vImageOne );
142  assert( Gia_ManPiNum(pSuff) == Gia_ManCiNum(p) );
143  // create SAT solver
144  pNew = Jf_ManDeriveCnf( pSuff, 0 );
145  pCnf = (Cnf_Dat_t *)pSuff->pData; pSuff->pData = NULL;
146  Gia_ManStop( pSuff );
147  // derive the SAT solver
148  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
149  // create new constraints
150  vLits = Vec_IntAlloc( 1000 );
151  Vec_IntForEachEntryStart( vImagesAll, Limit, i, 1 )
152  {
153  Vec_IntClear( vLits );
154  for ( k = 0; k < Limit; k++ )
155  {
156  i++;
157  Lit = Vec_IntEntry( vSop, i + k );
158  Vec_IntPush( vLits, Abc_LitNot(Lit) );
159  }
160  if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) ) // UNSAT
161  {
162  Vec_IntFree( vLits );
163  Cnf_DataFree( pCnf );
164  Gia_ManStop( pNew );
165  *pvCoMap = NULL;
166  return NULL;
167  }
168  }
169  Vec_IntFree( vLits );
170  // collect indexes of CO variables
171  *pvCoMap = Vec_IntAlloc( 100 );
172  Gia_ManForEachRo( p, pObj, i )
173  {
174  pObj = Gia_ManPi( pNew, i + Gia_ManPiNum(p) );
175  Vec_IntPush( *pvCoMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
176  }
177  // cleanup
178  Cnf_DataFree( pCnf );
179  if ( ppSuff )
180  *ppSuff = pNew;
181  else
182  Gia_ManStop( pNew );
183  return pSat;
184 }
185 
186 /**Function*************************************************************
187 
188  Synopsis [Returns the cube cover and status.]
189 
190  Description []
191 
192  SideEffects []
193 
194  SeeAlso []
195 
196 ***********************************************************************/
197 Vec_Int_t * Int2_ManComputePreimage( Gia_Man_t * pSuff, sat_solver * pSatPref, sat_solver * pSatSuff, Vec_Int_t * vCiMap, Vec_Int_t * vCoMap, Vec_Int_t * vPrio )
198 {
199  int i, iVar, status;
200  Vec_IntClear( p->vImage );
201  while ( 1 )
202  {
203  // run suffix solver
204  status = sat_solver_solve( p->pSatSuff, NULL, NULL, 0, 0, 0, 0 );
205  if ( status == l_Undef )
206  return NULL; // timeout
207  if ( status == l_False )
208  return INT2_COMPUTED;
209  assert( status == l_True );
210  // collect assignment
211  Vec_IntClear( p->vAssign );
212  Vec_IntForEachEntry( p->vCiMap, iVar, i )
213  Vec_IntPush( p->vAssign, sat_solver_var_value(p->pSatSuff, iVar) );
214  // derive initial cube
215  vCube = Int2_ManRefineCube( p->pSuff, p->vAssign, p->vPrio );
216  // expend the cube using prefix
217  status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
218  if ( status == l_False )
219  {
220  int k, nCoreLits, * pCoreLits;
221  nCoreLits = sat_solver_final( p->pSatPref, &pCoreLits );
222  // create cube
223  Vec_IntClear( vCube );
224  Vec_IntPush( vImage, nCoreLits );
225  for ( k = 0; k < nCoreLits; k++ )
226  {
227  Vec_IntPush( vCube, pCoreLits[k] );
228  Vec_IntPush( vImage, pCoreLits[k] );
229  }
230  // add cube to the solver
231  if ( !sat_solver_addclause( p->pSatSuff, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube) ) )
232  {
233  Vec_IntFree( vCube );
234  return INT2_COMPUTED;
235  }
236  }
237  Vec_IntFree( vCube );
238  if ( status == l_Undef )
239  return INT2_TIME_OUT;
240  if ( status == l_True )
241  return INT2_FALSE_NEG;
242  assert( status == l_False );
243  continue;
244  }
245  return p->vImage;
246 }
247 
248 /**Function*************************************************************
249 
250  Synopsis [Interpolates while the number of conflicts is not exceeded.]
251 
252  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
253 
254  SideEffects [Does not check the property in 0-th frame.]
255 
256  SeeAlso []
257 
258 ***********************************************************************/
260 {
261  Int2_Man_t * p;
262  int f, i, RetValue = -1;
263  abctime clk, clkTotal = Abc_Clock(), timeTemp = 0;
264  abctime nTimeToStop = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
265 
266  // sanity checks
267  assert( Gia_ManPiNum(pInit) > 0 );
268  assert( Gia_ManPoNum(pInit) > 0 );
269  assert( Gia_ManRegNum(pInit) > 0 );
270 
271  // create manager
272  p = Int2_ManCreate( pInit, pPars );
273 
274  // create SAT solver
275  p->pSatPref = sat_solver_new();
276  sat_solver_setnvars( p->pSatPref, 1000 );
277  sat_solver_set_runtime_limit( p->pSatPref, nTimeToStop );
278 
279  // check outputs in the first frame
280  for ( i = 0; i < Gia_ManPoNum(pInit); i++ )
281  Vec_IntPush( p->vPrefCos, i );
282  Int2_ManCreateFrames( p, 0, p->vPrefCos );
283  RetValue = Int2_ManCheckBmc( p, NULL );
284  if ( RetValue != 1 )
285  return RetValue;
286 
287  // create original image
288  for ( f = pPars->nFramesS; f < p->nFramesMax; f++ )
289  {
290  for ( i = 0; i < p->nFramesMax; i++ )
291  {
292  p->pSatSuff = Int2_ManPrepareSuffix( p, vImageOne. vImagesAll, &vCoMap, &pGiaSuff );
293  sat_solver_set_runtime_limit( p->pSatSuff, nTimeToStop );
294  Vec_IntFreeP( &vImageOne );
295  vImageOne = Int2_ManComputePreimage( pGiaSuff, p->pSatPref, p->pSatSuff, vCiMap, vCoMap );
296  Vec_IntFree( vCoMap );
297  Gia_ManStop( pGiaSuff );
298  if ( nTimeToStop && Abc_Clock() > nTimeToStop )
299  return -1;
300  if ( vImageOne == NULL )
301  {
302  if ( i == 0 )
303  {
304  printf( "Satisfiable in frame %d.\n", f );
305  Vec_IntFree( vCiMap );
306  sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
307  return 0;
308  }
309  f += i;
310  break;
311  }
312  Vec_IntAppend( vImagesAll, vImageOne );
313  sat_solver_delete( p->pSatSuff ); p->pSatSuff = NULL;
314  }
315  Vec_IntFree( vCiMap );
316  sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
317  }
318  Abc_PrintTime( "Time", Abc_Clock() - clk );
319 
320 
321 p->timeSatPref += Abc_Clock() - clk;
322 
323  Int2_ManStop( p );
324  return RetValue;
325 }
326 
327 
328 
329 ////////////////////////////////////////////////////////////////////////
330 /// END OF FILE ///
331 ////////////////////////////////////////////////////////////////////////
332 
333 
335 
char * memset()
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_Man_t * Int2_ManUnroll(Gia_Man_t *p, int nFrames)
Definition: int2Core.c:70
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
void Int2_ManCreateFrames(Int2_Man_t *p, int iFrame, Vec_Int_t *vPrefCos)
Definition: int2Bmc.c:219
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Vec_Int_t * Int2_ManRefineCube(Gia_Man_t *p, Vec_Int_t *vAssign, Vec_Int_t *vPrio)
Definition: int2Refine.c:104
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define l_Undef
Definition: SolverTypes.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
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
int * pVarNums
Definition: cnf.h:63
#define l_True
Definition: SolverTypes.h:84
sat_solver * Int2_ManPrepareSuffix(Gia_Man_t *p, Vec_Int_t *vImageOne, Vec_Int_t *vImagesAll, Vec_Int_t **pvCoMap, Gia_Man_t **ppSuff)
Definition: int2Core.c:132
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition: giaJf.c:1746
static abctime Abc_Clock()
Definition: abc_global.h:279
Definition: cnf.h:56
Vec_Int_t * Int2_ManComputePreimage(Gia_Man_t *pSuff, sat_solver *pSatPref, sat_solver *pSatSuff, Vec_Int_t *vCiMap, Vec_Int_t *vCoMap, Vec_Int_t *vPrio)
Definition: int2Core.c:197
Definition: gia.h:75
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static int sat_solver_final(sat_solver *s, int **ppArray)
Definition: satSolver.h:227
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
typedefABC_NAMESPACE_HEADER_START struct Int2_Man_t_ Int2_Man_t
INCLUDES ///.
Definition: int2Int.h:45
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
int Int2_ManPerformInterpolation(Gia_Man_t *pInit, Int2_ManPars_t *pPars)
Definition: int2Core.c:259
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
int Int2_ManCheckBmc(Int2_Man_t *p, Vec_Int_t *vCube)
Definition: int2Bmc.c:318
ABC_NAMESPACE_IMPL_START void Int2_ManSetDefaultParams(Int2_ManPars_t *p)
DECLARATIONS ///.
Definition: int2Core.c:45
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
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
void * pData
Definition: gia.h:169
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static void Int2_ManStop(Int2_Man_t *p)
Definition: int2Int.h:105
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static Int2_Man_t * Int2_ManCreate(Gia_Man_t *pGia, Int2_ManPars_t *pPars)
Definition: int2Int.h:79
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_Man_t * Int2_ManProbToGia(Gia_Man_t *p, Vec_Int_t *vSop)
Definition: int2Util.c:98
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition: cnfMan.c:463
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
typedefABC_NAMESPACE_HEADER_START struct Int2_ManPars_t_ Int2_ManPars_t
INCLUDES ///.
Definition: int2.h:50
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
sat_solver * Int2_ManPreparePrefix(Gia_Man_t *p, int f, Vec_Int_t **pvCiMap)
Definition: int2Core.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387