distr/dddmp/dddmpInt.h

   1 /**CHeaderFile*****************************************************************
   2
   3   FileName     [dddmpInt.h]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Low level functions to read in and write out bdds to file]
   8
   9   Description  [A set of internal low-level routines of the dddmp package
  10     doing:
  11     <ul>
  12       <li> read and write of node codes in binary mode,
  13       <li> read and write of integers in binary mode,
  14       <li> marking/unmarking nodes as visited,
  15       <li> numbering nodes.
  16     </ul>
  17     ]
  18
  19   Author       [Gianpiero Cabodi and Stefano Quer]
  20
  21   Copyright    [
  22     Copyright (c) 2002 by Politecnico di Torino.
  23     All Rights Reserved. This software is for educational purposes only.
  24     Permission is given to academic institutions to use, copy, and modify
  25     this software and its documentation provided that this introductory
  26     message is not removed, that this software and its documentation is
  27     used for the institutions' internal research and educational purposes,
  28     and that no monies are exchanged. No guarantee is expressed or implied
  29     by the distribution of this code.
  30     Send bug-reports and/or questions to:
  31     {gianpiero.cabodi,stefano.quer}@polito.it.
  32     ]
  33
  34 ******************************************************************************/
  35
  36 #ifndef _DDDMPINT
  37 #define _DDDMPINT
  38
  39 #include "dddmp.h"
  40 #include "cuddInt.h"
  41
  42 #ifdef __cplusplus
  43 extern "C" {
  44 #endif
  45
  46 /*---------------------------------------------------------------------------*/
  47 /* Constant declarations                                                     */
  48 /*---------------------------------------------------------------------------*/
  49
  50 /* constants for code fields */
  51 #define DDDMP_TERMINAL      0
  52 #define DDDMP_ABSOLUTE_ID   1
  53 #define DDDMP_RELATIVE_ID   2
  54 #define DDDMP_RELATIVE_1    3
  55
  56 #define DDDMP_MAXSTRLEN 500
  57
  58 /*---------------------------------------------------------------------------*/
  59 /* Type declarations                                                         */
  60 /*---------------------------------------------------------------------------*/
  61
  62 /*---------------------------------------------------------------------------*/
  63 /* Structure declarations                                                     */
  64 /*---------------------------------------------------------------------------*/
  65
  66 /**Struct**********************************************************************
  67  Synopsis    [used in binary mode to store code info of a dd node]
  68  Description [V , T , E store the mode used to represent variable, Then
  69               and Else indexes. An index is either an absolute
  70               ( DDDMP_ABSOLUTE_ID ),
  71               a relative numbers ( DDDMP_RELATIVE_ID , DDDMP_RELATIVE_1 ) or
  72               a terminal node ( DDDMP_TERMINAL ) .
  73               Ecomp is used for the complemented edge attribute.
  74              ]
  75  SideEffect  [none]
  76  SeeAlso     [DddmpWriteCode DddmpReadCode]
  77 ******************************************************************************/
  78
  79 struct binary_dd_code {
  80   unsigned  Unused : 1;
  81   unsigned  V      : 2;
  82   unsigned  T      : 2;
  83   unsigned  Ecompl : 1;
  84   unsigned  E      : 2;
  85 };
  86
  87 /**Struct*********************************************************************
  88
  89  Synopsis    [BDD file header]
  90
  91  Description [Structure containing the BDD header file infos]
  92
  93 ******************************************************************************/
  94
  95 struct Dddmp_Hdr_s {
  96   char *ver;
  97   char mode;
  98   Dddmp_DecompType ddType;
  99   Dddmp_VarInfoType varinfo;
 100   char *dd;
 101   int nnodes;
 102   int nVars;
 103   int nsuppvars;
 104   char **orderedVarNames;
 105   char **suppVarNames;
 106   int *ids;
 107   int *permids;
 108   int *auxids;
 109   int *cnfids;
 110   int nRoots;
 111   int *rootids;
 112   char **rootnames;
 113   int nAddedCnfVar;
 114   int nVarsCnf;
 115   int nClausesCnf;
 116 };
 117
 118 /*---------------------------------------------------------------------------*/
 119 /* Variable declarations                                                     */
 120 /*---------------------------------------------------------------------------*/
 121
 122 /*---------------------------------------------------------------------------*/
 123 /* Macro declarations                                                        */
 124 /*---------------------------------------------------------------------------*/
 125
 126 /**Macro***********************************************************************
 127
 128   Synopsis     [Memory Allocation Macro for DDDMP]
 129
 130   Description  []
 131
 132   SideEffects  [None]
 133
 134   SeeAlso      []
 135
 136 ******************************************************************************/
 137
 138 #ifdef ALLOC
 139 #  define DDDMP_ALLOC(type, num)        ALLOC(type,num)
 140 #else
 141 #  define DDDMP_ALLOC(type, num)        \
 142      ((type *) malloc(sizeof(type) * (num)))
 143 #endif
 144
 145 /**Macro***********************************************************************
 146
 147   Synopsis     [Memory Free Macro for DDDMP]
 148
 149   Description  []
 150
 151   SideEffects  [None]
 152
 153   SeeAlso      []
 154
 155 ******************************************************************************/
 156
 157 #ifdef FREE
 158 #define DDDMP_FREE(p)  (FREE(p))
 159 #else
 160 #define DDDMP_FREE(p)   \
 161     ((p)!=NULL)?(free(p)):0)
 162 #endif
 163
 164
 165 /**AutomaticStart*************************************************************/
 166
 167 /*---------------------------------------------------------------------------*/
 168 /* Function prototypes                                                       */
 169 /*---------------------------------------------------------------------------*/
 170
 171 extern int DddmpWriteCode(FILE *fp, struct binary_dd_code code);
 172 extern int DddmpReadCode(FILE *fp, struct binary_dd_code *pcode);
 173 extern int DddmpWriteInt(FILE *fp, int id);
 174 extern int DddmpReadInt(FILE *fp, int *pid);
 175 extern int DddmpNumberAddNodes(DdManager *ddMgr, DdNode **f, int n);
 176 extern void DddmpUnnumberAddNodes(DdManager *ddMgr, DdNode **f, int n);
 177 extern void DddmpWriteNodeIndexAdd(DdNode *f, int id);
 178 extern int DddmpReadNodeIndexAdd(DdNode *f);
 179 extern int DddmpVisitedAdd(DdNode *f);
 180 extern void DddmpSetVisitedAdd(DdNode *f);
 181 extern void DddmpClearVisitedAdd(DdNode *f);
 182 extern int DddmpNumberBddNodes(DdManager *ddMgr, DdNode **f, int n);
 183 extern void DddmpUnnumberBddNodes(DdManager *ddMgr, DdNode **f, int n);
 184 extern void DddmpWriteNodeIndexBdd(DdNode *f, int id);
 185 extern int DddmpReadNodeIndexBdd(DdNode *f);
 186 extern int DddmpVisitedBdd(DdNode *f);
 187 extern void DddmpSetVisitedBdd(DdNode *f);
 188 extern void DddmpClearVisitedBdd(DdNode *f);
 189 extern int DddmpNumberDdNodesCnf(DdManager *ddMgr, DdNode **f, int rootN, int *cnfIds, int id);
 190 extern int DddmpDdNodesCountEdgesAndNumber(DdManager *ddMgr, DdNode **f, int rootN, int edgeInTh, int pathLengthTh, int *cnfIds, int id);
 191 extern void DddmpUnnumberDdNodesCnf(DdManager *ddMgr, DdNode **f, int rootN);
 192 extern int DddmpPrintBddAndNext(DdManager *ddMgr, DdNode **f, int rootN);
 193 extern int DddmpWriteNodeIndexCnf(DdNode *f, int id);
 194 extern int DddmpVisitedCnf(DdNode *f);
 195 extern void DddmpSetVisitedCnf(DdNode *f);
 196 extern int DddmpReadNodeIndexCnf(DdNode *f);
 197 extern int DddmpCuddDdArrayStoreBdd(Dddmp_DecompType ddType, DdManager *ddMgr, char *ddname, int nRoots, DdNode **f, char **rootnames, char **varnames, int *auxids, int mode, Dddmp_VarInfoType varinfo, char *fname, FILE *fp);
 198 extern int DddmpCuddBddArrayStore(Dddmp_DecompType ddType, DdManager *ddMgr, char *ddname, int nRoots, DdNode **f, char **rootnames, char **varnames, int *auxids, int mode, Dddmp_VarInfoType varinfo, char *fname, FILE *fp);
 199 extern int QsortStrcmp(const void *ps1, const void *ps2);
 200 extern int FindVarname(char *name, char **array, int n);
 201 extern char * DddmpStrDup(char *str);
 202 extern char ** DddmpStrArrayDup(char **array, int n);
 203 extern char ** DddmpStrArrayRead(FILE *fp, int n);
 204 extern int DddmpStrArrayWrite(FILE *fp, char **array, int n);
 205 extern void DddmpStrArrayFree(char **array, int n);
 206 extern int * DddmpIntArrayDup(int *array, int n);
 207 extern int * DddmpIntArrayRead(FILE *fp, int n);
 208 extern int DddmpIntArrayWrite(FILE *fp, int *array, int n);
 209
 210 /**AutomaticEnd***************************************************************/
 211
 212 #ifdef __cplusplus
 213 }
 214 #endif
 215
 216 #endif