1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
/** \file     bdd_interface.h
 *  \brief    Functions to access BDD libraries.
 *  \author   Takahisa Toda
 */
#ifndef BDD_INTERFACE_H
#define BDD_INTERFACE_H

#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>
#include <limits.h>

#include "my_def.h"

#if defined(REDUCTION) // added
/*---------------------------------------------------------------------------*/
/* CUDD PACKAGE                                                  */
/*---------------------------------------------------------------------------*/
#include "util.h"
#include "cudd.h"
#include "cuddInt.h"

#define BDD_PACKAGE "CU Decision Diagram Package Release 2.5.0"
#define BDD_NULL  NULL
#define BDD_MAXITEMVAL  CUDD_MAXINDEX //!< maximum value that a BDD library can handle.

typedef DdNode *bddp; //!< pointer to a BDD node

extern DdManager *dd_mgr;


/* Common Operations */
static inline int bdd_init(itemval maxval, uintmax_t n)
{
  if(dd_mgr == NULL) {
    dd_mgr = Cudd_Init((DdHalfWord)maxval, (DdHalfWord)maxval, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, UINTMAX_C(1) << 34);
    //dd_mgr = Cudd_Init((DdHalfWord)maxval, (DdHalfWord)maxval, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
    ENSURE_TRUE_MSG(dd_mgr != NULL, "BDD manager initialization failed.");
    Cudd_DisableGarbageCollection(dd_mgr);// disable GC since we never do dereference of nodes.
#ifdef MISC_LOG
    if(Cudd_GarbageCollectionEnabled(dd_mgr)) printf("GC\tenabled\n");
    else                                      printf("GC\tdisabled\n");    
#endif /*MISC_LOG*/

    return ST_SUCCESS;
  } else {
    ENSURE_TRUE_WARN(false, "BDD manager already initialized.");
    return ST_FAILURE;
  }
}

static inline int bdd_quit(void)
{
  if(dd_mgr != NULL) {
    Cudd_Quit(dd_mgr);
    dd_mgr = NULL;
    return ST_SUCCESS;
  } else {
    ENSURE_TRUE_WARN(false, "BDD manager does not exist.");
    return ST_FAILURE;
  }
}

/* BDD Operations*/
static inline itemval bdd_itemval(bddp f)
{  
  assert(dd_mgr != NULL);
  assert(f      != BDD_NULL);

  bddp t = Cudd_Regular(f);
  return (itemval)Cudd_NodeReadIndex(t);
}

static inline bddp bdd_top(void)
{
  assert(dd_mgr != NULL);

  return Cudd_ReadOne(dd_mgr);
}

static inline bddp bdd_bot(void)
{
  assert(dd_mgr != NULL);

  return Cudd_ReadLogicZero(dd_mgr);
}

static inline int bdd_isconst(bddp f)
{
  assert(f != BDD_NULL);

  return (f==bdd_top() || f==bdd_bot());
}

static inline uintmax_t bdd_size(bddp f)
{
  assert(dd_mgr != NULL);
  assert(f      != BDD_NULL);

  return (uintmax_t)Cudd_DagSize(f);
}

static inline bddp bdd_hi(bddp f)
{
  assert(dd_mgr != NULL);
  assert(f      != BDD_NULL);
  assert(!bdd_isconst(f));

  bddp t = Cudd_Regular(f);
  if (Cudd_IsComplement(f)) return Cudd_Not(cuddT(t));
  else                      return cuddT(t);
}

static inline bddp bdd_lo(bddp f)
{
  assert(dd_mgr != NULL);
  assert(f      != BDD_NULL);
  assert(!bdd_isconst(f));

  bddp t = Cudd_Regular(f);
  if (Cudd_IsComplement(f)) return Cudd_Not(cuddE(t));
  else                      return cuddE(t);
}


static inline bddp bdd_and(bddp f, bddp g)
{
  assert(dd_mgr != NULL);
  assert(f != BDD_NULL && g != BDD_NULL);

  return Cudd_bddAnd(dd_mgr, f, g);
}

static inline bddp bdd_node(itemval i, bddp lo, bddp hi)
{
  assert(dd_mgr != NULL);
  assert(!bdd_isconst(hi)? i < bdd_itemval(hi): true);
  assert(!bdd_isconst(lo)? i < bdd_itemval(lo): true);

  bddp f;
  if(lo == hi) {
    f = hi;
  } else {
    if (Cudd_IsComplement(hi)) {
      f = cuddUniqueInter(dd_mgr,(int)i,Cudd_Not(hi),Cudd_Not(lo));
      ENSURE_TRUE_MSG(f != BDD_NULL, "BDD operation failed");
      f = Cudd_Not(f);
    } else {
      f = cuddUniqueInter(dd_mgr,(int)i, hi, lo);
      ENSURE_TRUE_MSG(f != BDD_NULL, "BDD operation failed");
    }
  }
  return f;
}

#endif /*REDUCTION*/

#endif /*BDD_INTERFACE_H*/