diff options
Diffstat (limited to 'src')
34 files changed, 3305 insertions, 1996 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 84c1e0b5..ef821d12 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -486,7 +486,7 @@ extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl ); -extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum ); +extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs ); /*=== aigFanout.c ==========================================================*/ extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c index bddc9288..4cfdaaf1 100644 --- a/src/aig/aig/aigCheck.c +++ b/src/aig/aig/aigCheck.c @@ -17,7 +17,7 @@ Revision [$Id: aigCheck.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] ***********************************************************************/ - + #include "aig.h" //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index db9e7288..c6a4d19a 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -905,7 +905,7 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum ) +Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs ) { Aig_Man_t * pNew; Aig_Obj_t * pObj; @@ -922,8 +922,8 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum ) Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi( pNew ); // set registers - pNew->nRegs = p->nRegs; - pNew->nTruePis = p->nTruePis; + pNew->nRegs = fAddRegs? p->nRegs : 0; + pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs; pNew->nTruePos = 1; // duplicate internal nodes Aig_ManForEachNode( p, pObj, i ) @@ -932,8 +932,11 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum ) pObj = Aig_ManPo( p, iPoNum ); Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); // create register inputs with MUXes - Aig_ManForEachLiSeq( p, pObj, i ) - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + if ( fAddRegs ) + { + Aig_ManForEachLiSeq( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } Aig_ManCleanup( pNew ); return pNew; } diff --git a/src/aig/bar/bar.c b/src/aig/bar/bar.c index 8c215b48..13bd9fe7 100644 --- a/src/aig/bar/bar.c +++ b/src/aig/bar/bar.c @@ -60,9 +60,9 @@ static void Bar_ProgressClean( Bar_Progress_t * p ); Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal ) { Bar_Progress_t * p; -// extern int Abc_FrameShowProgress( void * p ); -// extern void * Abc_FrameGetGlobalFrame(); -// if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL; + extern int Abc_FrameShowProgress( void * p ); + extern void * Abc_FrameGetGlobalFrame(); + if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL; p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t)); memset( p, 0, sizeof(Bar_Progress_t) ); p->pFile = pFile; diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 04adb7e3..5944cf56 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -20,6 +20,7 @@ #include "fra.h" #include "ioa.h" +#include "int.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -389,11 +390,15 @@ PRT( "Time", clock() - clkTotal ); clk = clock(); if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 ) { - extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); + Inter_ManParams_t Pars, * pPars = &Pars; int Depth; pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 0, 0, 1, 1, pParSec->fVeryVerbose, &Depth ); + + Inter_ManSetDefaultParams( pPars ); + pPars->fVerbose = pParSec->fVeryVerbose; + RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth ); + if ( pParSec->fVerbose ) { if ( RetValue == 1 ) @@ -454,7 +459,7 @@ PRT( "Time", clock() - clk ); iCount++; if ( !pParSec->fSilent ) printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter ); - pNew2 = Aig_ManDupOneOutput( pNew, i ); + pNew2 = Aig_ManDupOneOutput( pNew, i, 1 ); TimeLimitCopy = pParSec->TimeLimit; pParSec->TimeLimit = TimeLimit2; diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 53493201..d1d73a03 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -542,6 +542,35 @@ void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) SeeAlso [] ***********************************************************************/ +int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 ) +{ + unsigned * pSims0, * pSims1; + int i; + assert( !Aig_IsComplement(pObj0) ); + assert( !Aig_IsComplement(pObj1) ); + assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal ); + assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal ); + // get hold of the simulation information + pSims0 = Fra_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0; + pSims1 = Fra_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1; + // compare + for ( i = 0; i < p->nWordsFrame; i++ ) + if ( pSims0[i] != pSims1[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) { unsigned * pSims, * pSims0; diff --git a/src/aig/int/int.h b/src/aig/int/int.h new file mode 100644 index 00000000..bc9c1237 --- /dev/null +++ b/src/aig/int/int.h @@ -0,0 +1,85 @@ +/**CFile**************************************************************** + + FileName [int.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 - June 24, 2008.] + + Revision [$Id: int.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __INT_H__ +#define __INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +/* + The interpolation algorithm implemented here was introduced in the paper: + K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13. +*/ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// simulation manager +typedef struct Inter_ManParams_t_ Inter_ManParams_t; +struct Inter_ManParams_t_ +{ + int nBTLimit; // limit on the number of conflicts + int nFramesMax; // the max number timeframes to unroll + 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 fUsePudlak; // use Pudluk interpolation procedure + int fUseOther; // use other undisclosed option + int fUseMiniSat; // use MiniSat-1.14p instead of internal proof engine + int fCheckKstep; // check using K-step induction + int fUseBias; // bias decisions to global variables + int fUseBackward; // perform backward interpolation + int fVerbose; // print verbose statistics +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== intCore.c ==========================================================*/ +extern void Inter_ManSetDefaultParams( Inter_ManParams_t * p ); +extern int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c new file mode 100644 index 00000000..fa52e2b6 --- /dev/null +++ b/src/aig/int/intContain.c @@ -0,0 +1,328 @@ +/**CFile**************************************************************** + + FileName [intContain.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Interpolant containment checking.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intContain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" +#include "fra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks constainment of two interpolants.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) +{ + Aig_Man_t * pMiter, * pAigTemp; + int RetValue; + pMiter = Aig_ManCreateMiter( pNew, pOld, 1 ); +// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); +// Aig_ManStop( pAigTemp ); + RetValue = Fra_FraigMiterStatus( pMiter ); + if ( RetValue == -1 ) + { + pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); + RetValue = Fra_FraigMiterStatus( pAigTemp ); + Aig_ManStop( pAigTemp ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); + } + assert( RetValue != -1 ); + Aig_ManStop( pMiter ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Checks constainment of two interpolants.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ) +{ + Aig_Man_t * pMiter, * pAigTemp; + int RetValue; + pMiter = Aig_ManCreateMiter( pNew, pOld, 0 ); +// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); +// Aig_ManStop( pAigTemp ); + RetValue = Fra_FraigMiterStatus( pMiter ); + if ( RetValue == -1 ) + { + pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); + RetValue = Fra_FraigMiterStatus( pAigTemp ); + Aig_ManStop( pAigTemp ); +// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); + } + assert( RetValue != -1 ); + Aig_ManStop( pMiter ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for interpolation.] + + Description [The resulting manager is combinational. The primary inputs + corresponding to register outputs are ordered first.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) ); + Saig_ManForEachLo( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreatePi( pFrames ); + Vec_PtrPush( *pvMapReg, pObj->pData ); + } + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + pObjLo->pData = pObjLi->pData; + Vec_PtrPush( *pvMapReg, pObjLo->pData ); + } + } + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while mapping PIs into the given array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl ) +{ + Aig_Obj_t * pObj; + int i; + assert( Aig_ManPoNum(pOld) == 1 ); + // create the PIs + Aig_ManCleanData( pOld ); + Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( pOld, pObj, i ) + pObj->pData = ppNewPis[i]; + // duplicate internal nodes + Aig_ManForEachNode( pOld, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add one PO to new + pObj = Aig_ManPo( pOld, 0 ); + Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); +} + + +/**Function************************************************************* + + Synopsis [Checks constainment of two interpolants inductively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t ** ppNodes; + Vec_Ptr_t * vMapRegs; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int f, nRegs, status; + nRegs = Saig_ManRegNum(pTrans); + assert( nRegs > 0 ); + // generate the timeframes + pFrames = Inter_ManFramesLatches( pTrans, nSteps, &vMapRegs ); + assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs ); + // add main constraints to the timeframes + ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs); + if ( fBackward ) + { + // p -> !p -> ... -> !p + Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 ); + for ( f = 1; f <= nSteps; f++ ) + Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 ); + } + else + { + // !p -> p -> ... -> p + for ( f = 0; f < nSteps; f++ ) + Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 ); + Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 ); + } + Vec_PtrFree( vMapRegs ); + Aig_ManCleanup( pFrames ); + + // convert to CNF + pCnf = Cnf_Derive( pFrames, 0 ); + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); +// Cnf_DataFree( pCnf ); +// Aig_ManStop( pFrames ); + + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + return 1; + } + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + +// Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps ); + + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + + sat_solver_delete( pSat ); + return status == l_False; +} + +#include "fra.h" + +/**Function************************************************************* + + Synopsis [Check if cex satisfies uniqueness constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames ) +{ + extern int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 ); + extern void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ); + extern void Fra_SmlSimulateOne( Fra_Sml_t * p ); + + Fra_Sml_t * pSml; + Vec_Int_t * vPis; + Aig_Obj_t * pObj, * pObj0; + int i, k, v, iBit, * pCounterEx; + int Counter; + if ( nFrames == 1 ) + return 1; + if ( pSat->model.size == 0 ) + return 1; +// assert( Saig_ManPoNum(p) == 1 ); + assert( Aig_ManRegNum(p) > 0 ); + assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) ); + + // get the counter-example + vPis = Vec_IntAlloc( 100 ); + Aig_ManForEachPi( pCnf->pMan, pObj, k ) + Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] ); + assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) ); + pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize ); + Vec_IntFree( vPis ); + + // start a new sequential simulator + pSml = Fra_SmlStart( p, 0, nFrames, 1 ); + // assign simulation info for the registers + iBit = 0; + Aig_ManForEachLoSeq( p, pObj, i ) + Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], 0 ); + // assign simulation info for the primary inputs + for ( i = 0; i < nFrames; i++ ) + Aig_ManForEachPiSeq( p, pObj, k ) + Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i ); + assert( iBit == Aig_ManPiNum(pCnf->pMan) ); + // run simulation + Fra_SmlSimulateOne( pSml ); + + // check if the given output has failed +// RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) ); +// assert( RetValue ); + + // check values at the internal nodes + Counter = 0; + for ( i = 0; i < nFrames; i++ ) + for ( k = i+1; k < nFrames; k++ ) + { + for ( v = 0; v < Aig_ManRegNum(p); v++ ) + { + pObj0 = Aig_ManLo(p, v); + if ( !Fra_SmlNodesCompareInFrame( pSml, pObj0, pObj0, i, k ) ) + break; + } + if ( v == Aig_ManRegNum(p) ) + Counter++; + } + printf( "Uniquness does not hold in %d frames.\n", Counter ); + + Fra_SmlStop( pSml ); + free( pCounterEx ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c new file mode 100644 index 00000000..d959ff07 --- /dev/null +++ b/src/aig/int/intCore.c @@ -0,0 +1,286 @@ +/**CFile**************************************************************** + + FileName [intCore.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 - June 24, 2008.] + + Revision [$Id: intCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default values of interpolation parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManSetDefaultParams( Inter_ManParams_t * p ) +{ + memset( p, 0, sizeof(Inter_ManParams_t) ); + p->nBTLimit = 10000; // limit on the number of conflicts + p->nFramesMax = 40; // the max number timeframes to unroll + p->nFramesK = 1; // the number of timeframes to use in induction + p->fRewrite = 0; // use additional rewriting to simplify timeframes + p->fTransLoop = 1; // add transition into the init state under new PI var + p->fUsePudlak = 0; // use Pudluk interpolation procedure + p->fUseOther = 0; // use other undisclosed option + p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine + p->fCheckKstep = 1; // check using K-step induction + p->fUseBias = 0; // bias decisions to global variables + p->fUseBackward = 0; // perform backward interpolation + p->fVerbose = 0; // print verbose statistics +} + +/**Function************************************************************* + + Synopsis [Interplates 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 Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth ) +{ + extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ); + Inter_Man_t * p; + Aig_Man_t * pAigTemp; + int s, i, RetValue, Status, clk, clk2, clkTotal = clock(); + // sanity checks + assert( Saig_ManRegNum(pAig) > 0 ); + assert( Saig_ManPiNum(pAig) > 0 ); + assert( Saig_ManPoNum(pAig) == 1 ); +/* + if ( Inter_ManCheckInitialState(pAig) ) + { + printf( "Property trivially fails in the initial state.\n" ); + return 0; + } + if ( Inter_ManCheckAllStates(pAig) ) + { + printf( "Property trivially holds in all states.\n" ); + return 1; + } +*/ + // create interpolation manager + // can perform SAT sweeping and/or rewriting of this AIG... + p = Inter_ManCreate( pAig, pPars ); + if ( pPars->fTransLoop ) + p->pAigTrans = Inter_ManStartOneOutput( pAig, 0 ); + else + p->pAigTrans = Inter_ManStartDuplicated( pAig ); + // derive CNF for the transformed AIG +clk = clock(); + p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); +p->timeCnf += clock() - clk; + if ( pPars->fVerbose ) + { + printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d. CNF: Var/Cla = %d/%d.\n", + Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), + Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig), + p->pCnfAig->nVars, p->pCnfAig->nClauses ); + } + + // derive interpolant + *pDepth = -1; + p->nFrames = 1; + for ( s = 0; ; s++ ) + { +clk2 = clock(); + // initial state + if ( pPars->fUseBackward ) + p->pInter = Inter_ManStartOneOutput( pAig, 1 ); + else + p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) ); + assert( Aig_ManPoNum(p->pInter) == 1 ); +clk = clock(); + p->pCnfInter = Cnf_Derive( p->pInter, 0 ); +p->timeCnf += clock() - clk; + // timeframes + p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward ); +clk = clock(); + if ( pPars->fRewrite ) + { + p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 ); + Aig_ManStop( pAigTemp ); +// p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 ); +// Aig_ManStop( pAigTemp ); + } +p->timeRwr += clock() - clk; + // can also do SAT sweeping on the timeframes... +clk = clock(); + if ( pPars->fUseBackward ) + p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) ); + else + p->pCnfFrames = Cnf_Derive( p->pFrames, 0 ); +p->timeCnf += clock() - clk; + // report statistics + if ( pPars->fVerbose ) + { + printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d. ", + s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) ); + PRT( "Time", clock() - clk2 ); + } + // iterate the interpolation procedure + for ( i = 0; ; i++ ) + { + if ( p->nFrames + i >= pPars->nFramesMax ) + { + if ( pPars->fVerbose ) + printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax ); + p->timeTotal = clock() - clkTotal; + Inter_ManStop( p ); + return -1; + } + + // perform interpolation + clk = clock(); +#ifdef ABC_USE_LIBRARIES + if ( pPars->fUseMiniSat ) + { + assert( !pPars->fUseBackward ); + RetValue = Inter_ManPerformOneStepM114p( p, pPars->fUsePudlak, pPars->fUseOther ); + } + else +#endif + RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward ); + + if ( pPars->fVerbose ) + { + printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ", + i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur ); + PRT( "Time", clock() - clk ); + } + if ( RetValue == 0 ) // found a (spurious?) counter-example + { + if ( i == 0 ) // real counterexample + { + if ( pPars->fVerbose ) + printf( "Found a real counterexample in the first frame.\n" ); + p->timeTotal = clock() - clkTotal; + *pDepth = p->nFrames + 1; + Inter_ManStop( p ); + return 0; + } + // likely spurious counter-example + p->nFrames += i; + Inter_ManClean( p ); + break; + } + else if ( RetValue == -1 ) // timed out + { + if ( pPars->fVerbose ) + printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit ); + assert( p->nConfCur >= p->nConfLimit ); + p->timeTotal = clock() - clkTotal; + Inter_ManStop( p ); + return -1; + } + assert( RetValue == 1 ); // found new interpolant + // compress the interpolant +clk = clock(); + if ( p->pInterNew ) + { + p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 ); + Aig_ManStop( pAigTemp ); + } +p->timeRwr += clock() - clk; + + // check if interpolant is trivial + if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) ) + { +// printf( "interpolant is constant 0\n" ); + if ( pPars->fVerbose ) + printf( "The problem is trivially true for all states.\n" ); + p->timeTotal = clock() - clkTotal; + Inter_ManStop( p ); + return 1; + } + + // check containment of interpolants +clk = clock(); + if ( pPars->fCheckKstep ) // k-step unique-state induction + { + if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) ) + Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward ); + else + Status = 0; + } + else // combinational containment + { + if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) ) + Status = Inter_ManCheckContainment( p->pInterNew, p->pInter ); + else + Status = 0; + } +p->timeEqu += clock() - clk; + if ( Status ) // contained + { + if ( pPars->fVerbose ) + printf( "Proved containment of interpolants.\n" ); + p->timeTotal = clock() - clkTotal; + Inter_ManStop( p ); + return 1; + } + // save interpolant and convert it into CNF + if ( pPars->fTransLoop ) + { + Aig_ManStop( p->pInter ); + p->pInter = p->pInterNew; + } + else + { + p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 ); + Aig_ManStop( pAigTemp ); + Aig_ManStop( p->pInterNew ); + // compress the interpolant +clk = clock(); + p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 ); + Aig_ManStop( pAigTemp ); +p->timeRwr += clock() - clk; + } + p->pInterNew = NULL; + Cnf_DataFree( p->pCnfInter ); +clk = clock(); + p->pCnfInter = Cnf_Derive( p->pInter, 0 ); +p->timeCnf += clock() - clk; + } + } + assert( 0 ); + return RetValue; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intDup.c b/src/aig/int/intDup.c new file mode 100644 index 00000000..3e5aaa7e --- /dev/null +++ b/src/aig/int/intDup.c @@ -0,0 +1,161 @@ +/**CFile**************************************************************** + + FileName [intDup.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Specialized AIG duplication procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create trivial AIG manager for the init state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManStartInitState( int nRegs ) +{ + Aig_Man_t * p; + Aig_Obj_t * pRes; + Aig_Obj_t ** ppInputs; + int i; + assert( nRegs > 0 ); + ppInputs = ALLOC( Aig_Obj_t *, nRegs ); + p = Aig_ManStart( nRegs ); + for ( i = 0; i < nRegs; i++ ) + ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) ); + pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND ); + Aig_ObjCreatePo( p, pRes ); + free( ppInputs ); + return p; +} + +/**Function************************************************************* + + Synopsis [Duplicate the AIG w/o POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( Aig_ManRegNum(p) > 0 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // set registers + pNew->nRegs = p->nRegs; + pNew->nTruePis = p->nTruePis; + pNew->nTruePos = 0; + // duplicate internal nodes + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create register inputs with MUXes + Saig_ManForEachLi( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ManCleanup( pNew ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicate the AIG w/o POs and transforms to transit into init state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized" + int i; + assert( Aig_ManRegNum(p) > 0 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + { + if ( i == Saig_ManPiNum(p) ) + pCtrl = Aig_ObjCreatePi( pNew ); + pObj->pData = Aig_ObjCreatePi( pNew ); + } + // set registers + pNew->nRegs = fAddFirstPo? 0 : p->nRegs; + pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1; + pNew->nTruePos = fAddFirstPo; + // duplicate internal nodes + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add the PO + if ( fAddFirstPo ) + { + pObj = Aig_ManPo( p, 0 ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + else + { + // create register inputs with MUXes + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + { + pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); + // pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) ); + Aig_ObjCreatePo( pNew, pObj ); + } + } + Aig_ManCleanup( pNew ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intFrames.c b/src/aig/int/intFrames.c new file mode 100644 index 00000000..809cb06b --- /dev/null +++ b/src/aig/int/intFrames.c @@ -0,0 +1,103 @@ +/**CFile**************************************************************** + + FileName [intFrames.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Sequential AIG unrolling for interpolation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intFrames.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for interpolation.] + + Description [The resulting manager is combinational. The primary inputs + corresponding to register outputs are ordered first. The only POs of the + manager is the property output of the last timeframe.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + assert( Saig_ManPoNum(pAig) == 1 ); + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + if ( fAddRegOuts ) + { + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + } + else + { + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + } + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + // create POs for each register output + if ( fAddRegOuts ) + { + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + } + // create the only PO of the manager + else + { + pObj = Aig_ManPo( pAig, 0 ); + Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h new file mode 100644 index 00000000..ea2c48b8 --- /dev/null +++ b/src/aig/int/intInt.h @@ -0,0 +1,127 @@ +/**CFile**************************************************************** + + FileName [intInt.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 - June 24, 2008.] + + Revision [$Id: intInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __INT_INT_H__ +#define __INT_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "saig.h" +#include "cnf.h" +#include "satSolver.h" +#include "satStore.h" +#include "int.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// simulation manager +typedef struct Inter_Man_t_ Inter_Man_t; +struct Inter_Man_t_ +{ + // AIG manager + Aig_Man_t * pAig; // the original AIG manager + Aig_Man_t * pAigTrans; // the transformed original AIG manager + Cnf_Dat_t * pCnfAig; // CNF for the original manager + // interpolant + Aig_Man_t * pInter; // the current interpolant + Cnf_Dat_t * pCnfInter; // CNF for the current interplant + // timeframes + Aig_Man_t * pFrames; // the timeframes + Cnf_Dat_t * pCnfFrames; // CNF for the timeframes + // other data + Vec_Int_t * vVarsAB; // the variables participating in + // temporary place for the new interpolant + Aig_Man_t * pInterNew; + Vec_Ptr_t * vInters; + // parameters + int nFrames; // the number of timeframes + int nConfCur; // the current number of conflicts + int nConfLimit; // the limit on the number of conflicts + int fVerbose; // the verbosiness flag + // runtime + int timeRwr; + int timeCnf; + int timeSat; + int timeInt; + int timeEqu; + int timeOther; + int timeTotal; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== intContain.c ==========================================================*/ +extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ); +extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ); +extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward ); + +/*=== intDup.c ==========================================================*/ +extern Aig_Man_t * Inter_ManStartInitState( int nRegs ); +extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ); +extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ); + +/*=== intFrames.c ==========================================================*/ +extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts ); + +/*=== intMan.c ==========================================================*/ +extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars ); +extern void Inter_ManClean( Inter_Man_t * p ); +extern void Inter_ManStop( Inter_Man_t * p ); + +/*=== intM114.c ==========================================================*/ +extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ); + +/*=== intM114p.c ==========================================================*/ +#ifdef ABC_USE_LIBRARIES +extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther ); +#endif + +/*=== intUtil.c ==========================================================*/ +extern int Inter_ManCheckInitialState( Aig_Man_t * p ); +extern int Inter_ManCheckAllStates( Aig_Man_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/int/intInter.c b/src/aig/int/intInter.c new file mode 100644 index 00000000..592eedcf --- /dev/null +++ b/src/aig/int/intInter.c @@ -0,0 +1,140 @@ +/**CFile**************************************************************** + + FileName [intInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Experimental procedures to derive and compare interpolants.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther ) +{ + Aig_Man_t * pInterC; + assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) ); + pInterC = Aig_ManDupSimple( pInter ); + Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 ); + assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) ); + return pInterC; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManVerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) +{ + extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); + Aig_Man_t * pLower, * pUpper, * pInterC; + int RetValue1, RetValue2; + + pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 ); + pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 ); + Aig_ManFlipFirstPo( pUpper ); + + pInterC = Inter_ManDupExpand( pInter, pLower ); + RetValue1 = Inter_ManCheckContainment( pLower, pInterC ); + Aig_ManStop( pInterC ); + + pInterC = Inter_ManDupExpand( pInter, pUpper ); + RetValue2 = Inter_ManCheckContainment( pInterC, pUpper ); + Aig_ManStop( pInterC ); + + if ( RetValue1 && RetValue2 ) + printf( "Im is correct.\n" ); + if ( !RetValue1 ) + printf( "Property A => Im fails.\n" ); + if ( !RetValue2 ) + printf( "Property Im => !B fails.\n" ); + + Aig_ManStop( pLower ); + Aig_ManStop( pUpper ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManVerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) +{ + extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); + Aig_Man_t * pLower, * pUpper, * pInterC; + int RetValue1, RetValue2; + + pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 ); + pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 ); + Aig_ManFlipFirstPo( pUpper ); + + pInterC = Inter_ManDupExpand( pInter, pLower ); +//Aig_ManPrintStats( pLower ); +//Aig_ManPrintStats( pUpper ); +//Aig_ManPrintStats( pInterC ); +//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL ); + RetValue1 = Inter_ManCheckContainment( pLower, pInterC ); + Aig_ManStop( pInterC ); + + pInterC = Inter_ManDupExpand( pInter, pUpper ); + RetValue2 = Inter_ManCheckContainment( pInterC, pUpper ); + Aig_ManStop( pInterC ); + + if ( RetValue1 && RetValue2 ) + printf( "Ip is correct.\n" ); + if ( !RetValue1 ) + printf( "Property A => Ip fails.\n" ); + if ( !RetValue2 ) + printf( "Property Ip => !B fails.\n" ); + + Aig_ManStop( pLower ); + Aig_ManStop( pUpper ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c new file mode 100644 index 00000000..f92ba179 --- /dev/null +++ b/src/aig/int/intM114.c @@ -0,0 +1,311 @@ +/**CFile**************************************************************** + + FileName [intM114.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Intepolation using ABC's proof generator added to MiniSat-1.14c.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intM114.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the SAT solver for one interpolation run.] + + Description [pInter is the previous interpolant. pAig is one time frame. + pFrames is the unrolled time frames.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * Inter_ManDeriveSatSolver( + Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, + Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, + Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, + Vec_Int_t * vVarsAB, int fUseBackward ) +{ + sat_solver * pSat; + Aig_Obj_t * pObj, * pObj2; + int i, Lits[2]; + +//Aig_ManDumpBlif( pInter, "out_inter.blif", NULL, NULL ); +//Aig_ManDumpBlif( pAig, "out_aig.blif", NULL, NULL ); +//Aig_ManDumpBlif( pFrames, "out_frames.blif", NULL, NULL ); + + // sanity checks + assert( Aig_ManRegNum(pInter) == 0 ); + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pFrames) == 0 ); + assert( Aig_ManPoNum(pInter) == 1 ); + assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 ); + assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); +// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); + + // prepare CNFs + Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); + + // start the solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars ); + + // add clauses of A + // interpolant + for ( i = 0; i < pCnfInter->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) ) + { + sat_solver_delete( pSat ); + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); + return NULL; + } + } + // connector clauses + if ( fUseBackward ) + { + Saig_ManForEachLi( pAig, pObj2, i ) + { + if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) ) + pObj = Aig_ManPi( pInter, i ); + else + { + assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) ); + pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i ); + } + + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + else + { + Aig_ManForEachPi( pInter, pObj, i ) + { + pObj2 = Saig_ManLo( pAig, i ); + + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + // one timeframe + for ( i = 0; i < pCnfAig->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Vec_IntClear( vVarsAB ); + if ( fUseBackward ) + { + Aig_ManForEachPo( pFrames, pObj, i ) + { + assert( pCnfFrames->pVarNums[pObj->Id] >= 0 ); + Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); + + pObj2 = Saig_ManLo( pAig, i ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + else + { + Aig_ManForEachPi( pFrames, pObj, i ) + { + if ( i == Aig_ManRegNum(pAig) ) + break; + Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); + + pObj2 = Saig_ManLi( pAig, i ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + } + // add clauses of B + sat_solver_store_mark_clauses_a( pSat ); + for ( i = 0; i < pCnfFrames->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) + { + pSat->fSolved = 1; + break; + } + } + sat_solver_store_mark_roots( pSat ); + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Performs one SAT run with interpolation.] + + Description [Returns 1 if proven. 0 if failed. -1 if undecided.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ) +{ + sat_solver * pSat; + void * pSatCnf = NULL; + Inta_Man_t * pManInterA; +// Intb_Man_t * pManInterB; + int * pGlobalVars; + int clk, status, RetValue; + int i, Var; + assert( p->pInterNew == NULL ); + + // derive the SAT solver + pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward ); + if ( pSat == NULL ) + { + p->pInterNew = NULL; + return 1; + } + + // collect global variables + pGlobalVars = CALLOC( int, sat_solver_nvars(pSat) ); + Vec_IntForEachEntry( p->vVarsAB, Var, i ) + pGlobalVars[Var] = 1; + pSat->pGlobalVars = fUseBias? pGlobalVars : NULL; + + // solve the problem +clk = clock(); + status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); + p->nConfCur = pSat->stats.conflicts; +p->timeSat += clock() - clk; + + pSat->pGlobalVars = NULL; + FREE( pGlobalVars ); + if ( status == l_False ) + { + pSatCnf = sat_solver_store_release( pSat ); + RetValue = 1; + } + else if ( status == l_True ) + { + RetValue = 0; + } + else + { + RetValue = -1; + } + sat_solver_delete( pSat ); + if ( pSatCnf == NULL ) + return RetValue; + + // create the resulting manager +clk = clock(); +/* + if ( !fUseIp ) + { + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); + Inta_ManFree( pManInterA ); + } + else + { + Aig_Man_t * pInterNew2; + int RetValue; + + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); +// Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew ); + Inta_ManFree( pManInterA ); + + pManInterB = Intb_ManAlloc(); + pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 ); + Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 ); + Intb_ManFree( pManInterB ); + + // check relationship + RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew ); + if ( RetValue ) + printf( "Equivalence \"Ip == Im\" holds\n" ); + else + { +// printf( "Equivalence \"Ip == Im\" does not hold\n" ); + RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew ); + if ( RetValue ) + printf( "Containment \"Ip -> Im\" holds\n" ); + else + printf( "Containment \"Ip -> Im\" does not hold\n" ); + + RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 ); + if ( RetValue ) + printf( "Containment \"Im -> Ip\" holds\n" ); + else + printf( "Containment \"Im -> Ip\" does not hold\n" ); + } + + Aig_ManStop( pInterNew2 ); + } +*/ + + pManInterA = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); + Inta_ManFree( pManInterA ); + +p->timeInt += clock() - clk; + Sto_ManFree( pSatCnf ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c new file mode 100644 index 00000000..69c643ae --- /dev/null +++ b/src/aig/int/intM114p.c @@ -0,0 +1,435 @@ +/**CFile**************************************************************** + + FileName [intM114p.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Intepolation using interfaced to MiniSat-1.14p.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intM114p.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifdef ABC_USE_LIBRARIES + +#include "intInt.h" +#include "m114p.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the SAT solver for one interpolation run.] + + Description [pInter is the previous interpolant. pAig is one time frame. + pFrames is the unrolled time frames.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +M114p_Solver_t Inter_ManDeriveSatSolverM114p( + Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, + Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, + Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, + Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars ) +{ + M114p_Solver_t pSat; + Aig_Obj_t * pObj, * pObj2; + int i, Lits[2]; + + // sanity checks + assert( Aig_ManRegNum(pInter) == 0 ); + assert( Aig_ManRegNum(pAig) > 0 ); + assert( Aig_ManRegNum(pFrames) == 0 ); + assert( Aig_ManPoNum(pInter) == 1 ); + assert( Aig_ManPoNum(pFrames) == 1 ); + assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); +// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); + + // prepare CNFs + Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); + + *pvMapRoots = Vec_IntAlloc( 10000 ); + *pvMapVars = Vec_IntAlloc( 0 ); + Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 ); + for ( i = 0; i < pCnfFrames->nVars; i++ ) + Vec_IntWriteEntry( *pvMapVars, i, -2 ); + + // start the solver + pSat = M114p_SolverNew( 1 ); + M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars ); + + // add clauses of A + // interpolant + for ( i = 0; i < pCnfInter->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Aig_ManForEachPi( pInter, pObj, i ) + { + pObj2 = Saig_ManLo( pAig, i ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // one timeframe + for ( i = 0; i < pCnfAig->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) ) + assert( 0 ); + } + // connector clauses + Aig_ManForEachPi( pFrames, pObj, i ) + { + if ( i == Aig_ManRegNum(pAig) ) + break; +// Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); + Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i ); + + pObj2 = Saig_ManLi( pAig, i ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); + Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); + Vec_IntPush( *pvMapRoots, 0 ); + if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // add clauses of B + for ( i = 0; i < pCnfFrames->nClauses; i++ ) + { + Vec_IntPush( *pvMapRoots, 1 ); + if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) + { +// assert( 0 ); + break; + } + } + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); + Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); + return pSat; +} + + +/**Function************************************************************* + + Synopsis [Performs one resolution step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManResolveM114p( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar ) +{ + int i, k, iLit = -1, fFound = 0; + // find the variable in the clause + for ( i = 0; i < vResolvent->nSize; i++ ) + if ( lit_var(vResolvent->pArray[i]) == iVar ) + { + iLit = vResolvent->pArray[i]; + vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize]; + break; + } + assert( iLit != -1 ); + // add other variables + for ( i = 0; i < nLits; i++ ) + { + if ( lit_var(pLits[i]) == iVar ) + { + assert( iLit == lit_neg(pLits[i]) ); + fFound = 1; + continue; + } + // check if this literal appears + for ( k = 0; k < vResolvent->nSize; k++ ) + if ( vResolvent->pArray[k] == pLits[i] ) + break; + if ( k < vResolvent->nSize ) + continue; + // add this literal + Vec_IntPush( vResolvent, pLits[i] ); + } + assert( fFound ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + Vec_Int_t * vLiterals, * vClauses, * vResolvent; + int * pLitsNext, nLitsNext, nOffset, iLit; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, v, iVar; + assert( M114p_SolverProofIsReady(s) ); + vInters = Vec_PtrAlloc( 1000 ); + + vLiterals = Vec_IntAlloc( 10000 ); + vClauses = Vec_IntAlloc( 1000 ); + vResolvent = Vec_IntAlloc( 100 ); + + // create elementary variables + p = Aig_ManStart( 10000 ); + Vec_IntForEachEntry( vMapVars, iVar, i ) + if ( iVar >= 0 ) + Aig_IthVar(p, iVar); + // process root clauses + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + pInter = Aig_ManConst1(p); + else // clause of A + pInter = Aig_ManConst0(p); + Vec_PtrPush( vInters, pInter ); + + // save the root clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, nLits ); + for ( v = 0; v < nLits; v++ ) + Vec_IntPush( vLiterals, pLits[v] ); + } + assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + pInter = Vec_PtrEntry( vInters, pClauses[0] ); + + // initialize the resolvent + nOffset = Vec_IntEntry( vClauses, pClauses[0] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Vec_IntClear( vResolvent ); + for ( v = 0; v < nLitsNext; v++ ) + Vec_IntPush( vResolvent, pLitsNext[v] ); + + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + + // resolve it with the next clause + nOffset = Vec_IntEntry( vClauses, pClauses[k+1] ); + nLitsNext = Vec_IntEntry( vLiterals, nOffset ); + pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; + Inter_ManResolveM114p( vResolvent, pLitsNext, nLitsNext, pVars[k] ); + + if ( iVar == -1 ) // var of A + pInter = Aig_Or( p, pInter, pInter2 ); + else if ( iVar == -2 ) // var of B + pInter = Aig_And( p, pInter, pInter2 ); + else // var of C + { + // check polarity of the pivot variable in the clause + for ( v = 0; v < nLitsNext; v++ ) + if ( lit_var(pLitsNext[v]) == pVars[k] ) + break; + assert( v < nLitsNext ); + pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) ); + pInter = Aig_Mux( p, pVar, pInter, pInter2 ); + } + } + Vec_PtrPush( vInters, pInter ); + + // store the resulting clause + Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); + Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) ); + Vec_IntForEachEntry( vResolvent, iLit, v ) + Vec_IntPush( vLiterals, iLit ); + } + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause + Vec_PtrFree( vInters ); + Vec_IntFree( vLiterals ); + Vec_IntFree( vClauses ); + Vec_IntFree( vResolvent ); + Aig_ObjCreatePo( p, pInter ); + Aig_ManCleanup( p ); + return p; +} + + +/**Function************************************************************* + + Synopsis [Computes interpolant using MiniSat-1.14p.] + + Description [Assumes that the solver returned UNSAT and proof + logging was enabled. Array vMapRoots maps number of each root clause + into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT + solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), + where <num> is the var's 0-based number in the ordering of C variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) +{ + Aig_Man_t * p; + Aig_Obj_t * pInter, * pInter2, * pVar; + Vec_Ptr_t * vInters; + int * pLits, * pClauses, * pVars; + int nLits, nVars, i, k, iVar; + + assert( M114p_SolverProofIsReady(s) ); + + vInters = Vec_PtrAlloc( 1000 ); + // process root clauses + p = Aig_ManStart( 10000 ); + M114p_SolverForEachRoot( s, &pLits, nLits, i ) + { + if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B + pInter = Aig_ManConst1(p); + else // clause of A + { + pInter = Aig_ManConst0(p); + for ( k = 0; k < nLits; k++ ) + { + iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) ); + if ( iVar < 0 ) // var of A or B + continue; + // this is a variable of C + pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) ); + pInter = Aig_Or( p, pInter, pVar ); + } + } + Vec_PtrPush( vInters, pInter ); + } +// assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); + + // process learned clauses + M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) + { + pInter = Vec_PtrEntry( vInters, pClauses[0] ); + for ( k = 0; k < nVars; k++ ) + { + iVar = Vec_IntEntry( vMapVars, pVars[k] ); + pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); + if ( iVar == -1 ) // var of A + pInter = Aig_Or( p, pInter, pInter2 ); + else // var of B or C + pInter = Aig_And( p, pInter, pInter2 ); + } + Vec_PtrPush( vInters, pInter ); + } + + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); + Vec_PtrFree( vInters ); + Aig_ObjCreatePo( p, pInter ); + Aig_ManCleanup( p ); + assert( Aig_ManCheck(p) ); + return p; +} + + +/**Function************************************************************* + + Synopsis [Performs one SAT run with interpolation.] + + Description [Returns 1 if proven. 0 if failed. -1 if undecided.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther ) +{ + M114p_Solver_t pSat; + Vec_Int_t * vMapRoots, * vMapVars; + int clk, status, RetValue; + assert( p->pInterNew == NULL ); + // derive the SAT solver + pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter, + p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, + &vMapRoots, &vMapVars ); + // solve the problem +clk = clock(); + status = M114p_SolverSolve( pSat, NULL, NULL, 0 ); + p->nConfCur = M114p_SolverGetConflictNum( pSat ); +p->timeSat += clock() - clk; + if ( status == 0 ) + { + RetValue = 1; +// Inter_ManpInterpolateM114Report( pSat, vMapRoots, vMapVars ); + +clk = clock(); + if ( fUsePudlak ) + p->pInterNew = Inter_ManInterpolateM114pPudlak( pSat, vMapRoots, vMapVars ); + else + p->pInterNew = Inter_ManpInterpolateM114( pSat, vMapRoots, vMapVars ); +p->timeInt += clock() - clk; + } + else if ( status == 1 ) + { + RetValue = 0; + } + else + { + RetValue = -1; + } + M114p_SolverDelete( pSat ); + Vec_IntFree( vMapRoots ); + Vec_IntFree( vMapVars ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + + diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c new file mode 100644 index 00000000..b9b2bce9 --- /dev/null +++ b/src/aig/int/intMan.c @@ -0,0 +1,128 @@ +/**CFile**************************************************************** + + FileName [intMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Interpolation manager procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Frees the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars ) +{ + Inter_Man_t * p; + // create interpolation manager + p = ALLOC( Inter_Man_t, 1 ); + memset( p, 0, sizeof(Inter_Man_t) ); + p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) ); + p->nConfLimit = pPars->nBTLimit; + p->fVerbose = pPars->fVerbose; + p->pAig = pAig; + return p; +} + +/**Function************************************************************* + + Synopsis [Frees the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManClean( Inter_Man_t * p ) +{ + if ( p->pCnfInter ) + Cnf_DataFree( p->pCnfInter ); + if ( p->pCnfFrames ) + Cnf_DataFree( p->pCnfFrames ); + if ( p->pInter ) + Aig_ManStop( p->pInter ); + if ( p->pFrames ) + Aig_ManStop( p->pFrames ); +} + +/**Function************************************************************* + + Synopsis [Frees the interpolation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Inter_ManStop( Inter_Man_t * p ) +{ + if ( p->fVerbose ) + { + p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu; + printf( "Runtime statistics:\n" ); + PRTP( "Rewriting ", p->timeRwr, p->timeTotal ); + PRTP( "CNF mapping", p->timeCnf, p->timeTotal ); + PRTP( "SAT solving", p->timeSat, p->timeTotal ); + PRTP( "Interpol ", p->timeInt, p->timeTotal ); + PRTP( "Containment", p->timeEqu, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + } + + if ( p->pCnfAig ) + Cnf_DataFree( p->pCnfAig ); + if ( p->pCnfFrames ) + Cnf_DataFree( p->pCnfFrames ); + if ( p->pCnfInter ) + Cnf_DataFree( p->pCnfInter ); + Vec_IntFree( p->vVarsAB ); + if ( p->pAigTrans ) + Aig_ManStop( p->pAigTrans ); + if ( p->pFrames ) + Aig_ManStop( p->pFrames ); + if ( p->pInter ) + Aig_ManStop( p->pInter ); + if ( p->pInterNew ) + Aig_ManStop( p->pInterNew ); + free( p ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/intUtil.c b/src/aig/int/intUtil.c new file mode 100644 index 00000000..722a3611 --- /dev/null +++ b/src/aig/int/intUtil.c @@ -0,0 +1,92 @@ +/**CFile**************************************************************** + + FileName [intUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Interpolation engine.] + + Synopsis [Various interpolation utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 24, 2008.] + + Revision [$Id: intUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "intInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Returns 1 if the property fails in the initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckInitialState( Aig_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int status; + int clk = clock(); + pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 1 ); + Cnf_DataFree( pCnf ); + if ( pSat == NULL ) + return 0; + status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + sat_solver_delete( pSat ); + PRT( "Time", clock() - clk ); + return status == l_True; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the property holds in all states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Inter_ManCheckAllStates( Aig_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + sat_solver * pSat; + int status; + int clk = clock(); + pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); + pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Cnf_DataFree( pCnf ); + if ( pSat == NULL ) + return 1; + status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); + sat_solver_delete( pSat ); + PRT( "Time", clock() - clk ); + return status == l_False; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/int/module.make b/src/aig/int/module.make new file mode 100644 index 00000000..0652ab39 --- /dev/null +++ b/src/aig/int/module.make @@ -0,0 +1,9 @@ +SRC += src/aig/int/intContain.c \ + src/aig/int/intCore.c \ + src/aig/int/intDup.c \ + src/aig/int/intFrames.c \ + src/aig/int/intInter.c \ + src/aig/int/intM114.c \ + src/aig/int/intM114p.c \ + src/aig/int/intMan.c \ + src/aig/int/intUtil.c diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 79cd640a..3ef1d60e 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -803,8 +803,8 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan pNtk->pManTime = Tim_ManDup( pManTime, 0 ); else pNtk->pManTime = Tim_ManDup( p->pManTime, 0 ); -// Nwk_ManRemoveDupFanins( pNtk, 0 ); -// assert( Nwk_ManCheck( pNtk ) ); + Nwk_ManRemoveDupFanins( pNtk, 0 ); + assert( Nwk_ManCheck( pNtk ) ); return pNtk; } diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index bd39956e..38568d26 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -145,13 +145,20 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig ) continue; assert( pObj != pObjRepr ); pNet = pObj->pData; - // do not reduce the net if it is driven by a multi-output box - if ( Ntl_ObjIsBox(pNet->pDriver) && Ntl_ObjFanoutNum(pNet->pDriver) > 1 ) - continue; - // do not reduce the net if it has no-merge attribute - if ( Ntl_ObjIsBox(pNet->pDriver) && pNet->pDriver->pImplem->attrNoMerge ) - continue; pNetRepr = pObjRepr->pData; + // consider special cases, when the net should not be reduced + if ( Ntl_ObjIsBox(pNet->pDriver) ) + { + // do not reduce the net if it is driven by a multi-output box + if ( Ntl_ObjFanoutNum(pNet->pDriver) > 1 ) + continue; + // do not reduce the net if it has no-merge attribute + if ( pNet->pDriver->pImplem->attrNoMerge ) + continue; + // do not reduce the net if the replacement net has no-merge attribute + if ( pNetRepr != NULL && pNetRepr->pDriver->pImplem->attrNoMerge ) + continue; + } if ( pNetRepr == NULL ) { // this is the constant node diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index b9a18ce2..5a0f98da 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,7 +1,6 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigCone.c \ src/aig/saig/saigHaig.c \ - src/aig/saig/saigInter.c \ src/aig/saig/saigIoa.c \ src/aig/saig/saigMiter.c \ src/aig/saig/saigPhase.c \ @@ -9,5 +8,4 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigRetMin.c \ src/aig/saig/saigRetStep.c \ src/aig/saig/saigScl.c \ - src/aig/saig/saigTrans.c \ - src/aig/saig/saigUnique.c + src/aig/saig/saigTrans.c diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index e2fbda2d..88cc2c2d 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -30,6 +30,7 @@ extern "C" { //////////////////////////////////////////////////////////////////////// #include "aig.h" +#include "int.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -85,7 +86,7 @@ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); /*=== saigInter.c ==========================================================*/ -extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); +extern int Saig_Interpolate( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth ); /*=== saigMiter.c ==========================================================*/ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); /*=== saigPhase.c ==========================================================*/ diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c deleted file mode 100644 index 65fe6d87..00000000 --- a/src/aig/saig/saigInter.c +++ /dev/null @@ -1,1735 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigInter.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Interplation for unbounded model checking.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "fra.h" -#include "cnf.h" -#include "satStore.h" - -/* - The interpolation algorithm implemented here was introduced in the paper: - K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13. -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// simulation manager -typedef struct Saig_IntMan_t_ Saig_IntMan_t; -struct Saig_IntMan_t_ -{ - // AIG manager - Aig_Man_t * pAig; // the original AIG manager - Aig_Man_t * pAigTrans; // the transformed original AIG manager - Cnf_Dat_t * pCnfAig; // CNF for the original manager - // interpolant - Aig_Man_t * pInter; // the current interpolant - Cnf_Dat_t * pCnfInter; // CNF for the current interplant - // timeframes - Aig_Man_t * pFrames; // the timeframes - Cnf_Dat_t * pCnfFrames; // CNF for the timeframes - // other data - Vec_Int_t * vVarsAB; // the variables participating in - // temporary place for the new interpolant - Aig_Man_t * pInterNew; - Vec_Ptr_t * vInters; - // parameters - int nFrames; // the number of timeframes - int nConfCur; // the current number of conflicts - int nConfLimit; // the limit on the number of conflicts - int fVerbose; // the verbosiness flag - // runtime - int timeRwr; - int timeCnf; - int timeSat; - int timeInt; - int timeEqu; - int timeOther; - int timeTotal; -}; - -#ifdef ABC_USE_LIBRARIES -static int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther ); -#endif - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Create trivial AIG manager for the init state.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManInit( int nRegs ) -{ - Aig_Man_t * p; - Aig_Obj_t * pRes; - Aig_Obj_t ** ppInputs; - int i; - assert( nRegs > 0 ); - ppInputs = ALLOC( Aig_Obj_t *, nRegs ); - p = Aig_ManStart( nRegs ); - for ( i = 0; i < nRegs; i++ ) - ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) ); - pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND ); - Aig_ObjCreatePo( p, pRes ); - free( ppInputs ); - return p; -} - -/**Function************************************************************* - - Synopsis [Duplicate the AIG w/o POs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManDuplicated( Aig_Man_t * p ) -{ - Aig_Man_t * pNew; - Aig_Obj_t * pObj; - int i; - assert( Aig_ManRegNum(p) > 0 ); - // create the new manager - pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->pSpec = Aig_UtilStrsav( p->pSpec ); - // create the PIs - Aig_ManCleanData( p ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( p, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pNew ); - // set registers - pNew->nRegs = p->nRegs; - pNew->nTruePis = p->nTruePis; - pNew->nTruePos = 0; - // duplicate internal nodes - Aig_ManForEachNode( p, pObj, i ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create register inputs with MUXes - Saig_ManForEachLi( p, pObj, i ) - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); - Aig_ManCleanup( pNew ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Duplicate the AIG w/o POs and transforms to transit into init state.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p ) -{ - Aig_Man_t * pNew; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized" - int i; - assert( Aig_ManRegNum(p) > 0 ); - // create the new manager - pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->pSpec = Aig_UtilStrsav( p->pSpec ); - // create the PIs - Aig_ManCleanData( p ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( p, pObj, i ) - { - if ( i == Saig_ManPiNum(p) ) - pCtrl = Aig_ObjCreatePi( pNew ); - pObj->pData = Aig_ObjCreatePi( pNew ); - } - // set registers - pNew->nRegs = p->nRegs; - pNew->nTruePis = p->nTruePis + 1; - pNew->nTruePos = 0; - // duplicate internal nodes - Aig_ManForEachNode( p, pObj, i ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // create register inputs with MUXes - Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) - { - pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); -// pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) ); - Aig_ObjCreatePo( pNew, pObj ); - } - Aig_ManCleanup( pNew ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Create timeframes of the manager for interpolation.] - - Description [The resulting manager is combinational. The primary inputs - corresponding to register outputs are ordered first. The only POs of the - manager is the property output of the last timeframe.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManFramesInter( Aig_Man_t * pAig, int nFrames ) -{ - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, f; - assert( Saig_ManRegNum(pAig) > 0 ); - assert( Saig_ManPoNum(pAig) == 1 ); - pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); - // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs - Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add timeframes - for ( f = 0; f < nFrames; f++ ) - { - // create PI nodes for this frame - Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - if ( f == nFrames - 1 ) - break; - // save register inputs - Saig_ManForEachLi( pAig, pObj, i ) - pObj->pData = Aig_ObjChild0Copy(pObj); - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; - } - // create the only PO of the manager - pObj = Aig_ManPo( pAig, 0 ); - Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); - Aig_ManCleanup( pFrames ); - return pFrames; -} - -/**Function************************************************************* - - Synopsis [Returns the SAT solver for one interpolation run.] - - Description [pInter is the previous interpolant. pAig is one time frame. - pFrames is the unrolled time frames.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -sat_solver * Saig_DeriveSatSolver( - Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, - Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, - Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, - Vec_Int_t * vVarsAB ) -{ - sat_solver * pSat; - Aig_Obj_t * pObj, * pObj2; - int i, Lits[2]; - - // sanity checks - assert( Aig_ManRegNum(pInter) == 0 ); - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pFrames) == 0 ); - assert( Aig_ManPoNum(pInter) == 1 ); - assert( Aig_ManPoNum(pFrames) == 1 ); - assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); -// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); - - // prepare CNFs - Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); - Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); - - // start the solver - pSat = sat_solver_new(); - sat_solver_store_alloc( pSat ); - sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars ); - - // add clauses of A - // interpolant - for ( i = 0; i < pCnfInter->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) ) - assert( 0 ); - } - // connector clauses - Aig_ManForEachPi( pInter, pObj, i ) - { - pObj2 = Saig_ManLo( pAig, i ); - Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - // one timeframe - for ( i = 0; i < pCnfAig->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) ) - assert( 0 ); - } - // connector clauses - Vec_IntClear( vVarsAB ); - Aig_ManForEachPi( pFrames, pObj, i ) - { - if ( i == Aig_ManRegNum(pAig) ) - break; - Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); - - pObj2 = Saig_ManLi( pAig, i ); - Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - // add clauses of B - sat_solver_store_mark_clauses_a( pSat ); - for ( i = 0; i < pCnfFrames->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) - { - pSat->fSolved = 1; - break; - } - } - sat_solver_store_mark_roots( pSat ); - // return clauses to the original state - Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); - Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); - return pSat; -} - -/**Function************************************************************* - - Synopsis [Checks constainment of two interpolants.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld ) -{ - Aig_Man_t * pMiter, * pAigTemp; - int RetValue; - pMiter = Aig_ManCreateMiter( pNew, pOld, 1 ); -// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); -// Aig_ManStop( pAigTemp ); - RetValue = Fra_FraigMiterStatus( pMiter ); - if ( RetValue == -1 ) - { - pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); - RetValue = Fra_FraigMiterStatus( pAigTemp ); - Aig_ManStop( pAigTemp ); -// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); - } - assert( RetValue != -1 ); - Aig_ManStop( pMiter ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Checks constainment of two interpolants.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld ) -{ - Aig_Man_t * pMiter, * pAigTemp; - int RetValue; - pMiter = Aig_ManCreateMiter( pNew, pOld, 0 ); -// pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 ); -// Aig_ManStop( pAigTemp ); - RetValue = Fra_FraigMiterStatus( pMiter ); - if ( RetValue == -1 ) - { - pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 ); - RetValue = Fra_FraigMiterStatus( pAigTemp ); - Aig_ManStop( pAigTemp ); -// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 ); - } - assert( RetValue != -1 ); - Aig_ManStop( pMiter ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Performs one SAT run with interpolation.] - - Description [Returns 1 if proven. 0 if failed. -1 if undecided.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_PerformOneStep_old( Saig_IntMan_t * p, int fUseIp ) -{ - sat_solver * pSat; - void * pSatCnf = NULL; - Inta_Man_t * pManInterA; - Intb_Man_t * pManInterB; - int clk, status, RetValue; - assert( p->pInterNew == NULL ); - - // derive the SAT solver - pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB ); -//Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 ); - // solve the problem -clk = clock(); - status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); - p->nConfCur = pSat->stats.conflicts; -p->timeSat += clock() - clk; - if ( status == l_False ) - { - pSatCnf = sat_solver_store_release( pSat ); - RetValue = 1; - } - else if ( status == l_True ) - { - RetValue = 0; - } - else - { - RetValue = -1; - } - sat_solver_delete( pSat ); - if ( pSatCnf == NULL ) - return RetValue; - - // create the resulting manager -clk = clock(); - if ( !fUseIp ) - { - pManInterA = Inta_ManAlloc(); - p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); - Inta_ManFree( pManInterA ); - } - else - { - pManInterB = Intb_ManAlloc(); - p->pInterNew = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 ); - Intb_ManFree( pManInterB ); - } -p->timeInt += clock() - clk; - Sto_ManFree( pSatCnf ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Aig_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther ) -{ - Aig_Man_t * pInterC; - assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) ); - pInterC = Aig_ManDupSimple( pInter ); - Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 ); - assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) ); - return pInterC; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_VerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) -{ - extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); - Aig_Man_t * pLower, * pUpper, * pInterC; - int RetValue1, RetValue2; - - pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 ); - pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 ); - Aig_ManFlipFirstPo( pUpper ); - - pInterC = Aig_ManDupExpand( pInter, pLower ); - RetValue1 = Saig_ManCheckContainment( pLower, pInterC ); - Aig_ManStop( pInterC ); - - pInterC = Aig_ManDupExpand( pInter, pUpper ); - RetValue2 = Saig_ManCheckContainment( pInterC, pUpper ); - Aig_ManStop( pInterC ); - - if ( RetValue1 && RetValue2 ) - printf( "Im is correct.\n" ); - if ( !RetValue1 ) - printf( "Property A => Im fails.\n" ); - if ( !RetValue2 ) - printf( "Property Im => !B fails.\n" ); - - Aig_ManStop( pLower ); - Aig_ManStop( pUpper ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_VerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter ) -{ - extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA ); - Aig_Man_t * pLower, * pUpper, * pInterC; - int RetValue1, RetValue2; - - pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 ); - pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 ); - Aig_ManFlipFirstPo( pUpper ); - - pInterC = Aig_ManDupExpand( pInter, pLower ); -//Aig_ManPrintStats( pLower ); -//Aig_ManPrintStats( pUpper ); -//Aig_ManPrintStats( pInterC ); -//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL ); - RetValue1 = Saig_ManCheckContainment( pLower, pInterC ); - Aig_ManStop( pInterC ); - - pInterC = Aig_ManDupExpand( pInter, pUpper ); - RetValue2 = Saig_ManCheckContainment( pInterC, pUpper ); - Aig_ManStop( pInterC ); - - if ( RetValue1 && RetValue2 ) - printf( "Ip is correct.\n" ); - if ( !RetValue1 ) - printf( "Property A => Ip fails.\n" ); - if ( !RetValue2 ) - printf( "Property Ip => !B fails.\n" ); - - Aig_ManStop( pLower ); - Aig_ManStop( pUpper ); -} - -/**Function************************************************************* - - Synopsis [Performs one SAT run with interpolation.] - - Description [Returns 1 if proven. 0 if failed. -1 if undecided.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_PerformOneStep( Saig_IntMan_t * p, int fUseIp ) -{ - sat_solver * pSat; - void * pSatCnf = NULL; - Inta_Man_t * pManInterA; - Intb_Man_t * pManInterB; - int clk, status, RetValue; - assert( p->pInterNew == NULL ); - - // derive the SAT solver - pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB ); -//Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 ); - // solve the problem -clk = clock(); - status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); - p->nConfCur = pSat->stats.conflicts; -p->timeSat += clock() - clk; - if ( status == l_False ) - { - pSatCnf = sat_solver_store_release( pSat ); - RetValue = 1; - } - else if ( status == l_True ) - { - RetValue = 0; - } - else - { - RetValue = -1; - } - sat_solver_delete( pSat ); - if ( pSatCnf == NULL ) - return RetValue; - - // create the resulting manager -clk = clock(); - if ( !fUseIp ) - { - pManInterA = Inta_ManAlloc(); - p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); - Inta_ManFree( pManInterA ); - } - else - { - Aig_Man_t * pInterNew2; - int RetValue; - - pManInterA = Inta_ManAlloc(); - p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 ); -// Saig_VerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew ); - Inta_ManFree( pManInterA ); - - pManInterB = Intb_ManAlloc(); - pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 ); - Saig_VerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 ); - Intb_ManFree( pManInterB ); - - // check relationship - RetValue = Saig_ManCheckEquivalence( pInterNew2, p->pInterNew ); - if ( RetValue ) - printf( "Equivalence \"Ip == Im\" holds\n" ); - else - { -// printf( "Equivalence \"Ip == Im\" does not hold\n" ); - RetValue = Saig_ManCheckContainment( pInterNew2, p->pInterNew ); - if ( RetValue ) - printf( "Containment \"Ip -> Im\" holds\n" ); - else - printf( "Containment \"Ip -> Im\" does not hold\n" ); - - RetValue = Saig_ManCheckContainment( p->pInterNew, pInterNew2 ); - if ( RetValue ) - printf( "Containment \"Im -> Ip\" holds\n" ); - else - printf( "Containment \"Im -> Ip\" does not hold\n" ); - } - - Aig_ManStop( pInterNew2 ); - } -p->timeInt += clock() - clk; - Sto_ManFree( pSatCnf ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Frees the interpolation manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManagerClean( Saig_IntMan_t * p ) -{ - if ( p->pCnfInter ) - Cnf_DataFree( p->pCnfInter ); - if ( p->pCnfFrames ) - Cnf_DataFree( p->pCnfFrames ); - if ( p->pInter ) - Aig_ManStop( p->pInter ); - if ( p->pFrames ) - Aig_ManStop( p->pFrames ); -} - -/**Function************************************************************* - - Synopsis [Frees the interpolation manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManagerFreeInters( Saig_IntMan_t * p ) -{ - Aig_Man_t * pTemp; - int i; - Vec_PtrForEachEntry( p->vInters, pTemp, i ) - Aig_ManStop( pTemp ); - Vec_PtrClear( p->vInters ); -} - -/**Function************************************************************* - - Synopsis [Frees the interpolation manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManagerFree( Saig_IntMan_t * p ) -{ - if ( p->fVerbose ) - { - p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu; - printf( "Runtime statistics:\n" ); - PRTP( "Rewriting ", p->timeRwr, p->timeTotal ); - PRTP( "CNF mapping", p->timeCnf, p->timeTotal ); - PRTP( "SAT solving", p->timeSat, p->timeTotal ); - PRTP( "Interpol ", p->timeInt, p->timeTotal ); - PRTP( "Containment", p->timeEqu, p->timeTotal ); - PRTP( "Other ", p->timeOther, p->timeTotal ); - PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); - } - - if ( p->pCnfAig ) - Cnf_DataFree( p->pCnfAig ); - if ( p->pCnfFrames ) - Cnf_DataFree( p->pCnfFrames ); - if ( p->pCnfInter ) - Cnf_DataFree( p->pCnfInter ); - Vec_IntFree( p->vVarsAB ); - if ( p->pAigTrans ) - Aig_ManStop( p->pAigTrans ); - if ( p->pFrames ) - Aig_ManStop( p->pFrames ); - if ( p->pInter ) - Aig_ManStop( p->pInter ); - if ( p->pInterNew ) - Aig_ManStop( p->pInterNew ); - Saig_ManagerFreeInters( p ); - Vec_PtrFree( p->vInters ); - free( p ); -} - - -/**Function************************************************************* - - Synopsis [Check inductive containment.] - - Description [Given interpolant I and transition relation T, here we - check that I(x) * T(x,y) => T(y). ] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p, int fSubtractOld ) -{ - sat_solver * pSat; - Aig_Man_t * pInterOld = p->pInter; - Aig_Man_t * pInterNew = p->pInterNew; - Aig_Man_t * pTrans = p->pAigTrans; - Cnf_Dat_t * pCnfOld = p->pCnfInter; - Cnf_Dat_t * pCnfNew = Cnf_Derive( p->pInterNew, 0 ); - Cnf_Dat_t * pCnfTrans = p->pCnfAig; - Aig_Obj_t * pObj, * pObj2; - int status, i, Lits[2]; - - // start the solver - pSat = sat_solver_new(); - if ( fSubtractOld ) - sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars + pCnfOld->nVars ); - else - sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars ); - - // interpolant - for ( i = 0; i < pCnfNew->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) ) - assert( 0 ); - } - - // connector clauses - Cnf_DataLift( pCnfTrans, pCnfNew->nVars ); - Aig_ManForEachPi( pInterNew, pObj, i ) - { - pObj2 = Saig_ManLo( pTrans, i ); - Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 ); - Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 ); - Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - // one timeframe - for ( i = 0; i < pCnfTrans->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnfTrans->pClauses[i], pCnfTrans->pClauses[i+1] ) ) - assert( 0 ); - } - - // connector clauses - Cnf_DataLift( pCnfNew, pCnfNew->nVars + pCnfTrans->nVars ); - Aig_ManForEachPi( pInterNew, pObj, i ) - { - pObj2 = Saig_ManLi( pTrans, i ); - Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 ); - Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 ); - Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - - // complement the last literal - // add clauses of B - Cnf_DataFlipLastLiteral( pCnfNew ); - for ( i = 0; i < pCnfNew->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) ) - { -// assert( 0 ); - Cnf_DataFree( pCnfNew ); - return 1; - } - } - Cnf_DataFlipLastLiteral( pCnfNew ); - - // return clauses to the original state - Cnf_DataLift( pCnfTrans, -pCnfNew->nVars ); - Cnf_DataLift( pCnfNew, -pCnfNew->nVars -pCnfTrans->nVars ); - if ( fSubtractOld ) - { - Cnf_DataLift( pCnfOld, 2 * pCnfNew->nVars + pCnfTrans->nVars ); - // old interpolant clauses - Cnf_DataFlipLastLiteral( pCnfOld ); - for ( i = 0; i < pCnfOld->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnfOld->pClauses[i], pCnfOld->pClauses[i+1] ) ) - assert( 0 ); - } - Cnf_DataFlipLastLiteral( pCnfOld ); - // connector clauses - Aig_ManForEachPi( pInterOld, pObj, i ) - { - pObj2 = Aig_ManPi( pInterNew, i ); - Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 0 ); - Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 1 ); - Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - Cnf_DataLift( pCnfOld, - 2 * pCnfNew->nVars - pCnfTrans->nVars ); - } - Cnf_DataFree( pCnfNew ); - - // solve the problem - status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); - sat_solver_delete( pSat ); - return status == l_False; -} - - -/**Function************************************************************* - - Synopsis [Interplates 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 Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ) -{ - extern int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters ); - Saig_IntMan_t * p; - Aig_Man_t * pAigTemp; - int s, i, RetValue, Status, clk, clk2, clkTotal = clock(); - - // sanity checks - assert( Saig_ManRegNum(pAig) > 0 ); - assert( Saig_ManPiNum(pAig) > 0 ); - assert( Saig_ManPoNum(pAig) == 1 ); - - // create interpolation manager - p = ALLOC( Saig_IntMan_t, 1 ); - memset( p, 0, sizeof(Saig_IntMan_t) ); - p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) ); - p->nFrames = 1; - p->nConfLimit = nConfLimit; - p->fVerbose = fVerbose; - p->vInters = Vec_PtrAlloc( 10 ); - // can perform SAT sweeping and/or rewriting of this AIG... - p->pAig = pAig; - if ( fTransLoop ) - p->pAigTrans = Saig_ManTransformed( pAig ); - else - p->pAigTrans = Saig_ManDuplicated( pAig ); - // derive CNF for the transformed AIG -clk = clock(); - p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); -p->timeCnf += clock() - clk; - if ( fVerbose ) - { - printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d. CNF: Var/Cla = %d/%d.\n", - Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), - Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig), - p->pCnfAig->nVars, p->pCnfAig->nClauses ); - } - - // derive interpolant - *pDepth = -1; - for ( s = 0; ; s++ ) - { - Saig_ManagerFreeInters( p ); -clk2 = clock(); - // initial state - p->pInter = Saig_ManInit( Aig_ManRegNum(pAig) ); - Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) ); -clk = clock(); - p->pCnfInter = Cnf_Derive( p->pInter, 0 ); -p->timeCnf += clock() - clk; - // timeframes - p->pFrames = Saig_ManFramesInter( pAig, p->nFrames ); -clk = clock(); - if ( fRewrite ) - { - p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 ); - Aig_ManStop( pAigTemp ); -// p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 ); -// Aig_ManStop( pAigTemp ); - } -p->timeRwr += clock() - clk; - // can also do SAT sweeping on the timeframes... -clk = clock(); - p->pCnfFrames = Cnf_Derive( p->pFrames, 0 ); -p->timeCnf += clock() - clk; - // report statistics - if ( fVerbose ) - { - printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d. ", - s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) ); - PRT( "Time", clock() - clk2 ); - } - // iterate the interpolation procedure - for ( i = 0; ; i++ ) - { - if ( p->nFrames + i >= nFramesMax ) - { - if ( fVerbose ) - printf( "Reached limit (%d) on the number of timeframes.\n", nFramesMax ); - p->timeTotal = clock() - clkTotal; - Saig_ManagerFree( p ); - return -1; - } - // perform interplation - clk = clock(); -#ifdef ABC_USE_LIBRARIES - if ( fUseMiniSat ) - RetValue = Saig_M144pPerformOneStep( p, fUsePudlak, fUseOther ); - else -#endif - RetValue = Saig_PerformOneStep( p, 0 ); - - if ( fVerbose ) - { - printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ", - i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur ); - PRT( "Time", clock() - clk ); - } - if ( RetValue == 0 ) // found a (spurious?) counter-example - { - if ( i == 0 ) // real counterexample - { - if ( fVerbose ) - printf( "Found a real counterexample in the first frame.\n" ); - p->timeTotal = clock() - clkTotal; - *pDepth = p->nFrames + 1; - Saig_ManagerFree( p ); - return 0; - } - // likely spurious counter-example - p->nFrames += i; - Saig_ManagerClean( p ); - break; - } - else if ( RetValue == -1 ) // timed out - { - if ( fVerbose ) - printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit ); - assert( p->nConfCur >= p->nConfLimit ); - p->timeTotal = clock() - clkTotal; - Saig_ManagerFree( p ); - return -1; - } - assert( RetValue == 1 ); // found new interpolant - // compress the interpolant -clk = clock(); - p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 ); - Aig_ManStop( pAigTemp ); -p->timeRwr += clock() - clk; - // save the new interpolant - Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) ); - // check containment of interpolants -clk = clock(); - if ( fCheckKstep ) // k-step unique-state induction - Status = Saig_ManUniqueState( p->pAigTrans, p->vInters ); - else if ( fCheckInd ) // simple induction - Status = Saig_ManCheckInductiveContainment( p, 1 ); - else // combinational containment - Status = Saig_ManCheckContainment( p->pInterNew, p->pInter ); -p->timeEqu += clock() - clk; - if ( Status ) // contained - { - if ( fVerbose ) - printf( "Proved containment of interpolants.\n" ); - p->timeTotal = clock() - clkTotal; - Saig_ManagerFree( p ); - return 1; - } - // save interpolant and convert it into CNF - if ( fTransLoop ) - { - Aig_ManStop( p->pInter ); - p->pInter = p->pInterNew; - } - else - { - p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 ); - Aig_ManStop( pAigTemp ); - Aig_ManStop( p->pInterNew ); - // compress the interpolant -clk = clock(); - p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 ); - Aig_ManStop( pAigTemp ); -p->timeRwr += clock() - clk; - } - p->pInterNew = NULL; - Cnf_DataFree( p->pCnfInter ); -clk = clock(); - p->pCnfInter = Cnf_Derive( p->pInter, 0 ); -p->timeCnf += clock() - clk; - } - } - assert( 0 ); - return RetValue; -} - - -#ifdef ABC_USE_LIBRARIES - -#include "m114p.h" - -/**Function************************************************************* - - Synopsis [Returns the SAT solver for one interpolation run.] - - Description [pInter is the previous interpolant. pAig is one time frame. - pFrames is the unrolled time frames.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -M114p_Solver_t Saig_M144pDeriveSatSolver( - Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, - Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, - Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, - Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars ) -{ - M114p_Solver_t pSat; - Aig_Obj_t * pObj, * pObj2; - int i, Lits[2]; - - // sanity checks - assert( Aig_ManRegNum(pInter) == 0 ); - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pFrames) == 0 ); - assert( Aig_ManPoNum(pInter) == 1 ); - assert( Aig_ManPoNum(pFrames) == 1 ); - assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); -// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); - - // prepare CNFs - Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); - Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars ); - - *pvMapRoots = Vec_IntAlloc( 10000 ); - *pvMapVars = Vec_IntAlloc( 0 ); - Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 ); - for ( i = 0; i < pCnfFrames->nVars; i++ ) - Vec_IntWriteEntry( *pvMapVars, i, -2 ); - - // start the solver - pSat = M114p_SolverNew( 1 ); - M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars ); - - // add clauses of A - // interpolant - for ( i = 0; i < pCnfInter->nClauses; i++ ) - { - Vec_IntPush( *pvMapRoots, 0 ); - if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) ) - assert( 0 ); - } - // connector clauses - Aig_ManForEachPi( pInter, pObj, i ) - { - pObj2 = Saig_ManLo( pAig, i ); - Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); - Vec_IntPush( *pvMapRoots, 0 ); - if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); - Vec_IntPush( *pvMapRoots, 0 ); - if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - // one timeframe - for ( i = 0; i < pCnfAig->nClauses; i++ ) - { - Vec_IntPush( *pvMapRoots, 0 ); - if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) ) - assert( 0 ); - } - // connector clauses - Aig_ManForEachPi( pFrames, pObj, i ) - { - if ( i == Aig_ManRegNum(pAig) ) - break; -// Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); - Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i ); - - pObj2 = Saig_ManLi( pAig, i ); - Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 ); - Vec_IntPush( *pvMapRoots, 0 ); - if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 ); - Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 ); - Vec_IntPush( *pvMapRoots, 0 ); - if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - // add clauses of B - for ( i = 0; i < pCnfFrames->nClauses; i++ ) - { - Vec_IntPush( *pvMapRoots, 1 ); - if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) - { -// assert( 0 ); - break; - } - } - // return clauses to the original state - Cnf_DataLift( pCnfAig, -pCnfFrames->nVars ); - Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars ); - return pSat; -} - -/**Function************************************************************* - - Synopsis [Computes interpolant using MiniSat-1.14p.] - - Description [Assumes that the solver returned UNSAT and proof - logging was enabled. Array vMapRoots maps number of each root clause - into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT - solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), - where <num> is the var's 0-based number in the ordering of C variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_M144pInterpolateReport( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) -{ - Vec_Int_t * vASteps; - int * pLits, * pClauses, * pVars; - int nLits, nVars, i, k, iVar, haveASteps; - int CountA, CountB, CountC, CountCsaved; - - assert( M114p_SolverProofIsReady(s) ); - vASteps = Vec_IntAlloc( 1000 ); - // process root clauses - M114p_SolverForEachRoot( s, &pLits, nLits, i ) - { - if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B - { - } - else // clause of A - { - } - Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) ); - } -// assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) ); - - // process learned clauses - CountA = CountB = CountC = CountCsaved = 0; - M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) - { - haveASteps = Vec_IntEntry( vASteps, pClauses[0] ); - for ( k = 0; k < nVars; k++ ) - { - iVar = Vec_IntEntry( vMapVars, pVars[k] ); - haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] ); - if ( iVar == -1 ) // var of A - { - haveASteps = 1; - } - else // var of B or C - { - } - - if ( iVar == -1 ) - CountA++; - else if ( iVar == -2 ) - CountB++; - else - { - if ( haveASteps == 0 ) - CountCsaved++; - CountC++; - } - } - Vec_IntPush( vASteps, haveASteps ); - } - assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) ); - - printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", - CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC ); - Vec_IntFree( vASteps ); -} - -/**Function************************************************************* - - Synopsis [Computes interpolant using MiniSat-1.14p.] - - Description [Assumes that the solver returned UNSAT and proof - logging was enabled. Array vMapRoots maps number of each root clause - into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT - solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), - where <num> is the var's 0-based number in the ordering of C variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_M144pInterpolateLastStep( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) -{ - int * pLits, * pClauses, * pVars; - int nLits, nVars, i, k, iVar; - int nSteps, iStepA, iStepB; - assert( M114p_SolverProofIsReady(s) ); - // process root clauses - M114p_SolverForEachRoot( s, &pLits, nLits, i ) - { - if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B - { - } - else // clause of A - { - } - } -// assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) ); - // process learned clauses - nSteps = 0; - M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) - { - for ( k = 0; k < nVars; k++ ) - { - iVar = Vec_IntEntry( vMapVars, pVars[k] ); - if ( iVar == -1 ) // var of A - { - iStepA = nSteps; - } - else if ( iVar == -2 ) // var of B - { - iStepB = nSteps; - } - else // var of C - { - } - nSteps++; - } - } -// assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) ); - if ( iStepA < iStepB ) - return iStepB; - return iStepA; -} - -/**Function************************************************************* - - Synopsis [Computes interpolant using MiniSat-1.14p.] - - Description [Assumes that the solver returned UNSAT and proof - logging was enabled. Array vMapRoots maps number of each root clause - into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT - solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), - where <num> is the var's 0-based number in the ordering of C variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) -{ - Aig_Man_t * p; - Aig_Obj_t * pInter, * pInter2, * pVar; - Vec_Ptr_t * vInters; - int * pLits, * pClauses, * pVars; - int nLits, nVars, i, k, iVar; - assert( M114p_SolverProofIsReady(s) ); - vInters = Vec_PtrAlloc( 1000 ); - // process root clauses - p = Aig_ManStart( 10000 ); - M114p_SolverForEachRoot( s, &pLits, nLits, i ) - { - if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B - pInter = Aig_ManConst1(p); - else // clause of A - { - pInter = Aig_ManConst0(p); - for ( k = 0; k < nLits; k++ ) - { - iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) ); - if ( iVar < 0 ) // var of A or B - continue; - pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) ); - pInter = Aig_Or( p, pInter, pVar ); - } - } - Vec_PtrPush( vInters, pInter ); - } -// assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); - - // process learned clauses - M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) - { - pInter = Vec_PtrEntry( vInters, pClauses[0] ); - for ( k = 0; k < nVars; k++ ) - { - iVar = Vec_IntEntry( vMapVars, pVars[k] ); - pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); - if ( iVar == -1 ) // var of A - pInter = Aig_Or( p, pInter, pInter2 ); - else // var of B or C - pInter = Aig_And( p, pInter, pInter2 ); - } - Vec_PtrPush( vInters, pInter ); - } - assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); - Vec_PtrFree( vInters ); - Aig_ObjCreatePo( p, pInter ); - Aig_ManCleanup( p ); - return p; -} - -/**Function************************************************************* - - Synopsis [Performs one resolution step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_M144pResolve( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar ) -{ - int i, k, iLit = -1, fFound = 0; - // find the variable in the clause - for ( i = 0; i < vResolvent->nSize; i++ ) - if ( lit_var(vResolvent->pArray[i]) == iVar ) - { - iLit = vResolvent->pArray[i]; - vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize]; - break; - } - assert( iLit != -1 ); - // add other variables - for ( i = 0; i < nLits; i++ ) - { - if ( lit_var(pLits[i]) == iVar ) - { - assert( iLit == lit_neg(pLits[i]) ); - fFound = 1; - continue; - } - // check if this literal appears - for ( k = 0; k < vResolvent->nSize; k++ ) - if ( vResolvent->pArray[k] == pLits[i] ) - break; - if ( k < vResolvent->nSize ) - continue; - // add this literal - Vec_IntPush( vResolvent, pLits[i] ); - } - assert( fFound ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Computes interpolant using MiniSat-1.14p.] - - Description [Assumes that the solver returned UNSAT and proof - logging was enabled. Array vMapRoots maps number of each root clause - into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT - solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), - where <num> is the var's 0-based number in the ordering of C variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_M144pInterpolatePudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) -{ - Aig_Man_t * p; - Aig_Obj_t * pInter, * pInter2, * pVar; - Vec_Ptr_t * vInters; - Vec_Int_t * vLiterals, * vClauses, * vResolvent; - int * pLitsNext, nLitsNext, nOffset, iLit; - int * pLits, * pClauses, * pVars; - int nLits, nVars, i, k, v, iVar; - assert( M114p_SolverProofIsReady(s) ); - vInters = Vec_PtrAlloc( 1000 ); - - vLiterals = Vec_IntAlloc( 10000 ); - vClauses = Vec_IntAlloc( 1000 ); - vResolvent = Vec_IntAlloc( 100 ); - - // create elementary variables - p = Aig_ManStart( 10000 ); - Vec_IntForEachEntry( vMapVars, iVar, i ) - if ( iVar >= 0 ) - Aig_IthVar(p, iVar); - // process root clauses - M114p_SolverForEachRoot( s, &pLits, nLits, i ) - { - if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B - pInter = Aig_ManConst1(p); - else // clause of A - pInter = Aig_ManConst0(p); - Vec_PtrPush( vInters, pInter ); - - // save the root clause - Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); - Vec_IntPush( vLiterals, nLits ); - for ( v = 0; v < nLits; v++ ) - Vec_IntPush( vLiterals, pLits[v] ); - } - assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); - - // process learned clauses - M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) - { - pInter = Vec_PtrEntry( vInters, pClauses[0] ); - - // initialize the resolvent - nOffset = Vec_IntEntry( vClauses, pClauses[0] ); - nLitsNext = Vec_IntEntry( vLiterals, nOffset ); - pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; - Vec_IntClear( vResolvent ); - for ( v = 0; v < nLitsNext; v++ ) - Vec_IntPush( vResolvent, pLitsNext[v] ); - - for ( k = 0; k < nVars; k++ ) - { - iVar = Vec_IntEntry( vMapVars, pVars[k] ); - pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); - - // resolve it with the next clause - nOffset = Vec_IntEntry( vClauses, pClauses[k+1] ); - nLitsNext = Vec_IntEntry( vLiterals, nOffset ); - pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; - Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] ); - - if ( iVar == -1 ) // var of A - pInter = Aig_Or( p, pInter, pInter2 ); - else if ( iVar == -2 ) // var of B - pInter = Aig_And( p, pInter, pInter2 ); - else // var of C - { - // check polarity of the pivot variable in the clause - for ( v = 0; v < nLitsNext; v++ ) - if ( lit_var(pLitsNext[v]) == pVars[k] ) - break; - assert( v < nLitsNext ); - pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) ); - pInter = Aig_Mux( p, pVar, pInter, pInter2 ); - } - } - Vec_PtrPush( vInters, pInter ); - - // store the resulting clause - Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); - Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) ); - Vec_IntForEachEntry( vResolvent, iLit, v ) - Vec_IntPush( vLiterals, iLit ); - } - assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); - assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause - Vec_PtrFree( vInters ); - Vec_IntFree( vLiterals ); - Vec_IntFree( vClauses ); - Vec_IntFree( vResolvent ); - Aig_ObjCreatePo( p, pInter ); - Aig_ManCleanup( p ); - return p; -} - -/**Function************************************************************* - - Synopsis [Computes interpolant using MiniSat-1.14p.] - - Description [Assumes that the solver returned UNSAT and proof - logging was enabled. Array vMapRoots maps number of each root clause - into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT - solver variable into -1 (var of A), -2 (var of B), and <num> (var of C), - where <num> is the var's 0-based number in the ordering of C variables.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_M144pInterpolatePudlakASteps( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars ) -{ - Aig_Man_t * p; - Aig_Obj_t * pInter, * pInter2, * pVar; - Vec_Ptr_t * vInters; - Vec_Int_t * vASteps; - Vec_Int_t * vLiterals, * vClauses, * vResolvent; - int * pLitsNext, nLitsNext, nOffset, iLit; - int * pLits, * pClauses, * pVars; - int nLits, nVars, i, k, v, iVar, haveASteps; - assert( M114p_SolverProofIsReady(s) ); - vInters = Vec_PtrAlloc( 1000 ); - vASteps = Vec_IntAlloc( 1000 ); - - vLiterals = Vec_IntAlloc( 10000 ); - vClauses = Vec_IntAlloc( 1000 ); - vResolvent = Vec_IntAlloc( 100 ); - - // create elementary variables - p = Aig_ManStart( 10000 ); - Vec_IntForEachEntry( vMapVars, iVar, i ) - if ( iVar >= 0 ) - Aig_IthVar(p, iVar); - // process root clauses - M114p_SolverForEachRoot( s, &pLits, nLits, i ) - { - if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B - pInter = Aig_ManConst1(p); - else // clause of A - pInter = Aig_ManConst0(p); - Vec_PtrPush( vInters, pInter ); - Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) ); - - // save the root clause - Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); - Vec_IntPush( vLiterals, nLits ); - for ( v = 0; v < nLits; v++ ) - Vec_IntPush( vLiterals, pLits[v] ); - } - assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); - - // process learned clauses - M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) - { - pInter = Vec_PtrEntry( vInters, pClauses[0] ); - haveASteps = Vec_IntEntry( vASteps, pClauses[0] ); - - // initialize the resolvent - nOffset = Vec_IntEntry( vClauses, pClauses[0] ); - nLitsNext = Vec_IntEntry( vLiterals, nOffset ); - pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; - Vec_IntClear( vResolvent ); - for ( v = 0; v < nLitsNext; v++ ) - Vec_IntPush( vResolvent, pLitsNext[v] ); - - for ( k = 0; k < nVars; k++ ) - { - iVar = Vec_IntEntry( vMapVars, pVars[k] ); - pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] ); - haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] ); - - // resolve it with the next clause - nOffset = Vec_IntEntry( vClauses, pClauses[k+1] ); - nLitsNext = Vec_IntEntry( vLiterals, nOffset ); - pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1; - Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] ); - - if ( iVar == -1 ) // var of A - pInter = Aig_Or( p, pInter, pInter2 ), haveASteps = 1; - else if ( iVar == -2 ) // var of B - pInter = Aig_And( p, pInter, pInter2 ); - else // var of C - { - if ( haveASteps == 0 ) - pInter = Aig_ManConst0(p); - else - { - // check polarity of the pivot variable in the clause - for ( v = 0; v < nLitsNext; v++ ) - if ( lit_var(pLitsNext[v]) == pVars[k] ) - break; - assert( v < nLitsNext ); - pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) ); - pInter = Aig_Mux( p, pVar, pInter, pInter2 ); - } - } - } - Vec_PtrPush( vInters, pInter ); - Vec_IntPush( vASteps, haveASteps ); - - // store the resulting clause - Vec_IntPush( vClauses, Vec_IntSize(vLiterals) ); - Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) ); - Vec_IntForEachEntry( vResolvent, iLit, v ) - Vec_IntPush( vLiterals, iLit ); - } - assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); - assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause - Vec_PtrFree( vInters ); - Vec_IntFree( vASteps ); - - Vec_IntFree( vLiterals ); - Vec_IntFree( vClauses ); - Vec_IntFree( vResolvent ); - Aig_ObjCreatePo( p, pInter ); - Aig_ManCleanup( p ); - return p; -} - -/**Function************************************************************* - - Synopsis [Performs one SAT run with interpolation.] - - Description [Returns 1 if proven. 0 if failed. -1 if undecided.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther ) -{ - M114p_Solver_t pSat; - Vec_Int_t * vMapRoots, * vMapVars; - int clk, status, RetValue; - assert( p->pInterNew == NULL ); - // derive the SAT solver - pSat = Saig_M144pDeriveSatSolver( p->pInter, p->pCnfInter, - p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, - &vMapRoots, &vMapVars ); - // solve the problem -clk = clock(); - status = M114p_SolverSolve( pSat, NULL, NULL, 0 ); - p->nConfCur = M114p_SolverGetConflictNum( pSat ); -p->timeSat += clock() - clk; - if ( status == 0 ) - { - RetValue = 1; - - ///// report the savings of the modified Pudlak's approach - Saig_M144pInterpolateReport( pSat, vMapRoots, vMapVars ); - ///// - -clk = clock(); - if ( fUseOther ) - p->pInterNew = Saig_M144pInterpolatePudlakASteps( pSat, vMapRoots, vMapVars ); - else if ( fUsePudlak ) - p->pInterNew = Saig_M144pInterpolatePudlak( pSat, vMapRoots, vMapVars ); - else - p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars ); -p->timeInt += clock() - clk; - } - else if ( status == 1 ) - { - RetValue = 0; - } - else - { - RetValue = -1; - } - M114p_SolverDelete( pSat ); - Vec_IntFree( vMapRoots ); - Vec_IntFree( vMapVars ); - return RetValue; -} - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/saig/saigUnique.c b/src/aig/saig/saigUnique.c deleted file mode 100644 index 8b4d80e7..00000000 --- a/src/aig/saig/saigUnique.c +++ /dev/null @@ -1,170 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigUnique.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Containment checking with unique state constraints.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigUnique.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "cnf.h" -#include "satSolver.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Create timeframes of the manager for interpolation.] - - Description [The resulting manager is combinational. The primary inputs - corresponding to register outputs are ordered first.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg ) -{ - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, f; - assert( Saig_ManRegNum(pAig) > 0 ); - pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); - // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs - *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) ); - Saig_ManForEachLo( pAig, pObj, i ) - { - pObj->pData = Aig_ObjCreatePi( pFrames ); - Vec_PtrPush( *pvMapReg, pObj->pData ); - } - // add timeframes - for ( f = 0; f < nFrames; f++ ) - { - // create PI nodes for this frame - Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // save register inputs - Saig_ManForEachLi( pAig, pObj, i ) - pObj->pData = Aig_ObjChild0Copy(pObj); - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - { - pObjLo->pData = pObjLi->pData; - Vec_PtrPush( *pvMapReg, pObjLo->pData ); - } - } - return pFrames; -} - -/**Function************************************************************* - - Synopsis [Duplicates AIG while mapping PIs into the given array.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl ) -{ - Aig_Obj_t * pObj; - int i; - assert( Aig_ManPoNum(pOld) == 1 ); - // create the PIs - Aig_ManCleanData( pOld ); - Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( pOld, pObj, i ) - pObj->pData = ppNewPis[i]; - // duplicate internal nodes - Aig_ManForEachNode( pOld, pObj, i ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // add one PO to new - pObj = Aig_ManPo( pOld, 0 ); - Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters ) -{ - Aig_Man_t * pFrames, * pInterNext, * pInterThis; - Aig_Obj_t ** ppNodes; - Vec_Ptr_t * vMapRegs; - Cnf_Dat_t * pCnf; - sat_solver * pSat; - int f, nRegs, status; - nRegs = Saig_ManRegNum(pTrans); - assert( nRegs > 0 ); - assert( Vec_PtrSize(vInters) > 1 ); - // generate the timeframes - pFrames = Saig_ManFramesLatches( pTrans, Vec_PtrSize(vInters)-1, &vMapRegs ); - assert( Vec_PtrSize(vMapRegs) == Vec_PtrSize(vInters) * nRegs ); - // add main constraints to the timeframes - ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs); - Vec_PtrForEachEntryStop( vInters, pInterThis, f, Vec_PtrSize(vInters)-1 ) - { - assert( nRegs == Aig_ManPiNum(pInterThis) ); - pInterNext = Vec_PtrEntry( vInters, f+1 ); - Saig_ManAppendCone( pInterNext, pFrames, ppNodes + f * nRegs, 0 ); - Saig_ManAppendCone( pInterThis, pFrames, ppNodes + f * nRegs, 1 ); - } - Saig_ManAppendCone( Vec_PtrEntryLast(vInters), pFrames, ppNodes + f * nRegs, 1 ); - Aig_ManCleanup( pFrames ); - Vec_PtrFree( vMapRegs ); - - // convert to CNF - pCnf = Cnf_Derive( pFrames, 0 ); - pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - Cnf_DataFree( pCnf ); - Aig_ManStop( pFrames ); - - if ( pSat == NULL ) - return 1; - - // solve the problem - status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 ); - sat_solver_delete( pSat ); - return status == l_False; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 09ea8b16..e4b0ad69 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -748,7 +748,7 @@ extern ABC_DLL bool Abc_NodeIsBuf( Abc_Obj_t * pNode ); extern ABC_DLL bool Abc_NodeIsInv( Abc_Obj_t * pNode ); extern ABC_DLL void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcPrint.c ==========================================================*/ -extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ); +extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes ); extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 39f44c11..90cf50b0 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -933,9 +933,9 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode ) pNode0 = Abc_ObjFanin0(pNode); pNode1 = Abc_ObjFanin1(pNode); // if the children are not ANDs, this is not MUX - if ( Abc_ObjFaninNum(pNode0) != 2 || Abc_ObjFaninNum(pNode1) != 2 ) + if ( !Abc_AigNodeIsAnd(pNode0) || !Abc_AigNodeIsAnd(pNode1) ) return 0; - // otherwise the node is MUX iff it has a pair of equal grandchildren + // otherwise the node is MUX iff it has a pair of equal grandchildren with opposite polarity return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC0(pNode1))) || (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC1(pNode1))) || (Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC0(pNode1))) || @@ -944,6 +944,27 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode ) /**Function************************************************************* + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i; + int Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + Counter += Abc_NodeIsMuxType( pNode ); + return Counter; +} + +/**Function************************************************************* + Synopsis [Returns 1 if the node is the control type of the MUX.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b8a9cefe..b0cd2f7e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -34,6 +34,7 @@ #include "fra.h" #include "saig.h" #include "nwkMerge.h" +#include "int.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -65,6 +66,7 @@ static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMuxStruct ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMulti ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -327,6 +329,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "balance", Abc_CommandBalance, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "mux_struct", Abc_CommandMuxStruct, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "multi", Abc_CommandMulti, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "renode", Abc_CommandRenode, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Abc_CommandCleanup, 1 ); @@ -588,6 +591,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) int fDumpResult; int fUseLutLib; int fPrintTime; + int fPrintMuxes; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -600,8 +604,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) fDumpResult = 0; fUseLutLib = 0; fPrintTime = 0; + fPrintMuxes = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "fbdlth" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF ) { switch ( c ) { @@ -620,6 +625,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': fPrintTime ^= 1; break; + case 'm': + fPrintMuxes ^= 1; + break; case 'h': goto usage; default: @@ -632,7 +640,12 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" ); return 1; } - Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib ); + if ( !Abc_NtkIsLogic(pNtk) && fUseLutLib ) + { + fprintf( Abc_FrameReadErr(pAbc), "Cannot print LUT delay for a non-logic network.\n" ); + return 1; + } + Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes ); if ( fPrintTime ) { pAbc->TimeTotal += pAbc->TimeCommand; @@ -643,13 +656,14 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: print_stats [-fbdlth]\n" ); + fprintf( pErr, "usage: print_stats [-fbdltmh]\n" ); fprintf( pErr, "\t prints the network statistics\n" ); fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" ); fprintf( pErr, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" ); fprintf( pErr, "\t-d : toggles dumping network into file \"<input_file_name>_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" ); fprintf( pErr, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" ); fprintf( pErr, "\t-t : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" ); + fprintf( pErr, "\t-m : toggles printing MUX statistics [default = %s]\n", fPrintMuxes? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -735,7 +749,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv ) } else printf( "EXDC network statistics: \n" ); - Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0 ); + Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0 ); return 0; usage: @@ -2483,6 +2497,78 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandMuxStruct( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + int fVerbose; + + extern Abc_Ntk_t * Abc_NtkMuxRestructure( Abc_Ntk_t * pNtk, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + // get the new network + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Does not work for a logic network.\n" ); + return 1; + } + // check if balancing worked +// pNtkRes = Abc_NtkMuxRestructure( pNtk, fVerbose ); + pNtkRes = NULL; + if ( pNtkRes == NULL ) + { + fprintf( pErr, "MUX restructuring has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: mux_struct [-vh]\n" ); + fprintf( pErr, "\t performs MUX restructuring of the current network\n" ); + fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandMulti( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -15494,6 +15580,7 @@ usage: return 1; } + /**Function************************************************************* Synopsis [] @@ -15507,39 +15594,21 @@ usage: ***********************************************************************/ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) { + Inter_ManParams_t Pars, * pPars = &Pars; FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - int nBTLimit; - int nFramesMax; - int fRewrite; - int fTransLoop; - int fUsePudlak; - int fUseOther; - int fUseMiniSat; - int fCheckInd; - int fCheckKstep; - int fVerbose; - extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose ); + extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nBTLimit = 20000; - nFramesMax = 40; - fRewrite = 0; - fTransLoop = 1; - fUsePudlak = 0; - fUseOther = 0; - fUseMiniSat= 0; - fCheckInd = 0; - fCheckKstep= 0; - fVerbose = 0; + Inter_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF ) { switch ( c ) { @@ -15549,9 +15618,20 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nBTLimit = atoi(argv[globalUtilOptind]); + pPars->nBTLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nBTLimit < 0 ) + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesMax < 0 ) goto usage; break; case 'F': @@ -15560,34 +15640,37 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFramesMax = atoi(argv[globalUtilOptind]); + pPars->nFramesK = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesMax < 0 ) + if ( pPars->nFramesK < 0 ) goto usage; break; case 'r': - fRewrite ^= 1; + pPars->fRewrite ^= 1; break; case 't': - fTransLoop ^= 1; + pPars->fTransLoop ^= 1; break; case 'p': - fUsePudlak ^= 1; + pPars->fUsePudlak ^= 1; break; case 'o': - fUseOther ^= 1; + pPars->fUseOther ^= 1; break; case 'm': - fUseMiniSat ^= 1; + pPars->fUseMiniSat ^= 1; break; - case 'i': - fCheckInd ^= 1; + case 'c': + pPars->fCheckKstep ^= 1; break; - case 'k': - fCheckKstep ^= 1; + case 'g': + pPars->fUseBias ^= 1; + break; + case 'b': + pPars->fUseBackward ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -15615,22 +15698,24 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" ); return 0; } - Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose ); + Abc_NtkDarBmcInter( pNtk, pPars ); return 0; usage: - fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" ); + fprintf( pErr, "usage: int [-CNF num] [-rtpomcgbvh]\n" ); fprintf( pErr, "\t uses interpolation to prove the property\n" ); - fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit ); - fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax ); - fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); - fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" ); - fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); - fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" ); - fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" ); - fprintf( pErr, "\t-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" ); - fprintf( pErr, "\t-k : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" ); - fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", pPars->nBTLimit ); + fprintf( pErr, "\t-N num : the limit on number of frames to unroll [default = %d]\n", pPars->nFramesMax ); + fprintf( pErr, "\t-F num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK ); + fprintf( pErr, "\t-r : toggle the use of rewriting unrolled timeframes [default = %s]\n", pPars->fRewrite? "yes": "no" ); + fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", pPars->fTransLoop? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", pPars->fUsePudlak? "yes": "no" ); + fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", pPars->fUseOther? "yes": "no" ); + fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", pPars->fUseMiniSat? "yes": "no" ); + fprintf( pErr, "\t-c : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" ); + fprintf( pErr, "\t-g : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" ); + fprintf( pErr, "\t-b : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 03790c4b..71f84272 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -25,6 +25,7 @@ #include "cnf.h" #include "fra.h" #include "fraig.h" +#include "int.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1295,7 +1296,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars ) { Aig_Man_t * pMan; int RetValue, Depth, clk = clock(); @@ -1307,7 +1308,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR return -1; } assert( pMan->nRegs > 0 ); - RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose, &Depth ); + RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index b753700e..2e01a141 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -111,7 +111,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ) +void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes ) { int Num; @@ -153,6 +153,12 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave // fprintf( pFile, " (mux = %d)", Num2-Num ); // if ( Num2 ) // fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 ); + if ( fPrintMuxes ) + { + extern int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk ); + fprintf( pFile, " (mux = %d)", Abc_NtkCountMuxes(pNtk)-Num ); + fprintf( pFile, " (pure and = %d)", Abc_NtkNodeNum(pNtk) - (Abc_NtkCountMuxes(pNtk) * 3) ); + } } else { diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 54beb8b6..64be1425 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -275,6 +275,12 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho fprintf( pFile, " Level%d;\n", Level ); Vec_PtrForEachEntry( vNodes, pNode, i ) { + if ( (int)pNode->Level != Level ) + continue; + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; + +/* int SuppSize; Vec_Ptr_t * vSupp; if ( (int)pNode->Level != Level ) @@ -284,6 +290,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 ); SuppSize = Vec_PtrSize( vSupp ); Vec_PtrFree( vSupp ); +*/ // fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); if ( Abc_NtkIsStrash(pNtk) ) @@ -294,10 +301,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData)); else pSopString = Abc_NtkPrintSop(pNode->pData); -// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); - fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, - SuppSize, - pSopString ); + fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); +// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, +// SuppSize, +// pSopString ); fprintf( pFile, ", shape = ellipse" ); if ( pNode->fMarkB ) diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c index 76c1e520..6e69bc69 100644 --- a/src/map/mapper/mapperTree.c +++ b/src/map/mapper/mapperTree.c @@ -34,7 +34,7 @@ static int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate ); static unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate ); // fanout limits -static const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ }; +extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -124,7 +124,14 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam // get the genlib file name (base) pLibName = strtok( pTemp, " \t\r\n" ); - +#ifdef __linux__ + if( strchr( pLibName, '/' ) != NULL ) + pLibName = strrchr( pLibName, '/' ) + 1; +#else + if( strchr( pLibName, '\\' ) != NULL ) + pLibName = strrchr( pLibName, '\\' ) + 1; +#endif + if ( strcmp( pLibName, "GATE" ) == 0 ) { printf( "The input file \"%s\" looks like a GENLIB file and not a supergate library file.\n", pLib->pName ); @@ -145,7 +152,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam if ( pStr == pLibFile ) strcpy( pLibFile, pLibName ); else - sprintf( pStr, "/%s", pLibName ); + sprintf( pStr, "\\%s", pLibName ); } #endif diff --git a/src/map/mapper/mapperTree_old.c b/src/map/mapper/mapperTree_old.c new file mode 100644 index 00000000..041ba2a0 --- /dev/null +++ b/src/map/mapper/mapperTree_old.c @@ -0,0 +1,823 @@ +/**CFile**************************************************************** + + FileName [mapperTree.c] + + PackageName [MVSIS 1.3: Multi-valued logic synthesis system.] + + Synopsis [Generic technology mapping engine.] + + Author [MVSIS Group] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - June 1, 2004.] + + Revision [$Id: mapperTree.c,v 1.9 2005/01/23 06:59:45 alanmi Exp $] + +***********************************************************************/ + +#ifdef __linux__ +#include <libgen.h> +#endif + +#include "mapperInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileName ); +static Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, int Number, int nVars ); +static int Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate ); +static void Map_LibraryAddFaninDelays( Map_SuperLib_t * pLib, Map_Super_t * pGate, Map_Super_t * pFanin, Mio_Pin_t * pPin ); +static int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate ); +static unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate ); + +// fanout limits +extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ }; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Reads the supergate library from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Map_LibraryReadTree( Map_SuperLib_t * pLib, char * pFileName, char * pExcludeFile ) +{ + FILE * pFile; + int Status, num; + Abc_Frame_t * pAbc; + st_table * tExcludeGate = 0; + + // read the beginning of the file + assert( pLib->pGenlib == NULL ); + pFile = Io_FileOpen( pFileName, "open_path", "r", 1 ); +// pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Cannot open input file \"%s\".\n", pFileName ); + return 0; + } + + if ( pExcludeFile ) + { + pAbc = Abc_FrameGetGlobalFrame(); + + tExcludeGate = st_init_table(strcmp, st_strhash); + if ( (num = Mio_LibraryReadExclude( pAbc, pExcludeFile, tExcludeGate )) == -1 ) + { + st_free_table( tExcludeGate ); + tExcludeGate = 0; + return 0; + } + + fprintf ( Abc_FrameReadOut( pAbc ), "Read %d gates from exclude file\n", num ); + } + + Status = Map_LibraryReadFileTree( pLib, pFile, pFileName ); + fclose( pFile ); + if ( Status == 0 ) + return 0; + // prepare the info about the library + return Map_LibraryDeriveGateInfo( pLib, tExcludeGate ); +} + + +/**Function************************************************************* + + Synopsis [Reads the library file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileName ) +{ + ProgressBar * pProgress; + char pBuffer[5000], pLibFile[5000]; + FILE * pFileGen; + Map_Super_t * pGate; + char * pTemp = 0, * pLibName; + int nCounter, k, i; + + // skip empty and comment lines + while ( fgets( pBuffer, 5000, pFile ) != NULL ) + { + // skip leading spaces + for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ ); + // skip comment lines and empty lines + if ( *pTemp != 0 && *pTemp != '#' ) + break; + } + + // get the genlib file name (base) + pLibName = strtok( pTemp, " \t\r\n" ); +#ifdef __linux__ + pLibName = strrchr( pLibName, '/' )+1; +#else + pLibName = strrchr( pLibName, '\\' )+1; +#endif + + if ( strcmp( pLibName, "GATE" ) == 0 ) + { + printf( "The input file \"%s\" looks like a GENLIB file and not a supergate library file.\n", pLib->pName ); + return 0; + } + + + // now figure out the directory if any in the pFileName +#ifdef __linux__ + snprintf( pLibFile, 5000, "%s/%s", dirname(strdup(pFileName)), pLibName ); +#else + { + char * pStr; + strcpy( pLibFile, pFileName ); + pStr = pLibFile + strlen(pBuffer) - 1; + while ( pStr > pLibFile && *pStr != '\\' && *pStr != '/' ) + pStr--; + if ( pStr == pLibFile ) + strcpy( pLibFile, pLibName ); + else + sprintf( pStr, "\\%s", pLibName ); + } +#endif + + pFileGen = Io_FileOpen( pLibFile, "open_path", "r", 1 ); +// pFileGen = fopen( pLibFile, "r" ); + if ( pFileGen == NULL ) + { + printf( "Cannot open the GENLIB file \"%s\".\n", pLibFile ); + return 0; + } + fclose( pFileGen ); + + // read the genlib library + pLib->pGenlib = Mio_LibraryRead( Abc_FrameGetGlobalFrame(), pLibFile, 0, 0 ); + if ( pLib->pGenlib == NULL ) + { + printf( "Cannot read GENLIB file \"%s\".\n", pLibFile ); + return 0; + } + + // read the number of variables + fscanf( pFile, "%d\n", &pLib->nVarsMax ); + if ( pLib->nVarsMax < 2 || pLib->nVarsMax > 10 ) + { + printf( "Suspicious number of variables (%d).\n", pLib->nVarsMax ); + return 0; + } + + // read the number of gates + fscanf( pFile, "%d\n", &pLib->nSupersReal ); + if ( pLib->nSupersReal < 1 || pLib->nSupersReal > 10000000 ) + { + printf( "Suspicious number of gates (%d).\n", pLib->nSupersReal ); + return 0; + } + + // read the number of lines + fscanf( pFile, "%d\n", &pLib->nLines ); + if ( pLib->nLines < 1 || pLib->nLines > 10000000 ) + { + printf( "Suspicious number of lines (%d).\n", pLib->nLines ); + return 0; + } + + // allocate room for supergate pointers + pLib->ppSupers = ALLOC( Map_Super_t *, pLib->nLines + 10000 ); + + // create the elementary supergates + for ( i = 0; i < pLib->nVarsMax; i++ ) + { + // get a new gate + pGate = (Map_Super_t *)Extra_MmFixedEntryFetch( pLib->mmSupers ); + memset( pGate, 0, sizeof(Map_Super_t) ); + // assign the elementary variable, the truth table, and the delays + pGate->Num = i; + // set the truth table + pGate->uTruth[0] = pLib->uTruths[i][0]; + pGate->uTruth[1] = pLib->uTruths[i][1]; + // set the arrival times of all input to non-existent delay + for ( k = 0; k < pLib->nVarsMax; k++ ) + { + pGate->tDelaysR[k].Rise = pGate->tDelaysR[k].Fall = MAP_NO_VAR; + pGate->tDelaysF[k].Rise = pGate->tDelaysF[k].Fall = MAP_NO_VAR; + } + // set an existent arrival time for rise and fall + pGate->tDelaysR[i].Rise = 0.0; + pGate->tDelaysF[i].Fall = 0.0; + // set the gate + pLib->ppSupers[i] = pGate; + } + + // read the lines + nCounter = pLib->nVarsMax; + pProgress = Extra_ProgressBarStart( stdout, pLib->nLines ); + while ( fgets( pBuffer, 5000, pFile ) != NULL ) + { + for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ ); + if ( pTemp[0] == '\0' ) + continue; +// if ( pTemp[0] == 'a' || pTemp[2] == 'a' ) +// { +// pLib->nLines--; +// continue; +// } + + // get the gate + pGate = Map_LibraryReadGateTree( pLib, pTemp, nCounter, pLib->nVarsMax ); + if ( pGate == NULL ) + { + Extra_ProgressBarStop( pProgress ); + return 0; + } + pLib->ppSupers[nCounter++] = pGate; + // later we will derive: truth table, delays, area, number of component gates, etc + + // update the progress bar + Extra_ProgressBarUpdate( pProgress, nCounter, NULL ); + } + Extra_ProgressBarStop( pProgress ); + if ( nCounter != pLib->nLines ) + printf( "The number of lines read (%d) is different what the file says (%d).\n", nCounter, pLib->nLines ); + pLib->nSupersAll = nCounter; + // count the number of real supergates + nCounter = 0; + for ( k = 0; k < pLib->nLines; k++ ) + nCounter += pLib->ppSupers[k]->fSuper; + if ( nCounter != pLib->nSupersReal ) + printf( "The number of gates read (%d) is different what the file says (%d).\n", nCounter, pLib->nSupersReal ); + pLib->nSupersReal = nCounter; + return 1; +} + +/**Function************************************************************* + + Synopsis [Reads one gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, int Number, int nVarsMax ) +{ + Map_Super_t * pGate; + char * pTemp; + int i, Num; + + // start and clean the gate + pGate = (Map_Super_t *)Extra_MmFixedEntryFetch( pLib->mmSupers ); + memset( pGate, 0, sizeof(Map_Super_t) ); + + // set the gate number + pGate->Num = Number; + + // read the mark + pTemp = strtok( pBuffer, " " ); + if ( pTemp[0] == '*' ) + { + pGate->fSuper = 1; + pTemp = strtok( NULL, " " ); + } + + // read the root gate + pGate->pRoot = Mio_LibraryReadGateByName( pLib->pGenlib, pTemp ); + if ( pGate->pRoot == NULL ) + { + printf( "Cannot read the root gate names %s.\n", pTemp ); + return NULL; + } + // set the max number of fanouts + pGate->nFanLimit = s_MapFanoutLimits[ Mio_GateReadInputs(pGate->pRoot) ]; + + // read the pin-to-pin delay + for ( i = 0; ( pTemp = strtok( NULL, " \n\0" ) ); i++ ) + { + if ( pTemp[0] == '#' ) + break; + if ( i == nVarsMax ) + { + printf( "There are too many entries on the line.\n" ); + return NULL; + } + Num = atoi(pTemp); + if ( Num < 0 ) + { + printf( "The number of a child supergate is negative.\n" ); + return NULL; + } + if ( Num > pLib->nLines ) + { + printf( "The number of a child supergate (%d) exceeded the number of lines (%d).\n", + Num, pLib->nLines ); + return NULL; + } + pGate->pFanins[i] = pLib->ppSupers[Num]; + } + pGate->nFanins = i; + if ( pGate->nFanins != (unsigned)Mio_GateReadInputs(pGate->pRoot) ) + { + printf( "The number of fanins of a root gate is wrong.\n" ); + return NULL; + } + + // save the gate name, just in case + if ( pTemp && pTemp[0] == '#' ) + { + if ( pTemp[1] == 0 ) + pTemp = strtok( NULL, " \n\0" ); + else // skip spaces + for ( pTemp++; *pTemp == ' '; pTemp++ ); + // save the formula + pGate->pFormula = Extra_MmFlexEntryFetch( pLib->mmForms, strlen(pTemp)+1 ); + strcpy( pGate->pFormula, pTemp ); + } + // check the rest of the string + pTemp = strtok( NULL, " \n\0" ); + if ( pTemp != NULL ) + printf( "The following trailing symbols found \"%s\".\n", pTemp ); + return pGate; +} + + +/**Function************************************************************* + + Synopsis [Derives information about the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate ) +{ + Map_Super_t * pGate, * pFanin; + Mio_Pin_t * pPin; + unsigned uCanon[2]; + unsigned uTruths[6][2]; + int i, k, nRealVars; + + // set all the derivable info related to the supergates + for ( i = pLib->nVarsMax; i < (int)pLib->nLines; i++ ) + { + pGate = pLib->ppSupers[i]; + + if ( tExcludeGate ) + { + if ( st_is_member( tExcludeGate, Mio_GateReadName( pGate->pRoot ) ) ) + pGate->fExclude = 1; + for ( k = 0; k < (int)pGate->nFanins; k++ ) + { + pFanin = pGate->pFanins[k]; + if ( pFanin->fExclude ) + { + pGate->fExclude = 1; + continue; + } + } + } + + // collect the truth tables of the fanins + for ( k = 0; k < (int)pGate->nFanins; k++ ) + { + pFanin = pGate->pFanins[k]; + uTruths[k][0] = pFanin->uTruth[0]; + uTruths[k][1] = pFanin->uTruth[1]; + } + // derive the new truth table + Mio_DeriveTruthTable( pGate->pRoot, uTruths, pGate->nFanins, 6, pGate->uTruth ); + + // set the initial delays of the supergate + for ( k = 0; k < pLib->nVarsMax; k++ ) + { + pGate->tDelaysR[k].Rise = pGate->tDelaysR[k].Fall = MAP_NO_VAR; + pGate->tDelaysF[k].Rise = pGate->tDelaysF[k].Fall = MAP_NO_VAR; + } + // get the linked list of pins for the given root gate + pPin = Mio_GateReadPins( pGate->pRoot ); + // update the initial delay of the supergate using info from the corresponding pin + for ( k = 0; k < (int)pGate->nFanins; k++, pPin = Mio_PinReadNext(pPin) ) + { + // if there is no corresponding pin, this is a bug, return fail + if ( pPin == NULL ) + { + printf( "There are less pins than gate inputs.\n" ); + return 0; + } + // update the delay information of k-th fanins info from the corresponding pin + Map_LibraryAddFaninDelays( pLib, pGate, pGate->pFanins[k], pPin ); + } + // if there are some pins left, this is a bug, return fail + if ( pPin != NULL ) + { + printf( "There are more pins than gate inputs.\n" ); + return 0; + } + // find the max delay + pGate->tDelayMax.Rise = pGate->tDelayMax.Fall = MAP_NO_VAR; + for ( k = 0; k < pLib->nVarsMax; k++ ) + { + // the rise of the output depends on the rise and fall of the output + if ( pGate->tDelayMax.Rise < pGate->tDelaysR[k].Rise ) + pGate->tDelayMax.Rise = pGate->tDelaysR[k].Rise; + if ( pGate->tDelayMax.Rise < pGate->tDelaysR[k].Fall ) + pGate->tDelayMax.Rise = pGate->tDelaysR[k].Fall; + // the fall of the output depends on the rise and fall of the output + if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Rise ) + pGate->tDelayMax.Fall = pGate->tDelaysF[k].Rise; + if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Fall ) + pGate->tDelayMax.Fall = pGate->tDelaysF[k].Fall; + + pGate->tDelaysF[k].Worst = MAP_MAX( pGate->tDelaysF[k].Fall, pGate->tDelaysF[k].Rise ); + pGate->tDelaysR[k].Worst = MAP_MAX( pGate->tDelaysR[k].Fall, pGate->tDelaysR[k].Rise ); + } + + // count gates and area of the supergate + pGate->nGates = 1; + pGate->Area = (float)Mio_GateReadArea(pGate->pRoot); + for ( k = 0; k < (int)pGate->nFanins; k++ ) + { + pGate->nGates += pGate->pFanins[k]->nGates; + pGate->Area += pGate->pFanins[k]->Area; + } + // do not add the gate to the table, if this gate is an internal gate + // of some supegate and does not correspond to a supergate output + if ( ( !pGate->fSuper ) || pGate->fExclude ) + continue; + + // find the maximum index of a variable in the support of the supergates + // this is important for two reasons: + // (1) to limit the number of permutations considered for canonicization + // (2) to get rid of equivalence phases to speed-up matching + nRealVars = Map_LibraryGetMaxSuperPi_rec( pGate ) + 1; + assert( nRealVars > 0 && nRealVars <= pLib->nVarsMax ); + // if there are some problems with this code, try this instead +// nRealVars = pLib->nVarsMax; + + // find the N-canonical form of this supergate + pGate->nPhases = Map_CanonComputeSlow( pLib->uTruths, pLib->nVarsMax, nRealVars, pGate->uTruth, pGate->uPhases, uCanon ); + // add the supergate into the table by its N-canonical table + Map_SuperTableInsertC( pLib->tTableC, uCanon, pGate ); +/* + { + int uCanon1, uCanon2; + uCanon1 = uCanon[0]; + pGate->uTruth[0] = ~pGate->uTruth[0]; + pGate->uTruth[1] = ~pGate->uTruth[1]; + Map_CanonComputeSlow( pLib->uTruths, pLib->nVarsMax, nRealVars, pGate->uTruth, pGate->uPhases, uCanon ); + uCanon2 = uCanon[0]; +Rwt_Man5ExploreCount( uCanon1 < uCanon2 ? uCanon1 : uCanon2 ); + } +*/ + } + // sort the gates in each line + Map_SuperTableSortSupergatesByDelay( pLib->tTableC, pLib->nSupersAll ); + + // let the glory be manifest +// Map_LibraryPrintTree( pLib ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Finds the largest PI number in the support of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate ) +{ + int i, VarCur, VarMax = 0; + if ( pGate->pRoot == NULL ) + return pGate->Num; + for ( i = 0; i < (int)pGate->nFanins; i++ ) + { + VarCur = Map_LibraryGetMaxSuperPi_rec( pGate->pFanins[i] ); + if ( VarMax < VarCur ) + VarMax = VarCur; + } + return VarMax; +} + +/**Function************************************************************* + + Synopsis [Finds the largest PI number in the support of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate ) +{ + unsigned uSupport; + int i; + if ( pGate->pRoot == NULL ) + return (unsigned)(1 << (pGate->Num)); + uSupport = 0; + for ( i = 0; i < (int)pGate->nFanins; i++ ) + uSupport |= Map_LibraryGetGateSupp_rec( pGate->pFanins[i] ); + return uSupport; +} + +/**Function************************************************************* + + Synopsis [Derives the pin-to-pin delay constraints for the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Map_LibraryAddFaninDelays( Map_SuperLib_t * pLib, Map_Super_t * pGate, Map_Super_t * pFanin, Mio_Pin_t * pPin ) +{ + Mio_PinPhase_t PinPhase; + float tDelayBlockRise, tDelayBlockFall, tDelayPin; + bool fMaxDelay = 0; + int i; + + // use this node to enable max-delay model + if ( fMaxDelay ) + { + float tDelayBlockMax; + // get the maximum delay + tDelayBlockMax = (float)Mio_PinReadDelayBlockMax(pPin); + // go through the supergate inputs + for ( i = 0; i < pLib->nVarsMax; i++ ) + { + if ( pFanin->tDelaysR[i].Rise < 0 ) + continue; + tDelayPin = pFanin->tDelaysR[i].Rise + tDelayBlockMax; + if ( pGate->tDelaysR[i].Rise < tDelayPin ) + pGate->tDelaysR[i].Rise = tDelayPin; + } + // go through the supergate inputs + for ( i = 0; i < pLib->nVarsMax; i++ ) + { + if ( pFanin->tDelaysF[i].Fall < 0 ) + continue; + tDelayPin = pFanin->tDelaysF[i].Fall + tDelayBlockMax; + if ( pGate->tDelaysF[i].Fall < tDelayPin ) + pGate->tDelaysF[i].Fall = tDelayPin; + } + return; + } + + // get the interesting parameters of this pin + PinPhase = Mio_PinReadPhase(pPin); + tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin ); + tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin ); + + // update the rise and fall of the output depending on the phase of the pin + if ( PinPhase != MIO_PHASE_INV ) // NONINV phase is present + { + // the rise of the gate is determined by the rise of the fanin + // the fall of the gate is determined by the fall of the fanin + for ( i = 0; i < pLib->nVarsMax; i++ ) + { + //////////////////////////////////////////////////////// + // consider the rise of the gate + //////////////////////////////////////////////////////// + // check two types of constraints on the rise of the fanin: + // (1) the constraints related to the rise of the PIs + // (2) the constraints related to the fall of the PIs + if ( pFanin->tDelaysR[i].Rise >= 0 ) // case (1) + { // fanin's rise depends on the rise of i-th PI + // update the rise of the gate's output + if ( pGate->tDelaysR[i].Rise < pFanin->tDelaysR[i].Rise + tDelayBlockRise ) + pGate->tDelaysR[i].Rise = pFanin->tDelaysR[i].Rise + tDelayBlockRise; + } + if ( pFanin->tDelaysR[i].Fall >= 0 ) // case (2) + { // fanin's rise depends on the fall of i-th PI + // update the rise of the gate's output + if ( pGate->tDelaysR[i].Fall < pFanin->tDelaysR[i].Fall + tDelayBlockRise ) + pGate->tDelaysR[i].Fall = pFanin->tDelaysR[i].Fall + tDelayBlockRise; + } + //////////////////////////////////////////////////////// + + //////////////////////////////////////////////////////// + // consider the fall of the gate (similar) + //////////////////////////////////////////////////////// + // check two types of constraints on the fall of the fanin: + // (1) the constraints related to the rise of the PIs + // (2) the constraints related to the fall of the PIs + if ( pFanin->tDelaysF[i].Rise >= 0 ) // case (1) + { + if ( pGate->tDelaysF[i].Rise < pFanin->tDelaysF[i].Rise + tDelayBlockFall ) + pGate->tDelaysF[i].Rise = pFanin->tDelaysF[i].Rise + tDelayBlockFall; + } + if ( pFanin->tDelaysF[i].Fall >= 0 ) // case (2) + { + if ( pGate->tDelaysF[i].Fall < pFanin->tDelaysF[i].Fall + tDelayBlockFall ) + pGate->tDelaysF[i].Fall = pFanin->tDelaysF[i].Fall + tDelayBlockFall; + } + //////////////////////////////////////////////////////// + } + } + if ( PinPhase != MIO_PHASE_NONINV ) // INV phase is present + { + // the rise of the gate is determined by the fall of the fanin + // the fall of the gate is determined by the rise of the fanin + for ( i = 0; i < pLib->nVarsMax; i++ ) + { + //////////////////////////////////////////////////////// + // consider the rise of the gate's output + //////////////////////////////////////////////////////// + // check two types of constraints on the fall of the fanin: + // (1) the constraints related to the rise of the PIs + // (2) the constraints related to the fall of the PIs + if ( pFanin->tDelaysF[i].Rise >= 0 ) // case (1) + { // fanin's rise depends on the rise of i-th PI + // update the rise of the gate + if ( pGate->tDelaysR[i].Rise < pFanin->tDelaysF[i].Rise + tDelayBlockRise ) + pGate->tDelaysR[i].Rise = pFanin->tDelaysF[i].Rise + tDelayBlockRise; + } + if ( pFanin->tDelaysF[i].Fall >= 0 ) // case (2) + { // fanin's rise depends on the fall of i-th PI + // update the rise of the gate + if ( pGate->tDelaysR[i].Fall < pFanin->tDelaysF[i].Fall + tDelayBlockRise ) + pGate->tDelaysR[i].Fall = pFanin->tDelaysF[i].Fall + tDelayBlockRise; + } + //////////////////////////////////////////////////////// + + //////////////////////////////////////////////////////// + // consider the fall of the gate (similar) + //////////////////////////////////////////////////////// + // check two types of constraints on the rise of the fanin: + // (1) the constraints related to the rise of the PIs + // (2) the constraints related to the fall of the PIs + if ( pFanin->tDelaysR[i].Rise >= 0 ) // case (1) + { + if ( pGate->tDelaysF[i].Rise < pFanin->tDelaysR[i].Rise + tDelayBlockFall ) + pGate->tDelaysF[i].Rise = pFanin->tDelaysR[i].Rise + tDelayBlockFall; + } + if ( pFanin->tDelaysR[i].Fall >= 0 ) // case (2) + { + if ( pGate->tDelaysF[i].Fall < pFanin->tDelaysR[i].Fall + tDelayBlockFall ) + pGate->tDelaysF[i].Fall = pFanin->tDelaysR[i].Fall + tDelayBlockFall; + } + //////////////////////////////////////////////////////// + } + } +} + + +/**Function************************************************************* + + Synopsis [Performs phase transformation for one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Map_CalculatePhase( unsigned uTruths[][2], int nVars, unsigned uTruth, unsigned uPhase ) +{ + int v, Shift; + for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 ) + if ( uPhase & Shift ) + uTruth = (((uTruth & ~uTruths[v][0]) << Shift) | ((uTruth & uTruths[v][0]) >> Shift)); + return uTruth; +} + +/**Function************************************************************* + + Synopsis [Performs phase transformation for one function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Map_CalculatePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[], unsigned uPhase, unsigned uTruthRes[] ) +{ + unsigned uTemp; + int v, Shift; + + // initialize the result + uTruthRes[0] = uTruth[0]; + uTruthRes[1] = uTruth[1]; + if ( uPhase == 0 ) + return; + // compute the phase + for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 ) + if ( uPhase & Shift ) + { + if ( Shift < 32 ) + { + uTruthRes[0] = (((uTruthRes[0] & ~uTruths[v][0]) << Shift) | ((uTruthRes[0] & uTruths[v][0]) >> Shift)); + uTruthRes[1] = (((uTruthRes[1] & ~uTruths[v][1]) << Shift) | ((uTruthRes[1] & uTruths[v][1]) >> Shift)); + } + else + { + uTemp = uTruthRes[0]; + uTruthRes[0] = uTruthRes[1]; + uTruthRes[1] = uTemp; + } + } +} + +/**Function************************************************************* + + Synopsis [Prints the supergate library after deriving parameters.] + + Description [This procedure is very useful to see the library after + it has been read into the mapper by "read_super" and all the information + about the supergates derived.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Map_LibraryPrintTree( Map_SuperLib_t * pLib ) +{ + Map_Super_t * pGate; + int i, k; + + // print all the info related to the supergates +// for ( i = pLib->nVarsMax; i < (int)pLib->nLines; i++ ) + for ( i = pLib->nVarsMax; i < 20; i++ ) + { + pGate = pLib->ppSupers[i]; + + // write the gate's fanin info and formula + printf( "%6d ", pGate->Num ); + printf( "%c ", pGate->fSuper? '*' : ' ' ); + printf( "%6s", Mio_GateReadName(pGate->pRoot) ); + for ( k = 0; k < (int)pGate->nFanins; k++ ) + printf( " %6d", pGate->pFanins[k]->Num ); + printf( " %s", pGate->pFormula ); + printf( "\n" ); + + // write the gate's derived info + Extra_PrintBinary( stdout, pGate->uTruth, 64 ); + printf( " %3d", pGate->nGates ); + printf( " %6.2f", pGate->Area ); + printf( " (%4.2f, %4.2f)", pGate->tDelayMax.Rise, pGate->tDelayMax.Fall ); + printf( "\n" ); + for ( k = 0; k < pLib->nVarsMax; k++ ) + { + // print the constraint on the rise of the gate in the form (D1, D2), + // where D1 is the constraint related to the rise of the k-th PI + // where D2 is the constraint related to the fall of the k-th PI + if ( pGate->tDelaysR[k].Rise < 0 && pGate->tDelaysR[k].Fall < 0 ) + printf( " (----, ----)" ); + else if ( pGate->tDelaysR[k].Fall < 0 ) + printf( " (%4.2f, ----)", pGate->tDelaysR[k].Rise ); + else if ( pGate->tDelaysR[k].Rise < 0 ) + printf( " (----, %4.2f)", pGate->tDelaysR[k].Fall ); + else + printf( " (%4.2f, %4.2f)", pGate->tDelaysR[k].Rise, pGate->tDelaysR[k].Fall ); + + // print the constraint on the fall of the gate in the form (D1, D2), + // where D1 is the constraint related to the rise of the k-th PI + // where D2 is the constraint related to the fall of the k-th PI + if ( pGate->tDelaysF[k].Rise < 0 && pGate->tDelaysF[k].Fall < 0 ) + printf( " (----, ----)" ); + else if ( pGate->tDelaysF[k].Fall < 0 ) + printf( " (%4.2f, ----)", pGate->tDelaysF[k].Rise ); + else if ( pGate->tDelaysF[k].Rise < 0 ) + printf( " (----, %4.2f)", pGate->tDelaysF[k].Fall ); + else + printf( " (%4.2f, %4.2f)", pGate->tDelaysF[k].Rise, pGate->tDelaysF[k].Fall ); + printf( "\n" ); + } + printf( "\n" ); + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 12529ca7..833ea394 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -226,7 +226,8 @@ static inline void act_var_rescale(sat_solver* s) { } static inline void act_var_bump(sat_solver* s, int v) { - s->activity[v] += s->var_inc; +// s->activity[v] += s->var_inc; + s->activity[v] += (s->pGlobalVars? 3.0 : 1.0) * s->var_inc; if (s->activity[v] > 1e100) act_var_rescale(s); //printf("bump %d %f\n", v-1, activity[v]); @@ -243,6 +244,15 @@ static inline void act_var_bump_factor(sat_solver* s, int v) { order_update(s,v); } +static inline void act_var_bump_global(sat_solver* s, int v) { + s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]); + if (s->activity[v] > 1e100) + act_var_rescale(s); + //printf("bump %d %f\n", v-1, activity[v]); + if (s->orderpos[v] != -1) + order_update(s,v); +} + static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } static inline void act_clause_rescale(sat_solver* s) { @@ -845,6 +855,11 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l for ( i = 0; i < s->act_vars.size; i++ ) act_var_bump_factor(s, s->act_vars.ptr[i]); + // use activity factors in every restart + if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 ) + for ( i = 0; i < s->act_vars.size; i++ ) + act_var_bump_global(s, s->act_vars.ptr[i]); + for (;;){ clause* confl = sat_solver_propagate(s); if (confl != 0){ diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 86e7a966..00ac60ca 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -180,6 +180,7 @@ struct sat_solver_t int fSkipSimplify; // set to one to skip simplification of the clause database + int * pGlobalVars; // for experiments with global vars during interpolation // clause store void * pStore; int fSolved; |