/**CHeaderFile***************************************************************** FileName [absInt.h] PackageName [abs] Synopsis [Internal declarations required for the incremental CTL model checker.] Description [The definitions in this file can be divided in three categories: The verbosity constants, the structure definitions and the macros to access to all the fields in the structures.] Author [Abelardo Pardo ] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] Revision [$Id: absInt.h,v 1.16 2002/09/08 22:18:10 fabio Exp $] ******************************************************************************/ #ifndef _ABSINT #define _ABSINT /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include #include "ntm.h" #include "abs.h" #include /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /* The verbosity system used throughout the entire code is based on a mask. This mask is assumed to have 32 bits, every bit turns on and off the printout of certain info related to the algorithm. The way to use this mask is to go bit by bit and write a 0 to turn off the printing or a 1 to turn it on. Be careful with printing information that is too verbose, such as the cubes for sat or goalSet, or the minterms of a result. The program does not have any mechanism to detect this situation, and if the output is redirected to a file, for a complex example, the size of that file might potentially overflow the biggest of the filesystems. Please refer to the man page of the incremental_ctl_verification command on how to specify the mask. */ #define ABS_VB_PIFF (1<<0) /* system's primary inputs and flip-flops */ #define ABS_VB_GRAPH (1<<1) /* labeled operational graph */ #define ABS_VB_PTIME (1<<2) /* cpu-time for each vertex */ #define ABS_VB_SCUBE (1<<3) /* cubes of sat */ #define ABS_VB_GCUBE (1<<4) /* cubes of goalSet */ #define ABS_VB_VTXCNT (1<<5) /* vertex's contents after evaluation */ #define ABS_VB_CARE (1<<6) /* care set for every evaluation */ #define ABS_VB_CARESZ (1<<7) /* care set size for every evaluation */ #define ABS_VB_TSAT (1<<8) /* number of states that satisfy formula */ #define ABS_VB_PRCH (1<<9) /* number of reachable states */ #define ABS_VB_PITER (1<<10) /* iterate minterms of a fixed point */ #define ABS_VB_ITSIZ (1<<11) /* iterate's size in a fixed point */ #define ABS_VB_PRDOT (1<<12) /* formulas in dot format */ #define ABS_VB_PENV (1<<13) /* number of envelope states */ #define ABS_VB_PRINIT (1<<14) /* number of states to be refined */ #define ABS_VB_PREFSZ (1<<15) /* size of the refinement operands */ #define ABS_VB_PREFCB (1<<16) /* cubes of the refinement operands */ #define ABS_VB_SIMPLE (1<<17) /* how the system has been simplified */ #define ABS_VB_PPROGR (1<<18) /* partial progress: reach, EG(true, etc) */ #define ABS_VB_REFINE (1<<19) /* Begin/End refinement process */ #define ABS_VB_GOALSZ (1<<20) /* Size of goal set */ #define ABS_VB_GLCUBE (1<<21) /* cubes of the goal set */ #define ABS_VB_REFVTX (1<<22) /* Contents of vertex after refinement */ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef struct AbsVertexInfo AbsVertexInfo_t; typedef struct AbsOptions AbsOptions_t; typedef struct AbsVertexCatalog AbsVertexCatalog_t; typedef struct AbsParseInfo AbsParseInfo_t; typedef struct AbsStats AbsStats_t; typedef struct AbsEvalCacheEntry AbsEvalCacheEntry_t; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Enum************************************************************************ Synopsis [Type of result obtained from the verification algorithm.] Description [The algorithm may provide a conclusive or inconclusive result. The conclusive result itself can be that the formula is TRUE or FALSE.] SeeAlso [AbsFormulaArrayVerify] ******************************************************************************/ typedef enum { trueVerification_c, falseVerification_c, inconclusiveVerification_c } AbsVerificationResult_t; /**Enum************************************************************************ Synopsis [Type of vertices representing a formula] Description [A formula is represented by a data structure referred to as the "labeled operational graph". This graph has a structure structure close to the parse tree of the formula. This enumerated type contains the different types of vertices that can be found in that graph.] SeeAlso [AbsCtlFormulaArrayTranslate] ******************************************************************************/ typedef enum { fixedPoint_c, and_c, xor_c, xnor_c, not_c, preImage_c, identifier_c, variable_c, false_c } AbsVertex_t; /**Struct********************************************************************** Synopsis [Data structure attached to every vertex of labeled operational graph representing a given formula] Description [This structure holds all the per vertex information that is relevant to the verification procedure. The structure has a union to store the information that is different depending on the type of vertex. The main highlights of this data structure is that for the case of the vertex of type EX, the field exData contains a table storing the previous solutions computed for that vertex. This can be seen as a cache. The reason for this cache is because since the algorithm works incrementally, it has to perform numerous re-evaluation of formulas, and the most expensive to re-evaluate are the EX vertices, so the storage of the previous results pays off.] SeeAlso [AbsCtlFormulaArrayTranslate AbsSubFormulaRefine AbsSubFormulaVerify] ******************************************************************************/ struct AbsVertexInfo { AbsVertex_t vertexType; /* Type of vertex */ mdd_t *sat; /* Set of states that satisfy the sub-formula */ int vertexId; /* Integer identifying a vertex */ int refs; /* Number of vertices pointing to this one */ int served; /* Times the vertex's results have been read */ int depth; /* Depth of the formula it represents */ boolean polarity; /* Boolean saying the node's polarity */ boolean localApprox; /* Local approximation has been computed */ boolean globalApprox; /* Approximated in a sub-formula */ boolean constant; /* The sub-formula does not have variables */ boolean trueRefine; /* The refinement process is conclusive */ AbsVertexInfo_t *leftKid; /* Left sub-formula */ AbsVertexInfo_t *rightKid; /* Right sub-formula */ lsList parent; /* Pointers to the parent formulas */ union { struct { st_table *solutions; /* Already computed results */ } exData; struct { int varId; /* Variable id */ mdd_t *goalSet; /* States that need to be include/excluded */ } varData; struct { AbsVertexInfo_t *fpVar; /* Right sub-formula */ array_t *rings; /* mdd_ts computed in the fixed point */ array_t *ringApprox; /* Approximations made in the rings */ array_t *subApprox; /* Approximation made from the previous iteration */ boolean useExtraCareSet;/* Use care set ala reachability */ } fpData; struct { char *name; /* name of the id */ char *value; /* value of the id */ } idData; } vertexData; }; /**Struct********************************************************************** Synopsis [Structure to store the information needed in the overall verification process.] Description [Some of these fields are owned by the package, that is, they are created inside the Abs code, and some others are just pointers to other data structures not created in abs. The allocation and free procedures take care of that by de-allocating only the structures locally created. The overall algorithm also performs a series of image computations. Because of the high number of re-evaluation of formulas, the overall algorithm keeps a table storing the results of previous image computations. This table is global to the entire algorithm, therefore, any image computation that is performed at any point checks first if the result is already in the "imageCache" table.] SeeAlso [AbsCtlFormulaArrayTranslate AbsSubFormulaRefine AbsSubFormulaVerify] ******************************************************************************/ struct AbsVerificationInfo { Ntk_Network_t *network; /* Pointer to network. Not owned */ graph_t *partition; /* Pointer to the partition. Not owned */ mdd_manager *mddManager; /* Manager. Not Owned */ Fsm_Fsm_t *fsm; /* Fsm being considered. Not Owned */ int numStateVars; /* Number of bdd state variables */ Fsm_Fsm_t *approxFsm; /* Approximate FSM. Not Owned */ st_table *stateVars; /* Table with the state variable ids. Owned */ st_table *quantifyVars; /* Variables to Quantify. Owned */ mdd_t *careSet; /* Global care set */ mdd_t *tmpCareSet; /* Temporary care set */ st_table *imageCache; /* To store the image computations */ AbsVertexCatalog_t *catalog; /* Catalog to detect common sub-formulas */ AbsStats_t *stats; /* Statistics gathered during execution */ AbsOptions_t *options; /* Command line options */ }; /**Struct********************************************************************** Synopsis [Structure for storing the command line options.] SeeAlso [AbsVerificationInfo] ******************************************************************************/ struct AbsOptions { long verbosity; /* Level of verbosity throughout the verification */ int timeOut; /* Time limit in the execution */ boolean reachability; /* Do reachability analysis prior to verification */ boolean envelope; /* Compute EG(true) as the first formula */ char *fileName; /* File to read the formulas from */ char *fairFileName; /* File to read the fairness constraints for FCTL */ boolean exact; /* Perform exact verification */ boolean printStats; /* Print the stats after verification */ boolean minimizeIterate; /* Minimize the iterates of the fixed points */ boolean negateFormula; /* Verify the negation of the formula instead */ boolean partApprox; /* Use partition transition relation approximation */ }; /**Struct********************************************************************** Synopsis [Structure to store statistics about the algorithm.] Description [The statistics collected through execution will be stored in this structure which itself is stored inside the AbsVerificationInfo_t structure.] SeeAlso [AbsVerificationInfo_t] ******************************************************************************/ struct AbsStats { int numReorderings; /* Number of BDD variable re-orderings performed */ int evalFixedPoint; /* Number of FixedPoint vertex evaluations */ int evalAnd; /* Number of And vertex evaluations*/ int evalNot; /* Number of Not vertex evaluations*/ int evalPreImage; /* Number of PreImage vertex evaluations*/ int evalIdentifier; /* Number of Identifier vertex evaluations*/ int evalVariable; /* Number of Variable vertex evaluations*/ int refineFixedPoint; /* Number of FixedPoint vertex refinements */ int refineAnd; /* Number of And vertex refinements */ int refineNot; /* Number of Not vertex refinements */ int refinePreImage; /* Number of PreImage vertex refinements */ int refineIdentifier; /* Number of Identifier vertex refinements */ int refineVariable; /* Number of Variable vertex refinements */ int exactPreImage; /* Number of exact pre-image computations */ int approxPreImage; /* Number of approximate pre-image computations */ int exactImage; /* Number of exact image computations */ int preImageCacheEntries; /* Size of the pre-image cache */ int imageCacheEntries; /* Size of the image cache */ long imageCpuTime; /* CPU time spent in exact image computation */ long preImageCpuTime; /* CPU time spent in exact pre-image computation */ long appPreCpuTime; /* CPU time spent in approximate pre-image comp. */ }; /**Struct********************************************************************** Synopsis [Cache entry for image and pre-image cache] SeeAlso [AbsSubFormulaRefine] ******************************************************************************/ struct AbsEvalCacheEntry { mdd_t *key; /* BDD operand */ boolean approx; /* Is it an approximation? */ int complement; /* Is it complemented? */ mdd_t *result; /* Result BDD */ mdd_t *careSet; /* Care set used for the computation */ }; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Macro to read the vertexType field from a AbsVertexInfo_t structure.] SideEffects [] ******************************************************************************/ #define AbsVertexReadType( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexType) /**Macro*********************************************************************** Synopsis [Macro to read the vertexId field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [] ******************************************************************************/ #define AbsVertexReadId( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexId) /**Macro*********************************************************************** Synopsis [Macro to read the sat field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadSat( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->sat) /**Macro*********************************************************************** Synopsis [Macro to read the references field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadRefs( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->refs) /**Macro*********************************************************************** Synopsis [Macro to read the served field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadServed( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->served) /**Macro*********************************************************************** Synopsis [Macro to read the polarity field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadPolarity( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->polarity) /**Macro*********************************************************************** Synopsis [Macro to read the depth field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadDepth( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->depth) /**Macro*********************************************************************** Synopsis [Macro to read the localApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadLocalApprox( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->localApprox) /**Macro*********************************************************************** Synopsis [Macro to read the globalApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadGlobalApprox( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->globalApprox) /**Macro*********************************************************************** Synopsis [Macro to read the constant field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadConstant( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->constant) /**Macro*********************************************************************** Synopsis [Macro to read the trueRefine field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadTrueRefine( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->trueRefine) /**Macro*********************************************************************** Synopsis [Macro to read the leftKid field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadLeftKid( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->leftKid) /**Macro*********************************************************************** Synopsis [Macro to read the rightKid field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadRightKid( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->rightKid) /**Macro*********************************************************************** Synopsis [Macro to read the parent field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadParent( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->parent) /**Macro*********************************************************************** Synopsis [Macro to read the solutions field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadSolutions( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.exData.solutions) /**Macro*********************************************************************** Synopsis [Macro to read the varId field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadVarId( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.varData.varId) /**Macro*********************************************************************** Synopsis [Macro to read the goalSet field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadGoalSet( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.varData.goalSet) /**Macro*********************************************************************** Synopsis [Macro to read the fpVar field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadFpVar( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.fpData.fpVar) /**Macro*********************************************************************** Synopsis [Macro to read the rings field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadRings( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.fpData.rings) /**Macro*********************************************************************** Synopsis [Macro to fetch an element from the rings field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexFetchRing( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ index \ ) \ (array_fetch(mdd_t *, ((sfPtr)->vertexData.fpData.rings), (index))) /**Macro*********************************************************************** Synopsis [Macro to read the ringApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadRingApprox( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.fpData.ringApprox) /**Macro*********************************************************************** Synopsis [Macro to fetch an element from the ringApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexFetchRingApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ index \ ) \ (array_fetch(boolean, ((sfPtr)->vertexData.fpData.ringApprox), (index))) /**Macro*********************************************************************** Synopsis [Macro to read the subApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadSubApprox( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.fpData.subApprox) /**Macro*********************************************************************** Synopsis [Macro to fetch an element from the subApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexFetchSubApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ index \ ) \ (array_fetch(boolean, ((sfPtr)->vertexData.fpData.subApprox), (index))) /**Macro*********************************************************************** Synopsis [Macro to read the useExtraCareSet field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadUseExtraCareSet( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.fpData.useExtraCareSet) /**Macro*********************************************************************** Synopsis [Macro to read the name field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadName( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.idData.name) /**Macro*********************************************************************** Synopsis [Macro to read the value field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexReadValue( \ /* AbsVertexInfo_t * */ sfPtr \ ) \ ((sfPtr)->vertexData.idData.value) /**Macro*********************************************************************** Synopsis [Macro to set the vertexType field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetType( \ /* AbsVertexInfo_t * */ sfPtr, \ /* AbsVertex_t */ vtype \ ) \ ((sfPtr)->vertexType) = (vtype) /**Macro*********************************************************************** Synopsis [Macro to set the vertexId field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetId( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ data \ ) \ ((sfPtr)->vertexId) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the sat field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetSat( \ /* AbsVertexInfo_t * */ sfPtr, \ /* mdd_t * */ set \ ) \ ((sfPtr)->sat) = (set) /**Macro*********************************************************************** Synopsis [Macro to set the refs field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetRefs( \ /* AbsVertexInfo_t * */ sfPtr, \ /* boolean */ data \ ) \ ((sfPtr)->refs) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the served field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetServed( \ /* AbsVertexInfo_t * */ sfPtr, \ /* boolean */ data \ ) \ ((sfPtr)->served) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the polarity field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetPolarity( \ /* AbsVertexInfo_t * */ sfPtr, \ /* boolean */ data \ ) \ ((sfPtr)->polarity) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the depth field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetDepth( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ data \ ) \ ((sfPtr)->depth) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the localApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetLocalApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* boolean */ data \ ) \ ((sfPtr)->localApprox) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the globalApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetGlobalApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* boolean */ data \ ) \ ((sfPtr)->globalApprox) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the constant field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetConstant( \ /* AbsVertexInfo_t * */ sfPtr, \ /* boolean */ data \ ) \ ((sfPtr)->constant) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the trueRefine field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetTrueRefine( \ /* AbsVertexInfo_t * */ sfPtr, \ /* boolean */ data \ ) \ ((sfPtr)->trueRefine) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the leftKid field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetLeftKid( \ /* AbsVertexInfo_t * */ sfPtr, \ /* AbsVertexInfo_t * */ subFormulaPtr \ ) \ ((sfPtr)->leftKid) = (subFormulaPtr) /**Macro*********************************************************************** Synopsis [Macro to set the rightKid field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetRightKid( \ /* AbsVertexInfo_t * */ sfPtr, \ /* AbsVertexInfo_t * */ subFormulaPtr \ ) \ ((sfPtr)->rightKid) = (subFormulaPtr) /**Macro*********************************************************************** Synopsis [Macro to set the parent field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetParent( \ /* AbsVertexInfo_t * */ sfPtr, \ /* AbsVertexInfo_t * */ subFormulaPtr \ ) \ lsNewBegin(((sfPtr)->parent), (lsGeneric)subFormulaPtr, NIL(lsHandle)) /**Macro*********************************************************************** Synopsis [Macro to set the solutions field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetSolutions( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ ((sfPtr)->vertexData.exData.solutions) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the varId field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetVarId( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ ((sfPtr)->vertexData.varData.varId) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the goalSet field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetGoalSet( \ /* AbsVertexInfo_t * */ sfPtr, \ /* mdd_t * */ set \ ) \ ((sfPtr)->vertexData.varData.goalSet) = (set) /**Macro*********************************************************************** Synopsis [Macro to set the fpVar field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetFpVar( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ data \ ) \ ((sfPtr)->vertexData.fpData.fpVar) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the rings field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetRings( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ ((sfPtr)->vertexData.fpData.rings) = (data) /**Macro*********************************************************************** Synopsis [Macro to insert a ring in the rings field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexInsertRing( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ array_insert_last(mdd_t *, ((sfPtr)->vertexData.fpData.rings), (data)) /**Macro*********************************************************************** Synopsis [Macro to set the ringApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetRingApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ ((sfPtr)->vertexData.fpData.ringApprox) = (data) /**Macro*********************************************************************** Synopsis [Macro to insert an element in the ringApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexInsertRingApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ array_insert_last(boolean, ((sfPtr)->vertexData.fpData.ringApprox), (data)) /**Macro*********************************************************************** Synopsis [Macro to set the subApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetSubApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ ((sfPtr)->vertexData.fpData.subApprox) = (data) /**Macro*********************************************************************** Synopsis [Macro to insert an element in the subApprox field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexInsertSubApprox( \ /* AbsVertexInfo_t * */ sfPtr, \ /* array_t * */ data \ ) \ array_insert_last(boolean, ((sfPtr)->vertexData.fpData.subApprox), (data)) /**Macro*********************************************************************** Synopsis [Macro to set the useExtraCareSet field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetUseExtraCareSet( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ data \ ) \ ((sfPtr)->vertexData.fpData.useExtraCareSet) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the name field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetName( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ data \ ) \ ((sfPtr)->vertexData.idData.name) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the value field from a AbsVertexInfo_t structure.] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ #define AbsVertexSetValue( \ /* AbsVertexInfo_t * */ sfPtr, \ /* int */ data \ ) \ ((sfPtr)->vertexData.idData.value) = (data) /**Macro*********************************************************************** Synopsis [Macro to read the network field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadNetwork( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->network) /**Macro*********************************************************************** Synopsis [Macro to read the partition field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadPartition( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->partition) /**Macro*********************************************************************** Synopsis [Macro to read the fsm field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadFsm( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->fsm) /**Macro*********************************************************************** Synopsis [Macro to read the numStateVars field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadNumStateVars( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->numStateVars) /**Macro*********************************************************************** Synopsis [Macro to read the approxFsm field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadApproxFsm( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->approxFsm) /**Macro*********************************************************************** Synopsis [Macro to read the stateVars field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadStateVars( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->stateVars) /**Macro*********************************************************************** Synopsis [Macro to read the quantifyVars field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadQuantifyVars( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->quantifyVars) /**Macro*********************************************************************** Synopsis [Macro to read the careSet field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadCareSet( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->careSet) /**Macro*********************************************************************** Synopsis [Macro to read the tmpCareSet field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadTmpCareSet( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->tmpCareSet) /**Macro*********************************************************************** Synopsis [Macro to read the imageCache field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadImageCache( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->imageCache) /**Macro*********************************************************************** Synopsis [Macro to read the mddManager field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadMddManager( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->mddManager) /**Macro*********************************************************************** Synopsis [Macro to read the catalog field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadCatalog( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->catalog) /**Macro*********************************************************************** Synopsis [Macro to read the stats field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadStats( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->stats) /**Macro*********************************************************************** Synopsis [Macro to read the options field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoReadOptions( \ /* Abs_VerificationInfo_t * */ vInfo \ ) \ ((vInfo)->options) /**Macro*********************************************************************** Synopsis [Macro to set the network field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetNetwork( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* Ntk_Network_t */ data \ ) \ ((vInfo)->network) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the partition field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetPartition( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* graph_t */ data \ ) \ ((vInfo)->partition) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the fsm field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetFsm( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* Fsm_Fsm_t */ data \ ) \ ((vInfo)->fsm) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the numStateVars field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetNumStateVars( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* Fsm_Fsm_t */ data \ ) \ ((vInfo)->numStateVars) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the approxFsm field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetApproxFsm( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* Fsm_Fsm_t */ data \ ) \ ((vInfo)->approxFsm) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the stateVars field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetStateVars( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* st_table * */ data \ ) \ ((vInfo)->stateVars) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the quantifyVars field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetQuantifyVars( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* st_table **/ data \ ) \ ((vInfo)->quantifyVars) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the careSet field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetCareSet( \ /* Abs_VerificationInfo_t * */ vInfo,\ /* st_table **/ data \ ) \ ((vInfo)->careSet) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the tmpCareSet field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetTmpCareSet( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* st_table **/ data \ ) \ ((vInfo)->tmpCareSet) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the imageCache field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetImageCache( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* st_table **/ data \ ) \ ((vInfo)->imageCache) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the mddManager field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetMddManager( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* mdd_manager * */ data \ ) \ ((vInfo)->mddManager) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the catalog field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetCatalog( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* AbsVertexInfo_t * */ data \ ) \ ((vInfo)->catalog) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the stats field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetStats( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* AbsVertexInfo_t * */ data \ ) \ ((vInfo)->stats) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the options field from a Abs_VerificationInfo_t structure.] SideEffects [] SeeAlso [Abs_VerificationInfo_t] ******************************************************************************/ #define AbsVerificationInfoSetOptions( \ /* Abs_VerificationInfo_t * */ vInfo, \ /* AbsOptions_t * */ data \ ) \ ((vInfo)->options) = (data) /**Macro*********************************************************************** Synopsis [Macro to read the verbosity field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadVerbosity( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->verbosity) /**Macro*********************************************************************** Synopsis [Macro to read the timeOut field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadTimeOut( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->timeOut) /**Macro*********************************************************************** Synopsis [Macro to read the reachability field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadReachability( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->reachability) /**Macro*********************************************************************** Synopsis [Macro to read the envelope field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadEnvelope( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->envelope) /**Macro*********************************************************************** Synopsis [Macro to read the fileName field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadFileName( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->fileName) /**Macro*********************************************************************** Synopsis [Macro to read the fairFileName field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadFairFileName( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->fairFileName) /**Macro*********************************************************************** Synopsis [Macro to read the exact field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadExact( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->exact) /**Macro*********************************************************************** Synopsis [Macro to read the printStats field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadPrintStats( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->printStats) /**Macro*********************************************************************** Synopsis [Macro to read the minimizeIterate field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadMinimizeIterate( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->minimizeIterate) /**Macro*********************************************************************** Synopsis [Macro to read the negateFormula field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadNegateFormula( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->negateFormula) /**Macro*********************************************************************** Synopsis [Macro to read the partApprox field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsReadPartApprox( \ /* AbsOptions_t * */ oInfo \ ) \ ((oInfo)->partApprox) /**Macro*********************************************************************** Synopsis [Macro to set the verbosity field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsSetVerbosity( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->verbosity) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the timeOut field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsSetTimeOut( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->timeOut) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the reachability field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsSetReachability( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->reachability) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the envelope field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsSetEnvelope( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->envelope) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the fileName field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ #define AbsOptionsSetFileName( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->fileName) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the fairFileName field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions_t] ******************************************************************************/ #define AbsOptionsSetFairFileName( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->fairFileName) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the exact field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions_t] ******************************************************************************/ #define AbsOptionsSetExact( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->exact) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the printStats field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions_t] ******************************************************************************/ #define AbsOptionsSetPrintStats( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->printStats) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the minimizeIterate field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions_t] ******************************************************************************/ #define AbsOptionsSetMinimizeIterate( \ /* AbsOptions_t * */ oInfo, \ /* int */ data \ ) \ ((oInfo)->minimizeIterate) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the negateFormula field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions_t] ******************************************************************************/ #define AbsOptionsSetNegateFormula( \ /* AbsOptions_t * */ oInfo, \ /* boolean */ data \ ) \ ((oInfo)->negateFormula) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the partApprox field from a AbsOptions_t structure.] SideEffects [] SeeAlso [AbsOptions_t] ******************************************************************************/ #define AbsOptionsSetPartApprox( \ /* AbsOptions_t * */ oInfo, \ /* boolean */ data \ ) \ ((oInfo)->partApprox) = (data) /**Macro*********************************************************************** Synopsis [Macro to read the numReorderings field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadNumReorderings( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->numReorderings /**Macro*********************************************************************** Synopsis [Macro to read the evalFixedPoint field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadEvalFixedPoint( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->evalFixedPoint /**Macro*********************************************************************** Synopsis [Macro to set the numReorderings field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetNumReorderings( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->numReorderings = (data) /**Macro*********************************************************************** Synopsis [Macro to set the evalFixedPoint field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetEvalFixedPoint( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->evalFixedPoint = (data) /**Macro*********************************************************************** Synopsis [Macro to read the evalAnd field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadEvalAnd( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->evalAnd /**Macro*********************************************************************** Synopsis [Macro to set the evalAnd field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetEvalAnd( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->evalAnd = (data) /**Macro*********************************************************************** Synopsis [Macro to read the evalNot field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadEvalNot( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->evalNot /**Macro*********************************************************************** Synopsis [Macro to set the evalNot field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetEvalNot( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->evalNot = (data) /**Macro*********************************************************************** Synopsis [Macro to read the evalPreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadEvalPreImage( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->evalPreImage /**Macro*********************************************************************** Synopsis [Macro to set the evalPreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetEvalPreImage( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->evalPreImage = (data) /**Macro*********************************************************************** Synopsis [Macro to read the evalIdentifier field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadEvalIdentifier( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->evalIdentifier /**Macro*********************************************************************** Synopsis [Macro to set the evalIdentifier field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetEvalIdentifier( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->evalIdentifier = (data) /**Macro*********************************************************************** Synopsis [Macro to read the evalVariable field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadEvalVariable( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->evalVariable /**Macro*********************************************************************** Synopsis [Macro to set the evalVariable field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetEvalVariable( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->evalVariable = (data) /**Macro*********************************************************************** Synopsis [Macro to read the refineFixedPoint field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadRefineFixedPoint( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->refineFixedPoint /**Macro*********************************************************************** Synopsis [Macro to set the refineFixedPoint field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetRefineFixedPoint( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->refineFixedPoint = (data) /**Macro*********************************************************************** Synopsis [Macro to read the refineAnd field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadRefineAnd( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->refineAnd /**Macro*********************************************************************** Synopsis [Macro to set the refineAnd field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetRefineAnd( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->refineAnd = (data) /**Macro*********************************************************************** Synopsis [Macro to read the refineNot field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadRefineNot( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->refineNot /**Macro*********************************************************************** Synopsis [Macro to set the refineNot field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetRefineNot( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->refineNot = (data) /**Macro*********************************************************************** Synopsis [Macro to read the refinePreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadRefinePreImage( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->refinePreImage /**Macro*********************************************************************** Synopsis [Macro to set the refinePreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetRefinePreImage( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->refinePreImage = (data) /**Macro*********************************************************************** Synopsis [Macro to read the refineIdentifier field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadRefineIdentifier( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->refineIdentifier /**Macro*********************************************************************** Synopsis [Macro to set the refineIdentifier field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetRefineIdentifier( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->refineIdentifier = (data) /**Macro*********************************************************************** Synopsis [Macro to read the refineVariable field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadRefineVariable( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->refineVariable /**Macro*********************************************************************** Synopsis [Macro to set the refineVariable field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetRefineVariable( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->refineVariable = (data) /**Macro*********************************************************************** Synopsis [Macro to read the exactPreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadExactPreImage( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->exactPreImage /**Macro*********************************************************************** Synopsis [Macro to set the exactPreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetExactPreImage( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->exactPreImage = (data) /**Macro*********************************************************************** Synopsis [Macro to read the approxPreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadApproxPreImage( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->approxPreImage /**Macro*********************************************************************** Synopsis [Macro to set the approxPreImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetApproxPreImage( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->approxPreImage = (data) /**Macro*********************************************************************** Synopsis [Macro to read the exactImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadExactImage( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->exactImage /**Macro*********************************************************************** Synopsis [Macro to set the exactImage field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetExactImage( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->exactImage = (data) /**Macro*********************************************************************** Synopsis [Macro to read the preImageCacheEntries field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadPreImageCacheEntries( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->preImageCacheEntries /**Macro*********************************************************************** Synopsis [Macro to set the preImageCacheEntries field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetPreImageCacheEntries( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->preImageCacheEntries = (data) /**Macro*********************************************************************** Synopsis [Macro to read the imageCacheEntries field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadImageCacheEntries( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->imageCacheEntries /**Macro*********************************************************************** Synopsis [Macro to set the imageCacheEntries field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetImageCacheEntries( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->imageCacheEntries = (data) /**Macro*********************************************************************** Synopsis [Macro to read the imageCpuTime field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadImageCpuTime( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->imageCpuTime /**Macro*********************************************************************** Synopsis [Macro to set the imageCpuTime field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetImageCpuTime( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->imageCpuTime = (data) /**Macro*********************************************************************** Synopsis [Macro to read the preImageCpuTime field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadPreImageCpuTime( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->preImageCpuTime /**Macro*********************************************************************** Synopsis [Macro to set the preImageCpuTime field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetPreImageCpuTime( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->preImageCpuTime = (data) /**Macro*********************************************************************** Synopsis [Macro to read the appPreCpuTime field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsReadAppPreCpuTime( \ /* AbsStats_t * */ sInfo \ ) \ (sInfo)->appPreCpuTime /**Macro*********************************************************************** Synopsis [Macro to set the appPreCpuTime field from a AbsStats_t structure.] SideEffects [] SeeAlso [AbsStats_t] ******************************************************************************/ #define AbsStatsSetAppPreCpuTime( \ /* AbsStats_t * */ sInfo, \ /* int */ data \ ) \ (sInfo)->appPreCpuTime = (data) /**Macro*********************************************************************** Synopsis [Macro to read the key field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntryReadKey( \ /* AbsEvalCacheEntry_t * */ eInfo \ ) \ ((eInfo)->key) /**Macro*********************************************************************** Synopsis [Macro to set the key field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntrySetKey( \ /* AbsEvalCacheEntry_t * */ eInfo, \ /* mdd_t * */ data \ ) \ ((eInfo)->key) = (data) /**Macro*********************************************************************** Synopsis [Macro to read the approx field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntryReadApprox( \ /* AbsEvalCacheEntry_t * */ eInfo \ ) \ ((eInfo)->approx) /**Macro*********************************************************************** Synopsis [Macro to set the approx field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntrySetApprox( \ /* AbsEvalCacheEntry_t * */ eInfo, \ /* mdd_t * */ data \ ) \ ((eInfo)->approx) = (data) /**Macro*********************************************************************** Synopsis [Macro to read the complement field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntryReadComplement( \ /* AbsEvalCacheEntry_t * */ eInfo \ ) \ ((eInfo)->complement) /**Macro*********************************************************************** Synopsis [Macro to set the complement field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntrySetComplement( \ /* AbsEvalCacheEntry_t * */ eInfo, \ /* mdd_t * */ data \ ) \ ((eInfo)->complement) = (data) /**Macro*********************************************************************** Synopsis [Macro to read the result field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntryReadResult( \ /* AbsEvalCacheEntry_t * */ eInfo \ ) \ ((eInfo)->result) /**Macro*********************************************************************** Synopsis [Macro to read the careSet field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntryReadCareSet( \ /* AbsEvalCacheEntry_t * */ eInfo \ ) \ ((eInfo)->careSet) /**Macro*********************************************************************** Synopsis [Macro to set the result field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntrySetResult( \ /* AbsEvalCacheEntry_t * */ eInfo, \ /* mdd_t * */ data \ ) \ ((eInfo)->result) = (data) /**Macro*********************************************************************** Synopsis [Macro to set the careSet field of the AbsEvalCacheEntry_t structure.] SideEffects [] SeeAlso [AbsEvalCacheEntry_t] ******************************************************************************/ #define AbsEvalCacheEntrySetCareSet( \ /* AbsEvalCacheEntry_t * */ eInfo, \ /* mdd_t * */ data \ ) \ ((eInfo)->careSet) = (data) /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN AbsVertexCatalog_t * AbsVertexCatalogInitialize(void); EXTERN void AbsVertexCatalogFree(AbsVertexCatalog_t *c); EXTERN AbsVertexInfo_t * AbsVertexCatalogFindOrAdd(AbsVertexCatalog_t *catalog, AbsVertex_t type, boolean polarity, AbsVertexInfo_t *leftKid, AbsVertexInfo_t *rightKid, int localId, char *idName, char *idValue); EXTERN void AbsCatalogDelete(AbsVertexCatalog_t *catalog, AbsVertexInfo_t *vertex); EXTERN void AbsSubFormulaVerify(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); EXTERN void AbsFormulaScheduleEvaluation(AbsVertexInfo_t *current, AbsVertexInfo_t *limit); EXTERN mdd_t * AbsComputeOptimalIterate(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *lowerIterate, mdd_t *upperIterate); EXTERN boolean AbsFixedPointIterate(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, int iterateIndex); EXTERN AbsVertexInfo_t * AbsVertexInitialize(void); EXTERN void AbsVertexFree(AbsVertexCatalog_t *catalog, AbsVertexInfo_t *v, AbsVertexInfo_t *fromVertex); EXTERN Abs_VerificationInfo_t * AbsVerificationInfoInitialize(void); EXTERN void AbsVerificationInfoFree(Abs_VerificationInfo_t *v); EXTERN AbsOptions_t * AbsOptionsInitialize(void); EXTERN void AbsOptionsFree(AbsOptions_t *unit); EXTERN AbsStats_t * AbsStatsInitialize(void); EXTERN void AbsStatsFree(AbsStats_t *unit); EXTERN AbsEvalCacheEntry_t * AbsCacheEntryInitialize(void); EXTERN void AbsCacheEntryFree(AbsEvalCacheEntry_t *unit); EXTERN void AbsEvalCacheInsert(st_table *solutions, mdd_t *key, mdd_t *result, mdd_t *careSet, boolean approx, boolean replace); EXTERN boolean AbsEvalCacheLookup(st_table *solutions, mdd_t *key, mdd_t *careSet, boolean approx, mdd_t **result, boolean *storedApprox); EXTERN void AbsVerificationFlushCache(Abs_VerificationInfo_t *absInfo); EXTERN void AbsVertexFlushCache(AbsVertexInfo_t *vertexPtr); EXTERN mdd_t * AbsImageReadOrCompute(Abs_VerificationInfo_t *absInfo, Img_ImageInfo_t *imageInfo, mdd_t *set, mdd_t *careSet); EXTERN array_t * AbsFormulaArrayVerify(Abs_VerificationInfo_t *absInfo, array_t *formulaArray); EXTERN Fsm_Fsm_t * AbsCreateReducedFsm(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, Fsm_Fsm_t **approxFsm); EXTERN boolean AbsMddEqualModCareSet(mdd_t *f, mdd_t *g, mdd_t *careSet); EXTERN boolean AbsMddLEqualModCareSet(mdd_t *f, mdd_t *g, mdd_t *careSet); EXTERN AbsParseInfo_t * AbsParseInfoInitialize(void); EXTERN void AbsParseInfoFree(AbsParseInfo_t *data); EXTERN mdd_t * AbsSubFormulaRefine(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet); EXTERN array_t * AbsCtlFormulaArrayTranslate(Abs_VerificationInfo_t *verInfo, array_t *formulaArray, array_t *fairArray); EXTERN void AbsVertexPrintDot(FILE *fp, array_t *vertexArray); EXTERN void AbsVertexPrint(AbsVertexInfo_t *vertexPtr, st_table *visitedSF, boolean recur, long verbosity); EXTERN void AbsBddPrintMinterms(mdd_t *function); EXTERN void AbsFormulaSetConstantBit(AbsVertexInfo_t *vertexPtr); EXTERN boolean AbsFormulaSanityCheck(AbsVertexInfo_t *vertexPtr, st_table *rootTable); EXTERN boolean AbsIteratesSanityCheck(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr); EXTERN void AbsStatsPrintReport(FILE *fp, AbsStats_t *stats); /**AutomaticEnd***************************************************************/ #endif /* _ABSINT */