From 689cbe904e3a28d7502feb9931b748764f947aaf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 27 Sep 2008 08:01:00 -0700 Subject: Version abc80927 --- src/aig/aig/aig.h | 1 + src/aig/aig/aigDup.c | 37 ++++++ src/aig/fra/fraSec.c | 1 + src/aig/saig/module.make | 4 +- src/aig/saig/saig.h | 1 + src/aig/saig/saigAbs.c | 311 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/saig/saigBmc.c | 6 +- src/aig/saig/saigDup.c | 60 +++++++++ src/aig/saig/saigLoc.c | 169 +++++++++++++++++++++++++ src/aig/ssw/module.make | 3 +- src/aig/ssw/ssw.h | 5 + src/aig/ssw/sswCore.c | 10 +- src/aig/ssw/sswInt.h | 9 +- src/aig/ssw/sswMan.c | 3 + src/aig/ssw/sswSat.c | 34 ++++-- src/aig/ssw/sswSweep.c | 32 ++++- src/aig/ssw/sswUnique.c | 254 ++++++++++++++++++++++++++++++++++++++ 17 files changed, 914 insertions(+), 26 deletions(-) create mode 100644 src/aig/saig/saigAbs.c create mode 100644 src/aig/saig/saigLoc.c create mode 100644 src/aig/ssw/sswUnique.c (limited to 'src/aig') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index fcaf41fa..503985b7 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -480,6 +480,7 @@ extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper /*=== aigDup.c ==========================================================*/ extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos ); extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ); diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index c6a4d19a..9fb19b36 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -192,6 +192,43 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates part of the AIG manager.] + + Description [Orders nodes as follows: PIs, ANDs, POs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int i; + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1( pNew ); + Vec_PtrForEachEntry( vPis, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // duplicate internal nodes + Vec_PtrForEachEntry( vPos, pObj, i ) + { + pObjNew = Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) ); + pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ); + Aig_ObjCreatePo( pNew, pObjNew ); + } + Aig_ManSetRegNum( pNew, 0 ); + // check the resulting network + if ( !Aig_ManCheck(pNew) ) + printf( "Aig_ManDupSimple(): The check has failed.\n" ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates the AIG manager.] diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 232a789e..dce34600 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -56,6 +56,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) p->fInterpolation = 1; // enables interpolation p->fReachability = 1; // enables BDD based reachability p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove + p->fUseNewProver = 0; // enables new prover p->fSilent = 0; // disables all output p->fVerbose = 0; // enables verbose reporting of statistics p->fVeryVerbose = 0; // enables very verbose reporting diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index b09091fb..c3c0a1b6 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,8 +1,10 @@ -SRC += src/aig/saig/saigBmc.c \ +SRC += src/aig/saig/saigAbs.c \ + src/aig/saig/saigBmc.c \ src/aig/saig/saigCone.c \ src/aig/saig/saigDup.c \ src/aig/saig/saigHaig.c \ src/aig/saig/saigIoa.c \ + src/aig/saig/saigLoc.c \ src/aig/saig/saigMiter.c \ src/aig/saig/saigPhase.c \ src/aig/saig/saigRetFwd.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 81f0fcf5..c7a40f96 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -84,6 +84,7 @@ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int n extern void Saig_ManPrintCones( Aig_Man_t * p ); /*=== saigDup.c ==========================================================*/ extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p ); +extern Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); /*=== saigHaig.c ==========================================================*/ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); /*=== saigIoa.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c new file mode 100644 index 00000000..48a26a3c --- /dev/null +++ b/src/aig/saig/saigAbs.c @@ -0,0 +1,311 @@ +/**CFile**************************************************************** + + FileName [saigAbs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Proof-based abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +#include "cnf.h" +#include "satSolver.h" +#include "satStore.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Aig_Obj_t * Saig_ObjFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { return ppMap[nFrames*pObj->Id + i]; } +static inline void Saig_ObjSetFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + i] = pNode; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. The only PO is + the output of the last frame.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** pppMap ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t ** ppMap; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f; + assert( Saig_ManRegNum(pAig) > 0 ); + // start the mapping + ppMap = *pppMap = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) * nFrames ); + // start the manager + pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + { + pObj->pData = Aig_ManConst0( pFrames ); + Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData ); + } + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + Saig_ObjSetFrame( ppMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pAig)->pData ); + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreatePi( pFrames ); + Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData ); + } + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + { + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData ); + } + // create POs for this frame + if ( f == nFrames - 1 ) + { + Saig_ManForEachPo( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData ); + } + break; + } + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + { + pObj->pData = Aig_ObjChild0Copy(pObj); + Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData ); + } + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + pObjLo->pData = pObjLi->pData; + Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData ); + } + } + Aig_ManCleanup( pFrames ); + // remove mapping for the nodes that are no longer there + for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ ) + if ( ppMap[i] && Aig_ObjIsNone( Aig_Regular(ppMap[i]) ) ) + ppMap[i] = NULL; + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Finds the set of variables involved in the UNSAT core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose ) +{ + void * pSatCnf; + Intp_Man_t * pManProof; + sat_solver * pSat; + Vec_Int_t * vCore; + int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars; + int i, RetValue; + // create the SAT solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + sat_solver_setnvars( pSat, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + { + printf( "The BMC problem is trivially UNSAT.\n" ); + sat_solver_delete( pSat ); + return NULL; + } + } + sat_solver_store_mark_roots( pSat ); + // solve the problem + RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 ); + if ( RetValue == l_Undef ) + { + printf( "Conflict limit is reached.\n" ); + sat_solver_delete( pSat ); + return NULL; + } + if ( RetValue == l_True ) + { + printf( "The BMC problem is SAT.\n" ); + sat_solver_delete( pSat ); + return NULL; + } + printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts ); + assert( RetValue == l_False ); + pSatCnf = sat_solver_store_release( pSat ); + sat_solver_delete( pSat ); + // derive the UNSAT core + pManProof = Intp_ManAlloc(); + vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose ); + Intp_ManFree( pManProof ); + Sto_ManFree( pSatCnf ); + // derive the set of variables on which the core depends + // collect the variable numbers + nVars = 0; + pVars = ALLOC( int, pCnf->nVars ); + memset( pVars, 0, sizeof(int) * pCnf->nVars ); + Vec_IntForEachEntry( vCore, iClause, i ) + { + pClause1 = pCnf->pClauses[iClause]; + pClause2 = pCnf->pClauses[iClause+1]; + for ( pLit = pClause1; pLit < pClause2; pLit++ ) + { + if ( pVars[ (*pLit) >> 1 ] == 0 ) + nVars++; + pVars[ (*pLit) >> 1 ] = 1; + if ( fVerbose ) + printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 ); + } + if ( fVerbose ) + printf( "\n" ); + } + Vec_IntFree( vCore ); + return pVars; +} + +/**Function************************************************************* + + Synopsis [Labels nodes with the given CNF variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iVar ) +{ + int iVarThis = pCnf->pVarNums[pObj->Id]; + if ( iVarThis >= 0 && iVarThis != iVar ) + return; + assert( Aig_ObjIsNode(pObj) ); + Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin0(pObj), pCnf, iVar ); + Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin1(pObj), pCnf, iVar ); + pCnf->pVarNums[pObj->Id] = iVar; +} + +/**Function************************************************************* + + Synopsis [Performs proof-based abstraction using BMC of the given depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ) +{ + Cnf_Dat_t * pCnf; + Vec_Int_t * vFlops; + Aig_Man_t * pFrames, * pResult; + Aig_Obj_t ** ppAigToFrames; + Aig_Obj_t * pObj, * pObjFrame; + int f, i, * pUnsatCoreVars, clk = clock(); + assert( Saig_ManPoNum(p) == 1 ); + Aig_ManSetPioNumbers( p ); + if ( fVerbose ) + printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax ); + // create the timeframes + pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames ); + // convert them into CNF +// pCnf = Cnf_Derive( pFrames, 0 ); + pCnf = Cnf_DeriveSimple( pFrames, 0 ); + // collect CNF variables involved in UNSAT core + pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, nConfMax, 0 ); + if ( pUnsatCoreVars == NULL ) + { + Aig_ManStop( pFrames ); + Cnf_DataFree( pCnf ); + return NULL; + } + if ( fVerbose ) + { + int Counter = 0; + for ( i = 0; i < pCnf->nVars; i++ ) + Counter += pUnsatCoreVars[i]; + printf( "The number of variables in the UNSAT core is %d (out of %d).\n", Counter, pCnf->nVars ); + } + // map other nodes into existing CNF variables + Aig_ManForEachNode( pFrames, pObj, i ) + if ( pCnf->pVarNums[pObj->Id] >= 0 ) + Saig_ManMarkIntoPresentVars_rec( pObj, pCnf, pCnf->pVarNums[pObj->Id] ); + // collect relevant registers + for ( f = 0; f < nFrames; f++ ) + { + Saig_ManForEachLo( p, pObj, i ) + { + pObjFrame = Saig_ObjFrame( ppAigToFrames, nFrames, pObj, f ); + if ( pObjFrame == NULL ) + continue; + pObjFrame = Aig_Regular(pObjFrame); + if ( Aig_ObjIsConst1( pObjFrame ) ) + continue; + assert( pCnf->pVarNums[pObjFrame->Id] >= 0 ); + if ( pUnsatCoreVars[ pCnf->pVarNums[pObjFrame->Id] ] ) + pObj->fMarkA = 1; + } + } + // collect the flops + vFlops = Vec_IntAlloc( 1000 ); + Saig_ManForEachLo( p, pObj, i ) + if ( pObj->fMarkA ) + { + pObj->fMarkA = 0; + Vec_IntPush( vFlops, i ); + } + if ( fVerbose ) + { + printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); + PRT( "Time", clock() - clk ); + } + // create the resulting AIG + pResult = Saig_ManAbstraction( p, vFlops ); + // cleanup + Aig_ManStop( pFrames ); + Cnf_DataFree( pCnf ); + free( ppAigToFrames ); + free( pUnsatCoreVars ); + Vec_IntFree( vFlops ); + return pResult; + +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index f03364a4..baf00241 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -34,8 +34,7 @@ Synopsis [Create timeframes of the manager for BMC.] - Description [The resulting manager is combinational. The primary inputs - corresponding to register outputs are ordered first. POs correspond to \ + Description [The resulting manager is combinational. POs correspond to \ the property outputs in each time-frame.] SideEffects [] @@ -106,8 +105,7 @@ int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) Synopsis [Create timeframes of the manager for BMC.] - Description [The resulting manager is combinational. The primary inputs - corresponding to register outputs are ordered first. POs correspond to + Description [The resulting manager is combinational. POs correspond to the property outputs in each time-frame. The unrolling is stopped as soon as the number of nodes in the frames exceeds the given maximum size.] diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index 1a050741..165a08f2 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -67,6 +67,66 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) return pAigNew; } +/**Function************************************************************* + + Synopsis [Numbers of flops included in the abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ) +{ + Aig_Man_t * pAigNew; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, Entry; + // start the new manager + pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); + // label included flops + Vec_IntForEachEntry( vFlops, Entry, i ) + { + pObjLi = Saig_ManLi( pAig, Entry ); + assert( pObjLi->fMarkA == 0 ); + pObjLi->fMarkA = 1; + pObjLo = Saig_ManLo( pAig, Entry ); + assert( pObjLo->fMarkA == 0 ); + pObjLo->fMarkA = 1; + } + // create variables for PIs + Aig_ManForEachPi( pAig, pObj, i ) + if ( !pObj->fMarkA ) + pObj->pData = Aig_ObjCreatePi( pAigNew ); + // create variables for LOs + Aig_ManForEachPi( pAig, pObj, i ) + if ( pObj->fMarkA ) + { + pObj->fMarkA = 0; + pObj->pData = Aig_ObjCreatePi( pAigNew ); + } + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs + Aig_ManForEachPo( pAig, pObj, i ) + if ( !pObj->fMarkA ) + Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + // create LIs + Aig_ManForEachPo( pAig, pObj, i ) + if ( pObj->fMarkA ) + { + pObj->fMarkA = 0; + Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManCleanup( pAigNew ); + Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) ); + return pAigNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigLoc.c b/src/aig/saig/saigLoc.c new file mode 100644 index 00000000..60c547dd --- /dev/null +++ b/src/aig/saig/saigLoc.c @@ -0,0 +1,169 @@ +/**CFile**************************************************************** + + FileName [saigLoc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Localization package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigLoc.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 [Performs localization by unrolling timeframes backward.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose ) +{ + sat_solver * pSat; + Vec_Int_t * vTopVarNums; + Vec_Ptr_t * vTop, * vBot; + Cnf_Dat_t * pCnfTop, * pCnfBot; + Aig_Man_t * pPartTop, * pPartBot; + Aig_Obj_t * pObj, * pObjBot; + int i, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev; + assert( Saig_ManPoNum(p) == 1 ); + Aig_ManSetPioNumbers( p ); + + // start the top by including the PO + vBot = Vec_PtrAlloc( 100 ); + vTop = Vec_PtrAlloc( 100 ); + Vec_PtrPush( vTop, Aig_ManPo(p, 0) ); + // create the manager composed of one PI/PO pair + pPartTop = Aig_ManStart( 10 ); + Aig_ObjCreatePo( pPartTop, Aig_ObjCreatePi(pPartTop) ); + pCnfTop = Cnf_Derive( pPartTop, 0 ); + // start the array of CNF variables + vTopVarNums = Vec_IntAlloc( 100 ); + Vec_IntPush( vTopVarNums, pCnfTop->pVarNums[Aig_ManPi(pPartTop,0)->Id] ); + // start the solver + pSat = Cnf_DataWriteIntoSolver( pCnfTop, 1, 0 ); + + // iterate backward unrolling + RetValue = -1; + nSatVarNum = pCnfTop->nVars; + if ( fVerbose ) + printf( "Localization parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax ); + for ( f = 0; ; f++ ) + { + clk = clock(); + // get the bottom + Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot ); + // derive AIG for the part between top and bottom + pPartBot = Aig_ManDupSimpleDfsPart( p, vBot, vTop ); + // convert it into CNF + pCnfBot = Cnf_Derive( pPartBot, Aig_ManPoNum(pPartBot) ); + Cnf_DataLift( pCnfBot, nSatVarNum ); + nSatVarNum += pCnfBot->nVars; + // stitch variables of top and bot + assert( Aig_ManPoNum(pPartBot) == Vec_IntSize(vTopVarNums) ); + Aig_ManForEachPo( pPartBot, pObjBot, i ) + { + Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 0 ); + Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 1 ); + Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) + assert( 0 ); + } + // add CNF to the SAT solver + for ( i = 0; i < pCnfBot->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnfBot->pClauses[i], pCnfBot->pClauses[i+1] ) ) + break; + if ( i < pCnfBot->nClauses ) + { +// printf( "SAT solver became UNSAT after adding clauses.\n" ); + RetValue = 1; + break; + } + // run the SAT solver + nConfPrev = pSat->stats.conflicts; + status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 ); + if ( fVerbose ) + { + printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ", + f+1, Aig_ManPiNum(pPartBot), Aig_ManPoNum(pPartBot), Aig_ManNodeNum(pPartBot), + nSatVarNum, pSat->stats.conflicts-nConfPrev ); + PRT( "Time", clock() - clk ); + } + if ( status == l_Undef ) + break; + if ( status == l_False ) + { + RetValue = 1; + break; + } + assert( status == l_True ); + if ( f == nFramesMax - 1 ) + break; + // the problem is SAT - add more clauses + // create new set of POs to derive new top + Vec_PtrClear( vTop ); + Vec_IntClear( vTopVarNums ); + Vec_PtrForEachEntry( vBot, pObj, i ) + { + assert( Aig_ObjIsPi(pObj) ); + if ( Saig_ObjIsLo(p, pObj) ) + { + pObjBot = pObj->pData; + assert( pObjBot != NULL ); + Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObj) ); + Vec_IntPush( vTopVarNums, pCnfBot->pVarNums[pObjBot->Id] ); + } + } + // remove old top and replace it by bottom + Aig_ManStop( pPartTop ); + pPartTop = pPartBot; + pPartBot = NULL; + Cnf_DataFree( pCnfTop ); + pCnfTop = pCnfBot; + pCnfBot = NULL; + } +// printf( "Completed %d interations.\n", f+1 ); + // cleanup + sat_solver_delete( pSat ); + Aig_ManStop( pPartTop ); + Cnf_DataFree( pCnfTop ); + Aig_ManStop( pPartBot ); + Cnf_DataFree( pCnfBot ); + Vec_IntFree( vTopVarNums ); + Vec_PtrFree( vTop ); + Vec_PtrFree( vBot ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index 6b748598..625d72d1 100644 --- a/src/aig/ssw/module.make +++ b/src/aig/ssw/module.make @@ -10,4 +10,5 @@ SRC += src/aig/ssw/sswAig.c \ src/aig/ssw/sswSat.c \ src/aig/ssw/sswSim.c \ src/aig/ssw/sswSimSat.c \ - src/aig/ssw/sswSweep.c + src/aig/ssw/sswSweep.c \ + src/aig/ssw/sswUnique.c diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 98e8c9d7..766407d4 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -53,6 +53,7 @@ struct Ssw_Pars_t_ int fSkipCheck; // do not run equivalence check for unaffected cones int fLatchCorr; // perform register correspondence int fSemiFormal; // enable semiformal filtering + int fUniqueness; // enable uniqueness constraints int fVerbose; // verbose stats // optimized latch correspondence int fLatchCorrOpt; // perform register correspondence (optimized) @@ -82,11 +83,15 @@ struct Ssw_Cex_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== sswAbs.c ==========================================================*/ +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ); /*=== sswCore.c ==========================================================*/ extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ); extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); +/*=== sswLoc.c ==========================================================*/ +extern int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose ); /*=== sswPart.c ==========================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); /*=== sswPairs.c ===================================================*/ diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 424e3531..8052ffcd 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -45,7 +45,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nPartSize = 0; // size of the partition p->nOverSize = 0; // size of the overlap between partitions p->nFramesK = 1; // the induction depth - p->nFramesAddSim = 2; // additional frames to simulate + p->nFramesAddSim = 0; // additional frames to simulate p->nConstrs = 0; // treat the last nConstrs POs as seq constraints p->nBTLimit = 1000; // conflict limit at a node p->nMinDomSize = 100; // min clock domain considered for optimization @@ -53,6 +53,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->fSkipCheck = 0; // do not run equivalence check for unaffected cones p->fLatchCorr = 0; // performs register correspondence p->fSemiFormal = 0; // enable semiformal filtering + p->fUniqueness = 0; // enable uniqueness constraints p->fVerbose = 0; // verbose stats // latch correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence @@ -153,9 +154,9 @@ clk = clock(); RetValue = Ssw_ManSweep( p ); if ( p->pPars->fVerbose ) { - printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", + printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), - p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal ); + p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal ); if ( p->pPars->fSkipCheck ) printf( "Use = %5d. Skip = %5d. ", p->nRefUse, p->nRefSkip ); @@ -165,7 +166,7 @@ clk = clock(); Ssw_ManCleanup( p ); if ( !RetValue ) break; - +/* { static int Flag = 0; if ( Flag++ == 4 && nIter == 4 ) @@ -176,6 +177,7 @@ clk = clock(); Aig_ManStop( pSRed ); } } +*/ } p->pPars->nIters = nIter + 1; diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 5daffc75..636bd139 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -78,6 +78,10 @@ struct Ssw_Man_t_ int nRecycleCalls; // the number of calls since last recycling int nRecycles; // the number of time SAT solver was recycled int nConeMax; // the maximum cone size + // uniqueness + Vec_Ptr_t * vCommon; // the set of common variables in the logic cones + int iOutputLit; // the output literal of the uniqueness constaint + int nUniques; // the number of uniqueness constaints used // sequential simulator Ssw_Sml_t * pSml; // counter example storage @@ -205,10 +209,13 @@ extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrame extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ); extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ +extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ); extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ); extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); - +/*=== sswUnique.c ===================================================*/ +extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ); +extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 ); #ifdef __cplusplus } diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index ba19d46e..d4a26f64 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -59,6 +59,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // SAT solving (latch corr only) p->vUsedNodes = Vec_PtrAlloc( 1000 ); p->vUsedPis = Vec_PtrAlloc( 1000 ); + p->vCommon = Vec_PtrAlloc( 100 ); + p->iOutputLit = -1; // allocate storage for sim pattern p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) ); p->pPatWords = ALLOC( unsigned, p->nPatWords ); @@ -190,6 +192,7 @@ void Ssw_ManStop( Ssw_Man_t * p ) Vec_PtrFree( p->vUsedNodes ); Vec_PtrFree( p->vUsedPis ); Vec_IntFree( p->vSatVars ); + Vec_PtrFree( p->vCommon ); FREE( p->pNodeToFrames ); FREE( p->pPatWords ); free( p ); diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index 264b39d1..af3bf80e 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -42,7 +42,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) { int nBTLimit = p->pPars->nBTLimit; - int pLits[2], RetValue, RetValue1, clk;//, status; + int pLits[3], nLits, RetValue, RetValue1, clk;//, status; p->nSatCalls++; // sanity checks @@ -59,8 +59,11 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) // solve under assumptions // A = 1; B = 0 OR A = 1; B = 1 + nLits = 2; pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); + if ( p->iOutputLit > -1 ) + pLits[nLits++] = p->iOutputLit; if ( p->pPars->fPolarFlip ) { if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); @@ -75,16 +78,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } clk = clock(); - RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) { p->timeSatUnsat += clock() - clk; - pLits[0] = lit_neg( pLits[0] ); - pLits[1] = lit_neg( pLits[1] ); - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); - assert( RetValue ); + if ( nLits == 2 ) + { + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } p->nSatCallsUnsat++; } else if ( RetValue1 == l_True ) @@ -109,8 +115,11 @@ p->timeSatUndec += clock() - clk; // solve under assumptions // A = 0; B = 1 OR A = 0; B = 0 + nLits = 2; pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); + if ( p->iOutputLit > -1 ) + pLits[nLits++] = p->iOutputLit; if ( p->pPars->fPolarFlip ) { if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); @@ -124,16 +133,19 @@ p->timeSatUndec += clock() - clk; } clk = clock(); - RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) { p->timeSatUnsat += clock() - clk; - pLits[0] = lit_neg( pLits[0] ); - pLits[1] = lit_neg( pLits[1] ); - RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); - assert( RetValue ); + if ( nLits == 2 ) + { + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } p->nSatCallsUnsat++; } else if ( RetValue1 == l_True ) diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index add00a88..b971a13a 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -87,14 +87,15 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) { Aig_Obj_t * pObjFraig; int nVarNum, Value; - assert( Aig_ObjIsPi(pObj) ); +// assert( Aig_ObjIsPi(pObj) ); pObjFraig = Ssw_ObjFrame( p, pObj, f ); nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) ); Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); +// Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum ))); // Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); if ( p->pPars->fPolarFlip ) { @@ -120,7 +121,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ) int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); Aig_ManForEachPi( p->pAig, pObj, i ) - if ( Ssw_ManOriginalPiValue( p, pObj, f ) ) + if ( Ssw_ManGetSatVarValue( p, pObj, f ) ) Aig_InfoSetBit( p->pPatWords, i ); } @@ -179,7 +180,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) { // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - return 0; + return 0; // count the number of skipped calls if ( !pObj->fMarkA && !pObjRepr->fMarkA ) p->nRefSkip++; @@ -212,6 +213,18 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) // disproved the equivalence Ssw_SmlSavePatternAig( p, f ); } + if ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 && + Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 ) + { + if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) ) + { + int RetValue; + assert( p->iOutputLit > -1 ); + RetValue = Ssw_ManSweepNode( p, pObj, f, 0 ); + p->iOutputLit = -1; + return RetValue; + } + } if ( p->pPars->nConstrs == 0 ) Ssw_ManResimulateWord( p, pObj, pObjRepr, f ); else @@ -300,6 +313,7 @@ int Ssw_ManSweep( Ssw_Man_t * p ) Bar_Progress_t * pProgress = NULL; Aig_Obj_t * pObj, * pObj2, * pObjNew; int nConstrPairs, clk, i, f; + int v; // perform speculative reduction clk = clock(); @@ -330,6 +344,8 @@ clk = clock(); Ssw_ManSweepMarkRefinement( p ); p->timeMarkCones += clock() - clk; +//Ssw_ManUnique( p ); + // map constants and PIs of the last frame f = p->pPars->nFramesK; Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); @@ -338,10 +354,18 @@ p->timeMarkCones += clock() - clk; // make sure LOs are assigned Saig_ManForEachLo( p->pAig, pObj, i ) assert( Ssw_ObjFrame( p, pObj, f ) != NULL ); +//// + // bring up the previous frames + if ( p->pPars->fUniqueness ) + for ( v = 0; v < f; v++ ) + Saig_ManForEachLo( p->pAig, pObj, i ) + Ssw_CnfNodeAddToSolver( p, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) ); +//// // sweep internal nodes p->fRefined = 0; p->nSatFailsReal = 0; p->nRefUse = p->nRefSkip = 0; + p->nUniques = 0; Ssw_ClassesClearRefined( p->ppClasses ); if ( p->pPars->fVerbose ) pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c new file mode 100644 index 00000000..888ed3da --- /dev/null +++ b/src/aig/ssw/sswUnique.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [sswSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [On-demand uniqueness constraints.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the result of merging the two vectors.] + + Description [Assumes that the vectors are sorted in the increasing order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr ) +{ + Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray; + Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray; + Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; + Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; + Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; + Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) ); + pBeg = (Aig_Obj_t **)vArr->pArray; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( (*pBeg1)->Id == (*pBeg2)->Id ) + *pBeg++ = *pBeg1++, pBeg2++; + else if ( (*pBeg1)->Id < (*pBeg2)->Id ) + *pBeg++ = *pBeg1++; + else + *pBeg++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pBeg++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pBeg++ = *pBeg2++; + vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray; + assert( vArr->nSize <= vArr->nCap ); + assert( vArr->nSize >= vArr1->nSize ); + assert( vArr->nSize >= vArr2->nSize ); +} + +/**Function************************************************************* + + Synopsis [Returns the result of merging the two vectors.] + + Description [Assumes that the vectors are sorted in the increasing order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr ) +{ + Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray; + Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray; + Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; + Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; + Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; + Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) ); + pBeg = (Aig_Obj_t **)vArr->pArray; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( (*pBeg1)->Id == (*pBeg2)->Id ) + *pBeg++ = *pBeg1++, pBeg2++; + else if ( (*pBeg1)->Id < (*pBeg2)->Id ) +// *pBeg++ = *pBeg1++; + pBeg1++; + else +// *pBeg++ = *pBeg2++; + pBeg2++; + } +// while ( pBeg1 < pEnd1 ) +// *pBeg++ = *pBeg1++; +// while ( pBeg2 < pEnd2 ) +// *pBeg++ = *pBeg2++; + vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray; + assert( vArr->nSize <= vArr->nCap ); + assert( vArr->nSize <= vArr1->nSize ); + assert( vArr->nSize <= vArr2->nSize ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if uniqueness constraints can be added.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) +{ + int fVerbose = 0; + Aig_Obj_t * ppObjs[2], * pTemp; + Vec_Ptr_t * vSupp, * vSupp2; + int i, k, Value0, Value1, RetValue; + assert( p->pPars->nFramesK > 1 ); + + vSupp = Vec_PtrAlloc( 100 ); + vSupp2 = Vec_PtrAlloc( 100 ); + Vec_PtrClear( p->vCommon ); + + // compute the first support in terms of LOs + ppObjs[0] = pRepr; + ppObjs[1] = pObj; + Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp ); + // modify support to be in terms of LIs + k = 0; + Vec_PtrForEachEntry( vSupp, pTemp, i ) + if ( Saig_ObjIsLo(p->pAig, pTemp) ) + Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) ); + Vec_PtrShrink( vSupp, k ); + // compute the support of support + Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 ); + // return support to LO + Vec_PtrForEachEntry( vSupp, pTemp, i ) + Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) ); + // find the number of common vars + Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease ); + Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease ); + Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon ); +/* + { + Vec_Ptr_t * vNew = Vec_PtrDup(vSupp); + Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease ); + if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) ) + printf( "Not unique!\n" ); + } + { + Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2); + Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease ); + if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) ) + printf( "Not unique!\n" ); + } + { + Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon); + Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease ); + if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) ) + printf( "Not unique!\n" ); + } +*/ + if ( fVerbose ) + printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ", + Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) ); + + // check the current values + RetValue = 1; + Vec_PtrForEachEntry( p->vCommon, pTemp, i ) + { + Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 ); + Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 ); + if ( Value0 != Value1 ) + RetValue = 0; + if ( fVerbose ) + printf( "%d", Value0 ^ Value1 ); + } + if ( Vec_PtrSize(p->vCommon) == 0 ) + RetValue = 0; + if ( fVerbose ) + printf( "\n" ); + + Vec_PtrFree( vSupp ); + Vec_PtrFree( vSupp2 ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Returns the output of the uniqueness constraint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 ) +{ + Aig_Obj_t * pObj, * pObj1New, * pObj2New, * pMiter, * pTotal; + int i, pLits[2]; +// int RetValue; + assert( Vec_PtrSize(vCommon) > 0 ); + // generate the constraint + pTotal = Aig_ManConst0(p->pFrames); + Vec_PtrForEachEntry( vCommon, pObj, i ) + { + assert( Saig_ObjIsLo(p->pAig, pObj) ); + pObj1New = Ssw_ObjFrame( p, pObj, f1 ); + pObj2New = Ssw_ObjFrame( p, pObj, f2 ); + pMiter = Aig_Exor( p->pFrames, pObj1New, pObj2New ); + pTotal = Aig_Or( p->pFrames, pTotal, pMiter ); + } + if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) ) + { +// printf( "Skipped\n" ); + return 0; + } + p->nUniques++; + // create CNF + Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) ); + // add output constraint + pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) ); +/* + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); + assert( RetValue ); + // simplify the solver + if ( p->pSat->qtail != p->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + } +*/ + assert( p->iOutputLit == -1 ); + p->iOutputLit = pLits[0]; + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3