source: vis_dev/vis-2.3/src/abs/absInt.h @ 93

Last change on this file since 93 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 88.1 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [absInt.h]
4
5  PackageName [abs]
6
7  Synopsis [Internal declarations required for the incremental CTL model
8  checker.]
9
10  Description [The definitions in this file can be divided in three categories:
11  The verbosity constants, the structure definitions and the macros to access
12  to all the fields in the structures.]
13 
14  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
15
16  Copyright   [This file was created at the University of Colorado at
17  Boulder.  The University of Colorado at Boulder makes no warranty
18  about the suitability of this software for any purpose.  It is
19  presented on an AS IS basis.]
20
21  Revision    [$Id: absInt.h,v 1.16 2002/09/08 22:18:10 fabio Exp $]
22
23******************************************************************************/
24
25#ifndef _ABSINT
26#define _ABSINT
27
28/*---------------------------------------------------------------------------*/
29/* Nested includes                                                           */
30/*---------------------------------------------------------------------------*/
31#include <unistd.h>
32#include "ntm.h"
33#include "abs.h"
34#include <string.h>
35
36/*---------------------------------------------------------------------------*/
37/* Constant declarations                                                     */
38/*---------------------------------------------------------------------------*/
39
40/* The verbosity system used throughout the entire code is based on a
41   mask. This mask is assumed to have 32 bits, every bit turns on and off the
42   printout of certain info related to the algorithm. The way to use this mask
43   is to go bit by bit and write a 0 to turn off the printing or a 1 to turn it
44   on. Be careful with printing information that is too verbose, such as the
45   cubes for sat or goalSet, or the minterms of a result. The program does not
46   have any mechanism to detect this situation, and if the output is redirected
47   to a file, for a complex example, the size of that file might potentially
48   overflow the biggest of the filesystems. Please refer to the man page of the
49   incremental_ctl_verification command on how to specify the mask. */
50
51#define ABS_VB_PIFF        (1<<0)  /* system's primary inputs and flip-flops */
52#define ABS_VB_GRAPH       (1<<1)  /* labeled operational graph */
53#define ABS_VB_PTIME       (1<<2)  /* cpu-time for each vertex */
54#define ABS_VB_SCUBE       (1<<3)  /* cubes of sat */
55#define ABS_VB_GCUBE       (1<<4)  /* cubes of goalSet */
56#define ABS_VB_VTXCNT      (1<<5)  /* vertex's contents after evaluation */
57#define ABS_VB_CARE        (1<<6)  /* care set for every evaluation */
58#define ABS_VB_CARESZ      (1<<7)  /* care set size for every evaluation */
59#define ABS_VB_TSAT        (1<<8)  /* number of states that satisfy formula */
60#define ABS_VB_PRCH        (1<<9)  /* number of reachable states */
61#define ABS_VB_PITER       (1<<10) /* iterate minterms of a fixed point */
62#define ABS_VB_ITSIZ       (1<<11) /* iterate's size in a fixed point */
63#define ABS_VB_PRDOT       (1<<12) /* formulas in dot format */
64#define ABS_VB_PENV        (1<<13) /* number of envelope states */
65#define ABS_VB_PRINIT      (1<<14) /* number of states to be refined */
66#define ABS_VB_PREFSZ      (1<<15) /* size of the refinement operands */
67#define ABS_VB_PREFCB      (1<<16) /* cubes of the refinement operands */
68#define ABS_VB_SIMPLE      (1<<17) /* how the system has been simplified */
69#define ABS_VB_PPROGR      (1<<18) /* partial progress: reach, EG(true, etc) */
70#define ABS_VB_REFINE      (1<<19) /* Begin/End refinement process */
71#define ABS_VB_GOALSZ      (1<<20) /* Size of goal set */
72#define ABS_VB_GLCUBE      (1<<21) /* cubes of the goal set */
73#define ABS_VB_REFVTX      (1<<22) /* Contents of vertex after refinement */
74
75/*---------------------------------------------------------------------------*/
76/* Type declarations                                                         */
77/*---------------------------------------------------------------------------*/
78
79typedef struct AbsVertexInfo AbsVertexInfo_t;
80typedef struct AbsOptions AbsOptions_t;
81typedef struct AbsVertexCatalog AbsVertexCatalog_t;
82typedef struct AbsParseInfo AbsParseInfo_t;
83typedef struct AbsStats AbsStats_t;
84typedef struct AbsEvalCacheEntry AbsEvalCacheEntry_t;
85
86/*---------------------------------------------------------------------------*/
87/* Structure declarations                                                    */
88/*---------------------------------------------------------------------------*/
89
90/**Enum************************************************************************
91
92  Synopsis    [Type of result obtained from the verification algorithm.]
93
94  Description [The algorithm may provide a conclusive or inconclusive
95  result. The conclusive result itself can be that the formula is TRUE or
96  FALSE.]
97
98  SeeAlso     [AbsFormulaArrayVerify]
99
100******************************************************************************/
101typedef enum {
102  trueVerification_c,
103  falseVerification_c,
104  inconclusiveVerification_c
105} AbsVerificationResult_t;
106
107/**Enum************************************************************************
108
109  Synopsis    [Type of vertices representing a formula]
110
111  Description [A formula is represented by a data structure referred to as the
112  "labeled operational graph". This graph has a structure structure close to
113  the parse tree of the formula. This enumerated type contains the different
114  types of vertices that can be found in that graph.]
115
116  SeeAlso     [AbsCtlFormulaArrayTranslate]
117
118******************************************************************************/
119typedef enum {
120  fixedPoint_c,
121  and_c, 
122  xor_c,
123  xnor_c,
124  not_c,
125  preImage_c,
126  identifier_c,
127  variable_c,
128  false_c
129} AbsVertex_t;
130
131/**Struct**********************************************************************
132
133  Synopsis [Data structure attached to every vertex of labeled operational
134  graph representing a given formula]
135
136  Description [This structure holds all the per vertex information that is
137  relevant to the verification procedure. The structure has a union to store
138  the information that is different depending on the type of vertex. The main
139  highlights of this data structure is that for the case of the vertex of type
140  EX, the field exData contains a table storing the previous solutions computed
141  for that vertex. This can be seen as a cache. The reason for this cache is
142  because since the algorithm works incrementally, it has to perform numerous
143  re-evaluation of formulas, and the most expensive to re-evaluate are the EX
144  vertices, so the storage of the previous results pays off.]
145
146  SeeAlso [AbsCtlFormulaArrayTranslate AbsSubFormulaRefine AbsSubFormulaVerify]
147
148******************************************************************************/
149struct AbsVertexInfo {
150  AbsVertex_t vertexType;     /* Type of vertex */
151  mdd_t *sat;                 /* Set of states that satisfy the sub-formula */ 
152  int vertexId;               /* Integer identifying a vertex */
153  int refs;                   /* Number of vertices pointing to this one */
154  int served;                 /* Times the vertex's results have been read */ 
155  int depth;                  /* Depth of the formula it represents */
156  boolean  polarity;          /* Boolean saying the node's polarity */
157  boolean localApprox;        /* Local approximation has been computed */
158  boolean globalApprox;       /* Approximated in a sub-formula */
159  boolean constant;           /* The sub-formula does not have variables */
160  boolean trueRefine;         /* The refinement process is conclusive */
161  AbsVertexInfo_t *leftKid;   /* Left sub-formula */
162  AbsVertexInfo_t *rightKid;  /* Right sub-formula */
163  lsList parent;              /* Pointers to the parent formulas */
164  union {
165    struct {
166      st_table *solutions;    /* Already computed results */
167    } exData;
168    struct {
169      int varId;              /* Variable id */
170      mdd_t *goalSet;         /* States that need to be include/excluded */
171    } varData;
172    struct {
173      AbsVertexInfo_t *fpVar; /* Right sub-formula */
174      array_t *rings;         /* mdd_ts computed in the fixed point */
175      array_t *ringApprox;    /* Approximations made in the rings */
176      array_t *subApprox;     /* Approximation made from the previous
177                                 iteration */
178      boolean useExtraCareSet;/* Use care set ala reachability */
179    } fpData;
180    struct {
181      char *name;             /* name of the id */
182      char *value;            /* value of the id */
183    } idData;
184  } vertexData;
185};
186
187/**Struct**********************************************************************
188
189  Synopsis [Structure to store the information needed in the overall
190  verification process.]
191
192  Description [Some of these fields are owned by the package, that is, they are
193  created inside the Abs code, and some others are just pointers to other data
194  structures not created in abs. The allocation and free procedures take care
195  of that by de-allocating only the structures locally created. The overall
196  algorithm also performs a series of image computations. Because of the high
197  number of re-evaluation of formulas, the overall algorithm keeps a table
198  storing the results of previous image computations. This table is global to
199  the entire algorithm, therefore, any image computation that is performed at
200  any point checks first if the result is already in the "imageCache" table.]
201
202  SeeAlso [AbsCtlFormulaArrayTranslate AbsSubFormulaRefine AbsSubFormulaVerify]
203
204******************************************************************************/
205struct AbsVerificationInfo {
206  Ntk_Network_t   *network;      /* Pointer to network. Not owned */
207  graph_t         *partition;    /* Pointer to the partition. Not owned */
208  mdd_manager     *mddManager;   /* Manager. Not Owned */
209  Fsm_Fsm_t       *fsm;          /* Fsm being considered. Not Owned */
210  int             numStateVars;  /* Number of bdd state variables */
211  Fsm_Fsm_t       *approxFsm;    /* Approximate FSM. Not Owned */
212  st_table        *stateVars;    /* Table with the state variable ids. Owned */
213  st_table        *quantifyVars; /* Variables to Quantify. Owned */
214  mdd_t           *careSet;      /* Global care set */
215  mdd_t           *tmpCareSet;   /* Temporary care set */
216  st_table        *imageCache;   /* To store the image computations */
217  AbsVertexCatalog_t *catalog;   /* Catalog to detect common sub-formulas */
218  AbsStats_t      *stats;        /* Statistics gathered during execution */
219  AbsOptions_t    *options;      /* Command line options */
220};
221
222/**Struct**********************************************************************
223
224  Synopsis    [Structure for storing the command line options.]
225
226  SeeAlso     [AbsVerificationInfo]
227
228******************************************************************************/
229struct AbsOptions {
230  long verbosity;       /* Level of verbosity throughout the verification */
231  int timeOut;          /* Time limit in the execution */
232  boolean reachability; /* Do reachability analysis prior to verification */
233  boolean envelope;     /* Compute EG(true) as the first formula */
234  char *fileName;       /* File to read the formulas from */
235  char *fairFileName;   /* File to read the fairness constraints for FCTL */
236  boolean exact;        /* Perform exact verification */
237  boolean printStats;   /* Print the stats after verification */
238  boolean minimizeIterate; /* Minimize the iterates of the fixed points */
239  boolean negateFormula; /* Verify the negation of the formula instead */
240  boolean partApprox;   /* Use partition transition relation approximation */
241};
242
243/**Struct**********************************************************************
244
245  Synopsis    [Structure to store statistics about the algorithm.]
246
247  Description [The statistics collected through execution will be stored in
248  this structure which itself is stored inside the AbsVerificationInfo_t
249  structure.]
250
251  SeeAlso     [AbsVerificationInfo_t]
252
253******************************************************************************/
254struct AbsStats {
255  int numReorderings;   /* Number of BDD variable re-orderings performed */
256  int evalFixedPoint;   /* Number of FixedPoint vertex evaluations */
257  int evalAnd;          /* Number of And vertex evaluations*/
258  int evalNot;          /* Number of Not vertex evaluations*/
259  int evalPreImage;     /* Number of PreImage vertex evaluations*/
260  int evalIdentifier;   /* Number of Identifier vertex evaluations*/
261  int evalVariable;     /* Number of Variable vertex evaluations*/
262  int refineFixedPoint; /* Number of FixedPoint vertex refinements */
263  int refineAnd;        /* Number of And vertex refinements */
264  int refineNot;        /* Number of Not vertex refinements */
265  int refinePreImage;   /* Number of PreImage vertex refinements */
266  int refineIdentifier; /* Number of Identifier vertex refinements */
267  int refineVariable;   /* Number of Variable vertex refinements */
268  int exactPreImage;    /* Number of exact pre-image computations */
269  int approxPreImage;   /* Number of approximate pre-image computations */
270  int exactImage;       /* Number of exact image computations */
271  int preImageCacheEntries; /* Size of the pre-image cache */
272  int imageCacheEntries;    /* Size of the image cache */
273  long imageCpuTime;        /* CPU time spent in exact image computation */
274  long preImageCpuTime;     /* CPU time spent in exact pre-image computation */
275  long appPreCpuTime;       /* CPU time spent in approximate pre-image comp. */
276};
277
278/**Struct**********************************************************************
279
280  Synopsis    [Cache entry for image and pre-image cache]
281
282  SeeAlso     [AbsSubFormulaRefine]
283
284******************************************************************************/
285struct AbsEvalCacheEntry {
286  mdd_t *key;      /* BDD operand */
287  boolean approx;  /* Is it an approximation? */
288  int complement;  /* Is it complemented? */
289  mdd_t *result;   /* Result BDD */
290  mdd_t *careSet;  /* Care set used for the computation */
291};
292
293
294/*---------------------------------------------------------------------------*/
295/* Macro declarations                                                        */
296/*---------------------------------------------------------------------------*/
297
298/**Macro***********************************************************************
299
300  Synopsis [Macro to read the vertexType field from a AbsVertexInfo_t
301  structure.]
302
303  SideEffects  []
304
305******************************************************************************/
306#define AbsVertexReadType(      \
307  /* AbsVertexInfo_t * */ sfPtr \
308)                               \
309    ((sfPtr)->vertexType)
310
311/**Macro***********************************************************************
312
313  Synopsis [Macro to read the vertexId field from a AbsVertexInfo_t
314  structure.]
315
316  SideEffects  []
317
318  SeeAlso      []
319
320******************************************************************************/
321#define AbsVertexReadId(        \
322  /* AbsVertexInfo_t * */ sfPtr \
323)                               \
324    ((sfPtr)->vertexId)
325
326/**Macro***********************************************************************
327
328  Synopsis [Macro to read the sat field from a AbsVertexInfo_t structure.]
329
330  SideEffects  []
331
332  SeeAlso      [AbsVertexInfo]
333
334******************************************************************************/
335#define AbsVertexReadSat(       \
336  /* AbsVertexInfo_t * */ sfPtr \
337)                               \
338    ((sfPtr)->sat)
339
340/**Macro***********************************************************************
341
342  Synopsis [Macro to read the references field from a AbsVertexInfo_t
343  structure.]
344
345  SideEffects  []
346
347  SeeAlso      [AbsVertexInfo]
348
349******************************************************************************/
350#define AbsVertexReadRefs(      \
351  /* AbsVertexInfo_t * */ sfPtr \
352)                               \
353    ((sfPtr)->refs)
354
355/**Macro***********************************************************************
356
357  Synopsis [Macro to read the served field from a AbsVertexInfo_t
358  structure.]
359
360  SideEffects  []
361
362  SeeAlso      [AbsVertexInfo]
363
364******************************************************************************/
365#define AbsVertexReadServed(    \
366  /* AbsVertexInfo_t * */ sfPtr \
367)                               \
368    ((sfPtr)->served)
369
370/**Macro***********************************************************************
371
372  Synopsis [Macro to read the polarity field from a AbsVertexInfo_t structure.]
373
374  SideEffects  []
375
376  SeeAlso      [AbsVertexInfo]
377
378******************************************************************************/
379#define AbsVertexReadPolarity(  \
380  /* AbsVertexInfo_t * */ sfPtr \
381)                               \
382    ((sfPtr)->polarity)
383
384/**Macro***********************************************************************
385
386  Synopsis [Macro to read the depth field from a AbsVertexInfo_t structure.]
387
388  SideEffects  []
389
390  SeeAlso      [AbsVertexInfo]
391
392******************************************************************************/
393#define AbsVertexReadDepth(     \
394  /* AbsVertexInfo_t * */ sfPtr \
395)                               \
396    ((sfPtr)->depth)
397
398
399/**Macro***********************************************************************
400
401  Synopsis [Macro to read the localApprox field from a AbsVertexInfo_t
402  structure.]
403
404  SideEffects  []
405
406  SeeAlso      [AbsVertexInfo]
407
408******************************************************************************/
409#define AbsVertexReadLocalApprox( \
410  /* AbsVertexInfo_t * */ sfPtr   \
411)                                 \
412    ((sfPtr)->localApprox)
413
414/**Macro***********************************************************************
415
416  Synopsis [Macro to read the globalApprox field from a AbsVertexInfo_t
417  structure.]
418
419  SideEffects  []
420
421  SeeAlso      [AbsVertexInfo]
422
423******************************************************************************/
424#define AbsVertexReadGlobalApprox( \
425  /* AbsVertexInfo_t * */ sfPtr    \
426)                                  \
427    ((sfPtr)->globalApprox)
428
429/**Macro***********************************************************************
430
431  Synopsis [Macro to read the constant field from a AbsVertexInfo_t
432  structure.]
433
434  SideEffects  []
435
436  SeeAlso      [AbsVertexInfo]
437
438******************************************************************************/
439#define AbsVertexReadConstant(  \
440  /* AbsVertexInfo_t * */ sfPtr \
441)                               \
442    ((sfPtr)->constant)
443
444/**Macro***********************************************************************
445
446  Synopsis [Macro to read the trueRefine field from a AbsVertexInfo_t
447  structure.]
448
449  SideEffects  []
450
451  SeeAlso      [AbsVertexInfo]
452
453******************************************************************************/
454#define AbsVertexReadTrueRefine( \
455  /* AbsVertexInfo_t * */ sfPtr  \
456)                                \
457    ((sfPtr)->trueRefine)
458
459/**Macro***********************************************************************
460
461  Synopsis [Macro to read the leftKid field from a AbsVertexInfo_t structure.]
462
463  SideEffects  []
464
465  SeeAlso      [AbsVertexInfo]
466
467******************************************************************************/
468#define AbsVertexReadLeftKid(   \
469  /* AbsVertexInfo_t * */ sfPtr \
470)                               \
471    ((sfPtr)->leftKid)
472
473/**Macro***********************************************************************
474
475  Synopsis [Macro to read the rightKid field from a AbsVertexInfo_t structure.]
476
477  SideEffects  []
478
479  SeeAlso      [AbsVertexInfo]
480
481******************************************************************************/
482#define AbsVertexReadRightKid(  \
483  /* AbsVertexInfo_t * */ sfPtr \
484)                               \
485    ((sfPtr)->rightKid)
486
487/**Macro***********************************************************************
488
489  Synopsis [Macro to read the parent field from a AbsVertexInfo_t structure.]
490
491  SideEffects  []
492
493  SeeAlso      [AbsVertexInfo]
494
495******************************************************************************/
496#define AbsVertexReadParent(    \
497  /* AbsVertexInfo_t * */ sfPtr \
498)                               \
499    ((sfPtr)->parent)
500
501/**Macro***********************************************************************
502
503  Synopsis [Macro to read the solutions field from a AbsVertexInfo_t
504  structure.]
505
506  SideEffects  []
507
508  SeeAlso      [AbsVertexInfo]
509
510******************************************************************************/
511#define AbsVertexReadSolutions( \
512  /* AbsVertexInfo_t * */ sfPtr \
513)                               \
514    ((sfPtr)->vertexData.exData.solutions)
515
516/**Macro***********************************************************************
517
518  Synopsis [Macro to read the varId field from a AbsVertexInfo_t
519  structure.]
520
521  SideEffects  []
522
523  SeeAlso      [AbsVertexInfo]
524
525******************************************************************************/
526#define AbsVertexReadVarId(     \
527  /* AbsVertexInfo_t * */ sfPtr \
528)                               \
529    ((sfPtr)->vertexData.varData.varId)
530
531/**Macro***********************************************************************
532
533  Synopsis [Macro to read the goalSet field from a AbsVertexInfo_t structure.]
534
535  SideEffects  []
536
537  SeeAlso      [AbsVertexInfo]
538
539******************************************************************************/
540#define AbsVertexReadGoalSet(   \
541  /* AbsVertexInfo_t * */ sfPtr \
542)                               \
543    ((sfPtr)->vertexData.varData.goalSet)
544
545/**Macro***********************************************************************
546
547  Synopsis [Macro to read the fpVar field from a AbsVertexInfo_t structure.]
548
549  SideEffects  []
550
551  SeeAlso      [AbsVertexInfo]
552
553******************************************************************************/
554#define AbsVertexReadFpVar(     \
555  /* AbsVertexInfo_t * */ sfPtr \
556)                               \
557    ((sfPtr)->vertexData.fpData.fpVar)
558
559/**Macro***********************************************************************
560
561  Synopsis [Macro to read the rings field from a AbsVertexInfo_t structure.]
562
563  SideEffects  []
564
565  SeeAlso      [AbsVertexInfo]
566
567******************************************************************************/
568#define AbsVertexReadRings(     \
569  /* AbsVertexInfo_t * */ sfPtr \
570)                               \
571    ((sfPtr)->vertexData.fpData.rings)
572
573/**Macro***********************************************************************
574
575  Synopsis [Macro to fetch an element from the rings field from a
576  AbsVertexInfo_t structure.]
577
578  SideEffects  []
579
580  SeeAlso      [AbsVertexInfo]
581
582******************************************************************************/
583#define AbsVertexFetchRing(      \
584  /* AbsVertexInfo_t * */ sfPtr, \
585  /* int */ index                \
586)                                \
587    (array_fetch(mdd_t *, ((sfPtr)->vertexData.fpData.rings), (index)))
588
589/**Macro***********************************************************************
590
591  Synopsis [Macro to read the ringApprox field from a AbsVertexInfo_t
592  structure.]
593
594  SideEffects  []
595
596  SeeAlso      [AbsVertexInfo]
597
598******************************************************************************/
599#define AbsVertexReadRingApprox( \
600  /* AbsVertexInfo_t * */ sfPtr  \
601)                                \
602    ((sfPtr)->vertexData.fpData.ringApprox)
603
604/**Macro***********************************************************************
605
606  Synopsis [Macro to fetch an element from the ringApprox field from a
607  AbsVertexInfo_t structure.]
608
609  SideEffects  []
610
611  SeeAlso      [AbsVertexInfo]
612
613******************************************************************************/
614#define AbsVertexFetchRingApprox( \
615  /* AbsVertexInfo_t * */ sfPtr,  \
616  /* int */ index                 \
617)                                 \
618    (array_fetch(boolean, ((sfPtr)->vertexData.fpData.ringApprox), (index)))
619
620/**Macro***********************************************************************
621
622  Synopsis [Macro to read the subApprox field from a AbsVertexInfo_t
623  structure.]
624
625  SideEffects  []
626
627  SeeAlso      [AbsVertexInfo]
628
629******************************************************************************/
630#define AbsVertexReadSubApprox( \
631  /* AbsVertexInfo_t * */ sfPtr \
632)                               \
633    ((sfPtr)->vertexData.fpData.subApprox)
634
635/**Macro***********************************************************************
636
637  Synopsis [Macro to fetch an element from the subApprox field from a
638  AbsVertexInfo_t structure.]
639
640  SideEffects  []
641
642  SeeAlso      [AbsVertexInfo]
643
644******************************************************************************/
645#define AbsVertexFetchSubApprox( \
646  /* AbsVertexInfo_t * */ sfPtr, \
647  /* int */ index                \
648)                                \
649    (array_fetch(boolean, ((sfPtr)->vertexData.fpData.subApprox), (index)))
650
651/**Macro***********************************************************************
652
653  Synopsis [Macro to read the useExtraCareSet field from a AbsVertexInfo_t
654  structure.]
655
656  SideEffects  []
657
658  SeeAlso      [AbsVertexInfo]
659
660******************************************************************************/
661#define AbsVertexReadUseExtraCareSet( \
662  /* AbsVertexInfo_t * */ sfPtr       \
663)                                     \
664    ((sfPtr)->vertexData.fpData.useExtraCareSet)
665
666/**Macro***********************************************************************
667
668  Synopsis [Macro to read the name field from a AbsVertexInfo_t
669  structure.]
670
671  SideEffects  []
672
673  SeeAlso      [AbsVertexInfo]
674
675******************************************************************************/
676#define AbsVertexReadName(      \
677  /* AbsVertexInfo_t * */ sfPtr \
678)                               \
679    ((sfPtr)->vertexData.idData.name)
680
681/**Macro***********************************************************************
682
683  Synopsis [Macro to read the value field from a AbsVertexInfo_t
684  structure.]
685
686  SideEffects  []
687
688  SeeAlso      [AbsVertexInfo]
689
690******************************************************************************/
691#define AbsVertexReadValue(     \
692  /* AbsVertexInfo_t * */ sfPtr \
693)                               \
694    ((sfPtr)->vertexData.idData.value)
695
696/**Macro***********************************************************************
697
698  Synopsis     [Macro to set the vertexType field from a AbsVertexInfo_t
699  structure.]
700
701  SideEffects  []
702
703  SeeAlso      [AbsVertexInfo]
704
705******************************************************************************/
706#define AbsVertexSetType(        \
707  /* AbsVertexInfo_t * */ sfPtr, \
708  /* AbsVertex_t */ vtype        \
709)                                \
710    ((sfPtr)->vertexType) = (vtype)
711
712/**Macro***********************************************************************
713
714  Synopsis     [Macro to set the vertexId field from a AbsVertexInfo_t
715  structure.]
716
717  SideEffects  []
718
719  SeeAlso      [AbsVertexInfo]
720
721******************************************************************************/
722#define AbsVertexSetId(          \
723  /* AbsVertexInfo_t * */ sfPtr, \
724  /* int */ data                 \
725)                                \
726    ((sfPtr)->vertexId) = (data)
727
728/**Macro***********************************************************************
729
730  Synopsis [Macro to set the sat field from a AbsVertexInfo_t structure.]
731
732  SideEffects  []
733
734  SeeAlso      [AbsVertexInfo]
735
736******************************************************************************/
737#define AbsVertexSetSat(         \
738  /* AbsVertexInfo_t * */ sfPtr, \
739  /* mdd_t * */ set              \
740)                                \
741    ((sfPtr)->sat) = (set)
742
743/**Macro***********************************************************************
744
745  Synopsis [Macro to set the refs field from a AbsVertexInfo_t structure.]
746
747  SideEffects  []
748
749  SeeAlso      [AbsVertexInfo]
750
751******************************************************************************/
752#define AbsVertexSetRefs(        \
753  /* AbsVertexInfo_t * */ sfPtr, \
754  /* boolean */ data             \
755)                                \
756    ((sfPtr)->refs) = (data)
757
758/**Macro***********************************************************************
759
760  Synopsis [Macro to set the served field from a AbsVertexInfo_t structure.]
761
762  SideEffects  []
763
764  SeeAlso      [AbsVertexInfo]
765
766******************************************************************************/
767#define AbsVertexSetServed(      \
768  /* AbsVertexInfo_t * */ sfPtr, \
769  /* boolean */ data             \
770)                                \
771    ((sfPtr)->served) = (data)
772
773/**Macro***********************************************************************
774
775  Synopsis [Macro to set the polarity field from a AbsVertexInfo_t structure.]
776
777  SideEffects  []
778
779  SeeAlso      [AbsVertexInfo]
780
781******************************************************************************/
782#define AbsVertexSetPolarity(    \
783  /* AbsVertexInfo_t * */ sfPtr, \
784  /* boolean */ data             \
785)                                \
786    ((sfPtr)->polarity) = (data)
787
788/**Macro***********************************************************************
789
790  Synopsis [Macro to set the depth field from a AbsVertexInfo_t structure.]
791
792  SideEffects  []
793
794  SeeAlso      [AbsVertexInfo]
795
796******************************************************************************/
797#define AbsVertexSetDepth(       \
798  /* AbsVertexInfo_t * */ sfPtr, \
799  /* int */ data                 \
800)                                \
801    ((sfPtr)->depth) = (data)
802
803
804/**Macro***********************************************************************
805
806  Synopsis [Macro to set the localApprox field from a AbsVertexInfo_t
807  structure.]
808
809  SideEffects  []
810
811  SeeAlso      [AbsVertexInfo]
812
813******************************************************************************/
814#define AbsVertexSetLocalApprox( \
815  /* AbsVertexInfo_t * */ sfPtr, \
816  /* boolean */ data             \
817)                                \
818    ((sfPtr)->localApprox) = (data)
819
820/**Macro***********************************************************************
821
822  Synopsis [Macro to set the globalApprox field from a AbsVertexInfo_t
823  structure.]
824
825  SideEffects  []
826
827  SeeAlso      [AbsVertexInfo]
828
829******************************************************************************/
830#define AbsVertexSetGlobalApprox( \
831  /* AbsVertexInfo_t * */ sfPtr,  \
832  /* boolean */ data              \
833)                                 \
834    ((sfPtr)->globalApprox) = (data)
835
836/**Macro***********************************************************************
837
838  Synopsis [Macro to set the constant field from a AbsVertexInfo_t
839  structure.]
840
841  SideEffects  []
842
843  SeeAlso      [AbsVertexInfo]
844
845******************************************************************************/
846#define AbsVertexSetConstant(    \
847  /* AbsVertexInfo_t * */ sfPtr, \
848  /* boolean */ data             \
849)                                \
850    ((sfPtr)->constant) = (data)
851
852/**Macro***********************************************************************
853
854  Synopsis [Macro to set the trueRefine field from a AbsVertexInfo_t
855  structure.]
856
857  SideEffects  []
858
859  SeeAlso      [AbsVertexInfo]
860
861******************************************************************************/
862#define AbsVertexSetTrueRefine(  \
863  /* AbsVertexInfo_t * */ sfPtr, \
864  /* boolean */ data             \
865)                                \
866    ((sfPtr)->trueRefine) = (data)
867
868/**Macro***********************************************************************
869
870  Synopsis [Macro to set the leftKid field from a AbsVertexInfo_t structure.]
871
872  SideEffects  []
873
874  SeeAlso      [AbsVertexInfo]
875
876******************************************************************************/
877#define AbsVertexSetLeftKid(            \
878  /* AbsVertexInfo_t * */ sfPtr,        \
879  /* AbsVertexInfo_t * */ subFormulaPtr \
880)                                       \
881    ((sfPtr)->leftKid) = (subFormulaPtr)
882
883/**Macro***********************************************************************
884
885  Synopsis [Macro to set the rightKid field from a AbsVertexInfo_t structure.]
886
887  SideEffects  []
888
889  SeeAlso      [AbsVertexInfo]
890
891******************************************************************************/
892#define AbsVertexSetRightKid(           \
893  /* AbsVertexInfo_t * */ sfPtr,        \
894  /* AbsVertexInfo_t * */ subFormulaPtr \
895)                                       \
896    ((sfPtr)->rightKid) = (subFormulaPtr)
897
898/**Macro***********************************************************************
899
900  Synopsis [Macro to set the parent field from a AbsVertexInfo_t structure.]
901
902  SideEffects  []
903
904  SeeAlso      [AbsVertexInfo]
905
906******************************************************************************/
907#define AbsVertexSetParent(             \
908  /* AbsVertexInfo_t * */ sfPtr,        \
909  /* AbsVertexInfo_t * */ subFormulaPtr \
910)                                       \
911    lsNewBegin(((sfPtr)->parent), (lsGeneric)subFormulaPtr, NIL(lsHandle))
912
913/**Macro***********************************************************************
914
915  Synopsis [Macro to set the solutions field from a AbsVertexInfo_t
916  structure.]
917
918  SideEffects  []
919
920  SeeAlso      [AbsVertexInfo]
921
922******************************************************************************/
923#define AbsVertexSetSolutions(   \
924  /* AbsVertexInfo_t * */ sfPtr, \
925  /* array_t * */ data           \
926)                                \
927    ((sfPtr)->vertexData.exData.solutions) = (data)
928
929/**Macro***********************************************************************
930
931  Synopsis [Macro to set the varId field from a AbsVertexInfo_t
932  structure.]
933
934  SideEffects  []
935
936  SeeAlso      [AbsVertexInfo]
937
938******************************************************************************/
939#define AbsVertexSetVarId(       \
940  /* AbsVertexInfo_t * */ sfPtr, \
941  /* array_t * */ data           \
942)                                \
943    ((sfPtr)->vertexData.varData.varId) = (data)
944
945/**Macro***********************************************************************
946
947  Synopsis [Macro to set the goalSet field from a AbsVertexInfo_t structure.]
948
949  SideEffects  []
950
951  SeeAlso      [AbsVertexInfo]
952
953******************************************************************************/
954#define AbsVertexSetGoalSet(     \
955  /* AbsVertexInfo_t * */ sfPtr, \
956  /* mdd_t * */ set              \
957)                                \
958    ((sfPtr)->vertexData.varData.goalSet) = (set)
959
960/**Macro***********************************************************************
961
962  Synopsis [Macro to set the fpVar field from a AbsVertexInfo_t structure.]
963
964  SideEffects  []
965
966  SeeAlso      [AbsVertexInfo]
967
968******************************************************************************/
969#define AbsVertexSetFpVar(       \
970  /* AbsVertexInfo_t * */ sfPtr, \
971  /* int */ data                 \
972)                                \
973    ((sfPtr)->vertexData.fpData.fpVar) = (data)
974
975/**Macro***********************************************************************
976
977  Synopsis [Macro to set the rings field from a AbsVertexInfo_t structure.]
978
979  SideEffects  []
980
981  SeeAlso      [AbsVertexInfo]
982
983******************************************************************************/
984#define AbsVertexSetRings(       \
985  /* AbsVertexInfo_t * */ sfPtr, \
986  /* array_t * */ data           \
987)                                \
988    ((sfPtr)->vertexData.fpData.rings) = (data)
989
990/**Macro***********************************************************************
991
992  Synopsis [Macro to insert a ring in the rings field from a AbsVertexInfo_t
993  structure.]
994
995  SideEffects  []
996
997  SeeAlso      [AbsVertexInfo]
998
999******************************************************************************/
1000#define AbsVertexInsertRing(     \
1001  /* AbsVertexInfo_t * */ sfPtr, \
1002  /* array_t * */ data           \
1003)                                \
1004    array_insert_last(mdd_t *, ((sfPtr)->vertexData.fpData.rings), (data))
1005
1006/**Macro***********************************************************************
1007
1008  Synopsis [Macro to set the ringApprox field from a AbsVertexInfo_t
1009  structure.]
1010
1011  SideEffects  []
1012
1013  SeeAlso      [AbsVertexInfo]
1014
1015******************************************************************************/
1016#define AbsVertexSetRingApprox(  \
1017  /* AbsVertexInfo_t * */ sfPtr, \
1018  /* array_t * */ data           \
1019)                                \
1020    ((sfPtr)->vertexData.fpData.ringApprox) = (data)
1021
1022/**Macro***********************************************************************
1023
1024  Synopsis [Macro to insert an element in the ringApprox field from a
1025  AbsVertexInfo_t structure.]
1026
1027  SideEffects  []
1028
1029  SeeAlso      [AbsVertexInfo]
1030
1031******************************************************************************/
1032#define AbsVertexInsertRingApprox( \
1033  /* AbsVertexInfo_t * */ sfPtr,   \
1034  /* array_t * */ data             \
1035)                                  \
1036    array_insert_last(boolean, ((sfPtr)->vertexData.fpData.ringApprox), (data))
1037
1038/**Macro***********************************************************************
1039
1040  Synopsis [Macro to set the subApprox field from a AbsVertexInfo_t
1041  structure.]
1042
1043  SideEffects  []
1044
1045  SeeAlso      [AbsVertexInfo]
1046
1047******************************************************************************/
1048#define AbsVertexSetSubApprox(   \
1049  /* AbsVertexInfo_t * */ sfPtr, \
1050  /* array_t * */ data           \
1051)                                \
1052    ((sfPtr)->vertexData.fpData.subApprox) = (data)
1053
1054/**Macro***********************************************************************
1055
1056  Synopsis [Macro to insert an element in the subApprox field from a
1057  AbsVertexInfo_t structure.]
1058
1059  SideEffects  []
1060
1061  SeeAlso      [AbsVertexInfo]
1062
1063******************************************************************************/
1064#define AbsVertexInsertSubApprox( \
1065  /* AbsVertexInfo_t * */ sfPtr,  \
1066  /* array_t * */ data            \
1067)                                 \
1068    array_insert_last(boolean, ((sfPtr)->vertexData.fpData.subApprox), (data))
1069
1070/**Macro***********************************************************************
1071
1072  Synopsis [Macro to set the useExtraCareSet field from a AbsVertexInfo_t
1073  structure.]
1074
1075  SideEffects  []
1076
1077  SeeAlso      [AbsVertexInfo]
1078
1079******************************************************************************/
1080#define AbsVertexSetUseExtraCareSet( \
1081  /* AbsVertexInfo_t * */ sfPtr,     \
1082  /* int */ data                     \
1083)                                    \
1084    ((sfPtr)->vertexData.fpData.useExtraCareSet) = (data)
1085
1086/**Macro***********************************************************************
1087
1088  Synopsis [Macro to set the name field from a AbsVertexInfo_t
1089  structure.]
1090
1091  SideEffects  []
1092
1093  SeeAlso      [AbsVertexInfo]
1094
1095******************************************************************************/
1096#define AbsVertexSetName(        \
1097  /* AbsVertexInfo_t * */ sfPtr, \
1098  /* int */ data                 \
1099)                                \
1100    ((sfPtr)->vertexData.idData.name) = (data)
1101
1102/**Macro***********************************************************************
1103
1104  Synopsis [Macro to set the value field from a AbsVertexInfo_t
1105  structure.]
1106
1107  SideEffects  []
1108
1109  SeeAlso      [AbsVertexInfo]
1110
1111******************************************************************************/
1112#define AbsVertexSetValue(       \
1113  /* AbsVertexInfo_t * */ sfPtr, \
1114  /* int */ data                 \
1115)                                \
1116    ((sfPtr)->vertexData.idData.value) = (data)
1117
1118/**Macro***********************************************************************
1119
1120  Synopsis [Macro to read the network field from a Abs_VerificationInfo_t
1121  structure.]
1122
1123  SideEffects  []
1124
1125  SeeAlso      [Abs_VerificationInfo_t]
1126
1127******************************************************************************/
1128#define AbsVerificationInfoReadNetwork( \
1129  /* Abs_VerificationInfo_t * */ vInfo  \
1130)                                       \
1131    ((vInfo)->network)
1132
1133/**Macro***********************************************************************
1134
1135  Synopsis [Macro to read the partition field from a Abs_VerificationInfo_t
1136  structure.]
1137
1138  SideEffects  []
1139
1140  SeeAlso      [Abs_VerificationInfo_t]
1141
1142******************************************************************************/
1143#define AbsVerificationInfoReadPartition( \
1144  /* Abs_VerificationInfo_t * */ vInfo    \
1145)                                         \
1146    ((vInfo)->partition)
1147
1148/**Macro***********************************************************************
1149
1150  Synopsis [Macro to read the fsm field from a Abs_VerificationInfo_t
1151  structure.]
1152
1153  SideEffects  []
1154
1155  SeeAlso      [Abs_VerificationInfo_t]
1156
1157******************************************************************************/
1158#define AbsVerificationInfoReadFsm(    \
1159  /* Abs_VerificationInfo_t * */ vInfo \
1160)                                      \
1161    ((vInfo)->fsm)
1162
1163/**Macro***********************************************************************
1164
1165  Synopsis [Macro to read the numStateVars field from a Abs_VerificationInfo_t
1166  structure.]
1167
1168  SideEffects  []
1169
1170  SeeAlso      [Abs_VerificationInfo_t]
1171
1172******************************************************************************/
1173#define AbsVerificationInfoReadNumStateVars(    \
1174  /* Abs_VerificationInfo_t * */ vInfo \
1175)                                      \
1176    ((vInfo)->numStateVars)
1177
1178/**Macro***********************************************************************
1179
1180  Synopsis [Macro to read the approxFsm field from a Abs_VerificationInfo_t
1181  structure.]
1182
1183  SideEffects  []
1184
1185  SeeAlso      [Abs_VerificationInfo_t]
1186
1187******************************************************************************/
1188#define AbsVerificationInfoReadApproxFsm( \
1189  /* Abs_VerificationInfo_t * */ vInfo    \
1190)                                         \
1191    ((vInfo)->approxFsm)
1192
1193/**Macro***********************************************************************
1194
1195  Synopsis [Macro to read the stateVars field from a Abs_VerificationInfo_t
1196  structure.]
1197
1198  SideEffects  []
1199
1200  SeeAlso      [Abs_VerificationInfo_t]
1201
1202******************************************************************************/
1203#define AbsVerificationInfoReadStateVars( \
1204  /* Abs_VerificationInfo_t * */ vInfo    \
1205)                                         \
1206    ((vInfo)->stateVars)
1207
1208/**Macro***********************************************************************
1209
1210  Synopsis [Macro to read the quantifyVars field from a Abs_VerificationInfo_t
1211  structure.]
1212
1213  SideEffects  []
1214
1215  SeeAlso      [Abs_VerificationInfo_t]
1216
1217******************************************************************************/
1218#define AbsVerificationInfoReadQuantifyVars( \
1219  /* Abs_VerificationInfo_t * */ vInfo       \
1220)                                            \
1221    ((vInfo)->quantifyVars)
1222
1223/**Macro***********************************************************************
1224
1225  Synopsis [Macro to read the careSet field from a Abs_VerificationInfo_t
1226  structure.]
1227
1228  SideEffects  []
1229
1230  SeeAlso      [Abs_VerificationInfo_t]
1231
1232******************************************************************************/
1233#define AbsVerificationInfoReadCareSet( \
1234  /* Abs_VerificationInfo_t * */ vInfo  \
1235)                                       \
1236    ((vInfo)->careSet)
1237
1238/**Macro***********************************************************************
1239
1240  Synopsis [Macro to read the tmpCareSet field from a Abs_VerificationInfo_t
1241  structure.]
1242
1243  SideEffects  []
1244
1245  SeeAlso      [Abs_VerificationInfo_t]
1246
1247******************************************************************************/
1248#define AbsVerificationInfoReadTmpCareSet( \
1249  /* Abs_VerificationInfo_t * */ vInfo     \
1250)                                          \
1251    ((vInfo)->tmpCareSet)
1252
1253/**Macro***********************************************************************
1254
1255  Synopsis [Macro to read the imageCache field from a Abs_VerificationInfo_t
1256  structure.]
1257
1258  SideEffects  []
1259
1260  SeeAlso      [Abs_VerificationInfo_t]
1261
1262******************************************************************************/
1263#define AbsVerificationInfoReadImageCache( \
1264  /* Abs_VerificationInfo_t * */ vInfo     \
1265)                                          \
1266    ((vInfo)->imageCache)
1267
1268/**Macro***********************************************************************
1269
1270  Synopsis [Macro to read the mddManager field from a Abs_VerificationInfo_t
1271  structure.]
1272
1273  SideEffects  []
1274
1275  SeeAlso      [Abs_VerificationInfo_t]
1276
1277******************************************************************************/
1278#define AbsVerificationInfoReadMddManager( \
1279  /* Abs_VerificationInfo_t * */ vInfo     \
1280)                                          \
1281    ((vInfo)->mddManager)
1282
1283/**Macro***********************************************************************
1284
1285  Synopsis [Macro to read the catalog field from a Abs_VerificationInfo_t
1286  structure.]
1287
1288  SideEffects  []
1289
1290  SeeAlso      [Abs_VerificationInfo_t]
1291
1292******************************************************************************/
1293#define AbsVerificationInfoReadCatalog( \
1294  /* Abs_VerificationInfo_t * */ vInfo  \
1295)                                       \
1296    ((vInfo)->catalog)
1297
1298/**Macro***********************************************************************
1299
1300  Synopsis [Macro to read the stats field from a Abs_VerificationInfo_t
1301  structure.]
1302
1303  SideEffects  []
1304
1305  SeeAlso      [Abs_VerificationInfo_t]
1306
1307******************************************************************************/
1308#define AbsVerificationInfoReadStats(  \
1309  /* Abs_VerificationInfo_t * */ vInfo \
1310)                                      \
1311    ((vInfo)->stats)
1312
1313/**Macro***********************************************************************
1314
1315  Synopsis [Macro to read the options field from a Abs_VerificationInfo_t
1316  structure.]
1317
1318  SideEffects  []
1319
1320  SeeAlso      [Abs_VerificationInfo_t]
1321
1322******************************************************************************/
1323#define AbsVerificationInfoReadOptions( \
1324  /* Abs_VerificationInfo_t * */ vInfo  \
1325)                                       \
1326    ((vInfo)->options)
1327
1328/**Macro***********************************************************************
1329
1330  Synopsis     [Macro to set the network field from a Abs_VerificationInfo_t
1331  structure.]
1332
1333  SideEffects  []
1334
1335  SeeAlso      [Abs_VerificationInfo_t]
1336
1337******************************************************************************/
1338#define AbsVerificationInfoSetNetwork(  \
1339  /* Abs_VerificationInfo_t * */ vInfo, \
1340  /* Ntk_Network_t */ data              \
1341)                                       \
1342    ((vInfo)->network) = (data)
1343
1344/**Macro***********************************************************************
1345
1346  Synopsis     [Macro to set the partition field from a Abs_VerificationInfo_t
1347  structure.]
1348
1349  SideEffects  []
1350
1351  SeeAlso      [Abs_VerificationInfo_t]
1352
1353******************************************************************************/
1354#define AbsVerificationInfoSetPartition( \
1355  /* Abs_VerificationInfo_t * */ vInfo,  \
1356  /* graph_t */ data                     \
1357)                                        \
1358    ((vInfo)->partition) = (data)
1359
1360/**Macro***********************************************************************
1361
1362  Synopsis [Macro to set the fsm field from a Abs_VerificationInfo_t
1363  structure.]
1364
1365  SideEffects  []
1366
1367  SeeAlso      [Abs_VerificationInfo_t]
1368
1369******************************************************************************/
1370#define AbsVerificationInfoSetFsm(      \
1371  /* Abs_VerificationInfo_t * */ vInfo, \
1372  /* Fsm_Fsm_t */ data                  \
1373)                                       \
1374    ((vInfo)->fsm) = (data)
1375
1376/**Macro***********************************************************************
1377
1378  Synopsis [Macro to set the numStateVars field from a Abs_VerificationInfo_t
1379  structure.]
1380
1381  SideEffects  []
1382
1383  SeeAlso      [Abs_VerificationInfo_t]
1384
1385******************************************************************************/
1386#define AbsVerificationInfoSetNumStateVars( \
1387  /* Abs_VerificationInfo_t * */ vInfo,     \
1388  /* Fsm_Fsm_t */ data                      \
1389)                                           \
1390    ((vInfo)->numStateVars) = (data)
1391
1392/**Macro***********************************************************************
1393
1394  Synopsis [Macro to set the approxFsm field from a Abs_VerificationInfo_t
1395  structure.]
1396
1397  SideEffects  []
1398
1399  SeeAlso      [Abs_VerificationInfo_t]
1400
1401******************************************************************************/
1402#define AbsVerificationInfoSetApproxFsm( \
1403  /* Abs_VerificationInfo_t * */ vInfo,  \
1404  /* Fsm_Fsm_t */ data                   \
1405)                                        \
1406    ((vInfo)->approxFsm) = (data)
1407
1408/**Macro***********************************************************************
1409
1410  Synopsis     [Macro to set the stateVars field from a Abs_VerificationInfo_t
1411  structure.]
1412
1413  SideEffects  []
1414
1415  SeeAlso      [Abs_VerificationInfo_t]
1416
1417******************************************************************************/
1418#define AbsVerificationInfoSetStateVars( \
1419  /* Abs_VerificationInfo_t * */ vInfo,  \
1420  /* st_table * */ data                  \
1421)                                        \
1422    ((vInfo)->stateVars) = (data)
1423
1424/**Macro***********************************************************************
1425
1426  Synopsis [Macro to set the quantifyVars field from a Abs_VerificationInfo_t
1427  structure.]
1428
1429  SideEffects  []
1430
1431  SeeAlso      [Abs_VerificationInfo_t]
1432
1433******************************************************************************/
1434#define AbsVerificationInfoSetQuantifyVars( \
1435  /* Abs_VerificationInfo_t * */ vInfo,     \
1436  /* st_table **/ data                      \
1437)                                           \
1438    ((vInfo)->quantifyVars) = (data)
1439
1440/**Macro***********************************************************************
1441
1442  Synopsis [Macro to set the careSet field from a Abs_VerificationInfo_t
1443  structure.]
1444
1445  SideEffects  []
1446
1447  SeeAlso      [Abs_VerificationInfo_t]
1448
1449******************************************************************************/
1450#define AbsVerificationInfoSetCareSet( \
1451  /* Abs_VerificationInfo_t * */ vInfo,\
1452  /* st_table **/ data                 \
1453)                                      \
1454    ((vInfo)->careSet) = (data)
1455
1456/**Macro***********************************************************************
1457
1458  Synopsis [Macro to set the tmpCareSet field from a Abs_VerificationInfo_t
1459  structure.]
1460
1461  SideEffects  []
1462
1463  SeeAlso      [Abs_VerificationInfo_t]
1464
1465******************************************************************************/
1466#define AbsVerificationInfoSetTmpCareSet( \
1467  /* Abs_VerificationInfo_t * */ vInfo,   \
1468  /* st_table **/ data                    \
1469)                                         \
1470    ((vInfo)->tmpCareSet) = (data)
1471
1472/**Macro***********************************************************************
1473
1474  Synopsis [Macro to set the imageCache field from a Abs_VerificationInfo_t
1475  structure.]
1476
1477  SideEffects  []
1478
1479  SeeAlso      [Abs_VerificationInfo_t]
1480
1481******************************************************************************/
1482#define AbsVerificationInfoSetImageCache( \
1483  /* Abs_VerificationInfo_t * */ vInfo,   \
1484  /* st_table **/ data                    \
1485)                                         \
1486    ((vInfo)->imageCache) = (data)
1487
1488/**Macro***********************************************************************
1489
1490  Synopsis     [Macro to set the mddManager field from a Abs_VerificationInfo_t
1491  structure.]
1492
1493  SideEffects  []
1494
1495  SeeAlso      [Abs_VerificationInfo_t]
1496
1497******************************************************************************/
1498#define AbsVerificationInfoSetMddManager( \
1499  /* Abs_VerificationInfo_t * */ vInfo,   \
1500  /* mdd_manager * */ data                \
1501)                                         \
1502    ((vInfo)->mddManager) = (data)
1503
1504/**Macro***********************************************************************
1505
1506  Synopsis     [Macro to set the catalog field from a Abs_VerificationInfo_t
1507  structure.]
1508
1509  SideEffects  []
1510
1511  SeeAlso      [Abs_VerificationInfo_t]
1512
1513******************************************************************************/
1514#define AbsVerificationInfoSetCatalog(  \
1515  /* Abs_VerificationInfo_t * */ vInfo, \
1516  /* AbsVertexInfo_t * */ data          \
1517)                                       \
1518    ((vInfo)->catalog) = (data)
1519
1520/**Macro***********************************************************************
1521
1522  Synopsis     [Macro to set the stats field from a Abs_VerificationInfo_t
1523  structure.]
1524
1525  SideEffects  []
1526
1527  SeeAlso      [Abs_VerificationInfo_t]
1528
1529******************************************************************************/
1530#define AbsVerificationInfoSetStats(    \
1531  /* Abs_VerificationInfo_t * */ vInfo, \
1532  /* AbsVertexInfo_t * */ data          \
1533)                                       \
1534    ((vInfo)->stats) = (data)
1535
1536/**Macro***********************************************************************
1537
1538  Synopsis     [Macro to set the options field from a Abs_VerificationInfo_t
1539  structure.]
1540
1541  SideEffects  []
1542
1543  SeeAlso      [Abs_VerificationInfo_t]
1544
1545******************************************************************************/
1546#define AbsVerificationInfoSetOptions(  \
1547  /* Abs_VerificationInfo_t * */ vInfo, \
1548  /* AbsOptions_t * */ data             \
1549)                                       \
1550    ((vInfo)->options) = (data)
1551
1552/**Macro***********************************************************************
1553
1554  Synopsis [Macro to read the verbosity field from a AbsOptions_t structure.]
1555
1556  SideEffects  []
1557
1558  SeeAlso      [AbsOptions]
1559
1560******************************************************************************/
1561#define AbsOptionsReadVerbosity( \
1562  /* AbsOptions_t * */ oInfo     \
1563)                                \
1564    ((oInfo)->verbosity)
1565
1566/**Macro***********************************************************************
1567
1568  Synopsis [Macro to read the timeOut field from a AbsOptions_t
1569  structure.]
1570
1571  SideEffects  []
1572
1573  SeeAlso      [AbsOptions]
1574
1575******************************************************************************/
1576#define AbsOptionsReadTimeOut( \
1577  /* AbsOptions_t * */ oInfo   \
1578)                              \
1579    ((oInfo)->timeOut)
1580
1581/**Macro***********************************************************************
1582
1583  Synopsis [Macro to read the reachability field from a AbsOptions_t
1584  structure.]
1585
1586  SideEffects  []
1587
1588  SeeAlso      [AbsOptions]
1589
1590******************************************************************************/
1591#define AbsOptionsReadReachability( \
1592  /* AbsOptions_t * */ oInfo        \
1593)                                   \
1594    ((oInfo)->reachability)
1595
1596/**Macro***********************************************************************
1597
1598  Synopsis [Macro to read the envelope field from a AbsOptions_t
1599  structure.]
1600
1601  SideEffects  []
1602
1603  SeeAlso      [AbsOptions]
1604
1605******************************************************************************/
1606#define AbsOptionsReadEnvelope( \
1607  /* AbsOptions_t * */ oInfo    \
1608)                               \
1609    ((oInfo)->envelope)
1610
1611/**Macro***********************************************************************
1612
1613  Synopsis [Macro to read the fileName field from a AbsOptions_t
1614  structure.]
1615
1616  SideEffects  []
1617
1618  SeeAlso      [AbsOptions]
1619
1620******************************************************************************/
1621#define AbsOptionsReadFileName( \
1622  /* AbsOptions_t * */ oInfo    \
1623)                               \
1624    ((oInfo)->fileName)
1625
1626/**Macro***********************************************************************
1627
1628  Synopsis [Macro to read the fairFileName field from a AbsOptions_t
1629  structure.]
1630
1631  SideEffects  []
1632
1633  SeeAlso      [AbsOptions]
1634
1635******************************************************************************/
1636#define AbsOptionsReadFairFileName( \
1637  /* AbsOptions_t * */ oInfo        \
1638)                                   \
1639    ((oInfo)->fairFileName)
1640
1641/**Macro***********************************************************************
1642
1643  Synopsis [Macro to read the exact field from a AbsOptions_t
1644  structure.]
1645
1646  SideEffects  []
1647
1648  SeeAlso      [AbsOptions]
1649
1650******************************************************************************/
1651#define AbsOptionsReadExact( \
1652  /* AbsOptions_t * */ oInfo \
1653)                            \
1654    ((oInfo)->exact)
1655
1656/**Macro***********************************************************************
1657
1658  Synopsis [Macro to read the printStats field from a AbsOptions_t structure.]
1659
1660  SideEffects  []
1661
1662  SeeAlso      [AbsOptions]
1663
1664******************************************************************************/
1665#define AbsOptionsReadPrintStats( \
1666  /* AbsOptions_t * */ oInfo      \
1667)                                 \
1668    ((oInfo)->printStats)
1669
1670/**Macro***********************************************************************
1671
1672  Synopsis [Macro to read the minimizeIterate field from a AbsOptions_t
1673  structure.]
1674
1675  SideEffects  []
1676
1677  SeeAlso      [AbsOptions]
1678
1679******************************************************************************/
1680#define AbsOptionsReadMinimizeIterate( \
1681  /* AbsOptions_t * */ oInfo           \
1682)                                      \
1683    ((oInfo)->minimizeIterate)
1684
1685/**Macro***********************************************************************
1686
1687  Synopsis [Macro to read the negateFormula field from a AbsOptions_t
1688  structure.]
1689
1690  SideEffects  []
1691
1692  SeeAlso      [AbsOptions]
1693
1694******************************************************************************/
1695#define AbsOptionsReadNegateFormula( \
1696  /* AbsOptions_t * */ oInfo         \
1697)                                    \
1698    ((oInfo)->negateFormula)
1699
1700/**Macro***********************************************************************
1701
1702  Synopsis [Macro to read the partApprox field from a AbsOptions_t
1703  structure.]
1704
1705  SideEffects  []
1706
1707  SeeAlso      [AbsOptions]
1708
1709******************************************************************************/
1710#define AbsOptionsReadPartApprox( \
1711  /* AbsOptions_t * */ oInfo      \
1712)                                 \
1713    ((oInfo)->partApprox)
1714
1715/**Macro***********************************************************************
1716
1717  Synopsis [Macro to set the verbosity field from a AbsOptions_t structure.]
1718
1719  SideEffects []
1720
1721  SeeAlso      [AbsOptions]
1722
1723******************************************************************************/
1724#define AbsOptionsSetVerbosity( \
1725  /* AbsOptions_t * */ oInfo,   \
1726  /* int */ data                \
1727)                               \
1728    ((oInfo)->verbosity) = (data)
1729
1730/**Macro***********************************************************************
1731
1732  Synopsis [Macro to set the timeOut field from a AbsOptions_t
1733  structure.]
1734
1735  SideEffects  []
1736
1737  SeeAlso      [AbsOptions]
1738
1739******************************************************************************/
1740#define AbsOptionsSetTimeOut( \
1741  /* AbsOptions_t * */ oInfo, \
1742  /* int */ data              \
1743)                             \
1744    ((oInfo)->timeOut) = (data)
1745
1746/**Macro***********************************************************************
1747
1748  Synopsis [Macro to set the reachability field from a AbsOptions_t
1749  structure.]
1750
1751  SideEffects  []
1752
1753  SeeAlso      [AbsOptions]
1754
1755******************************************************************************/
1756#define AbsOptionsSetReachability( \
1757  /* AbsOptions_t * */ oInfo,      \
1758  /* int */ data                   \
1759)                                  \
1760    ((oInfo)->reachability) = (data)
1761
1762/**Macro***********************************************************************
1763
1764  Synopsis [Macro to set the envelope field from a AbsOptions_t
1765  structure.]
1766
1767  SideEffects  []
1768
1769  SeeAlso      [AbsOptions]
1770
1771******************************************************************************/
1772#define AbsOptionsSetEnvelope( \
1773  /* AbsOptions_t * */ oInfo,  \
1774  /* int */ data               \
1775)                              \
1776    ((oInfo)->envelope) = (data)
1777
1778/**Macro***********************************************************************
1779
1780  Synopsis [Macro to set the fileName field from a AbsOptions_t
1781  structure.]
1782
1783  SideEffects  []
1784
1785  SeeAlso      [AbsOptions]
1786
1787******************************************************************************/
1788#define AbsOptionsSetFileName( \
1789  /* AbsOptions_t * */ oInfo,  \
1790  /* int */ data               \
1791)                              \
1792    ((oInfo)->fileName) = (data)
1793
1794/**Macro***********************************************************************
1795
1796  Synopsis [Macro to set the fairFileName field from a AbsOptions_t
1797  structure.]
1798
1799  SideEffects  []
1800
1801  SeeAlso      [AbsOptions_t]
1802
1803******************************************************************************/
1804#define AbsOptionsSetFairFileName( \
1805  /* AbsOptions_t * */ oInfo,      \
1806  /* int */ data                   \
1807)                                  \
1808    ((oInfo)->fairFileName) = (data)
1809
1810/**Macro***********************************************************************
1811
1812  Synopsis [Macro to set the exact field from a AbsOptions_t structure.]
1813
1814  SideEffects  []
1815
1816  SeeAlso      [AbsOptions_t]
1817
1818******************************************************************************/
1819#define AbsOptionsSetExact(   \
1820  /* AbsOptions_t * */ oInfo, \
1821  /* int */ data              \
1822)                             \
1823    ((oInfo)->exact) = (data)
1824
1825/**Macro***********************************************************************
1826
1827  Synopsis [Macro to set the printStats field from a AbsOptions_t structure.]
1828
1829  SideEffects  []
1830
1831  SeeAlso      [AbsOptions_t]
1832
1833******************************************************************************/
1834#define AbsOptionsSetPrintStats( \
1835  /* AbsOptions_t * */ oInfo,    \
1836  /* int */ data                 \
1837)                                \
1838    ((oInfo)->printStats) = (data)
1839
1840/**Macro***********************************************************************
1841
1842  Synopsis [Macro to set the minimizeIterate field from a AbsOptions_t
1843  structure.]
1844
1845  SideEffects  []
1846
1847  SeeAlso      [AbsOptions_t]
1848
1849******************************************************************************/
1850#define AbsOptionsSetMinimizeIterate( \
1851  /* AbsOptions_t * */ oInfo,         \
1852  /* int */ data                      \
1853)                                     \
1854    ((oInfo)->minimizeIterate) = (data)
1855
1856/**Macro***********************************************************************
1857
1858  Synopsis [Macro to set the negateFormula field from a AbsOptions_t
1859  structure.]
1860
1861  SideEffects  []
1862
1863  SeeAlso      [AbsOptions_t]
1864
1865******************************************************************************/
1866#define AbsOptionsSetNegateFormula( \
1867  /* AbsOptions_t * */ oInfo,       \
1868  /* boolean */ data                \
1869)                                   \
1870    ((oInfo)->negateFormula) = (data)
1871
1872/**Macro***********************************************************************
1873
1874  Synopsis [Macro to set the partApprox field from a AbsOptions_t structure.]
1875
1876  SideEffects  []
1877
1878  SeeAlso      [AbsOptions_t]
1879
1880******************************************************************************/
1881#define AbsOptionsSetPartApprox( \
1882  /* AbsOptions_t * */ oInfo,    \
1883  /* boolean */ data             \
1884)                                \
1885    ((oInfo)->partApprox) = (data)
1886
1887/**Macro***********************************************************************
1888
1889  Synopsis [Macro to read the numReorderings field from a AbsStats_t
1890  structure.]
1891
1892  SideEffects  []
1893
1894  SeeAlso      [AbsStats_t]
1895
1896******************************************************************************/
1897#define AbsStatsReadNumReorderings( \
1898  /* AbsStats_t * */ sInfo          \
1899)                                   \
1900    (sInfo)->numReorderings
1901
1902/**Macro***********************************************************************
1903
1904  Synopsis [Macro to read the evalFixedPoint field from a AbsStats_t
1905  structure.]
1906
1907  SideEffects  []
1908
1909  SeeAlso      [AbsStats_t]
1910
1911******************************************************************************/
1912#define AbsStatsReadEvalFixedPoint( \
1913  /* AbsStats_t * */ sInfo          \
1914)                                   \
1915    (sInfo)->evalFixedPoint
1916
1917/**Macro***********************************************************************
1918
1919  Synopsis [Macro to set the numReorderings field from a AbsStats_t structure.]
1920
1921  SideEffects  []
1922
1923  SeeAlso      [AbsStats_t]
1924
1925******************************************************************************/
1926#define AbsStatsSetNumReorderings( \
1927  /* AbsStats_t * */ sInfo,        \
1928  /* int  */ data                  \
1929)                                  \
1930    (sInfo)->numReorderings = (data)
1931
1932/**Macro***********************************************************************
1933
1934  Synopsis [Macro to set the evalFixedPoint field from a AbsStats_t structure.]
1935
1936  SideEffects  []
1937
1938  SeeAlso      [AbsStats_t]
1939
1940******************************************************************************/
1941#define AbsStatsSetEvalFixedPoint( \
1942  /* AbsStats_t * */ sInfo,        \
1943  /* int  */ data                  \
1944)                                  \
1945    (sInfo)->evalFixedPoint = (data)
1946
1947/**Macro***********************************************************************
1948
1949  Synopsis [Macro to read the evalAnd field from a AbsStats_t
1950  structure.]
1951
1952  SideEffects  []
1953
1954  SeeAlso      [AbsStats_t]
1955
1956******************************************************************************/
1957#define AbsStatsReadEvalAnd( \
1958  /* AbsStats_t * */ sInfo   \
1959)                            \
1960    (sInfo)->evalAnd
1961
1962/**Macro***********************************************************************
1963
1964  Synopsis [Macro to set the evalAnd field from a AbsStats_t structure.]
1965
1966  SideEffects  []
1967
1968  SeeAlso      [AbsStats_t]
1969
1970******************************************************************************/
1971#define AbsStatsSetEvalAnd( \
1972  /* AbsStats_t * */ sInfo, \
1973  /* int  */ data           \
1974)                           \
1975    (sInfo)->evalAnd = (data)
1976
1977/**Macro***********************************************************************
1978
1979  Synopsis [Macro to read the evalNot field from a AbsStats_t
1980  structure.]
1981
1982  SideEffects  []
1983
1984  SeeAlso      [AbsStats_t]
1985
1986******************************************************************************/
1987#define AbsStatsReadEvalNot( \
1988  /* AbsStats_t * */ sInfo   \
1989)                            \
1990    (sInfo)->evalNot
1991
1992/**Macro***********************************************************************
1993
1994  Synopsis [Macro to set the evalNot field from a AbsStats_t structure.]
1995
1996  SideEffects  []
1997
1998  SeeAlso      [AbsStats_t]
1999
2000******************************************************************************/
2001#define AbsStatsSetEvalNot( \
2002  /* AbsStats_t * */ sInfo, \
2003  /* int  */ data           \
2004)                           \
2005    (sInfo)->evalNot = (data)
2006
2007/**Macro***********************************************************************
2008
2009  Synopsis [Macro to read the evalPreImage field from a AbsStats_t
2010  structure.]
2011
2012  SideEffects  []
2013
2014  SeeAlso      [AbsStats_t]
2015
2016******************************************************************************/
2017#define AbsStatsReadEvalPreImage( \
2018  /* AbsStats_t * */ sInfo        \
2019)                                 \
2020    (sInfo)->evalPreImage
2021
2022/**Macro***********************************************************************
2023
2024  Synopsis [Macro to set the evalPreImage field from a AbsStats_t structure.]
2025
2026  SideEffects  []
2027
2028  SeeAlso      [AbsStats_t]
2029
2030******************************************************************************/
2031#define AbsStatsSetEvalPreImage( \
2032  /* AbsStats_t * */ sInfo,      \
2033  /* int  */ data                \
2034)                                \
2035    (sInfo)->evalPreImage = (data)
2036
2037/**Macro***********************************************************************
2038
2039  Synopsis [Macro to read the evalIdentifier field from a AbsStats_t
2040  structure.]
2041
2042  SideEffects  []
2043
2044  SeeAlso      [AbsStats_t]
2045
2046******************************************************************************/
2047#define AbsStatsReadEvalIdentifier( \
2048  /* AbsStats_t * */ sInfo          \
2049)                                   \
2050    (sInfo)->evalIdentifier
2051
2052/**Macro***********************************************************************
2053
2054  Synopsis [Macro to set the evalIdentifier field from a AbsStats_t structure.]
2055
2056  SideEffects  []
2057
2058  SeeAlso      [AbsStats_t]
2059
2060******************************************************************************/
2061#define AbsStatsSetEvalIdentifier( \
2062  /* AbsStats_t * */ sInfo,        \
2063  /* int  */ data                  \
2064)                                  \
2065    (sInfo)->evalIdentifier = (data)
2066
2067/**Macro***********************************************************************
2068
2069  Synopsis [Macro to read the evalVariable field from a AbsStats_t
2070  structure.]
2071
2072  SideEffects  []
2073
2074  SeeAlso      [AbsStats_t]
2075
2076******************************************************************************/
2077#define AbsStatsReadEvalVariable( \
2078  /* AbsStats_t * */ sInfo        \
2079)                                 \
2080    (sInfo)->evalVariable
2081
2082/**Macro***********************************************************************
2083
2084  Synopsis [Macro to set the evalVariable field from a AbsStats_t structure.]
2085
2086  SideEffects  []
2087
2088  SeeAlso      [AbsStats_t]
2089
2090******************************************************************************/
2091#define AbsStatsSetEvalVariable( \
2092  /* AbsStats_t * */ sInfo,      \
2093  /* int  */ data                \
2094)                                \
2095    (sInfo)->evalVariable = (data)
2096
2097/**Macro***********************************************************************
2098
2099  Synopsis [Macro to read the refineFixedPoint field from a AbsStats_t
2100  structure.]
2101
2102  SideEffects  []
2103
2104  SeeAlso      [AbsStats_t]
2105
2106******************************************************************************/
2107#define AbsStatsReadRefineFixedPoint( \
2108  /* AbsStats_t * */ sInfo            \
2109)                                     \
2110    (sInfo)->refineFixedPoint
2111
2112/**Macro***********************************************************************
2113
2114  Synopsis [Macro to set the refineFixedPoint field from a AbsStats_t
2115  structure.]
2116
2117  SideEffects  []
2118
2119  SeeAlso      [AbsStats_t]
2120
2121******************************************************************************/
2122#define AbsStatsSetRefineFixedPoint( \
2123  /* AbsStats_t * */ sInfo,          \
2124  /* int  */ data                    \
2125)                                    \
2126    (sInfo)->refineFixedPoint = (data)
2127
2128/**Macro***********************************************************************
2129
2130  Synopsis [Macro to read the refineAnd field from a AbsStats_t structure.]
2131
2132  SideEffects  []
2133
2134  SeeAlso      [AbsStats_t]
2135
2136******************************************************************************/
2137#define AbsStatsReadRefineAnd( \
2138  /* AbsStats_t * */ sInfo     \
2139)                              \
2140    (sInfo)->refineAnd
2141
2142/**Macro***********************************************************************
2143
2144  Synopsis [Macro to set the refineAnd field from a AbsStats_t structure.]
2145
2146  SideEffects  []
2147
2148  SeeAlso      [AbsStats_t]
2149
2150******************************************************************************/
2151#define AbsStatsSetRefineAnd( \
2152  /* AbsStats_t * */ sInfo,   \
2153  /* int  */ data             \
2154)                             \
2155    (sInfo)->refineAnd = (data)
2156
2157/**Macro***********************************************************************
2158
2159  Synopsis [Macro to read the refineNot field from a AbsStats_t structure.]
2160
2161  SideEffects  []
2162
2163  SeeAlso      [AbsStats_t]
2164
2165******************************************************************************/
2166#define AbsStatsReadRefineNot( \
2167  /* AbsStats_t * */ sInfo     \
2168)                              \
2169    (sInfo)->refineNot
2170
2171/**Macro***********************************************************************
2172
2173  Synopsis [Macro to set the refineNot field from a AbsStats_t structure.]
2174
2175  SideEffects  []
2176
2177  SeeAlso      [AbsStats_t]
2178
2179******************************************************************************/
2180#define AbsStatsSetRefineNot( \
2181  /* AbsStats_t * */ sInfo,   \
2182  /* int  */ data             \
2183)                             \
2184    (sInfo)->refineNot = (data)
2185
2186/**Macro***********************************************************************
2187
2188  Synopsis [Macro to read the refinePreImage field from a AbsStats_t
2189  structure.]
2190
2191  SideEffects  []
2192
2193  SeeAlso      [AbsStats_t]
2194
2195******************************************************************************/
2196#define AbsStatsReadRefinePreImage( \
2197  /* AbsStats_t * */ sInfo          \
2198)                                   \
2199    (sInfo)->refinePreImage
2200
2201/**Macro***********************************************************************
2202
2203  Synopsis [Macro to set the refinePreImage field from a AbsStats_t structure.]
2204
2205  SideEffects  []
2206
2207  SeeAlso      [AbsStats_t]
2208
2209******************************************************************************/
2210#define AbsStatsSetRefinePreImage( \
2211  /* AbsStats_t * */ sInfo,        \
2212  /* int  */ data                  \
2213)                                  \
2214    (sInfo)->refinePreImage = (data)
2215
2216/**Macro***********************************************************************
2217
2218  Synopsis [Macro to read the refineIdentifier field from a AbsStats_t
2219  structure.]
2220
2221  SideEffects  []
2222
2223  SeeAlso      [AbsStats_t]
2224
2225******************************************************************************/
2226#define AbsStatsReadRefineIdentifier( \
2227  /* AbsStats_t * */ sInfo            \
2228)                                     \
2229    (sInfo)->refineIdentifier
2230
2231/**Macro***********************************************************************
2232
2233  Synopsis [Macro to set the refineIdentifier field from a AbsStats_t
2234  structure.]
2235
2236  SideEffects  []
2237
2238  SeeAlso      [AbsStats_t]
2239
2240******************************************************************************/
2241#define AbsStatsSetRefineIdentifier( \
2242  /* AbsStats_t * */ sInfo,          \
2243  /* int  */ data                    \
2244)                                    \
2245    (sInfo)->refineIdentifier = (data)
2246
2247/**Macro***********************************************************************
2248
2249  Synopsis [Macro to read the refineVariable field from a AbsStats_t
2250  structure.]
2251
2252  SideEffects  []
2253
2254  SeeAlso      [AbsStats_t]
2255
2256******************************************************************************/
2257#define AbsStatsReadRefineVariable( \
2258  /* AbsStats_t * */ sInfo          \
2259)                                   \
2260    (sInfo)->refineVariable
2261
2262/**Macro***********************************************************************
2263
2264  Synopsis [Macro to set the refineVariable field from a AbsStats_t structure.]
2265
2266  SideEffects  []
2267
2268  SeeAlso      [AbsStats_t]
2269
2270******************************************************************************/
2271#define AbsStatsSetRefineVariable( \
2272  /* AbsStats_t * */ sInfo,        \
2273  /* int  */ data                  \
2274)                                  \
2275    (sInfo)->refineVariable = (data)
2276
2277/**Macro***********************************************************************
2278
2279  Synopsis [Macro to read the exactPreImage field from a AbsStats_t structure.]
2280
2281  SideEffects  []
2282
2283  SeeAlso      [AbsStats_t]
2284
2285******************************************************************************/
2286#define AbsStatsReadExactPreImage( \
2287  /* AbsStats_t * */ sInfo         \
2288)                                  \
2289    (sInfo)->exactPreImage
2290
2291/**Macro***********************************************************************
2292
2293  Synopsis [Macro to set the exactPreImage field from a AbsStats_t structure.]
2294
2295  SideEffects  []
2296
2297  SeeAlso      [AbsStats_t]
2298
2299******************************************************************************/
2300#define AbsStatsSetExactPreImage( \
2301  /* AbsStats_t * */ sInfo,       \
2302  /* int  */ data                 \
2303)                                 \
2304    (sInfo)->exactPreImage = (data)
2305
2306/**Macro***********************************************************************
2307
2308  Synopsis [Macro to read the approxPreImage field from a AbsStats_t
2309  structure.]
2310
2311  SideEffects  []
2312
2313  SeeAlso      [AbsStats_t]
2314
2315******************************************************************************/
2316#define AbsStatsReadApproxPreImage( \
2317  /* AbsStats_t * */ sInfo          \
2318)                                   \
2319    (sInfo)->approxPreImage
2320
2321/**Macro***********************************************************************
2322
2323  Synopsis [Macro to set the approxPreImage field from a AbsStats_t structure.]
2324
2325  SideEffects  []
2326
2327  SeeAlso      [AbsStats_t]
2328
2329******************************************************************************/
2330#define AbsStatsSetApproxPreImage( \
2331  /* AbsStats_t * */ sInfo,        \
2332  /* int  */ data                  \
2333)                                  \
2334    (sInfo)->approxPreImage = (data)
2335
2336
2337/**Macro***********************************************************************
2338
2339  Synopsis [Macro to read the exactImage field from a AbsStats_t structure.]
2340
2341  SideEffects  []
2342
2343  SeeAlso      [AbsStats_t]
2344
2345******************************************************************************/
2346#define AbsStatsReadExactImage( \
2347  /* AbsStats_t * */ sInfo      \
2348)                               \
2349    (sInfo)->exactImage
2350
2351/**Macro***********************************************************************
2352
2353  Synopsis [Macro to set the exactImage field from a AbsStats_t structure.]
2354
2355  SideEffects  []
2356
2357  SeeAlso      [AbsStats_t]
2358
2359******************************************************************************/
2360#define AbsStatsSetExactImage( \
2361  /* AbsStats_t * */ sInfo,    \
2362  /* int  */ data              \
2363)                              \
2364    (sInfo)->exactImage = (data)
2365
2366/**Macro***********************************************************************
2367
2368  Synopsis [Macro to read the preImageCacheEntries field from a AbsStats_t
2369  structure.]
2370
2371  SideEffects  []
2372
2373  SeeAlso      [AbsStats_t]
2374
2375******************************************************************************/
2376#define AbsStatsReadPreImageCacheEntries( \
2377  /* AbsStats_t * */ sInfo                \
2378)                                         \
2379    (sInfo)->preImageCacheEntries
2380
2381/**Macro***********************************************************************
2382
2383  Synopsis [Macro to set the preImageCacheEntries field from a AbsStats_t
2384  structure.]
2385
2386  SideEffects  []
2387
2388  SeeAlso      [AbsStats_t]
2389
2390******************************************************************************/
2391#define AbsStatsSetPreImageCacheEntries( \
2392  /* AbsStats_t * */ sInfo,              \
2393  /* int  */ data                        \
2394)                                        \
2395    (sInfo)->preImageCacheEntries = (data)
2396
2397/**Macro***********************************************************************
2398
2399  Synopsis [Macro to read the imageCacheEntries field from a AbsStats_t
2400  structure.]
2401
2402  SideEffects  []
2403
2404  SeeAlso      [AbsStats_t]
2405
2406******************************************************************************/
2407#define AbsStatsReadImageCacheEntries( \
2408  /* AbsStats_t * */ sInfo             \
2409)                                      \
2410    (sInfo)->imageCacheEntries
2411
2412/**Macro***********************************************************************
2413
2414  Synopsis [Macro to set the imageCacheEntries field from a AbsStats_t
2415  structure.]
2416
2417  SideEffects  []
2418
2419  SeeAlso      [AbsStats_t]
2420
2421******************************************************************************/
2422#define AbsStatsSetImageCacheEntries( \
2423  /* AbsStats_t * */ sInfo,           \
2424  /* int  */ data                     \
2425)                                     \
2426    (sInfo)->imageCacheEntries = (data)
2427
2428/**Macro***********************************************************************
2429
2430  Synopsis [Macro to read the imageCpuTime field from a AbsStats_t
2431  structure.]
2432
2433  SideEffects  []
2434
2435  SeeAlso      [AbsStats_t]
2436
2437******************************************************************************/
2438#define AbsStatsReadImageCpuTime( \
2439  /* AbsStats_t * */ sInfo        \
2440)                                 \
2441    (sInfo)->imageCpuTime
2442
2443/**Macro***********************************************************************
2444
2445  Synopsis [Macro to set the imageCpuTime field from a AbsStats_t
2446  structure.]
2447
2448  SideEffects  []
2449
2450  SeeAlso      [AbsStats_t]
2451
2452******************************************************************************/
2453#define AbsStatsSetImageCpuTime( \
2454  /* AbsStats_t * */ sInfo,      \
2455  /* int  */ data                \
2456)                                \
2457    (sInfo)->imageCpuTime = (data)
2458
2459/**Macro***********************************************************************
2460
2461  Synopsis [Macro to read the preImageCpuTime field from a AbsStats_t
2462  structure.]
2463
2464  SideEffects  []
2465
2466  SeeAlso      [AbsStats_t]
2467
2468******************************************************************************/
2469#define AbsStatsReadPreImageCpuTime( \
2470  /* AbsStats_t * */ sInfo        \
2471)                                 \
2472    (sInfo)->preImageCpuTime
2473
2474/**Macro***********************************************************************
2475
2476  Synopsis [Macro to set the preImageCpuTime field from a AbsStats_t
2477  structure.]
2478
2479  SideEffects  []
2480
2481  SeeAlso      [AbsStats_t]
2482
2483******************************************************************************/
2484#define AbsStatsSetPreImageCpuTime( \
2485  /* AbsStats_t * */ sInfo,      \
2486  /* int  */ data                \
2487)                                \
2488    (sInfo)->preImageCpuTime = (data)
2489
2490/**Macro***********************************************************************
2491
2492  Synopsis [Macro to read the appPreCpuTime field from a AbsStats_t
2493  structure.]
2494
2495  SideEffects  []
2496
2497  SeeAlso      [AbsStats_t]
2498
2499******************************************************************************/
2500#define AbsStatsReadAppPreCpuTime( \
2501  /* AbsStats_t * */ sInfo        \
2502)                                 \
2503    (sInfo)->appPreCpuTime
2504
2505/**Macro***********************************************************************
2506
2507  Synopsis [Macro to set the appPreCpuTime field from a AbsStats_t
2508  structure.]
2509
2510  SideEffects  []
2511
2512  SeeAlso      [AbsStats_t]
2513
2514******************************************************************************/
2515#define AbsStatsSetAppPreCpuTime( \
2516  /* AbsStats_t * */ sInfo,      \
2517  /* int  */ data                \
2518)                                \
2519    (sInfo)->appPreCpuTime = (data)
2520
2521/**Macro***********************************************************************
2522
2523  Synopsis [Macro to read the key field of the AbsEvalCacheEntry_t structure.]
2524
2525  SideEffects  []
2526
2527  SeeAlso      [AbsEvalCacheEntry_t]
2528
2529******************************************************************************/
2530#define AbsEvalCacheEntryReadKey(   \
2531  /* AbsEvalCacheEntry_t * */ eInfo \
2532)                                   \
2533    ((eInfo)->key)
2534
2535/**Macro***********************************************************************
2536
2537  Synopsis [Macro to set the key field of the AbsEvalCacheEntry_t structure.]
2538
2539  SideEffects  []
2540
2541  SeeAlso      [AbsEvalCacheEntry_t]
2542
2543******************************************************************************/
2544#define AbsEvalCacheEntrySetKey(     \
2545  /* AbsEvalCacheEntry_t * */ eInfo, \
2546  /* mdd_t * */ data                 \
2547)                                    \
2548    ((eInfo)->key) = (data)
2549
2550/**Macro***********************************************************************
2551
2552  Synopsis [Macro to read the approx field of the AbsEvalCacheEntry_t
2553  structure.]
2554
2555  SideEffects  []
2556
2557  SeeAlso      [AbsEvalCacheEntry_t]
2558
2559******************************************************************************/
2560#define AbsEvalCacheEntryReadApprox( \
2561  /* AbsEvalCacheEntry_t * */ eInfo  \
2562)                                    \
2563    ((eInfo)->approx)
2564
2565/**Macro***********************************************************************
2566
2567  Synopsis [Macro to set the approx field of the AbsEvalCacheEntry_t
2568  structure.]
2569
2570  SideEffects  []
2571
2572  SeeAlso      [AbsEvalCacheEntry_t]
2573
2574******************************************************************************/
2575#define AbsEvalCacheEntrySetApprox(  \
2576  /* AbsEvalCacheEntry_t * */ eInfo, \
2577  /* mdd_t * */ data                 \
2578)                                    \
2579    ((eInfo)->approx) = (data)
2580
2581/**Macro***********************************************************************
2582
2583  Synopsis [Macro to read the complement field of the AbsEvalCacheEntry_t
2584  structure.]
2585
2586  SideEffects  []
2587
2588  SeeAlso      [AbsEvalCacheEntry_t]
2589
2590******************************************************************************/
2591#define AbsEvalCacheEntryReadComplement( \
2592  /* AbsEvalCacheEntry_t * */ eInfo      \
2593)                                        \
2594    ((eInfo)->complement)
2595
2596/**Macro***********************************************************************
2597
2598  Synopsis [Macro to set the complement field of the AbsEvalCacheEntry_t
2599  structure.]
2600
2601  SideEffects  []
2602
2603  SeeAlso      [AbsEvalCacheEntry_t]
2604
2605******************************************************************************/
2606#define AbsEvalCacheEntrySetComplement( \
2607  /* AbsEvalCacheEntry_t * */ eInfo,    \
2608  /* mdd_t * */ data                    \
2609)                                       \
2610    ((eInfo)->complement) = (data)
2611
2612/**Macro***********************************************************************
2613
2614  Synopsis [Macro to read the result field of the AbsEvalCacheEntry_t
2615  structure.]
2616
2617  SideEffects  []
2618
2619  SeeAlso      [AbsEvalCacheEntry_t]
2620
2621******************************************************************************/
2622#define AbsEvalCacheEntryReadResult( \
2623  /* AbsEvalCacheEntry_t * */ eInfo  \
2624)                                    \
2625    ((eInfo)->result)
2626
2627/**Macro***********************************************************************
2628
2629  Synopsis [Macro to read the careSet field of the AbsEvalCacheEntry_t
2630  structure.]
2631
2632  SideEffects  []
2633
2634  SeeAlso      [AbsEvalCacheEntry_t]
2635
2636******************************************************************************/
2637#define AbsEvalCacheEntryReadCareSet( \
2638  /* AbsEvalCacheEntry_t * */ eInfo   \
2639)                                     \
2640    ((eInfo)->careSet)
2641
2642/**Macro***********************************************************************
2643
2644  Synopsis [Macro to set the result field of the AbsEvalCacheEntry_t
2645  structure.]
2646
2647  SideEffects  []
2648
2649  SeeAlso      [AbsEvalCacheEntry_t]
2650
2651******************************************************************************/
2652#define AbsEvalCacheEntrySetResult(  \
2653  /* AbsEvalCacheEntry_t * */ eInfo, \
2654  /* mdd_t * */ data                 \
2655)                                    \
2656    ((eInfo)->result) = (data)
2657
2658/**Macro***********************************************************************
2659
2660  Synopsis [Macro to set the careSet field of the AbsEvalCacheEntry_t
2661  structure.]
2662
2663  SideEffects  []
2664
2665  SeeAlso      [AbsEvalCacheEntry_t]
2666
2667******************************************************************************/
2668#define AbsEvalCacheEntrySetCareSet(  \
2669  /* AbsEvalCacheEntry_t * */ eInfo,  \
2670  /* mdd_t * */ data                  \
2671)                                     \
2672    ((eInfo)->careSet) = (data)
2673
2674/**AutomaticStart*************************************************************/
2675
2676/*---------------------------------------------------------------------------*/
2677/* Function prototypes                                                       */
2678/*---------------------------------------------------------------------------*/
2679
2680EXTERN AbsVertexCatalog_t * AbsVertexCatalogInitialize(void);
2681EXTERN void AbsVertexCatalogFree(AbsVertexCatalog_t *c);
2682EXTERN AbsVertexInfo_t * AbsVertexCatalogFindOrAdd(AbsVertexCatalog_t *catalog, AbsVertex_t type, boolean polarity, AbsVertexInfo_t *leftKid, AbsVertexInfo_t *rightKid, int localId, char *idName, char *idValue);
2683EXTERN void AbsCatalogDelete(AbsVertexCatalog_t *catalog, AbsVertexInfo_t *vertex);
2684EXTERN void AbsSubFormulaVerify(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
2685EXTERN void AbsFormulaScheduleEvaluation(AbsVertexInfo_t *current, AbsVertexInfo_t *limit);
2686EXTERN mdd_t * AbsComputeOptimalIterate(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *lowerIterate, mdd_t *upperIterate);
2687EXTERN boolean AbsFixedPointIterate(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, int iterateIndex);
2688EXTERN AbsVertexInfo_t * AbsVertexInitialize(void);
2689EXTERN void AbsVertexFree(AbsVertexCatalog_t *catalog, AbsVertexInfo_t *v, AbsVertexInfo_t *fromVertex);
2690EXTERN Abs_VerificationInfo_t * AbsVerificationInfoInitialize(void);
2691EXTERN void AbsVerificationInfoFree(Abs_VerificationInfo_t *v);
2692EXTERN AbsOptions_t * AbsOptionsInitialize(void);
2693EXTERN void AbsOptionsFree(AbsOptions_t *unit);
2694EXTERN AbsStats_t * AbsStatsInitialize(void);
2695EXTERN void AbsStatsFree(AbsStats_t *unit);
2696EXTERN AbsEvalCacheEntry_t * AbsCacheEntryInitialize(void);
2697EXTERN void AbsCacheEntryFree(AbsEvalCacheEntry_t *unit);
2698EXTERN void AbsEvalCacheInsert(st_table *solutions, mdd_t *key, mdd_t *result, mdd_t *careSet, boolean approx, boolean replace);
2699EXTERN boolean AbsEvalCacheLookup(st_table *solutions, mdd_t *key, mdd_t *careSet, boolean approx, mdd_t **result, boolean *storedApprox);
2700EXTERN void AbsVerificationFlushCache(Abs_VerificationInfo_t *absInfo);
2701EXTERN void AbsVertexFlushCache(AbsVertexInfo_t *vertexPtr);
2702EXTERN mdd_t * AbsImageReadOrCompute(Abs_VerificationInfo_t *absInfo, Img_ImageInfo_t *imageInfo, mdd_t *set, mdd_t *careSet);
2703EXTERN array_t * AbsFormulaArrayVerify(Abs_VerificationInfo_t *absInfo, array_t *formulaArray);
2704EXTERN Fsm_Fsm_t * AbsCreateReducedFsm(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, Fsm_Fsm_t **approxFsm);
2705EXTERN boolean AbsMddEqualModCareSet(mdd_t *f, mdd_t *g, mdd_t *careSet);
2706EXTERN boolean AbsMddLEqualModCareSet(mdd_t *f, mdd_t *g, mdd_t *careSet);
2707EXTERN AbsParseInfo_t * AbsParseInfoInitialize(void);
2708EXTERN void AbsParseInfoFree(AbsParseInfo_t *data);
2709EXTERN mdd_t * AbsSubFormulaRefine(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
2710EXTERN array_t * AbsCtlFormulaArrayTranslate(Abs_VerificationInfo_t *verInfo, array_t *formulaArray, array_t *fairArray);
2711EXTERN void AbsVertexPrintDot(FILE *fp, array_t *vertexArray);
2712EXTERN void AbsVertexPrint(AbsVertexInfo_t *vertexPtr, st_table *visitedSF, boolean recur, long verbosity);
2713EXTERN void AbsBddPrintMinterms(mdd_t *function);
2714EXTERN void AbsFormulaSetConstantBit(AbsVertexInfo_t *vertexPtr);
2715EXTERN boolean AbsFormulaSanityCheck(AbsVertexInfo_t *vertexPtr, st_table *rootTable);
2716EXTERN boolean AbsIteratesSanityCheck(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
2717EXTERN void AbsStatsPrintReport(FILE *fp, AbsStats_t *stats);
2718
2719/**AutomaticEnd***************************************************************/
2720
2721#endif /* _ABSINT */
2722
Note: See TracBrowser for help on using the repository browser.