DSD.h

Go to the documentation of this file.

#ifndef _DSD
#define _DSD

#ifdef DISABLE_SBDD
  #define DISABLE_GC
  #define DISABLE_SM
#endif

#include "util.h"
#include "cudd.h"
#include "cuddInt.h"
#include "fixheap.h"
#include <assert.h>
#include <stdio.h>


#define VAR 0
#define PRIME 1
#define OR  2
#define XOR 3

#define MAX_NOT_ALLOWED ~0
#define TYPE_MASK 127<<25
#define SIZE_MASK 255<<24
#define MARK_MASK 1<<24
#define SATURATION 16384
#define CAN_MASK ((1<<16) - 1)<<16 



typedef struct DSDNode DSDNode;
typedef unsigned int int_32;
typedef unsigned short int_16;
typedef struct ActualNode ActualNode;
typedef struct DSDManager DSDManager;
typedef struct SupportList SupportList;



extern FixHeapPtr dsd_malloc_ptr;
extern FixHeapPtr actual_malloc_ptr;

struct ActualNode{
  DSDNode * decomposition;
  ActualNode * next;
};

struct SupportList{
  int_32 support_var;
  SupportList *next;
};



struct DSDNode{
  int_32 type_actualsize;
  
  int_32 topvar_refsize;

  ActualNode * actual_list;
  
  DdNode * symbolic_kernel;
  
  DdNode * bdd_analogue;
  
  DSDNode * next;
  
  DSDNode *parent;
  int *support;
};


struct DSDManager{
  DdManager * Ddmanager_analogue;

  DSDNode *one; 

  int_32 num_outputs;
  
  int_32 decomposed_outputs;
  
  int_32 num_blocks;
  
  int_32 num_unique_blocks;
  int_32 num_unique_symbolic_blocks;
  int_32 theoretical_DSD_consumption; 
  int_32 theoretical_Actual_consumption;
  int_32 theoretical_memory_consumption;
  int_32 garbage_cleans;

  DSDNode ** DSD_unique_table;
  
  int_32 DSD_unique_table_size;

  int_32 notdisjoint;

  int_32 num_DSD_nodes;
  int_32 max_DSD_nodes;

  int_32 support_size;
  int_32 max_support_size;

  double max_average_actualsize;
  double current_average_actualsize;
  int_32 max_actualsize;
  int_32 total_actualsize;

  int_32 max_memory_used; 
  int_32 current_memory_used;  


  int_32 dead_nodes_threshold; 

  int_32 dead_nodes_current; 


  int_32 num_disjoint;
  int_32 num_commons;
  int_32 num_entered;
  int_32 num_primes;
  int_32 num_newdecomp;

  int_32 num_snodes;
  int_32 num_onodes;
  DdNode **snodes_array;
  DdNode **onodes_array;
  int_32 snode_size;
  int_32 onode_size;
  int_32 snode_counter;
  int_32 onode_counter;

  int_32 num_nodes;
  DdNode **nodes_array;
  int_32 node_size;
  int_32 node_counter;

};


#define DSD_Regular(x) ((DSDNode *)((int)(x) & ~01))
#define DSD_Not(x) ((DSDNode *) ((int)(x) ^ 01))
#define DSD_Complement(x) ((DSDNode *) ((int)(x) | 01))
#define DSD_IsComplement(x) ((int) ((int) (x) & 01))


#define GET_TYPE(x) (((x)->type_actualsize & TYPE_MASK)>>25)
#define SET_TYPE(x, type) ((x)->type_actualsize = (((x)->type_actualsize & ~(TYPE_MASK)) | (type << 25)))
#define INPUT_SIZE(x) ((x)->type_actualsize & ~(SIZE_MASK))
#define SET_SIZE(x, size) ((x)->type_actualsize = (((x)->type_actualsize & (SIZE_MASK)) | (size)))
#define mark(x) ((x)->type_actualsize = (((x)->type_actualsize | (MARK_MASK))))
#define unmark(x) ((x)->type_actualsize = (((x)->type_actualsize & ~(MARK_MASK))))

#define marked(x) (((x)->type_actualsize & (MARK_MASK))>>24)
#define SET_CAN(x, value) ((x)->topvar_refsize = (((x)->topvar_refsize & ~(CAN_MASK)) | (value << 16)))
#define GET_CAN(x) (((x)->topvar_refsize & CAN_MASK)>>16)
#define GET_REF(x) ((x)->topvar_refsize & ~(CAN_MASK))

#endif

---