立法重新划分的模拟方法。_C++_R_下载.zip

/********************************************************************* Copyright 2013 JST ERATO Minato project and other contributors http://www-erato.ist.hokudai.ac.jp/?language=en Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **********************************************************************/ /***************************************** * BDD Package (SAPPORO-1.57) - Body * * (C) Shin-ichi MINATO (June 14, 2013) * ******************************************/ #include <stdio.h> #include <stdlib.h> #include "SAPPOROBDD/bddc.h" /* ----------------- MACRO Definitions ---------------- */ /* Operation IDs in Cache */ #define BC_NULL 0 #define BC_AND 1 #define BC_XOR 2 #define BC_AT0 3 #define BC_AT1 4 #define BC_LSHIFT 5 #define BC_RSHIFT 6 #define BC_COFACTOR 7 #define BC_UNIV 8 #define BC_SUPPORT 9 #define BC_INTERSEC 10 #define BC_UNION 11 #define BC_SUBTRACT 12 #define BC_OFFSET 13 #define BC_ONSET 14 #define BC_CHANGE 15 #define BC_CARD 16 #define BC_LIT 17 #define BC_LEN 18 /* Macros for malloc, realloc */ #define B_MALLOC(type, size) \ (type *)malloc(sizeof(type) * size) #define B_REALLOC(ptr, type, size) \ (type *)realloc(ptr, sizeof(type) * size) /* Printf format of bddp */ #ifdef B_64 # define B_BDDP_FD "%lld" # define B_BDDP_FX "0x%llX" #else # define B_BDDP_FD "%d" # define B_BDDP_FX "0x%X" #endif /* strtol or strtoll */ #ifdef B_64 # define B_STRTOI strtoll #else # define B_STRTOI strtol #endif /* Table spaces */ #define B_NODE_MAX (B_VAL_MASK>>1U) /* Max number of BDD nodes */ #define B_NODE_SPC0 256 /* Default initial node size */ #define B_VAR_SPC0 16 /* Initial var table size */ #define B_HASH_SPC0 4 /* Initial hash size */ #define B_RFCT_SPC0 4 /* Initial RFCT size */ /* Negative edge manipulation */ #define B_NEG(f) ((f) & B_INV_MASK) #define B_NOT(f) ((f) ^ B_INV_MASK) #define B_ABS(f) ((f) & ~B_INV_MASK) /* Constant node manipulation */ #define B_CST(f) ((f) & B_CST_MASK) #define B_VAL(f) ((f) & B_VAL_MASK) /* Conversion of bddp and node index/pointer */ #define B_NP(f) (Node+(B_ABS(f)>>1U)) #define B_NDX(f) (B_ABS(f)>>1U) #define B_BDDP_NP(p) ((bddp)((p)-Node) << 1U) /* Read & Write of bddp field in the tables */ #ifdef B_64 # define B_LOW32(f) ((bddp_32)((f)&((1ULL<<32U)-1U))) # define B_HIGH8(f) ((bddp_h8)((f)>>32U)) # define B_SET_NXP(p, f, i) \ (p ## _h8 = f ## _h8 + i, p ## _32 = f ## _32 + i) # define B_GET_BDDP(f) \ ((bddp) f ## _32 | ((bddp) f ## _h8 << 32U)) # define B_SET_BDDP(f, g) \ (f ## _h8 = B_HIGH8(g), f ## _32 = B_LOW32(g)) # define B_CPY_BDDP(f, g) \ (f ## _h8 = g ## _h8, f ## _32 = g ## _32) #else # define B_SET_NXP(p, f, i) (p ## _32 = f ## _32 + i) # define B_GET_BDDP(f) (f ## _32) # define B_SET_BDDP(f, g) (f ## _32 = g) # define B_CPY_BDDP(f, g) (f ## _32 = g ## _32) #endif /* B_64 */ /* var & rfc manipulation */ #define B_VAR_NP(p) ((p)->varrfc & B_VAR_MASK) #define B_RFC_MASK (~B_VAR_MASK) #define B_RFC_UNIT (1U << B_VAR_WIDTH) #define B_RFC_NP(p) ((p)->varrfc >> B_VAR_WIDTH) #define B_RFC_ZERO_NP(p) ((p)->varrfc < B_RFC_UNIT) #define B_RFC_ONE_NP(p) (((p)->varrfc & B_RFC_MASK) == B_RFC_UNIT) #define B_RFC_INC_NP(p) \ (((p)->varrfc < B_RFC_MASK - B_RFC_UNIT)? \ ((p)->varrfc += B_RFC_UNIT, 0) : rfc_inc_ovf(p)) #define B_RFC_DEC_NP(p) \ (((p)->varrfc >= B_RFC_MASK)? rfc_dec_ovf(p): \ (B_RFC_ZERO_NP(p))? \ err("B_RFC_DEC_NP: rfc under flow", p-Node): \ ((p)->varrfc -= B_RFC_UNIT, 0)) /* ----------- Stack overflow limitter ------------ */ const int BDD_RecurLimit = 65536; int BDD_RecurCount = 0; #define BDD_RECUR_INC \ {if(++BDD_RecurCount >= BDD_RecurLimit) \ err("BDD_RECUR_INC: Recursion Limit", BDD_RecurCount);} #define BDD_RECUR_DEC BDD_RecurCount-- /* Conversion of ZBDD node flag */ #define B_Z_NP(p) ((p)->f0_32 & (bddp_32)B_INV_MASK) /* Hash Functions */ #define B_HASHKEY(f0, f1, hashSpc) \ (((B_CST(f0)? (f0): (f0)+2U) \ ^(B_NEG(f0)? ~((f0)>>1U): ((f0)>>1U)) \ ^(B_CST(f1)? (f1)<<1U: ((f1)+2U)<<1U) \ ^(B_NEG(f1)? ~((f1)>>1U): ((f1)>>1U)) )\ & (hashSpc-1U)) /* (((f0)^((f0)>>10)^((f0)>>31)^(f1)^((f1)>>8)^((f1)>>31)) \*/ #define B_CACHEKEY(op, f, g) \ ((((bddp)(op)<<2U) \ ^(B_CST(f)? (f): (f)+2U) \ ^(B_NEG(f)? ~((f)>>1U): ((f)>>1U)) \ ^(B_CST(g)? (g)<<3U: ((g)+2U)<<3U) \ ^(B_NEG(g)? ~((g)>>1U): ((g)>>1U)) )\ & (CacheSpc-1U)) /* ------- Declaration of static (internal) data ------- */ /* typedef of bddp field in the tables */ typedef unsigned int bddp_32; #ifdef B_64 typedef unsigned char bddp_h8; #endif /* Declaration of Node table */ struct B_NodeTable { bddp_32 f0_32; /* 0-edge */ bddp_32 f1_32; /* 1-edge */ bddp_32 nx_32; /* Node index */ unsigned int varrfc; /* VarID & Reference counter */ #ifdef B_64 bddp_h8 f0_h8; /* Extention of 0-edge */ bddp_h8 f1_h8; /* Extention of 1-edge */ bddp_h8 nx_h8; /* Extention of node index */ #endif /* B_64 */ }; static struct B_NodeTable *Node = 0; /* Node Table */ static bddp NodeLimit = 0; /* Final limit size */ static bddp NodeUsed = 0; /* Number of used node */ static bddp Avail = bddnull; /* Head of available node */ static bddp NodeSpc = 0; /* Current Node-Table size */ /* Declaration of Hash-table per Var */ struct B_VarTable { bddp hashSpc; /* Current hash-table size */ bddp hashUsed; /* Current used entries */ bddvar lev; /* Level of the variable */ bddp_32 *hash_32; /* Hash-table */ #ifdef B_64 bddp_h8 *hash_h8; /* Extension of hash-table */ #endif /* B_64 */ }; static struct B_VarTable *Var = 0; /* Var-tables */ static bddvar *VarID = 0; /* VarID reverse table */ static bddvar VarUsed = 0; /* Number of used Var */ static bddvar VarSpc = 0; /* Current Var-table size */ /* Declaration of Operation Cache */ struct B_CacheTable { bddp_32 f_32; /* an operand BDD */ bddp_32 g_32; /* an operand BDD */ bddp_32 h_32; /* Result BDD */ unsigned char op; /* Operation code */ #ifdef B_64 bddp_h8 f_h8; /* Extention of an operand BDD */ bddp_h8 g_h8; /* Extention of an operand BDD */ bddp_h8 h_h8; /* Extention of result BDD */ #endif /* B_64 */ }; static struct B_CacheTable *Cache = 0; /* Opeartion cache */ static bddp CacheSpc = 0; /* Current cache size */ /* Declaration of RFC-table */ struct B_RFC_Table { bddp_32 nx_32; /* Node index */ bddp_32 rfc_32; /* RFC */ #ifdef B_64 bddp_h8 nx_h8; /* Extension of Node index */ bddp_h8 rfc_h8; /* Extension of RFC */ #endif /* B_64 */ }; static struct B_RFC_Table *RFCT = 0; /* RFC-Table */ static bddp RFCT_Spc; /* Current RFC-table size */ static bddp RFCT_Used; /* Current RFC-table used entries */ /* ----- Declaration of static (internal) functions ------ */ /* Private procedure */ static int err B_ARG((char *msg, bddp num)); static int rfc_in