diff options
-rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
-rw-r--r-- | src/aig/gia/giaAbs.c | 8 | ||||
-rw-r--r-- | src/aig/saig/module.make | 1 | ||||
-rw-r--r-- | src/aig/saig/saigGlaPba.c | 17 | ||||
-rw-r--r-- | src/aig/saig/saigGlaPba2.c | 558 | ||||
-rw-r--r-- | src/base/abci/abc.c | 11 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 350 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 50 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.h | 15 |
9 files changed, 766 insertions, 246 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index a79e12dd..c652f1a0 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -606,7 +606,7 @@ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Ce extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ); extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ); -extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ); +extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ); /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 165bc996..e9861977 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -424,9 +424,10 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) SeeAlso [] ***********************************************************************/ -int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ) +int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ) { extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ); + extern Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses; Gia_Man_t * pGiaAbs; @@ -447,7 +448,10 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ) } // perform abstraction - vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); + if ( fNewSolver ) + vGateClasses = Aig_Gla3ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); + else + vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); Aig_ManStop( pAig ); // update the BMC depth diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index df6fd7cb..cbd25a18 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -13,6 +13,7 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigDup.c \ src/aig/saig/saigGlaCba.c \ src/aig/saig/saigGlaPba.c \ + src/aig/saig/saigGlaPba2.c \ src/aig/saig/saigHaig.c \ src/aig/saig/saigInd.c \ src/aig/saig/saigIoa.c \ diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index 5834db76..cdbc05c7 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -432,11 +432,10 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo Vec_Int_t * vCore; void * pSatCnf; Intp_Man_t * pManProof; - int RetValue; + int RetValue, clk = clock(); if ( piRetValue ) *piRetValue = -1; // solve the problem - Abc_Clock(2,1); 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 ) { @@ -453,19 +452,19 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo if ( fVerbose ) { printf( "SAT solver returned UNSAT after %7d conflicts. ", pSat->stats.conflicts ); - ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC ); + Abc_PrintTime( 1, "Time", clock() - clk ); } assert( RetValue == l_False ); pSatCnf = sat_solver_store_release( pSat ); // derive the UNSAT core - Abc_Clock(2,1); + clk = clock(); pManProof = Intp_ManAlloc(); vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 ); Intp_ManFree( pManProof ); if ( fVerbose ) { - printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots ); - ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC ); + printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) ); + Abc_PrintTime( 1, "Time", clock() - clk ); } Sto_ManFree( (Sto_Man_t *)pSatCnf ); return vCore; @@ -561,7 +560,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in int clk, clk2 = clock(); assert( Saig_ManPoNum(pAig) == 1 ); - Abc_Clock(0,1); if ( fVerbose ) { if ( TimeLimit ) @@ -572,7 +570,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in // start the solver clk = clock(); - Abc_Clock(1,1); p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose ); if ( !Aig_Gla2CreateSatSolver( p ) ) { @@ -581,7 +578,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in return NULL; } sat_solver_set_random( p->pSat, fSkipRand ); -// p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; p->timePre += clock() - clk; // set runtime limit @@ -590,15 +586,12 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in // compute UNSAT core clk = clock(); - Abc_Clock(1,1); vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL ); if ( vCore == NULL ) { Aig_Gla2ManStop( p ); return NULL; } -// p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC; -// p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC; p->timeSat += clock() - clk; p->timeTotal += clock() - clk2; diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c new file mode 100644 index 00000000..8de5fb32 --- /dev/null +++ b/src/aig/saig/saigGlaPba2.c @@ -0,0 +1,558 @@ +/**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 "satSolver2.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Aig_Gla3Man_t_ Aig_Gla3Man_t; +struct Aig_Gla3Man_t_ +{ + // user data + Aig_Man_t * pAig; + int nStart; + 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 + // clause mapping + Vec_Int_t * vCla2Obj; // maps clause into its root object + Vec_Int_t * vCla2Fra; // maps clause into its frame + Vec_Int_t * vVec2Use; // maps vec ID into its used frames (nFrames per vec ID) + // SAT solver + sat_solver2 * pSat; + // statistics + int timePre; + int timeSat; + int timeTotal; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define ABC_CPS 1000 + +/**Function************************************************************* + + Synopsis [Adds constant to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_Gla3AddConst( sat_solver2 * pSat, int iVar, int fCompl ) +{ + lit Lit = toLitCond( iVar, fCompl ); + if ( !sat_solver2_addclause( pSat, &Lit, &Lit + 1 ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds buffer to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_Gla3AddBuffer( sat_solver2 * pSat, int iVar0, int iVar1, int fCompl ) +{ + lit Lits[2]; + + Lits[0] = toLitCond( iVar0, 0 ); + Lits[1] = toLitCond( iVar1, !fCompl ); + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar0, 1 ); + Lits[1] = toLitCond( iVar1, fCompl ); + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds buffer to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_Gla3AddNode( sat_solver2 * 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_solver2_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar1, fCompl1 ); + if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 0 ); + Lits[1] = toLitCond( iVar0, !fCompl0 ); + Lits[2] = toLitCond( iVar1, !fCompl1 ); + if ( !sat_solver2_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_Gla3FetchVar( Aig_Gla3Man_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_Gla3AssignVars_rec( Aig_Gla3Man_t * p, Aig_Obj_t * pObj, int f ) +{ + int nVars = Vec_IntSize(p->vVar2Inf); + Aig_Gla3FetchVar( p, pObj, f ); + if ( nVars == Vec_IntSize(p->vVar2Inf) ) + return; + if ( Aig_ObjIsConst1(pObj) ) + return; + if ( Saig_ObjIsPo( p->pAig, pObj ) ) + { + Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); + return; + } + if ( Aig_ObjIsPi( pObj ) ) + { + if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 ) + Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); + Aig_Gla3AssignVars_rec( p, Aig_ObjFanin1(pObj), f ); +} + +/**Function************************************************************* + + Synopsis [Creates SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_Gla3CreateSatSolver( Aig_Gla3Man_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-- ) + Aig_Gla3AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f ); + + // create SAT solver + p->pSat = sat_solver2_new(); + sat_solver2_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) ) + { + Aig_Gla3AddNode( p->pSat, Aig_Gla3FetchVar(p, pObj, f), + Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObj), f), + Aig_Gla3FetchVar(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 ); + + Vec_IntPush( p->vCla2Fra, f ); + Vec_IntPush( p->vCla2Fra, f ); + Vec_IntPush( p->vCla2Fra, f ); + } + else if ( Saig_ObjIsLo(p->pAig, pObj) ) + { + if ( f == 0 ) + { + Aig_Gla3AddConst( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 1 ); + Vec_IntPush( p->vCla2Obj, ObjId ); + + Vec_IntPush( p->vCla2Fra, f ); + } + else + { + Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); + Aig_Gla3AddBuffer( p->pSat, Aig_Gla3FetchVar(p, pObj, f), + Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObjLi), f-1), + Aig_ObjFaninC0(pObjLi) ); + Vec_IntPush( p->vCla2Obj, ObjId ); + Vec_IntPush( p->vCla2Obj, ObjId ); + + Vec_IntPush( p->vCla2Fra, f ); + Vec_IntPush( p->vCla2Fra, f ); + } + } + else if ( Saig_ObjIsPo(p->pAig, pObj) ) + { + Aig_Gla3AddBuffer( p->pSat, Aig_Gla3FetchVar(p, pObj, f), + Aig_Gla3FetchVar(p, Aig_ObjFanin0(pObj), f), + Aig_ObjFaninC0(pObj) ); + Vec_IntPush( p->vCla2Obj, ObjId ); + Vec_IntPush( p->vCla2Obj, ObjId ); + + Vec_IntPush( p->vCla2Fra, f ); + Vec_IntPush( p->vCla2Fra, f ); + } + else if ( Aig_ObjIsConst1(pObj) ) + { + Aig_Gla3AddConst( p->pSat, Aig_Gla3FetchVar(p, pObj, f), 0 ); + Vec_IntPush( p->vCla2Obj, ObjId ); + + Vec_IntPush( p->vCla2Fra, f ); + } + else assert( Saig_ObjIsPi(p->pAig, pObj) ); + } + + // add output clause + vPoLits = Vec_IntAlloc( p->nFramesMax ); + for ( f = p->nStart; f < p->nFramesMax; f++ ) + Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManPo(p->pAig, 0), f) ); + sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ); + Vec_IntFree( vPoLits ); + Vec_IntPush( p->vCla2Obj, 0 ); + Vec_IntPush( p->vCla2Fra, 0 ); + assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) ); + assert( nVars == Vec_IntSize(p->vVar2Inf) ); + assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses ); + if ( p->fVerbose ) + printf( "The resulting SAT problem contains %d variables and %d clauses.\n", + p->pSat->size, p->pSat->stats.clauses ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Gla3Man_t * Aig_Gla3ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, int fVerbose ) +{ + Aig_Gla3Man_t * p; + int i; + + p = ABC_CALLOC( Aig_Gla3Man_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 ); + p->vCla2Fra = Vec_IntAlloc( 1 << 20 ); + + // skip first vector ID + p->nStart = nStart; + p->nFramesMax = nFramesMax; + p->fVerbose = fVerbose; + 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_Gla3ManStop( Aig_Gla3Man_t * p ) +{ + Vec_IntFreeP( &p->vObj2Vec ); + Vec_IntFreeP( &p->vVec2Var ); + Vec_IntFreeP( &p->vVar2Inf ); + Vec_IntFreeP( &p->vCla2Obj ); + Vec_IntFreeP( &p->vCla2Fra ); + Vec_IntFreeP( &p->vVec2Use ); + + if ( p->pSat ) + sat_solver2_delete( p->pSat ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Finds the set of clauses involved in the UNSAT core.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_Gla3ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue ) +{ + Vec_Int_t * vCore; + int RetValue, clk = clock(); + if ( piRetValue ) + *piRetValue = -1; + // solve the problem + RetValue = sat_solver2_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 %7d conflicts. ", pSat->stats.conflicts ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } + assert( RetValue == l_False ); + + // derive the UNSAT core + clk = clock(); + vCore = Sat_ProofCore( pSat ); + if ( fVerbose ) + { + printf( "SAT core contains %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } + return vCore; +} + +/**Function************************************************************* + + Synopsis [Collects abstracted objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Aig_Gla3ManCollect( Aig_Gla3Man_t * p, Vec_Int_t * vCore ) +{ + Vec_Int_t * vResult; + Aig_Obj_t * pObj; + int i, ClaId, iVecId; +// p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) ); + + 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) || Aig_ObjIsConst1(pObj) ) + continue; + assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) ); + Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 ); + if ( p->vVec2Use ) + { + iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); + Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 ); + } + } + // count the number of objects in each frame + if ( p->vVec2Use ) + { + Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax ); + int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax; + for ( f = 0; f < p->nFramesMax; f++ ) + for ( v = 0; v < nVecIds; v++ ) + if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) ) + Vec_IntAddToEntry( vCounts, f, 1 ); + Vec_IntForEachEntry( vCounts, Entry, f ) + printf( "%d ", Entry ); + printf( "\n" ); + Vec_IntFree( vCounts ); + } + 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_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ) +{ + Aig_Gla3Man_t * p; + Vec_Int_t * vCore, * vResult; + int nTimeToStop = time(NULL) + TimeLimit; + int clk, clk2 = 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_Gla3ManStart( pAig, nStart, nFramesMax, fVerbose ); + if ( !Aig_Gla3CreateSatSolver( p ) ) + { + printf( "Error! SAT solver became UNSAT.\n" ); + Aig_Gla3ManStop( p ); + return NULL; + } + sat_solver2_set_random( p->pSat, fSkipRand ); + p->timePre += clock() - clk; + + // set runtime limit + if ( TimeLimit ) + sat_solver2_set_runtime_limit( p->pSat, nTimeToStop ); + + // compute UNSAT core + clk = clock(); + vCore = Aig_Gla3ManUnsatCore( p->pSat, nConfLimit, fVerbose, NULL ); + if ( vCore == NULL ) + { + Aig_Gla3ManStop( p ); + return NULL; + } + p->timeSat += clock() - clk; + p->timeTotal += clock() - clk2; + + // 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_Gla3ManCollect( p, vCore ); + Vec_IntFree( vCore ); + Aig_Gla3ManStop( p ); + return vResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index daf92b1b..2050d985 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29093,13 +29093,14 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) { Saig_ParBmc_t Pars, * pPars = &Pars; int c; + int fNewSolver = 0; Saig_ParBmcSetDefaultParams( pPars ); pPars->nStart = 0; pPars->nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 10; pPars->nConfLimit = 0; pPars->fSkipRand = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrnvh" ) ) != EOF ) { switch ( c ) { @@ -29150,6 +29151,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': pPars->fSkipRand ^= 1; break; + case 'n': + fNewSolver ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -29186,20 +29190,21 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pPars->nStart ) Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" ); - pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars ); + pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars, fNewSolver ); // if ( pPars->nStart == 0 ) pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rvh]\n" ); + Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rnvh]\n" ); Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-r : toggle using random decisiont during SAT solving [default = %s]\n", !pPars->fSkipRand? "yes": "no" ); + Abc_Print( -2, "\t-n : toggle using on-the-fly proof-logging [default = %s]\n", fNewSolver? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index f817ab3d..d51df229 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -66,7 +66,7 @@ static inline void Rec_IntPush( Rec_Int_t * p, int Entry ) { if ( (p->nSize >> p->nShift) == Vec_PtrSize(p->vPages) ) Vec_PtrPush( p->vPages, ABC_ALLOC(int, p->Mask+1) ); - ((int*)p->vPages->pArray[p->nSize >> p->nShift])[p->nSize++ & p->Mask] = Entry; + ((int*)Vec_PtrEntry(p->vPages, p->nSize >> p->nShift))[p->nSize++ & p->Mask] = Entry; } static inline void Rec_IntAppend( Rec_Int_t * p, int * pArray, int nSize ) { @@ -79,7 +79,7 @@ static inline void Rec_IntAppend( Rec_Int_t * p, int * pArray, int nSize ) if ( (p->nSize >> p->nShift) == Vec_PtrSize(p->vPages) ) Vec_PtrPush( p->vPages, ABC_ALLOC(int, p->Mask+1) ); // assert( (p->nSize >> p->nShift) + 1 == Vec_PtrSize(p->vPages) ); - memmove( (int*)p->vPages->pArray[p->nSize >> p->nShift] + (p->nSize & p->Mask), pArray, sizeof(int) * nSize ); + memmove( (int*)Vec_PtrEntry(p->vPages, p->nSize >> p->nShift) + (p->nSize & p->Mask), pArray, sizeof(int) * nSize ); p->nLast = p->nSize; p->nSize += nSize; } @@ -357,149 +357,6 @@ Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hR - -/**Function************************************************************* - - Synopsis [Collects nodes belonging to the UNSAT core.] - - Description [The result is the array of root clause indexes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed ) -{ - Vec_Int_t * vCore; - satset * pNode, * pFanin; - int i, k, clk = clock(); - vCore = Vec_IntAlloc( 1000 ); - Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - { - pNode->Id = 0; - Proof_NodeForeachLeaf( vClauses, pNode, pFanin, k ) - if ( pFanin && !pFanin->mark ) - { - pFanin->mark = 1; - Vec_IntPush( vCore, Proof_NodeHandle(vClauses, pFanin) ); - } - } - // clean core clauses - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) - pNode->mark = 0; - return vCore; -} - - -/**Function************************************************************* - - Synopsis [Computes UNSAT core.] - - Description [The result is the array of root clause indexes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Sat_ProofCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hNode ) -{ - Vec_Int_t * vCore, * vUsed; - // collect visited clauses - vUsed = Proof_CollectUsedIter( vProof, NULL, hNode ); - // collect core clauses - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); - Vec_IntFree( vUsed ); - return vCore; -} - -/**Function************************************************************* - - Synopsis [Computes interpolant of the proof.] - - Description [Aassuming that vars/clause of partA are marked.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hNode, Vec_Int_t * vGlobVars ) -{ - Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; - satset * pNode, * pFanin; - Aig_Man_t * pAig; - Aig_Obj_t * pObj; - int i, k, iVar, Entry; - - // collect visited nodes - vUsed = Proof_CollectUsedIter( vProof, NULL, hNode ); - // collect core clauses (cleans vUsed and vCore) - vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); - - // map variables into their global numbers - vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 ); - Vec_IntForEachEntry( vGlobVars, Entry, i ) - Vec_IntWriteEntry( vVarMap, Entry, i ); - - // start the AIG - pAig = Aig_ManStart( 10000 ); - pAig->pName = Aig_UtilStrsav( "interpol" ); - for ( i = 0; i < Vec_IntSize(vGlobVars); i++ ) - Aig_ObjCreatePi( pAig ); - - // copy the numbers out and derive interpol for clause - vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) - { - if ( pNode->partA ) - { - pObj = Aig_ManConst0( pAig ); - satset_foreach_var( pNode, iVar, k, 0 ) - if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 ) - pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) ); - } - else - pObj = Aig_ManConst1( pAig ); - // remember the interpolant - Vec_IntPush( vCoreNums, pNode->Id ); - pNode->Id = Aig_ObjToLit(pObj); - } - Vec_IntFree( vVarMap ); - - // copy the numbers out and derive interpol for resolvents - Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - { - assert( pNode->nEnts > 1 ); - Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) - { - if ( k == 0 ) - pObj = Aig_ObjFromLit( pAig, pFanin->Id ); - else if ( pNode->pEnts[k] & 2 ) // variable of A - pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); - else - pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); - } - // remember the interpolant - pNode->Id = Aig_ObjToLit(pObj); - } - // save the result - assert( Proof_NodeHandle(vProof, pNode) == hNode ); - Aig_ObjCreatePo( pAig, pObj ); - Aig_ManCleanup( pAig ); - - // move the results back - Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) - pNode->Id = Vec_IntEntry( vCoreNums, i ); - Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) - pNode->Id = 0; - // cleanup - Vec_IntFree( vCore ); - Vec_IntFree( vUsed ); - Vec_IntFree( vCoreNums ); - return pAig; -} /**Function************************************************************* @@ -512,11 +369,12 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int SeeAlso [] ***********************************************************************/ -void Sat_ProofReduce( veci * pProof, veci * pRoots ) +void Sat_ProofReduce( sat_solver2 * s ) { + Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Int_t * vRoots = (Vec_Int_t *)&s->claProofs; + int fVerbose = 0; - Vec_Int_t * vProof = (Vec_Int_t *)pProof; - Vec_Int_t * vRoots = (Vec_Int_t *)pRoots; Vec_Int_t * vUsed; satset * pNode, * pFanin; int i, k, hTemp, hNewHandle = 1, clk = clock(); @@ -575,7 +433,7 @@ void Sat_ProofReduce( veci * pProof, veci * pRoots ) SeeAlso [] ***********************************************************************/ -satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) +satset * Sat_ProofCheckResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) { satset * c; int i, k, hNode, Var = -1, Count = 0; @@ -627,7 +485,7 @@ satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * SeeAlso [] ***********************************************************************/ -satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) +satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt ) { satset * pAnt; if ( iAnt & 1 ) @@ -649,14 +507,13 @@ satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t SeeAlso [] ***********************************************************************/ -void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) +void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) { Vec_Int_t * vUsed, * vResolves, * vTemp; satset * pSet, * pSet0, * pSet1; int i, k, Counter = 0, clk = clock(); // collect visited clauses - vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); -// vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); Proof_CleanCollected( vProof, vUsed ); // perform resolution steps vTemp = Vec_IntAlloc( 1000 ); @@ -664,11 +521,11 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) Vec_IntPush( vResolves, -1 ); Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) { - pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); + pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); for ( k = 1; k < (int)pSet->nEnts; k++ ) { - pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); - pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1, vTemp ); + pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); + pSet0 = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp ); } pSet->Id = Proof_NodeHandle( vResolves, pSet0 ); //printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) ); @@ -703,7 +560,7 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) SeeAlso [] ***********************************************************************/ -satset * Proof_ResolveOne( Rec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) +satset * Sat_ProofCheckResolveOne( Rec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp ) { satset * c; int i, k, Var = -1, Count = 0; @@ -754,7 +611,7 @@ satset * Proof_ResolveOne( Rec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * SeeAlso [] ***********************************************************************/ -satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Rec_Int_t * vResolves, int iAnt ) +satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Rec_Int_t * vResolves, int iAnt ) { satset * pAnt; if ( iAnt & 1 ) @@ -776,14 +633,17 @@ satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Rec_Int_t SeeAlso [] ***********************************************************************/ -void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) +void Sat_ProofCheck( sat_solver2 * s ) { + Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; + Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id]; + Rec_Int_t * vResolves; Vec_Int_t * vUsed, * vTemp; satset * pSet, * pSet0, * pSet1; int i, k, Counter = 0, clk = clock(); // collect visited clauses -// vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); Proof_CleanCollected( vProof, vUsed ); // perform resolution steps @@ -792,11 +652,11 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) Rec_IntPush( vResolves, -1 ); Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) { - pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); + pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); for ( k = 1; k < (int)pSet->nEnts; k++ ) { - pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); - pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1, vTemp ); + pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] ); + pSet0 = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp ); } pSet->Id = Rec_IntSizeLast( vResolves ); //printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) ); @@ -818,52 +678,162 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) Vec_IntFree( vUsed ); } +/**Function************************************************************* + + Synopsis [Collects nodes belonging to the UNSAT core.] + + Description [The resulting array contains 0-based IDs of root clauses.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed ) +{ + Vec_Int_t * vCore; + satset * pNode, * pFanin; + int i, k, clk = clock(); + vCore = Vec_IntAlloc( 1000 ); + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + { + pNode->Id = 0; + Proof_NodeForeachLeaf( vClauses, pNode, pFanin, k ) + if ( pFanin && !pFanin->mark ) + { + pFanin->mark = 1; + Vec_IntPush( vCore, Proof_NodeHandle(vClauses, pFanin) ); + } + } + // clean core clauses and reexpress core in terms of clause IDs + Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + { + pNode->mark = 0; + Vec_IntWriteEntry( vCore, i, pNode->Id - 1 ); + } + return vCore; +} + /**Function************************************************************* Synopsis [Computes interpolant of the proof.] - Description [Aassuming that global vars and A-clauses are marked.] + Description [Aassuming that vars/clause of partA are marked.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot ) +void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) { - Vec_Int_t * vClauses = (Vec_Int_t *)pClauses; - Vec_Int_t * vProof = (Vec_Int_t *)pProof; - Vec_Int_t * vRoots = (Vec_Int_t *)pRoots; -// Vec_Int_t * vUsed, * vCore; -// int i, Entry; -/* - // collect visited clauses - vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); - Proof_CleanCollected( vProof, vUsed ); - printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); - Vec_IntFree( vUsed ); -*/ -/* - // collect visited clauses + Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; + Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; + int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id]; + + Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; + satset * pNode, * pFanin; + Aig_Man_t * pAig; + Aig_Obj_t * pObj; + int i, k, iVar, Entry; + + // collect visited nodes vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); - Proof_CleanCollected( vProof, vUsed ); - printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); - Vec_IntFree( vUsed ); + // collect core clauses (cleans vUsed and vCore) + vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); + + // map variables into their global numbers + vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 ); + Vec_IntForEachEntry( vGlobVars, Entry, i ) + Vec_IntWriteEntry( vVarMap, Entry, i ); + + // start the AIG + pAig = Aig_ManStart( 10000 ); + pAig->pName = Aig_UtilStrsav( "interpol" ); + for ( i = 0; i < Vec_IntSize(vGlobVars); i++ ) + Aig_ObjCreatePi( pAig ); + + // copy the numbers out and derive interpol for clause + vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); + Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + { + if ( pNode->partA ) + { + pObj = Aig_ManConst0( pAig ); + satset_foreach_var( pNode, iVar, k, 0 ) + if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 ) + pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) ); + } + else + pObj = Aig_ManConst1( pAig ); + // remember the interpolant + Vec_IntPush( vCoreNums, pNode->Id ); + pNode->Id = Aig_ObjToLit(pObj); + } + Vec_IntFree( vVarMap ); - vCore = Sat_ProofCore( vClauses, vProof, hRoot ); + // copy the numbers out and derive interpol for resolvents + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + { + assert( pNode->nEnts > 1 ); + Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) + { + if ( k == 0 ) + pObj = Aig_ObjFromLit( pAig, pFanin->Id ); + else if ( pNode->pEnts[k] & 2 ) // variable of A + pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); + else + pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); + } + // remember the interpolant + pNode->Id = Aig_ObjToLit(pObj); + } + // save the result + assert( Proof_NodeHandle(vProof, pNode) == hRoot ); + Aig_ObjCreatePo( pAig, pObj ); + Aig_ManCleanup( pAig ); + + // move the results back + Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + pNode->Id = Vec_IntEntry( vCoreNums, i ); + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + pNode->Id = 0; + // cleanup Vec_IntFree( vCore ); -*/ -/* - printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); Vec_IntFree( vUsed ); - vUsed = Proof_CollectAll( vProof ); - printf( "Found %d total resolution nodes.\n", Vec_IntSize(vUsed) ); + Vec_IntFree( vCoreNums ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [Computes UNSAT core.] + + Description [The result is the array of root clause indexes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Sat_ProofCore( sat_solver2 * s ) +{ + Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; + Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id]; + + Vec_Int_t * vCore, * vUsed; + // collect visited clauses + vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + // collect core clauses + vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed ); Vec_IntFree( vUsed ); -*/ - Proof_Check( vClauses, vProof, hRoot ); + return vCore; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 8fdc2ecb..fab5e7da 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -28,7 +28,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_IMPL_START - #define SAT_USE_ANALYZE_FINAL #define SAT_USE_PROOF_LOGGING @@ -369,7 +368,7 @@ static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc //================================================================================================= // Clause functions: -static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id) +static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id) { satset* c; int i, Cid, nLits = end - begin; @@ -516,7 +515,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id) { lit* begin = veci_begin(cls); lit* end = begin + veci_size(cls); - int Cid = clause_new(s,begin,end,1, proof_id); + int Cid = clause_create_new(s,begin,end,1, proof_id); assert(veci_size(cls) > 0); if ( veci_size(cls) == 1 ) { @@ -888,6 +887,7 @@ satset* solver2_propagate(sat_solver2* s) veci* ws; lit* lits, false_lit, p, * stop, * k; cla* begin,* end, *i, *j; + int Lit; while (confl == 0 && s->qtail - s->qhead > 0){ @@ -926,9 +926,10 @@ satset* solver2_propagate(sat_solver2* s) } // Did not find watch -- clause is unit under assignment: + Lit = lits[0]; if (s->fProofLogging && solver2_dlevel(s) == 0){ - int k, x, proof_id, Cid, Var = lit_var(lits[0]); - int fLitIsFalse = (var_value(s, Var) == !lit_sign(lits[0])); + int k, x, proof_id, Cid, Var = lit_var(Lit); + int fLitIsFalse = (var_value(s, Var) == !lit_sign(Lit)); // Log production of top-level unit clause: proof_chain_start( s, c ); satset_foreach_var( c, x, k, 1 ){ @@ -937,7 +938,7 @@ satset* solver2_propagate(sat_solver2* s) } proof_id = proof_chain_stop( s ); // get a new clause - Cid = clause_new( s, lits, lits + 1, 1, proof_id ); + Cid = clause_create_new( s, &Lit, &Lit + 1, 1, proof_id ); assert( (var_unit_clause(s, Var) == NULL) != fLitIsFalse ); // if variable already has unit clause, it must be with the other polarity // in this case, we should derive the empty clause here @@ -948,13 +949,13 @@ satset* solver2_propagate(sat_solver2* s) proof_chain_start( s, clause_read(s,Cid) ); proof_chain_resolve( s, NULL, Var ); proof_id = proof_chain_stop( s ); - clause_new( s, lits, lits, 1, proof_id ); + clause_create_new( s, &Lit, &Lit, 1, proof_id ); } } *j++ = *i; // Clause is unit under assignment: - if (!solver2_enqueue(s,lits[0], *i)){ + if (!solver2_enqueue(s,Lit, *i)){ confl = clause_read(s,*i++); // Copy the remaining watches: while (i < end) @@ -1275,16 +1276,17 @@ void sat_solver2_setnvars(sat_solver2* s,int n) void sat_solver2_delete(sat_solver2* s) { - satset * c = clause_read(s, s->hLearntLast); +// veci * pCore; // report statistics printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits ); +/* + pCore = Sat_ProofCore( s ); + printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); + veci_delete( pCore ); + ABC_FREE( pCore ); - Sat_ProofTest( - &s->clauses, // clauses - &s->proofs, // proof clauses - NULL, // proof roots - veci_begin(&s->claProofs)[c->Id] // one root - ); +*/ +// Sat_ProofCheck( s ); // delete vectors veci_delete(&s->order); @@ -1308,10 +1310,7 @@ void sat_solver2_delete(sat_solver2* s) int i; if ( s->wlists ) for (i = 0; i < s->size*2; i++) - { -// printf( "%d ", s->wlists[i].size ); veci_delete(&s->wlists[i]); - } ABC_FREE(s->wlists ); ABC_FREE(s->vi ); ABC_FREE(s->trail ); @@ -1375,7 +1374,7 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) return solver2_enqueue(s,*begin,0); // create new clause - return clause_new(s,begin,j,0,0); + return clause_create_new(s,begin,j,0,0); } int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) @@ -1404,21 +1403,17 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end) sat_solver2_setnvars(s,maxvar+1); // create a new clause - Cid = clause_new( s, begin, end, 0, 0 ); + Cid = clause_create_new( s, begin, end, 0, 0 ); // handle unit clause if ( begin + 1 == end ) { - printf( "Adding unit clause %d\n", begin[0] ); +// printf( "Adding unit clause %d\n", begin[0] ); // solver2_canceluntil(s, 0); if ( s->fProofLogging ) var_set_unit_clause( s, lit_var(begin[0]), Cid ); if ( !solver2_enqueue(s,begin[0],0) ) assert( 0 ); } - - // count literals - s->stats.clauses++; - s->stats.clauses_literals += end - begin; return Cid; } @@ -1447,7 +1442,6 @@ void luby2_test() // updates clauses, watches, units, and proof void solver2_reducedb(sat_solver2* s) { - extern void Sat_ProofReduce( veci * pProof, veci * pRoots ); satset * c; cla h,* pArray,* pArray2; int Counter = 0, CounterStart = s->stats.learnts * 3 / 4; // 2/3; @@ -1504,7 +1498,7 @@ void solver2_reducedb(sat_solver2* s) s->stats.learnts = veci_size(&s->learnt_live); // compact proof (compacts 'proofs' and update 'claProofs') - Sat_ProofReduce( &s->proofs, &s->claProofs ); + Sat_ProofReduce( s ); TimeTotal += clock() - clk; Abc_PrintTime( 1, "Time", TimeTotal ); @@ -1658,7 +1652,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim // reduce the set of learnt clauses: if (nof_learnts > 0 && s->stats.learnts > nof_learnts) { - solver2_reducedb(s); +// solver2_reducedb(s); nof_learnts = nof_learnts * 11 / 10; } // perform next run diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 2e745bc2..137f1968 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -59,14 +59,6 @@ extern void sat_solver2TraceStart( sat_solver2 * pSat, char * pName ); extern void sat_solver2TraceStop( sat_solver2 * pSat ); extern void sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot ); -// clause storage -extern void sat_solver2_store_alloc( sat_solver2 * s ); -extern void sat_solver2_store_write( sat_solver2 * s, char * pFileName ); -extern void sat_solver2_store_free( sat_solver2 * s ); -extern void sat_solver2_store_mark_roots( sat_solver2 * s ); -extern void sat_solver2_store_mark_clauses_a( sat_solver2 * s ); -extern void * sat_solver2_store_release( sat_solver2 * s ); - // global variables extern int var_is_partA (sat_solver2* s, int v); extern void var_set_partA(sat_solver2* s, int v, int partA); @@ -76,6 +68,11 @@ extern void clause_set_partA(sat_solver2* s, int handle, int partA); // other clause functions extern int clause_id(sat_solver2* s, int h); +// proof-based APIs +extern void * Sat_ProofCore( sat_solver2 * s ); +extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ); +extern void Sat_ProofReduce( sat_solver2 * s ); +extern void Sat_ProofCheck( sat_solver2 * s ); //================================================================================================= // Solver representation: @@ -247,8 +244,6 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) return fNotUseRandomOld; } -extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot ); - ABC_NAMESPACE_HEADER_END #endif |