pdrInt.h

/**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"
    #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                 satoko_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             satoko_read_cex_varvalue
    #define sat_solver_set_runtime_limit     satoko_set_runtime_limit
    #define sat_solver_set_runid             satoko_set_runid           
    #define sat_solver_set_stop_func         satoko_set_stop_func          
    #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                                ///
////////////////////////////////////////////////////////////////////////