abc/src/proof/ssw/sswInt.h

/**CFile****************************************************************

  FileName    [sswInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef ABC__aig__ssw__sswInt_h
#define ABC__aig__ssw__sswInt_h


////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "aig/saig/saig.h"
#include "sat/bsat/satSolver.h"
#include "ssw.h"
#include "aig/ioa/ioa.h"

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////



ABC_NAMESPACE_HEADER_START


////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
typedef struct Ssw_Frm_t_ Ssw_Frm_t; // unrolled frames manager
typedef struct Ssw_Sat_t_ Ssw_Sat_t; // SAT solver manager
typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager

struct Ssw_Man_t_
{
    // parameters
    Ssw_Pars_t *     pPars;          // parameters
    int              nFrames;        // for quick lookup
    // AIGs used in the package
    Aig_Man_t *      pAig;           // user-given AIG
    Aig_Man_t *      pFrames;        // final AIG
    Aig_Obj_t **     pNodeToFrames;  // mapping of AIG nodes into FRAIG nodes
    // equivalence classes
    Ssw_Cla_t *      ppClasses;      // equivalence classes of nodes
    int              fRefined;       // is set to 1 when refinement happens
    // SAT solving 
    Ssw_Sat_t *      pMSatBmc;       // SAT manager for base case
    Ssw_Sat_t *      pMSat;          // SAT manager for inductive case
    // SAT solving (latch corr only)
    Vec_Ptr_t *      vSimInfo;       // simulation information for the framed PIs
    int              nPatterns;      // the number of patterns saved
    int              nSimRounds;     // the number of simulation rounds performed
    int              nCallsCount;    // the number of calls in this round
    int              nCallsDelta;    // the number of calls to skip
    int              nCallsSat;      // the number of SAT calls in this round
    int              nCallsUnsat;    // the number of UNSAT calls in this round
    int              nRecycleCalls;  // the number of calls since last recycling
    int              nRecycles;      // the number of time SAT solver was recycled
    int              nRecyclesTotal; // the number of time SAT solver was recycled
    int              nVarsMax;       // the maximum variables in the solver
    int              nCallsMax;      // the maximum number of SAT calls
    // uniqueness
    Vec_Ptr_t *      vCommon;        // the set of common variables in the logic cones
    int              iOutputLit;     // the output literal of the uniqueness constraint
    Vec_Int_t *      vDiffPairs;     // is set to 1 if reg pair can be diff
    int              nUniques;       // the number of uniqueness constraints used 
    int              nUniquesAdded;  // useful uniqueness constraints
    int              nUniquesUseful; // useful uniqueness constraints
    // dynamic constraint addition
    int              nSRMiterMaxId;  // max ID after which the last frame begins
    Vec_Ptr_t *      vNewLos;        // new time frame LOs of to constrain
    Vec_Int_t *      vNewPos;        // new time frame POs of to add constraints
    int *            pVisited;       // flags to label visited nodes in each frame
    int              nVisCounter;    // the traversal ID
    // sequential simulation
    Ssw_Sml_t *      pSml;           // the simulator
    int              iNodeStart;     // the first node considered
    int              iNodeLast;      // the last node considered
    Vec_Ptr_t *      vResimConsts;   // resimulation constants
    Vec_Ptr_t *      vResimClasses;  // resimulation classes
    Vec_Int_t *      vInits;         // the init values of primary inputs under constraints
    // counter example storage
    int              nPatWords;      // the number of words in the counter example
    unsigned *       pPatWords;      // the counter example
    // constraints
    int              nConstrTotal;   // the number of total constraints
    int              nConstrReduced; // the number of reduced constraints
    int              nStrangers;     // the number of strange situations
    // SAT calls statistics
    int              nSatCalls;      // the number of SAT calls
    int              nSatProof;      // the number of proofs
    int              nSatFailsReal;  // the number of timeouts
    int              nSatCallsUnsat; // the number of unsat SAT calls
    int              nSatCallsSat;   // the number of sat SAT calls
    // node/register/lit statistics
    int              nLitsBeg;
    int              nLitsEnd;
    int              nNodesBeg;
    int              nNodesEnd;
    int              nRegsBeg;
    int              nRegsEnd;
    // equiv statistis
    int              nConesTotal;
    int              nConesConstr;
    int              nEquivsTotal;
    int              nEquivsConstr;
    int              nNodesBegC;
    int              nNodesEndC;
    int              nRegsBegC;
    int              nRegsEndC;
    // runtime stats
    abctime          timeBmc;        // bounded model checking
    abctime          timeReduce;     // speculative reduction
    abctime          timeMarkCones;  // marking the cones not to be refined
    abctime          timeSimSat;     // simulation of the counter-examples
    abctime          timeSat;        // solving SAT
    abctime          timeSatSat;     // sat
    abctime          timeSatUnsat;   // unsat
    abctime          timeSatUndec;   // undecided
    abctime          timeOther;      // other runtime
    abctime          timeTotal;      // total runtime
};

// internal SAT manager
struct Ssw_Sat_t_
{
    Aig_Man_t *      pAig;           // the AIG manager
    int              fPolarFlip;     // flips polarity 
    sat_solver *     pSat;           // recyclable SAT solver
    int              nSatVars;       // the counter of SAT variables
    Vec_Int_t *      vSatVars;       // mapping of each node into its SAT var
    Vec_Ptr_t *      vFanins;        // fanins of the CNF node
    Vec_Ptr_t *      vUsedPis;       // the PIs with SAT variables 
    int              nSolverCalls;   // the total number of SAT calls
};

// internal frames manager
struct Ssw_Frm_t_
{
    Aig_Man_t *      pAig;           // user-given AIG
    int              nObjs;          // offset in terms of AIG nodes
    int              nFrames;        // the number of frames in current unrolling
    Aig_Man_t *      pFrames;        // unrolled AIG
    Vec_Ptr_t *      vAig2Frm;       // mapping of AIG nodes into frame nodes
};

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

static inline int  Ssw_ObjSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj )             { return Vec_IntGetEntry( p->vSatVars, pObj->Id );  }
static inline void Ssw_ObjSetSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vSatVars, pObj->Id, Num);      }

static inline int  Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
{
    return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
}
static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
{
    assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) );
    Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}

static inline Aig_Obj_t * Ssw_ObjFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i )                       { return p->pNodeToFrames[p->nFrames*pObj->Id + i];  }
static inline void        Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFrames[p->nFrames*pObj->Id + i] = pNode; }

static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }
static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }

static inline Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i )                       { return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     }
static inline void        Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );     }

static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }
static inline Aig_Obj_t * Ssw_ObjChild1Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== sswAig.c ===================================================*/
extern Ssw_Frm_t *   Ssw_FrmStart( Aig_Man_t * pAig );
extern void          Ssw_FrmStop( Ssw_Frm_t * p );
extern Aig_Man_t *   Ssw_FramesWithClasses( Ssw_Man_t * p );
extern Aig_Man_t *   Ssw_SpeculativeReduction( Ssw_Man_t * p );
/*=== sswBmc.c ===================================================*/
/*=== sswClass.c =================================================*/
extern Ssw_Cla_t *   Ssw_ClassesStart( Aig_Man_t * pAig );
extern void          Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
                         unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
                         int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
                         int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void          Ssw_ClassesStop( Ssw_Cla_t * p );
extern Aig_Man_t *   Ssw_ClassesReadAig( Ssw_Cla_t * p );
extern Vec_Ptr_t *   Ssw_ClassesGetRefined( Ssw_Cla_t * p );
extern void          Ssw_ClassesClearRefined( Ssw_Cla_t * p );
extern int           Ssw_ClassesCand1Num( Ssw_Cla_t * p );
extern int           Ssw_ClassesClassNum( Ssw_Cla_t * p );
extern int           Ssw_ClassesLitNum( Ssw_Cla_t * p );
extern Aig_Obj_t **  Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
extern void          Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
extern void          Ssw_ClassesCheck( Ssw_Cla_t * p );
extern void          Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
extern void          Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t *   Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig );
extern Ssw_Cla_t *   Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
extern Ssw_Cla_t *   Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
extern Ssw_Cla_t *   Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int           Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive );
extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int           Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int           Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
extern int           Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr );
/*=== sswCnf.c ===================================================*/
extern Ssw_Sat_t *   Ssw_SatStart( int fPolarFlip );
extern void          Ssw_SatStop( Ssw_Sat_t * p );
extern void          Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj );
extern int           Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig );
/*=== sswConstr.c ===================================================*/
extern int           Ssw_ManSweepBmcConstr( Ssw_Man_t * p );
extern int           Ssw_ManSweepConstr( Ssw_Man_t * p );
extern void          Ssw_ManRefineByConstrSim( Ssw_Man_t * p );
/*=== sswCore.c ===================================================*/
extern Aig_Man_t *   Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
/*=== sswDyn.c ===================================================*/
extern void          Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
extern int           Ssw_ManSweepDyn( Ssw_Man_t * p );
/*=== sswLcorr.c ==========================================================*/
extern int           Ssw_ManSweepLatch( Ssw_Man_t * p );
/*=== sswMan.c ===================================================*/
extern Ssw_Man_t *   Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern void          Ssw_ManCleanup( Ssw_Man_t * p );
extern void          Ssw_ManStop( Ssw_Man_t * p );
/*=== sswSat.c ===================================================*/
extern int           Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int           Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int           Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj );
/*=== sswSemi.c ===================================================*/
extern int           Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
/*=== sswSim.c ===================================================*/
extern unsigned      Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int           Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int           Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern int           Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
extern int           Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void          Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame );
extern Ssw_Sml_t *   Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void          Ssw_SmlClean( Ssw_Sml_t * p );
extern void          Ssw_SmlStop( Ssw_Sml_t * p );
extern void          Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
extern void          Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
extern void          Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void          Ssw_SmlSimulateOne( Ssw_Sml_t * p );
extern void          Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
extern void          Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pVisited, int nVisCounter );
extern void          Ssw_SmlResimulateSeq( Ssw_Sml_t * p );
/*=== sswSimSat.c ===================================================*/
extern void          Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
extern void          Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
extern int           Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern void          Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f );
extern int           Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs );
extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int           Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/
extern void          Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
extern int           Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose );
extern int           Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );



ABC_NAMESPACE_HEADER_END



#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////