From de978ced7b754706efaf18ae588e18eb05624faf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 19 Jul 2008 08:01:00 -0700 Subject: Version abc80719 --- src/aig/cnf/cnf.h | 1 + src/aig/cnf/cnfMan.c | 16 +++++ src/aig/fra/fraSec.c | 4 +- src/aig/saig/module.make | 3 +- src/aig/saig/saig.h | 2 +- src/aig/saig/saigInter.c | 131 +++++++++++++++++++++++++++++++---- src/aig/saig/saigUnique.c | 170 ++++++++++++++++++++++++++++++++++++++++++++++ 7 files changed, 308 insertions(+), 19 deletions(-) create mode 100644 src/aig/saig/saigUnique.c (limited to 'src/aig') diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h index 5c742f5d..f4f782df 100644 --- a/src/aig/cnf/cnf.h +++ b/src/aig/cnf/cnf.h @@ -136,6 +136,7 @@ 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_DataFlipLastLiteral( Cnf_Dat_t * p ); extern void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable ); extern void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit ); diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c index f1c446fe..1e650a05 100644 --- a/src/aig/cnf/cnfMan.c +++ b/src/aig/cnf/cnfMan.c @@ -202,6 +202,22 @@ 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_DataFlipLastLiteral( Cnf_Dat_t * p ) +{ + p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] ); +} + /**Function************************************************************* Synopsis [Writes CNF into a file.] diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 3365ac9a..3aafeb18 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -389,11 +389,11 @@ 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 fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth ); + extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth ); int Depth; pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Saig_Interpolate( pNew, 5000, 0, 1, 0, pParSec->fVeryVerbose, &Depth ); + RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 1, 1, pParSec->fVeryVerbose, &Depth ); if ( pParSec->fVerbose ) { if ( RetValue == 1 ) diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 6639db21..b9a18ce2 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -9,4 +9,5 @@ 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/saigTrans.c \ + src/aig/saig/saigUnique.c diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 4ae07063..5a7beeec 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -85,7 +85,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 fCheckInd, int fVerbose, int * pDepth ); +extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose, 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 index 37eb3349..86982d46 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -50,6 +50,7 @@ struct Saig_IntMan_t_ 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 @@ -65,7 +66,9 @@ struct Saig_IntMan_t_ int timeTotal; }; +#ifdef ABC_USE_LIBRARIES static int Saig_M144pPerformOneStep( Saig_IntMan_t * p ); +#endif //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -328,7 +331,10 @@ sat_solver * Saig_DeriveSatSolver( for ( i = 0; i < pCnfFrames->nClauses; i++ ) { if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) ) - assert( 0 ); + { + pSat->fSolved = 1; + break; + } } sat_solver_store_mark_roots( pSat ); // return clauses to the original state @@ -604,7 +610,7 @@ p->timeSat += clock() - clk; else if ( status == l_True ) { RetValue = 0; - } + } else { RetValue = -1; @@ -686,6 +692,26 @@ void Saig_ManagerClean( Saig_IntMan_t * p ) 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.] @@ -727,6 +753,8 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) Aig_ManStop( p->pInter ); if ( p->pInterNew ) Aig_ManStop( p->pInterNew ); + Saig_ManagerFreeInters( p ); + Vec_PtrFree( p->vInters ); free( p ); } @@ -743,7 +771,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) +int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p, int fSubtractOld ) { sat_solver * pSat; Aig_Man_t * pInterOld = p->pInter; @@ -757,7 +785,10 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) // start the solver pSat = sat_solver_new(); - sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars ); + 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++ ) @@ -803,21 +834,48 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) } // complement the last literal - Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1]; - pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]); // 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 ); + { +// assert( 0 ); + Cnf_DataFree( pCnfNew ); + return 1; + } } - // complement the last literal - Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1]; - pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]); + 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 @@ -838,8 +896,9 @@ int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fVerbose, int * pDepth ) +int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, 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(); @@ -856,6 +915,7 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRew 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 ) @@ -878,9 +938,11 @@ p->timeCnf += clock() - clk; *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; @@ -919,10 +981,13 @@ p->timeCnf += clock() - clk; } // perform interplation clk = clock(); +#ifdef ABC_USE_LIBRARIES if ( fUseIp ) RetValue = Saig_M144pPerformOneStep( p ); else +#endif RetValue = Saig_PerformOneStep( p, 0 ); + if ( fVerbose ) { printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ", @@ -960,11 +1025,15 @@ 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 ( fCheckInd ) - Status = Saig_ManCheckInductiveContainment( p ); - else + 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 @@ -1004,6 +1073,8 @@ p->timeCnf += clock() - clk; } +#ifdef ABC_USE_LIBRARIES + #include "m114p.h" /**Function************************************************************* @@ -1134,10 +1205,14 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_ Aig_Man_t * p; Aig_Obj_t * pInter, * pInter2, * pVar; Vec_Ptr_t * vInters; + Vec_Int_t * vASteps; int * pLits, * pClauses, * pVars; - int nLits, nVars, i, k, iVar; + int nLits, nVars, i, k, iVar, haveASteps; + int CountA, CountB, CountC, CountCsaved; + assert( M114p_SolverProofIsReady(s) ); vInters = Vec_PtrAlloc( 1000 ); + vASteps = Vec_IntAlloc( 1000 ); // process root clauses p = Aig_ManStart( 10000 ); M114p_SolverForEachRoot( s, &pLits, nLits, i ) @@ -1157,26 +1232,50 @@ Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_ } } Vec_PtrPush( vInters, pInter ); + Vec_IntPush( vASteps, 0 ); } assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); // process learned clauses + CountA = CountB = CountC = CountCsaved = 0; M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i ) { pInter = Vec_PtrEntry( vInters, pClauses[0] ); + haveASteps = Vec_IntEntry( vASteps, pClauses[0] ); 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] ); if ( iVar == -1 ) // var of A + { + haveASteps = 1; pInter = Aig_Or( p, pInter, pInter2 ); + } else // var of B or C pInter = Aig_And( p, pInter, pInter2 ); + + if ( iVar == -1 ) + CountA++; + else if ( iVar == -2 ) + CountB++; + else + { + if ( haveASteps == 0 ) + CountCsaved++; + CountC++; + } } Vec_PtrPush( vInters, pInter ); + Vec_IntPush( vASteps, haveASteps ); } +// printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", +// CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC ); + assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); Vec_PtrFree( vInters ); + Vec_IntFree( vASteps ); + Aig_ObjCreatePo( p, pInter ); Aig_ManCleanup( p ); return p; @@ -1229,6 +1328,8 @@ p->timeInt += clock() - clk; return RetValue; } +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigUnique.c b/src/aig/saig/saigUnique.c new file mode 100644 index 00000000..8b4d80e7 --- /dev/null +++ b/src/aig/saig/saigUnique.c @@ -0,0 +1,170 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3