From 0f03f34924b64814791347c5dcf0633dd244d341 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 10 May 2008 08:01:00 -0700 Subject: Version abc80510 --- src/aig/aig/aig.h | 4 +- src/aig/aig/aigDup.c | 55 ++++ src/aig/aig/aigMan.c | 2 +- src/aig/aig/aigObj.c | 5 + src/aig/cnf/cnf.h | 3 +- src/aig/cnf/cnfMan.c | 25 ++ src/aig/ntl/ntl.h | 13 +- src/aig/ntl/ntlSweep.c | 31 ++- src/aig/saig/module.make | 1 + src/aig/saig/saig.h | 2 + src/aig/saig/saigInter.c | 657 +++++++++++++++++++++++++++++++++++++++++++++++ 11 files changed, 787 insertions(+), 11 deletions(-) create mode 100644 src/aig/saig/saigInter.c (limited to 'src/aig') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 6ecec3f8..1450ad21 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -64,7 +64,7 @@ typedef enum { } Aig_Type_t; // the AIG node -struct Aig_Obj_t_ // 8 words +struct Aig_Obj_t_ // 9 words { union { Aig_Obj_t * pNext; // strashing table @@ -477,6 +477,7 @@ extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p ); 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 ); /*=== 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 ); @@ -524,6 +525,7 @@ extern Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ); extern Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ); extern Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 ); extern Aig_Obj_t * Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC ); +extern Aig_Obj_t * Aig_Multi( Aig_Man_t * p, Aig_Obj_t ** pArgs, int nArgs, Aig_Type_t Type ); extern Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs ); extern Aig_Obj_t * Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 ); extern Aig_Obj_t * Aig_CreateAnd( Aig_Man_t * p, int nVars ); diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index 9dfa2ddf..55dc5625 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -732,6 +732,61 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Creates the miter of the two AIG managers.] + + Description [Oper is the operation to perform on the outputs of the miter. + Oper == 0 is XOR + Oper == 1 is complemented implication (p1 => p2) + Oper == 2 is OR + Oper == 3 is AND + ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + assert( Aig_ManRegNum(p1) == 0 ); + assert( Aig_ManRegNum(p2) == 0 ); + assert( Aig_ManPoNum(p1) == 1 ); + assert( Aig_ManPoNum(p2) == 1 ); + assert( Aig_ManPiNum(p1) == Aig_ManPiNum(p2) ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) ); + // add first AIG + Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p1, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Aig_ManForEachNode( p1, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add second AIG + Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p2, pObj, i ) + pObj->pData = Aig_ManPi( pNew, i ); + Aig_ManForEachNode( p2, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // add the output + if ( Oper == 0 ) // XOR + pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) ); + else if ( Oper == 1 ) // implication is PO(p1) -> PO(p2) ... complement is PO(p1) & !PO(p2) + pObj = Aig_And( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,0))) ); + else if ( Oper == 2 ) // OR + pObj = Aig_Or( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) ); + else if ( Oper == 3 ) // AND + pObj = Aig_And( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) ); + else + assert( 0 ); + Aig_ObjCreatePo( pNew, pObj ); + Aig_ManCleanup( pNew ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 2e68e93c..47ee8d4d 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -216,7 +216,7 @@ void Aig_ManStop( Aig_Man_t * p ) FREE( p->pObjCopies ); FREE( p->pReprs ); FREE( p->pEquivs ); -// free( p->pTable ); + free( p->pTable ); free( p ); } diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 88fb9c9d..73b15caf 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -370,6 +370,11 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in // make sure object is not pointing to itself assert( pObjOld != Aig_ObjFanin0(pObjNewR) ); assert( pObjOld != Aig_ObjFanin1(pObjNewR) ); + if ( pObjOld == Aig_ObjFanin0(pObjNewR) || pObjOld == Aig_ObjFanin1(pObjNewR) ) + { + printf( "Aig_ObjReplace(): Internal error!\n" ); + exit(1); + } // recursively delete the old node - but leave the object there pObjNewR->nRefs++; if ( !Aig_ObjIsPi(pObjOld) ) diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 9a49805b..e664b1bc 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -136,8 +136,9 @@ extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); +extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); -void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); +extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); extern void Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf ); /*=== cnfMap.c ========================================================*/ extern void Cnf_DeriveMapping( Cnf_Man_t * p ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index 934aab1c..b6ed3da0 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -201,6 +201,31 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ) p->pClauses[0][v] += 2*nVarsPlus; } +/**Function************************************************************* + + Synopsis [Writes CNF into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) +{ + FILE * pFile = stdout; + int * pLit, * pStop, i; + fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses ); + for ( i = 0; i < p->nClauses; i++ ) + { + for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) + fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + fprintf( pFile, "\n" ); + } + fprintf( pFile, "\n" ); +} + /**Function************************************************************* Synopsis [Writes CNF into a file.] diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 55581026..c4950650 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -98,6 +98,7 @@ struct Ntl_Mod_t_ float * pDelayTable; // other data members void * pCopy; + int nUsed, nRems; }; struct Ntl_Obj_t_ @@ -186,12 +187,12 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int /// ITERATORS /// //////////////////////////////////////////////////////////////////////// -#define Ntl_ManForEachModel( p, pNtl, i ) \ - Vec_PtrForEachEntry( p->vModels, pNtl, i ) -#define Ntl_ManForEachCiNet( p, pNtl, i ) \ - Vec_PtrForEachEntry( p->vCis, pNtl, i ) -#define Ntl_ManForEachCoNet( p, pNtl, i ) \ - Vec_PtrForEachEntry( p->vCos, pNtl, i ) +#define Ntl_ManForEachModel( p, pMod, i ) \ + Vec_PtrForEachEntry( p->vModels, pMod, i ) +#define Ntl_ManForEachCiNet( p, pNet, i ) \ + Vec_PtrForEachEntry( p->vCis, pNet, i ) +#define Ntl_ManForEachCoNet( p, pNet, i ) \ + Vec_PtrForEachEntry( p->vCos, pNet, i ) #define Ntl_ManForEachNode( p, pObj, i ) \ for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \ if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c index ed602297..8309e1b3 100644 --- a/src/aig/ntl/ntlSweep.c +++ b/src/aig/ntl/ntlSweep.c @@ -97,11 +97,11 @@ void Ntl_ManSweepMark( Ntl_Man_t * p ) int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ) { int nObjsOld[NTL_OBJ_VOID]; - Ntl_Mod_t * pRoot; + Ntl_Mod_t * pRoot, * pMod; Ntl_Net_t * pNet; Ntl_Obj_t * pObj; int i, k, nNetsOld; - int Counter = 0; + int ModelCounter = 0, Counter = 0; // remember the number of objects pRoot = Ntl_ManRootModel( p ); @@ -112,6 +112,23 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ) // mark the nets that do not fanout into POs Ntl_ManSweepMark( p ); + // count how many boxes of each type are swept away + if ( fVerbose ) + { + Ntl_ManForEachModel( p, pMod, i ) + pMod->nUsed = pMod->nRems = 0; + Ntl_ModelForEachObj( pRoot, pObj, i ) + if ( Ntl_ObjIsBox(pObj) && pObj->pImplem ) + { + pObj->pImplem->nUsed++; + if ( !pObj->fMark ) + { + if ( pObj->pImplem->nRems++ == 0 ) + ModelCounter++; + } + } + } + // remove the useless objects and their nets Ntl_ModelForEachObj( pRoot, pObj, i ) { @@ -134,6 +151,8 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ) Counter++; } + + // print detailed statistics of sweeping if ( fVerbose ) { @@ -151,6 +170,14 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ) nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX], !nObjsOld[NTL_OBJ_BOX]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX]) / nObjsOld[NTL_OBJ_BOX] ); printf( "\n" ); + if ( ModelCounter ) + { + printf( "Sweep removed %d boxed of %d types (out of %d types):\n", + nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX], ModelCounter, Vec_PtrSize(p->vModels)-1 ); + Ntl_ManForEachModel( p, pMod, i ) + if ( i ) + printf( "Model %3d : %-40s Swept = %5d. Left = %5d.\n", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems ); + } } if ( !Ntl_ManCheck( p ) ) printf( "Ntl_ManSweep: The check has failed for design %s.\n", p->pName ); diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index c9172024..20428b36 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,4 +1,5 @@ SRC += src/aig/saig/saig_.c \ + src/aig/saig/saigInter.c \ src/aig/saig/saigPhase.c \ src/aig/saig/saigRetFwd.c \ src/aig/saig/saigRetMin.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 7f6bb292..60db874b 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -75,6 +75,8 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== saigInter.c ==========================================================*/ +extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fVerbose, int * pDepth ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c new file mode 100644 index 00000000..34069b03 --- /dev/null +++ b/src/aig/saig/saigInter.c @@ -0,0 +1,657 @@ +/**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" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + The interpolation algorithm implemented here was introduced in the paper: + K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13. +*/ + + +// 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; + // 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; +}; + +//////////////////////////////////////////////////////////////////////// +/// 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, * pCtrl; + 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) ); + 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_ManPoNum(pAig) == 1 ); + // start the fraig package + 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] ) ) + assert( 0 ); + } + sat_solver_store_mark_roots( pSat ); + // return clauses to the original state + Cnf_DataLift( pCnfAig, -pCnfFrames->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 Saig_PerformOneStep( Saig_IntMan_t * p ) +{ + sat_solver * pSat; + void * pSatCnf = NULL; + Inta_Man_t * pManInter; + 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(); + pManInter = Inta_ManAlloc(); + p->pInterNew = Inta_ManInterpolate( pManInter, pSatCnf, p->vVarsAB, 0 ); + Inta_ManFree( pManInter ); +p->timeInt += clock() - clk; + Sto_ManFree( pSatCnf ); + return RetValue; +} + +/**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 ); + } + assert( RetValue != -1 ); + Aig_ManStop( pMiter ); + 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_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 ); + free( p ); +} + +/**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 fVerbose, int * pDepth ) +{ + int fUseTransRel = 0; + 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; + // can perform SAT sweeping and/or rewriting of this AIG... + p->pAig = pAig; + if ( fUseTransRel ) + 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", + Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), Aig_ManRegNum(pAig), + Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig), + p->pCnfAig->nVars, p->pCnfAig->nClauses ); + } + + // derive interpolant + *pDepth = -1; + for ( s = 0; ; s++ ) + { +clk2 = clock(); + // initial state + p->pInter = Saig_ManInit( Aig_ManRegNum(pAig) ); +clk = clock(); + p->pCnfInter = Cnf_Derive( p->pInter, 0 ); +p->timeCnf += clock() - clk; + // timeframes + p->pFrames = Saig_ManFramesInter( pAig, p->nFrames ); +clk = clock(); +// 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++ ) + { + // perform interplation + clk = clock(); + RetValue = Saig_PerformOneStep( p ); + if ( fVerbose ) + { + printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%4d. Conf =%6d. ", + i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur ); + PRT( "Time", clock() - clk ); + if ( Aig_ManNodeNum(p->pInter) == 0 ) + { + Aig_Obj_t * pObj = Aig_ManPo(p->pInter, 0); + Aig_Obj_t * pObjR = Aig_Regular(pObj); + int x = 0; + } + } + 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; + // check containment of interpolants +clk = clock(); + 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 ( fUseTransRel ) + { + 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 /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3