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

Go to the source code of this file.

Data Structures

struct  Saig_RefMan_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Saig_RefMan_t_ 
Saig_RefMan_t
 DECLARATIONS ///. More...
 

Functions

int Saig_ManSimDataInit (Aig_Man_t *p, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo, Vec_Int_t *vRes)
 
Vec_Int_tSaig_RefManReason2Inputs (Saig_RefMan_t *p, Vec_Int_t *vReasons)
 FUNCTION DEFINITIONS ///. More...
 
Abc_Cex_tSaig_RefManReason2Cex (Saig_RefMan_t *p, Vec_Int_t *vReasons)
 
void Saig_RefManFindReason_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Int_t *vPrios, Vec_Int_t *vReasons)
 
Vec_Int_tSaig_RefManFindReason (Saig_RefMan_t *p)
 
void Saig_ManUnrollCollect_rec (Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vObjs, Vec_Int_t *vRoots)
 
Aig_Man_tSaig_ManUnrollWithCex (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, Vec_Int_t **pvMapPiF2A)
 
Saig_RefMan_tSaig_RefManStart (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
 
void Saig_RefManStop (Saig_RefMan_t *p)
 
int Saig_RefManSetPhases (Saig_RefMan_t *p, Abc_Cex_t *pCare, int fValue1)
 
Vec_Vec_tSaig_RefManOrderLiterals (Saig_RefMan_t *p, Vec_Int_t *vVar2PiId, Vec_Int_t *vAssumps)
 
Abc_Cex_tSaig_RefManCreateCex (Saig_RefMan_t *p, Vec_Int_t *vVar2PiId, Vec_Int_t *vAssumps)
 
Abc_Cex_tSaig_RefManRunSat (Saig_RefMan_t *p, int fNewOrder)
 
Vec_Int_tSaig_RefManRefineWithSat (Saig_RefMan_t *p, Vec_Int_t *vAigPis)
 
Abc_Cex_tSaig_ManFindCexCareBits (Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fNewOrder, int fVerbose)
 
Vec_Int_tSaig_ManExtendCounterExampleTest3 (Aig_Man_t *pAig, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Saig_RefMan_t_ Saig_RefMan_t

DECLARATIONS ///.

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

FileName [saigRefSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [SAT based refinement of a counter-example.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 33 of file saigRefSat.c.

Function Documentation

Vec_Int_t* Saig_ManExtendCounterExampleTest3 ( Aig_Man_t pAig,
int  iFirstFlopPi,
Abc_Cex_t pCex,
int  fVerbose 
)

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

Synopsis [Returns the array of PIs for flops that should not be absracted.]

Description []

SideEffects []

SeeAlso []

Definition at line 930 of file saigRefSat.c.

931 {
932  Saig_RefMan_t * p;
933  Vec_Int_t * vRes, * vReasons;
934  clock_t clk;
935  if ( Saig_ManPiNum(pAig) != pCex->nPis )
936  {
937  printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n",
938  Aig_ManCiNum(pAig), pCex->nPis );
939  return NULL;
940  }
941 
942 clk = clock();
943 
944  p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose );
945  vReasons = Saig_RefManFindReason( p );
946  vRes = Saig_RefManReason2Inputs( p, vReasons );
947 
948 // if ( fVerbose )
949  {
950  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
951  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
952  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
953 ABC_PRT( "Time", clock() - clk );
954  }
955 
956 /*
957  ////////////////////////////////////
958  Vec_IntFree( vReasons );
959  vReasons = Saig_RefManRefineWithSat( p, vRes );
960  ////////////////////////////////////
961 
962  // derive new result
963  Vec_IntFree( vRes );
964  vRes = Saig_RefManReason2Inputs( p, vReasons );
965 // if ( fVerbose )
966  {
967  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
968  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
969  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
970 ABC_PRT( "Time", clock() - clk );
971  }
972 */
973 
974  Vec_IntFree( vReasons );
975  Saig_RefManStop( p );
976  return vRes;
977 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Int_t * Saig_RefManFindReason(Saig_RefMan_t *p)
Definition: saigRefSat.c:168
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Saig_RefMan_t * Saig_RefManStart(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Definition: saigRefSat.c:363
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Vec_Int_t * Saig_RefManReason2Inputs(Saig_RefMan_t *p, Vec_Int_t *vReasons)
FUNCTION DEFINITIONS ///.
Definition: saigRefSat.c:64
void Saig_RefManStop(Saig_RefMan_t *p)
Definition: saigRefSat.c:386
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
typedefABC_NAMESPACE_IMPL_START struct Saig_RefMan_t_ Saig_RefMan_t
DECLARATIONS ///.
Definition: saigRefSat.c:33
Abc_Cex_t* Saig_ManFindCexCareBits ( Aig_Man_t pAig,
Abc_Cex_t pCex,
int  nInputs,
int  fNewOrder,
int  fVerbose 
)

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

Synopsis [SAT-based refinement of the counter-example.]

Description [The first parameter (nInputs) indicates how many first primary inputs to skip without considering as care candidates.]

SideEffects []

SeeAlso []

Definition at line 866 of file saigRefSat.c.

867 {
868  Saig_RefMan_t * p;
869  Vec_Int_t * vReasons;
870  Abc_Cex_t * pCare;
871  clock_t clk = clock();
872 
873  clk = clock();
874  p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
875  vReasons = Saig_RefManFindReason( p );
876 
877 if ( fVerbose )
878 Aig_ManPrintStats( p->pFrames );
879 
880 // if ( fVerbose )
881  {
882  Vec_Int_t * vRes = Saig_RefManReason2Inputs( p, vReasons );
883  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
884  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
885  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
886 ABC_PRT( "Time", clock() - clk );
887 
888  Vec_IntFree( vRes );
889 
890 /*
891  ////////////////////////////////////
892  Vec_IntFree( vReasons );
893  vReasons = Saig_RefManRefineWithSat( p, vRes );
894  ////////////////////////////////////
895 
896  Vec_IntFree( vRes );
897  vRes = Saig_RefManReason2Inputs( p, vReasons );
898  printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
899  Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
900  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
901 
902  Vec_IntFree( vRes );
903 ABC_PRT( "Time", clock() - clk );
904 */
905  }
906 
907  pCare = Saig_RefManReason2Cex( p, vReasons );
908  Vec_IntFree( vReasons );
909  Saig_RefManStop( p );
910 
911 if ( fVerbose )
912 Abc_CexPrintStats( pCex );
913 if ( fVerbose )
914 Abc_CexPrintStats( pCare );
915 
916  return pCare;
917 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_Cex_t * Saig_RefManReason2Cex(Saig_RefMan_t *p, Vec_Int_t *vReasons)
Definition: saigRefSat.c:93
Vec_Int_t * Saig_RefManFindReason(Saig_RefMan_t *p)
Definition: saigRefSat.c:168
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
void Abc_CexPrintStats(Abc_Cex_t *p)
Definition: utilCex.c:256
Saig_RefMan_t * Saig_RefManStart(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Definition: saigRefSat.c:363
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Vec_Int_t * Saig_RefManReason2Inputs(Saig_RefMan_t *p, Vec_Int_t *vReasons)
FUNCTION DEFINITIONS ///.
Definition: saigRefSat.c:64
void Saig_RefManStop(Saig_RefMan_t *p)
Definition: saigRefSat.c:386
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
typedefABC_NAMESPACE_IMPL_START struct Saig_RefMan_t_ Saig_RefMan_t
DECLARATIONS ///.
Definition: saigRefSat.c:33
int Saig_ManSimDataInit ( Aig_Man_t p,
Abc_Cex_t pCex,
Vec_Ptr_t vSimInfo,
Vec_Int_t vRes 
)

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

Synopsis [Performs ternary simulation for one design.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file absOldSim.c.

175 {
176  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
177  int i, f, Entry, iBit = 0;
178  Saig_ManForEachLo( p, pObj, i )
179  Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
180  for ( f = 0; f <= pCex->iFrame; f++ )
181  {
182  Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE );
183  Saig_ManForEachPi( p, pObj, i )
184  Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
185  if ( vRes )
186  Vec_IntForEachEntry( vRes, Entry, i )
187  Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND );
188  Aig_ManForEachNode( p, pObj, i )
189  Saig_ManExtendOneEval( vSimInfo, pObj, f );
190  Aig_ManForEachCo( p, pObj, i )
191  Saig_ManExtendOneEval( vSimInfo, pObj, f );
192  if ( f == pCex->iFrame )
193  break;
194  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
195  Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) );
196  }
197  // make sure the output of the property failed
198  pObj = Aig_ManCo( p, pCex->iPo );
199  return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
200 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Saig_ManExtendOneEval(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
FUNCTION DEFINITIONS ///.
Definition: absOldSim.c:143
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
#define SAIG_ONE
Definition: absOldSim.c:31
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
for(p=first;p->value< newval;p=p->next)
#define SAIG_UND
Definition: absOldSim.c:32
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define SAIG_ZER
DECLARATIONS ///.
Definition: absOldSim.c:30
static void Saig_ManSimInfoSet(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame, int Value)
Definition: absOldSim.c:58
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Saig_ManSimInfoGet(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
Definition: absOldSim.c:52
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Saig_ManUnrollCollect_rec ( Aig_Man_t pAig,
Aig_Obj_t pObj,
Vec_Int_t vObjs,
Vec_Int_t vRoots 
)

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

Synopsis [Collect nodes in the unrolled timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file saigRefSat.c.

237 {
238  if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
239  return;
240  Aig_ObjSetTravIdCurrent(pAig, pObj);
241  if ( Aig_ObjIsCo(pObj) )
242  Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
243  else if ( Aig_ObjIsNode(pObj) )
244  {
245  Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
246  Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
247  }
248  if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
249  Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
250  Vec_IntPush( vObjs, Aig_ObjId(pObj) );
251 }
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
void Saig_ManUnrollCollect_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vObjs, Vec_Int_t *vRoots)
Definition: saigRefSat.c:236
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Aig_Man_t* Saig_ManUnrollWithCex ( Aig_Man_t pAig,
Abc_Cex_t pCex,
int  nInputs,
Vec_Int_t **  pvMapPiF2A 
)

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

Synopsis [Derive unrolled timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file saigRefSat.c.

265 {
266  Aig_Man_t * pFrames; // unrolled timeframes
267  Vec_Vec_t * vFrameCos; // the list of COs per frame
268  Vec_Vec_t * vFrameObjs; // the list of objects per frame
269  Vec_Int_t * vRoots, * vObjs;
270  Aig_Obj_t * pObj;
271  int i, f;
272  // sanity checks
273  assert( Saig_ManPiNum(pAig) == pCex->nPis );
274  assert( Saig_ManRegNum(pAig) == pCex->nRegs );
275  assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
276 
277  // map PIs of the unrolled frames into PIs of the original design
278  *pvMapPiF2A = Vec_IntAlloc( 1000 );
279 
280  // collect COs and Objs visited in each frame
281  vFrameCos = Vec_VecStart( pCex->iFrame+1 );
282  vFrameObjs = Vec_VecStart( pCex->iFrame+1 );
283  // initialized the topmost frame
284  pObj = Aig_ManCo( pAig, pCex->iPo );
285  Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) );
286  for ( f = pCex->iFrame; f >= 0; f-- )
287  {
288  // collect nodes starting from the roots
289  Aig_ManIncrementTravId( pAig );
290  vRoots = Vec_VecEntryInt( vFrameCos, f );
291  Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
292  Saig_ManUnrollCollect_rec( pAig, pObj,
293  Vec_VecEntryInt(vFrameObjs, f),
294  (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
295  }
296 
297  // derive unrolled timeframes
298  pFrames = Aig_ManStart( 10000 );
299  pFrames->pName = Abc_UtilStrsav( pAig->pName );
300  pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
301  // initialize the flops
302  Saig_ManForEachLo( pAig, pObj, i )
303  pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) );
304  // iterate through the frames
305  for ( f = 0; f <= pCex->iFrame; f++ )
306  {
307  // construct
308  vObjs = Vec_VecEntryInt( vFrameObjs, f );
309  Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
310  {
311  if ( Aig_ObjIsNode(pObj) )
312  pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
313  else if ( Aig_ObjIsCo(pObj) )
314  pObj->pData = Aig_ObjChild0Copy(pObj);
315  else if ( Aig_ObjIsConst1(pObj) )
316  pObj->pData = Aig_ManConst1(pFrames);
317  else if ( Saig_ObjIsPi(pAig, pObj) )
318  {
319  if ( Aig_ObjCioId(pObj) < nInputs )
320  {
321  int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
322  pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
323  }
324  else
325  {
326  pObj->pData = Aig_ObjCreateCi( pFrames );
327  Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
328  Vec_IntPush( *pvMapPiF2A, f );
329  }
330  }
331  }
332  if ( f == pCex->iFrame )
333  break;
334  // transfer
335  vRoots = Vec_VecEntryInt( vFrameCos, f );
336  Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
337  Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
338  }
339  // create output
340  pObj = Aig_ManCo( pAig, pCex->iPo );
341  Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
342  Aig_ManSetRegNum( pFrames, 0 );
343  // cleanup
344  Vec_VecFree( vFrameCos );
345  Vec_VecFree( vFrameObjs );
346  // finallize
347  Aig_ManCleanup( pFrames );
348  // return
349  return pFrames;
350 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_Not(Aig_Obj_t *p)
Definition: aig.h:247
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
for(p=first;p->value< newval;p=p->next)
void Saig_ManUnrollCollect_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vObjs, Vec_Int_t *vRoots)
Definition: saigRefSat.c:236
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static void Vec_VecPushInt(Vec_Vec_t *p, int Level, int Entry)
Definition: vecVec.h:468
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
static Aig_Obj_t * Saig_ObjLiToLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:87
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
static Vec_Ptr_t * Vec_VecEntry(Vec_Vec_t *p, int i)
Definition: vecVec.h:271
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
Abc_Cex_t* Saig_RefManCreateCex ( Saig_RefMan_t p,
Vec_Int_t vVar2PiId,
Vec_Int_t vAssumps 
)

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

Synopsis [Generate the care set using SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 473 of file saigRefSat.c.

474 {
475  Abc_Cex_t * pCare;
476  int i, Entry, iInput, iFrame;
477  // create counter-example
478  pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
479  memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
480  Vec_IntForEachEntry( vAssumps, Entry, i )
481  {
482  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
483  assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
484  iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
485  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
486  Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
487  }
488  return pCare;
489 }
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int lit_var(lit l)
Definition: satVec.h:145
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
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition: utilCex.c:145
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t* Saig_RefManFindReason ( Saig_RefMan_t p)

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

Synopsis [Returns reasons for the property to fail.]

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file saigRefSat.c.

169 {
170  Aig_Obj_t * pObj;
171  Vec_Int_t * vPrios, * vPi2Prio, * vReasons;
172  int i, CountPrios;
173 
174  vPi2Prio = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
175  vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
176 
177  // set PI values according to CEX
178  CountPrios = 0;
179  Aig_ManConst1(p->pFrames)->fPhase = 1;
180  Aig_ManForEachCi( p->pFrames, pObj, i )
181  {
182  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
183  int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
184  pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
185  // assign priority
186  if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 )
187  Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ );
188 // Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPi2Prio, iInput) );
189  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
190  }
191 // printf( "Priority numbers = %d.\n", CountPrios );
192  Vec_IntFree( vPi2Prio );
193 
194  // traverse and set the priority
195  Aig_ManForEachNode( p->pFrames, pObj, i )
196  {
197  int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
198  int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
199  int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
200  int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
201  pObj->fPhase = fPhase0 && fPhase1;
202  if ( fPhase0 && fPhase1 ) // both are one
203  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
204  else if ( !fPhase0 && fPhase1 )
205  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
206  else if ( fPhase0 && !fPhase1 )
207  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
208  else // both are zero
209  Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
210  }
211  // check the property output
212  pObj = Aig_ManCo( p->pFrames, 0 );
213  assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) );
214 
215  // select the reason
216  vReasons = Vec_IntAlloc( 100 );
217  Aig_ManIncrementTravId( p->pFrames );
218  if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
219  Saig_RefManFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
220  Vec_IntFree( vPrios );
221  return vReasons;
222 }
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
static int Aig_ObjFaninId1(Aig_Obj_t *pObj)
Definition: aig.h:305
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
void Saig_RefManFindReason_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Int_t *vPrios, Vec_Int_t *vReasons)
Definition: saigRefSat.c:120
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Definition: aig.h:69
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
unsigned int fPhase
Definition: aig.h:78
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void Saig_RefManFindReason_rec ( Aig_Man_t p,
Aig_Obj_t pObj,
Vec_Int_t vPrios,
Vec_Int_t vReasons 
)

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

Synopsis [Returns reasons for the property to fail.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file saigRefSat.c.

121 {
122  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
123  return;
124  Aig_ObjSetTravIdCurrent(p, pObj);
125  if ( Aig_ObjIsCi(pObj) )
126  {
127  Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
128  return;
129  }
130  assert( Aig_ObjIsNode(pObj) );
131  if ( pObj->fPhase )
132  {
133  Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
134  Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
135  }
136  else
137  {
138  int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
139  int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
140  assert( !fPhase0 || !fPhase1 );
141  if ( !fPhase0 && fPhase1 )
142  Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
143  else if ( fPhase0 && !fPhase1 )
144  Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
145  else
146  {
147  int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
148  int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
149  if ( iPrio0 <= iPrio1 )
150  Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
151  else
152  Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
153  }
154  }
155 }
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static int Aig_ObjFaninId1(Aig_Obj_t *pObj)
Definition: aig.h:305
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
void Saig_RefManFindReason_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Int_t *vPrios, Vec_Int_t *vReasons)
Definition: saigRefSat.c:120
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
unsigned int fPhase
Definition: aig.h:78
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
Vec_Vec_t* Saig_RefManOrderLiterals ( Saig_RefMan_t p,
Vec_Int_t vVar2PiId,
Vec_Int_t vAssumps 
)

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

Synopsis [Tries to remove literals from abstraction.]

Description [The literals are sorted more desirable first.]

SideEffects []

SeeAlso []

Definition at line 438 of file saigRefSat.c.

439 {
440  Vec_Vec_t * vLits;
441  Vec_Int_t * vVar2New;
442  int i, Entry, iInput, iFrame;
443  // collect literals
444  vLits = Vec_VecAlloc( 100 );
445  vVar2New = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
446  Vec_IntForEachEntry( vAssumps, Entry, i )
447  {
448  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
449  assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
450  iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
451  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
452 // Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
453  if ( Vec_IntEntry( vVar2New, iInput ) == ~0 )
454  Vec_IntWriteEntry( vVar2New, iInput, Vec_VecSize(vLits) );
455  Vec_VecPushInt( vLits, Vec_IntEntry( vVar2New, iInput ), Entry );
456  }
457  Vec_IntFree( vVar2New );
458  return vLits;
459 }
static Vec_Vec_t * Vec_VecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecVec.h:145
Aig_Man_t * pAig
Definition: llb3Image.c:49
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int lit_var(lit l)
Definition: satVec.h:145
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static void Vec_VecPushInt(Vec_Vec_t *p, int Level, int Entry)
Definition: vecVec.h:468
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
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
static int Vec_VecSize(Vec_Vec_t *p)
Definition: vecVec.h:222
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Abc_Cex_t* Saig_RefManReason2Cex ( Saig_RefMan_t p,
Vec_Int_t vReasons 
)

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

Synopsis [Creates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file saigRefSat.c.

94 {
95  Abc_Cex_t * pCare;
96  int i, Entry, iInput, iFrame;
97  pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
98  memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
99  Vec_IntForEachEntry( vReasons, Entry, i )
100  {
101  assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) );
102  iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
103  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
104  Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
105  }
106  return pCare;
107 }
char * memset()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
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
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition: utilCex.c:145
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t* Saig_RefManReason2Inputs ( Saig_RefMan_t p,
Vec_Int_t vReasons 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Maps array of frame PI IDs into array of original PI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file saigRefSat.c.

65 {
66  Vec_Int_t * vOriginal, * vVisited;
67  int i, Entry;
68  vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) );
69  vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
70  Vec_IntForEachEntry( vReasons, Entry, i )
71  {
72  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
73  assert( iInput >= 0 && iInput < Aig_ManCiNum(p->pAig) );
74  if ( Vec_IntEntry(vVisited, iInput) == 0 )
75  Vec_IntPush( vOriginal, iInput );
76  Vec_IntAddToEntry( vVisited, iInput, 1 );
77  }
78  Vec_IntFree( vVisited );
79  return vOriginal;
80 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
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
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t* Saig_RefManRefineWithSat ( Saig_RefMan_t p,
Vec_Int_t vAigPis 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 706 of file saigRefSat.c.

707 {
708  int nConfLimit = 1000000;
709  Cnf_Dat_t * pCnf;
710  sat_solver * pSat;
711  Aig_Obj_t * pObj;
712  Vec_Vec_t * vLits;
713  Vec_Int_t * vReasons, * vAssumps, * vVisited, * vVar2PiId;
714  int i, k, f, Entry, RetValue, Counter;
715 
716  // create CNF and SAT solver
717  pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
718  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
719  if ( pSat == NULL )
720  {
721  Cnf_DataFree( pCnf );
722  return NULL;
723  }
724 
725  // mark used AIG inputs
726  vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
727  Vec_IntForEachEntry( vAigPis, Entry, i )
728  {
729  assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pAig) );
730  Vec_IntWriteEntry( vVisited, Entry, 1 );
731  }
732 
733  // create assumptions
734  vVar2PiId = Vec_IntStartFull( pCnf->nVars );
735  vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) );
736  Aig_ManForEachCi( p->pFrames, pObj, i )
737  {
738  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
739  int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
740  if ( Vec_IntEntry(vVisited, iInput) == 0 )
741  continue;
742  RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
743  Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
744 // Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
745  Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
746  }
747  Vec_IntFree( vVisited );
748 
749  // try assumptions in different order
750  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
751  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
752  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
753  Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
754 
755 /*
756  // AnalizeFinal does not work because it implications propagate directly
757  // and SAT solver does not kick in (the number of conflicts in 0).
758 
759  // count the number of lits in the unsat core
760  {
761  int nCoreLits, * pCoreLits;
762  nCoreLits = sat_solver_final( pSat, &pCoreLits );
763  assert( nCoreLits > 0 );
764 
765  // count the number of flops
766  vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
767  for ( i = 0; i < nCoreLits; i++ )
768  {
769  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) );
770  int iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
771  int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
772  Vec_IntWriteEntry( vVisited, iInput, 1 );
773  }
774  // count the number of entries
775  Counter = 0;
776  Vec_IntForEachEntry( vVisited, Entry, i )
777  Counter += Entry;
778  Vec_IntFree( vVisited );
779 
780 // if ( p->fVerbose )
781  printf( "AnalizeFinal: Assumptions %d (out of %d). Essential PIs = %d. Conflicts = %d.\n",
782  nCoreLits, Vec_IntSize(vAssumps), Counter, (int)pSat->stats.conflicts );
783  }
784 */
785 
786  // derive literals
787  vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
788  for ( i = 0; i < Vec_VecSize(vLits); i++ )
789  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
790  printf( "\n" );
791 
792  // create different sets of assumptions
793  Counter = Vec_VecSize(vLits);
794  for ( f = 0; f < Vec_VecSize(vLits); f++ )
795  {
796  Vec_IntClear( vAssumps );
797  Vec_VecForEachEntryInt( vLits, Entry, i, k )
798  if ( i != f )
799  Vec_IntPush( vAssumps, Entry );
800 
801  // try the new assumptions
802  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
803  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
804  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
805  Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
806  if ( RetValue != l_False )
807  continue;
808 
809  // UNSAT - remove literals
810  Vec_IntClear( Vec_VecEntryInt(vLits, f) );
811  Counter--;
812  }
813 
814  for ( i = 0; i < Vec_VecSize(vLits); i++ )
815  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
816  printf( "\n" );
817 
818  // create assumptions
819  Vec_IntClear( vAssumps );
820  Vec_VecForEachEntryInt( vLits, Entry, i, k )
821  Vec_IntPush( vAssumps, Entry );
822 
823  // try assumptions in different order
824  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
825  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
826  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
827  Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
828 
829 // if ( p->fVerbose )
830 // printf( "Total PIs = %d. Essential PIs = %d.\n",
831 // Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
832 
833 
834  // transform assumptions into reasons
835  vReasons = Vec_IntAlloc( 100 );
836  Vec_IntForEachEntry( vAssumps, Entry, i )
837  {
838  int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
839  assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) );
840  Vec_IntPush( vReasons, iPiNum );
841  }
842 
843  // cleanup
844  Cnf_DataFree( pCnf );
845  sat_solver_delete( pSat );
846  Vec_IntFree( vAssumps );
847  Vec_IntFree( vVar2PiId );
848  Vec_VecFreeP( &vLits );
849 
850  return vReasons;
851 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Aig_Man_t * pAig
Definition: llb3Image.c:49
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
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 lit_var(lit l)
Definition: satVec.h:145
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Vec_Vec_t * Saig_RefManOrderLiterals(Saig_RefMan_t *p, Vec_Int_t *vVar2PiId, Vec_Int_t *vAssumps)
Definition: saigRefSat.c:438
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
stats_t stats
Definition: satSolver.h:156
Definition: cnf.h:56
#define Vec_VecForEachEntryInt(vGlob, Entry, i, k)
Definition: vecVec.h:109
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
for(p=first;p->value< newval;p=p->next)
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
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
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
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Counter
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
ABC_INT64_T conflicts
Definition: satVec.h:154
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
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
static int Vec_VecSize(Vec_Vec_t *p)
Definition: vecVec.h:222
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Abc_Cex_t* Saig_RefManRunSat ( Saig_RefMan_t p,
int  fNewOrder 
)

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

Synopsis [Generate the care set using SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 502 of file saigRefSat.c.

503 {
504  int nConfLimit = 1000000;
505  Abc_Cex_t * pCare;
506  Cnf_Dat_t * pCnf;
507  sat_solver * pSat;
508  Aig_Obj_t * pObj;
509  Vec_Vec_t * vLits = NULL;
510  Vec_Int_t * vAssumps, * vVar2PiId;
511  int i, k, Entry, RetValue;//, f = 0, Counter = 0;
512  int nCoreLits, * pCoreLits;
513  clock_t clk = clock();
514  // create CNF
515  assert( Aig_ManRegNum(p->pFrames) == 0 );
516 // pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow
517  pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
518  RetValue = Saig_RefManSetPhases( p, NULL, 0 );
519  if ( RetValue )
520  {
521  printf( "Constructed frames are incorrect.\n" );
522  Cnf_DataFree( pCnf );
523  return NULL;
524  }
525  Cnf_DataTranformPolarity( pCnf, 0 );
526  // create SAT solver
527  pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
528  if ( pSat == NULL )
529  {
530  Cnf_DataFree( pCnf );
531  return NULL;
532  }
533 //Abc_PrintTime( 1, "Preparing", clock() - clk );
534  // look for a true counter-example
535  if ( p->nInputs > 0 )
536  {
537  RetValue = sat_solver_solve( pSat, NULL, NULL,
538  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
539  if ( RetValue == l_False )
540  {
541  printf( "The problem is trivially UNSAT. The CEX is real.\n" );
542  // create counter-example
543  pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
544  memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
545  return pCare;
546  }
547  // the problem is SAT - it is expected
548  }
549  // create assumptions
550  vVar2PiId = Vec_IntStartFull( pCnf->nVars );
551  vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) );
552  Aig_ManForEachCi( p->pFrames, pObj, i )
553  {
554 // RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
555 // Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
556  Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
557  Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
558  }
559 
560  // reverse the order of assumptions
561 // if ( fNewOrder )
562 // Vec_IntReverseOrder( vAssumps );
563 
564  if ( fNewOrder )
565  {
566  // create literals
567  vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
568  // sort literals
569  Vec_VecSort( vLits, 1 );
570  // save literals
571  Vec_IntClear( vAssumps );
572  Vec_VecForEachEntryInt( vLits, Entry, i, k )
573  Vec_IntPush( vAssumps, Entry );
574 
575  for ( i = 0; i < Vec_VecSize(vLits); i++ )
576  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
577  printf( "\n" );
578 
579  if ( p->fVerbose )
580  printf( "Total PIs = %d. Essential PIs = %d.\n",
581  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
582  }
583 
584  // solve
585 clk = clock();
586  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
587  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
588 //Abc_PrintTime( 1, "Solving", clock() - clk );
589  if ( RetValue != l_False )
590  {
591  if ( RetValue == l_True )
592  printf( "Internal Error!!! The resulting problem is SAT.\n" );
593  else
594  printf( "Internal Error!!! SAT solver timed out.\n" );
595  Cnf_DataFree( pCnf );
596  sat_solver_delete( pSat );
597  Vec_IntFree( vAssumps );
598  Vec_IntFree( vVar2PiId );
599  return NULL;
600  }
601  assert( RetValue == l_False ); // UNSAT
602 
603  // get relevant SAT literals
604  nCoreLits = sat_solver_final( pSat, &pCoreLits );
605  assert( nCoreLits > 0 );
606  if ( p->fVerbose )
607  printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n",
608  nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
609 
610  // save literals
611  Vec_IntClear( vAssumps );
612  for ( i = 0; i < nCoreLits; i++ )
613  Vec_IntPush( vAssumps, pCoreLits[i] );
614 
615 
616  // create literals
617  vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
618  // sort literals
619 // Vec_VecSort( vLits, 0 );
620  // save literals
621  Vec_IntClear( vAssumps );
622  Vec_VecForEachEntryInt( vLits, Entry, i, k )
623  Vec_IntPush( vAssumps, Entry );
624 
625 // for ( i = 0; i < Vec_VecSize(vLits); i++ )
626 // printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
627 // printf( "\n" );
628 
629  if ( p->fVerbose )
630  printf( "Total PIs = %d. Essential PIs = %d.\n",
631  Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
632 /*
633  // try assumptions in different order
634  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
635  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
636  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
637  Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
638 
639  // create different sets of assumptions
640  Counter = Vec_VecSize(vLits);
641  for ( f = 0; f < Vec_VecSize(vLits); f++ )
642  {
643  Vec_IntClear( vAssumps );
644  Vec_VecForEachEntryInt( vLits, Entry, i, k )
645  if ( i != f )
646  Vec_IntPush( vAssumps, Entry );
647 
648  // try the new assumptions
649  RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps),
650  (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
651  printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n",
652  Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
653  if ( RetValue != l_False )
654  continue;
655 
656  // UNSAT - remove literals
657  Vec_IntClear( Vec_VecEntryInt(vLits, f) );
658  Counter--;
659  }
660 
661  for ( i = 0; i < Vec_VecSize(vLits); i++ )
662  printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) );
663  printf( "\n" );
664 
665  if ( p->fVerbose )
666  printf( "Total PIs = %d. Essential PIs = %d.\n",
667  Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
668 
669  // save literals
670  Vec_IntClear( vAssumps );
671  Vec_VecForEachEntryInt( vLits, Entry, i, k )
672  Vec_IntPush( vAssumps, Entry );
673 */
674  // create counter-example
675  pCare = Saig_RefManCreateCex( p, vVar2PiId, vAssumps );
676 
677  // cleanup
678  Cnf_DataFree( pCnf );
679  sat_solver_delete( pSat );
680  Vec_IntFree( vAssumps );
681  Vec_IntFree( vVar2PiId );
682  Vec_VecFreeP( &vLits );
683 
684  // verify counter-example
685  RetValue = Saig_RefManSetPhases( p, pCare, 0 );
686  if ( RetValue )
687  printf( "Reduced CEX verification has failed.\n" );
688  RetValue = Saig_RefManSetPhases( p, pCare, 1 );
689  if ( RetValue )
690  printf( "Reduced CEX verification has failed.\n" );
691  return pCare;
692 }
char * memset()
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static void Vec_VecSort(Vec_Vec_t *p, int fReverse)
Definition: vecVec.h:546
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
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
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Vec_Vec_t * Saig_RefManOrderLiterals(Saig_RefMan_t *p, Vec_Int_t *vVar2PiId, Vec_Int_t *vAssumps)
Definition: saigRefSat.c:438
int Saig_RefManSetPhases(Saig_RefMan_t *p, Abc_Cex_t *pCare, int fValue1)
Definition: saigRefSat.c:404
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int * pVarNums
Definition: cnf.h:63
void Cnf_DataTranformPolarity(Cnf_Dat_t *pCnf, int fTransformPos)
Definition: cnfMan.c:652
#define l_True
Definition: SolverTypes.h:84
Definition: cnf.h:56
#define Vec_VecForEachEntryInt(vGlob, Entry, i, k)
Definition: vecVec.h:109
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
for(p=first;p->value< newval;p=p->next)
static int sat_solver_final(sat_solver *s, int **ppArray)
Definition: satSolver.h:227
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Abc_Cex_t * Saig_RefManCreateCex(Saig_RefMan_t *p, Vec_Int_t *vVar2PiId, Vec_Int_t *vAssumps)
Definition: saigRefSat.c:473
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
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static Vec_Int_t * Vec_VecEntryInt(Vec_Vec_t *p, int i)
Definition: vecVec.h:276
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
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
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition: cnfWrite.c:587
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition: utilCex.c:145
static int Vec_VecSize(Vec_Vec_t *p)
Definition: vecVec.h:222
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
static void Vec_VecFreeP(Vec_Vec_t **p)
Definition: vecVec.h:367
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
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
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int Saig_RefManSetPhases ( Saig_RefMan_t p,
Abc_Cex_t pCare,
int  fValue1 
)

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

Synopsis [Sets phase bits in the timeframe AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 404 of file saigRefSat.c.

405 {
406  Aig_Obj_t * pObj;
407  int i, iFrame, iInput;
408  Aig_ManConst1( p->pFrames )->fPhase = 1;
409  Aig_ManForEachCi( p->pFrames, pObj, i )
410  {
411  iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
412  iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
413  pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
414  // update value if it is a don't-care
415  if ( pCare && !Abc_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) )
416  pObj->fPhase = fValue1;
417  }
418  Aig_ManForEachNode( p->pFrames, pObj, i )
419  pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
420  & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) );
421  Aig_ManForEachCo( p->pFrames, pObj, i )
422  pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) );
423  pObj = Aig_ManCo( p->pFrames, 0 );
424  return pObj->fPhase;
425 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Definition: aig.h:69
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
unsigned int fPhase
Definition: aig.h:78
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Saig_RefMan_t* Saig_RefManStart ( Aig_Man_t pAig,
Abc_Cex_t pCex,
int  nInputs,
int  fVerbose 
)

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

Synopsis [Creates refinement manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 363 of file saigRefSat.c.

364 {
365  Saig_RefMan_t * p;
366  p = ABC_CALLOC( Saig_RefMan_t, 1 );
367  p->pAig = pAig;
368  p->pCex = pCex;
369  p->nInputs = nInputs;
370  p->fVerbose = fVerbose;
371  p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A );
372  return p;
373 }
Aig_Man_t * Saig_ManUnrollWithCex(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, Vec_Int_t **pvMapPiF2A)
Definition: saigRefSat.c:264
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
typedefABC_NAMESPACE_IMPL_START struct Saig_RefMan_t_ Saig_RefMan_t
DECLARATIONS ///.
Definition: saigRefSat.c:33
void Saig_RefManStop ( Saig_RefMan_t p)

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

Synopsis [Destroys refinement manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file saigRefSat.c.

387 {
388  Aig_ManStopP( &p->pFrames );
389  Vec_IntFreeP( &p->vMapPiF2A );
390  ABC_FREE( p );
391 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Aig_ManStopP(Aig_Man_t **p)
Definition: aigMan.c:246
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
#define ABC_FREE(obj)
Definition: abc_global.h:232