/**CFile**************************************************************** FileName [pdrInt.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [Property driven reachability.] Synopsis [Internal declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - November 20, 2010.] Revision [$Id: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef ABC__sat__pdr__pdrInt_h #define ABC__sat__pdr__pdrInt_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include "aig/saig/saig.h" #include "misc/vec/vecWec.h" #include "sat/cnf/cnf.h" #include "pdr.h" #include "misc/hash/hashInt.h" #include "aig/gia/giaAig.h" //#define PDR_USE_SATOKO 1 #ifndef PDR_USE_SATOKO #include "sat/bsat/satSolver.h" #else #include "sat/satoko/satoko.h" #include "sat/satoko/solver.h" #define l_Undef 0 #define l_True 1 #define l_False -1 #define sat_solver satoko_t #define sat_solver_new satoko_create #define sat_solver_delete satoko_destroy #define zsat_solver_new_seed(s) satoko_create() #define zsat_solver_restart_seed(s,a) satoko_reset(s) #define sat_solver_nvars solver_varnum #define sat_solver_setnvars satoko_setnvars #define sat_solver_addclause(s,b,e) satoko_add_clause(s,b,e-b) #define sat_solver_final satoko_final_conflict #define sat_solver_solve(s,b,e,c,x,y,z) satoko_solve_assumptions_limit(s,b,e-b,(int)c) #define sat_solver_var_value solver_read_cex_varvalue #define sat_solver_set_runtime_limit solver_set_runtime_limit #define sat_solver_compress(s) #endif ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// typedef struct Txs_Man_t_ Txs_Man_t; typedef struct Txs3_Man_t_ Txs3_Man_t; typedef struct Pdr_Set_t_ Pdr_Set_t; struct Pdr_Set_t_ { word Sign; // signature int nRefs; // ref counter int nTotal; // total literals int nLits; // num flop literals int Lits[0]; }; typedef struct Pdr_Obl_t_ Pdr_Obl_t; struct Pdr_Obl_t_ { int iFrame; // time frame int prio; // priority int nRefs; // reference counter Pdr_Set_t * pState; // state cube Pdr_Obl_t * pNext; // next one Pdr_Obl_t * pLink; // queue link }; typedef struct Pdr_Man_t_ Pdr_Man_t; struct Pdr_Man_t_ { // input problem Pdr_Par_t * pPars; // parameters Aig_Man_t * pAig; // user's AIG Gia_Man_t * pGia; // user's AIG // static CNF representation Cnf_Man_t * pCnfMan; // CNF manager Cnf_Dat_t * pCnf1; // CNF for this AIG Vec_Int_t * vVar2Reg; // mapping of SAT var into registers // dynamic CNF representation Cnf_Dat_t * pCnf2; // CNF for this AIG Vec_Int_t * pvId2Vars; // for each used ObjId, maps frame into SAT var Vec_Ptr_t vVar2Ids; // for each used frame, maps SAT var into ObjId Vec_Wec_t * vVLits; // CNF literals // data representation int iOutCur; // current output int nPrioShift;// priority shift Vec_Ptr_t * vCexes; // counter-examples for each output Vec_Ptr_t * vSolvers; // SAT solvers Vec_Vec_t * vClauses; // clauses by timeframe Pdr_Obl_t * pQueue; // proof obligations int * pOrder; // ordering of the lits Vec_Int_t * vActVars; // the counter of activation variables int iUseFrame; // the first used frame int nAbsFlops; // the number of flops used Vec_Int_t * vAbsFlops; // flops currently used Vec_Int_t * vMapFf2Ppi; Vec_Int_t * vMapPpi2Ff; int nCexes; int nCexesTotal; // terminary simulation Txs3_Man_t * pTxs3; // internal use Vec_Int_t * vPrio; // priority flops Vec_Int_t * vLits; // array of literals Vec_Int_t * vCiObjs; // cone leaves Vec_Int_t * vCoObjs; // cone roots Vec_Int_t * vCiVals; // cone leaf values Vec_Int_t * vCoVals; // cone root values Vec_Int_t * vNodes; // cone nodes Vec_Int_t * vUndo; // cone undos Vec_Int_t * vVisits; // intermediate Vec_Int_t * vCi2Rem; // CIs to be removed Vec_Int_t * vRes; // final result abctime * pTime4Outs;// timeout per output Vec_Ptr_t * vInfCubes; // infinity clauses/cubes // statistics int nBlocks; // the number of times blockState was called int nObligs; // the number of proof obligations derived int nCubes; // the number of cubes derived int nCalls; // the number of SAT calls int nCallsS; // the number of SAT calls (sat) int nCallsU; // the number of SAT calls (unsat) int nStarts; // the number of SAT solver restarts int nFrames; // frames explored int nCasesSS; int nCasesSU; int nCasesUS; int nCasesUU; int nQueCur; int nQueMax; int nQueLim; int nXsimRuns; int nXsimLits; // runtime abctime timeToStop; abctime timeToStopOne; // time stats abctime tSat; abctime tSatSat; abctime tSatUnsat; abctime tGeneral; abctime tPush; abctime tTsim; abctime tContain; abctime tCnf; abctime tAbs; abctime tTotal; }; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); } static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p ) { if ( p->timeToStop == 0 ) return p->timeToStopOne; if ( p->timeToStopOne == 0 ) return p->timeToStop; if ( p->timeToStop < p->timeToStopOne ) return p->timeToStop; return p->timeToStopOne; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== pdrCnf.c ==========================================================*/ extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj ); extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar ); extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k ); extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit ); /*=== pdrCore.c ==========================================================*/ extern int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet ); /*=== pdrInv.c ==========================================================*/ extern Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p ); extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ); extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ); extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ); extern Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ); extern void Pdr_ManReportInvariant( Pdr_Man_t * p ); extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p ); extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ); /*=== pdrMan.c ==========================================================*/ extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit ); extern void Pdr_ManStop( Pdr_Man_t * p ); extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); extern Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ); /*=== pdrSat.c ==========================================================*/ extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ); extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ); extern void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ); extern Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext ); extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray ); extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues ); extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit ); /*=== pdrTsim.c ==========================================================*/ extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); /*=== pdrTsim2.c ==========================================================*/ extern Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio ); extern void Txs_ManStop( Txs_Man_t * ); extern Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube ); /*=== pdrTsim3.c ==========================================================*/ extern Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio ); extern void Txs3_ManStop( Txs3_Man_t * ); extern Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube ); /*=== pdrUtil.c ==========================================================*/ extern Pdr_Set_t * Pdr_SetAlloc( int nSize ); extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits ); extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove ); extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits ); extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet ); extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p ); extern void Pdr_SetDeref( Pdr_Set_t * p ); extern Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep ); extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove ); extern int ZPdr_SetIsInit( Pdr_Set_t * p ); extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); extern void ZPdr_SetPrint( Pdr_Set_t * p ); extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ); extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ); extern void Pdr_OblDeref( Pdr_Obl_t * p ); extern int Pdr_QueueIsEmpty( Pdr_Man_t * p ); extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p ); extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p ); extern void Pdr_QueueClean( Pdr_Man_t * p ); extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl ); extern void Pdr_QueuePrint( Pdr_Man_t * p ); extern void Pdr_QueueStop( Pdr_Man_t * p ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////