abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Macros | Typedefs | Functions
bmcBmc3.c File Reference
#include "proof/fra/fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecWec.h"
#include "bmc.h"

Go to the source code of this file.

Data Structures

struct  Gia_ManBmc_t_
 

Macros

#define SAIG_TER_NON   0
 FUNCTION DEFINITIONS ///. More...
 
#define SAIG_TER_ZER   1
 
#define SAIG_TER_ONE   2
 
#define SAIG_TER_UND   3
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Gia_ManBmc_t_ 		Gia_ManBmc_t
 DECLARATIONS ///. More...
 

Functions

int Gia_ManToBridgeResult (FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
 DECLARATIONS ///. More...
 
void Gia_ManReportProgress (FILE *pFile, int prop_no, int depth)
 
static int Saig_ManBmcSimInfoNot (int Value)
 
static int Saig_ManBmcSimInfoAnd (int Value0, int Value1)
 
static int Saig_ManBmcSimInfoGet (unsigned *pInfo, Aig_Obj_t *pObj)
 
static void Saig_ManBmcSimInfoSet (unsigned *pInfo, Aig_Obj_t *pObj, int Value)
 
static int Saig_ManBmcSimInfoClear (unsigned *pInfo, Aig_Obj_t *pObj)
 
int Saig_ManBmcTerSimCount01 (Aig_Man_t *p, unsigned *pInfo)
 
unsigned * Saig_ManBmcTerSimOne (Aig_Man_t *p, unsigned *pPrev)
 
Vec_Ptr_t * Saig_ManBmcTerSim (Aig_Man_t *p)
 
void Saig_ManBmcTerSimTest (Aig_Man_t *p)
 
int Saig_ManBmcCountNonternary_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vInfos, unsigned *pInfo, int f, int *pCounter)
 
void Saig_ManBmcCountNonternary (Aig_Man_t *p, Vec_Ptr_t *vInfos, int iFrame)
 
int Saig_ManBmcTerSimCount01Po (Aig_Man_t *p, unsigned *pInfo)
 
Vec_Ptr_t * Saig_ManBmcTerSimPo (Aig_Man_t *p)
 
void Saig_ManBmcTerSimTestPo (Aig_Man_t *p)
 
void Saig_ManBmcDfs_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
 
Vec_Ptr_t * Saig_ManBmcDfsNodes (Aig_Man_t *p, Vec_Ptr_t *vRoots)
 
Vec_Vec_t * Saig_ManBmcSections (Aig_Man_t *p)
 
void Saig_ManBmcSectionsTest (Aig_Man_t *p)
 
void Saig_ManBmcSupergate_rec (Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
 
Vec_Ptr_t * Saig_ManBmcSupergate (Aig_Man_t *p, int iPo)
 
int Saig_ManBmcCountRefed (Aig_Man_t *p, Vec_Ptr_t *vSuper)
 
void Saig_ManBmcSupergateTest (Aig_Man_t *p)
 
void Saig_ManBmcWriteBlif (Aig_Man_t *p, Vec_Int_t *vMapping, char *pFileName)
 
void Saig_ManBmcMappingTest (Aig_Man_t *p)
 
Vec_Int_t * Saig_ManBmcComputeMappingRefs (Aig_Man_t *p, Vec_Int_t *vMap)
 
Gia_ManBmc_t * Saig_Bmc3ManStart (Aig_Man_t *pAig, int nTimeOutOne)
 
void Saig_Bmc3ManStop (Gia_ManBmc_t *p)
 
static int * Saig_ManBmcMapping (Gia_ManBmc_t *p, Aig_Obj_t *pObj)
 
static int Saig_ManBmcLiteral (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
 
static int Saig_ManBmcSetLiteral (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, int iLit)
 
static int Saig_ManBmcCof0 (int t, int v)
 
static int Saig_ManBmcCof1 (int t, int v)
 
static int Saig_ManBmcCofEqual (int t, int v)
 
static int Saig_ManBmcReduceTruth (int uTruth, int Lits[])
 
static void Saig_ManBmcAddClauses (Gia_ManBmc_t *p, int uTruth, int Lits[], int iLitOut)
 
int Saig_ManBmcCreateCnf_rec (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
 
void Saig_ManBmcCreateCnf_iter (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, Vec_Int_t *vVisit)
 
int Saig_ManBmcRunTerSim_rec (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
 
int Saig_ManBmcCreateCnf (Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
 
int Aig_NodeCompareRefsIncrease (Aig_Obj_t **pp1, Aig_Obj_t **pp2)
 
void Saig_ParBmcSetDefaultParams (Saig_ParBmc_t *p)
 
abctime Saig_ManBmcTimeToStop (Saig_ParBmc_t *pPars, abctime nTimeToStopNG)
 
Abc_Cex_t * Saig_ManGenerateCex (Gia_ManBmc_t *p, int f, int i)
 
int Saig_ManCallSolver (Gia_ManBmc_t *p, int Lit)
 
int Saig_ManBmcScalable (Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
 

Macro Definition Documentation

#define SAIG_TER_NON   0

FUNCTION DEFINITIONS ///.

Definition at line 83 of file bmcBmc3.c.

#define SAIG_TER_ONE   2

Definition at line 85 of file bmcBmc3.c.

#define SAIG_TER_UND   3

Definition at line 86 of file bmcBmc3.c.

#define SAIG_TER_ZER   1

Definition at line 84 of file bmcBmc3.c.

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Gia_ManBmc_t_ Gia_ManBmc_t

DECLARATIONS ///.

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

FileName [bmcBmc3.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Simple BMC package.]

Author [Alan Mishchenko in collaboration with Niklas Een.]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 34 of file bmcBmc3.c.

Function Documentation

int Aig_NodeCompareRefsIncrease ( Aig_Obj_t **  pp1,
Aig_Obj_t **  pp2 
)

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

Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 1258 of file bmcBmc3.c.

1259 {
1260  int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2);
1261  if ( Diff < 0 )
1262  return -1;
1263  if ( Diff > 0 )
1264  return 1;
1265  Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
1266  if ( Diff < 0 )
1267  return -1;
1268  if ( Diff > 0 )
1269  return 1;
1270  return 0;
1271 }
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
void Gia_ManReportProgress ( FILE *  pFile,
int  prop_no,
int  depth 
)

Definition at line 71 of file bmcBmc3.c.

72 {
73  extern int Gia_ManToBridgeProgress( FILE * pFile, int Size, unsigned char * pBuffer );
74  char buf[100];
75  sprintf(buf, "property: safe<%d>\nbug-free-depth: %d\n", prop_no, depth);
76  Gia_ManToBridgeProgress(pFile, strlen(buf), (unsigned char *)buf);
77 }
sprintf
char * sprintf()
Gia_ManToBridgeProgress
int Gia_ManToBridgeProgress(FILE *pFile, int Size, unsigned char *pBuffer)
Definition: utilBridge.c:182
strlen
int strlen()
int Gia_ManToBridgeResult ( FILE *  pFile,
int  Result,
Abc_Cex_t *  pCex,
int  iPoProved 
)

DECLARATIONS ///.

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

FileName [pdrCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:
pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]

Definition at line 284 of file utilBridge.c.

285 {
286  if ( Result == 0 ) // sat
287  Gia_ManFromBridgeCex( pFile, pCex );
288  else if ( Result == 1 ) // unsat
289  Gia_ManFromBridgeHolds( pFile, iPoProved );
290  else if ( Result == -1 ) // undef
291  Gia_ManFromBridgeUnknown( pFile, iPoProved );
292  else assert( 0 );
293  return 1;
294 }
Gia_ManFromBridgeUnknown
void Gia_ManFromBridgeUnknown(FILE *pFile, int iPoUnknown)
Definition: utilBridge.c:242
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManFromBridgeHolds
void Gia_ManFromBridgeHolds(FILE *pFile, int iPoProved)
Definition: utilBridge.c:229
Gia_ManFromBridgeCex
void Gia_ManFromBridgeCex(FILE *pFile, Abc_Cex_t *pCex)
Definition: utilBridge.c:254
Gia_ManBmc_t* Saig_Bmc3ManStart ( Aig_Man_t *  pAig,
int  nTimeOutOne 
)

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

Synopsis [Create manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 717 of file bmcBmc3.c.

718 {
719  Gia_ManBmc_t * p;
720  Aig_Obj_t * pObj;
721  int i;
722 // assert( Aig_ManRegNum(pAig) > 0 );
723  p = ABC_CALLOC( Gia_ManBmc_t, 1 );
724  p->pAig = pAig;
725  // create mapping
726  p->vMapping = Cnf_DeriveMappingArray( pAig );
727  p->vMapRefs = Saig_ManBmcComputeMappingRefs( pAig, p->vMapping );
728  // create sections
729 // p->vSects = Saig_ManBmcSections( pAig );
730  // map object IDs into their numbers and section numbers
731  p->nObjNums = 0;
732  p->vId2Num = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
733  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(Aig_ManConst1(pAig)), p->nObjNums++ );
734  Aig_ManForEachCi( pAig, pObj, i )
735  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
736  Aig_ManForEachNode( pAig, pObj, i )
737  if ( Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) > 0 )
738  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
739  Aig_ManForEachCo( pAig, pObj, i )
740  Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ );
741  p->vId2Var = Vec_PtrAlloc( 100 );
742  p->vTerInfo = Vec_PtrAlloc( 100 );
743  p->vVisited = Vec_WecAlloc( 100 );
744  // create solver
745  p->nSatVars = 1;
746  p->pSat = sat_solver_new();
747  sat_solver_setnvars( p->pSat, 1000 );
748  Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
749  // terminary simulation
750  p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
751  // hash table
752  p->vData = Vec_IntAlloc( 5 * 10000 );
753  p->vHash = Hsh_IntManStart( p->vData, 5, 10000 );
754  p->vId2Lit = Vec_IntAlloc( 10000 );
755  // time spent on each outputs
756  if ( nTimeOutOne )
757  {
758  p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
759  for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
760  p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
761  }
762  return p;
763 }
Vec_WecAlloc
static Vec_Wec_t * Vec_WecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWec.h:87
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Cnf_DeriveMappingArray
Vec_Int_t * Cnf_DeriveMappingArray(Aig_Man_t *pAig)
FUNCTION DECLARATIONS ///.
Definition: cnfCore.c:78
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition: cnfData.c:4537
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ManBmc_t
typedefABC_NAMESPACE_IMPL_START struct Gia_ManBmc_t_ Gia_ManBmc_t
DECLARATIONS ///.
Definition: bmcBmc3.c:34
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if
if(last==0)
Definition: sparse_int.h:34
Aig_Obj_t_
Definition: aig.h:69
Saig_ManBmcComputeMappingRefs
Vec_Int_t * Saig_ManBmcComputeMappingRefs(Aig_Man_t *p, Vec_Int_t *vMap)
Definition: bmcBmc3.c:686
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Hsh_IntManStart
static Hsh_IntMan_t * Hsh_IntManStart(Vec_Int_t *vData, int nSize, int nEntries)
FUNCTION DEFINITIONS ///.
Definition: vecHsh.h:109
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
void Saig_Bmc3ManStop ( Gia_ManBmc_t *  p)

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

Synopsis [Delete manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 776 of file bmcBmc3.c.

777 {
778  if ( p->pPars->fVerbose )
779  {
780  int nUsedVars = sat_solver_count_usedvars(p->pSat);
781  Abc_Print( 1, "LStart(P) = %d LDelta(Q) = %d LRatio(R) = %d ReduceDB = %d Vars = %d Used = %d (%.2f %%)\n",
782  p->pSat->nLearntStart, p->pSat->nLearntDelta, p->pSat->nLearntRatio,
783  p->pSat->nDBreduces, p->pSat->size, nUsedVars, 100.0*nUsedVars/p->pSat->size );
784  Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n",
785  p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
786  }
787 // Aig_ManCleanMarkA( p->pAig );
788  if ( p->vCexes )
789  {
790  assert( p->pAig->vSeqModelVec == NULL );
791  p->pAig->vSeqModelVec = p->vCexes;
792  p->vCexes = NULL;
793  }
794 // Vec_PtrFreeFree( p->vCexes );
795  Vec_WecFree( p->vVisited );
796  Vec_IntFree( p->vMapping );
797  Vec_IntFree( p->vMapRefs );
798 // Vec_VecFree( p->vSects );
799  Vec_IntFree( p->vId2Num );
800  Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
801  Vec_PtrFreeFree( p->vTerInfo );
802  sat_solver_delete( p->pSat );
803  ABC_FREE( p->pTime4Outs );
804  Vec_IntFree( p->vData );
805  Hsh_IntManStop( p->vHash );
806  Vec_IntFree( p->vId2Lit );
807  ABC_FREE( p->pSopSizes );
808  ABC_FREE( p->pSops[1] );
809  ABC_FREE( p->pSops );
810  ABC_FREE( p );
811 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_WecFree
static void Vec_WecFree(Vec_Wec_t *p)
Definition: vecWec.h:345
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Vec_PtrFreeFree
static void Vec_PtrFreeFree(Vec_Ptr_t *p)
Definition: vecPtr.h:569
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Hsh_IntManStop
static void Hsh_IntManStop(Hsh_IntMan_t *p)
Definition: vecHsh.h:119
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
sat_solver_count_usedvars
static int sat_solver_count_usedvars(sat_solver *s)
Definition: satSolver.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Saig_ManBmcAddClauses ( Gia_ManBmc_t *  p,
int  uTruth,
int  Lits[],
int  iLitOut 
)
inlinestatic

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 963 of file bmcBmc3.c.

964 {
965  int i, k, b, CutLit, nClaLits, ClaLits[5];
966  assert( uTruth > 0 && uTruth < 0xffff );
967  // write positive/negative polarity
968  for ( i = 0; i < 2; i++ )
969  {
970  if ( i )
971  uTruth = 0xffff & ~uTruth;
972 // Extra_PrintBinary( stdout, &uTruth, 16 ); Abc_Print( 1, "\n" );
973  for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
974  {
975  nClaLits = 0;
976  ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
977  CutLit = p->pSops[uTruth][k];
978  for ( b = 3; b >= 0; b-- )
979  {
980  if ( CutLit % 3 == 0 ) // value 0 --> write positive literal
981  {
982  assert( Lits[b] > 1 );
983  ClaLits[nClaLits++] = Lits[b];
984  }
985  else if ( CutLit % 3 == 1 ) // value 1 --> write negative literal
986  {
987  assert( Lits[b] > 1 );
988  ClaLits[nClaLits++] = lit_neg(Lits[b]);
989  }
990  CutLit = CutLit / 3;
991  }
992  if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
993  assert( 0 );
994  }
995  }
996 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
assert
#define assert(ex)
Definition: util_old.h:213
static int Saig_ManBmcCof0 ( int  t,
int  v 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 895 of file bmcBmc3.c.

896 {
897  static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
898  return 0xffff & ((t & ~s_Truth[v]) | ((t & ~s_Truth[v]) << (1<<v)));
899 }
static int Saig_ManBmcCof1 ( int  t,
int  v 
)
inlinestatic

Definition at line 900 of file bmcBmc3.c.

901 {
902  static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
903  return 0xffff & ((t & s_Truth[v]) | ((t & s_Truth[v]) >> (1<<v)));
904 }
static int Saig_ManBmcCofEqual ( int  t,
int  v 
)
inlinestatic

Definition at line 905 of file bmcBmc3.c.

906 {
907  assert( v >= 0 && v <= 3 );
908  if ( v == 0 )
909  return ((t & 0xAAAA) >> 1) == (t & 0x5555);
910  if ( v == 1 )
911  return ((t & 0xCCCC) >> 2) == (t & 0x3333);
912  if ( v == 2 )
913  return ((t & 0xF0F0) >> 4) == (t & 0x0F0F);
914  if ( v == 3 )
915  return ((t & 0xFF00) >> 8) == (t & 0x00FF);
916  return -1;
917 }
assert
#define assert(ex)
Definition: util_old.h:213
Vec_Int_t* Saig_ManBmcComputeMappingRefs ( Aig_Man_t *  p,
Vec_Int_t *  vMap 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 686 of file bmcBmc3.c.

687 {
688  Vec_Int_t * vRefs;
689  Aig_Obj_t * pObj;
690  int i, iFan, * pData;
691  vRefs = Vec_IntStart( Aig_ManObjNumMax(p) );
692  Aig_ManForEachCo( p, pObj, i )
693  Vec_IntAddToEntry( vRefs, Aig_ObjFaninId0(pObj), 1 );
694  Aig_ManForEachNode( p, pObj, i )
695  {
696  if ( Vec_IntEntry(vMap, i) == 0 )
697  continue;
698  pData = Vec_IntEntryP( vMap, Vec_IntEntry(vMap, i) );
699  for ( iFan = 0; iFan < 4; iFan++ )
700  if ( pData[iFan+1] >= 0 )
701  Vec_IntAddToEntry( vRefs, pData[iFan+1], 1 );
702  }
703  return vRefs;
704 }
Aig_ObjFaninId0
static int Aig_ObjFaninId0(Aig_Obj_t *pObj)
Definition: aig.h:304
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
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntAddToEntry
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_Obj_t_
Definition: aig.h:69
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
void Saig_ManBmcCountNonternary ( Aig_Man_t *  p,
Vec_Ptr_t *  vInfos,
int  iFrame 
)

Definition at line 281 of file bmcBmc3.c.

282 {
283  int i, * pCounters = ABC_CALLOC( int, iFrame + 1 );
284  unsigned * pInfo = (unsigned *)Vec_PtrEntry(vInfos, iFrame);
285  assert( Saig_ManBmcSimInfoGet( pInfo, Aig_ManCo(p, 0) ) == SAIG_TER_UND );
286  Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(Aig_ManCo(p, 0)), vInfos, pInfo, iFrame, pCounters );
287  for ( i = 0; i <= iFrame; i++ )
288  Abc_Print( 1, "%d=%d ", i, pCounters[i] );
289  Abc_Print( 1, "\n" );
290  ABC_FREE( pCounters );
291 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Saig_ManBmcCountNonternary_rec
int Saig_ManBmcCountNonternary_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vInfos, unsigned *pInfo, int f, int *pCounter)
Definition: bmcBmc3.c:263
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
assert
#define assert(ex)
Definition: util_old.h:213
int Saig_ManBmcCountNonternary_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vInfos,
unsigned *  pInfo,
int  f,
int *  pCounter 
)

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

Synopsis [Count the number of non-ternary per frame.]

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file bmcBmc3.c.

264 {
265  int Value = Saig_ManBmcSimInfoClear( pInfo, pObj );
266  if ( Value == SAIG_TER_NON )
267  return 0;
268  assert( f >= 0 );
269  pCounter[f] += (Value == SAIG_TER_UND);
270  if ( Saig_ObjIsPi(p, pObj) || (f == 0 && Saig_ObjIsLo(p, pObj)) || Aig_ObjIsConst1(pObj) )
271  return 0;
272  if ( Saig_ObjIsLi(p, pObj) )
273  return Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
274  if ( Saig_ObjIsLo(p, pObj) )
275  return Saig_ManBmcCountNonternary_rec( p, Saig_ObjLoToLi(p, pObj), vInfos, (unsigned *)Vec_PtrEntry(vInfos, f-1), f-1, pCounter );
276  assert( Aig_ObjIsNode(pObj) );
277  Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
278  Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin1(pObj), vInfos, pInfo, f, pCounter );
279  return 0;
280 }
Saig_ManBmcSimInfoClear
static int Saig_ManBmcSimInfoClear(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:118
SAIG_TER_NON
#define SAIG_TER_NON
FUNCTION DEFINITIONS ///.
Definition: bmcBmc3.c:83
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Saig_ManBmcCountNonternary_rec
int Saig_ManBmcCountNonternary_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vInfos, unsigned *pInfo, int f, int *pCounter)
Definition: bmcBmc3.c:263
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
assert
#define assert(ex)
Definition: util_old.h:213
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
int Saig_ManBmcCountRefed ( Aig_Man_t *  p,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Returns the number of nodes with ref counter more than 1.]

Description []

SideEffects []

SeeAlso []

Definition at line 532 of file bmcBmc3.c.

533 {
534  Aig_Obj_t * pObj;
535  int i, Counter = 0;
536  Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
537  {
538  assert( !Aig_IsComplement(pObj) );
539  Counter += (Aig_ObjRefs(pObj) > 1);
540  }
541  return Counter;
542 }
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Saig_ManBmcCreateCnf ( Gia_ManBmc_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1211 of file bmcBmc3.c.

1212 {
1213  Vec_Int_t * vVisit, * vVisit2;
1214  Aig_Obj_t * pTemp;
1215  int Lit, f, i;
1216  // perform ternary simulation
1217  int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame );
1218  if ( Value != SAIG_TER_UND )
1219  return (int)(Value == SAIG_TER_ONE);
1220  // construct CNF if value is ternary
1221 // Lit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
1222  Vec_WecClear( p->vVisited );
1223  vVisit = Vec_WecPushLevel( p->vVisited );
1224  Vec_IntPush( vVisit, Aig_ObjId(pObj) );
1225  for ( f = iFrame; f >= 0; f-- )
1226  {
1227  Aig_ManIncrementTravId( p->pAig );
1228  vVisit2 = Vec_WecPushLevel( p->vVisited );
1229  vVisit = Vec_WecEntry( p->vVisited, Vec_WecSize(p->vVisited)-2 );
1230  Aig_ManForEachObjVec( vVisit, p->pAig, pTemp, i )
1231  Saig_ManBmcCreateCnf_iter( p, pTemp, f, vVisit2 );
1232  if ( Vec_IntSize(vVisit2) == 0 )
1233  break;
1234  }
1235  Vec_WecForEachLevelReverse( p->vVisited, vVisit, f )
1236  Aig_ManForEachObjVec( vVisit, p->pAig, pTemp, i )
1237  Saig_ManBmcCreateCnf_rec( p, pTemp, iFrame-f );
1238  Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
1239  // extend the SAT solver
1240  if ( p->nSatVars > sat_solver_nvars(p->pSat) )
1241  sat_solver_setnvars( p->pSat, p->nSatVars );
1242  return Lit;
1243 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
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
Vec_WecPushLevel
static Vec_Int_t * Vec_WecPushLevel(Vec_Wec_t *p)
Definition: vecWec.h:284
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Saig_ManBmcCreateCnf_iter
void Saig_ManBmcCreateCnf_iter(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, Vec_Int_t *vVisit)
Definition: bmcBmc3.c:1096
Saig_ManBmcLiteral
static int Saig_ManBmcLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:843
Saig_ManBmcRunTerSim_rec
int Saig_ManBmcRunTerSim_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1136
Vec_WecSize
static int Vec_WecSize(Vec_Wec_t *p)
Definition: vecWec.h:193
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Vec_WecClear
static void Vec_WecClear(Vec_Wec_t *p)
Definition: vecWec.h:255
Saig_ManBmcCreateCnf_rec
int Saig_ManBmcCreateCnf_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1009
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
if
if(last==0)
Definition: sparse_int.h:34
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition: bmcBmc3.c:85
Vec_WecEntry
static Vec_Int_t * Vec_WecEntry(Vec_Wec_t *p, int i)
Definition: vecWec.h:142
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_WecForEachLevelReverse
#define Vec_WecForEachLevelReverse(vGlob, vVec, i)
Definition: vecWec.h:65
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
void Saig_ManBmcCreateCnf_iter ( Gia_ManBmc_t *  p,
Aig_Obj_t *  pObj,
int  iFrame,
Vec_Int_t *  vVisit 
)

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1096 of file bmcBmc3.c.

1097 {
1098  if ( Saig_ManBmcLiteral( p, pObj, iFrame ) != ~0 )
1099  return;
1100  if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
1101  return;
1102  Aig_ObjSetTravIdCurrent(p->pAig, pObj);
1103  if ( Aig_ObjIsCi(pObj) )
1104  {
1105  if ( Saig_ObjIsLo(p->pAig, pObj) )
1106  Vec_IntPush( vVisit, Saig_ObjLoToLi(p->pAig, pObj)->Id );
1107  return;
1108  }
1109  if ( Aig_ObjIsCo(pObj) )
1110  {
1111  Saig_ManBmcCreateCnf_iter( p, Aig_ObjFanin0(pObj), iFrame, vVisit );
1112  return;
1113  }
1114  else
1115  {
1116  int * pMapping, i;
1117  assert( Aig_ObjIsNode(pObj) );
1118  pMapping = Saig_ManBmcMapping( p, pObj );
1119  for ( i = 0; i < 4; i++ )
1120  if ( pMapping[i+1] != -1 )
1121  Saig_ManBmcCreateCnf_iter( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame, vVisit );
1122  }
1123 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Saig_ManBmcMapping
static int * Saig_ManBmcMapping(Gia_ManBmc_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:825
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Saig_ManBmcCreateCnf_iter
void Saig_ManBmcCreateCnf_iter(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, Vec_Int_t *vVisit)
Definition: bmcBmc3.c:1096
Saig_ManBmcLiteral
static int Saig_ManBmcLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:843
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
int Saig_ManBmcCreateCnf_rec ( Gia_ManBmc_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1009 of file bmcBmc3.c.

1010 {
1011  extern unsigned Dar_CutSortVars( unsigned uTruth, int * pVars );
1012  int * pMapping, i, iLit, Lits[5], uTruth;
1013  iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
1014  if ( iLit != ~0 )
1015  return iLit;
1016  assert( iFrame >= 0 );
1017  if ( Aig_ObjIsCi(pObj) )
1018  {
1019  if ( Saig_ObjIsPi(p->pAig, pObj) )
1020  iLit = toLit( p->nSatVars++ );
1021  else
1022  iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1 );
1023  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1024  }
1025  if ( Aig_ObjIsCo(pObj) )
1026  {
1027  iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame );
1028  if ( Aig_ObjFaninC0(pObj) )
1029  iLit = lit_neg(iLit);
1030  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1031  }
1032  assert( Aig_ObjIsNode(pObj) );
1033  pMapping = Saig_ManBmcMapping( p, pObj );
1034  for ( i = 0; i < 4; i++ )
1035  if ( pMapping[i+1] == -1 )
1036  Lits[i] = -1;
1037  else
1038  Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame );
1039  uTruth = 0xffff & (unsigned)pMapping[0];
1040  // propagate constants
1041  uTruth = Saig_ManBmcReduceTruth( uTruth, Lits );
1042  if ( uTruth == 0 || uTruth == 0xffff )
1043  {
1044  iLit = (uTruth == 0xffff);
1045  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1046  }
1047  // canonicize inputs
1048  uTruth = Dar_CutSortVars( uTruth, Lits );
1049  assert( uTruth != 0 && uTruth != 0xffff );
1050  if ( uTruth == 0xAAAA || uTruth == 0x5555 )
1051  {
1052  iLit = Abc_LitNotCond( Lits[0], uTruth == 0x5555 );
1053  p->nBufNum++;
1054  }
1055  else
1056  {
1057  int iEntry, iRes;
1058  int fCompl = (uTruth & 1);
1059  Lits[4] = (uTruth & 1) ? 0xffff & ~uTruth : uTruth;
1060  iEntry = Vec_IntSize(p->vData) / 5;
1061  assert( iEntry * 5 == Vec_IntSize(p->vData) );
1062  for ( i = 0; i < 5; i++ )
1063  Vec_IntPush( p->vData, Lits[i] );
1064  iRes = Hsh_IntManAdd( p->vHash, iEntry );
1065  if ( iRes == iEntry )
1066  {
1067  iLit = toLit( p->nSatVars++ );
1068  Saig_ManBmcAddClauses( p, Lits[4], Lits, iLit );
1069  assert( iEntry == Vec_IntSize(p->vId2Lit) );
1070  Vec_IntPush( p->vId2Lit, iLit );
1071  p->nHashMiss++;
1072  }
1073  else
1074  {
1075  iLit = Vec_IntEntry( p->vId2Lit, iRes );
1076  Vec_IntShrink( p->vData, Vec_IntSize(p->vData) - 5 );
1077  p->nHashHit++;
1078  }
1079  iLit = Abc_LitNotCond( iLit, fCompl );
1080  }
1081  return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
1082 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Saig_ManBmcMapping
static int * Saig_ManBmcMapping(Gia_ManBmc_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:825
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManObj
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
Saig_ManBmcLiteral
static int Saig_ManBmcLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:843
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Dar_CutSortVars
unsigned Dar_CutSortVars(unsigned uTruth, int *pVars)
Definition: darCut.c:521
toLit
static lit toLit(int v)
Definition: satVec.h:142
Saig_ManBmcCreateCnf_rec
int Saig_ManBmcCreateCnf_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1009
Saig_ManBmcSetLiteral
static int Saig_ManBmcSetLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, int iLit)
Definition: bmcBmc3.c:866
Saig_ManBmcAddClauses
static void Saig_ManBmcAddClauses(Gia_ManBmc_t *p, int uTruth, int Lits[], int iLitOut)
Definition: bmcBmc3.c:963
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Saig_ManBmcReduceTruth
static int Saig_ManBmcReduceTruth(int uTruth, int Lits[])
Definition: bmcBmc3.c:930
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Hsh_IntManAdd
static int Hsh_IntManAdd(Hsh_IntMan_t *p, int iData)
Definition: vecHsh.h:157
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
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
void Saig_ManBmcDfs_rec ( Aig_Man_t *  p,
Aig_Obj_t *  pObj,
Vec_Ptr_t *  vNodes 
)

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file bmcBmc3.c.

355 {
356  assert( !Aig_IsComplement(pObj) );
357  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
358  return;
359  Aig_ObjSetTravIdCurrent(p, pObj);
360  if ( Aig_ObjIsNode(pObj) )
361  {
362  Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
363  Saig_ManBmcDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
364  }
365  Vec_PtrPush( vNodes, pObj );
366 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Saig_ManBmcDfs_rec
void Saig_ManBmcDfs_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: bmcBmc3.c:354
assert
#define assert(ex)
Definition: util_old.h:213
Vec_Ptr_t* Saig_ManBmcDfsNodes ( Aig_Man_t *  p,
Vec_Ptr_t *  vRoots 
)

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

Synopsis [Collects internal nodes and PIs in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file bmcBmc3.c.

380 {
381  Vec_Ptr_t * vNodes;
382  Aig_Obj_t * pObj;
383  int i;
384  vNodes = Vec_PtrAlloc( 100 );
385  Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
386  Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
387  return vNodes;
388 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_Obj_t_
Definition: aig.h:69
Saig_ManBmcDfs_rec
void Saig_ManBmcDfs_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vNodes)
Definition: bmcBmc3.c:354
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
static int Saig_ManBmcLiteral ( Gia_ManBmc_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 843 of file bmcBmc3.c.

844 {
845  Vec_Int_t * vFrame;
846  int ObjNum;
847  assert( !Aig_ObjIsNode(pObj) || Saig_ManBmcMapping(p, pObj) );
848  ObjNum = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
849  assert( ObjNum >= 0 );
850  vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
851  assert( vFrame != NULL );
852  return Vec_IntEntry( vFrame, ObjNum );
853 }
Saig_ManBmcMapping
static int * Saig_ManBmcMapping(Gia_ManBmc_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:825
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
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
static int* Saig_ManBmcMapping ( Gia_ManBmc_t *  p,
Aig_Obj_t *  pObj 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 825 of file bmcBmc3.c.

826 {
827  if ( Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) == 0 )
828  return NULL;
829  return Vec_IntEntryP( p->vMapping, Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) );
830 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
void Saig_ManBmcMappingTest ( Aig_Man_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 666 of file bmcBmc3.c.

667 {
668  Vec_Int_t * vMapping;
669  vMapping = Cnf_DeriveMappingArray( p );
670  Saig_ManBmcWriteBlif( p, vMapping, "test.blif" );
671  Vec_IntFree( vMapping );
672 }
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
Saig_ManBmcWriteBlif
void Saig_ManBmcWriteBlif(Aig_Man_t *p, Vec_Int_t *vMapping, char *pFileName)
Definition: bmcBmc3.c:581
Cnf_DeriveMappingArray
Vec_Int_t * Cnf_DeriveMappingArray(Aig_Man_t *pAig)
FUNCTION DECLARATIONS ///.
Definition: cnfCore.c:78
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Saig_ManBmcReduceTruth ( int  uTruth,
int  Lits[] 
)
inlinestatic

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

Synopsis [Derives CNF for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 930 of file bmcBmc3.c.

931 {
932  int v;
933  for ( v = 0; v < 4; v++ )
934  if ( Lits[v] == 0 )
935  {
936  uTruth = Saig_ManBmcCof0(uTruth, v);
937  Lits[v] = -1;
938  }
939  else if ( Lits[v] == 1 )
940  {
941  uTruth = Saig_ManBmcCof1(uTruth, v);
942  Lits[v] = -1;
943  }
944  for ( v = 0; v < 4; v++ )
945  if ( Lits[v] == -1 )
946  assert( Saig_ManBmcCofEqual(uTruth, v) );
947  else if ( Saig_ManBmcCofEqual(uTruth, v) )
948  Lits[v] = -1;
949  return uTruth;
950 }
Saig_ManBmcCof1
static int Saig_ManBmcCof1(int t, int v)
Definition: bmcBmc3.c:900
Saig_ManBmcCofEqual
static int Saig_ManBmcCofEqual(int t, int v)
Definition: bmcBmc3.c:905
Saig_ManBmcCof0
static int Saig_ManBmcCof0(int t, int v)
Definition: bmcBmc3.c:895
assert
#define assert(ex)
Definition: util_old.h:213
int Saig_ManBmcRunTerSim_rec ( Gia_ManBmc_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Recursively performs terminary simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1136 of file bmcBmc3.c.

1137 {
1138  unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
1139  int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
1140  if ( Value != SAIG_TER_NON )
1141  {
1142 /*
1143  // check the value of this literal in the SAT solver
1144  if ( Value == SAIG_TER_UND && Saig_ManBmcMapping(p, pObj) )
1145  {
1146  int Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
1147  if ( Lit >= 0 )
1148  {
1149  assert( Lit >= 2 );
1150  if ( p->pSat->assigns[Abc_Lit2Var(Lit)] < 2 )
1151  {
1152  p->nUniProps++;
1153  if ( Abc_LitIsCompl(Lit) ^ (p->pSat->assigns[Abc_Lit2Var(Lit)] == 0) )
1154  Value = SAIG_TER_ONE;
1155  else
1156  Value = SAIG_TER_ZER;
1157 
1158 // Value = SAIG_TER_UND; // disable!
1159 
1160  // use the new value
1161  Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
1162  // transfer to the unrolling
1163  if ( Value != SAIG_TER_UND )
1164  Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
1165  }
1166  }
1167  }
1168 */
1169  return Value;
1170  }
1171  if ( Aig_ObjIsCo(pObj) )
1172  {
1173  Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
1174  if ( Aig_ObjFaninC0(pObj) )
1175  Value = Saig_ManBmcSimInfoNot( Value );
1176  }
1177  else if ( Saig_ObjIsLo(p->pAig, pObj) )
1178  {
1179  assert( iFrame > 0 );
1180  Value = Saig_ManBmcRunTerSim_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame - 1 );
1181  }
1182  else if ( Aig_ObjIsNode(pObj) )
1183  {
1184  Val0 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
1185  Val1 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin1(pObj), iFrame );
1186  if ( Aig_ObjFaninC0(pObj) )
1187  Val0 = Saig_ManBmcSimInfoNot( Val0 );
1188  if ( Aig_ObjFaninC1(pObj) )
1189  Val1 = Saig_ManBmcSimInfoNot( Val1 );
1190  Value = Saig_ManBmcSimInfoAnd( Val0, Val1 );
1191  }
1192  else assert( 0 );
1193  Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
1194  // transfer to the unrolling
1195  if ( Saig_ManBmcMapping(p, pObj) && Value != SAIG_TER_UND )
1196  Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
1197  return Value;
1198 }
SAIG_TER_NON
#define SAIG_TER_NON
FUNCTION DEFINITIONS ///.
Definition: bmcBmc3.c:83
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Saig_ManBmcMapping
static int * Saig_ManBmcMapping(Gia_ManBmc_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:825
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Saig_ManBmcRunTerSim_rec
int Saig_ManBmcRunTerSim_rec(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1136
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Saig_ManBmcSimInfoAnd
static int Saig_ManBmcSimInfoAnd(int Value0, int Value1)
Definition: bmcBmc3.c:97
Saig_ManBmcSimInfoSet
static void Saig_ManBmcSimInfoSet(unsigned *pInfo, Aig_Obj_t *pObj, int Value)
Definition: bmcBmc3.c:111
Saig_ManBmcSimInfoNot
static int Saig_ManBmcSimInfoNot(int Value)
Definition: bmcBmc3.c:88
Saig_ManBmcSetLiteral
static int Saig_ManBmcSetLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, int iLit)
Definition: bmcBmc3.c:866
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition: bmcBmc3.c:85
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
int Saig_ManBmcScalable ( Aig_Man_t *  pAig,
Saig_ParBmc_t *  pPars 
)

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

Synopsis [Bounded model checking engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 1390 of file bmcBmc3.c.

1391 {
1392  Gia_ManBmc_t * p;
1393  Aig_Obj_t * pObj;
1394  Abc_Cex_t * pCexNew, * pCexNew0;
1395  FILE * pLogFile = NULL;
1396  unsigned * pInfo;
1397  int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
1398  int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
1399  int i, f, k, Lit, status;
1400  abctime clk, clk2, clkSatRun, clkOther = 0, clkTotal = Abc_Clock();
1401  abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
1402  abctime nTimeToStopNG, nTimeToStop;
1403  if ( pPars->pLogFileName )
1404  pLogFile = fopen( pPars->pLogFileName, "wb" );
1405  if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
1406  pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
1407  if ( pPars->nTimeOutOne && !pPars->fSolveAll )
1408  pPars->nTimeOutOne = 0;
1409  nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
1410  nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
1411  // create BMC manager
1412  p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
1413  p->pPars = pPars;
1414  p->pSat->nLearntStart = p->pPars->nLearnedStart;
1415  p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
1416  p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
1417  p->pSat->nLearntMax = p->pSat->nLearntStart;
1418  if ( pPars->fSolveAll && p->vCexes == NULL )
1419  p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
1420  if ( pPars->fVerbose )
1421  {
1422  Abc_Print( 1, "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d.\n",// Sect =%3d.\n",
1423  Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
1424  Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums );//, Vec_VecSize(p->vSects) );
1425  Abc_Print( 1, "Params: FramesMax = %d. Start = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n",
1426  pPars->nFramesMax, pPars->nStart, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
1427  }
1428  pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
1429  // set runtime limit
1430  if ( nTimeToStop )
1431  sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
1432  // perform frames
1433  Aig_ManRandom( 1 );
1434  pPars->timeLastSolved = Abc_Clock();
1435  for ( f = 0; f < pPars->nFramesMax; f++ )
1436  {
1437  // stop BMC after exploring all reachable states
1438  if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
1439  {
1440  Abc_Print( 1, "Stopping BMC because all 2^%d reachable states are visited.\n", Aig_ManRegNum(pAig) );
1441  if ( p->pPars->fUseBridge )
1442  Saig_ManForEachPo( pAig, pObj, i )
1443  if ( !(p->vCexes && Vec_PtrEntry(p->vCexes, i)) && !(p->pTime4Outs && p->pTime4Outs[i] == 0) ) // not SAT and not timed out
1444  Gia_ManToBridgeResult( stdout, 1, NULL, i );
1445  RetValue = pPars->nFailOuts ? 0 : 1;
1446  goto finish;
1447  }
1448  // stop BMC if all targets are solved
1449  if ( pPars->fSolveAll && pPars->nFailOuts + pPars->nDropOuts >= Saig_ManPoNum(pAig) )
1450  {
1451  Abc_Print( 1, "Stopping BMC because all targets are disproved or timed out.\n" );
1452  RetValue = pPars->nFailOuts ? 0 : 1;
1453  goto finish;
1454  }
1455  // consider the next timeframe
1456  if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
1457  pPars->iFrame = f-1;
1458  // map nodes of this section
1459  Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
1460  Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) );
1461 /*
1462  // cannot remove mapping of frame values for any timeframes
1463  // because with constant propagation they may be needed arbitrarily far
1464  if ( f > 2*Vec_VecSize(p->vSects) )
1465  {
1466  int iFrameOld = f - 2*Vec_VecSize( p->vSects );
1467  void * pMemory = Vec_IntReleaseArray( Vec_PtrEntry(p->vId2Var, iFrameOld) );
1468  ABC_FREE( pMemory );
1469  }
1470 */
1471  // prepare some nodes
1472  Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 );
1473  Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE );
1474  Saig_ManForEachPi( pAig, pObj, i )
1475  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
1476  if ( f == 0 )
1477  {
1478  Saig_ManForEachLo( p->pAig, pObj, i )
1479  {
1480  Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
1481  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
1482  }
1483  }
1484  if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
1485  continue;
1486  // create CNF upfront
1487  if ( pPars->fSolveAll )
1488  {
1489  Saig_ManForEachPo( pAig, pObj, i )
1490  {
1491  if ( i >= Saig_ManPoNum(pAig) )
1492  break;
1493  // check for timeout
1494  if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
1495  {
1496  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
1497  goto finish;
1498  }
1499  if ( nTimeToStop && Abc_Clock() > nTimeToStop )
1500  {
1501  if ( !pPars->fSilent )
1502  Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
1503  goto finish;
1504  }
1505  // skip solved outputs
1506  if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
1507  continue;
1508  // skip output whose time has run out
1509  if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
1510  continue;
1511  // add constraints for this output
1512 clk2 = Abc_Clock();
1513  Saig_ManBmcCreateCnf( p, pObj, f );
1514 clkOther += Abc_Clock() - clk2;
1515  }
1516  }
1517  // solve SAT
1518  clk = Abc_Clock();
1519  Saig_ManForEachPo( pAig, pObj, i )
1520  {
1521  if ( i >= Saig_ManPoNum(pAig) )
1522  break;
1523  // check for timeout
1524  if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
1525  {
1526  Abc_Print( 1, "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
1527  goto finish;
1528  }
1529  if ( nTimeToStop && Abc_Clock() > nTimeToStop )
1530  {
1531  if ( !pPars->fSilent )
1532  Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
1533  goto finish;
1534  }
1535  // skip solved outputs
1536  if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
1537  continue;
1538  // skip output whose time has run out
1539  if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
1540  continue;
1541  // add constraints for this output
1542 clk2 = Abc_Clock();
1543  Lit = Saig_ManBmcCreateCnf( p, pObj, f );
1544 clkOther += Abc_Clock() - clk2;
1545  // solve this output
1546  fUnfinished = 0;
1547  sat_solver_compress( p->pSat );
1548  if ( p->pTime4Outs )
1549  {
1550  assert( p->pTime4Outs[i] > 0 );
1551  clkOne = Abc_Clock();
1552  sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
1553  }
1554 clk2 = Abc_Clock();
1555  status = Saig_ManCallSolver( p, Lit );
1556 clkSatRun = Abc_Clock() - clk2;
1557  if ( pLogFile )
1558  fprintf( pLogFile, "Frame %5d Output %5d Time(ms) %8d %8d\n", f, i,
1559  Lit < 2 ? 0 : (int)(clkSatRun * 1000 / CLOCKS_PER_SEC),
1560  Lit < 2 ? 0 : Abc_MaxInt(0, Abc_MinInt(pPars->nTimeOutOne, pPars->nTimeOutOne - (int)((p->pTime4Outs[i] - clkSatRun) * 1000 / CLOCKS_PER_SEC))) );
1561  if ( p->pTime4Outs )
1562  {
1563  abctime timeSince = Abc_Clock() - clkOne;
1564  assert( p->pTime4Outs[i] > 0 );
1565  p->pTime4Outs[i] = (p->pTime4Outs[i] > timeSince) ? p->pTime4Outs[i] - timeSince : 0;
1566  if ( p->pTime4Outs[i] == 0 && status != l_True )
1567  pPars->nDropOuts++;
1568  }
1569  if ( status == l_False )
1570  {
1571 nTimeUnsat += clkSatRun;
1572  if ( Lit != 0 )
1573  {
1574  // add final unit clause
1575  Lit = lit_neg( Lit );
1576  status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
1577  assert( status );
1578  // add learned units
1579  for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
1580  {
1581  Lit = veci_begin(&p->pSat->unit_lits)[k];
1582  status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
1583  assert( status );
1584  }
1585  veci_resize(&p->pSat->unit_lits, 0);
1586  // propagate units
1587  sat_solver_compress( p->pSat );
1588  }
1589  if ( p->pPars->fUseBridge )
1590  Gia_ManReportProgress( stdout, i, f );
1591  }
1592  else if ( status == l_True )
1593  {
1594 nTimeSat += clkSatRun;
1595  RetValue = 0;
1596  fFirst = 0;
1597  if ( !pPars->fSolveAll )
1598  {
1599  if ( pPars->fVerbose )
1600  {
1601  Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
1602  Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
1603  Abc_Print( 1, "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
1604  Abc_Print( 1, "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
1605 // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
1606  Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
1607 // ABC_PRT( "Time", Abc_Clock() - clk );
1608  Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) );
1609  Abc_Print( 1, "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
1610  Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
1611 // Abc_Print( 1, "\n" );
1612 // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
1613 // ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
1614 // Abc_Print( 1, "S =%6d. ", p->nBufNum );
1615 // Abc_Print( 1, "D =%6d. ", p->nDupNum );
1616  Abc_Print( 1, "\n" );
1617  fflush( stdout );
1618  }
1619  ABC_FREE( pAig->pSeqModel );
1620  pAig->pSeqModel = Saig_ManGenerateCex( p, f, i );
1621  goto finish;
1622  }
1623  pPars->nFailOuts++;
1624  if ( !pPars->fNotVerbose )
1625  Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
1626  nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
1627  if ( p->vCexes == NULL )
1628  p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
1629  pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
1630  pCexNew0 = NULL;
1631  if ( p->pPars->fUseBridge )
1632  {
1633  Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
1634  //Abc_CexFree( pCexNew );
1635  pCexNew0 = pCexNew;
1636  pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1;
1637  }
1638  Vec_PtrWriteEntry( p->vCexes, i, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
1639  if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
1640  {
1641  Abc_CexFreeP( &pCexNew0 );
1642  Abc_Print( 1, "Quitting due to callback on fail.\n" );
1643  goto finish;
1644  }
1645  // reset the timeout
1646  pPars->timeLastSolved = Abc_Clock();
1647  nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
1648  if ( nTimeToStop )
1649  sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
1650 
1651  // check if other outputs failed under the same counter-example
1652  Saig_ManForEachPo( pAig, pObj, k )
1653  {
1654  if ( k >= Saig_ManPoNum(pAig) )
1655  break;
1656  // skip solved outputs
1657  if ( p->vCexes && Vec_PtrEntry(p->vCexes, k) )
1658  continue;
1659  // check if this output is solved
1660  Lit = Saig_ManBmcCreateCnf( p, pObj, f );
1661  if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
1662  continue;
1663  // write entry
1664  pPars->nFailOuts++;
1665  if ( !pPars->fNotVerbose )
1666  Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
1667  nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
1668  // report to the bridge
1669  if ( p->pPars->fUseBridge )
1670  {
1671  // set the output number
1672  pCexNew0->iPo = k;
1673  Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
1674  }
1675  // remember solved output
1676  Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
1677  }
1678  Abc_CexFreeP( &pCexNew0 );
1679  Abc_CexFree( pCexNew );
1680  }
1681  else
1682  {
1683 nTimeUndec += clkSatRun;
1684  assert( status == l_Undef );
1685  if ( pPars->nFramesJump )
1686  {
1687  pPars->nConfLimit = pPars->nConfLimitJump;
1688  nJumpFrame = f + pPars->nFramesJump;
1689  fUnfinished = 1;
1690  break;
1691  }
1692  if ( p->pTime4Outs == NULL )
1693  goto finish;
1694  }
1695  }
1696  if ( pPars->fVerbose )
1697  {
1698  if ( fFirst == 1 && f > 0 && p->pSat->stats.conflicts > 1 )
1699  {
1700  fFirst = 0;
1701 // Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
1702  }
1703  Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
1704  Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
1705 // Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
1706  Abc_Print( 1, "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
1707  Abc_Print( 1, "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
1708 // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
1709  Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
1710  if ( pPars->fSolveAll )
1711  Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
1712  if ( pPars->nTimeOutOne )
1713  Abc_Print( 1, "T/O =%4d. ", pPars->nDropOuts );
1714 // ABC_PRT( "Time", Abc_Clock() - clk );
1715 // Abc_Print( 1, "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) );
1716  Abc_Print( 1, "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) );
1717  Abc_Print( 1, "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
1718 // Abc_Print( 1, " %6d %6d ", p->nLitUsed, p->nLitUseless );
1719  Abc_Print( 1, "%9.2f sec ", 1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
1720 // Abc_Print( 1, "\n" );
1721 // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
1722 // ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
1723 // Abc_Print( 1, "Simples = %6d. ", p->nBufNum );
1724 // Abc_Print( 1, "Dups = %6d. ", p->nDupNum );
1725  Abc_Print( 1, "\n" );
1726  fflush( stdout );
1727  }
1728  }
1729  // consider the next timeframe
1730  if ( nJumpFrame && pPars->nStart == 0 )
1731  pPars->iFrame = nJumpFrame - pPars->nFramesJump;
1732  else if ( RetValue == -1 && pPars->nStart == 0 )
1733  pPars->iFrame = f-1;
1734 //ABC_PRT( "CNF generation runtime", clkOther );
1735 finish:
1736  if ( pPars->fVerbose )
1737  {
1738  Abc_Print( 1, "Runtime: " );
1739  Abc_Print( 1, "CNF = %.1f sec (%.1f %%) ", 1.0*clkOther/CLOCKS_PER_SEC, 100.0*clkOther/(Abc_Clock() - clkTotal) );
1740  Abc_Print( 1, "UNSAT = %.1f sec (%.1f %%) ", 1.0*nTimeUnsat/CLOCKS_PER_SEC, 100.0*nTimeUnsat/(Abc_Clock() - clkTotal) );
1741  Abc_Print( 1, "SAT = %.1f sec (%.1f %%) ", 1.0*nTimeSat/CLOCKS_PER_SEC, 100.0*nTimeSat/(Abc_Clock() - clkTotal) );
1742  Abc_Print( 1, "UNDEC = %.1f sec (%.1f %%)", 1.0*nTimeUndec/CLOCKS_PER_SEC, 100.0*nTimeUndec/(Abc_Clock() - clkTotal) );
1743  Abc_Print( 1, "\n" );
1744  }
1745  Saig_Bmc3ManStop( p );
1746  fflush( stdout );
1747  if ( pLogFile )
1748  fclose( pLogFile );
1749  return RetValue;
1750 }
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Saig_ParBmc_t_::nConfLimitJump
int nConfLimitJump
Definition: bmc.h:51
Saig_ManCallSolver
int Saig_ManCallSolver(Gia_ManBmc_t *p, int Lit)
Definition: bmcBmc3.c:1370
Saig_ParBmc_t_::nDropOuts
int nDropOuts
Definition: bmc.h:72
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Saig_ManGenerateCex
Abc_Cex_t * Saig_ManGenerateCex(Gia_ManBmc_t *p, int f, int i)
Definition: bmcBmc3.c:1343
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Saig_ParBmc_t_::nLearnedStart
int nLearnedStart
Definition: bmc.h:63
sat_solver_compress
static void sat_solver_compress(sat_solver *s)
Definition: satSolver.h:217
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Saig_ParBmc_t_::nTimeOutOne
int nTimeOutOne
Definition: bmc.h:55
Saig_ParBmc_t_::fVerbose
int fVerbose
Definition: bmc.h:66
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
l_True
#define l_True
Definition: SolverTypes.h:84
Saig_ParBmc_t_::nFailOuts
int nFailOuts
Definition: bmc.h:71
Saig_ParBmc_t_::nStart
int nStart
Definition: bmc.h:48
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Saig_ParBmc_t_::pFuncOnFail
int(* pFuncOnFail)(int, Abc_Cex_t *)
Definition: bmc.h:74
Saig_ParBmc_t_::nTimeOutGap
int nTimeOutGap
Definition: bmc.h:54
Saig_ParBmc_t_::iFrame
int iFrame
Definition: bmc.h:70
veci_resize
static void veci_resize(veci *v, int k)
Definition: satVec.h:47
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Saig_ParBmc_t_::nConfLimit
int nConfLimit
Definition: bmc.h:50
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
sat_solver_memory
double sat_solver_memory(sat_solver *s)
Definition: satSolver.c:1236
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
sat_solver_count_assigned
int sat_solver_count_assigned(sat_solver *s)
Definition: satSolver.c:609
Aig_ManNodeNum
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Saig_ParBmc_t_::nTimeOut
int nTimeOut
Definition: bmc.h:53
lit_neg
static lit lit_neg(lit l)
Definition: satVec.h:144
Saig_ParBmc_t_::nFramesMax
int nFramesMax
Definition: bmc.h:49
Saig_ParBmc_t_::timeLastSolved
abctime timeLastSolved
Definition: bmc.h:73
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Saig_ManBmcSimInfoSet
static void Saig_ManBmcSimInfoSet(unsigned *pInfo, Aig_Obj_t *pObj, int Value)
Definition: bmcBmc3.c:111
Saig_Bmc3ManStart
Gia_ManBmc_t * Saig_Bmc3ManStart(Aig_Man_t *pAig, int nTimeOutOne)
Definition: bmcBmc3.c:717
Saig_Bmc3ManStop
void Saig_Bmc3ManStop(Gia_ManBmc_t *p)
Definition: bmcBmc3.c:776
Saig_ParBmc_t_::nFramesJump
int nFramesJump
Definition: bmc.h:52
Saig_ParBmc_t_::fStoreCex
int fStoreCex
Definition: bmc.h:58
Saig_ManBmcSetLiteral
static int Saig_ManBmcSetLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame, int iLit)
Definition: bmcBmc3.c:866
Gia_ManBmc_t
typedefABC_NAMESPACE_IMPL_START struct Gia_ManBmc_t_ Gia_ManBmc_t
DECLARATIONS ///.
Definition: bmcBmc3.c:34
Abc_Base10Log
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition: utilCex.c:350
Saig_ParBmc_t_::fNotVerbose
int fNotVerbose
Definition: bmc.h:67
if
if(last==0)
Definition: sparse_int.h:34
Aig_Obj_t_
Definition: aig.h:69
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition: bmcBmc3.c:85
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManLevelNum
int Aig_ManLevelNum(Aig_Man_t *p)
Definition: aigDfs.c:486
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Saig_ManBmcTimeToStop
abctime Saig_ManBmcTimeToStop(Saig_ParBmc_t *pPars, abctime nTimeToStopNG)
Definition: bmcBmc3.c:1319
Saig_ParBmc_t_::fSilent
int fSilent
Definition: bmc.h:69
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_CexDup
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition: utilCex.c:145
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
l_False
#define l_False
Definition: SolverTypes.h:85
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Saig_ParBmc_t_::pLogFileName
char * pLogFileName
Definition: bmc.h:68
Saig_ManBmcCreateCnf
int Saig_ManBmcCreateCnf(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:1211
Gia_ManReportProgress
void Gia_ManReportProgress(FILE *pFile, int prop_no, int depth)
Definition: bmcBmc3.c:71
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
veci_begin
static int * veci_begin(veci *v)
Definition: satVec.h:45
SAIG_TER_ZER
#define SAIG_TER_ZER
Definition: bmcBmc3.c:84
veci_size
static int veci_size(veci *v)
Definition: satVec.h:46
Gia_ManToBridgeResult
int Gia_ManToBridgeResult(FILE *pFile, int Result, Abc_Cex_t *pCex, int iPoProved)
DECLARATIONS ///.
Definition: utilBridge.c:284
Saig_ParBmc_t_::fSolveAll
int fSolveAll
Definition: bmc.h:57
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Vec_Vec_t* Saig_ManBmcSections ( Aig_Man_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file bmcBmc3.c.

402 {
403  Vec_Ptr_t * vSects, * vRoots, * vCone;
404  Aig_Obj_t * pObj, * pObjPo;
405  int i;
406  Aig_ManIncrementTravId( p );
407  Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
408  // start the roots
409  vRoots = Vec_PtrAlloc( 1000 );
410  Saig_ManForEachPo( p, pObjPo, i )
411  {
412  Aig_ObjSetTravIdCurrent( p, pObjPo );
413  Vec_PtrPush( vRoots, pObjPo );
414  }
415  // compute the cones
416  vSects = Vec_PtrAlloc( 20 );
417  while ( Vec_PtrSize(vRoots) > 0 )
418  {
419  vCone = Saig_ManBmcDfsNodes( p, vRoots );
420  Vec_PtrPush( vSects, vCone );
421  // get the next set of roots
422  Vec_PtrClear( vRoots );
423  Vec_PtrForEachEntry( Aig_Obj_t *, vCone, pObj, i )
424  {
425  if ( !Saig_ObjIsLo(p, pObj) )
426  continue;
427  pObjPo = Saig_ObjLoToLi( p, pObj );
428  if ( Aig_ObjIsTravIdCurrent(p, pObjPo) )
429  continue;
430  Aig_ObjSetTravIdCurrent( p, pObjPo );
431  Vec_PtrPush( vRoots, pObjPo );
432  }
433  }
434  Vec_PtrFree( vRoots );
435  return (Vec_Vec_t *)vSects;
436 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_Obj_t_
Definition: aig.h:69
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManBmcDfsNodes
Vec_Ptr_t * Saig_ManBmcDfsNodes(Aig_Man_t *p, Vec_Ptr_t *vRoots)
Definition: bmcBmc3.c:379
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Saig_ManBmcSectionsTest ( Aig_Man_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 449 of file bmcBmc3.c.

450 {
451  Vec_Vec_t * vSects;
452  Vec_Ptr_t * vOne;
453  int i;
454  vSects = Saig_ManBmcSections( p );
455  Vec_VecForEachLevel( vSects, vOne, i )
456  Abc_Print( 1, "%d=%d ", i, Vec_PtrSize(vOne) );
457  Abc_Print( 1, "\n" );
458  Vec_VecFree( vSects );
459 }
Vec_VecForEachLevel
#define Vec_VecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition: vecVec.h:55
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Vec_VecFree
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Saig_ManBmcSections
Vec_Vec_t * Saig_ManBmcSections(Aig_Man_t *p)
Definition: bmcBmc3.c:401
static int Saig_ManBmcSetLiteral ( Gia_ManBmc_t *  p,
Aig_Obj_t *  pObj,
int  iFrame,
int  iLit 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 866 of file bmcBmc3.c.

867 {
868  Vec_Int_t * vFrame;
869  int ObjNum;
870  assert( !Aig_ObjIsNode(pObj) || Saig_ManBmcMapping(p, pObj) );
871  ObjNum = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
872  vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
873  Vec_IntWriteEntry( vFrame, ObjNum, iLit );
874 /*
875  if ( Vec_IntEntry( p->vMapRefs, Aig_ObjId(pObj) ) > 1 )
876  p->nLitUsed++;
877  else
878  p->nLitUseless++;
879 */
880  return iLit;
881 }
Saig_ManBmcMapping
static int * Saig_ManBmcMapping(Gia_ManBmc_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:825
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
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
static int Saig_ManBmcSimInfoAnd ( int  Value0,
int  Value1 
)
inlinestatic

Definition at line 97 of file bmcBmc3.c.

98 {
99  if ( Value0 == SAIG_TER_ZER || Value1 == SAIG_TER_ZER )
100  return SAIG_TER_ZER;
101  if ( Value0 == SAIG_TER_ONE && Value1 == SAIG_TER_ONE )
102  return SAIG_TER_ONE;
103  return SAIG_TER_UND;
104 }
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition: bmcBmc3.c:85
SAIG_TER_ZER
#define SAIG_TER_ZER
Definition: bmcBmc3.c:84
static int Saig_ManBmcSimInfoClear ( unsigned *  pInfo,
Aig_Obj_t *  pObj 
)
inlinestatic

Definition at line 118 of file bmcBmc3.c.

119 {
120  int Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
121  pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
122  return Value;
123 }
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
static int Saig_ManBmcSimInfoGet ( unsigned *  pInfo,
Aig_Obj_t *  pObj 
)
inlinestatic

Definition at line 106 of file bmcBmc3.c.

107 {
108  return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
109 }
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
static int Saig_ManBmcSimInfoNot ( int  Value)
inlinestatic

Definition at line 88 of file bmcBmc3.c.

89 {
90  if ( Value == SAIG_TER_ZER )
91  return SAIG_TER_ONE;
92  if ( Value == SAIG_TER_ONE )
93  return SAIG_TER_ZER;
94  return SAIG_TER_UND;
95 }
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition: bmcBmc3.c:85
SAIG_TER_ZER
#define SAIG_TER_ZER
Definition: bmcBmc3.c:84
static void Saig_ManBmcSimInfoSet ( unsigned *  pInfo,
Aig_Obj_t *  pObj,
int  Value 
)
inlinestatic

Definition at line 111 of file bmcBmc3.c.

112 {
113  assert( Value >= SAIG_TER_ZER && Value <= SAIG_TER_UND );
114  Value ^= Saig_ManBmcSimInfoGet( pInfo, pObj );
115  pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
116 }
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
SAIG_TER_ZER
#define SAIG_TER_ZER
Definition: bmcBmc3.c:84
Vec_Ptr_t* Saig_ManBmcSupergate ( Aig_Man_t *  p,
int  iPo 
)

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

Synopsis [Collect the topmost supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file bmcBmc3.c.

499 {
500  Vec_Ptr_t * vSuper;
501  Aig_Obj_t * pObj;
502  vSuper = Vec_PtrAlloc( 10 );
503  pObj = Aig_ManCo( p, iPo );
504  pObj = Aig_ObjChild0( pObj );
505  if ( !Aig_IsComplement(pObj) )
506  {
507  Vec_PtrPush( vSuper, pObj );
508  return vSuper;
509  }
510  pObj = Aig_Regular( pObj );
511  if ( !Aig_ObjIsNode(pObj) )
512  {
513  Vec_PtrPush( vSuper, pObj );
514  return vSuper;
515  }
516  Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
517  Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
518  return vSuper;
519 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Saig_ManBmcSupergate_rec
void Saig_ManBmcSupergate_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition: bmcBmc3.c:474
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_Obj_t_
Definition: aig.h:69
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
void Saig_ManBmcSupergate_rec ( Aig_Obj_t *  pObj,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 474 of file bmcBmc3.c.

475 {
476  // if the new node is complemented or a PI, another gate begins
477  if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ) // || (Aig_ObjRefs(pObj) > 1) )
478  {
479  Vec_PtrPushUnique( vSuper, Aig_Regular(pObj) );
480  return;
481  }
482  // go through the branches
483  Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
484  Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
485 }
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Saig_ManBmcSupergate_rec
void Saig_ManBmcSupergate_rec(Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
Definition: bmcBmc3.c:474
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
void Saig_ManBmcSupergateTest ( Aig_Man_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 555 of file bmcBmc3.c.

556 {
557  Vec_Ptr_t * vSuper;
558  Aig_Obj_t * pObj;
559  int i;
560  Abc_Print( 1, "Supergates: " );
561  Saig_ManForEachPo( p, pObj, i )
562  {
563  vSuper = Saig_ManBmcSupergate( p, i );
564  Abc_Print( 1, "%d=%d(%d) ", i, Vec_PtrSize(vSuper), Saig_ManBmcCountRefed(p, vSuper) );
565  Vec_PtrFree( vSuper );
566  }
567  Abc_Print( 1, "\n" );
568 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Saig_ManBmcCountRefed
int Saig_ManBmcCountRefed(Aig_Man_t *p, Vec_Ptr_t *vSuper)
Definition: bmcBmc3.c:532
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_Obj_t_
Definition: aig.h:69
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Saig_ManBmcSupergate
Vec_Ptr_t * Saig_ManBmcSupergate(Aig_Man_t *p, int iPo)
Definition: bmcBmc3.c:498
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Vec_Ptr_t* Saig_ManBmcTerSim ( Aig_Man_t *  p)

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

Synopsis [Collects internal nodes and PIs in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file bmcBmc3.c.

210 {
211  Vec_Ptr_t * vInfos;
212  unsigned * pInfo = NULL;
213  int i, TerPrev = ABC_INFINITY, TerCur, CountIncrease = 0;
214  vInfos = Vec_PtrAlloc( 100 );
215  for ( i = 0; i < 1000 && CountIncrease < 5 && TerPrev > 0; i++ )
216  {
217  TerCur = Saig_ManBmcTerSimCount01( p, pInfo );
218  if ( TerCur >= TerPrev )
219  CountIncrease++;
220  TerPrev = TerCur;
221  pInfo = Saig_ManBmcTerSimOne( p, pInfo );
222  Vec_PtrPush( vInfos, pInfo );
223  }
224  return vInfos;
225 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Saig_ManBmcTerSimCount01
int Saig_ManBmcTerSimCount01(Aig_Man_t *p, unsigned *pInfo)
Definition: bmcBmc3.c:136
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Saig_ManBmcTerSimOne
unsigned * Saig_ManBmcTerSimOne(Aig_Man_t *p, unsigned *pPrev)
Definition: bmcBmc3.c:159
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
int Saig_ManBmcTerSimCount01 ( Aig_Man_t *  p,
unsigned *  pInfo 
)

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

Synopsis [Returns the number of LIs with binary ternary info.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file bmcBmc3.c.

137 {
138  Aig_Obj_t * pObj;
139  int i, Counter = 0;
140  if ( pInfo == NULL )
141  return Saig_ManRegNum(p);
142  Saig_ManForEachLi( p, pObj, i )
143  if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
144  Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
145  return Counter;
146 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
if
if(last==0)
Definition: sparse_int.h:34
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
int Saig_ManBmcTerSimCount01Po ( Aig_Man_t *  p,
unsigned *  pInfo 
)

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

Synopsis [Returns the number of POs with binary ternary info.]

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file bmcBmc3.c.

306 {
307  Aig_Obj_t * pObj;
308  int i, Counter = 0;
309  Saig_ManForEachPo( p, pObj, i )
310  Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
311  return Counter;
312 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
unsigned* Saig_ManBmcTerSimOne ( Aig_Man_t *  p,
unsigned *  pPrev 
)

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

Synopsis [Performs ternary simulation of one frame.]

Description []

SideEffects []

SeeAlso []

Definition at line 159 of file bmcBmc3.c.

160 {
161  Aig_Obj_t * pObj, * pObjLi;
162  unsigned * pInfo;
163  int i, Val0, Val1;
164  pInfo = ABC_CALLOC( unsigned, Abc_BitWordNum(2 * Aig_ManObjNumMax(p)) );
165  Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(p), SAIG_TER_ONE );
166  Saig_ManForEachPi( p, pObj, i )
167  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
168  if ( pPrev == NULL )
169  {
170  Saig_ManForEachLo( p, pObj, i )
171  Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
172  }
173  else
174  {
175  Saig_ManForEachLiLo( p, pObjLi, pObj, i )
176  Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoGet(pPrev, pObjLi) );
177  }
178  Aig_ManForEachNode( p, pObj, i )
179  {
180  Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
181  Val1 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin1(pObj) );
182  if ( Aig_ObjFaninC0(pObj) )
183  Val0 = Saig_ManBmcSimInfoNot( Val0 );
184  if ( Aig_ObjFaninC1(pObj) )
185  Val1 = Saig_ManBmcSimInfoNot( Val1 );
186  Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoAnd(Val0, Val1) );
187  }
188  Aig_ManForEachCo( p, pObj, i )
189  {
190  Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
191  if ( Aig_ObjFaninC0(pObj) )
192  Val0 = Saig_ManBmcSimInfoNot( Val0 );
193  Saig_ManBmcSimInfoSet( pInfo, pObj, Val0 );
194  }
195  return pInfo;
196 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
SAIG_TER_UND
#define SAIG_TER_UND
Definition: bmcBmc3.c:86
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Saig_ManBmcSimInfoGet
static int Saig_ManBmcSimInfoGet(unsigned *pInfo, Aig_Obj_t *pObj)
Definition: bmcBmc3.c:106
Saig_ManBmcSimInfoAnd
static int Saig_ManBmcSimInfoAnd(int Value0, int Value1)
Definition: bmcBmc3.c:97
Saig_ManBmcSimInfoSet
static void Saig_ManBmcSimInfoSet(unsigned *pInfo, Aig_Obj_t *pObj, int Value)
Definition: bmcBmc3.c:111
Saig_ManBmcSimInfoNot
static int Saig_ManBmcSimInfoNot(int Value)
Definition: bmcBmc3.c:88
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Aig_Obj_t_
Definition: aig.h:69
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
SAIG_TER_ONE
#define SAIG_TER_ONE
Definition: bmcBmc3.c:85
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
SAIG_TER_ZER
#define SAIG_TER_ZER
Definition: bmcBmc3.c:84
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Vec_Ptr_t* Saig_ManBmcTerSimPo ( Aig_Man_t *  p)

Definition at line 313 of file bmcBmc3.c.

314 {
315  Vec_Ptr_t * vInfos;
316  unsigned * pInfo = NULL;
317  int i, nPoBin;
318  vInfos = Vec_PtrAlloc( 100 );
319  for ( i = 0; ; i++ )
320  {
321  if ( i % 100 == 0 )
322  Abc_Print( 1, "Frame %5d\n", i );
323  pInfo = Saig_ManBmcTerSimOne( p, pInfo );
324  Vec_PtrPush( vInfos, pInfo );
325  nPoBin = Saig_ManBmcTerSimCount01Po( p, pInfo );
326  if ( nPoBin < Saig_ManPoNum(p) )
327  break;
328  }
329  Abc_Print( 1, "Detected terminary PO in frame %d.\n", i );
330  Saig_ManBmcCountNonternary( p, vInfos, i );
331  return vInfos;
332 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Saig_ManBmcTerSimOne
unsigned * Saig_ManBmcTerSimOne(Aig_Man_t *p, unsigned *pPrev)
Definition: bmcBmc3.c:159
Saig_ManBmcTerSimCount01Po
int Saig_ManBmcTerSimCount01Po(Aig_Man_t *p, unsigned *pInfo)
Definition: bmcBmc3.c:305
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Saig_ManBmcCountNonternary
void Saig_ManBmcCountNonternary(Aig_Man_t *p, Vec_Ptr_t *vInfos, int iFrame)
Definition: bmcBmc3.c:281
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
void Saig_ManBmcTerSimTest ( Aig_Man_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file bmcBmc3.c.

239 {
240  Vec_Ptr_t * vInfos;
241  unsigned * pInfo;
242  int i;
243  vInfos = Saig_ManBmcTerSim( p );
244  Vec_PtrForEachEntry( unsigned *, vInfos, pInfo, i )
245  Abc_Print( 1, "%d=%d ", i, Saig_ManBmcTerSimCount01(p, pInfo) );
246  Abc_Print( 1, "\n" );
247  Vec_PtrFreeFree( vInfos );
248 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_PtrFreeFree
static void Vec_PtrFreeFree(Vec_Ptr_t *p)
Definition: vecPtr.h:569
Saig_ManBmcTerSimCount01
int Saig_ManBmcTerSimCount01(Aig_Man_t *p, unsigned *pInfo)
Definition: bmcBmc3.c:136
Saig_ManBmcTerSim
Vec_Ptr_t * Saig_ManBmcTerSim(Aig_Man_t *p)
Definition: bmcBmc3.c:209
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
void Saig_ManBmcTerSimTestPo ( Aig_Man_t *  p)

Definition at line 333 of file bmcBmc3.c.

334 {
335  Vec_Ptr_t * vInfos;
336  vInfos = Saig_ManBmcTerSimPo( p );
337  Vec_PtrFreeFree( vInfos );
338 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_PtrFreeFree
static void Vec_PtrFreeFree(Vec_Ptr_t *p)
Definition: vecPtr.h:569
Saig_ManBmcTerSimPo
Vec_Ptr_t * Saig_ManBmcTerSimPo(Aig_Man_t *p)
Definition: bmcBmc3.c:313
abctime Saig_ManBmcTimeToStop ( Saig_ParBmc_t *  pPars,
abctime  nTimeToStopNG 
)

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

Synopsis [Returns time to stop.]

Description []

SideEffects []

SeeAlso []

Definition at line 1319 of file bmcBmc3.c.

1320 {
1321  abctime nTimeToStopGap = pPars->nTimeOutGap ? pPars->nTimeOutGap * CLOCKS_PER_SEC + Abc_Clock(): 0;
1322  abctime nTimeToStop = 0;
1323  if ( nTimeToStopNG && nTimeToStopGap )
1324  nTimeToStop = nTimeToStopNG < nTimeToStopGap ? nTimeToStopNG : nTimeToStopGap;
1325  else if ( nTimeToStopNG )
1326  nTimeToStop = nTimeToStopNG;
1327  else if ( nTimeToStopGap )
1328  nTimeToStop = nTimeToStopGap;
1329  return nTimeToStop;
1330 }
Saig_ParBmc_t_::nTimeOutGap
int nTimeOutGap
Definition: bmc.h:54
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
void Saig_ManBmcWriteBlif ( Aig_Man_t *  p,
Vec_Int_t *  vMapping,
char *  pFileName 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 581 of file bmcBmc3.c.

582 {
583  FILE * pFile;
584  char * pSopSizes, ** pSops;
585  Aig_Obj_t * pObj;
586  char Vals[4];
587  int i, k, b, iFan, iTruth, * pData;
588  pFile = fopen( pFileName, "w" );
589  if ( pFile == NULL )
590  {
591  Abc_Print( 1, "Cannot open file %s\n", pFileName );
592  return;
593  }
594  fprintf( pFile, ".model test\n" );
595  fprintf( pFile, ".inputs" );
596  Aig_ManForEachCi( p, pObj, i )
597  fprintf( pFile, " n%d", Aig_ObjId(pObj) );
598  fprintf( pFile, "\n" );
599  fprintf( pFile, ".outputs" );
600  Aig_ManForEachCo( p, pObj, i )
601  fprintf( pFile, " n%d", Aig_ObjId(pObj) );
602  fprintf( pFile, "\n" );
603  fprintf( pFile, ".names" );
604  fprintf( pFile, " n%d\n", Aig_ObjId(Aig_ManConst1(p)) );
605  fprintf( pFile, " 1\n" );
606 
607  Cnf_ReadMsops( &pSopSizes, &pSops );
608  Aig_ManForEachNode( p, pObj, i )
609  {
610  if ( Vec_IntEntry(vMapping, i) == 0 )
611  continue;
612  pData = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, i) );
613  fprintf( pFile, ".names" );
614  for ( iFan = 0; iFan < 4; iFan++ )
615  if ( pData[iFan+1] >= 0 )
616  fprintf( pFile, " n%d", pData[iFan+1] );
617  else
618  break;
619  fprintf( pFile, " n%d\n", i );
620  // write SOP
621  iTruth = pData[0] & 0xffff;
622  for ( k = 0; k < pSopSizes[iTruth]; k++ )
623  {
624  int Lit = pSops[iTruth][k];
625  for ( b = 3; b >= 0; b-- )
626  {
627  if ( Lit % 3 == 0 )
628  Vals[b] = '0';
629  else if ( Lit % 3 == 1 )
630  Vals[b] = '1';
631  else
632  Vals[b] = '-';
633  Lit = Lit / 3;
634  }
635  for ( b = 0; b < iFan; b++ )
636  fprintf( pFile, "%c", Vals[b] );
637  fprintf( pFile, " 1\n" );
638  }
639  }
640  free( pSopSizes );
641  free( pSops[1] );
642  free( pSops );
643 
644  Aig_ManForEachCo( p, pObj, i )
645  {
646  fprintf( pFile, ".names" );
647  fprintf( pFile, " n%d", Aig_ObjId(Aig_ObjFanin0(pObj)) );
648  fprintf( pFile, " n%d\n", Aig_ObjId(pObj) );
649  fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
650  }
651  fprintf( pFile, ".end\n" );
652  fclose( pFile );
653 }
free
VOID_HACK free()
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition: cnfData.c:4537
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_Obj_t_
Definition: aig.h:69
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
int Saig_ManCallSolver ( Gia_ManBmc_t *  p,
int  Lit 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1370 of file bmcBmc3.c.

1371 {
1372  if ( Lit == 0 )
1373  return l_False;
1374  if ( Lit == 1 )
1375  return l_True;
1376  return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1377 }
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
l_True
#define l_True
Definition: SolverTypes.h:84
l_False
#define l_False
Definition: SolverTypes.h:85
Abc_Cex_t* Saig_ManGenerateCex ( Gia_ManBmc_t *  p,
int  f,
int  i 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1343 of file bmcBmc3.c.

1344 {
1345  Aig_Obj_t * pObjPi;
1346  Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), f*Saig_ManPoNum(p->pAig)+i );
1347  int j, k, iBit = Saig_ManRegNum(p->pAig);
1348  for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(p->pAig) )
1349  Saig_ManForEachPi( p->pAig, pObjPi, k )
1350  {
1351  int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
1352  if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
1353  Abc_InfoSetBit( pCex->pData, iBit + k );
1354  }
1355  return pCex;
1356 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
lit_var
static int lit_var(lit l)
Definition: satVec.h:145
Saig_ManBmcLiteral
static int Saig_ManBmcLiteral(Gia_ManBmc_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: bmcBmc3.c:843
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition: utilCex.c:85
Aig_Obj_t_
Definition: aig.h:69
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Saig_ParBmcSetDefaultParams ( Saig_ParBmc_t *  p)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 1284 of file bmcBmc3.c.

1285 {
1286  memset( p, 0, sizeof(Saig_ParBmc_t) );
1287  p->nStart = 0; // maximum number of timeframes
1288  p->nFramesMax = 0; // maximum number of timeframes
1289  p->nConfLimit = 0; // maximum number of conflicts at a node
1290  p->nConfLimitJump = 0; // maximum number of conflicts after jumping
1291  p->nFramesJump = 0; // the number of tiemframes to jump
1292  p->nTimeOut = 0; // approximate timeout in seconds
1293  p->nTimeOutGap = 0; // time since the last CEX found
1294  p->nPisAbstract = 0; // the number of PIs to abstract
1295  p->fSolveAll = 0; // stops on the first SAT instance
1296  p->fDropSatOuts = 0; // replace sat outputs by constant 0
1297  p->nLearnedStart = 10000; // starting learned clause limit
1298  p->nLearnedDelta = 2000; // delta of learned clause limit
1299  p->nLearnedPerce = 80; // ratio of learned clause limit
1300  p->fVerbose = 0; // verbose
1301  p->fNotVerbose = 0; // skip line-by-line print-out
1302  p->iFrame = -1; // explored up to this frame
1303  p->nFailOuts = 0; // the number of failed outputs
1304  p->nDropOuts = 0; // the number of timed out outputs
1305  p->timeLastSolved = 0; // time when the last one was solved
1306 }
memset
char * memset()
Saig_ParBmc_t_::nConfLimitJump
int nConfLimitJump
Definition: bmc.h:51
Saig_ParBmc_t_::nLearnedPerce
int nLearnedPerce
Definition: bmc.h:65
Saig_ParBmc_t_::nDropOuts
int nDropOuts
Definition: bmc.h:72
Saig_ParBmc_t_::nLearnedStart
int nLearnedStart
Definition: bmc.h:63
Saig_ParBmc_t_
Definition: bmc.h:46
Saig_ParBmc_t_::fVerbose
int fVerbose
Definition: bmc.h:66
Saig_ParBmc_t_::nFailOuts
int nFailOuts
Definition: bmc.h:71
Saig_ParBmc_t_::nStart
int nStart
Definition: bmc.h:48
Saig_ParBmc_t_::nTimeOutGap
int nTimeOutGap
Definition: bmc.h:54
Saig_ParBmc_t_::iFrame
int iFrame
Definition: bmc.h:70
Saig_ParBmc_t_::nConfLimit
int nConfLimit
Definition: bmc.h:50
Saig_ParBmc_t_::nTimeOut
int nTimeOut
Definition: bmc.h:53
Saig_ParBmc_t_::nFramesMax
int nFramesMax
Definition: bmc.h:49
Saig_ParBmc_t_::timeLastSolved
abctime timeLastSolved
Definition: bmc.h:73
Saig_ParBmc_t_::fDropSatOuts
int fDropSatOuts
Definition: bmc.h:60
Saig_ParBmc_t_::nFramesJump
int nFramesJump
Definition: bmc.h:52
Saig_ParBmc_t_::fNotVerbose
int fNotVerbose
Definition: bmc.h:67
Saig_ParBmc_t_::nPisAbstract
int nPisAbstract
Definition: bmc.h:56
Saig_ParBmc_t_::nLearnedDelta
int nLearnedDelta
Definition: bmc.h:64
Saig_ParBmc_t_::fSolveAll
int fSolveAll
Definition: bmc.h:57