ntr.h

Go to the documentation of this file.

#ifndef _NTR
#define _NTR

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/

#include "dddmp.h"
#include "bnet.h"

#ifdef __cplusplus
extern "C" {
#endif

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define PI_PS_FROM_FILE 0
#define PI_PS_DFS   1
#define PI_PS_GIVEN 2

#define NTR_IMAGE_MONO 0
#define NTR_IMAGE_PART 1
#define NTR_IMAGE_CLIP 2
#define NTR_IMAGE_DEPEND 3

#define NTR_UNDER_APPROX 0
#define NTR_OVER_APPROX 1

#define NTR_FROM_NEW 0
#define NTR_FROM_REACHED 1
#define NTR_FROM_RESTRICT 2
#define NTR_FROM_COMPACT 3
#define NTR_FROM_SQUEEZE 4
#define NTR_FROM_UNDERAPPROX 5
#define NTR_FROM_OVERAPPROX 6

#define NTR_GROUP_NONE 0
#define NTR_GROUP_DEFAULT 1
#define NTR_GROUP_FIXED 2

#define NTR_SHORT_NONE 0
#define NTR_SHORT_BELLMAN 1
#define NTR_SHORT_FLOYD 2
#define NTR_SHORT_SQUARE 3

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct  NtrOptions {
    long    initialTime;    
    int     verify;     
    char    *file1;     
    char    *file2;     
    int     second;     
    int     traverse;   
    int     depend;     
    int     image;      
    double  imageClip;  
    int     approx;     
    int     threshold;  
    int     from;       
    int     groupnsps;  
    int     closure;    
    double  closureClip;    
    int     envelope;   
    int     scc;        
    int     zddtest;    
    int     printcover; 
    int     maxflow;    
    int     shortPath;  
    int     selectiveTrace; 
    char    *sinkfile;  
    int     partition;  
    int     char2vect;  
    int     density;    
    double  quality;    
    int     decomp;     
    int     cofest;     
    double  clip;       
    int     dontcares;  
    int     closestCube;    
    int     clauses;    
    int     noBuild;    
    int     stateOnly;  
    char    *node;      
    int     locGlob;    
    int     progress;   
    int     cacheSize;  
    size_t   maxMemory; 
    size_t   maxMemHard;    
    unsigned int maxLive;   
    int     slots;      
    int     ordering;   
    char    *orderPiPs; 
    Cudd_ReorderingType reordering; 
    int     autoDyn;    
    Cudd_ReorderingType autoMethod; 
    char    *treefile;  
    int     firstReorder;   
    int     countDead;  
    int     maxGrowth;  
    Cudd_AggregationType groupcheck; 
    int     arcviolation;   
    int     symmviolation;  
    int     recomb;     
    int     nodrop;     
    int     signatures; 
    int     gaOnOff;    
    int     populationSize; 
    int     numberXovers;   
    int     bdddump;    
    int     dumpFmt;    
    char    *dumpfile;  
    int     store;      
    char    *storefile; 
    int     load;       
    char    *loadfile;  
    int     verb;       
    int32_t seed;       
} NtrOptions;

typedef struct NtrHeapSlot NtrHeapSlot;

typedef struct NtrHeap NtrHeap;

typedef struct NtrPartTR {
    int nparts;         
    DdNode **part;      
    DdNode **icube;     
    DdNode **pcube;     
    DdNode **nscube;        
    DdNode *preiabs;        
    DdNode *prepabs;        
    DdNode *xw;         
    NtrHeap *factors;       
    int nlatches;       
    DdNode **x;         
    DdNode **y;         
} NtrPartTR;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#ifndef TRUE
#   define TRUE 1
#endif
#ifndef FALSE
#   define FALSE 0
#endif

#define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0)


/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

extern int Ntr_buildDDs (BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2);
extern NtrPartTR * Ntr_buildTR (DdManager *dd, BnetNetwork *net, NtrOptions *option, int image);
extern DdNode * Ntr_TransitiveClosure (DdManager *dd, NtrPartTR *TR, NtrOptions *option);
extern int Ntr_Trav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
extern int Ntr_SCC (DdManager *dd, BnetNetwork *net, NtrOptions *option);
extern int Ntr_ClosureTrav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
extern void Ntr_freeTR (DdManager *dd, NtrPartTR *TR);
extern NtrPartTR * Ntr_cloneTR (NtrPartTR *TR);
extern DdNode * Ntr_initState (DdManager *dd, BnetNetwork *net, NtrOptions *option);
extern DdNode * Ntr_getStateCube (DdManager *dd, BnetNetwork *net, char *filename, int pr);
extern int Ntr_Envelope (DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option);
extern int Ntr_TestMinimization (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
extern int Ntr_TestDensity (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
extern int Ntr_TestDecomp (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
extern int Ntr_VerifyEquivalence (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
extern int Ntr_TestCofactorEstimate (DdManager * dd, BnetNetwork * net, NtrOptions * option);
extern int Ntr_TestClipping (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
extern int Ntr_TestEquivAndContain (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
extern int Ntr_TestClosestCube (DdManager * dd, BnetNetwork * net, NtrOptions * option);
extern int Ntr_TestTwoLiteralClauses (DdManager * dd, BnetNetwork * net1, NtrOptions * option);
extern int Ntr_TestCharToVect(DdManager * dd, BnetNetwork * net1, NtrOptions * option);
extern int Ntr_maxflow (DdManager *dd, BnetNetwork *net, NtrOptions *option);
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);
extern int Ntr_testZDD (DdManager *dd, BnetNetwork *net, NtrOptions *option);
extern int Ntr_testISOP (DdManager *dd, BnetNetwork *net, NtrOptions *option);
extern NtrHeap * Ntr_InitHeap (int size);
extern void Ntr_FreeHeap (NtrHeap *heap);
extern int Ntr_HeapInsert (NtrHeap *heap, void *item, int key);
extern int Ntr_HeapExtractMin (NtrHeap *heap, void *item, int *key);
extern int Ntr_HeapCount (NtrHeap *heap);
extern NtrHeap * Ntr_HeapClone (NtrHeap *source);
extern void Ntr_HeapForeach (NtrHeap *heap, void (*f)(void *e, void *arg), void *arg);
extern int Ntr_TestHeap (NtrHeap *heap, int i);
extern int Ntr_ShortestPaths (DdManager *dd, BnetNetwork *net, NtrOptions *option);

#ifdef __cplusplus
}
#endif

#endif /* _NTR */