1291 lines
50 KiB
C
1291 lines
50 KiB
C
/**CHeaderFile*****************************************************************
|
|
|
|
FileName [cuddInt.h]
|
|
|
|
PackageName [cudd]
|
|
|
|
Synopsis [Internal data structures of the CUDD package.]
|
|
|
|
Description []
|
|
|
|
SeeAlso []
|
|
|
|
Author [Fabio Somenzi]
|
|
|
|
Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
|
|
|
|
All rights reserved.
|
|
|
|
Redistribution and use in source and binary forms, with or without
|
|
modification, are permitted provided that the following conditions
|
|
are met:
|
|
|
|
Redistributions of source code must retain the above copyright
|
|
notice, this list of conditions and the following disclaimer.
|
|
|
|
Redistributions in binary form must reproduce the above copyright
|
|
notice, this list of conditions and the following disclaimer in the
|
|
documentation and/or other materials provided with the distribution.
|
|
|
|
Neither the name of the University of Colorado nor the names of its
|
|
contributors may be used to endorse or promote products derived from
|
|
this software without specific prior written permission.
|
|
|
|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
|
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
|
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
|
|
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
|
|
COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
|
|
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
|
|
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
|
|
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
|
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
|
|
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
|
|
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
|
POSSIBILITY OF SUCH DAMAGE.]
|
|
|
|
Revision [$Id: cuddInt.h,v 1.1.2.1 2010-02-04 10:41:15 nusmv Exp $]
|
|
|
|
******************************************************************************/
|
|
|
|
#ifndef _CUDDINT
|
|
#define _CUDDINT
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Nested includes */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
#ifdef DD_MIS
|
|
#include "array.h"
|
|
#include "list.h"
|
|
#include "st.h"
|
|
#include "espresso.h"
|
|
|
|
#ifdef SIS
|
|
#include "graph.h"
|
|
#include "astg.h"
|
|
#endif
|
|
#include "network.h"
|
|
#endif
|
|
|
|
#include <math.h>
|
|
#include "cudd.h"
|
|
#include "st.h"
|
|
|
|
#ifdef __cplusplus
|
|
extern "C" {
|
|
#endif
|
|
|
|
#if defined(__GNUC__)
|
|
# define DD_INLINE __inline__
|
|
# if (__GNUC__ >2 || __GNUC_MINOR__ >=7)
|
|
# define DD_UNUSED __attribute__ ((__unused__))
|
|
# else
|
|
# define DD_UNUSED
|
|
# endif
|
|
#else
|
|
# if defined(__cplusplus)
|
|
# define DD_INLINE inline
|
|
# else
|
|
# define DD_INLINE
|
|
# endif
|
|
# define DD_UNUSED
|
|
#endif
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Constant declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
#define DD_MAXREF ((DdHalfWord) ~0)
|
|
|
|
#define DD_DEFAULT_RESIZE 10 /* how many extra variables */
|
|
/* should be added when resizing */
|
|
#define DD_MEM_CHUNK 1022
|
|
|
|
/* These definitions work for CUDD_VALUE_TYPE == double */
|
|
#define DD_TRUE_VAL (1.0)
|
|
#define DD_ZERO_VAL (0.0)
|
|
#define DD_EPSILON (1.0e-12)
|
|
|
|
/* The definitions of +/- infinity in terms of HUGE_VAL work on
|
|
** the DECstations and on many other combinations of OS/compiler.
|
|
*/
|
|
#ifdef HAVE_IEEE_754
|
|
# define DD_PLUS_INF_VAL (HUGE_VAL)
|
|
#else
|
|
# define DD_PLUS_INF_VAL (10e301)
|
|
# define DD_CRI_HI_MARK (10e150)
|
|
# define DD_CRI_LO_MARK (-(DD_CRI_HI_MARK))
|
|
#endif
|
|
#define DD_MINUS_INF_VAL (-(DD_PLUS_INF_VAL))
|
|
|
|
#define DD_NON_CONSTANT ((DdNode *) 1) /* for Cudd_bddIteConstant */
|
|
|
|
/* Unique table and cache management constants. */
|
|
#define DD_MAX_SUBTABLE_DENSITY 4 /* tells when to resize a subtable */
|
|
/* gc when this percent are dead (measured w.r.t. slots, not keys)
|
|
** The first limit (LO) applies normally. The second limit applies when
|
|
** the package believes more space for the unique table (i.e., more dead
|
|
** nodes) would improve performance, and the unique table is not already
|
|
** too large. The third limit applies when memory is low.
|
|
*/
|
|
#define DD_GC_FRAC_LO DD_MAX_SUBTABLE_DENSITY * 0.25
|
|
#define DD_GC_FRAC_HI DD_MAX_SUBTABLE_DENSITY * 1.0
|
|
#define DD_GC_FRAC_MIN 0.2
|
|
#define DD_MIN_HIT 30 /* resize cache when hit ratio
|
|
above this percentage (default) */
|
|
#define DD_MAX_LOOSE_FRACTION 5 /* 1 / (max fraction of memory used for
|
|
unique table in fast growth mode) */
|
|
#define DD_MAX_CACHE_FRACTION 3 /* 1 / (max fraction of memory used for
|
|
computed table if resizing enabled) */
|
|
#define DD_STASH_FRACTION 64 /* 1 / (fraction of memory set
|
|
aside for emergencies) */
|
|
#define DD_MAX_CACHE_TO_SLOTS_RATIO 4 /* used to limit the cache size */
|
|
|
|
/* Variable ordering default parameter values. */
|
|
#define DD_SIFT_MAX_VAR 1000
|
|
#define DD_SIFT_MAX_SWAPS 2000000
|
|
#define DD_DEFAULT_RECOMB 0
|
|
#define DD_MAX_REORDER_GROWTH 1.2
|
|
#define DD_FIRST_REORDER 4004 /* 4 for the constants */
|
|
#define DD_DYN_RATIO 2 /* when to dynamically reorder */
|
|
|
|
/* Primes for cache hash functions. */
|
|
#define DD_P1 12582917
|
|
#define DD_P2 4256249
|
|
#define DD_P3 741457
|
|
#define DD_P4 1618033999
|
|
|
|
/* Cache tags for 3-operand operators. These tags are stored in the
|
|
** least significant bits of the cache operand pointers according to
|
|
** the following scheme. The tag consists of two hex digits. Both digits
|
|
** must be even, so that they do not interfere with complementation bits.
|
|
** The least significant one is stored in Bits 3:1 of the f operand in the
|
|
** cache entry. Bit 1 is always 1, so that we can differentiate
|
|
** three-operand operations from one- and two-operand operations.
|
|
** Therefore, the least significant digit is one of {2,6,a,e}. The most
|
|
** significant digit occupies Bits 3:1 of the g operand in the cache
|
|
** entry. It can by any even digit between 0 and e. This gives a total
|
|
** of 5 bits for the tag proper, which means a maximum of 32 three-operand
|
|
** operations. */
|
|
#define DD_ADD_ITE_TAG 0x02
|
|
#define DD_BDD_AND_ABSTRACT_TAG 0x06
|
|
#define DD_BDD_XOR_EXIST_ABSTRACT_TAG 0x0a
|
|
#define DD_BDD_ITE_TAG 0x0e
|
|
#define DD_ADD_BDD_DO_INTERVAL_TAG 0x22
|
|
#define DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG 0x26
|
|
#define DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG 0x2a
|
|
#define DD_BDD_COMPOSE_RECUR_TAG 0x2e
|
|
#define DD_ADD_COMPOSE_RECUR_TAG 0x42
|
|
#define DD_ADD_NON_SIM_COMPOSE_TAG 0x46
|
|
#define DD_EQUIV_DC_TAG 0x4a
|
|
#define DD_ZDD_ITE_TAG 0x4e
|
|
#define DD_ADD_ITE_CONSTANT_TAG 0x62
|
|
#define DD_ADD_EVAL_CONST_TAG 0x66
|
|
#define DD_BDD_ITE_CONSTANT_TAG 0x6a
|
|
#define DD_ADD_OUT_SUM_TAG 0x6e
|
|
#define DD_BDD_LEQ_UNLESS_TAG 0x82
|
|
#define DD_ADD_TRIANGLE_TAG 0x86
|
|
|
|
/* Generator constants. */
|
|
#define CUDD_GEN_CUBES 0
|
|
#define CUDD_GEN_PRIMES 1
|
|
#define CUDD_GEN_NODES 2
|
|
#define CUDD_GEN_ZDD_PATHS 3
|
|
#define CUDD_GEN_EMPTY 0
|
|
#define CUDD_GEN_NONEMPTY 1
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Stucture declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
struct DdGen {
|
|
DdManager *manager;
|
|
int type;
|
|
int status;
|
|
union {
|
|
struct {
|
|
int *cube;
|
|
CUDD_VALUE_TYPE value;
|
|
} cubes;
|
|
struct {
|
|
int *cube;
|
|
DdNode *ub;
|
|
} primes;
|
|
struct {
|
|
int size;
|
|
} nodes;
|
|
} gen;
|
|
struct {
|
|
int sp;
|
|
#ifdef __osf__
|
|
#pragma pointer_size save
|
|
#pragma pointer_size short
|
|
#endif
|
|
DdNode **stack;
|
|
#ifdef __osf__
|
|
#pragma pointer_size restore
|
|
#endif
|
|
} stack;
|
|
DdNode *node;
|
|
};
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Type declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/* Hooks in CUDD are functions that the application registers with the
|
|
** manager so that they are called at appropriate times. The functions
|
|
** are passed the manager as argument; they should return 1 if
|
|
** successful and 0 otherwise.
|
|
*/
|
|
typedef struct DdHook { /* hook list element */
|
|
DD_HFP f; /* function to be called */
|
|
struct DdHook *next; /* next element in the list */
|
|
} DdHook;
|
|
|
|
#ifdef __osf__
|
|
#pragma pointer_size save
|
|
#pragma pointer_size short
|
|
#endif
|
|
|
|
typedef DdNode *DdNodePtr;
|
|
|
|
/* Generic local cache item. */
|
|
typedef struct DdLocalCacheItem {
|
|
DdNode *value;
|
|
#ifdef DD_CACHE_PROFILE
|
|
ptrint count;
|
|
#endif
|
|
DdNode *key[1];
|
|
} DdLocalCacheItem;
|
|
|
|
/* Local cache. */
|
|
typedef struct DdLocalCache {
|
|
DdLocalCacheItem *item;
|
|
unsigned int itemsize;
|
|
unsigned int keysize;
|
|
unsigned int slots;
|
|
int shift;
|
|
double lookUps;
|
|
double minHit;
|
|
double hits;
|
|
unsigned int maxslots;
|
|
DdManager *manager;
|
|
struct DdLocalCache *next;
|
|
} DdLocalCache;
|
|
|
|
/* Generic hash item. */
|
|
typedef struct DdHashItem {
|
|
struct DdHashItem *next;
|
|
ptrint count;
|
|
DdNode *value;
|
|
DdNode *key[1];
|
|
} DdHashItem;
|
|
|
|
/* Local hash table */
|
|
typedef struct DdHashTable {
|
|
unsigned int keysize;
|
|
unsigned int itemsize;
|
|
DdHashItem **bucket;
|
|
DdHashItem *nextFree;
|
|
DdHashItem **memoryList;
|
|
unsigned int numBuckets;
|
|
int shift;
|
|
unsigned int size;
|
|
unsigned int maxsize;
|
|
DdManager *manager;
|
|
} DdHashTable;
|
|
|
|
typedef struct DdCache {
|
|
DdNode *f,*g; /* DDs */
|
|
ptruint h; /* either operator or DD */
|
|
DdNode *data; /* already constructed DD */
|
|
#ifdef DD_CACHE_PROFILE
|
|
ptrint count;
|
|
#endif
|
|
} DdCache;
|
|
|
|
typedef struct DdSubtable { /* subtable for one index */
|
|
DdNode **nodelist; /* hash table */
|
|
int shift; /* shift for hash function */
|
|
unsigned int slots; /* size of the hash table */
|
|
unsigned int keys; /* number of nodes stored in this table */
|
|
unsigned int maxKeys; /* slots * DD_MAX_SUBTABLE_DENSITY */
|
|
unsigned int dead; /* number of dead nodes in this table */
|
|
unsigned int next; /* index of next variable in group */
|
|
int bindVar; /* flag to bind this variable to its level */
|
|
/* Fields for lazy sifting. */
|
|
Cudd_VariableType varType; /* variable type (ps, ns, pi) */
|
|
int pairIndex; /* corresponding variable index (ps <-> ns) */
|
|
int varHandled; /* flag: 1 means variable is already handled */
|
|
Cudd_LazyGroupType varToBeGrouped; /* tells what grouping to apply */
|
|
} DdSubtable;
|
|
|
|
struct DdManager { /* specialized DD symbol table */
|
|
/* Constants */
|
|
DdNode sentinel; /* for collision lists */
|
|
DdNode *one; /* constant 1 */
|
|
DdNode *zero; /* constant 0 */
|
|
/* NuSMV: add begin */
|
|
DdNode *val_true; /* constant TRUE */
|
|
DdNode *val_false; /* constant FALSE */
|
|
void *env_arg;
|
|
int (*print_fun)(struct DdManager*, FILE*, CUDD_VALUE_TYPE, void*);
|
|
char* (*sprint_fun)(struct DdManager*, CUDD_VALUE_TYPE, void*);
|
|
void (*type_error_fun)(struct DdManager*, FILE*, CUDD_VALUE_TYPE, void*);
|
|
void (*fatal_error_fun)(struct DdManager*, FILE*, const char*, void*);
|
|
/* NuSMV: add end */
|
|
DdNode *plusinfinity; /* plus infinity */
|
|
DdNode *minusinfinity; /* minus infinity */
|
|
DdNode *background; /* background value */
|
|
/* Computed Table */
|
|
DdCache *acache; /* address of allocated memory for cache */
|
|
DdCache *cache; /* the cache-based computed table */
|
|
unsigned int cacheSlots; /* total number of cache entries */
|
|
int cacheShift; /* shift value for cache hash function */
|
|
double cacheMisses; /* number of cache misses (since resizing) */
|
|
double cacheHits; /* number of cache hits (since resizing) */
|
|
double minHit; /* hit percentage above which to resize */
|
|
int cacheSlack; /* slots still available for resizing */
|
|
unsigned int maxCacheHard; /* hard limit for cache size */
|
|
/* Unique Table */
|
|
int size; /* number of unique subtables */
|
|
int sizeZ; /* for ZDD */
|
|
int maxSize; /* max number of subtables before resizing */
|
|
int maxSizeZ; /* for ZDD */
|
|
DdSubtable *subtables; /* array of unique subtables */
|
|
DdSubtable *subtableZ; /* for ZDD */
|
|
DdSubtable constants; /* unique subtable for the constants */
|
|
unsigned int slots; /* total number of hash buckets */
|
|
unsigned int keys; /* total number of BDD and ADD nodes */
|
|
unsigned int keysZ; /* total number of ZDD nodes */
|
|
unsigned int dead; /* total number of dead BDD and ADD nodes */
|
|
unsigned int deadZ; /* total number of dead ZDD nodes */
|
|
unsigned int maxLive; /* maximum number of live nodes */
|
|
unsigned int minDead; /* do not GC if fewer than these dead */
|
|
double gcFrac; /* gc when this fraction is dead */
|
|
int gcEnabled; /* gc is enabled */
|
|
unsigned int looseUpTo; /* slow growth beyond this limit */
|
|
/* (measured w.r.t. slots, not keys) */
|
|
unsigned int initSlots; /* initial size of a subtable */
|
|
DdNode **stack; /* stack for iterative procedures */
|
|
double allocated; /* number of nodes allocated */
|
|
/* (not during reordering) */
|
|
double reclaimed; /* number of nodes brought back from the dead */
|
|
int isolated; /* isolated projection functions */
|
|
int *perm; /* current variable perm. (index to level) */
|
|
int *permZ; /* for ZDD */
|
|
int *invperm; /* current inv. var. perm. (level to index) */
|
|
int *invpermZ; /* for ZDD */
|
|
DdNode **vars; /* projection functions */
|
|
int *map; /* variable map for fast swap */
|
|
DdNode **univ; /* ZDD 1 for each variable */
|
|
int linearSize; /* number of rows and columns of linear */
|
|
long *interact; /* interacting variable matrix */
|
|
long *linear; /* linear transform matrix */
|
|
/* Memory Management */
|
|
DdNode **memoryList; /* memory manager for symbol table */
|
|
DdNode *nextFree; /* list of free nodes */
|
|
char *stash; /* memory reserve */
|
|
#ifndef DD_NO_DEATH_ROW
|
|
DdNode **deathRow; /* queue for dereferencing */
|
|
int deathRowDepth; /* number of slots in the queue */
|
|
int nextDead; /* index in the queue */
|
|
unsigned deadMask; /* mask for circular index update */
|
|
#endif
|
|
/* General Parameters */
|
|
CUDD_VALUE_TYPE epsilon; /* tolerance on comparisons */
|
|
/* Dynamic Reordering Parameters */
|
|
int reordered; /* flag set at the end of reordering */
|
|
int reorderings; /* number of calls to Cudd_ReduceHeap */
|
|
int siftMaxVar; /* maximum number of vars sifted */
|
|
int siftMaxSwap; /* maximum number of swaps per sifting */
|
|
double maxGrowth; /* maximum growth during reordering */
|
|
double maxGrowthAlt; /* alternate maximum growth for reordering */
|
|
int reordCycle; /* how often to apply alternate threshold */
|
|
int autoDyn; /* automatic dynamic reordering flag (BDD) */
|
|
int autoDynZ; /* automatic dynamic reordering flag (ZDD) */
|
|
Cudd_ReorderingType autoMethod; /* default reordering method */
|
|
Cudd_ReorderingType autoMethodZ; /* default reordering method (ZDD) */
|
|
int realign; /* realign ZDD order after BDD reordering */
|
|
int realignZ; /* realign BDD order after ZDD reordering */
|
|
unsigned int nextDyn; /* reorder if this size is reached */
|
|
unsigned int countDead; /* if 0, count deads to trigger reordering */
|
|
MtrNode *tree; /* Variable group tree (BDD) */
|
|
MtrNode *treeZ; /* Variable group tree (ZDD) */
|
|
Cudd_AggregationType groupcheck; /* Used during group sifting */
|
|
int recomb; /* Used during group sifting */
|
|
int symmviolation; /* Used during group sifting */
|
|
int arcviolation; /* Used during group sifting */
|
|
int populationSize; /* population size for GA */
|
|
int numberXovers; /* number of crossovers for GA */
|
|
DdLocalCache *localCaches; /* local caches currently in existence */
|
|
#ifdef __osf__
|
|
#pragma pointer_size restore
|
|
#endif
|
|
char *hooks; /* application-specific field (used by vis) */
|
|
DdHook *preGCHook; /* hooks to be called before GC */
|
|
DdHook *postGCHook; /* hooks to be called after GC */
|
|
DdHook *preReorderingHook; /* hooks to be called before reordering */
|
|
DdHook *postReorderingHook; /* hooks to be called after reordering */
|
|
FILE *out; /* stdout for this manager */
|
|
FILE *err; /* stderr for this manager */
|
|
#ifdef __osf__
|
|
#pragma pointer_size save
|
|
#pragma pointer_size short
|
|
#endif
|
|
Cudd_ErrorType errorCode; /* info on last error */
|
|
/* Statistical counters. */
|
|
|
|
/* NuSMV: add begin */
|
|
ptruint memused; /* total memory allocated for the manager */
|
|
ptruint maxmem; /* target maximum memory */
|
|
ptruint maxmemhard; /* hard limit for maximum memory */
|
|
/* WAS: unsigned long memused; total memory allocated for the manager
|
|
unsigned long maxmem; target maximum memory
|
|
unsigned long maxmemhard; hard limit for maximum memory */
|
|
/* NuSMV: add end */
|
|
|
|
int garbageCollections; /* number of garbage collections */
|
|
long GCTime; /* total time spent in garbage collection */
|
|
long reordTime; /* total time spent in reordering */
|
|
double totCachehits; /* total number of cache hits */
|
|
double totCacheMisses; /* total number of cache misses */
|
|
double cachecollisions; /* number of cache collisions */
|
|
double cacheinserts; /* number of cache insertions */
|
|
double cacheLastInserts; /* insertions at the last cache resizing */
|
|
double cachedeletions; /* number of deletions during garbage coll. */
|
|
#ifdef DD_STATS
|
|
double nodesFreed; /* number of nodes returned to the free list */
|
|
double nodesDropped; /* number of nodes killed by dereferencing */
|
|
#endif
|
|
unsigned int peakLiveNodes; /* maximum number of live nodes */
|
|
#ifdef DD_UNIQUE_PROFILE
|
|
double uniqueLookUps; /* number of unique table lookups */
|
|
double uniqueLinks; /* total distance traveled in coll. chains */
|
|
#endif
|
|
#ifdef DD_COUNT
|
|
double recursiveCalls; /* number of recursive calls */
|
|
#ifdef DD_STATS
|
|
double nextSample; /* when to write next line of stats */
|
|
#endif
|
|
double swapSteps; /* number of elementary reordering steps */
|
|
#endif
|
|
#ifdef DD_MIS
|
|
/* mis/verif compatibility fields */
|
|
array_t *iton; /* maps ids in ddNode to node_t */
|
|
array_t *order; /* copy of order_list */
|
|
lsHandle handle; /* where it is in network BDD list */
|
|
network_t *network;
|
|
st_table *local_order; /* for local BDDs */
|
|
int nvars; /* variables used so far */
|
|
int threshold; /* for pseudo var threshold value*/
|
|
#endif
|
|
};
|
|
|
|
typedef struct Move {
|
|
DdHalfWord x;
|
|
DdHalfWord y;
|
|
unsigned int flags;
|
|
int size;
|
|
struct Move *next;
|
|
} Move;
|
|
|
|
/* Generic level queue item. */
|
|
typedef struct DdQueueItem {
|
|
struct DdQueueItem *next;
|
|
struct DdQueueItem *cnext;
|
|
void *key;
|
|
} DdQueueItem;
|
|
|
|
/* Level queue. */
|
|
typedef struct DdLevelQueue {
|
|
void *first;
|
|
DdQueueItem **last;
|
|
DdQueueItem *freelist;
|
|
DdQueueItem **buckets;
|
|
int levels;
|
|
int itemsize;
|
|
int size;
|
|
int maxsize;
|
|
int numBuckets;
|
|
int shift;
|
|
} DdLevelQueue;
|
|
|
|
#ifdef __osf__
|
|
#pragma pointer_size restore
|
|
#endif
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Variable declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Macro declarations */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Adds node to the head of the free list.]
|
|
|
|
Description [Adds node to the head of the free list. Does not
|
|
deallocate memory chunks that become free. This function is also
|
|
used by the dynamic reordering functions.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [cuddAllocNode cuddDynamicAllocNode cuddDeallocMove]
|
|
|
|
******************************************************************************/
|
|
#define cuddDeallocNode(unique,node) \
|
|
(node)->next = (unique)->nextFree; \
|
|
(unique)->nextFree = node;
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Adds node to the head of the free list.]
|
|
|
|
Description [Adds node to the head of the free list. Does not
|
|
deallocate memory chunks that become free. This function is also
|
|
used by the dynamic reordering functions.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [cuddDeallocNode cuddDynamicAllocNode]
|
|
|
|
******************************************************************************/
|
|
#define cuddDeallocMove(unique,node) \
|
|
((DdNode *)(node))->ref = 0; \
|
|
((DdNode *)(node))->next = (unique)->nextFree; \
|
|
(unique)->nextFree = (DdNode *)(node);
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Increases the reference count of a node, if it is not
|
|
saturated.]
|
|
|
|
Description [Increases the reference count of a node, if it is not
|
|
saturated. This being a macro, it is faster than Cudd_Ref, but it
|
|
cannot be used in constructs like cuddRef(a = b()).]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_Ref]
|
|
|
|
******************************************************************************/
|
|
#define cuddRef(n) cuddSatInc(Cudd_Regular(n)->ref)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Decreases the reference count of a node, if it is not
|
|
saturated.]
|
|
|
|
Description [Decreases the reference count of node. It is primarily
|
|
used in recursive procedures to decrease the ref count of a result
|
|
node before returning it. This accomplishes the goal of removing the
|
|
protection applied by a previous cuddRef. This being a macro, it is
|
|
faster than Cudd_Deref, but it cannot be used in constructs like
|
|
cuddDeref(a = b()).]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_Deref]
|
|
|
|
******************************************************************************/
|
|
#define cuddDeref(n) cuddSatDec(Cudd_Regular(n)->ref)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns 1 if the node is a constant node.]
|
|
|
|
Description [Returns 1 if the node is a constant node (rather than an
|
|
internal node). All constant nodes have the same index
|
|
(CUDD_CONST_INDEX). The pointer passed to cuddIsConstant must be regular.]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_IsConstant]
|
|
|
|
******************************************************************************/
|
|
#define cuddIsConstant(node) ((node)->index == CUDD_CONST_INDEX)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the then child of an internal node.]
|
|
|
|
Description [Returns the then child of an internal node. If
|
|
<code>node</code> is a constant node, the result is unpredictable.
|
|
The pointer passed to cuddT must be regular.]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_T]
|
|
|
|
******************************************************************************/
|
|
#define cuddT(node) ((node)->type.kids.T)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the else child of an internal node.]
|
|
|
|
Description [Returns the else child of an internal node. If
|
|
<code>node</code> is a constant node, the result is unpredictable.
|
|
The pointer passed to cuddE must be regular.]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_E]
|
|
|
|
******************************************************************************/
|
|
#define cuddE(node) ((node)->type.kids.E)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the value of a constant node.]
|
|
|
|
Description [Returns the value of a constant node. If
|
|
<code>node</code> is an internal node, the result is unpredictable.
|
|
The pointer passed to cuddV must be regular.]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_V]
|
|
|
|
******************************************************************************/
|
|
#define cuddV(node) ((node)->type.value)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Finds the current position of variable index in the
|
|
order.]
|
|
|
|
Description [Finds the current position of variable index in the
|
|
order. This macro duplicates the functionality of Cudd_ReadPerm,
|
|
but it does not check for out-of-bounds indices and it is more
|
|
efficient.]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_ReadPerm]
|
|
|
|
******************************************************************************/
|
|
#define cuddI(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->perm[(index)])
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Finds the current position of ZDD variable index in the
|
|
order.]
|
|
|
|
Description [Finds the current position of ZDD variable index in the
|
|
order. This macro duplicates the functionality of Cudd_ReadPermZdd,
|
|
but it does not check for out-of-bounds indices and it is more
|
|
efficient.]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [Cudd_ReadPermZdd]
|
|
|
|
******************************************************************************/
|
|
#define cuddIZ(dd,index) (((index)==CUDD_CONST_INDEX)?(int)(index):(dd)->permZ[(index)])
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Hash function for the unique table.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [ddCHash ddCHash2]
|
|
|
|
******************************************************************************/
|
|
/* NuSMV: add begin */
|
|
#define ddHash(f,g,s) \
|
|
((((unsigned)(ptruint)(f) * DD_P1 + \
|
|
(unsigned)(ptruint)(g)) * DD_P2) >> (s))
|
|
/* WAS: #if NUSMV_SIZEOF_VOID_P == 8 && NUSMV_SIZEOF_INT == 4
|
|
#define ddHash(f,g,s) \
|
|
((((unsigned)(unsigned long)(f) * DD_P1 + \
|
|
(unsigned)(unsigned long)(g)) * DD_P2) >> (s))
|
|
#else
|
|
#define ddHash(f,g,s) \
|
|
((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
|
|
#endif */
|
|
/* NuSMV: add end */
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Hash function for the cache.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [ddHash ddCHash2]
|
|
|
|
******************************************************************************/
|
|
/* NuSMV: add begin */
|
|
#define ddCHash(o,f,g,h,s) \
|
|
((((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
|
|
(unsigned)(ptruint)(g)) * DD_P2 + \
|
|
(unsigned)(ptruint)(h)) * DD_P3) >> (s))
|
|
/* WAS: #if NUSMV_SIZEOF_VOID_P == 8 && NUSMV_SIZEOF_INT == 4
|
|
#define ddCHash(o,f,g,h,s) \
|
|
((((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \
|
|
(unsigned)(unsigned long)(g)) * DD_P2 + \
|
|
(unsigned)(unsigned long)(h)) * DD_P3) >> (s))
|
|
#else
|
|
#define ddCHash(o,f,g,h,s) \
|
|
((((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2 + \
|
|
(unsigned)(h)) * DD_P3) >> (s))
|
|
#endif */
|
|
/* NuSMV: add end */
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Hash function for the cache for functions with two
|
|
operands.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [ddHash ddCHash]
|
|
|
|
******************************************************************************/
|
|
/* NuSMV: add begin */
|
|
#define ddCHash2(o,f,g,s) \
|
|
(((((unsigned)(ptruint)(f) + (unsigned)(ptruint)(o)) * DD_P1 + \
|
|
(unsigned)(ptruint)(g)) * DD_P2) >> (s))
|
|
/* WAS: #if NUSMV_SIZEOF_VOID_P == 8 && NUSMV_SIZEOF_INT == 4
|
|
#define ddCHash2(o,f,g,s) \
|
|
(((((unsigned)(unsigned long)(f) + (unsigned)(unsigned long)(o)) * DD_P1 + \
|
|
(unsigned)(unsigned long)(g)) * DD_P2) >> (s))
|
|
#else
|
|
#define ddCHash2(o,f,g,s) \
|
|
(((((unsigned)(f) + (unsigned)(o)) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s))
|
|
#endif */
|
|
/* NuSMV: add end */
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Clears the 4 least significant bits of a pointer.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
#define cuddClean(p) ((DdNode *)((ptruint)(p) & ~0xf))
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Computes the minimum of two numbers.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [ddMax]
|
|
|
|
******************************************************************************/
|
|
#define ddMin(x,y) (((y) < (x)) ? (y) : (x))
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Computes the maximum of two numbers.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [ddMin]
|
|
|
|
******************************************************************************/
|
|
#define ddMax(x,y) (((y) > (x)) ? (y) : (x))
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Computes the absolute value of a number.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
#define ddAbs(x) (((x)<0) ? -(x) : (x))
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns 1 if the absolute value of the difference of the two
|
|
arguments x and y is less than e.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
#define ddEqualVal(x,y,e) (ddAbs((x)-(y))<(e))
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Saturating increment operator.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [cuddSatDec]
|
|
|
|
******************************************************************************/
|
|
#if NUSMV_SIZEOF_VOID_P == 8 && NUSMV_SIZEOF_INT == 4
|
|
#define cuddSatInc(x) ((x)++)
|
|
#else
|
|
#define cuddSatInc(x) ((x) += (x) != (DdHalfWord)DD_MAXREF)
|
|
#endif
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Saturating decrement operator.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [cuddSatInc]
|
|
|
|
******************************************************************************/
|
|
#if NUSMV_SIZEOF_VOID_P == 8 && NUSMV_SIZEOF_INT == 4
|
|
#define cuddSatDec(x) ((x)--)
|
|
#else
|
|
#define cuddSatDec(x) ((x) -= (x) != (DdHalfWord)DD_MAXREF)
|
|
#endif
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the constant 1 node.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [DD_ZERO DD_PLUS_INFINITY DD_MINUS_INFINITY]
|
|
|
|
******************************************************************************/
|
|
#define DD_ONE(dd) ((dd)->one)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the arithmetic 0 constant node.]
|
|
|
|
Description [Returns the arithmetic 0 constant node. This is different
|
|
from the logical zero. The latter is obtained by
|
|
Cudd_Not(DD_TRUE(dd)).]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [DD_ONE Cudd_Not DD_PLUS_INFINITY DD_MINUS_INFINITY]
|
|
|
|
******************************************************************************/
|
|
#define DD_ZERO(dd) ((dd)->zero)
|
|
|
|
/* NuSMV: add begin */
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the constant TRUE node.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [DD_FALSE DD_PLUS_INFINITY DD_MINUS_INFINITY]
|
|
|
|
******************************************************************************/
|
|
#define DD_TRUE(dd) ((dd)->val_true)
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the constant FALSE node.]
|
|
|
|
Description [Returns the constant FALSE node. This is different
|
|
from the logical zero. The latter is obtained by
|
|
Cudd_Not(DD_TRUE(dd)).]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [DD_TRUE Cudd_Not DD_PLUS_INFINITY DD_MINUS_INFINITY]
|
|
|
|
******************************************************************************/
|
|
#define DD_FALSE(dd) ((dd)->val_false)
|
|
/* NuSMV: add end */
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the plus infinity constant node.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [DD_TRUE DD_FALSE DD_MINUS_INFINITY]
|
|
|
|
******************************************************************************/
|
|
#define DD_PLUS_INFINITY(dd) ((dd)->plusinfinity)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Returns the minus infinity constant node.]
|
|
|
|
Description []
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso [DD_TRUE DD_FALSE DD_PLUS_INFINITY]
|
|
|
|
******************************************************************************/
|
|
#define DD_MINUS_INFINITY(dd) ((dd)->minusinfinity)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.]
|
|
|
|
Description [Enforces DD_MINUS_INF_VAL <= x <= DD_PLUS_INF_VAL.
|
|
Furthermore, if x <= DD_MINUS_INF_VAL/2, x is set to
|
|
DD_MINUS_INF_VAL. Similarly, if DD_PLUS_INF_VAL/2 <= x, x is set to
|
|
DD_PLUS_INF_VAL. Normally this macro is a NOOP. However, if
|
|
HAVE_IEEE_754 is not defined, it makes sure that a value does not
|
|
get larger than infinity in absolute value, and once it gets to
|
|
infinity, stays there. If the value overflows before this macro is
|
|
applied, no recovery is possible.]
|
|
|
|
SideEffects [none]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
#ifdef HAVE_IEEE_754
|
|
#define cuddAdjust(x)
|
|
#else
|
|
#define cuddAdjust(x) ((x) = ((x) >= DD_CRI_HI_MARK) ? DD_PLUS_INF_VAL : (((x) <= DD_CRI_LO_MARK) ? DD_MINUS_INF_VAL : (x)))
|
|
#endif
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Extract the least significant digit of a double digit.]
|
|
|
|
Description [Extract the least significant digit of a double digit. Used
|
|
in the manipulation of arbitrary precision integers.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [DD_MSDIGIT]
|
|
|
|
******************************************************************************/
|
|
#define DD_LSDIGIT(x) ((x) & DD_APA_MASK)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Extract the most significant digit of a double digit.]
|
|
|
|
Description [Extract the most significant digit of a double digit. Used
|
|
in the manipulation of arbitrary precision integers.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso [DD_LSDIGIT]
|
|
|
|
******************************************************************************/
|
|
#define DD_MSDIGIT(x) ((x) >> DD_APA_BITS)
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Outputs a line of stats.]
|
|
|
|
Description [Outputs a line of stats if DD_COUNT and DD_STATS are
|
|
defined. Increments the number of recursive calls if DD_COUNT is
|
|
defined.]
|
|
|
|
SideEffects [None]
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
#ifdef DD_COUNT
|
|
#ifdef DD_STATS
|
|
#define statLine(dd) dd->recursiveCalls++; \
|
|
if (dd->recursiveCalls == dd->nextSample) {(void) fprintf(dd->err, \
|
|
"@%.0f: %u nodes %u live %.0f dropped %.0f reclaimed\n", dd->recursiveCalls, \
|
|
dd->keys, dd->keys - dd->dead, dd->nodesDropped, dd->reclaimed); \
|
|
dd->nextSample += 250000;}
|
|
#else
|
|
#define statLine(dd) dd->recursiveCalls++;
|
|
#endif
|
|
#else
|
|
#define statLine(dd)
|
|
#endif
|
|
|
|
/* NuSMV: added begin */
|
|
extern int node_is_failure(struct node* x);
|
|
#if !defined(NODE_PTR)
|
|
# define NODE_PTR(x) ((struct node*) x)
|
|
#endif
|
|
|
|
|
|
/**Macro***********************************************************************
|
|
|
|
Synopsis [Used to handle FAILURE noded (this is an extension
|
|
required by NuSMV]
|
|
|
|
Description []
|
|
|
|
SeeAlso []
|
|
|
|
******************************************************************************/
|
|
#define HANDLE_FAILURE(dd, n) \
|
|
if (cuddIsConstant(n) && node_is_failure(NODE_PTR(cuddV(n)))) return(n)
|
|
/* NuSMV: added end */
|
|
|
|
|
|
/**AutomaticStart*************************************************************/
|
|
|
|
/*---------------------------------------------------------------------------*/
|
|
/* Function prototypes */
|
|
/*---------------------------------------------------------------------------*/
|
|
|
|
extern DdNode * cuddAddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
|
|
extern DdNode * cuddAddUnivAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
|
|
extern DdNode * cuddAddOrAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
|
|
/* NuSMV: added begin */
|
|
extern DdNode * cudd_addApplyRecur (DdManager *dd, CUDD_VALUE_TYPE (*op)(), DdNode *f, DdNode *g, void* arg);
|
|
extern DdNode * cudd_addAndRecur (DdManager *manager, DdNode *f, DdNode *g);
|
|
extern DdNode * cudd_addOrRecur (DdManager *manager, DdNode *f, DdNode *g);
|
|
extern DdNode * cudd_addXorRecur (DdManager *manager, DdNode *f, DdNode *g);
|
|
extern DdNode * cudd_addNotRecur (DdManager *manager, DdNode *f);
|
|
extern DdNode * cudd_addIfThenRecur (DdManager *manager, DdNode *f, DdNode *g);
|
|
extern DdNode * cudd_addElseRecur (DdManager *manager, DdNode *f, DdNode *g);
|
|
extern DdNode * cudd_addCubeDiffRecur (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cudd_bddCubeDiffRecur (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern int Cudd_BddGetLowestVarRecur (DdManager *dd, DdNode * N, int index);
|
|
extern DdNode * Cudd_AddMakeVarMaskRecur (DdManager *dd, DdNode * N, int n, int l, int offset);
|
|
#if 0
|
|
/* NuSMV: added end */
|
|
extern DdNode * cuddAddApplyRecur (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
|
|
/* NuSMV: added begin */
|
|
#endif
|
|
/* NuSMV: added end */
|
|
extern DdNode * cuddAddMonadicApplyRecur (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
|
|
extern DdNode * cuddAddScalarInverseRecur (DdManager *dd, DdNode *f, DdNode *epsilon);
|
|
extern DdNode * cuddAddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
|
|
extern DdNode * cuddAddCmplRecur (DdManager *dd, DdNode *f);
|
|
extern DdNode * cuddAddNegateRecur (DdManager *dd, DdNode *f);
|
|
extern DdNode * cuddAddRoundOffRecur (DdManager *dd, DdNode *f, double trunc);
|
|
extern DdNode * cuddUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, int safe, double quality);
|
|
extern DdNode * cuddRemapUnderApprox (DdManager *dd, DdNode *f, int numVars, int threshold, double quality);
|
|
extern DdNode * cuddBiasedUnderApprox (DdManager *dd, DdNode *f, DdNode *b, int numVars, int threshold, double quality1, double quality0);
|
|
extern DdNode * cuddBddAndAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
|
|
extern int cuddAnnealing (DdManager *table, int lower, int upper);
|
|
extern DdNode * cuddBddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
|
|
extern DdNode * cuddBddXorExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube);
|
|
extern DdNode * cuddBddBooleanDiffRecur (DdManager *manager, DdNode *f, DdNode *var);
|
|
extern DdNode * cuddBddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
|
|
extern DdNode * cuddBddIntersectRecur (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddBddAndRecur (DdManager *manager, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddBddXorRecur (DdManager *manager, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddBddTransfer (DdManager *ddS, DdManager *ddD, DdNode *f);
|
|
extern DdNode * cuddAddBddDoPattern (DdManager *dd, DdNode *f);
|
|
extern int cuddInitCache (DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize);
|
|
extern void cuddCacheInsert (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data);
|
|
extern void cuddCacheInsert2 (DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g, DdNode *data);
|
|
extern void cuddCacheInsert1 (DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f, DdNode *data);
|
|
extern DdNode * cuddCacheLookup (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
|
|
extern DdNode * cuddCacheLookupZdd (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
|
|
extern DdNode * cuddCacheLookup2 (DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g);
|
|
extern DdNode * cuddCacheLookup1 (DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f);
|
|
extern DdNode * cuddCacheLookup2Zdd (DdManager *table, DdNode * (*)(DdManager *, DdNode *, DdNode *), DdNode *f, DdNode *g);
|
|
extern DdNode * cuddCacheLookup1Zdd (DdManager *table, DdNode * (*)(DdManager *, DdNode *), DdNode *f);
|
|
extern DdNode * cuddConstantLookup (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h);
|
|
extern int cuddCacheProfile (DdManager *table, FILE *fp);
|
|
extern void cuddCacheResize (DdManager *table);
|
|
extern void cuddCacheFlush (DdManager *table);
|
|
extern int cuddComputeFloorLog2 (unsigned int value);
|
|
extern int cuddHeapProfile (DdManager *dd);
|
|
extern void cuddPrintNode (DdNode *f, FILE *fp);
|
|
extern void cuddPrintVarGroups (DdManager * dd, MtrNode * root, int zdd, int silent);
|
|
extern DdNode * cuddBddClippingAnd (DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction);
|
|
extern DdNode * cuddBddClippingAndAbstract (DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction);
|
|
extern void cuddGetBranches (DdNode *g, DdNode **g1, DdNode **g0);
|
|
extern int cuddCheckCube (DdManager *dd, DdNode *g);
|
|
extern DdNode * cuddCofactorRecur (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddBddComposeRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *proj);
|
|
extern DdNode * cuddAddComposeRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *proj);
|
|
extern int cuddExact (DdManager *table, int lower, int upper);
|
|
extern DdNode * cuddBddConstrainRecur (DdManager *dd, DdNode *f, DdNode *c);
|
|
extern DdNode * cuddBddRestrictRecur (DdManager *dd, DdNode *f, DdNode *c);
|
|
extern DdNode * cuddBddNPAndRecur (DdManager *dd, DdNode *f, DdNode *c);
|
|
extern DdNode * cuddAddConstrainRecur (DdManager *dd, DdNode *f, DdNode *c);
|
|
extern DdNode * cuddAddRestrictRecur (DdManager *dd, DdNode *f, DdNode *c);
|
|
extern DdNode * cuddBddLICompaction (DdManager *dd, DdNode *f, DdNode *c);
|
|
extern int cuddGa (DdManager *table, int lower, int upper);
|
|
extern int cuddTreeSifting (DdManager *table, Cudd_ReorderingType method);
|
|
extern int cuddZddInitUniv (DdManager *zdd);
|
|
extern void cuddZddFreeUniv (DdManager *zdd);
|
|
extern void cuddSetInteract (DdManager *table, int x, int y);
|
|
extern int cuddTestInteract (DdManager *table, int x, int y);
|
|
extern int cuddInitInteract (DdManager *table);
|
|
extern DdLocalCache * cuddLocalCacheInit (DdManager *manager, unsigned int keySize, unsigned int cacheSize, unsigned int maxCacheSize);
|
|
extern void cuddLocalCacheQuit (DdLocalCache *cache);
|
|
extern void cuddLocalCacheInsert (DdLocalCache *cache, DdNodePtr *key, DdNode *value);
|
|
extern DdNode * cuddLocalCacheLookup (DdLocalCache *cache, DdNodePtr *key);
|
|
extern void cuddLocalCacheClearDead (DdManager *manager);
|
|
extern int cuddIsInDeathRow (DdManager *dd, DdNode *f);
|
|
extern int cuddTimesInDeathRow (DdManager *dd, DdNode *f);
|
|
extern void cuddLocalCacheClearAll (DdManager *manager);
|
|
#ifdef DD_CACHE_PROFILE
|
|
extern int cuddLocalCacheProfile (DdLocalCache *cache);
|
|
#endif
|
|
extern DdHashTable * cuddHashTableInit (DdManager *manager, unsigned int keySize, unsigned int initSize);
|
|
extern void cuddHashTableQuit (DdHashTable *hash);
|
|
extern int cuddHashTableInsert (DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count);
|
|
extern DdNode * cuddHashTableLookup (DdHashTable *hash, DdNodePtr *key);
|
|
extern int cuddHashTableInsert1 (DdHashTable *hash, DdNode *f, DdNode *value, ptrint count);
|
|
extern DdNode * cuddHashTableLookup1 (DdHashTable *hash, DdNode *f);
|
|
extern int cuddHashTableInsert2 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count);
|
|
extern DdNode * cuddHashTableLookup2 (DdHashTable *hash, DdNode *f, DdNode *g);
|
|
extern int cuddHashTableInsert3 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count);
|
|
extern DdNode * cuddHashTableLookup3 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h);
|
|
extern DdLevelQueue * cuddLevelQueueInit (int levels, int itemSize, int numBuckets);
|
|
extern void cuddLevelQueueQuit (DdLevelQueue *queue);
|
|
extern void * cuddLevelQueueEnqueue (DdLevelQueue *queue, void *key, int level);
|
|
extern void cuddLevelQueueDequeue (DdLevelQueue *queue, int level);
|
|
extern int cuddLinearAndSifting (DdManager *table, int lower, int upper);
|
|
extern int cuddLinearInPlace (DdManager * table, int x, int y);
|
|
extern void cuddUpdateInteractionMatrix (DdManager * table, int xindex, int yindex);
|
|
extern int cuddInitLinear (DdManager *table);
|
|
extern int cuddResizeLinear (DdManager *table);
|
|
extern DdNode * cuddBddLiteralSetIntersectionRecur (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddCProjectionRecur (DdManager *dd, DdNode *R, DdNode *Y, DdNode *Ysupp);
|
|
extern DdNode * cuddBddClosestCube (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE bound);
|
|
extern void cuddReclaim (DdManager *table, DdNode *n);
|
|
extern void cuddReclaimZdd (DdManager *table, DdNode *n);
|
|
extern void cuddClearDeathRow (DdManager *table);
|
|
extern void cuddShrinkDeathRow (DdManager *table);
|
|
extern DdNode * cuddDynamicAllocNode (DdManager *table);
|
|
extern int cuddSifting (DdManager *table, int lower, int upper);
|
|
extern int cuddSwapping (DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic);
|
|
extern int cuddNextHigh (DdManager *table, int x);
|
|
extern int cuddNextLow (DdManager *table, int x);
|
|
extern int cuddSwapInPlace (DdManager *table, int x, int y);
|
|
extern int cuddBddAlignToZdd (DdManager *table);
|
|
extern DdNode * cuddBddMakePrime (DdManager *dd, DdNode *cube, DdNode *f);
|
|
extern DdNode * cuddSolveEqnRecur (DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i);
|
|
extern DdNode * cuddVerifySol (DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n);
|
|
#ifdef ST_INCLUDED
|
|
extern DdNode* cuddSplitSetRecur (DdManager *manager, st_table *mtable, int *varSeen, DdNode *p, double n, double max, int index);
|
|
#endif
|
|
extern DdNode * cuddSubsetHeavyBranch (DdManager *dd, DdNode *f, int numVars, int threshold);
|
|
extern DdNode * cuddSubsetShortPaths (DdManager *dd, DdNode *f, int numVars, int threshold, int hardlimit);
|
|
extern int cuddSymmCheck (DdManager *table, int x, int y);
|
|
extern int cuddSymmSifting (DdManager *table, int lower, int upper);
|
|
extern int cuddSymmSiftingConv (DdManager *table, int lower, int upper);
|
|
extern DdNode * cuddAllocNode (DdManager *unique);
|
|
extern DdManager * cuddInitTable (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo);
|
|
extern void cuddFreeTable (DdManager *unique);
|
|
extern int cuddGarbageCollect (DdManager *unique, int clearCache);
|
|
extern DdNode * cuddZddGetNode (DdManager *zdd, int id, DdNode *T, DdNode *E);
|
|
extern DdNode * cuddZddGetNodeIVO (DdManager *dd, int index, DdNode *g, DdNode *h);
|
|
extern DdNode * cuddUniqueInter (DdManager *unique, int index, DdNode *T, DdNode *E);
|
|
extern DdNode * cuddUniqueInterIVO (DdManager *unique, int index, DdNode *T, DdNode *E);
|
|
extern DdNode * cuddUniqueInterZdd (DdManager *unique, int index, DdNode *T, DdNode *E);
|
|
extern DdNode * cuddUniqueConst (DdManager *unique, CUDD_VALUE_TYPE value);
|
|
extern void cuddRehash (DdManager *unique, int i);
|
|
extern void cuddShrinkSubtable (DdManager *unique, int i);
|
|
extern int cuddInsertSubtables (DdManager *unique, int n, int level);
|
|
extern int cuddDestroySubtables (DdManager *unique, int n);
|
|
extern int cuddResizeTableZdd (DdManager *unique, int index);
|
|
extern void cuddSlowTableGrowth (DdManager *unique);
|
|
extern int cuddP (DdManager *dd, DdNode *f);
|
|
#ifdef ST_INCLUDED
|
|
extern enum st_retval cuddStCountfree (char *key, char *value, char *arg);
|
|
extern int cuddCollectNodes (DdNode *f, st_table *visited);
|
|
#endif
|
|
extern DdNodePtr * cuddNodeArray (DdNode *f, int *n);
|
|
extern int cuddWindowReorder (DdManager *table, int low, int high, Cudd_ReorderingType submethod);
|
|
extern DdNode * cuddZddProduct (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddZddUnateProduct (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddZddWeakDiv (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddZddWeakDivF (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddZddDivide (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern DdNode * cuddZddDivideF (DdManager *dd, DdNode *f, DdNode *g);
|
|
extern int cuddZddGetCofactors3 (DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd);
|
|
extern int cuddZddGetCofactors2 (DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0);
|
|
extern DdNode * cuddZddComplement (DdManager *dd, DdNode *node);
|
|
extern int cuddZddGetPosVarIndex(DdManager * dd, int index);
|
|
extern int cuddZddGetNegVarIndex(DdManager * dd, int index);
|
|
extern int cuddZddGetPosVarLevel(DdManager * dd, int index);
|
|
extern int cuddZddGetNegVarLevel(DdManager * dd, int index);
|
|
extern int cuddZddTreeSifting (DdManager *table, Cudd_ReorderingType method);
|
|
extern DdNode * cuddZddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I);
|
|
extern DdNode * cuddBddIsop (DdManager *dd, DdNode *L, DdNode *U);
|
|
extern DdNode * cuddMakeBddFromZddCover (DdManager *dd, DdNode *node);
|
|
extern int cuddZddLinearSifting (DdManager *table, int lower, int upper);
|
|
extern int cuddZddAlignToBdd (DdManager *table);
|
|
extern int cuddZddNextHigh (DdManager *table, int x);
|
|
extern int cuddZddNextLow (DdManager *table, int x);
|
|
extern int cuddZddUniqueCompare (int *ptr_x, int *ptr_y);
|
|
extern int cuddZddSwapInPlace (DdManager *table, int x, int y);
|
|
extern int cuddZddSwapping (DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic);
|
|
extern int cuddZddSifting (DdManager *table, int lower, int upper);
|
|
extern DdNode * cuddZddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h);
|
|
extern DdNode * cuddZddUnion (DdManager *zdd, DdNode *P, DdNode *Q);
|
|
extern DdNode * cuddZddIntersect (DdManager *zdd, DdNode *P, DdNode *Q);
|
|
extern DdNode * cuddZddDiff (DdManager *zdd, DdNode *P, DdNode *Q);
|
|
extern DdNode * cuddZddChangeAux (DdManager *zdd, DdNode *P, DdNode *zvar);
|
|
extern DdNode * cuddZddSubset1 (DdManager *dd, DdNode *P, int var);
|
|
extern DdNode * cuddZddSubset0 (DdManager *dd, DdNode *P, int var);
|
|
extern DdNode * cuddZddChange (DdManager *dd, DdNode *P, int var);
|
|
extern int cuddZddSymmCheck (DdManager *table, int x, int y);
|
|
extern int cuddZddSymmSifting (DdManager *table, int lower, int upper);
|
|
extern int cuddZddSymmSiftingConv (DdManager *table, int lower, int upper);
|
|
extern int cuddZddP (DdManager *zdd, DdNode *f);
|
|
|
|
/**AutomaticEnd***************************************************************/
|
|
|
|
#ifdef __cplusplus
|
|
} /* end of extern "C" */
|
|
#endif
|
|
|
|
#endif /* _CUDDINT */
|