distr/dddmp/dddmp.h

   1 /**CHeaderFile*****************************************************************
   2
   3   FileName     [dddmp.h]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to read in and write out BDDs, ADDs
   8     and CNF formulas from and to files.]
   9
  10   Description  []
  11
  12   Author       [Gianpiero Cabodi and Stefano Quer]
  13
  14   Copyright    [
  15     Copyright (c) 2002 by Politecnico di Torino.
  16     All Rights Reserved. This software is for educational purposes only.
  17     Permission is given to academic institutions to use, copy, and modify
  18     this software and its documentation provided that this introductory
  19     message is not removed, that this software and its documentation is
  20     used for the institutions' internal research and educational purposes,
  21     and that no monies are exchanged. No guarantee is expressed or implied
  22     by the distribution of this code.
  23     Send bug-reports and/or questions to:
  24     {gianpiero.cabodi,stefano.quer}@polito.it.
  25     ]
  26
  27 ******************************************************************************/
  28
  29 #ifndef _DDDMP
  30 #define _DDDMP
  31
  32 #if 0
  33 #define DDDMP_DEBUG
  34 #endif
  35
  36 /*---------------------------------------------------------------------------*/
  37 /* Nested includes                                                           */
  38 /*---------------------------------------------------------------------------*/
  39
  40 #include "util.h"
  41 #include "cudd.h"
  42
  43 #ifdef __cplusplus
  44 extern "C" {
  45 #endif
  46
  47 /*---------------------------------------------------------------------------*/
  48 /* Constant declarations                                                     */
  49 /*---------------------------------------------------------------------------*/
  50
  51 /*
  52  *  Dddmp format version
  53  */
  54
  55 #define DDDMP_VERSION           "DDDMP-2.0"
  56
  57 /*
  58  *  Returned values (for theorically ALL the function of the package)
  59  */
  60
  61 #define DDDMP_FAILURE ((int) 0)
  62 #define DDDMP_SUCCESS ((int) 1)
  63
  64 /*
  65  *  Format modes for DD (BDD and ADD) files
  66  */
  67
  68 #define DDDMP_MODE_TEXT           ((int)'A')
  69 #define DDDMP_MODE_BINARY         ((int)'B')
  70 #define DDDMP_MODE_DEFAULT        ((int)'D')
  71
  72 /*---------------------------------------------------------------------------*/
  73 /* Structure declarations                                                    */
  74 /*---------------------------------------------------------------------------*/
  75
  76 /*---------------------------------------------------------------------------*/
  77 /* Type declarations                                                         */
  78 /*---------------------------------------------------------------------------*/
  79
  80 /**Enum************************************************************************
  81
  82   Synopsis    [Format modes for storing CNF files]
  83
  84   Description [Type supported for storing BDDs into CNF
  85     formulas.
  86     Used internally to select the proper storing format:
  87       DDDMP_CNF_MODE_NODE: create a CNF temporary variables for
  88                            each BDD node
  89       DDDMP_CNF_MODE_MAXTERM: no temporary variables
  90       DDDMP_CNF_MODE_BEST: trade-off between the two previous methods
  91     ]
  92
  93 ******************************************************************************/
  94
  95 typedef enum {
  96   DDDMP_CNF_MODE_NODE,
  97   DDDMP_CNF_MODE_MAXTERM,
  98   DDDMP_CNF_MODE_BEST
  99 } Dddmp_DecompCnfStoreType;
 100
 101 /**Enum************************************************************************
 102
 103   Synopsis    [Format modes for loading CNF files.]
 104
 105   Description [Type supported for loading CNF formulas into BDDs.
 106     Used internally to select the proper returning format:
 107     ]
 108
 109 ******************************************************************************/
 110
 111 typedef enum {
 112   DDDMP_CNF_MODE_NO_CONJ,
 113   DDDMP_CNF_MODE_NO_QUANT,
 114   DDDMP_CNF_MODE_CONJ_QUANT
 115 } Dddmp_DecompCnfLoadType;
 116
 117 /**Enum************************************************************************
 118
 119   Synopsis    [Type for supported decomposition types.]
 120
 121   Description [Type for supported decomposition types.
 122     Used internally to select the proper type (bdd, add, ...).
 123     Given externally as information fule content.
 124     ]
 125
 126 ******************************************************************************/
 127
 128 typedef enum {
 129   DDDMP_BDD,
 130   DDDMP_ADD,
 131   DDDMP_CNF,
 132   DDDMP_NONE
 133 } Dddmp_DecompType;
 134
 135
 136 /**Enum************************************************************************
 137
 138   Synopsis    [Type for variable extra info.]
 139
 140   Description [Type for variable extra info. Used to specify info stored
 141     in text mode.]
 142
 143 ******************************************************************************/
 144
 145 typedef enum {
 146   DDDMP_VARIDS,
 147   DDDMP_VARPERMIDS,
 148   DDDMP_VARAUXIDS,
 149   DDDMP_VARNAMES,
 150   DDDMP_VARDEFAULT
 151 } Dddmp_VarInfoType;
 152
 153 /**Enum************************************************************************
 154
 155   Synopsis    [Type for variable matching in BDD load.]
 156
 157   Description []
 158
 159 ******************************************************************************/
 160
 161 typedef enum {
 162   DDDMP_VAR_MATCHIDS,
 163   DDDMP_VAR_MATCHPERMIDS,
 164   DDDMP_VAR_MATCHAUXIDS,
 165   DDDMP_VAR_MATCHNAMES,
 166   DDDMP_VAR_COMPOSEIDS
 167 } Dddmp_VarMatchType;
 168
 169 /**Enum************************************************************************
 170
 171   Synopsis    [Type for BDD root matching in BDD load.]
 172
 173   Description []
 174
 175 ******************************************************************************/
 176
 177 typedef enum {
 178   DDDMP_ROOT_MATCHNAMES,
 179   DDDMP_ROOT_MATCHLIST
 180 } Dddmp_RootMatchType;
 181
 182 typedef struct Dddmp_Hdr_s Dddmp_Hdr_t;
 183
 184 /*---------------------------------------------------------------------------*/
 185 /* Variable declarations                                                     */
 186 /*---------------------------------------------------------------------------*/
 187
 188 /*---------------------------------------------------------------------------*/
 189 /* Macro declarations                                                        */
 190 /*---------------------------------------------------------------------------*/
 191
 192 /**Macro***********************************************************************
 193
 194   Synopsis    [Checks for fatal bugs]
 195
 196   Description [Conditional safety assertion. It prints out the file
 197     name and line number where the fatal error occurred.
 198     Messages are printed out on stderr.
 199     ]
 200
 201   SideEffects [None]
 202
 203   SeeAlso     []
 204
 205 ******************************************************************************/
 206
 207 #ifdef DDDMP_DEBUG
 208 #  define Dddmp_Assert(expr,errMsg) \
 209      { \
 210      if ((expr) == 0) { \
 211        fprintf (stderr, "FATAL ERROR: %s\n", errMsg); \
 212        fprintf (stderr, "             File %s -> Line %d\n", \
 213          __FILE__, __LINE__); \
 214        fflush (stderr); \
 215        exit (DDDMP_FAILURE); \
 216        } \
 217      }
 218 #else
 219 #  define Dddmp_Assert(expr,errMsg) \
 220      {}
 221 #endif
 222
 223 /**Macro***********************************************************************
 224
 225   Synopsis    [Checks for Warnings: If expr==1 it prints out the warning
 226     on stderr.]
 227
 228   Description []
 229
 230   SideEffects [None]
 231
 232   SeeAlso     []
 233
 234 ******************************************************************************/
 235
 236 #define Dddmp_Warning(expr,errMsg) \
 237   { \
 238   if ((expr) == 1) { \
 239     fprintf (stderr, "WARNING: %s\n", errMsg); \
 240     fprintf (stderr, "         File %s -> Line %d\n", \
 241       __FILE__, __LINE__); \
 242     fflush (stderr); \
 243     } \
 244   }
 245
 246 /**Macro***********************************************************************
 247
 248   Synopsis    [Checks for fatal bugs and return the DDDMP_FAILURE flag.]
 249
 250   Description []
 251
 252   SideEffects [None]
 253
 254   SeeAlso     []
 255
 256 ******************************************************************************/
 257
 258 #define Dddmp_CheckAndReturn(expr,errMsg) \
 259   { \
 260   if ((expr) == 1) { \
 261     fprintf (stderr, "FATAL ERROR: %s\n", errMsg); \
 262     fprintf (stderr, "             File %s -> Line %d\n", \
 263       __FILE__, __LINE__); \
 264     fflush (stderr); \
 265     return (DDDMP_FAILURE); \
 266     } \
 267   }
 268
 269 /**Macro***********************************************************************
 270
 271   Synopsis    [Checks for fatal bugs and go to the label to deal with
 272     the error.
 273     ]
 274
 275   Description []
 276
 277   SideEffects [None]
 278
 279   SeeAlso     []
 280
 281 ******************************************************************************/
 282
 283 #define Dddmp_CheckAndGotoLabel(expr,errMsg,label) \
 284   { \
 285   if ((expr) == 1) { \
 286     fprintf (stderr, "FATAL ERROR: %s\n", errMsg); \
 287     fprintf (stderr, "             File %s -> Line %d\n", \
 288       __FILE__, __LINE__); \
 289     fflush (stderr); \
 290     goto label; \
 291     } \
 292   }
 293
 294 /**AutomaticStart*************************************************************/
 295
 296 /*---------------------------------------------------------------------------*/
 297 /* Function prototypes                                                       */
 298 /*---------------------------------------------------------------------------*/
 299
 300 extern int Dddmp_Text2Bin(char *filein, char *fileout);
 301 extern int Dddmp_Bin2Text(char *filein, char *fileout);
 302 extern int Dddmp_cuddBddDisplayBinary(char *fileIn, char *fileOut);
 303 extern DdNode * Dddmp_cuddBddLoad(DdManager *ddMgr, Dddmp_VarMatchType varMatchMode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp);
 304 extern int Dddmp_cuddBddArrayLoad(DdManager *ddMgr, Dddmp_RootMatchType rootMatchMode, char **rootmatchnames, Dddmp_VarMatchType varMatchMode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp, DdNode ***pproots);
 305 extern DdNode * Dddmp_cuddAddLoad(DdManager *ddMgr, Dddmp_VarMatchType varMatchMode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp);
 306 extern int Dddmp_cuddAddArrayLoad(DdManager *ddMgr, Dddmp_RootMatchType rootMatchMode, char **rootmatchnames, Dddmp_VarMatchType varMatchMode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp, DdNode ***pproots);
 307 extern int Dddmp_cuddHeaderLoad (Dddmp_DecompType *ddType, int *nVars, int *nsuppvars, char ***suppVarNames, char ***orderedVarNames, int **varIds, int **composeIds, int **auxIds, int *nRoots, char *file, FILE *fp);
 308 extern int Dddmp_cuddBddLoadCnf(DdManager *ddMgr, Dddmp_VarMatchType varmatchmode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp, DdNode ***rootsPtrPtr, int *nRoots);
 309 extern int Dddmp_cuddBddArrayLoadCnf(DdManager *ddMgr, Dddmp_RootMatchType rootmatchmode, char **rootmatchnames, Dddmp_VarMatchType varmatchmode, char **varmatchnames, int *varmatchauxids, int *varcomposeids, int mode, char *file, FILE *fp, DdNode ***rootsPtrPtr, int *nRoots);
 310 extern int Dddmp_cuddHeaderLoadCnf (int *nVars, int *nsuppvars, char ***suppVarNames, char ***orderedVarNames, int **varIds, int **composeIds, int **auxIds, int *nRoots, char *file, FILE *fp);
 311 extern int Dddmp_cuddAddStore(DdManager *ddMgr, char *ddname, DdNode *f, char **varnames, int *auxids, int mode, Dddmp_VarInfoType varinfo, char *fname, FILE *fp);
 312 extern int Dddmp_cuddAddArrayStore(DdManager *ddMgr, char *ddname, int nRoots, DdNode **f, char **rootnames, char **varnames, int *auxids, int mode, Dddmp_VarInfoType varinfo, char *fname, FILE *fp);
 313 extern int Dddmp_cuddBddStore(DdManager *ddMgr, char *ddname, DdNode *f, char **varnames, int *auxids, int mode, Dddmp_VarInfoType varinfo, char *fname, FILE *fp);
 314 extern int Dddmp_cuddBddArrayStore(DdManager *ddMgr, char *ddname, int nRoots, DdNode **f, char **rootnames, char **varnames, int *auxids, int mode, Dddmp_VarInfoType varinfo, char *fname, FILE *fp);
 315 extern int Dddmp_cuddBddStoreCnf(DdManager *ddMgr, DdNode *f, Dddmp_DecompCnfStoreType mode, int noHeader, char **varNames, int *bddIds, int *bddAuxIds, int *cnfIds, int idInitial, int edgeInTh, int pathLengthTh, char *fname, FILE *fp, int *clauseNPtr, int *varNewNPtr);
 316 extern int Dddmp_cuddBddArrayStoreCnf(DdManager *ddMgr, DdNode **f, int rootN, Dddmp_DecompCnfStoreType mode, int noHeader, char **varNames, int *bddIds, int *bddAuxIds, int *cnfIds, int idInitial, int edgeInTh, int pathLengthTh, char *fname, FILE *fp, int *clauseNPtr, int *varNewNPtr);
 317 extern int Dddmp_cuddBddStorePrefix(DdManager *ddMgr, int nRoots, DdNode *f, char **inputNames, char **outputNames, char *modelName, char *fileName, FILE *fp);
 318 extern int Dddmp_cuddBddArrayStorePrefix(DdManager *ddMgr, int nroots, DdNode **f, char **inputNames, char **outputNames, char *modelName, char *fname, FILE *fp);
 319 extern int Dddmp_cuddBddStoreBlif(DdManager *ddMgr, int nRoots, DdNode *f, char **inputNames, char **outputNames, char *modelName, char *fileName, FILE *fp);
 320 extern int Dddmp_cuddBddArrayStoreBlif(DdManager *ddMgr, int nroots, DdNode **f, char **inputNames, char **outputNames, char *modelName, char *fname, FILE *fp);
 321 extern int Dddmp_cuddBddStoreSmv(DdManager *ddMgr, int nRoots, DdNode *f, char **inputNames, char **outputNames, char *modelName, char *fileName, FILE *fp);
 322 extern int Dddmp_cuddBddArrayStoreSmv(DdManager *ddMgr, int nroots, DdNode **f, char **inputNames, char **outputNames, char *modelName, char *fname, FILE *fp);
 323
 324 /**AutomaticEnd***************************************************************/
 325
 326 #ifdef __cplusplus
 327 }
 328 #endif
 329
 330 #endif