From b910cba3e2e065d444d4a7b1bcbf81227417fc11 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 28 Jan 2014 17:46:11 +0800 Subject: Initial new interpolation code. --- src/proof/int2/int2.h | 90 +++++++++++ src/proof/int2/int2Bmc.c | 355 ++++++++++++++++++++++++++++++++++++++++++++ src/proof/int2/int2Core.c | 335 +++++++++++++++++++++++++++++++++++++++++ src/proof/int2/int2Int.h | 164 ++++++++++++++++++++ src/proof/int2/int2Refine.c | 154 +++++++++++++++++++ src/proof/int2/int2Util.c | 152 +++++++++++++++++++ src/proof/int2/module.make | 4 + 7 files changed, 1254 insertions(+) create mode 100644 src/proof/int2/int2.h create mode 100644 src/proof/int2/int2Bmc.c create mode 100644 src/proof/int2/int2Core.c create mode 100644 src/proof/int2/int2Int.h create mode 100644 src/proof/int2/int2Refine.c create mode 100644 src/proof/int2/int2Util.c create mode 100644 src/proof/int2/module.make (limited to 'src/proof') diff --git a/src/proof/int2/int2.h b/src/proof/int2/int2.h new file mode 100644 index 00000000..b85006b7 --- /dev/null +++ b/src/proof/int2/int2.h @@ -0,0 +1,90 @@ +/**CFile**************************************************************** + + FileName [int2.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 1, 2013.] + + Revision [$Id: int2.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__aig__int2__int_h +#define ABC__aig__int2__int_h + + +/* + The interpolation algorithm implemented here was introduced in the papers: + K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13. + C.-Y. Wu et al. A CEX-Guided Interpolant Generation Algorithm for + SAT-based Model Checking. DAC'13. +*/ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// simulation manager +typedef struct Int2_ManPars_t_ Int2_ManPars_t; +struct Int2_ManPars_t_ +{ + int nBTLimit; // limit on the number of conflicts + int nFramesS; // the starting number timeframes + int nFramesMax; // the max number timeframes to unroll + int nSecLimit; // time limit in seconds + int nFramesK; // the number of timeframes to use in induction + int fRewrite; // use additional rewriting to simplify timeframes + int fTransLoop; // add transition into the init state under new PI var + int fDropInvar; // dump inductive invariant into file + int fVerbose; // print verbose statistics + int iFrameMax; // the time frame reached + char * pFileName; // file name to dump interpolant +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== intCore.c ==========================================================*/ +extern void Int2_ManSetDefaultParams( Int2_ManPars_t * p ); +extern int Int2_ManPerformInterpolation( Gia_Man_t * p, Int2_ManPars_t * pPars ); + + + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/int2/int2Bmc.c b/src/proof/int2/int2Bmc.c new file mode 100644 index 00000000..cd7f1a74 --- /dev/null +++ b/src/proof/int2/int2Bmc.c @@ -0,0 +1,355 @@ +/**CFile**************************************************************** + + FileName [int2Bmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [BMC used inside IMC.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 1, 2013.] + + Revision [$Id: int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "int2Int.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Trasnforms AIG to transition into the init state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRi, * pObjRo; + int i, iCtrl; + assert( Gia_ManRegNum(p) > 0 ); + pNew = Gia_ManStart( 10000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + { + if ( i == Gia_ManPiNum(p) ) + iCtrl = Gia_ManAppendCi( pNew ); + pObj->Value = Gia_ManAppendCi( pNew ); + } + Gia_ManHashAlloc( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) + Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + // remove dangling + pNew = Gia_ManCleanup( pTemp = pNew ); + if ( fVerbose ) + printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", + Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) ); + Gia_ManStop( pTemp ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if AIG has transition into init state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Int2_ManCheckInit( Gia_Man_t * p ) +{ + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + Vec_Int_t * vLits; + int i, Lit, RetValue = 0; + assert( Gia_ManRegNum(p) > 0 ); + pNew = Jf_ManDeriveCnf( p, 0 ); + pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL; + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat != NULL ) + { + vLits = Vec_IntAlloc( Gia_ManRegNum(p) ); + Gia_ManForEachRi( pNew, pObj, i ) + { + Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ]; + Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) ); + Vec_IntPush( vLits, Abc_LitNot(Lit) ); + } + if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True ) + RetValue = 1; + Vec_IntFree( vLits ); + sat_solver_delete( pSat ); + } + Cnf_DataFree( pCnf ); + Gia_ManStop( pNew ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Creates the BMC instance in the SAT solver.] + + Description [The PIs are mapped in the natural order. The flop inputs + are the last Gia_ManRegNum(p) variables of resulting SAT solver.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Int2_ManFrameInit( Gia_Man_t * p, int nFrames, int fVerbose ) +{ + Gia_Man_t * pFrames, * pTemp; + Gia_Obj_t * pObj; + int i, f; + pFrames = Gia_ManStart( 10000 ); + pFrames->pName = Abc_UtilStrsav( p->pName ); + pFrames->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + // perform structural hashing + Gia_ManHashAlloc( pFrames ); + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pFrames ); + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = f ? Gia_ObjRoToRi(p, pObj)->Value : 0; + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + } + Gia_ManHashStop( pFrames ); + // create flop inputs + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) ); + // remove dangling + pFrames = Gia_ManCleanup( pTemp = pFrames ); + if ( fVerbose ) + printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", + Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) ); + Gia_ManStop( pTemp ); + return pFrames; +} +sat_solver * Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames ) +{ + Gia_Man_t * pFrames, * pTemp; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + // unfold for the given number of timeframes + pFrames = Int2_ManFrameInit( p, nFrames, 1 ); + assert( Gia_ManRegNum(pFrames) == 0 ); + // derive CNF for the timeframes + pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 ); Gia_ManStop( pTemp ); + pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL; + // create SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat != NULL ) + { + Gia_Obj_t * pObj; + int i, nVars = sat_solver_nvars( pSat ); + sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) ); + // add clauses for the POs + Gia_ManForEachCo( pFrames, pObj, i ) + sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) ); + } + Cnf_DataFree( pCnf ); + Gia_ManStop( pFrames ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Int2_ManCheckFrames( Int2_Man_t * p, int iFrame, int iObj ) +{ + Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame); + return Vec_IntEntry(vMapFrame, iObj); +} +static inline void Int2_ManWriteFrames( Int2_Man_t * p, int iFrame, int iObj, int iRes ) +{ + Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame); + assert( Vec_IntEntry(vMapFrame, iObj) == -1 ); + Vec_IntWriteEntry( vMapFrame, iObj, iRes ); +} +void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos ) +{ + Gia_Obj_t * pObj; + int i, Entry, iLit; + // create storage room for unfolded IDs + for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ ) + Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) ); + assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 ); + // create constant 0 node + if ( f == 0 ) + { + iLit = 1; + Int2_ManWriteFrames( p, iFrame, iObj, 0 ); + sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 ); + } + // start the stack + Vec_IntClear( p->vStack ); + Vec_IntForEachEntry( vPrefCos, Entry, i ) + { + pObj = Gia_ManCo( p->pGia, Entry ); + Vec_IntPush( p->vStack, iFrame ); + Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) ); + } + // construct unfolded AIG + while ( Vec_IntSize(p->vStack) > 0 ) + { + int iObj = Vec_IntPop(p->vStack); + int iFrame = Vec_IntPop(p->vStack); + if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 ) + continue; + pObj = Gia_ManObj( p->pGia, iObj ); + if ( Gia_ObjIsPi(p->pGia, pObj) ) + Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) ); + else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) ) + Int2_ManWriteFrames( p, iFrame, iObj, 0 ); + else if ( Gia_ObjIsRo(p->pGia, iObj) ) + { + int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) ); + int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF ); + if ( iLit >= 0 ) + Int2_ManWriteFrames( p, iFrame, iObj, iLit ); + else + { + Vec_IntPush( p->vStack, iFrame ); + Vec_IntPush( p->vStack, iObj ); + Vec_IntPush( p->vStack, iFrame-1 ); + Vec_IntPush( p->vStack, iObjF ); + } + } + else if ( Gia_ObjIsCo(pObj) ) + { + int iObjF = Gia_ObjFaninId0(p->pGia, iObj) ); + int iLit = Int2_ManCheckFrames( p, iFrame, iObjF ); + if ( iLit >= 0 ) + Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) ); + else + { + Vec_IntPush( p->vStack, iFrame ); + Vec_IntPush( p->vStack, iObj ); + Vec_IntPush( p->vStack, iFrame ); + Vec_IntPush( p->vStack, iObjF ); + } + } + else if ( Gia_ObjIsAnd(pObj) ) + { + int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) ); + int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 ); + int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) ); + int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 ); + if ( iLit0 >= 0 && iLit1 >= 0 ) + { + Entry = Gia_ManObjNum(pFrames); + iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1); + Int2_ManWriteFrames( p, iFrame, iObj, iLit ); + if ( Entry < Gia_ManObjNum(pFrames) ) + { + assert( !Abc_LitIsCompl(iLit) ); + sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) ); + } + } + else + { + Vec_IntPush( p->vStack, iFrame ); + Vec_IntPush( p->vStack, iObj ); + if ( iLit0 < 0 ) + { + Vec_IntPush( p->vStack, iFrame ); + Vec_IntPush( p->vStack, iObjF0 ); + } + if ( iLit1 < 0 ) + { + Vec_IntPush( p->vStack, iFrame ); + Vec_IntPush( p->vStack, iObjF1 ); + } + } + } + else assert( 0 ); + } +} +int Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube ) +{ + int status; + if ( vCube == NULL ) + { + Gia_Obj_t * pObj; + int i, iLit; + Gia_ManForEachPo( p->pGia, pObj, i ) + { + iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) ); + if ( iLit == 0 ) + continue; + if ( iLit == 1 ) + return 0; + status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 ); + if ( status == l_False ) + continue; + if ( status == l_True ) + return 0; + return -1; + } + return 1; + } + status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 ); + if ( status == l_False ) + return 1; + if ( status == l_True ) + return 0; + return -1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int2/int2Core.c b/src/proof/int2/int2Core.c new file mode 100644 index 00000000..feeab3ca --- /dev/null +++ b/src/proof/int2/int2Core.c @@ -0,0 +1,335 @@ +/**CFile**************************************************************** + + FileName [int2Core.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 1, 2013.] + + Revision [$Id: int2Core.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "int2Int.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default values of interpolation parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int2_ManSetDefaultParams( Int2_ManPars_t * p ) +{ + memset( p, 0, sizeof(Int2_ManPars_t) ); + p->nBTLimit = 0; // limit on the number of conflicts + p->nFramesS = 1; // the starting number timeframes + p->nFramesMax = 0; // the max number timeframes to unroll + p->nSecLimit = 0; // time limit in seconds + p->nFramesK = 1; // the number of timeframes to use in induction + p->fRewrite = 0; // use additional rewriting to simplify timeframes + p->fTransLoop = 0; // add transition into the init state under new PI var + p->fDropInvar = 0; // dump inductive invariant into file + p->fVerbose = 0; // print verbose statistics + p->iFrameMax = -1; +} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Int2_ManUnroll( Gia_Man_t * p, int nFrames ) +{ + Gia_Man_t * pFrames, * pTemp; + Gia_Obj_t * pObj; + int i, f; + assert( Gia_ManRegNum(pAig) > 0 ); + pFrames = Gia_ManStart( Gia_ManObjNum(pAig) ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); + Gia_ManHashAlloc( pFrames ); + Gia_ManConst0(pAig)->Value = 0; + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManForEachRo( pAig, pObj, i ) + pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0; + Gia_ManForEachPi( pAig, pObj, i ) + pObj->Value = Gia_ManAppendCi( pFrames ); + Gia_ManForEachAnd( pAig, pObj, i ) + pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachRi( pAig, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + } + Gia_ManForEachRi( pAig, pObj, i ) + Gia_ManAppendCo( pFrames, pObj->Value ); + Gia_ManHashStop( pFrames ); + pFrames = Gia_ManCleanup( pTemp = pFrames ); + Gia_ManStop( pTemp ); + return pFrames; +} +sat_solver * Int2_ManPreparePrefix( Gia_Man_t * p, int f, Vec_Int_t ** pvCiMap ) +{ + Gia_Man_t * pPref, * pNew; + sat_solver * pSat; + // create subset of the timeframe + pPref = Int2_ManUnroll( p, f ); + // create SAT solver + pNew = Jf_ManDeriveCnf( pPref, 0 ); + pCnf = (Cnf_Dat_t *)pPref->pData; pPref->pData = NULL; + Gia_ManStop( pPref ); + // derive the SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + // collect indexes of CO variables + *pvCiMap = Vec_IntAlloc( 100 ); + Gia_ManForEachPo( pNew, pObj, i ) + Vec_IntPush( *pvCiMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] ); + // cleanup + Cnf_DataFree( pCnf ); + Gia_ManStop( pNew ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Int2_ManPrepareSuffix( Gia_Man_t * p, Vec_Int_t * vImageOne, Vec_Int_t * vImagesAll, Vec_Int_t ** pvCoMap, Gia_Man_t ** ppSuff ) +{ + Gia_Man_t * pSuff, * pNew; + Gia_Obj_t * pObj; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Vec_Int_t * vLits; + int i, Lit, Limit; + // create subset of the timeframe + pSuff = Int2_ManProbToGia( p, vImageOne ); + assert( Gia_ManPiNum(pSuff) == Gia_ManCiNum(p) ); + // create SAT solver + pNew = Jf_ManDeriveCnf( pSuff, 0 ); + pCnf = (Cnf_Dat_t *)pSuff->pData; pSuff->pData = NULL; + Gia_ManStop( pSuff ); + // derive the SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + // create new constraints + vLits = Vec_IntAlloc( 1000 ); + Vec_IntForEachEntryStart( vImagesAll, Limit, i, 1 ) + { + Vec_IntClear( vLits ); + for ( k = 0; k < Limit; k++ ) + { + i++; + Lit = Vec_IntEntry( vSop, i + k ); + Vec_IntPush( vLits, Abc_LitNot(Lit) ); + } + if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) ) // UNSAT + { + Vec_IntFree( vLits ); + Cnf_DataFree( pCnf ); + Gia_ManStop( pNew ); + *pvCoMap = NULL; + return NULL; + } + } + Vec_IntFree( vLits ); + // collect indexes of CO variables + *pvCoMap = Vec_IntAlloc( 100 ); + Gia_ManForEachRo( p, pObj, i ) + { + pObj = Gia_ManPi( pNew, i + Gia_ManPiNum(p) ); + Vec_IntPush( *pvCoMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] ); + } + // cleanup + Cnf_DataFree( pCnf ); + if ( ppSuff ) + *ppSuff = pNew; + else + Gia_ManStop( pNew ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Returns the cube cover and status.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Int2_ManComputePreimage( Gia_Man_t * pSuff, sat_solver * pSatPref, sat_solver * pSatSuff, Vec_Int_t * vCiMap, Vec_Int_t * vCoMap, Vec_Int_t * vPrio ) +{ + int i, iVar, status; + Vec_IntClear( p->vImage ); + while ( 1 ) + { + // run suffix solver + status = sat_solver_solve( p->pSatSuff, NULL, NULL, 0, 0, 0, 0 ); + if ( status == l_Undef ) + return NULL; // timeout + if ( status == l_False ) + return INT2_COMPUTED; + assert( status == l_True ); + // collect assignment + Vec_IntClear( p->vAssign ); + Vec_IntForEachEntry( p->vCiMap, iVar, i ) + Vec_IntPush( p->vAssign, sat_solver_var_value(p->pSatSuff, iVar) ); + // derive initial cube + vCube = Int2_ManRefineCube( p->pSuff, p->vAssign, p->vPrio ); + // expend the cube using prefix + status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 ); + if ( status == l_False ) + { + int k, nCoreLits, * pCoreLits; + nCoreLits = sat_solver_final( p->pSatPref, &pCoreLits ); + // create cube + Vec_IntClear( vCube ); + Vec_IntPush( vImage, nCoreLits ); + for ( k = 0; k < nCoreLits; k++ ) + { + Vec_IntPush( vCube, pCoreLits[k] ); + Vec_IntPush( vImage, pCoreLits[k] ); + } + // add cube to the solver + if ( !sat_solver_addclause( p->pSatSuff, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube) ) ) + { + Vec_IntFree( vCube ); + return INT2_COMPUTED; + } + } + Vec_IntFree( vCube ); + if ( status == l_Undef ) + return INT2_TIME_OUT; + if ( status == l_True ) + return INT2_FALSE_NEG; + assert( status == l_False ); + continue; + } + return p->vImage; +} + +/**Function************************************************************* + + Synopsis [Interpolates while the number of conflicts is not exceeded.] + + Description [Returns 1 if proven. 0 if failed. -1 if undecided.] + + SideEffects [Does not check the property in 0-th frame.] + + SeeAlso [] + +***********************************************************************/ +int Int2_ManPerformInterpolation( Gia_Man_t * pInit, Int2_ManPars_t * pPars ) +{ + Int2_Man_t * p; + int f, i, RetValue = -1; + abctime clk, clkTotal = Abc_Clock(), timeTemp = 0; + abctime nTimeToStop = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0; + + // sanity checks + assert( Gia_ManPiNum(pInit) > 0 ); + assert( Gia_ManPoNum(pInit) > 0 ); + assert( Gia_ManRegNum(pInit) > 0 ); + + // create manager + p = Int2_ManCreate( pInit, pPars ); + + // create SAT solver + p->pSatPref = sat_solver_new(); + sat_solver_setnvars( p->pSatPref, 1000 ); + sat_solver_set_runtime_limit( p->pSatPref, nTimeToStop ); + + // check outputs in the first frame + for ( i = 0; i < Gia_ManPoNum(pInit); i++ ) + Vec_IntPush( p->vPrefCos, i ); + Int2_ManCreateFrames( p, 0, p->vPrefCos ); + RetValue = Int2_ManCheckBmc( p, NULL ); + if ( RetValue != 1 ) + return RetValue; + + // create original image + for ( f = pPars->nFramesS; f < p->nFramesMax; f++ ) + { + for ( i = 0; i < p->nFramesMax; i++ ) + { + p->pSatSuff = Int2_ManPrepareSuffix( p, vImageOne. vImagesAll, &vCoMap, &pGiaSuff ); + sat_solver_set_runtime_limit( p->pSatSuff, nTimeToStop ); + Vec_IntFreeP( &vImageOne ); + vImageOne = Int2_ManComputePreimage( pGiaSuff, p->pSatPref, p->pSatSuff, vCiMap, vCoMap ); + Vec_IntFree( vCoMap ); + Gia_ManStop( pGiaSuff ); + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + return -1; + if ( vImageOne == NULL ) + { + if ( i == 0 ) + { + printf( "Satisfiable in frame %d.\n", f ); + Vec_IntFree( vCiMap ); + sat_solver_delete( p->pSatPref ); p->pSatPref = NULL; + return 0; + } + f += i; + break; + } + Vec_IntAppend( vImagesAll, vImageOne ); + sat_solver_delete( p->pSatSuff ); p->pSatSuff = NULL; + } + Vec_IntFree( vCiMap ); + sat_solver_delete( p->pSatPref ); p->pSatPref = NULL; + } + Abc_PrintTime( "Time", Abc_Clock() - clk ); + + +p->timeSatPref += Abc_Clock() - clk; + + Int2_ManStop( p ); + return RetValue; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int2/int2Int.h b/src/proof/int2/int2Int.h new file mode 100644 index 00000000..837a2bca --- /dev/null +++ b/src/proof/int2/int2Int.h @@ -0,0 +1,164 @@ +/**CFile**************************************************************** + + FileName [int2Int.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 1, 2013.] + + Revision [$Id: int2Int.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__Gia__int2__intInt_h +#define ABC__Gia__int2__intInt_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig/gia/gia.h" +#include "sat/bsat/satSolver.h" +#include "sat/cnf/cnf.h" +#include "int2.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// interpolation manager +typedef struct Int2_Man_t_ Int2_Man_t; +struct Int2_Man_t_ +{ + // parameters + Int2_ManPars_t * pPars; // parameters + // GIA managers + Gia_Man_t * pGia; // original manager + Gia_Man_t * pGiaPref; // prefix manager + Gia_Man_t * pGiaSuff; // suffix manager + // subset of the manager + Vec_Int_t * vSuffCis; // suffix CIs + Vec_Int_t * vSuffCos; // suffix COs + Vec_Int_t * vPrefCos; // suffix POs + Vec_Int_t * vStack; // temporary stack + // preimages + Vec_Int_t * vImageOne; // latest preimage + Vec_Int_t * vImagesAll; // cumulative preimage + // variable maps + Vec_Ptr_t * vMapFrames; // mapping of GIA IDs into frame IDs + Vec_Int_t * vMapPref; // mapping of flop inputs into SAT variables + Vec_Int_t * vMapSuff; // mapping of flop outputs into SAT variables + // initial minimization + Vec_Int_t * vAssign; // assignment of PIs in pGiaSuff + Vec_Int_t * vPrio; // priority of PIs in pGiaSuff + // SAT solving + sat_solver * pSatPref; // prefix solver + sat_solver * pSatSuff; // suffix solver + // runtime + abctime timeSatPref; + abctime timeSatSuff; + abctime timeOther; + abctime timeTotal; +}; + +static inline Int2_Man_t * Int2_ManCreate( Gia_Man_t * pGia, Int2_ManPars_t * pPars ) +{ + Int2_Man_t * p; + p = ABC_CALLOC( Int2_Man_t, 1 ); + p->pPars = pPars; + p->pGia = pGia; + p->pGiaPref = Gia_ManStart( 10000 ); + // perform structural hashing + Gia_ManHashAlloc( pFrames ); + // subset of the manager + p->vSuffCis = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + p->vSuffCos = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + p->vPrefCos = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + p->vStack = Vec_IntAlloc( 10000 ); + // preimages + p->vImageOne = Vec_IntAlloc( 1000 ); + p->vImagesAll = Vec_IntAlloc( 1000 ); + // variable maps + p->vMapFrames = Vec_PtrAlloc( 100 ); + p->vMapPref = Vec_IntAlloc( Gia_ManRegNum(pGia) ); + p->vMapSuff = Vec_IntAlloc( Gia_ManRegNum(pGia) ); + // initial minimization + p->vAssign = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + p->vPrio = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + return p; +} +static inline void Int2_ManStop( Int2_Man_t * p ) +{ + // GIA managers + Gia_ManStopP( &p->pGiaPref ); + Gia_ManStopP( &p->pGiaSuff ); + // subset of the manager + Vec_IntFreeP( &p->vSuffCis ); + Vec_IntFreeP( &p->vSuffCos ); + Vec_IntFreeP( &p->vPrefCos ); + Vec_IntFreeP( &p->vStack ); + // preimages + Vec_IntFreeP( &p->vImageOne ); + Vec_IntFreeP( &p->vImagesAll ); + // variable maps + Vec_VecFree( (Vec_Vec_t *)p->vMapFrames ); + Vec_IntFreeP( &p->vMapPref ); + Vec_IntFreeP( &p->vMapSuff ); + // initial minimization + Vec_IntFreeP( &p->vAssign ); + Vec_IntFreeP( &p->vPrio ); + // SAT solving + if ( p->pSatPref ) + sat_solver_delete( p->pSatPref ); + if ( p->timeSatSuff ) + sat_solver_delete( p->pSatSuff ); + ABC_FREE( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== int2Bmc.c =============================================================*/ +extern int Int2_ManCheckInit( Gia_Man_t * p ); +extern Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose ); +extern sat_solver * Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames ); +extern void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos ); +extern int Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube ); + +/*=== int2Refine.c =============================================================*/ +extern Vec_Int_t * Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio ); + +/*=== int2Util.c ============================================================*/ +extern Gia_Man_t * Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop ); + + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/int2/int2Refine.c b/src/proof/int2/int2Refine.c new file mode 100644 index 00000000..91008ac6 --- /dev/null +++ b/src/proof/int2/int2Refine.c @@ -0,0 +1,154 @@ +/**CFile**************************************************************** + + FileName [int2Refine.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 1, 2013.] + + Revision [$Id: int2Refine.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "int2Int.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int2_ManJustify_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSelect ) +{ + if ( pObj->fMark1 ) + return; + pObj->fMark1 = 1; + if ( Gia_ObjIsPi(p, pObj) ) + return; + if ( Gia_ObjIsCo(pObj) ) + { + Vec_IntPush( vSelect, Gia_ObjCioId(pObj) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + if ( pObj->Value == 1 ) + { + if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY ) + Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect ); + if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY ) + Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect ); + return; + } + if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) + { + if ( Gia_ObjFanin0(pObj)->fMark0 <= Gia_ObjFanin1(pObj)->fMark0 ) // choice + { + if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY ) + Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect ); + } + else + { + if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY ) + Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect ); + } + } + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) + { + if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY ) + Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect ); + } + else if ( (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) + { + if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY ) + Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect ); + } + else assert( 0 ); + } + +/**Function************************************************************* + + Synopsis [Computes the reduced set of flop variables.] + + Description [Given is a single-output seq AIG manager and an assignment + of its CIs. Returned is a subset of flops that justifies the output.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio ) +{ + Vec_Int_t * vSubset; + Gia_Obj_t * pObj; + int i; + // set values and prios + assert( Gia_ManRegNum(p) > 0 ); + assert( Vec_IntSize(vAssign) == Vec_IntSize(vPrio) ); + Gia_ManConst0(p)->fMark0 = 0; + Gia_ManConst0(p)->fMark1 = 0; + Gia_ManConst0(p)->Value = ABC_INFINITY; + Gia_ManForEachCi( p, pObj, i ) + { + pObj->fMark0 = Vec_IntEntry(vAssign, i); + pObj->fMark1 = 0; + pObj->Value = Vec_IntEntry(vPrio, i); + } + Gia_ManForEachAnd( p, pObj, i ) + { + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + pObj->fMark1 = 0; + if ( pObj->fMark0 == 1 ) + pObj->Value = Abc_MaxInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 ) + pObj->Value = Abc_MinInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); // choice + else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 ) + pObj->Value = Gia_ObjFanin0(pObj)->Value; + else + pObj->Value = Gia_ObjFanin1(pObj)->Value; + } + pObj = Gia_ManPo( p, 0 ); + pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)); + pObj->fMark1 = 0; + pObj->Value = Gia_ObjFanin0(pObj)->Value; + assert( pObj->fMark0 == 1 ); + assert( pObj->Value < ABC_INFINITY ); + // select subset + vSubset = Vec_IntAlloc( 100 ); + Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSubset ); + return vSubset; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int2/int2Util.c b/src/proof/int2/int2Util.c new file mode 100644 index 00000000..f675d0b9 --- /dev/null +++ b/src/proof/int2/int2Util.c @@ -0,0 +1,152 @@ +/**CFile**************************************************************** + + FileName [int2Util.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 1, 2013.] + + Revision [$Id: int2Util.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "int2Int.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Int2_ManComputeCoPres( Vec_Int_t * vSop, int nRegs ) +{ + Vec_Int_t * vCoPres, * vMap; + vCoPres = Vec_IntAlloc( 100 ); + if ( vSop == NULL ) + Vec_IntPush( vCoPres, 0 ); + else + { + int i, k, Limit; + vMap = Vec_IntStart( nRegs ); + Vec_IntForEachEntryStart( vSop, Limit, i, 1 ) + { + for ( k = 0; k < Limit; k++ ) + { + i++; + assert( Vec_IntEntry(vSop, i + k) < 2 * nRegs ); + Vec_IntWriteEntry( vMap, Abc_Lit2Var(Vec_IntEntry(vSop, i + k)), 1 ); + } + } + Vec_IntForEachEntry( vMap, Limit, i ) + if ( Limit ) + Vec_IntPush( vCoPres, i+1 ); + Vec_IntFree( vMap ); + } + return vCoPres; +} + +void Int2_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(pObj), vNodes ); + Int2_ManCollectInternal_rec( p, Gia_ObjFanin1(pObj), vNodes ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); +} +Vec_Int_t * Int2_ManCollectInternal( Gia_Man_t * p, Vec_Int_t * vCoPres ) +{ + Vec_Int_t * vNodes; + Gia_Obj_t * pObj; + int i, Entry; + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p)); + Gia_ManForEachCi( p, pObj, i ) + Gia_ObjSetTravIdCurrent(p, pObj); + vNodes = Vec_IntAlloc( 1000 ); + Vec_IntForEachEntry( vCoPres, Entry, i ) + Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(Gia_ManCo(p, Entry)), vNodes ); + return vNodes; +} +Gia_Man_t * Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop ) +{ + Vec_Int_t * vCoPres, * vNodes; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, k, Entry, Limit; + int Lit, Cube, Sop; + assert( Gia_ManPoNum(p) == 1 ); + // collect COs and ANDs + vCoPres = Int2_ManComputeCoPres( vSop, Gia_ManRegNum(p) ); + vNodes = Int2_ManCollectInternal( p, vCoPres ); + // create new manager + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntForEachEntry( vCoPres, Entry, i ) + { + pObj = Gia_ManCo(p, Entry); + pObj->Value = Gia_ObjFanin0Copy( pObj ); + } + // create additional cubes + Sop = 0; + Vec_IntForEachEntryStart( vSop, Limit, i, 1 ) + { + Cube = 1; + for ( k = 0; k < Limit; k++ ) + { + i++; + Lit = Vec_IntEntry( vSop, i + k ); + pObj = Gia_ManRi( p, Abc_Lit2Var(Lit) ); + Cube = Gia_ManHashAnd( pNew, Cube, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(Lit)) ); + } + Sop = Gia_ManHashOr( pNew, Sop, Cube ); + } + Gia_ManAppendCo( pNew, Sop ); + Gia_ManHashStop( pNew ); + // cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/int2/module.make b/src/proof/int2/module.make new file mode 100644 index 00000000..900ec7f4 --- /dev/null +++ b/src/proof/int2/module.make @@ -0,0 +1,4 @@ +SRC += src/proof/int2/int2Bmc.c \ + src/proof/int2/int2Core.c \ + src/proof/int2/int2Refine.c \ + src/proof/int2/int2Util.c -- cgit v1.2.3