distr/nanotrav/ntr.h

   1 /**CHeaderFile*****************************************************************
   2
   3   FileName    [ntr.h]
   4
   5   PackageName [ntr]
   6
   7   Synopsis    [Simple-minded package to do traversal.]
   8
   9   Description []
  10
  11   SeeAlso     []
  12
  13   Author      [Fabio Somenzi]
  14
  15   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  16
  17   All rights reserved.
  18
  19   Redistribution and use in source and binary forms, with or without
  20   modification, are permitted provided that the following conditions
  21   are met:
  22
  23   Redistributions of source code must retain the above copyright
  24   notice, this list of conditions and the following disclaimer.
  25
  26   Redistributions in binary form must reproduce the above copyright
  27   notice, this list of conditions and the following disclaimer in the
  28   documentation and/or other materials provided with the distribution.
  29
  30   Neither the name of the University of Colorado nor the names of its
  31   contributors may be used to endorse or promote products derived from
  32   this software without specific prior written permission.
  33
  34   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  35   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  36   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  37   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  38   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  39   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  40   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  41   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  42   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  43   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  44   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  45   POSSIBILITY OF SUCH DAMAGE.]
  46
  47   Revision    [$Id: ntr.h,v 1.27 2009/02/20 02:19:02 fabio Exp fabio $]
  48
  49 ******************************************************************************/
  50
  51 #ifndef _NTR
  52 #define _NTR
  53
  54 /*---------------------------------------------------------------------------*/
  55 /* Nested includes                                                           */
  56 /*---------------------------------------------------------------------------*/
  57
  58 #include "dddmp.h"
  59 #include "bnet.h"
  60
  61 #ifdef __cplusplus
  62 extern "C" {
  63 #endif
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Constant declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69 #define PI_PS_FROM_FILE 0
  70 #define PI_PS_DFS       1
  71 #define PI_PS_GIVEN     2
  72
  73 #define NTR_IMAGE_MONO 0
  74 #define NTR_IMAGE_PART 1
  75 #define NTR_IMAGE_CLIP 2
  76 #define NTR_IMAGE_DEPEND 3
  77
  78 #define NTR_UNDER_APPROX 0
  79 #define NTR_OVER_APPROX 1
  80
  81 #define NTR_FROM_NEW 0
  82 #define NTR_FROM_REACHED 1
  83 #define NTR_FROM_RESTRICT 2
  84 #define NTR_FROM_COMPACT 3
  85 #define NTR_FROM_SQUEEZE 4
  86 #define NTR_FROM_UNDERAPPROX 5
  87 #define NTR_FROM_OVERAPPROX 6
  88
  89 #define NTR_GROUP_NONE 0
  90 #define NTR_GROUP_DEFAULT 1
  91 #define NTR_GROUP_FIXED 2
  92
  93 #define NTR_SHORT_NONE 0
  94 #define NTR_SHORT_BELLMAN 1
  95 #define NTR_SHORT_FLOYD 2
  96 #define NTR_SHORT_SQUARE 3
  97
  98 /*---------------------------------------------------------------------------*/
  99 /* Stucture declarations                                                     */
 100 /*---------------------------------------------------------------------------*/
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Type declarations                                                         */
 104 /*---------------------------------------------------------------------------*/
 105
 106 typedef struct  NtrOptions {
 107     long        initialTime;    /* this is here for convenience */
 108     int         verify;         /* read two networks and compare them */
 109     char        *file1;         /* first network file name */
 110     char        *file2;         /* second network file name */
 111     int         second;         /* a second network is given */
 112     int         traverse;       /* do reachability analysis */
 113     int         depend;         /* do latch dependence analysis */
 114     int         image;          /* monolithic, partitioned, or clip */
 115     double      imageClip;      /* clipping depth in image computation */
 116     int         approx;         /* under or over approximation */
 117     int         threshold;      /* approximation threshold */
 118     int         from;           /* method to compute from states */
 119     int         groupnsps;      /* group present state and next state vars */
 120     int         closure;        /* use transitive closure */
 121     double      closureClip;    /* clipping depth in closure computation */
 122     int         envelope;       /* compute outer envelope */
 123     int         scc;            /* compute strongly connected components */
 124     int         zddtest;        /* do zdd test */
 125     int         printcover;     /* print ISOP covers when testing ZDDs */
 126     int         maxflow;        /* compute maximum flow in network */
 127     int         shortPath;      /* compute shortest paths in network */
 128     int         selectiveTrace; /* use selective trace in shortest paths */
 129     char        *sinkfile;      /* file for externally provided sink node */
 130     int         partition;      /* test McMillan conjunctive partitioning */
 131     int         char2vect;      /* test char-to-vect decomposition */
 132     int         density;        /* test density-related functions */
 133     double      quality;        /* quality parameter for density functions */
 134     int         decomp;         /* test decomposition functions */
 135     int         cofest;         /* test cofactor estimation */
 136     double      clip;           /* test clipping functions */
 137     int         dontcares;      /* test equivalence and containment with DCs */
 138     int         closestCube;    /* test Cudd_bddClosestCube */
 139     int         clauses;        /* test extraction of two-literal clauses */
 140     int         noBuild;        /* do not build BDDs; just echo order */
 141     int         stateOnly;      /* ignore primary outputs */
 142     char        *node;          /* only node for which to build BDD */
 143     int         locGlob;        /* build global or local BDDs */
 144     int         progress;       /* report output names while building BDDs */
 145     int         cacheSize;      /* computed table initial size */
 146     unsigned long maxMemory;    /* target maximum memory */
 147     unsigned long maxMemHard;   /* maximum allowed memory */
 148     unsigned int maxLive;       /* maximum number of nodes */
 149     int         slots;          /* unique subtable initial slots */
 150     int         ordering;       /* FANIN DFS ... */
 151     char        *orderPiPs;     /* file for externally provided order */
 152     Cudd_ReorderingType reordering; /* NONE RANDOM PIVOT SIFTING ... */
 153     int         autoDyn;        /* ON OFF */
 154     Cudd_ReorderingType autoMethod; /* RANDOM PIVOT SIFTING CONVERGE ... */
 155     char        *treefile;      /* file name for variable tree */
 156     int         firstReorder;   /* when to do first reordering */
 157     int         countDead;      /* count dead nodes toward triggering
 158                                    reordering */
 159     int         maxGrowth;      /* maximum growth during reordering (%) */
 160     Cudd_AggregationType groupcheck; /* grouping function */
 161     int         arcviolation;   /* percent violation of arcs in
 162                                    extended symmetry check */
 163     int         symmviolation;  /* percent symm violation in
 164                                    extended symmetry check */
 165     int         recomb;         /* recombination parameter for grouping */
 166     int         nodrop;         /* don't drop intermediate BDDs ASAP */
 167     int         signatures;     /* computation of signatures */
 168     int         gaOnOff;        /* whether to run GA at the end */
 169     int         populationSize; /* population size for GA */
 170     int         numberXovers;   /* number of crossovers for GA */
 171     int         bdddump;        /* ON OFF */
 172     int         dumpFmt;        /* 0 -> dot 1 -> blif 2 ->daVinci 3 -> DDcal
 173                                 ** 4 -> factored form */
 174     char        *dumpfile;      /* filename for dump */
 175     int         store;          /* iteration at which to store Reached */
 176     char        *storefile;     /* filename for storing Reached */
 177     int         load;           /* load initial states from file */
 178     char        *loadfile;      /* filename for loading states */
 179     int         verb;           /* level of verbosity */
 180 } NtrOptions;
 181
 182 typedef struct NtrHeapSlot {
 183     void *item;
 184     int key;
 185 } NtrHeapSlot;
 186
 187 typedef struct NtrHeap {
 188     int size;
 189     int nslots;
 190     NtrHeapSlot *slots;
 191 } NtrHeap;
 192
 193 typedef struct NtrPartTR {
 194     int nparts;                 /* number of parts */
 195     DdNode **part;              /* array of parts */
 196     DdNode **icube;             /* quantification cubes for image */
 197     DdNode **pcube;             /* quantification cubes for preimage */
 198     DdNode **nscube;            /* next state variables in each part */
 199     DdNode *preiabs;            /* present state vars and inputs in no part */
 200     DdNode *prepabs;            /* inputs in no part */
 201     DdNode *xw;                 /* cube of all present states and PIs */
 202     NtrHeap *factors;           /* factors extracted from the image */
 203     int nlatches;               /* number of latches */
 204     DdNode **x;                 /* array of present state variables */
 205     DdNode **y;                 /* array of next state variables */
 206 } NtrPartTR;
 207
 208 /*---------------------------------------------------------------------------*/
 209 /* Variable declarations                                                     */
 210 /*---------------------------------------------------------------------------*/
 211
 212 /*---------------------------------------------------------------------------*/
 213 /* Macro declarations                                                        */
 214 /*---------------------------------------------------------------------------*/
 215
 216 #ifndef TRUE
 217 #   define TRUE 1
 218 #endif
 219 #ifndef FALSE
 220 #   define FALSE 0
 221 #endif
 222
 223 /**Macro***********************************************************************
 224
 225   Synopsis     [Returns 1 if the two arguments are identical strings.]
 226
 227   Description  []
 228
 229   SideEffects  [none]
 230
 231   SeeAlso      []
 232
 233 ******************************************************************************/
 234 #define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0)
 235
 236
 237 /**AutomaticStart*************************************************************/
 238
 239 /*---------------------------------------------------------------------------*/
 240 /* Function prototypes                                                       */
 241 /*---------------------------------------------------------------------------*/
 242
 243 extern int Ntr_buildDDs (BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2);
 244 extern NtrPartTR * Ntr_buildTR (DdManager *dd, BnetNetwork *net, NtrOptions *option, int image);
 245 extern DdNode * Ntr_TransitiveClosure (DdManager *dd, NtrPartTR *TR, NtrOptions *option);
 246 extern int Ntr_Trav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 247 extern int Ntr_SCC (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 248 extern int Ntr_ClosureTrav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 249 extern void Ntr_freeTR (DdManager *dd, NtrPartTR *TR);
 250 extern NtrPartTR * Ntr_cloneTR (NtrPartTR *TR);
 251 extern DdNode * Ntr_initState (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 252 extern DdNode * Ntr_getStateCube (DdManager *dd, BnetNetwork *net, char *filename, int pr);
 253 extern int Ntr_Envelope (DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option);
 254 extern int Ntr_TestMinimization (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
 255 extern int Ntr_TestDensity (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
 256 extern int Ntr_TestDecomp (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
 257 extern int Ntr_VerifyEquivalence (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
 258 extern int Ntr_TestCofactorEstimate (DdManager * dd, BnetNetwork * net, NtrOptions * option);
 259 extern int Ntr_TestClipping (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
 260 extern int Ntr_TestEquivAndContain (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
 261 extern int Ntr_TestClosestCube (DdManager * dd, BnetNetwork * net, NtrOptions * option);
 262 extern int Ntr_TestTwoLiteralClauses (DdManager * dd, BnetNetwork * net1, NtrOptions * option);
 263 extern int Ntr_TestCharToVect(DdManager * dd, BnetNetwork * net1, NtrOptions * option);
 264 extern int Ntr_maxflow (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 265 extern double Ntr_maximum01Flow (DdManager *bdd, DdNode *sx, DdNode *ty, DdNode *E, DdNode **F, DdNode **cut, DdNode **x, DdNode **y, DdNode **z, int n, int pr);
 266 extern int Ntr_testZDD (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 267 extern int Ntr_testISOP (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 268 extern NtrHeap * Ntr_InitHeap (int size);
 269 extern void Ntr_FreeHeap (NtrHeap *heap);
 270 extern int Ntr_HeapInsert (NtrHeap *heap, void *item, int key);
 271 extern int Ntr_HeapExtractMin (NtrHeap *heap, void *item, int *key);
 272 extern int Ntr_HeapCount (NtrHeap *heap);
 273 extern NtrHeap * Ntr_HeapClone (NtrHeap *source);
 274 extern int Ntr_TestHeap (NtrHeap *heap, int i);
 275 extern int Ntr_ShortestPaths (DdManager *dd, BnetNetwork *net, NtrOptions *option);
 276
 277 /**AutomaticEnd***************************************************************/
 278
 279 #ifdef __cplusplus
 280 }
 281 #endif
 282
 283 #endif /* _NTR */