diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/module.make | 3 | ||||
-rw-r--r-- | src/aig/saig/saigGlaCba.c (renamed from src/aig/saig/saigAbsGla.c) | 102 | ||||
-rw-r--r-- | src/aig/saig/saigGlaPba.c | 518 |
3 files changed, 571 insertions, 52 deletions
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 4efc1d80..df6fd7cb 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,6 +1,5 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigAbsCba.c \ - src/aig/saig/saigAbsGla.c \ src/aig/saig/saigAbsPba.c \ src/aig/saig/saigAbsStart.c \ src/aig/saig/saigAbsVfa.c \ @@ -12,6 +11,8 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigConstr.c \ src/aig/saig/saigConstr2.c \ src/aig/saig/saigDup.c \ + src/aig/saig/saigGlaCba.c \ + src/aig/saig/saigGlaPba.c \ src/aig/saig/saigHaig.c \ src/aig/saig/saigInd.c \ src/aig/saig/saigIoa.c \ diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigGlaCba.c index 69b4cb66..8fca4796 100644 --- a/src/aig/saig/saigAbsGla.c +++ b/src/aig/saig/saigGlaCba.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [saigAbsGla.c] + FileName [saigGlaCba.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: saigAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: saigGlaCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -29,8 +29,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Aig_GlaMan_t_ Aig_GlaMan_t; -struct Aig_GlaMan_t_ +typedef struct Aig_Gla1Man_t_ Aig_Gla1Man_t; +struct Aig_Gla1Man_t_ { // user data Aig_Man_t * pAig; @@ -79,7 +79,7 @@ struct Aig_GlaMan_t_ SeeAlso [] ***********************************************************************/ -static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl ) +static inline int Aig_Gla1AddConst( sat_solver * pSat, int iVar, int fCompl ) { lit Lit = toLitCond( iVar, fCompl ); if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) @@ -98,7 +98,7 @@ static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl ) SeeAlso [] ***********************************************************************/ -static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) +static inline int Aig_Gla1AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) { lit Lits[2]; @@ -126,7 +126,7 @@ static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int SeeAlso [] ***********************************************************************/ -static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) +static inline int Aig_Gla1AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) { lit Lits[3]; @@ -160,7 +160,7 @@ static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iV SeeAlso [] ***********************************************************************/ -Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses ) +Vec_Int_t * Aig_Gla1CollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses ) { Vec_Int_t * vAssigned; Aig_Obj_t * pObj; @@ -197,7 +197,7 @@ Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses ) SeeAlso [] ***********************************************************************/ -void Aig_GlaCollectAbstr( Aig_GlaMan_t * p ) +void Aig_Gla1CollectAbstr( Aig_Gla1Man_t * p ) { Aig_Obj_t * pObj; int i, Entry; @@ -210,20 +210,20 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p ) assert( Entry == 1 ); pObj = Aig_ManObj( p->pAig, i ); if ( Vec_IntFind( p->vAssigned, Aig_ObjId(pObj) ) == -1 ) - printf( "Aig_GlaCollectAbstr(): Object not found\n" ); + printf( "Aig_Gla1CollectAbstr(): Object not found\n" ); if ( Aig_ObjIsNode(pObj) ) { if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObj) ) == -1 ) - printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" ); + printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" ); if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId1(pObj) ) == -1 ) - printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" ); + printf( "Aig_Gla1CollectAbstr(): Node's fanin is not found\n" ); } else if ( Saig_ObjIsLo(p->pAig, pObj) ) { Aig_Obj_t * pObjLi; pObjLi = Saig_ObjLoToLi(p->pAig, pObj); if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObjLi) ) == -1 ) - printf( "Aig_GlaCollectAbstr(): Flop's fanin is not found\n" ); + printf( "Aig_Gla1CollectAbstr(): Flop's fanin is not found\n" ); } else assert( Aig_ObjIsConst1(pObj) ); } @@ -258,13 +258,13 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p ) SeeAlso [] ***********************************************************************/ -void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) +void Aig_Gla1DeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) { if ( pObj->pData ) return; assert( Aig_ObjIsNode(pObj) ); - Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) ); - Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) ); + Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_Gla1DeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) ); pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } @@ -279,7 +279,7 @@ void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) +Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p ) { Aig_Man_t * pNew; Aig_Obj_t * pObj; @@ -303,7 +303,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) // create internal nodes Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i ) // pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - Aig_GlaDeriveAbs_rec( pNew, pObj ); + Aig_Gla1DeriveAbs_rec( pNew, pObj ); // create PO Saig_ManForEachPo( p->pAig, pObj, i ) pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); @@ -332,7 +332,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) SeeAlso [] ***********************************************************************/ -int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) +int Aig_Gla1FetchVar( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k ) { int i, iVecId, iSatVar; assert( k < p->nFrames ); @@ -368,7 +368,7 @@ int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) SeeAlso [] ***********************************************************************/ -int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) +int Aig_Gla1ObjAddToSolver( Aig_Gla1Man_t * p, Aig_Obj_t * pObj, int k ) { if ( k == p->nFrames ) { @@ -388,17 +388,17 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) assert( k < p->nFrames ); assert( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) ); if ( Aig_ObjIsConst1(pObj) ) - return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 0 ); + return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 0 ); if ( Saig_ObjIsLo(p->pAig, pObj) ) { Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); if ( k == 0 ) { - Aig_GlaFetchVar( p, Aig_ObjFanin0(pObjLi), 0 ); - return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 1 ); + Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObjLi), 0 ); + return Aig_Gla1AddConst( p->pSat, Aig_Gla1FetchVar(p, pObj, k), 1 ); } - return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k), - Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), + return Aig_Gla1AddBuffer( p->pSat, Aig_Gla1FetchVar(p, pObj, k), + Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObjLi), k-1), Aig_ObjFaninC0(pObjLi) ); } else @@ -407,9 +407,9 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) int i, Entry; assert( Aig_ObjIsNode(pObj) ); if ( p->vObj2Cnf == NULL ) - return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), - Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), - Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), + return Aig_Gla1AddNode( p->pSat, Aig_Gla1FetchVar(p, pObj, k), + Aig_Gla1FetchVar(p, Aig_ObjFanin0(pObj), k), + Aig_Gla1FetchVar(p, Aig_ObjFanin1(pObj), k), Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); // derive clauses assert( pObj->fMarkA ); @@ -422,7 +422,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) // derive variables Cnf_CollectLeaves( pObj, p->vLeaves, 0 ); Vec_PtrForEachEntry( Aig_Obj_t *, p->vLeaves, pObj, i ) - Aig_GlaFetchVar( p, pObj, k ); + Aig_Gla1FetchVar( p, pObj, k ); // translate clauses assert( Vec_IntSize(vClauses) >= 2 ); assert( Vec_IntEntry(vClauses, 0) == 0 ); @@ -433,7 +433,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) Vec_IntClear( p->vLits ); continue; } - Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_GlaFetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) ); + Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_Gla1FetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) ); if ( i == Vec_IntSize(vClauses) - 1 || Vec_IntEntry(vClauses, i+1) == 0 ) { if ( !sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits)+Vec_IntSize(p->vLits) ) ) @@ -455,12 +455,12 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) SeeAlso [] ***********************************************************************/ -Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fNaiveCnf ) +Aig_Gla1Man_t * Aig_Gla1ManStart( Aig_Man_t * pAig, int fNaiveCnf ) { - Aig_GlaMan_t * p; + Aig_Gla1Man_t * p; int i; - p = ABC_CALLOC( Aig_GlaMan_t, 1 ); + p = ABC_CALLOC( Aig_Gla1Man_t, 1 ); p->pAig = pAig; p->vAssigned = Vec_IntAlloc( 1000 ); p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) ); @@ -511,7 +511,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fNaiveCnf ) SeeAlso [] ***********************************************************************/ -void Aig_GlaManStop( Aig_GlaMan_t * p ) +void Aig_Gla1ManStop( Aig_Gla1Man_t * p ) { Vec_IntFreeP( &p->vAssigned ); Vec_IntFreeP( &p->vIncluded ); @@ -551,7 +551,7 @@ void Aig_GlaManStop( Aig_GlaMan_t * p ) SeeAlso [] ***********************************************************************/ -Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame ) +Abc_Cex_t * Aig_Gla1DeriveCex( Aig_Gla1Man_t * p, int iFrame ) { Abc_Cex_t * pCex; Aig_Obj_t * pObj; @@ -600,7 +600,7 @@ Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame ) SeeAlso [] ***********************************************************************/ -void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c ) +void Aig_Gla1PrintAbstr( Aig_Gla1Man_t * p, int f, int r, int v, int c ) { if ( r == 0 ) printf( "== %3d ==", f ); @@ -621,7 +621,7 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c ) SeeAlso [] ***********************************************************************/ -void Aig_GlaExtendIncluded( Aig_GlaMan_t * p ) +void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p ) { Aig_Obj_t * pObj; int i, k; @@ -651,11 +651,11 @@ void Aig_GlaExtendIncluded( Aig_GlaMan_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose ) +Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose ) { int nStart = 0; Vec_Int_t * vResult = NULL; - Aig_GlaMan_t * p; + Aig_Gla1Man_t * p; Aig_Man_t * pAbs; Aig_Obj_t * pObj; Abc_Cex_t * pCex; @@ -673,14 +673,14 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in } // start the solver - p = Aig_GlaManStart( pAig, fNaiveCnf ); + p = Aig_Gla1ManStart( pAig, fNaiveCnf ); p->nFramesMax = nFramesMax; p->nConfLimit = nConfLimit; p->fVerbose = fVerbose; // include constant node Vec_IntWriteEntry( p->vIncluded, 0, 1 ); - Aig_GlaFetchVar( p, Aig_ManConst1(pAig), 0 ); + Aig_Gla1FetchVar( p, Aig_ManConst1(pAig), 0 ); // set runtime limit if ( TimeLimit ) @@ -692,16 +692,16 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in // initialize abstraction in this timeframe Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i ) if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) ) - if ( !Aig_GlaObjAddToSolver( p, pObj, f ) ) + if ( !Aig_Gla1ObjAddToSolver( p, pObj, f ) ) printf( "Error! SAT solver became UNSAT.\n" ); // create output literal to represent property failure pObj = Aig_ManPo( pAig, 0 ); - iSatVar = Aig_GlaFetchVar( p, Aig_ObjFanin0(pObj), f ); + iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f ); Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) ); // try solving the abstraction - Aig_GlaCollectAbstr( p ); + Aig_Gla1CollectAbstr( p ); for ( r = 0; r < 1000000; r++ ) { // try to find a counter-example @@ -730,9 +730,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in } clk = clock(); // derive abstraction - pAbs = Aig_GlaDeriveAbs( p ); + pAbs = Aig_Gla1DeriveAbs( p ); // derive counter-example - pCex = Aig_GlaDeriveCex( p, f ); + pCex = Aig_Gla1DeriveCex( p, f ); // verify the counter-example RetValue = Saig_ManVerifyCex( pAbs, pCex ); if ( RetValue == 0 ) @@ -746,7 +746,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 ); Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 ); for ( g = 0; g <= f; g++ ) - if ( !Aig_GlaObjAddToSolver( p, pObj, g ) ) + if ( !Aig_Gla1ObjAddToSolver( p, pObj, g ) ) printf( "Error! SAT solver became UNSAT.\n" ); } if ( Vec_IntSize(vPPiRefine) == 0 ) @@ -763,9 +763,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in p->timeRef += clock() - clk; // prepare abstraction - Aig_GlaCollectAbstr( p ); + Aig_Gla1CollectAbstr( p ); if ( fVerbose ) - Aig_GlaPrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef ); + Aig_Gla1PrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef ); } if ( RetValue != l_False ) break; @@ -786,9 +786,9 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in } // prepare return value if ( !fNaiveCnf && p->vIncluded ) - Aig_GlaExtendIncluded( p ); + Aig_Gla1ExtendIncluded( p ); vResult = p->vIncluded; p->vIncluded = NULL; - Aig_GlaManStop( p ); + Aig_Gla1ManStop( p ); return vResult; } diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c new file mode 100644 index 00000000..e18b6830 --- /dev/null +++ b/src/aig/saig/saigGlaPba.c @@ -0,0 +1,518 @@ +/**CFile**************************************************************** + + FileName [saigGlaPba.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Gate level abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "satSolver.h" +#include "satStore.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Aig_Gla2Man_t_ Aig_Gla2Man_t; +struct Aig_Gla2Man_t_ +{ + // user data + Aig_Man_t * pAig; + int nConfMax; + int nFramesMax; + int fVerbose; + // unrolling + Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID + Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID) + Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID + Vec_Int_t * vCla2Obj; // maps sat Var into its first clause + // SAT solver + sat_solver * pSat; + // statistics + int timePre; + int timeSat; + int timeTotal; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds constant to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_Gla2AddConst( sat_solver * pSat, int iVar, int fCompl ) +{ + lit Lit = toLitCond( iVar, fCompl ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds buffer to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_Gla2AddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) +{ + lit Lits[2]; + + Lits[0] = toLitCond( iVar0, 0 ); + Lits[1] = toLitCond( iVar1, !fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar0, 1 ); + Lits[1] = toLitCond( iVar1, fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds buffer to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_Gla2AddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) +{ + lit Lits[3]; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar0, fCompl0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar1, fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 0 ); + Lits[1] = toLitCond( iVar0, !fCompl0 ); + Lits[2] = toLitCond( iVar1, !fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + return 1; +} + + +/**Function************************************************************* + + Synopsis [Finds existing SAT variable or creates a new one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_Gla2FetchVar( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int k ) +{ + int i, iVecId, iSatVar; + assert( k < p->nFramesMax ); + iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); + if ( iVecId == 0 ) + { + iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax; + for ( i = 0; i < p->nFramesMax; i++ ) + Vec_IntPush( p->vVec2Var, 0 ); + Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId ); + } + iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k ); + if ( iSatVar == 0 ) + { + iSatVar = Vec_IntSize( p->vVar2Inf ) / 2; + Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) ); + Vec_IntPush( p->vVar2Inf, k ); + Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar ); + } + return iSatVar; +} + +/**Function************************************************************* + + Synopsis [Assigns variables to the AIG nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f ) +{ + int nVars = Vec_IntSize(p->vVar2Inf); + Aig_Gla2FetchVar( p, pObj, f ); + if ( nVars == Vec_IntSize(p->vVar2Inf) ) + return; + if ( Aig_ObjIsConst1(pObj) ) + return; + if ( Saig_ObjIsPo( p->pAig, pObj ) ) + { + Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); + return; + } + if ( Aig_ObjIsPi( pObj ) ) + { + if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 ) + Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); + Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f ); +} + +/**Function************************************************************* + + Synopsis [Creates SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p ) +{ + Vec_Int_t * vPoLits; + Aig_Obj_t * pObj; + int i, f, ObjId, nVars, RetValue = 1; + + // assign variables +// for ( f = p->nFramesMax - 1; f >= 0; f-- ) + for ( f = 0; f < p->nFramesMax; f++ ) + Aig_Gla2AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f ); + + // create SAT solver + p->pSat = sat_solver_new(); + sat_solver_store_alloc( p->pSat ); + sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 ); + + // add clauses + nVars = Vec_IntSize( p->vVar2Inf ); + Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i ) + { + if ( ObjId == -1 ) + continue; + pObj = Aig_ManObj( p->pAig, ObjId ); + if ( Aig_ObjIsNode(pObj) ) + { + RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f), + Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), + Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f), + Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) ); + Vec_IntPush( p->vCla2Obj, ObjId ); + Vec_IntPush( p->vCla2Obj, ObjId ); + Vec_IntPush( p->vCla2Obj, ObjId ); + } + else if ( Saig_ObjIsLo(p->pAig, pObj) ) + { + if ( f == 0 ) + { + RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 ); + Vec_IntPush( p->vCla2Obj, ObjId ); + } + else + { + Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); + RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), + Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1), + Aig_ObjFaninC0(pObjLi) ); + Vec_IntPush( p->vCla2Obj, ObjId ); + Vec_IntPush( p->vCla2Obj, ObjId ); + } + } + else if ( Saig_ObjIsPo(p->pAig, pObj) ) + { + RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), + Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), + Aig_ObjFaninC0(pObj) ); + Vec_IntPush( p->vCla2Obj, ObjId ); + Vec_IntPush( p->vCla2Obj, ObjId ); + } + else if ( Aig_ObjIsConst1(pObj) ) + { + RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 ); + Vec_IntPush( p->vCla2Obj, ObjId ); + } + else assert( Saig_ObjIsPi(p->pAig, pObj) ); + } + + // add output clause + vPoLits = Vec_IntAlloc( p->nFramesMax ); + for ( f = 0; f < p->nFramesMax; f++ ) + Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManPo(p->pAig, 0), f) ); + RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ); + Vec_IntFree( vPoLits ); + Vec_IntPush( p->vCla2Obj, 0 ); + + assert( nVars == Vec_IntSize(p->vVar2Inf) ); + assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) ); + + sat_solver_store_mark_roots( p->pSat ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Gla2Man_t * Aig_Gla2ManStart( Aig_Man_t * pAig, int nFramesMax ) +{ + Aig_Gla2Man_t * p; + int i; + + p = ABC_CALLOC( Aig_Gla2Man_t, 1 ); + p->pAig = pAig; + + p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) ); + p->vVec2Var = Vec_IntAlloc( 1 << 20 ); + p->vVar2Inf = Vec_IntAlloc( 1 << 20 ); + p->vCla2Obj = Vec_IntAlloc( 1 << 20 ); + + // skip first vector ID + p->nFramesMax = nFramesMax; + for ( i = 0; i < p->nFramesMax; i++ ) + Vec_IntPush( p->vVec2Var, -1 ); + + // skip first SAT variable + Vec_IntPush( p->vVar2Inf, -1 ); + Vec_IntPush( p->vVar2Inf, -1 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_Gla2ManStop( Aig_Gla2Man_t * p ) +{ + Vec_IntFreeP( &p->vObj2Vec ); + Vec_IntFreeP( &p->vVec2Var ); + Vec_IntFreeP( &p->vVar2Inf ); + Vec_IntFreeP( &p->vCla2Obj ); + + if ( p->pSat ) + sat_solver_delete( p->pSat ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Finds the set of clauses involved in the UNSAT core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue ) +{ + Vec_Int_t * vCore; + void * pSatCnf; + Intp_Man_t * pManProof; + int RetValue, clk = clock(); + if ( piRetValue ) + *piRetValue = -1; + // solve the problem + RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( RetValue == l_Undef ) + { + printf( "Conflict limit is reached.\n" ); + return NULL; + } + if ( RetValue == l_True ) + { + printf( "The BMC problem is SAT.\n" ); + if ( piRetValue ) + *piRetValue = 0; + return NULL; + } + if ( fVerbose ) + { + printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts ); + ABC_PRT( "Time", clock() - clk ); + } + assert( RetValue == l_False ); + pSatCnf = sat_solver_store_release( pSat ); + // derive the UNSAT core + clk = clock(); + pManProof = Intp_ManAlloc(); + vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 ); + Intp_ManFree( pManProof ); + Sto_ManFree( (Sto_Man_t *)pSatCnf ); + if ( fVerbose ) + { + printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), pSat->stats.clauses ); + ABC_PRT( "Time", clock() - clk ); + } + return vCore; +} + +/**Function************************************************************* + + Synopsis [Collects abstracted objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore ) +{ + Vec_Int_t * vResult; + Aig_Obj_t * pObj; + int i, ClaId; + vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); + Vec_IntWriteEntry( vResult, 0, 1 ); // add const1 + Vec_IntForEachEntry( vCore, ClaId, i ) + { + pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) ); + if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) ) + continue; + assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) ); + Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 ); + } + return vResult; +} + +/**Function************************************************************* + + Synopsis [Performs gate-level localization abstraction.] + + Description [Returns array of objects included in the abstraction. This array + may contain only const1, flop outputs, and internal nodes, that is, objects + that should have clauses added to the SAT solver.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ) +{ + int nStart = 0; + Aig_Gla2Man_t * p; + Vec_Int_t * vCore, * vResult; + int clk, clkTotal = clock(); + assert( Saig_ManPoNum(pAig) == 1 ); + + if ( fVerbose ) + { + if ( TimeLimit ) + printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit ); + else + printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax ); + } + + // start the solver + clk = clock(); + p = Aig_Gla2ManStart( pAig, nFramesMax ); + if ( !Aig_Gla2CreateSatSolver( p ) ) + { + printf( "Error! SAT solver became UNSAT.\n" ); + Aig_Gla2ManStop( p ); + return NULL; + } + p->timePre += clock() - clk; + + // set runtime limit + if ( TimeLimit ) + sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC ); + + // compute UNSAT core + clk = clock(); + vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL ); + if ( vCore == NULL ) + { + Aig_Gla2ManStop( p ); + return NULL; + } + p->timeSat += clock() - clk; + p->timeTotal = clock() - clkTotal; + + // print stats + if ( fVerbose ) + { + ABC_PRTP( "Pre ", p->timePre, p->timeTotal ); + ABC_PRTP( "Sat ", p->timeSat, p->timeTotal ); + ABC_PRTP( "Total ", p->timeTotal, p->timeTotal ); + } + + // prepare return value + vResult = Aig_Gla2ManCollect( p, vCore ); + Vec_IntFree( vCore ); + Aig_Gla2ManStop( p ); + return vResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |