mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-12 12:26:29 +00:00
c6a14c35b0
Estimated hours taken: 5 Branches: main Upgrade to version 7.0 alpha 6 (CVS 2006-08-14) of the Boehm garbage collector. The main reason is that thread-local allocation is not supported on Solaris in version 6.x of the collector. boehm_gc/*: Merge in changes from the vendor branch. .README.in: Update Boehm GC version number and copyright notice. Mmake.common.in: configure.in: runtime/RESERVED_MACRO_NAMES: scripts/mgnuc.in: Don't define `THREAD_LOCAL_ALLOC' nor `GC_REDIRECT_TO_LOCAL' as thread-local allocation is automatically enabled in gc 7.0. Consistently use `GC_WIN32_THREADS' and `GC_LINUX_THREADS' as the non-prefixed versions of those symbols are deprecated. Don't define `NO_SIGNALS' as it is no longer necessary. Add librt to the list of thread libraries on Solaris. This is needed for the POSIX semaphore functions now used on Solaris. runtime/mercury_prof_mem.c: runtime/mercury_prof_mem.h: Update comments mentioning `NO_SIGNALS'. compiler/compile_target_code.m: Make `--inline-alloc' do nothing as inline allocation is currently broken in gc 7.0. runtime/mercury.h: runtime/mercury_heap.h: Include `gc_inline.h' instead of `gc_inl.h' as the latter no longer exists. extras/concurrency/semaphore.m: library/par_builtin.m: robdd/bryant.c: Replace instances of `GC_PTR' by `void *' as the former no longer exists. runtime/mercury_wrapper.c: Remove references to `GC_quiet' which no longer exists. Replace uses of `GC_quiet' for the MPS collector by a new variable `MR_mps_quiet'. tools/bootcheck: Copy libatomic_ops-related files and directories when copying boehm_gc.
3512 lines
115 KiB
C
3512 lines
115 KiB
C
/*
|
|
** vim: ts=4 sw=4 expandtab
|
|
*/
|
|
/*
|
|
** Copyright (C) 1995, 2001-2004 Peter Schachte and, 2006 The University of Melbourne.
|
|
** This file may only be copied under the terms of the GNU Library General
|
|
** Public License - see the file COPYING.LIB in the Mercury distribution.
|
|
*/
|
|
|
|
/*****************************************************************
|
|
File : bryant.c
|
|
Author : Peter Schachte, based on code by Tania Armstrong
|
|
Purpose : Manipulation of boolean functions
|
|
|
|
*****************************************************************/
|
|
|
|
/*****************************************************************
|
|
|
|
Controlling #defined Symbols
|
|
|
|
This code is conditionalized on a number of #defined symbols. They are:
|
|
|
|
MR_ROBDD_STATISTICS Controls collecting of computed and unique
|
|
table hash performance. If defined,
|
|
MR_ROBDD_concludeRep() prints out a bunch of
|
|
statistics.
|
|
|
|
MR_ROBDD_CLEAR_CACHES If defined, all computed and unique tables are
|
|
cleared on a call to MR_ROBDD_initRep(). This makes
|
|
running a number of tests in sequence more
|
|
fair.
|
|
|
|
MR_ROBDD_NAIVE If defined, uses very naive algorithms for
|
|
MR_ROBDD_iff_conj_array, MR_ROBDD_renameArray,
|
|
MR_ROBDD_lub, MR_ROBDD_glb, and probably some I've
|
|
forgotten.
|
|
|
|
MR_ROBDD_OLD If defined, use slightly less naive algorithms for
|
|
MR_ROBDD_restrictThresh, MR_ROBDD_restricted_glb,
|
|
MR_ROBDD_vars_entailed, and
|
|
MR_ROBDD_iff_conj_array.
|
|
|
|
MR_ROBDD_USE_THRESH Like MR_ROBDD_OLD, except that it does use the new
|
|
code for MR_ROBDD_restrictThresh. Implies
|
|
MR_ROBDD_OLD.
|
|
|
|
MR_ROBDD_USE_RGLB Like MR_ROBDD_USE_THRESH, except that it also uses
|
|
the new code for MR_ROBDD_restricted_glb. Implies
|
|
MR_ROBDD_USE_THRESH.
|
|
|
|
MR_ROBDD_NEW Like MR_ROBDD_USE_RGLB, but uses all the lastest
|
|
and greatest algorithms. Implies MR_ROBDD_USE_RGLB.
|
|
|
|
MR_ROBDD_USE_ITE_CONSTANT
|
|
Include the MR_ROBDD_ite_constant function, and'
|
|
use it to speed up the non-MR_ROBDD_NEW version of
|
|
MR_ROBDD_var_entailed (and MR_ROBDD_vars_entailed).
|
|
|
|
MR_ROBDD_SHARING Include algorithms useful in sharing analysis
|
|
performed using Boolean functions.
|
|
|
|
MR_ROBDD_RESTRICT_SET Only meaningful if MR_ROBDD_OLD &&
|
|
!MR_ROBDD_USE_THRESH. If defined, then we restrict
|
|
by making a first pass over the ROBDD finding the
|
|
set of variables present that are greater than the
|
|
threshold, and then restrict away each variable
|
|
in that set.
|
|
|
|
MR_ROBDD_WHICH Is defined to "MR_ROBDD_NAIVE", "MR_ROBDD_OLD",
|
|
"MR_ROBDD_USE_THRESH", "MR_ROBDD_USE_RGLB", or
|
|
"MR_ROBDD_NEW", depending on which of the
|
|
MR_ROBDD_NAIVE, MR_ROBDD_OLD, MR_ROBDD_USE_THRESH,
|
|
and MR_ROBDD_USE_RGLB variables are defined. This
|
|
is automatically defined by bryant.h based on the
|
|
above variables.
|
|
|
|
MR_ROBDD_VE_GLB (only when MR_ROBDD_OLD is defined) if defined,
|
|
MR_ROBDD_var_entailed(fn, v) compares the fn to
|
|
MR_ROBDD_glb(MR_ROBDD_variableRep(v), fn). The var
|
|
is entailed if they are equal. Otherwise computes
|
|
MR_ROBDD_variableRep(v) -> fn. The variable is
|
|
entailed if this is 'MR_ROBDD_one'.
|
|
|
|
MR_ROBDD_ELIM_DUPS If defined, MR_ROBDD_iff_conj_array will not assume
|
|
that the input array has no duplicates. It will
|
|
still assume that it's sorted.
|
|
|
|
MR_ROBDD_COMPUTED_TABLE Enables the computed table in MR_ROBDD_lub,
|
|
MR_ROBDD_glb, MR_ROBDD_ite, and
|
|
MR_ROBDD_restricted_glb.
|
|
|
|
MR_ROBDD_EQUAL_TEST If defined, MR_ROBDD_lub(), MR_ROBDD_glb(), and
|
|
MR_ROBDD_restricted_glb compare their arguments for
|
|
equality, and if equal return it as value.
|
|
MR_ROBDD_ite and MR_ROBDD_ite_var always do this
|
|
with their last 2 args. The equality test is pretty
|
|
cheap, and the savings will sometimes be huge, so
|
|
this should probably always be defined.
|
|
|
|
MR_ROBDD_NO_CHEAP_SHIFT If defined, shifting an integer variable number
|
|
of places is relatively expensive on this platform,
|
|
and so should be avoided. In this case we use a
|
|
table where possible to avoid shifting.
|
|
|
|
*****************************************************************/
|
|
|
|
#include "mercury_imp.h"
|
|
#include <stdio.h>
|
|
#include <stdlib.h>
|
|
#include <math.h>
|
|
#include <ctype.h>
|
|
#include <limits.h>
|
|
#include "bryant.h"
|
|
|
|
#ifdef MR_ROBDD_BRYANT_CONSERVATIVE_GC
|
|
|
|
/* Don't use pools of nodes with the conservative GC. */
|
|
#undef MR_ROBDD_POOL
|
|
|
|
/* Redefine malloc() and free() to use the GC versions */
|
|
#define malloc(n) GC_malloc(n)
|
|
#define free(p) GC_free(p)
|
|
|
|
#else /* !MR_ROBDD_BRYANT_CONSERVATIVE_GC */
|
|
|
|
#define MR_ROBDD_POOL
|
|
|
|
#endif /* MR_ROBDD_BRYANT_CONSERVATIVE_GC */
|
|
|
|
#define MR_ROBDD_REVEAL_NODE_POINTER(p) \
|
|
((MR_ROBDD_node *) MR_ROBDD_REVEAL_POINTER(p))
|
|
|
|
#define MR_ROBDD_UNUSED_MAPPING -1 /* this MUST BE -1 */
|
|
|
|
#if !defined(MR_ROBDD_max)
|
|
#define MR_ROBDD_max(a,b) ((a)<(b) ? (b) : (a))
|
|
#endif
|
|
#if !defined(MR_ROBDD_min)
|
|
#define MR_ROBDD_min(a,b) ((a)<(b) ? (a) : (b))
|
|
#endif
|
|
|
|
#define MR_ROBDD_PERCENTAGE(x,y) ((100.0 * (float)(x)) / (float)(y))
|
|
|
|
#ifdef MR_ROBDD_POOL
|
|
typedef struct pool {
|
|
MR_ROBDD_node data[MR_ROBDD_POOL_SIZE];
|
|
struct pool *prev;
|
|
} pool;
|
|
#endif /* MR_ROBDD_POOL */
|
|
|
|
#if defined(MR_ROBDD_NO_CHEAP_SHIFT) && MR_ROBDD_BITS_PER_WORD == 32
|
|
MR_ROBDD_bitmask MR_ROBDD_following_bits[MR_ROBDD_BITS_PER_WORD] =
|
|
{ 0xffffffff, 0xfffffffe, 0xfffffffc, 0xfffffff8,
|
|
0xfffffff0, 0xffffffe0, 0xffffffc0, 0xffffff80,
|
|
0xffffff00, 0xfffffe00, 0xfffffc00, 0xfffff800,
|
|
0xfffff000, 0xffffe000, 0xffffc000, 0xffff8000,
|
|
0xffff0000, 0xfffe0000, 0xfffc0000, 0xfff80000,
|
|
0xfff00000, 0xffe00000, 0xffc00000, 0xff800000,
|
|
0xff000000, 0xfe000000, 0xfc000000, 0xf8000000,
|
|
0xf0000000, 0xe0000000, 0xc0000000, 0x80000000
|
|
};
|
|
|
|
MR_ROBDD_bitmask MR_ROBDD_preceding_bits[MR_ROBDD_BITS_PER_WORD] =
|
|
{ 0x00000001, 0x00000003, 0x00000007, 0x0000000f,
|
|
0x0000001f, 0x0000003f, 0x0000007f, 0x000000ff,
|
|
0x000001ff, 0x000003ff, 0x000007ff, 0x00000fff,
|
|
0x00001fff, 0x00003fff, 0x00007fff, 0x0000ffff,
|
|
0x0001ffff, 0x0003ffff, 0x0007ffff, 0x000fffff,
|
|
0x001fffff, 0x003fffff, 0x007fffff, 0x00ffffff,
|
|
0x01ffffff, 0x03ffffff, 0x07ffffff, 0x0fffffff,
|
|
0x1fffffff, 0x3fffffff, 0x7fffffff, 0xffffffff
|
|
};
|
|
#endif
|
|
|
|
unsigned char MR_ROBDD_first_one_bit[256] =
|
|
{255, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 16 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 32 */
|
|
5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 48 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 64 */
|
|
6, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 80 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 96 */
|
|
5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 112 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 128 */
|
|
7, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 144 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 160 */
|
|
5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 176 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 192 */
|
|
6, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 208 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 224 */
|
|
5, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 240 */
|
|
4, 0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, /* 256 */
|
|
};
|
|
|
|
unsigned char MR_ROBDD_last_one_bit[256] =
|
|
{255, 0, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, /* 16 */
|
|
4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, /* 32 */
|
|
5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, /* 48 */
|
|
5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, /* 64 */
|
|
6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 80 */
|
|
6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 96 */
|
|
6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 112 */
|
|
6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, /* 128 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 144 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 160 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 176 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 192 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 208 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 224 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 240 */
|
|
7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, /* 256 */
|
|
};
|
|
|
|
/* automatically initialized to all 0 bits: */
|
|
MR_ROBDD_bitset MR_ROBDD_emptyset;
|
|
|
|
/****************************************************************
|
|
|
|
Macros to avoid #ifdefs
|
|
|
|
****************************************************************/
|
|
|
|
#if defined(MR_ROBDD_COMPUTED_TABLE) && defined(MR_ROBDD_CLEAR_CACHES)
|
|
#define MR_ROBDD_CLEAR_CACHE(op) \
|
|
MR_memset(op##_computed_cache, 0, sizeof(op##_computed_cache))
|
|
#else /* !MR_ROBDD_CLEAR_CACHES || !MR_ROBDD_COMPUTED_TABLE */
|
|
#define MR_ROBDD_CLEAR_CACHE(op)
|
|
#endif
|
|
|
|
#if defined(MR_ROBDD_STATISTICS)
|
|
|
|
/* The largest bucket size to be separately counted. Larger buckets
|
|
* will be listed as "> MR_ROBDD_MAX_COUNT."
|
|
*/
|
|
#define MR_ROBDD_MAX_COUNT 1000
|
|
|
|
int MR_ROBDD_unique_table_hits, MR_ROBDD_unique_table_misses;
|
|
|
|
#define MR_ROBDD_DECLARE_FN_COUNT(op) int op##_count;
|
|
|
|
#define MR_ROBDD_COUNT_FN(fn) (++fn##_count)
|
|
|
|
#define MR_ROBDD_INIT_FN_COUNT(fn) fn##_count = 0
|
|
#define MR_ROBDD_PRINT_FN_COUNT(fn) \
|
|
if (fn##_count!=0) printf("%6d calls to " #fn "\n", fn##_count);
|
|
|
|
#define MR_ROBDD_COUNT_UNIQUE_HIT (++MR_ROBDD_unique_table_hits)
|
|
#define MR_ROBDD_COUNT_UNIQUE_MISS (++MR_ROBDD_unique_table_misses)
|
|
|
|
#if defined(MR_ROBDD_COMPUTED_TABLE)
|
|
|
|
#define MR_ROBDD_COUNT_HIT(op) (++op##_computed_hits)
|
|
#define MR_ROBDD_COUNT_MISS(op) (++op##_computed_misses, ++cache->count)
|
|
#define MR_ROBDD_INIT_CACHE(op) \
|
|
do { \
|
|
op##_computed_misses = 0; \
|
|
op##_computed_hits = 0; \
|
|
MR_ROBDD_CLEAR_CACHE(op); \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_CACHE_COUNT_MEMBER int count;
|
|
#define MR_ROBDD_PRINT_CACHE_PERFORMANCE(op) \
|
|
do { \
|
|
if (op##_computed_misses > 0 ) { \
|
|
int i, size_count[MR_ROBDD_MAX_COUNT+2]; \
|
|
printf( \
|
|
#op " computed table: %d hits, %d misses, %.2f%% hit rate\n",\
|
|
op##_computed_hits, op##_computed_misses, \
|
|
MR_ROBDD_PERCENTAGE(op##_computed_hits, \
|
|
op##_computed_hits + op##_computed_misses)); \
|
|
MR_memset(size_count, 0, sizeof(size_count)); \
|
|
for (i=0; i<MR_ROBDD_COMPUTED_TABLE_SIZE; ++i) { \
|
|
int count = op##_computed_cache[i].count; \
|
|
++size_count[(count<=MR_ROBDD_MAX_COUNT ? count : \
|
|
MR_ROBDD_MAX_COUNT+1)]; \
|
|
} \
|
|
MR_ROBDD_print_distribution(size_count, MR_ROBDD_MAX_COUNT); \
|
|
} \
|
|
} while (0)
|
|
|
|
#else /* !MR_ROBDD_COMPUTED_TABLE */
|
|
|
|
#define MR_ROBDD_PRINT_CACHE_PERFORMANCE(op)
|
|
|
|
#endif /* MR_ROBDD_COMPUTED_TABLE */
|
|
#else /* ! MR_ROBDD_STATISTICS */
|
|
|
|
#define MR_ROBDD_DECLARE_FN_COUNT(op)
|
|
#define MR_ROBDD_COUNT_FN(fn)
|
|
#define MR_ROBDD_INIT_FN_COUNT(fn)
|
|
#define MR_ROBDD_PRINT_FN_COUNT(fn)
|
|
#define MR_ROBDD_COUNT_UNIQUE_HIT
|
|
#define MR_ROBDD_COUNT_UNIQUE_MISS
|
|
#define MR_ROBDD_INIT_CACHE(op) MR_ROBDD_CLEAR_CACHE(op)
|
|
#define MR_ROBDD_PRINT_CACHE_PERFORMANCE(op)
|
|
|
|
#if defined(MR_ROBDD_COMPUTED_TABLE)
|
|
#define MR_ROBDD_COUNT_HIT(fn)
|
|
#define MR_ROBDD_COUNT_MISS(fn)
|
|
#define MR_ROBDD_CACHE_COUNT_MEMBER
|
|
#endif /* MR_ROBDD_COMPUTED_TABLE */
|
|
|
|
#endif /* MR_ROBDD_STATISTICS */
|
|
|
|
#if defined(MR_ROBDD_EQUAL_TEST)
|
|
#define MR_ROBDD_DIRECT_EQUAL_TEST(f,g,result) \
|
|
if ((f) == (g)) return (result)
|
|
#define MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,result) \
|
|
else MR_ROBDD_DIRECT_EQUAL_TEST(f,g,result);
|
|
#else /* ! MR_ROBDD_EQUAL_TEST */
|
|
#define MR_ROBDD_DIRECT_EQUAL_TEST(f,g,result)
|
|
#define MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,result)
|
|
#endif
|
|
|
|
#if defined(MR_ROBDD_CLEAR_CACHES)
|
|
#if defined(MR_ROBDD_POOL)
|
|
#define MR_ROBDD_INIT_UNIQUE_TABLE \
|
|
do { \
|
|
MR_memset(MR_ROBDD_unique_table, (char) 0, \
|
|
sizeof(MR_ROBDD_unique_table)); \
|
|
while (MR_ROBDD_curr_pool!=NULL) { \
|
|
pool *p = MR_ROBDD_curr_pool->prev; \
|
|
free(MR_ROBDD_curr_pool); \
|
|
MR_ROBDD_curr_pool = p; \
|
|
} \
|
|
MR_ROBDD_curr_pool_ptr = MR_ROBDD_curr_pool_end_ptr = NULL; \
|
|
MR_ROBDD_node_count = 0; \
|
|
} while (0)
|
|
|
|
#else /* !MR_ROBDD_POOL */
|
|
#define MR_ROBDD_INIT_UNIQUE_TABLE \
|
|
MR_memset(MR_ROBDD_unique_table, (char) 0, sizeof(MR_ROBDD_unique_table));
|
|
#endif /* MR_ROBDD_POOL */
|
|
#else /* !MR_ROBDD_CLEAR_CACHES */
|
|
#define MR_ROBDD_INIT_UNIQUE_TABLE
|
|
#endif /* MR_ROBDD_CLEAR_CACHES */
|
|
|
|
/********************************************************************
|
|
|
|
Caching of computed values
|
|
|
|
For improved efficiency, if MR_ROBDD_COMPUTED_TABLE is defined we maintain a
|
|
cache of previously computed values to certain functions, and use
|
|
this to avoid costly computations when possible. This is
|
|
particularly important for ROBDDs, because the high degree of fan-in
|
|
causes frequent repeated computations.
|
|
|
|
Because caching is in many ways extraneous to the functions being
|
|
cached, we put the caching code here as macros, so that the
|
|
presentation of the algorithms is minimally impacted by caching.
|
|
|
|
********************************************************************/
|
|
|
|
#if defined(MR_ROBDD_COMPUTED_TABLE)
|
|
|
|
#if defined(MR_ROBDD_STATISTICS)
|
|
#define MR_ROBDD_DECLARE_CACHE(op,MR_ROBDD_type) \
|
|
static int op##_computed_hits; \
|
|
static int op##_computed_misses; \
|
|
static MR_ROBDD_type op##_computed_cache[MR_ROBDD_COMPUTED_TABLE_SIZE]
|
|
#else /* !MR_ROBDD_STATISTICS */
|
|
#define MR_ROBDD_DECLARE_CACHE(op,MR_ROBDD_type) \
|
|
static MR_ROBDD_type op##_computed_cache[MR_ROBDD_COMPUTED_TABLE_SIZE]
|
|
#endif /* MR_ROBDD_STATISTICS */
|
|
|
|
/********************* the cache for MR_ROBDD_ite **************************/
|
|
|
|
#define MR_ROBDD_TERNARY_NODE_HASH(f,g,h) \
|
|
(((MR_ROBDD_INTCAST(f)>>4)+MR_ROBDD_INTCAST(g)+(MR_ROBDD_INTCAST(h)<<1)) \
|
|
% MR_ROBDD_COMPUTED_TABLE_SIZE)
|
|
|
|
typedef struct {
|
|
MR_ROBDD_node *f;
|
|
MR_ROBDD_node *g;
|
|
MR_ROBDD_node *h;
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} ite_cache_entry;
|
|
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_ite, ite_cache_entry);
|
|
#if defined(MR_ROBDD_USE_ITE_CONSTANT)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_ite_constant, ite_cache_entry);
|
|
#endif /* MR_ROBDD_USE_ITE_CONSTANT */
|
|
|
|
#define MR_ROBDD_DECLARE_ITE_CACHE_ENTRY ite_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_TRY_ITE_CACHE(n1,n2,n3,op) \
|
|
do { \
|
|
cache = &op##_computed_cache[MR_ROBDD_TERNARY_NODE_HASH(n1,n2,n3)]; \
|
|
if (cache->f==n1 && cache->g==n2 && cache->h==n3) { \
|
|
MR_ROBDD_COUNT_HIT(op); \
|
|
return cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_UPDATE_ITE_CACHE(n1,n2,n3,MR_ROBDD_node,op) \
|
|
do { \
|
|
cache->f = n1; \
|
|
cache->g = n2; \
|
|
cache->h = n3; \
|
|
cache->result = MR_ROBDD_node; \
|
|
MR_ROBDD_COUNT_MISS(op); \
|
|
} while (0)
|
|
|
|
/******************** the cache for unary operations ************/
|
|
|
|
#define MR_ROBDD_UNARY_NODE_HASH(a) \
|
|
(MR_ROBDD_INTCAST(a) % MR_ROBDD_COMPUTED_TABLE_SIZE)
|
|
|
|
typedef struct {
|
|
MR_ROBDD_node *f;
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} unary_cache_entry;
|
|
|
|
#if defined(MR_ROBDD_SHARING)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_upclose, unary_cache_entry);
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete_one, unary_cache_entry);
|
|
#endif /* MR_ROBDD_NEW */
|
|
#endif /* MR_ROBDD_SHARING */
|
|
|
|
#define MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY unary_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_UPDATE_UNARY_CACHE(n,MR_ROBDD_node,op) \
|
|
do { \
|
|
cache->f = n; \
|
|
cache->result = MR_ROBDD_node; \
|
|
MR_ROBDD_COUNT_MISS(op); \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_TRY_UNARY_CACHE(n,op) \
|
|
do { \
|
|
cache = &((op##_computed_cache)[MR_ROBDD_UNARY_NODE_HASH(n)]); \
|
|
if (cache->f==(n)) { \
|
|
MR_ROBDD_COUNT_HIT(op); \
|
|
return cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
/******************** the cache for MR_ROBDD_var_entailed ************/
|
|
|
|
#define MR_ROBDD_VAR_ENTAILED_HASH(a,n) \
|
|
((MR_ROBDD_INTCAST(a)+n) % MR_ROBDD_COMPUTED_TABLE_SIZE)
|
|
|
|
typedef struct {
|
|
MR_ROBDD_node *f;
|
|
int n;
|
|
int result;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} var_entailed_cache_entry;
|
|
|
|
#if defined(MR_ROBDD_USE_RGLB)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_var_entailed, var_entailed_cache_entry);
|
|
#endif /* MR_ROBDD_USE_RGLB */
|
|
|
|
#define MR_ROBDD_DECLARE_VAR_ENTAILED_CACHE_ENTRY \
|
|
var_entailed_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_UPDATE_VAR_ENTAILED_CACHE(MR_ROBDD_node,var,val) \
|
|
do { \
|
|
cache->f = MR_ROBDD_node; \
|
|
cache->n = var; \
|
|
cache->result = val; \
|
|
MR_ROBDD_COUNT_MISS(MR_ROBDD_var_entailed); \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_TRY_VAR_ENTAILED_CACHE(MR_ROBDD_node,var) \
|
|
do { \
|
|
cache = &((MR_ROBDD_var_entailed_computed_cache) \
|
|
[MR_ROBDD_VAR_ENTAILED_HASH(MR_ROBDD_node,var)]); \
|
|
if (cache->f==(MR_ROBDD_node) && cache->n==(var)) { \
|
|
MR_ROBDD_COUNT_HIT(op); \
|
|
return cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
/**************** the cache for unary set-valued operations ********/
|
|
|
|
typedef struct {
|
|
MR_ROBDD_node *f;
|
|
MR_ROBDD_bitset result;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} unary_bitset_cache_entry;
|
|
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_vars_entailed, unary_bitset_cache_entry);
|
|
#endif
|
|
|
|
#define MR_ROBDD_DECLARE_UNARY_BITSET_CACHE_ENTRY \
|
|
unary_bitset_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(n,set,op) \
|
|
do { \
|
|
cache->f = n; \
|
|
cache->result = set; \
|
|
MR_ROBDD_COUNT_MISS(op); \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_TRY_UNARY_BITSET_CACHE(n,op) \
|
|
do { \
|
|
cache = &((op##_computed_cache)[MR_ROBDD_UNARY_NODE_HASH(n)]); \
|
|
if (cache->f==(n)) { \
|
|
MR_ROBDD_COUNT_HIT(op); \
|
|
return &cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
/******************** the cache for symmetric binary operations ************/
|
|
|
|
/*
|
|
** NB: Since MR_ROBDD_glb and MR_ROBDD_lub are commutative, cache entries
|
|
** will work both ways round, so we want a symmetrical cache, ie, (a,b) should
|
|
** hash to the same value as (b,a). We achieve this by first exchanging
|
|
** a and b if a > b (comparing their addresses) in MR_ROBDD_TRY_BIN_CACHE.
|
|
** We assume that they won't be changed (or exchanged) before
|
|
** MR_ROBDD_UPDATE_BIN_CACHE is called.
|
|
*/
|
|
|
|
#define MR_ROBDD_BINARY_NODE_HASH(a,b) \
|
|
((MR_ROBDD_INTCAST(a)+(MR_ROBDD_INTCAST(b)<<1)) % MR_ROBDD_COMPUTED_TABLE_SIZE)
|
|
|
|
typedef struct {
|
|
MR_ROBDD_node *f;
|
|
MR_ROBDD_node *g;
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} bin_cache_entry;
|
|
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_glb, bin_cache_entry);
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_lub, bin_cache_entry);
|
|
#if defined(MR_ROBDD_SHARING)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_bin, bin_cache_entry);
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete, bin_cache_entry);
|
|
#endif
|
|
|
|
#define MR_ROBDD_DECLARE_BIN_CACHE_ENTRY bin_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_UPDATE_BIN_CACHE(n1,n2,MR_ROBDD_node,op) \
|
|
do { \
|
|
cache->f = n1; \
|
|
cache->g = n2; \
|
|
cache->result = MR_ROBDD_node; \
|
|
MR_ROBDD_COUNT_MISS(op); \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_TRY_BIN_CACHE(n1,n2,op) \
|
|
do { \
|
|
if (n2 < n1) { \
|
|
MR_ROBDD_node *temp = (n2); \
|
|
(n2) = (n1); \
|
|
(n1) = temp; \
|
|
} \
|
|
cache = &((op##_computed_cache)[MR_ROBDD_BINARY_NODE_HASH(n1,n2)]); \
|
|
if (cache->f==(n1) && cache->g==(n2)) { \
|
|
MR_ROBDD_COUNT_HIT(op); \
|
|
return cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
/******************** the cache for asymmetric binary operations ************/
|
|
|
|
#if defined(MR_ROBDD_SHARING) && defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete_one_or, bin_cache_entry);
|
|
#endif /* MR_ROBDD_SHARING && MR_ROBDD_NEW */
|
|
|
|
#if defined(MR_ROBDD_USE_THRESH)
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_restrictThresh, bin_cache_entry);
|
|
#endif /* MR_ROBDD_USE_THRESH */
|
|
|
|
#if (defined(MR_ROBDD_SHARING) && defined(MR_ROBDD_NEW)) || defined(MR_ROBDD_USE_THRESH)
|
|
|
|
#define MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY bin_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_UPDATE_ASYM_BIN_CACHE(n1,n2,MR_ROBDD_node,op) \
|
|
MR_ROBDD_UPDATE_BIN_CACHE(n1,n2,MR_ROBDD_node,op)
|
|
|
|
#define MR_ROBDD_TRY_ASYM_BIN_CACHE(n1,n2,op) \
|
|
do { \
|
|
cache = &((op##_computed_cache)[MR_ROBDD_BINARY_NODE_HASH(n1,n2)]); \
|
|
if (cache->f==(n1) && cache->g==(n2)) { \
|
|
MR_ROBDD_COUNT_HIT(op); \
|
|
return cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
#endif /* (MR_ROBDD_SHARING && MR_ROBDD_NEW) || MR_ROBDD_USE_THRESH */
|
|
|
|
/**************************** the cache for rglb ***********************/
|
|
|
|
#if defined(MR_ROBDD_USE_RGLB)
|
|
|
|
typedef struct {
|
|
MR_ROBDD_node *f;
|
|
MR_ROBDD_node *g;
|
|
MR_ROBDD_node *result;
|
|
int thresh;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} rglb_cache_entry;
|
|
|
|
MR_ROBDD_DECLARE_CACHE(rglb, rglb_cache_entry);
|
|
|
|
#define MR_ROBDD_DECLARE_RGLB_CACHE_ENTRY rglb_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_TRY_RGLB_CACHE(n1,n2,th) \
|
|
do { \
|
|
if (n2 < n1) { \
|
|
MR_ROBDD_node *temp = (n2); \
|
|
(n2) = (n1); \
|
|
(n1) = temp; \
|
|
} \
|
|
cache = &rglb_computed_cache[MR_ROBDD_BINARY_NODE_HASH(n1,n2)]; \
|
|
if (cache->f==(n1) && cache->g==(n2) && \
|
|
cache->thresh >= th) { \
|
|
MR_ROBDD_COUNT_HIT(rglb); \
|
|
if (cache->thresh == th) return cache->result; \
|
|
return MR_ROBDD_restrictThresh(th, cache->result); \
|
|
} \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_UPDATE_RGLB_CACHE(n1,n2,th,MR_ROBDD_node) \
|
|
do { \
|
|
cache->f = n1; \
|
|
cache->g = n2; \
|
|
cache->thresh = th; \
|
|
cache->result = MR_ROBDD_node; \
|
|
MR_ROBDD_COUNT_MISS(rglb); \
|
|
} while (0)
|
|
|
|
#endif /* MR_ROBDD_USE_RGLB */
|
|
|
|
/************************ the cache for MR_ROBDD_complete_or *******************/
|
|
|
|
#if defined(MR_ROBDD_SHARING) && defined(MR_ROBDD_NEW)
|
|
typedef struct {
|
|
MR_ROBDD_node *f;
|
|
MR_ROBDD_node *g;
|
|
MR_ROBDD_node *prev;
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} complete_or_cache_entry;
|
|
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_complete_or, complete_or_cache_entry);
|
|
|
|
#define MR_ROBDD_DECLARE_COMPLETE_OR_CACHE_ENTRY \
|
|
complete_or_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_TRY_COMPLETE_OR_CACHE(n1,n2,pr) \
|
|
do { \
|
|
if (n2 < n1) { \
|
|
MR_ROBDD_node *temp = (n2); \
|
|
(n2) = (n1); \
|
|
(n1) = temp; \
|
|
} \
|
|
cache = &complete_or_computed_cache \
|
|
[MR_ROBDD_TERNARY_NODE_HASH(n1,n2,pr)]; \
|
|
if ((cache->f==n1 && cache->g==n2 && cache->prev==pr)) { \
|
|
MR_ROBDD_COUNT_HIT(MR_ROBDD_complete_or); \
|
|
return cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,MR_ROBDD_node) \
|
|
do { \
|
|
cache->f = n1; \
|
|
cache->g = n2; \
|
|
cache->prev = pr; \
|
|
cache->result = MR_ROBDD_node; \
|
|
MR_ROBDD_COUNT_MISS(MR_ROBDD_complete_or); \
|
|
} while (0)
|
|
|
|
#endif /* MR_ROBDD_SHARING && MR_ROBDD_NEW */
|
|
|
|
/********************* the cache for MR_ROBDD_ite_var ***********************/
|
|
|
|
#if defined(MR_ROBDD_NEW)
|
|
|
|
#define MR_ROBDD_ITE_VAR_COMPUTED_HASH(f,g,h) \
|
|
((f+MR_ROBDD_INTCAST(g)+(MR_ROBDD_INTCAST(h)<<1)) \
|
|
% MR_ROBDD_COMPUTED_TABLE_SIZE)
|
|
|
|
typedef struct {
|
|
int f;
|
|
MR_ROBDD_node *g;
|
|
MR_ROBDD_node *h;
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_CACHE_COUNT_MEMBER
|
|
} ite_var_cache_entry;
|
|
|
|
MR_ROBDD_DECLARE_CACHE(MR_ROBDD_ite_var, ite_var_cache_entry);
|
|
|
|
#define MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY ite_var_cache_entry *cache;
|
|
|
|
#define MR_ROBDD_TRY_ITE_VAR_CACHE(n1,n2,h) \
|
|
do { \
|
|
cache = &MR_ROBDD_ite_var_computed_cache[ \
|
|
MR_ROBDD_ITE_VAR_COMPUTED_HASH(n1,n2,h)]; \
|
|
if (cache->f==n1 && cache->g==n2 && cache->h==h) { \
|
|
MR_ROBDD_COUNT_HIT(MR_ROBDD_ite_var); \
|
|
return cache->result; \
|
|
} \
|
|
} while (0)
|
|
|
|
#define MR_ROBDD_UPDATE_ITE_VAR_CACHE(n1,n2,h,MR_ROBDD_node) \
|
|
do { \
|
|
cache->f = n1; \
|
|
cache->g = n2; \
|
|
cache->h = h; \
|
|
cache->result = MR_ROBDD_node; \
|
|
MR_ROBDD_COUNT_MISS(MR_ROBDD_ite_var); \
|
|
} while (0)
|
|
|
|
#endif /* MR_ROBDD_NEW */
|
|
|
|
#else /* !MR_ROBDD_COMPUTED_TABLE */
|
|
|
|
/**************************** no caching at all **************************/
|
|
|
|
#define MR_ROBDD_DECLARE_ITE_CACHE_ENTRY
|
|
#define MR_ROBDD_TRY_ITE_CACHE(n1,n2,n3,op)
|
|
#define MR_ROBDD_UPDATE_ITE_CACHE(n1,n2,n3,MR_ROBDD_node,op)
|
|
|
|
#define MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY
|
|
#define MR_ROBDD_UPDATE_UNARY_CACHE(n,MR_ROBDD_node,op)
|
|
#define MR_ROBDD_TRY_UNARY_CACHE(n,op)
|
|
|
|
#define MR_ROBDD_DECLARE_VAR_ENTAILED_CACHE_ENTRY
|
|
#define MR_ROBDD_UPDATE_VAR_ENTAILED_CACHE(MR_ROBDD_node,var,val)
|
|
#define MR_ROBDD_TRY_VAR_ENTAILED_CACHE(MR_ROBDD_node,var)
|
|
|
|
#define MR_ROBDD_DECLARE_UNARY_BITSET_CACHE_ENTRY
|
|
#define MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(n,set,op)
|
|
#define MR_ROBDD_TRY_UNARY_BITSET_CACHE(n,op)
|
|
|
|
#define MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
|
|
#define MR_ROBDD_TRY_BIN_CACHE(n1,n2,op)
|
|
#define MR_ROBDD_UPDATE_BIN_CACHE(n1,n2,MR_ROBDD_node,op)
|
|
|
|
#define MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY
|
|
#define MR_ROBDD_UPDATE_ASYM_BIN_CACHE(n1,n2,MR_ROBDD_node,op)
|
|
#define MR_ROBDD_TRY_ASYM_BIN_CACHE(n1,n2,op)
|
|
|
|
#define MR_ROBDD_DECLARE_RGLB_CACHE_ENTRY
|
|
#define MR_ROBDD_TRY_RGLB_CACHE(n1,n2,th)
|
|
#define MR_ROBDD_UPDATE_RGLB_CACHE(n1,n2,th,MR_ROBDD_node)
|
|
|
|
#define MR_ROBDD_DECLARE_COMPLETE_OR_CACHE_ENTRY
|
|
#define MR_ROBDD_TRY_COMPLETE_OR_CACHE(n1,n2,pr)
|
|
#define MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(n1,n2,pr,MR_ROBDD_node)
|
|
|
|
#define MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
|
|
#define MR_ROBDD_TRY_ITE_VAR_CACHE(n1,n2,h)
|
|
#define MR_ROBDD_UPDATE_ITE_VAR_CACHE(n1,n2,h,MR_ROBDD_node)
|
|
|
|
#undef MR_ROBDD_COMPUTED_TABLE_SIZE
|
|
#define MR_ROBDD_COMPUTED_TABLE_SIZE 0
|
|
|
|
#endif /* MR_ROBDD_COMPUTED_TABLE */
|
|
|
|
/****************************************************************
|
|
|
|
The Unique Table
|
|
|
|
****************************************************************/
|
|
|
|
static MR_ROBDD_BRYANT_hidden_node_pointer
|
|
MR_ROBDD_unique_table[MR_ROBDD_UNIQUE_TABLE_SIZE];
|
|
|
|
#define MR_ROBDD_UNIQUE_HASH(var,tr,fa) \
|
|
(((var)+MR_ROBDD_INTCAST(tr)+(MR_ROBDD_INTCAST(fa)<<1)) \
|
|
% MR_ROBDD_UNIQUE_TABLE_SIZE)
|
|
|
|
/****************************************************************
|
|
|
|
Prototypes
|
|
|
|
****************************************************************/
|
|
|
|
extern void MR_ROBDD_printBryant(MR_ROBDD_node *a);
|
|
|
|
/* if then else algorithm */
|
|
MR_ROBDD_node *MR_ROBDD_ite(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h);
|
|
MR_ROBDD_node *MR_ROBDD_restricted_iff_conj_array(int v0, int n, int arr[],
|
|
int thresh);
|
|
|
|
MR_ROBDD_node *MR_ROBDD_renameArray(MR_ROBDD_node *in, int count,
|
|
int mappping[]);
|
|
MR_ROBDD_node *MR_ROBDD_reverseRenameArray(MR_ROBDD_node *in, int count,
|
|
int rev_mappping[]);
|
|
|
|
MR_ROBDD_node *MR_ROBDD_complete(MR_ROBDD_node *f, MR_ROBDD_node *g);
|
|
MR_ROBDD_node *MR_ROBDD_bin_univ(MR_ROBDD_node *f);
|
|
|
|
static int MR_ROBDD_intcompare(const void *i, const void *j);
|
|
|
|
/****************************************************************
|
|
|
|
Inline Bit Set Stuff
|
|
|
|
****************************************************************/
|
|
|
|
/*
|
|
** MR_ROBDD_next_element()
|
|
** finds the next element in set beginning with var,
|
|
** and updates var, word, and mask to refer to it.
|
|
** MR_ROBDD_prev_element()
|
|
** finds the next earlier element in set.
|
|
** MR_ROBDD_next_nonelement()
|
|
** finds the next potential element of set that is in fact not an element
|
|
** of set.
|
|
** MR_ROBDD_prev_nonelement()
|
|
** finds the next earlier non-element of set.
|
|
**
|
|
** NB: if the initally supplied element is a member of the set,
|
|
** MR_ROBDD_next_element and MR_ROBDD_prev_element will happily return
|
|
** that MR_ROBDD_one. Similarly, MR_ROBDD_next_nonelement and
|
|
** MR_ROBDD_prev_nonelement will happily return the initial input if it
|
|
** fits the bill. That is, these find the next or next earlier element
|
|
** INLCUDING THE INITIAL ONE that meets the criterion.
|
|
*/
|
|
|
|
#if defined(MR_ROBDD_NO_CHEAP_SHIFT)
|
|
|
|
__inline int
|
|
MR_ROBDD_next_element(MR_ROBDD_bitset *set, int *var, int *word,
|
|
MR_ROBDD_bitmask *mask)
|
|
{
|
|
int vr = *var;
|
|
int wd = *word;
|
|
MR_ROBDD_bitmask f = MR_ROBDD_FOLLOWING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
|
|
MR_ROBDD_bitmask bits = *ptr;
|
|
MR_ROBDD_bitmask msk = *mask;
|
|
|
|
assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
|
|
|
|
if ((bits&f) == 0) {
|
|
do {
|
|
if (++wd > ((MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD)) return MR_FALSE;
|
|
} while ((bits=*++ptr) == 0);
|
|
vr = wd<<MR_ROBDD_LOG_BITS_PER_WORD;
|
|
msk = 1;
|
|
}
|
|
/* I know there's a later bit set in bits, so this is safe */
|
|
while ((bits&msk) == 0) {
|
|
++vr;
|
|
msk <<= 1;
|
|
assert(vr < (wd+1)<<MR_ROBDD_LOG_BITS_PER_WORD);
|
|
}
|
|
*var = vr;
|
|
*word = wd;
|
|
*mask = msk;
|
|
return MR_TRUE;
|
|
}
|
|
|
|
#else /* !MR_ROBDD_NO_CHEAP_SHIFT */
|
|
|
|
__inline int
|
|
MR_ROBDD_next_element(MR_ROBDD_bitset *set, int *var, int *word,
|
|
MR_ROBDD_bitmask *mask)
|
|
{
|
|
int vr = *var;
|
|
int wd = *word;
|
|
MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
|
|
MR_ROBDD_bitmask bits = *ptr&MR_ROBDD_FOLLOWING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
|
|
assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
|
|
|
|
while (bits == 0) {
|
|
if (++wd > (MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD) return MR_FALSE;
|
|
bits = *++ptr;
|
|
}
|
|
vr = wd<<MR_ROBDD_LOG_BITS_PER_WORD;
|
|
/* I know there's a later bit set in bits, so this is safe */
|
|
while ((bits & MR_ROBDD_CHAR_MASK) == 0) {
|
|
bits >>= MR_ROBDD_BITS_PER_CHAR;
|
|
vr += MR_ROBDD_BITS_PER_CHAR;
|
|
assert(vr < (wd+1)<<MR_ROBDD_LOG_BITS_PER_WORD);
|
|
}
|
|
vr += MR_ROBDD_first_one_bit[bits & MR_ROBDD_CHAR_MASK];
|
|
|
|
*var = vr;
|
|
*word = wd;
|
|
*mask = 1<<(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
return MR_TRUE;
|
|
}
|
|
|
|
#endif /* MR_ROBDD_NO_CHEAP_SHIFT */
|
|
|
|
#if defined(MR_ROBDD_NO_CHEAP_SHIFT)
|
|
|
|
__inline int
|
|
MR_ROBDD_prev_element(MR_ROBDD_bitset *set, int *var, int *word,
|
|
MR_ROBDD_bitmask *mask)
|
|
{
|
|
int vr = *var;
|
|
int wd = *word;
|
|
|
|
assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
|
|
|
|
MR_ROBDD_bitmask f = MR_ROBDD_PRECEDING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
|
|
MR_ROBDD_bitmask bits = *ptr;
|
|
MR_ROBDD_bitmask msk = *mask;
|
|
|
|
if ((bits&f) == 0) {
|
|
do {
|
|
if (--wd < 0) {
|
|
return MR_FALSE;
|
|
}
|
|
} while ((bits=*--ptr) == 0);
|
|
vr = (wd<<MR_ROBDD_LOG_BITS_PER_WORD) + MR_ROBDD_BITS_PER_WORD-1;
|
|
msk = 1<<(MR_ROBDD_BITS_PER_WORD-1);
|
|
}
|
|
/* I know there's an earlier bit set in bits, so this is safe */
|
|
while ((bits&msk) == 0) {
|
|
--vr;
|
|
msk >>= 1;
|
|
assert(vr >= 0);
|
|
}
|
|
*var = vr;
|
|
*word = wd;
|
|
*mask = msk;
|
|
return MR_TRUE;
|
|
}
|
|
|
|
#else /* !MR_ROBDD_NO_CHEAP_SHIFT */
|
|
|
|
__inline int
|
|
MR_ROBDD_prev_element(MR_ROBDD_bitset *set, int *var, int *word,
|
|
MR_ROBDD_bitmask *mask)
|
|
{
|
|
int vr = *var;
|
|
int wd = *word;
|
|
MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
|
|
MR_ROBDD_bitmask bits = *ptr&MR_ROBDD_PRECEDING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
MR_ROBDD_bitmask temp;
|
|
|
|
assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
|
|
|
|
while (bits == 0) {
|
|
if (--wd < 0) {
|
|
return MR_FALSE;
|
|
}
|
|
bits = *--ptr;
|
|
}
|
|
|
|
vr = MR_ROBDD_BITS_PER_WORD - MR_ROBDD_BITS_PER_CHAR;
|
|
/* I know there's an earlier bit set in bits, so this is safe */
|
|
while ((temp=((bits>>vr)&MR_ROBDD_CHAR_MASK)) == 0) {
|
|
vr -= MR_ROBDD_BITS_PER_CHAR;
|
|
assert(vr >= 0);
|
|
}
|
|
vr += (int)MR_ROBDD_last_one_bit[(int)temp];
|
|
vr += (int)wd<<MR_ROBDD_LOG_BITS_PER_WORD;
|
|
|
|
*var = vr;
|
|
*word = wd;
|
|
*mask = 1<<(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
return MR_TRUE;
|
|
}
|
|
|
|
#endif /* MR_ROBDD_NO_CHEAP_SHIFT */
|
|
|
|
__inline int
|
|
MR_ROBDD_next_nonelement(MR_ROBDD_bitset *set, int *var, int *word,
|
|
MR_ROBDD_bitmask *mask)
|
|
{
|
|
int vr = *var;
|
|
int wd = *word;
|
|
MR_ROBDD_bitmask f = MR_ROBDD_FOLLOWING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
|
|
MR_ROBDD_bitmask bits = *ptr;
|
|
MR_ROBDD_bitmask msk = *mask;
|
|
|
|
assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
|
|
|
|
if ((bits&f) == f) {
|
|
do {
|
|
if (++wd >= MR_ROBDD_MAXVAR/MR_ROBDD_BITS_PER_WORD) {
|
|
return MR_FALSE;
|
|
}
|
|
} while ((bits=*++ptr) == ~0);
|
|
vr = wd<<MR_ROBDD_LOG_BITS_PER_WORD;
|
|
msk = 1;
|
|
}
|
|
/* I know there's a later bit clear in bits, so this is safe */
|
|
while ((bits&msk) != 0) {
|
|
++vr;
|
|
msk <<= 1;
|
|
}
|
|
*var = vr;
|
|
*word = wd;
|
|
*mask = msk;
|
|
return MR_TRUE;
|
|
}
|
|
|
|
__inline int
|
|
MR_ROBDD_prev_nonelement(MR_ROBDD_bitset *set, int *var, int *word,
|
|
MR_ROBDD_bitmask *mask)
|
|
{
|
|
int vr = *var;
|
|
int wd = *word;
|
|
MR_ROBDD_bitmask f = MR_ROBDD_PRECEDING_BITS(vr&(MR_ROBDD_BITS_PER_WORD-1));
|
|
MR_ROBDD_bitmask *ptr = &(set->bits[wd]);
|
|
MR_ROBDD_bitmask bits = *ptr;
|
|
MR_ROBDD_bitmask msk = *mask;
|
|
|
|
assert(vr >= 0 && vr < MR_ROBDD_MAXVAR);
|
|
|
|
if ((bits&f) == f) {
|
|
do {
|
|
if (--wd < 0) {
|
|
return MR_FALSE;
|
|
}
|
|
} while ((bits=*--ptr) == ~0);
|
|
vr = (wd<<MR_ROBDD_LOG_BITS_PER_WORD) + MR_ROBDD_BITS_PER_WORD-1;
|
|
msk = 1<<(MR_ROBDD_BITS_PER_WORD-1);
|
|
}
|
|
/* I know there's an earlier bit clear in bits, so this is safe */
|
|
while ((bits&msk) != 0) {
|
|
--vr;
|
|
msk >>= 1;
|
|
}
|
|
*var = vr;
|
|
*word = wd;
|
|
*mask = msk;
|
|
return MR_TRUE;
|
|
}
|
|
|
|
/* returns 1 if set1 is identical to set2 */
|
|
__inline int
|
|
MR_ROBDD_bitset_equal(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2);
|
|
|
|
__inline int
|
|
MR_ROBDD_bitset_equal(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2)
|
|
{
|
|
MR_ROBDD_bitmask *ptr1 = &set1->bits[0];
|
|
MR_ROBDD_bitmask *ptr2 = &set2->bits[0];
|
|
MR_ROBDD_bitmask *ptr1end =
|
|
&set1->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD)+1];
|
|
|
|
for (;;) {
|
|
if (*ptr1 != *ptr2) {
|
|
return 0;
|
|
}
|
|
if (++ptr1 >= ptr1end) {
|
|
return 1;
|
|
}
|
|
++ptr2;
|
|
}
|
|
}
|
|
|
|
/* returns 1 if 2 sets are disjoint, else 0 */
|
|
__inline int
|
|
MR_ROBDD_bitset_disjoint(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2);
|
|
|
|
__inline int
|
|
MR_ROBDD_bitset_disjoint(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2)
|
|
{
|
|
MR_ROBDD_bitmask *ptr1 = &set1->bits[0];
|
|
MR_ROBDD_bitmask *ptr2 = &set2->bits[0];
|
|
MR_ROBDD_bitmask *ptr1end =
|
|
&set1->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD)+1];
|
|
|
|
for (;;) {
|
|
if ((*ptr1 & *ptr2) != 0) {
|
|
return 0;
|
|
}
|
|
if (++ptr1 >= ptr1end) {
|
|
return 1;
|
|
}
|
|
++ptr2;
|
|
}
|
|
}
|
|
|
|
/* returns 1 if set1 is a subset of set2 */
|
|
__inline int
|
|
MR_ROBDD_bitset_subset(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2);
|
|
|
|
__inline int
|
|
MR_ROBDD_bitset_subset(MR_ROBDD_bitset *set1, MR_ROBDD_bitset *set2)
|
|
{
|
|
MR_ROBDD_bitmask *ptr1 = &set1->bits[0];
|
|
MR_ROBDD_bitmask *ptr2 = &set2->bits[0];
|
|
MR_ROBDD_bitmask *ptr1end =
|
|
&set1->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD)+1];
|
|
|
|
for (;;) {
|
|
if ((*ptr1 | *ptr2) != *ptr2) {
|
|
return 0;
|
|
}
|
|
if (++ptr1 >= ptr1end) {
|
|
return 1;
|
|
}
|
|
++ptr2;
|
|
}
|
|
|
|
}
|
|
|
|
/* returns 1 if set1 is a subset of set2 */
|
|
__inline int MR_ROBDD_bitset_empty(MR_ROBDD_bitset *set);
|
|
|
|
__inline int MR_ROBDD_bitset_empty(MR_ROBDD_bitset *set)
|
|
{
|
|
MR_ROBDD_bitmask *ptr = &set->bits[0];
|
|
MR_ROBDD_bitmask *ptrend =
|
|
&set->bits[((MR_ROBDD_MAXVAR-1)/MR_ROBDD_BITS_PER_WORD)+1];
|
|
|
|
for (;;) {
|
|
if ((*ptr) != 0) {
|
|
return 0;
|
|
}
|
|
if (++ptr >= ptrend) {
|
|
return 1;
|
|
}
|
|
}
|
|
}
|
|
|
|
/****************************************************************
|
|
|
|
Making Nodes
|
|
|
|
****************************************************************/
|
|
|
|
#if defined(MR_ROBDD_BRYANT_CONSERVATIVE_GC)
|
|
|
|
static int MR_ROBDD_removed_nodes = 0;
|
|
|
|
void MR_ROBDD_remove_node(void *obj, void *client_data);
|
|
void MR_ROBDD_remove_node(void *obj, void *client_data)
|
|
{
|
|
MR_ROBDD_node *n = (MR_ROBDD_node *) obj;
|
|
MR_ROBDD_BRYANT_hidden_node_pointer *bucket =
|
|
(MR_ROBDD_BRYANT_hidden_node_pointer *) client_data;
|
|
|
|
if (MR_ROBDD_REVEAL_NODE_POINTER(n->unique) != NULL) {
|
|
MR_ROBDD_REVEAL_NODE_POINTER(n->unique)->uprev = n->uprev;
|
|
}
|
|
|
|
if (MR_ROBDD_REVEAL_NODE_POINTER(n->uprev) != NULL) {
|
|
MR_ROBDD_REVEAL_NODE_POINTER(n->uprev)->unique = n->unique;
|
|
}
|
|
|
|
if (MR_ROBDD_REVEAL_NODE_POINTER(*bucket) == n) {
|
|
*bucket = n->unique;
|
|
}
|
|
|
|
MR_ROBDD_removed_nodes++;
|
|
}
|
|
|
|
#endif /* MR_ROBDD_BRYANT_CONSERVATIVE_GC */
|
|
|
|
#if defined(MR_ROBDD_POOL)
|
|
static pool *MR_ROBDD_curr_pool = NULL;
|
|
static MR_ROBDD_node *MR_ROBDD_curr_pool_ptr = NULL;
|
|
static MR_ROBDD_node *MR_ROBDD_curr_pool_end_ptr = NULL;
|
|
#endif /* MR_ROBDD_POOL */
|
|
|
|
static int MR_ROBDD_node_count = 0;
|
|
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_alloc_node(int value, MR_ROBDD_node* tr, MR_ROBDD_node* fa,
|
|
MR_ROBDD_BRYANT_hidden_node_pointer *bucket)
|
|
{
|
|
MR_ROBDD_node *n;
|
|
#if defined(MR_ROBDD_POOL)
|
|
pool *newpool;
|
|
|
|
if (MR_ROBDD_curr_pool_ptr >= MR_ROBDD_curr_pool_end_ptr) {
|
|
/* allocate a new pool */
|
|
newpool = (pool *) malloc(sizeof(pool));
|
|
newpool->prev = MR_ROBDD_curr_pool;
|
|
MR_ROBDD_curr_pool = newpool;
|
|
MR_ROBDD_curr_pool_ptr = &(newpool->data[0]);
|
|
MR_ROBDD_curr_pool_end_ptr = &(newpool->data[MR_ROBDD_POOL_SIZE]);
|
|
}
|
|
n = MR_ROBDD_curr_pool_ptr++;
|
|
#else /* !MR_ROBDD_POOL */
|
|
n = (MR_ROBDD_node *) malloc(sizeof(MR_ROBDD_node));
|
|
#if defined(MR_ROBDD_BRYANT_CONSERVATIVE_GC)
|
|
GC_register_finalizer(n, MR_ROBDD_remove_node, bucket, 0, 0);
|
|
#endif
|
|
#endif /* MR_ROBDD_POOL */
|
|
MR_ROBDD_node_count++;
|
|
n->value = value;
|
|
n->tr = tr;
|
|
n->fa = fa;
|
|
return n;
|
|
}
|
|
|
|
/* return the number of graph nodes that have been created. */
|
|
int
|
|
MR_ROBDD_nodes_in_use(void)
|
|
{
|
|
return MR_ROBDD_node_count;
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_make_node)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_make_node(int var, MR_ROBDD_node *tr, MR_ROBDD_node *fa)
|
|
{
|
|
MR_ROBDD_BRYANT_hidden_node_pointer *bucket;
|
|
MR_ROBDD_node *ptr;
|
|
|
|
assert(var>=0);
|
|
assert(var<MR_ROBDD_MAXVAR);
|
|
assert(MR_ROBDD_IS_TERMINAL(tr) || tr->value > var);
|
|
assert(MR_ROBDD_IS_TERMINAL(fa) || fa->value > var);
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_make_node);
|
|
|
|
if (tr == fa) {
|
|
return tr;
|
|
}
|
|
|
|
bucket = &MR_ROBDD_unique_table[MR_ROBDD_UNIQUE_HASH(var,tr,fa)];
|
|
|
|
/*
|
|
** The following check avoids the need to initialise the table
|
|
** elements to MR_ROBDD_HIDE_POINTER(NULL).
|
|
*/
|
|
if (*bucket == 0) {
|
|
*bucket = MR_ROBDD_HIDE_POINTER(NULL);
|
|
}
|
|
|
|
ptr = MR_ROBDD_REVEAL_NODE_POINTER(*bucket);
|
|
while (ptr != NULL && (var!=ptr->value || tr!=ptr->tr || fa!=ptr->fa)) {
|
|
ptr = MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique);
|
|
}
|
|
|
|
if (ptr != NULL) {
|
|
MR_ROBDD_COUNT_UNIQUE_HIT;
|
|
return ptr;
|
|
}
|
|
|
|
/* MR_ROBDD_node doesn't exist so create it and put in bucket */
|
|
MR_ROBDD_COUNT_UNIQUE_MISS;
|
|
ptr = MR_ROBDD_alloc_node(var, tr, fa, bucket);
|
|
ptr->unique = *bucket;
|
|
*bucket = MR_ROBDD_HIDE_POINTER(ptr);
|
|
#ifdef MR_ROBDD_BRYANT_CONSERVATIVE_GC
|
|
ptr->uprev = MR_ROBDD_HIDE_POINTER(NULL);
|
|
if (MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique) != NULL) {
|
|
MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique)->uprev =
|
|
MR_ROBDD_HIDE_POINTER(ptr);
|
|
}
|
|
#endif
|
|
return ptr;
|
|
}
|
|
|
|
void
|
|
MR_ROBDD_free_rep(MR_ROBDD_node *n)
|
|
{
|
|
/* never free ROBDD nodes */
|
|
}
|
|
|
|
/****************************************************************
|
|
|
|
The Basic Algorithms
|
|
|
|
****************************************************************/
|
|
|
|
int MR_ROBDD_max_variable(void);
|
|
|
|
int
|
|
MR_ROBDD_max_variable(void)
|
|
{
|
|
return MR_ROBDD_MAXVAR;
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_trueVar(void)
|
|
{
|
|
return MR_ROBDD_one;
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_falseVar(void)
|
|
{
|
|
return MR_ROBDD_zero;
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_variableRep)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_variableRep(int var)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_variableRep);
|
|
return MR_ROBDD_make_node(var,MR_ROBDD_one,MR_ROBDD_zero);
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_ite)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_ite(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h)
|
|
{
|
|
MR_ROBDD_node *f_tr, *f_fa;
|
|
MR_ROBDD_node *g_tr, *g_fa;
|
|
MR_ROBDD_node *h_tr, *h_fa;
|
|
MR_ROBDD_node *newnode;
|
|
int top;
|
|
MR_ROBDD_DECLARE_ITE_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_ite);
|
|
/* terminal cases */
|
|
if (f == MR_ROBDD_one) {
|
|
return g;
|
|
}
|
|
if (f == MR_ROBDD_zero) {
|
|
return h;
|
|
}
|
|
if ((g == MR_ROBDD_one) && (h == MR_ROBDD_zero)) {
|
|
return f;
|
|
}
|
|
if (g == h) {
|
|
return g;
|
|
}
|
|
|
|
/* look it up in computed table; finished if found */
|
|
MR_ROBDD_TRY_ITE_CACHE(f, g, h, MR_ROBDD_ite);
|
|
|
|
/* find top variable */
|
|
top = f->value; /* we know f is not terminal */
|
|
if (!MR_ROBDD_IS_TERMINAL(g) && (g->value < top)) {
|
|
top = g->value;
|
|
}
|
|
if (!MR_ROBDD_IS_TERMINAL(h) && (h->value < top)) {
|
|
top = h->value;
|
|
}
|
|
|
|
/* find then and else branches for recursive calls */
|
|
if (f->value==top) {
|
|
f_tr = f->tr; f_fa = f->fa;
|
|
} else {
|
|
f_tr = f; f_fa = f;
|
|
}
|
|
if (!MR_ROBDD_IS_TERMINAL(g) && g->value==top) {
|
|
g_tr = g->tr; g_fa = g->fa;
|
|
} else {
|
|
g_tr = g; g_fa = g;
|
|
}
|
|
if (!MR_ROBDD_IS_TERMINAL(h) && h->value==top) {
|
|
h_tr = h->tr; h_fa = h->fa;
|
|
} else {
|
|
h_tr = h; h_fa = h;
|
|
}
|
|
|
|
/* create new MR_ROBDD_node and add to table */
|
|
newnode = MR_ROBDD_make_node(top,
|
|
MR_ROBDD_ite(f_tr, g_tr, h_tr),
|
|
MR_ROBDD_ite(f_fa, g_fa, h_fa));
|
|
MR_ROBDD_UPDATE_ITE_CACHE(f,g,h,newnode,MR_ROBDD_ite);
|
|
return newnode;
|
|
}
|
|
|
|
#if defined(MR_ROBDD_USE_ITE_CONSTANT)
|
|
|
|
/*
|
|
** This is sort of an "approximate MR_ROBDD_ite()." It returns MR_ROBDD_zero
|
|
** or MR_ROBDD_one if that's what MR_ROBDD_ite() would do. Otherwise it just
|
|
** returns the pseudo-MR_ROBDD_node `MR_ROBDD_nonterminal' or some real
|
|
** MR_ROBDD_node. In any case, it does not create any new nodes.
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_ite_constant(MR_ROBDD_node *f,MR_ROBDD_node *g,MR_ROBDD_node *h)
|
|
{
|
|
MR_ROBDD_node *f_tr, *f_fa;
|
|
MR_ROBDD_node *g_tr, *g_fa;
|
|
MR_ROBDD_node *h_tr, *h_fa;
|
|
MR_ROBDD_node *tr_part, *fa_part;
|
|
MR_ROBDD_node *result;
|
|
int top;
|
|
MR_ROBDD_DECLARE_ITE_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_ite);
|
|
/* terminal cases */
|
|
if (f == MR_ROBDD_one) {
|
|
return g;
|
|
}
|
|
if (f == MR_ROBDD_zero) {
|
|
return h;
|
|
}
|
|
if (g == h) {
|
|
return g;
|
|
}
|
|
if (MR_ROBDD_IS_TERMINAL(g) && MR_ROBDD_IS_TERMINAL(h)) {
|
|
/* either f or ~f, which is MR_ROBDD_nonterminal since f is */
|
|
return MR_ROBDD_nonterminal;
|
|
}
|
|
|
|
/* look it up in computed table; finished if found */
|
|
MR_ROBDD_TRY_ITE_CACHE(f, g, h, MR_ROBDD_ite_constant);
|
|
|
|
/* find top variable */
|
|
top = f->value; /* we know f is not terminal */
|
|
if (!MR_ROBDD_IS_TERMINAL(g) && (g->value < top)) {
|
|
top = g->value;
|
|
}
|
|
if (!MR_ROBDD_IS_TERMINAL(h) && (h->value < top)) {
|
|
top = h->value;
|
|
}
|
|
|
|
/* find then and else branches for recursive calls */
|
|
if (f->value==top) {
|
|
f_tr = f->tr; f_fa = f->fa;
|
|
} else {
|
|
f_tr = f; f_fa = f;
|
|
}
|
|
if (!MR_ROBDD_IS_TERMINAL(g) && g->value==top) {
|
|
g_tr = g->tr; g_fa = g->fa;
|
|
} else {
|
|
g_tr = g; g_fa = g;
|
|
}
|
|
if (!MR_ROBDD_IS_TERMINAL(h) && h->value==top) {
|
|
h_tr = h->tr; h_fa = h->fa;
|
|
} else {
|
|
h_tr = h; h_fa = h;
|
|
}
|
|
|
|
tr_part = MR_ROBDD_ite_constant(f_tr, g_tr, h_tr);
|
|
fa_part = MR_ROBDD_ite_constant(f_fa, g_fa, h_fa);
|
|
if (tr_part == fa_part) {
|
|
result = tr_part;
|
|
} else {
|
|
result = MR_ROBDD_nonterminal;
|
|
}
|
|
|
|
MR_ROBDD_UPDATE_ITE_CACHE(f,g,h,result,MR_ROBDD_ite_constant);
|
|
return result;
|
|
}
|
|
#endif /* MR_ROBDD_USE_ITE_CONSTANT */
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_implies)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_implies(MR_ROBDD_node *a, MR_ROBDD_node *b)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_implies);
|
|
return MR_ROBDD_ite(a,b,MR_ROBDD_one);
|
|
}
|
|
|
|
/* returns a copy of graph a */
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_copy(MR_ROBDD_node *a)
|
|
{
|
|
return a;
|
|
}
|
|
|
|
/* returns true if graph a and b are equiv */
|
|
|
|
int
|
|
MR_ROBDD_equiv(MR_ROBDD_node *a, MR_ROBDD_node *b)
|
|
{
|
|
return (a == b);
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_lub)
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_glb)
|
|
|
|
#if defined(MR_ROBDD_NAIVE)
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_glb(MR_ROBDD_node *a, MR_ROBDD_node *b)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_glb);
|
|
return MR_ROBDD_ite(a,b,MR_ROBDD_zero);
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_lub(MR_ROBDD_node *a, MR_ROBDD_node *b)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_lub);
|
|
return MR_ROBDD_ite(a,MR_ROBDD_one,b);
|
|
}
|
|
|
|
#else /* !MR_ROBDD_NAIVE */
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_lub(MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_lub);
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f == MR_ROBDD_one ? MR_ROBDD_one : g;
|
|
} else if (MR_ROBDD_IS_TERMINAL(g)) {
|
|
return g == MR_ROBDD_one ? MR_ROBDD_one : f;
|
|
} MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,f)
|
|
else {
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
|
|
|
|
MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_lub);
|
|
|
|
if (f->value < g->value) {
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_lub(f->tr, g), MR_ROBDD_lub(f->fa, g));
|
|
} else if (f->value > g->value) {
|
|
result = MR_ROBDD_make_node(g->value,
|
|
MR_ROBDD_lub(f, g->tr), MR_ROBDD_lub(f, g->fa));
|
|
} else /* f->value == g->value */{
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_lub(f->tr, g->tr), MR_ROBDD_lub(f->fa, g->fa));
|
|
}
|
|
MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_lub);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_glb(MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_glb);
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f == MR_ROBDD_one ? g : MR_ROBDD_zero;
|
|
} else if (MR_ROBDD_IS_TERMINAL(g)) {
|
|
return g == MR_ROBDD_one ? f : MR_ROBDD_zero;
|
|
} MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,f)
|
|
else {
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
|
|
|
|
MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_glb);
|
|
|
|
if (f->value < g->value) {
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_glb(f->tr, g), MR_ROBDD_glb(f->fa, g));
|
|
} else if (f->value > g->value) {
|
|
result = MR_ROBDD_make_node(g->value,
|
|
MR_ROBDD_glb(f, g->tr), MR_ROBDD_glb(f, g->fa));
|
|
} else /* f->value == g->value */{
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_glb(f->tr, g->tr), MR_ROBDD_glb(f->fa, g->fa));
|
|
}
|
|
MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_glb);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
#endif /* MR_ROBDD_NAIVE */
|
|
|
|
#if defined(MR_ROBDD_NAIVE)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_glb_array(int n, int arr[])
|
|
{
|
|
int i;
|
|
MR_ROBDD_node *result = MR_ROBDD_one;
|
|
|
|
for (i = 0; i < n; ++i) {
|
|
result = MR_ROBDD_glb(result, MR_ROBDD_variableRep(arr[i]));
|
|
}
|
|
return result;
|
|
}
|
|
|
|
#else /* !MR_ROBDD_NAIVE */
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_glb_array(int n, int arr[])
|
|
{
|
|
int i;
|
|
MR_ROBDD_node *result = MR_ROBDD_one;
|
|
|
|
qsort((char *)arr, n, sizeof(int), MR_ROBDD_intcompare);
|
|
for (i = n-1; i >= 0; --i) {
|
|
result = MR_ROBDD_make_node(arr[i], result, MR_ROBDD_zero);
|
|
}
|
|
return result;
|
|
}
|
|
|
|
#endif /* MR_ROBDD_NAIVE */
|
|
|
|
/****************************************************************
|
|
|
|
Restriction (Projection, Existential Quantification)
|
|
|
|
****************************************************************/
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_restrict)
|
|
|
|
/* restricts c in f. */
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restrict(int c, MR_ROBDD_node *f)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_restrict);
|
|
if (MR_ROBDD_IS_TERMINAL(f) || (f->value > c)) {
|
|
return f;
|
|
} else if (f->value < c) {
|
|
return MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_restrict(c,f->tr), MR_ROBDD_restrict(c,f->fa));
|
|
} else {
|
|
return MR_ROBDD_lub(f->tr, f->fa);
|
|
}
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_restrictThresh)
|
|
|
|
#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restrictThresh(int lo, int hi, MR_ROBDD_node *a)
|
|
{
|
|
int i;
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_restrictThresh);
|
|
for(i = lo+1; i <= hi; ++i) {
|
|
a = MR_ROBDD_restrict(i, a);
|
|
}
|
|
return a;
|
|
}
|
|
|
|
#elif !defined(MR_ROBDD_USE_THRESH) /* && defined(MR_ROBDD_RESTRICT_SET) */
|
|
|
|
/*
|
|
** union vars with the set of all variables greater than thresh appearing in
|
|
** the ROBDD rooted at f.
|
|
*/
|
|
|
|
static void
|
|
MR_ROBDD_vars_present(MR_ROBDD_node *f, int thresh, MR_ROBDD_bitset *vars)
|
|
{
|
|
while (!MR_ROBDD_IS_TERMINAL(f)) {
|
|
if (f->value > thresh) {
|
|
MR_ROBDD_BITSET_ADD_ELEMENT(*vars, f->value);
|
|
}
|
|
MR_ROBDD_vars_present(f->tr, thresh, vars);
|
|
f = f->fa;
|
|
}
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restrictThresh(int thresh, MR_ROBDD_node *f)
|
|
{
|
|
MR_ROBDD_bitset vars;
|
|
int var;
|
|
int word;
|
|
MR_ROBDD_bitmask mask;
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_restrictThresh);
|
|
MR_ROBDD_BITSET_CLEAR(vars);
|
|
MR_ROBDD_vars_present(f, thresh, &vars);
|
|
MR_ROBDD_REV_FOREACH_ELEMENT(vars, var, word, mask) {
|
|
f = MR_ROBDD_restrict(var, f);
|
|
}
|
|
return f;
|
|
}
|
|
|
|
#else /* MR_ROBDD_USE_THRESH */
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restrictThresh(int thresh, MR_ROBDD_node *f)
|
|
{
|
|
/* restricts all variables greater than thresh. */
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_restrictThresh);
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f;
|
|
} else if (f->value <= thresh) {
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY;
|
|
|
|
MR_ROBDD_TRY_ASYM_BIN_CACHE((MR_ROBDD_node *) thresh, f, MR_ROBDD_restrictThresh);
|
|
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_restrictThresh(thresh, f->tr),
|
|
MR_ROBDD_restrictThresh(thresh, f->fa));
|
|
MR_ROBDD_UPDATE_ASYM_BIN_CACHE((MR_ROBDD_node *) thresh, f, result, MR_ROBDD_restrictThresh);
|
|
return result;
|
|
} else {
|
|
return MR_ROBDD_one;
|
|
}
|
|
}
|
|
|
|
#endif /* MR_ROBDD_USE_THRESH */
|
|
|
|
#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restricted_glb(int lo, int hi, MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
return MR_ROBDD_restrictThresh(lo, hi, MR_ROBDD_glb(f, g));
|
|
}
|
|
|
|
#elif !defined(MR_ROBDD_USE_RGLB) /* && ( MR_ROBDD_USE_THRESH || MR_ROBDD_RESTRICT_SET ) */
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restricted_glb(int thresh, MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
return MR_ROBDD_restrictThresh(thresh, MR_ROBDD_glb(f, g));
|
|
}
|
|
|
|
#else /* MR_ROBDD_USE_RGLB */
|
|
|
|
/* returns true iff MR_ROBDD_glb(f,g) is not 'MR_ROBDD_zero' */
|
|
static int
|
|
MR_ROBDD_exists_glb(MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_FALSE;
|
|
} else if (g == MR_ROBDD_zero) {
|
|
return MR_FALSE;
|
|
} else if (f == MR_ROBDD_one) {
|
|
/* since we know that g != MR_ROBDD_zero... */
|
|
return MR_TRUE;
|
|
} else if (g == MR_ROBDD_one) {
|
|
/* likewise f... */
|
|
return MR_TRUE;
|
|
} else if (f->value < g->value) {
|
|
return MR_ROBDD_exists_glb(f->tr, g) || MR_ROBDD_exists_glb(f->fa, g);
|
|
} else if (f->value > g->value) {
|
|
return MR_ROBDD_exists_glb(f, g->tr) || MR_ROBDD_exists_glb(f, g->fa);
|
|
} else {
|
|
return MR_ROBDD_exists_glb(f->tr, g->tr) || MR_ROBDD_exists_glb(f->fa, g->fa);
|
|
}
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restricted_glb(int c, MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return (f == MR_ROBDD_one) ? MR_ROBDD_restrictThresh(c, g)
|
|
: MR_ROBDD_zero;
|
|
} else if (MR_ROBDD_IS_TERMINAL(g)) {
|
|
return (g == MR_ROBDD_one) ? MR_ROBDD_restrictThresh(c, f)
|
|
: MR_ROBDD_zero;
|
|
} MR_ROBDD_ELSE_TRY_EQUAL_TEST(f,g,MR_ROBDD_restrictThresh(c, f))
|
|
else {
|
|
int v;
|
|
MR_ROBDD_node *tr1, *tr2, *fa1, *fa2;
|
|
MR_ROBDD_node *result;
|
|
|
|
MR_ROBDD_DECLARE_RGLB_CACHE_ENTRY
|
|
|
|
MR_ROBDD_TRY_RGLB_CACHE(f, g, c);
|
|
|
|
if (f->value < g->value) {
|
|
v = f->value;
|
|
tr1 = f->tr;
|
|
tr2 = g;
|
|
fa1 = f->fa;
|
|
fa2 = g;
|
|
} else if (f->value > g->value) {
|
|
v = g->value;
|
|
tr1 = f;
|
|
tr2 = g->tr;
|
|
fa1 = f;
|
|
fa2 = g->fa;
|
|
} else /* f->value == g->value */{
|
|
v = f->value;
|
|
tr1 = f->tr;
|
|
tr2 = g->tr;
|
|
fa1 = f->fa;
|
|
fa2 = g->fa;
|
|
}
|
|
if (v > c) {
|
|
result =
|
|
(MR_ROBDD_exists_glb(tr1,tr2)||MR_ROBDD_exists_glb(fa1,fa2)) ?
|
|
MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
result = MR_ROBDD_make_node(v,
|
|
MR_ROBDD_restricted_glb(c, tr1, tr2),
|
|
MR_ROBDD_restricted_glb(c, fa1, fa2));
|
|
}
|
|
MR_ROBDD_UPDATE_RGLB_CACHE(f,g,c,result);
|
|
return result;
|
|
}
|
|
}
|
|
#endif /* MR_ROBDD_USE_THRESH */
|
|
|
|
/****************************************************************
|
|
|
|
Renaming
|
|
|
|
****************************************************************/
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_renameArray)
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_reverseRenameArray)
|
|
|
|
#if defined(MR_ROBDD_NEW)
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_ite_var)
|
|
|
|
/* A special case version of MR_ROBDD_ite_var, where we know that f < g->value */
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_ite_var_g(int f, MR_ROBDD_node *g, MR_ROBDD_node *h)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_ite_var);
|
|
|
|
assert(MR_ROBDD_IS_TERMINAL(g) || f < g->value);
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(h) || f < h->value) {
|
|
/* f < g && f < h */
|
|
return MR_ROBDD_make_node(f, g, h);
|
|
} else if (f == h->value) {
|
|
return MR_ROBDD_make_node(f, g, h->fa);
|
|
} else {
|
|
/* h < f < g */
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
|
|
|
|
MR_ROBDD_TRY_ITE_VAR_CACHE(f, g, h);
|
|
|
|
result = MR_ROBDD_make_node(h->value,
|
|
MR_ROBDD_ite_var_g(f, g, h->tr),
|
|
MR_ROBDD_ite_var_g(f, g, h->fa));
|
|
MR_ROBDD_UPDATE_ITE_VAR_CACHE(f, g, h, result);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
/*
|
|
** A special case version of MR_ROBDD_ite_var, where we know that
|
|
** f < h->value
|
|
*/
|
|
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_ite_var_h(int f, MR_ROBDD_node *g, MR_ROBDD_node *h)
|
|
{
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_ite_var);
|
|
|
|
assert(MR_ROBDD_IS_TERMINAL(h) || f < h->value);
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(g) || f < g->value) {
|
|
/* f < g && f < h */
|
|
return MR_ROBDD_make_node(f, g, h);
|
|
} else if (f == g->value) {
|
|
return MR_ROBDD_make_node(f, g->tr, h);
|
|
} else {
|
|
/* h < f < g */
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
|
|
|
|
MR_ROBDD_TRY_ITE_VAR_CACHE(f, g, h);
|
|
result = MR_ROBDD_make_node(g->value,
|
|
MR_ROBDD_ite_var_h(f, g->tr, h),
|
|
MR_ROBDD_ite_var_h(f, g->fa, h));
|
|
MR_ROBDD_UPDATE_ITE_VAR_CACHE(f, g, h, result);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
/*
|
|
** A special case version of MR_ROBDD_ite, where we know that
|
|
** !MR_ROBDD_IS_TERMINAL(f) && f->tr == MR_ROBDD_one && f->fa == MR_ROBDD_zero.
|
|
** In fact, we refine this further and make f be just (what would have been)
|
|
** f->value.
|
|
**
|
|
** Recall the code for MR_ROBDD_ite: it finds the minimum value of f, g, and h
|
|
** (call it top), and sets each of ft, gt and ht to the tr branch of the
|
|
** corresponding arg if its value == top, else sets it to the arg itself, and
|
|
** correspondingly for ff, gf, and hf. Then the value of MR_ROBDD_ite is:
|
|
**
|
|
** mn(top, i(ft, gt, ht), i(ff, gf, hf))
|
|
**
|
|
** (abbreviating MR_ROBDD_make_node as mn and MR_ROBDD_ite as i). Given this,
|
|
** we can simplify things in several cases. Here are all the cases, and the
|
|
** simplified value. (We introduce ig for MR_ROBDD_ite_var_g and ih for
|
|
** MR_ROBDD_ite_var_h as special cases where we know f < g or f < h,
|
|
** respectively.)
|
|
**
|
|
** a) f = g = h (1) mn(f, g->tr, h->fa) *** Impossible
|
|
**
|
|
** b) f < g < h (2) mn(f, g, h)
|
|
** c) f < g = h (2) mn(f, g, h)
|
|
** d) f < h < g (2) mn(f, g, h)
|
|
** e) f = g < h (3) mn(f, g->tr, h) *** Impossible
|
|
** f) f = h < g (4) mn(f, g, h->fa) *** Impossible
|
|
**
|
|
** g) g < f < h (5) mn(gv, ih(f, g->tr, h), ih(f, g->fa, h))
|
|
** h) g < f = h (6) mn(gv, i(f, g->tr, h), i(f, g->fa, h)) *** Impossible
|
|
** i) g < h < f (6) mn(gv, i(f, g->tr, h), i(f, g->fa, h))
|
|
** j) g = h < f (7) mn(gv, i(f, g->tr, h->tr), i(f, g->fa, h->fa))
|
|
**
|
|
** k) h < f < g (8) mn(hv, ig(f, g, h->tr), ig(f, g, h->fa))
|
|
** l) h < f = g (9) mn(hv, i(f, g, h->tr), i(f, g, h->fa)) *** Impossible
|
|
** m) h < g < f (9) mn(hv, i(f, g, h->tr), i(f, g, h->fa))
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_ite_var(int f,MR_ROBDD_node *g,MR_ROBDD_node *h)
|
|
{
|
|
int g_val = INT_MAX;
|
|
int h_val = INT_MAX;
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_node *g_tr, *g_fa, *h_tr, *h_fa;
|
|
MR_ROBDD_DECLARE_ITE_VAR_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_ite_var);
|
|
MR_ROBDD_DIRECT_EQUAL_TEST(g,h,g);
|
|
MR_ROBDD_TRY_ITE_VAR_CACHE(f, g, h);
|
|
|
|
if (!MR_ROBDD_IS_TERMINAL(g)) g_val = g->value;
|
|
if (!MR_ROBDD_IS_TERMINAL(h)) h_val = h->value;
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(g)) {
|
|
g_tr = g_fa = g;
|
|
} else {
|
|
g_tr = g->tr;
|
|
g_fa = g->fa;
|
|
}
|
|
if (MR_ROBDD_IS_TERMINAL(h)) {
|
|
h_tr = h_fa = h;
|
|
} else {
|
|
h_tr = h->tr;
|
|
h_fa = h->fa;
|
|
}
|
|
|
|
if (f < g_val) {
|
|
if (f < h_val) /* case 2 (b,c,d): f < g && f < h */ {
|
|
result = MR_ROBDD_make_node(f, g, h);
|
|
} else /* case 8 (k): h < f < g */ {
|
|
result = MR_ROBDD_make_node(h_val,
|
|
MR_ROBDD_ite_var_g(f, g, h_tr),
|
|
MR_ROBDD_ite_var_g(f, g, h_fa));
|
|
}
|
|
/* g < f */
|
|
} else if (f < h_val) /* g < f < h */ {
|
|
result = MR_ROBDD_make_node(g_val,
|
|
MR_ROBDD_ite_var_h(f, g_tr, h),
|
|
MR_ROBDD_ite_var_h(f, g_fa, h));
|
|
/* g < f && h < f */
|
|
} else if (h_val < g_val) /* case 9 (l,m): h < g < f */ {
|
|
result = MR_ROBDD_make_node(h_val,
|
|
MR_ROBDD_ite_var(f, g, h_tr),
|
|
MR_ROBDD_ite_var(f, g, h_fa));
|
|
/* g < f && g <= h */
|
|
} else if (g_val == h_val) /* g == h < f */ {
|
|
result = MR_ROBDD_make_node(g_val,
|
|
MR_ROBDD_ite_var(f, g_tr, h_tr),
|
|
MR_ROBDD_ite_var(f, g_fa, h_fa));
|
|
} else /* case 6 (h,i): g < h < f */ {
|
|
result = MR_ROBDD_make_node(g_val,
|
|
MR_ROBDD_ite_var(f, g_tr, h),
|
|
MR_ROBDD_ite_var(f, g_fa, h));
|
|
}
|
|
|
|
MR_ROBDD_UPDATE_ITE_VAR_CACHE(f, g, h, result);
|
|
return result;
|
|
}
|
|
|
|
#else /* ! MR_ROBDD_NEW */
|
|
|
|
#define MR_ROBDD_ite_var(v,f,g) MR_ROBDD_ite(MR_ROBDD_variableRep(v), f, g)
|
|
|
|
#endif /* !MR_ROBDD_NEW */
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_renameArray(MR_ROBDD_node *f, int count, int mapping[])
|
|
{
|
|
int newval;
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_renameArray);
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f;
|
|
} else if (f->value > count) {
|
|
return MR_ROBDD_one;
|
|
} else if (MR_ROBDD_UNUSED_MAPPING==(newval=mapping[f->value])) {
|
|
return MR_ROBDD_lub(MR_ROBDD_renameArray(f->tr, count, mapping),
|
|
MR_ROBDD_renameArray(f->fa, count, mapping));
|
|
} else {
|
|
return MR_ROBDD_ite_var(newval,
|
|
MR_ROBDD_renameArray(f->tr, count, mapping),
|
|
MR_ROBDD_renameArray(f->fa, count, mapping));
|
|
}
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_reverseRenameArray(MR_ROBDD_node *f, int count, int mapping[])
|
|
{
|
|
int i, val, MR_ROBDD_max;
|
|
int rev_map[MR_ROBDD_MAXVAR];
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_reverseRenameArray);
|
|
/* NB: four -1 bytes is the same as a -1 word */
|
|
MR_memset(rev_map, ~((char) 0), sizeof(rev_map));
|
|
for (i=1,MR_ROBDD_max=-1; i<=count; ++i) {
|
|
rev_map[(val=mapping[i])] = i;
|
|
if (MR_ROBDD_max < val) MR_ROBDD_max = val;
|
|
}
|
|
|
|
return MR_ROBDD_renameArray(f, MR_ROBDD_max, rev_map);
|
|
}
|
|
|
|
/****************************************************************
|
|
|
|
Abstract Exit (renaming + conjunction + restriction)
|
|
|
|
****************************************************************/
|
|
|
|
#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_abstract_exit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
|
|
int mapping[], int lo, int hi)
|
|
{
|
|
return MR_ROBDD_restricted_glb(lo, hi, context,
|
|
MR_ROBDD_renameArray(f, count, mapping));
|
|
}
|
|
|
|
#elif 1 /* ( MR_ROBDD_USE_THRESH || MR_ROBDD_RESTRICT_SET ) */
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_abstract_exit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
|
|
int mapping[], int thresh)
|
|
{
|
|
return MR_ROBDD_restricted_glb(thresh, context,
|
|
MR_ROBDD_renameArray(f, count, mapping));
|
|
}
|
|
|
|
#else /* 0 (this code not used) */
|
|
|
|
/*
|
|
** returns MR_FALSE iff the function f restricted so that all variables in
|
|
** trues are set to true and all in falses are set to false evaluates to
|
|
** MR_ROBDD_zero.
|
|
*/
|
|
|
|
int
|
|
MR_ROBDD_exists_restrict_sets(MR_ROBDD_node *f, MR_ROBDD_bitset *trues,
|
|
MR_ROBDD_bitset *falses, int hielt)
|
|
{
|
|
for (;;) {
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f == MR_ROBDD_one;
|
|
} else if (f->value > hielt) {
|
|
return MR_TRUE;
|
|
} else {
|
|
int word = MR_ROBDD_BITSET_WORD(f->value);
|
|
MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
|
|
|
|
if (MR_ROBDD_BITSET_MEMBER(*trues,word,mask)) {
|
|
f = f->tr; /* continue loop */
|
|
} else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
|
|
f = f->fa; /* continue loop */
|
|
} else if (MR_ROBDD_exists_restrict_sets(f->tr, trues, falses,
|
|
hielt))
|
|
{
|
|
return MR_TRUE;
|
|
} else {
|
|
f = f->fa;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/*
|
|
** computes the function f restricted so that all variables in trues
|
|
** are set to true and all in falses are set to false.
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restrict_sets(MR_ROBDD_node *f, MR_ROBDD_bitset *trues,
|
|
MR_ROBDD_bitset *falses, int hielt, int thresh)
|
|
{
|
|
for (;;) {
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f;
|
|
} else if (f->value > hielt) {
|
|
return MR_ROBDD_restrictThresh(thresh, f);
|
|
} else if (f->value > thresh) {
|
|
return MR_ROBDD_exists_restrict_sets(f, trues, falses, hielt)
|
|
? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
int word = MR_ROBDD_BITSET_WORD(f->value);
|
|
MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
|
|
|
|
if (MR_ROBDD_BITSET_MEMBER(*trues,word,mask)) {
|
|
f = f->tr; /* continue loop */
|
|
} else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
|
|
f = f->fa; /* continue loop */
|
|
} else {
|
|
return MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_restrict_sets(f->tr, trues, falses, hielt,
|
|
thresh),
|
|
MR_ROBDD_restrict_sets(f->fa, trues, falses, hielt,
|
|
thresh));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/*
|
|
** if f->value > thresh, returns MR_ROBDD_one, else if f->value is in either
|
|
** trues (or falses), this returns
|
|
** MR_ROBDD_follow_path(f->tr (or fa), trues, falses}
|
|
** else it returns f.
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_follow_path(MR_ROBDD_node *f, MR_ROBDD_bitset *trues,
|
|
MR_ROBDD_bitset *falses)
|
|
{
|
|
|
|
while (!MR_ROBDD_IS_TERMINAL(f)) {
|
|
int word = MR_ROBDD_BITSET_WORD(f->value);
|
|
MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
|
|
|
|
if (MR_ROBDD_BITSET_MEMBER(*trues,word,mask)) {
|
|
f = f->tr;
|
|
} else if (MR_ROBDD_BITSET_MEMBER(*falses,word,mask)) {
|
|
f = f->fa;
|
|
} else {
|
|
break;
|
|
}
|
|
}
|
|
return f;
|
|
}
|
|
|
|
/*
|
|
** This function computes
|
|
**
|
|
** MR_ROBDD_restrictThresh(MR_ROBDD_renameArray(f, count, mapping), thresh)
|
|
**
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_restricted_rename(MR_ROBDD_node *f, int count, int mapping[],
|
|
int thresh)
|
|
{
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f;
|
|
} else {
|
|
int newval = mapping[f->value];
|
|
MR_ROBDD_node *tr, *fa;
|
|
|
|
tr = MR_ROBDD_restricted_rename(f->tr, count, mapping, thresh);
|
|
fa = MR_ROBDD_restricted_rename(f->fa, count, mapping, thresh);
|
|
|
|
if (newval > thresh) {
|
|
return MR_ROBDD_lub(tr, fa);
|
|
} else {
|
|
return MR_ROBDD_ite_var(newval, tr, fa);
|
|
}
|
|
}
|
|
}
|
|
|
|
/*
|
|
** This function computes
|
|
**
|
|
** MR_ROBDD_restrictThresh(MR_ROBDD_glb(context1,
|
|
** MR_ROBDD_renameArray(f, count, mapping)), thresh)
|
|
**
|
|
** where context1 is context restricted by the settings in trues and
|
|
** falses. We know that !MR_ROBDD_IS_TERMINAL(context).
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_abexit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
|
|
int mapping[], int thresh, MR_ROBDD_bitset *trues,
|
|
MR_ROBDD_bitset *falses, int hielt)
|
|
{
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
if (f==MR_ROBDD_one) {
|
|
return MR_ROBDD_restrict_sets(context, trues, falses, hielt,
|
|
thresh);
|
|
} else {
|
|
return f;
|
|
}
|
|
} else {
|
|
int newval = mapping[f->value];
|
|
MR_ROBDD_node *tr, *fa;
|
|
|
|
if (newval == context->value) {
|
|
tr = MR_ROBDD_follow_path(context->tr, trues, falses);
|
|
fa = MR_ROBDD_follow_path(context->fa, trues, falses);
|
|
|
|
if (tr == MR_ROBDD_one) {
|
|
tr = MR_ROBDD_restricted_rename(f->tr, count, mapping, thresh);
|
|
} else if (tr != MR_ROBDD_zero) {
|
|
tr = MR_ROBDD_abexit(tr, f->tr, count, mapping, thresh,
|
|
trues, falses, hielt);
|
|
}
|
|
if (fa == MR_ROBDD_one) {
|
|
fa = MR_ROBDD_restricted_rename(f->fa, count, mapping, thresh);
|
|
} else if (fa != MR_ROBDD_zero) {
|
|
fa = MR_ROBDD_abexit(fa, f->fa, count, mapping, thresh,
|
|
trues, falses, hielt);
|
|
}
|
|
} else {
|
|
int word = MR_ROBDD_BITSET_WORD(newval);
|
|
MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(newval);
|
|
int newhi = (newval>hielt ? newval : hielt);
|
|
|
|
MR_ROBDD_BITSET_ADD(*trues,word,mask); /* turn on true bit */
|
|
tr = MR_ROBDD_abexit(context, f->tr, count, mapping, thresh,
|
|
trues, falses, newhi);
|
|
MR_ROBDD_BITSET_TOGGLE(*trues,word,mask); /* turn off true bit */
|
|
MR_ROBDD_BITSET_ADD(*falses,word,mask); /* turn on false bit */
|
|
fa = MR_ROBDD_abexit(context, f->fa, count, mapping, thresh,
|
|
trues, falses, newhi);
|
|
MR_ROBDD_BITSET_TOGGLE(*falses,word,mask); /* turn off false bit */
|
|
}
|
|
if (newval > thresh) {
|
|
return MR_ROBDD_lub(tr, fa);
|
|
} else {
|
|
return MR_ROBDD_ite_var(newval, tr, fa);
|
|
}
|
|
}
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_abstract_exit(MR_ROBDD_node *context, MR_ROBDD_node *f, int count,
|
|
int mapping[], int thresh)
|
|
{
|
|
MR_ROBDD_bitset trues;
|
|
MR_ROBDD_bitset falses;
|
|
|
|
if (context == MR_ROBDD_zero)
|
|
return MR_ROBDD_zero;
|
|
if (context == MR_ROBDD_one)
|
|
return MR_ROBDD_restricted_rename(f, count, mapping, thresh);
|
|
|
|
MR_ROBDD_BITSET_CLEAR(trues);
|
|
MR_ROBDD_BITSET_CLEAR(falses);
|
|
|
|
return MR_ROBDD_abexit(context, f, count, mapping, thresh,
|
|
&trues, &falses, -1);
|
|
}
|
|
|
|
#endif /* 0 (end of unused code) */
|
|
|
|
/****************************************************************
|
|
|
|
Abstract Unification
|
|
|
|
****************************************************************/
|
|
|
|
/*
|
|
** NB: MR_ROBDD_iff_conj_array, and so all the functions that call it, now
|
|
** allow v0 to apear in the array of variables arr[]. This makes the
|
|
** analyzer robust for handling goals like X = f(X,Y). Since it's
|
|
** cheaper and easier to check this in C, I do it here.
|
|
*/
|
|
|
|
#if defined(MR_ROBDD_ELIM_DUPS)
|
|
#define MR_ROBDD_DECLARE_PREV(init) int prev = (init);
|
|
#define MR_ROBDD_HANDLE_DUP(this,rel) \
|
|
if ((this) == prev) continue; \
|
|
assert((this) rel prev); \
|
|
prev = (this);
|
|
#elif !defined(NDEBUG)
|
|
#define MR_ROBDD_DECLARE_PREV(init) int prev = (init);
|
|
#define MR_ROBDD_HANDLE_DUP(this,rel) \
|
|
assert((this) != prev); \
|
|
assert((this) rel prev); \
|
|
prev = (this);
|
|
#else
|
|
#define MR_ROBDD_DECLARE_PREV(init)
|
|
#define MR_ROBDD_HANDLE_DUP(this,rel)
|
|
#endif
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(iff_conj)
|
|
|
|
#if defined(MR_ROBDD_NAIVE)
|
|
MR_ROBDD_node *MR_ROBDD_iff_conj_array(int v0, int n, int arr[])
|
|
{
|
|
MR_ROBDD_node *conj = MR_ROBDD_one;
|
|
MR_ROBDD_node *v_rep = MR_ROBDD_variableRep(v0);
|
|
int i;
|
|
MR_ROBDD_DECLARE_PREV(-1)
|
|
|
|
MR_ROBDD_COUNT_FN(iff_conj);
|
|
/* We construct the conjunction from the lowest var up to the highest.
|
|
* This is a quadratic process, while the other way is linear.
|
|
*/
|
|
for (i=0; i<n; ++i) {
|
|
MR_ROBDD_HANDLE_DUP(arr[i], >)
|
|
if (arr[i] != v0) {
|
|
conj = MR_ROBDD_glb(conj, MR_ROBDD_variableRep(arr[i]));
|
|
}
|
|
}
|
|
return MR_ROBDD_glb(MR_ROBDD_implies(conj,v_rep),
|
|
MR_ROBDD_implies(v_rep,conj));
|
|
}
|
|
|
|
#elif !defined(MR_ROBDD_USE_THRESH)
|
|
|
|
MR_ROBDD_node *MR_ROBDD_iff_conj_array(int v0, int n, int arr[])
|
|
{
|
|
MR_ROBDD_node *conj = MR_ROBDD_one;
|
|
MR_ROBDD_node *pos_v = MR_ROBDD_variableRep(v0);
|
|
MR_ROBDD_node *neg_v = MR_ROBDD_ite(pos_v, MR_ROBDD_zero, MR_ROBDD_one);
|
|
int *ptr;
|
|
MR_ROBDD_DECLARE_PREV(MR_ROBDD_MAXVAR)
|
|
|
|
MR_ROBDD_COUNT_FN(iff_conj);
|
|
/* Note that to be efficient, we construct the conjunction
|
|
* from the highest var down to the lowest. This is a linear
|
|
* process, while the other way is n squared.
|
|
*/
|
|
for (ptr=&arr[n-1]; ptr>=arr; --ptr) {
|
|
int vi = *ptr;
|
|
MR_ROBDD_HANDLE_DUP(vi, <)
|
|
if (vi != v0) {
|
|
conj = MR_ROBDD_glb(conj, MR_ROBDD_variableRep(vi));
|
|
}
|
|
}
|
|
return MR_ROBDD_ite(conj, pos_v, neg_v);
|
|
}
|
|
|
|
#else /* MR_ROBDD_USE_THRESH */
|
|
|
|
MR_ROBDD_node *MR_ROBDD_iff_conj_array(int v0, int n, int arr[])
|
|
{
|
|
MR_ROBDD_node *thens = MR_ROBDD_one, *elses = MR_ROBDD_zero;
|
|
int *ptr;
|
|
int vi = 0; /* this value doesn't matter */
|
|
MR_ROBDD_DECLARE_PREV(MR_ROBDD_MAXVAR)
|
|
|
|
MR_ROBDD_COUNT_FN(iff_conj);
|
|
/*
|
|
** first build part of graph below v0. For this, we build two subgraphs:
|
|
** MR_ROBDD_one for when v0 is true, and MR_ROBDD_one for false.
|
|
** These are called thens and elses.
|
|
*/
|
|
|
|
for (ptr=&arr[n-1]; ptr>=arr && v0<(vi=*ptr); --ptr) {
|
|
MR_ROBDD_HANDLE_DUP(vi, <)
|
|
thens = MR_ROBDD_make_node(vi, thens, MR_ROBDD_zero);
|
|
elses = MR_ROBDD_make_node(vi, elses, MR_ROBDD_one);
|
|
}
|
|
|
|
if (v0 == vi) {
|
|
--ptr;
|
|
}
|
|
|
|
/* make v0 MR_ROBDD_node */
|
|
thens = MR_ROBDD_make_node(v0,thens,elses);
|
|
|
|
/* Finally build part of graph above v0. For this, we build
|
|
* only MR_ROBDD_one graph, whose then branch is the graph we've built
|
|
* so far and whose else branch is ~v0.
|
|
*/
|
|
|
|
if (ptr >= arr) {
|
|
MR_ROBDD_DECLARE_PREV(MR_ROBDD_MAXVAR)
|
|
/* make ~v0 */
|
|
elses = MR_ROBDD_make_node(v0,MR_ROBDD_zero,MR_ROBDD_one);
|
|
|
|
do {
|
|
vi = *ptr;
|
|
MR_ROBDD_HANDLE_DUP(vi, <)
|
|
thens = MR_ROBDD_make_node(vi, thens, elses);
|
|
} while (--ptr >= arr);
|
|
}
|
|
|
|
return thens;
|
|
}
|
|
#endif /* MR_ROBDD_OLD */
|
|
|
|
MR_ROBDD_node *MR_ROBDD_restricted_iff_conj_array(int v0, int n, int arr[],
|
|
int thresh)
|
|
{
|
|
if (v0 > thresh) {
|
|
return MR_ROBDD_one;
|
|
}
|
|
while (--n>=0 && arr[n]>thresh)
|
|
;
|
|
return MR_ROBDD_iff_conj_array(v0, n+1, arr);
|
|
}
|
|
|
|
#if !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_RESTRICT_SET)
|
|
MR_ROBDD_node *MR_ROBDD_abstract_unify(MR_ROBDD_node *f, int v0, int n,
|
|
int arr[], int lo, int hi)
|
|
{
|
|
return MR_ROBDD_restricted_glb(lo, hi, f,
|
|
MR_ROBDD_iff_conj_array(v0, n, arr));
|
|
}
|
|
|
|
#elif 1 /* ( MR_ROBDD_USE_THRESH || MR_ROBDD_RESTRICT_SET ) */
|
|
|
|
MR_ROBDD_node *MR_ROBDD_abstract_unify(MR_ROBDD_node *f, int v0, int n,
|
|
int arr[], int thresh)
|
|
{
|
|
return MR_ROBDD_restricted_glb(thresh, f,
|
|
MR_ROBDD_iff_conj_array(v0, n, arr));
|
|
}
|
|
|
|
#else /* !1 (this code is unused) */
|
|
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_build_and(int n, int arr[], MR_ROBDD_node *tr, MR_ROBDD_node *fa)
|
|
{
|
|
if (n<=0) {
|
|
return tr;
|
|
} else {
|
|
return MR_ROBDD_make_node(arr[0],
|
|
MR_ROBDD_build_and(n-1, &arr[1], tr, fa), fa);
|
|
}
|
|
}
|
|
|
|
static MR_ROBDD_node *MR_ROBDD_glb_and(MR_ROBDD_node *f, int n, int arr[])
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_ROBDD_zero;
|
|
} else if (f == MR_ROBDD_one) {
|
|
return MR_ROBDD_build_and(n, arr, MR_ROBDD_one, MR_ROBDD_zero);
|
|
} else if (n == 0) {
|
|
return f;
|
|
} else {
|
|
MR_ROBDD_node *result;
|
|
if (f->value < arr[0]) {
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_glb_and(f->tr, n, arr),
|
|
MR_ROBDD_glb_and(f->fa, n, arr));
|
|
} else if (f->value > arr[0]) {
|
|
result = MR_ROBDD_make_node(arr[0],
|
|
MR_ROBDD_glb_and(f, n-1, &arr[1]),
|
|
MR_ROBDD_zero);
|
|
} else /* f->value == arr[0] */{
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_glb_and(f->tr, n-1, &arr[1]),
|
|
MR_ROBDD_zero);
|
|
}
|
|
return result;
|
|
}
|
|
}
|
|
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_glb_nand(MR_ROBDD_node *f, int n, int arr[])
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_ROBDD_zero;
|
|
} else if (f == MR_ROBDD_one) {
|
|
return MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one);
|
|
} else if (n == 0) {
|
|
return MR_ROBDD_zero;
|
|
} else {
|
|
MR_ROBDD_node *result;
|
|
if (f->value < arr[0]) {
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_glb_nand(f->tr, n, arr),
|
|
MR_ROBDD_glb_nand(f->fa, n, arr));
|
|
} else if (f->value > arr[0]) {
|
|
result = MR_ROBDD_make_node(arr[0],
|
|
MR_ROBDD_glb_nand(f, n-1, &arr[1]),
|
|
f);
|
|
} else /* f->value == arr[0] */{
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_glb_nand(f->tr, n-1, &arr[1]),
|
|
f);
|
|
}
|
|
return result;
|
|
}
|
|
}
|
|
|
|
/*
|
|
** returns MR_ROBDD_zero != MR_ROBDD_glb(f,
|
|
** MR_ROBDD_build_and(n, arr, MR_ROBDD_one, MR_ROBDD_zero))
|
|
*/
|
|
|
|
static int
|
|
MR_ROBDD_exists_glb_and(MR_ROBDD_node *f, int n, int arr[])
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_FALSE;
|
|
} else if (f == MR_ROBDD_one || n == 0) {
|
|
return MR_TRUE;
|
|
} else if (f->value < arr[0]) {
|
|
return (MR_ROBDD_exists_glb_and(f->tr, n, arr) ||
|
|
MR_ROBDD_exists_glb_and(f->fa, n, arr));
|
|
} else {
|
|
if (f->value == arr[0]) {
|
|
f = f->tr;
|
|
}
|
|
return MR_ROBDD_exists_glb_and(f, n-1, arr+1);
|
|
}
|
|
}
|
|
|
|
/*
|
|
** returns MR_ROBDD_zero != MR_ROBDD_glb(f,
|
|
** MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one))
|
|
*/
|
|
|
|
static int
|
|
MR_ROBDD_exists_glb_nand(MR_ROBDD_node *f, int n, int arr[])
|
|
{
|
|
if (f == MR_ROBDD_zero || n == 0) {
|
|
return MR_FALSE;
|
|
} else if (f == MR_ROBDD_one || f->value > arr[0]) {
|
|
/*
|
|
** if f->value > arr[0], then the else branch of the MR_ROBDD_node we'd
|
|
** build would be MR_ROBDD_one, so we know the graph couldn't ==
|
|
** MR_ROBDD_zero.
|
|
*/
|
|
return MR_TRUE;
|
|
} else if (f->value < arr[0]) {
|
|
return MR_ROBDD_glb_nand(f->tr, n, arr)
|
|
|| MR_ROBDD_glb_nand(f->fa, n, arr);
|
|
} else if (f->fa != MR_ROBDD_zero) /* && f->value == arr[0] */ {
|
|
/*
|
|
** if f->fa isn't MR_ROBDD_zero, then conjoined with MR_ROBDD_one
|
|
** it won't be MR_ROBDD_zero, so the MR_ROBDD_node we'd build won't
|
|
** == MR_ROBDD_zero.
|
|
*/
|
|
return MR_TRUE;
|
|
} else /* f->value == arr[0] && f->fa == MR_ROBDD_zero */ {
|
|
return MR_ROBDD_exists_glb_nand(f->tr, n-1, arr+1);
|
|
}
|
|
}
|
|
|
|
/*
|
|
** returns MR_ROBDD_zero != MR_ROBDD_glb(f,
|
|
** MR_ROBDD_iff_conj_array(v0, n, arr))
|
|
*/
|
|
|
|
static int
|
|
MR_ROBDD_exists_glb_iffconj(MR_ROBDD_node *f, int v0, int n, int arr[])
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_FALSE;
|
|
} else if (f == MR_ROBDD_one) {
|
|
return MR_TRUE;
|
|
} else {
|
|
int v = (n>0 && arr[0]<v0) ? arr[0] : v0;
|
|
|
|
if (f->value < v) {
|
|
return (MR_ROBDD_exists_glb_iffconj(f->tr, v0, n, arr) ||
|
|
MR_ROBDD_exists_glb_iffconj(f->fa, v0, n, arr));
|
|
} else /* f->value >= v */ {
|
|
MR_ROBDD_node *tr, *fa;
|
|
|
|
if (f->value == v) {
|
|
tr = f->tr; fa = f->fa;
|
|
} else /* f->value > v */ {
|
|
tr = f; fa = f;
|
|
}
|
|
|
|
if (v == v0) {
|
|
return (MR_ROBDD_exists_glb_nand(fa, n, arr) ||
|
|
MR_ROBDD_exists_glb_and(tr, n, arr));
|
|
} else {
|
|
return (!MR_ROBDD_var_entailed(fa, v0) ||
|
|
MR_ROBDD_exists_glb_iffconj(tr, v0, n-1, &arr[1]));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/*
|
|
** returns MR_ROBDD_restricted_glb(f,
|
|
** MR_ROBDD_build_and(n, arr, MR_ROBDD_one, MR_ROBDD_zero), thresh)
|
|
*/
|
|
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_rglb_and(MR_ROBDD_node *f, int n, int arr[], int thresh)
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_ROBDD_zero;
|
|
} else if (f == MR_ROBDD_one) {
|
|
while (--n>=0 && arr[n]>thresh);
|
|
return MR_ROBDD_build_and(n+1, arr, MR_ROBDD_one, MR_ROBDD_zero);
|
|
} else if (n == 0) {
|
|
return MR_ROBDD_restrictThresh(thresh, f);
|
|
} else {
|
|
if (f->value < arr[0]) {
|
|
if (f->value > thresh) {
|
|
return (MR_ROBDD_exists_glb_and(f->tr, n, arr) ||
|
|
MR_ROBDD_exists_glb_and(f->fa, n, arr))
|
|
? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
return MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_rglb_and(f->tr, n, arr, thresh),
|
|
MR_ROBDD_rglb_and(f->fa, n, arr, thresh));
|
|
}
|
|
} else /* arr[0] <= f->value */ {
|
|
int v = arr[0];
|
|
|
|
if (v == f->value) {
|
|
f = f->tr;
|
|
}
|
|
if (v > thresh) {
|
|
return MR_ROBDD_exists_glb_and(f, n-1, arr+1)
|
|
? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
return MR_ROBDD_make_node(v,
|
|
MR_ROBDD_rglb_and(f, n-1, arr+1, thresh),
|
|
MR_ROBDD_zero);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/*
|
|
** returns MR_ROBDD_restricted_glb(f,
|
|
** MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one), thresh)
|
|
*/
|
|
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_rglb_nand(MR_ROBDD_node *f, int n, int arr[], int thresh)
|
|
{
|
|
if (f == MR_ROBDD_zero || n == 0) {
|
|
return MR_ROBDD_zero;
|
|
} else if (f == MR_ROBDD_one) {
|
|
/*
|
|
** just MR_ROBDD_restrictThresh(thresh,
|
|
** MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one)).
|
|
** Note that if anything is restricted away, then the whole graph
|
|
** degenerates to MR_ROBDD_one. So...
|
|
*/
|
|
if (arr[n-1]>thresh) {
|
|
return MR_ROBDD_one;
|
|
} else {
|
|
return MR_ROBDD_build_and(n, arr, MR_ROBDD_zero, MR_ROBDD_one);
|
|
}
|
|
} else {
|
|
if (f->value < arr[0]) {
|
|
if (f->value > thresh) {
|
|
return (MR_ROBDD_exists_glb_nand(f->tr, n, arr)||
|
|
MR_ROBDD_exists_glb_nand(f->fa, n, arr))
|
|
? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
return MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_rglb_nand(f->tr, n, arr, thresh),
|
|
MR_ROBDD_rglb_nand(f->fa, n, arr, thresh));
|
|
}
|
|
} else if (f->value > arr[0]) {
|
|
if (arr[0] > thresh) {
|
|
/* because f != MR_ROBDD_zero, restricting all vars yields MR_ROBDD_one */
|
|
return MR_ROBDD_one;
|
|
} else {
|
|
return MR_ROBDD_make_node(arr[0],
|
|
MR_ROBDD_rglb_nand(f, n-1, arr+1, thresh),
|
|
MR_ROBDD_restrictThresh(thresh, f));
|
|
}
|
|
} else /* f->value == arr[0] */ {
|
|
if (arr[0] > thresh) {
|
|
return (f->fa != MR_ROBDD_zero ||
|
|
MR_ROBDD_exists_glb_nand(f->tr, n-1, arr+1))
|
|
? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
return MR_ROBDD_make_node(arr[0],
|
|
MR_ROBDD_rglb_nand(f->tr, n-1, arr+1, thresh),
|
|
MR_ROBDD_restrictThresh(thresh, f->fa));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/*
|
|
** returns MR_ROBDD_restricted_glb(thresh, f,
|
|
** MR_ROBDD_make_node(v, MR_ROBDD_zero, MR_ROBDD_one))
|
|
*/
|
|
|
|
static MR_ROBDD_node *
|
|
MR_ROBDD_rglb_notvar(MR_ROBDD_node *f, int v, int thresh)
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_ROBDD_zero;
|
|
} else if (f == MR_ROBDD_one) {
|
|
if (v > thresh) return MR_ROBDD_one;
|
|
return MR_ROBDD_make_node(v, MR_ROBDD_zero, MR_ROBDD_one);
|
|
} else {
|
|
if (f->value < v) {
|
|
if (f->value > thresh) {
|
|
return (!MR_ROBDD_var_entailed(f->tr, v) ||
|
|
!MR_ROBDD_var_entailed(f->fa, v))
|
|
? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
return MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_rglb_notvar(f->tr, v, thresh),
|
|
MR_ROBDD_rglb_notvar(f->fa, v, thresh));
|
|
}
|
|
} else {
|
|
if (f->value == v) {
|
|
f = f->fa;
|
|
}
|
|
if (v > thresh) {
|
|
return f==MR_ROBDD_zero ? MR_ROBDD_zero : MR_ROBDD_one;
|
|
} else {
|
|
return MR_ROBDD_make_node(v, MR_ROBDD_zero,
|
|
MR_ROBDD_restrictThresh(thresh, f));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_abstract_unify(MR_ROBDD_node *f, int v0, int n, int arr[], int thresh)
|
|
{
|
|
if (f == MR_ROBDD_zero) {
|
|
return MR_ROBDD_zero;
|
|
} else if (f == MR_ROBDD_one) {
|
|
return MR_ROBDD_restricted_iff_conj_array(v0, n, arr, thresh);
|
|
} else {
|
|
int v = (n>0 && arr[0]<v0) ? arr[0] : v0;
|
|
MR_ROBDD_node *result;
|
|
|
|
if (f->value < v) {
|
|
if (f->value > thresh) {
|
|
result = (MR_ROBDD_exists_glb_iffconj(f->tr, v0, n, arr) ||
|
|
MR_ROBDD_exists_glb_iffconj(f->fa, v0, n, arr))
|
|
? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
result =
|
|
MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_abstract_unify(f->tr, v0, n, arr, thresh),
|
|
MR_ROBDD_abstract_unify(f->fa, v0, n, arr, thresh));
|
|
}
|
|
} else /* f->value >= v */ {
|
|
MR_ROBDD_node *tr = f, *fa = f;
|
|
|
|
if (f->value == v) {
|
|
tr = f->tr; fa = f->fa;
|
|
}
|
|
if (v > thresh) {
|
|
int value;
|
|
|
|
if (v == v0) {
|
|
value = (MR_ROBDD_exists_glb_nand(fa, n, arr) ||
|
|
MR_ROBDD_exists_glb_and(tr, n, arr));
|
|
} else {
|
|
value =
|
|
(!MR_ROBDD_var_entailed(fa, v0) ||
|
|
MR_ROBDD_exists_glb_iffconj(tr, v0, n-1, &arr[1]));
|
|
}
|
|
result = value ? MR_ROBDD_one : MR_ROBDD_zero;
|
|
} else {
|
|
if (v == v0) {
|
|
tr = MR_ROBDD_rglb_and(tr, n, arr, thresh);
|
|
fa = MR_ROBDD_rglb_nand(fa, n, arr, thresh);
|
|
} else {
|
|
tr = MR_ROBDD_abstract_unify(tr, v0, n-1, arr+1, thresh);
|
|
fa = MR_ROBDD_rglb_notvar(fa, v0, thresh);
|
|
}
|
|
result = MR_ROBDD_make_node(v, tr, fa);
|
|
}
|
|
}
|
|
return result;
|
|
}
|
|
}
|
|
|
|
#endif /* (end of unused code) */
|
|
|
|
/****************************************************************
|
|
|
|
Finding Entailed Variables
|
|
|
|
****************************************************************/
|
|
|
|
/*
|
|
** returns MR_TRUE iff var is implied by the boolean function specified by f
|
|
*/
|
|
|
|
int
|
|
MR_ROBDD_var_entailed(MR_ROBDD_node *f, int var)
|
|
{
|
|
#if defined(MR_ROBDD_NAIVE)
|
|
return f == MR_ROBDD_glb(f, MR_ROBDD_variableRep(var));
|
|
#elif !defined(MR_ROBDD_USE_THRESH) && !defined(MR_ROBDD_USE_ITE_CONSTANT)
|
|
return MR_ROBDD_one == MR_ROBDD_implies(f, MR_ROBDD_variableRep(var));
|
|
#elif !defined(MR_ROBDD_USE_RGLB)
|
|
return MR_ROBDD_one == MR_ROBDD_ite_constant(f, MR_ROBDD_variableRep(var),
|
|
MR_ROBDD_one);
|
|
#else /* MR_ROBDD_USE_RGLB */
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f==MR_ROBDD_zero;
|
|
} else {
|
|
MR_ROBDD_DECLARE_VAR_ENTAILED_CACHE_ENTRY
|
|
int result;
|
|
|
|
MR_ROBDD_TRY_VAR_ENTAILED_CACHE(f, var);
|
|
if (f->value < var) {
|
|
result = MR_ROBDD_var_entailed(f->tr, var)
|
|
&& MR_ROBDD_var_entailed(f->fa, var);
|
|
} else if (f->value == var) {
|
|
result = (f->fa==MR_ROBDD_zero);
|
|
} else /* f->value > var */ {
|
|
result = MR_FALSE;
|
|
}
|
|
MR_ROBDD_UPDATE_VAR_ENTAILED_CACHE(f, var, result);
|
|
return result;
|
|
}
|
|
#endif /* MR_ROBDD_NEW */
|
|
}
|
|
|
|
/*
|
|
** returns a MR_ROBDD_bitset of all the variables implied by f. A variable i
|
|
** is implied by f iff
|
|
**
|
|
** MR_ROBDD_BITSET_IS_MEMBER(*result, i)
|
|
*/
|
|
|
|
#if !defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_bitset *
|
|
MR_ROBDD_vars_entailed(MR_ROBDD_node *f, int MR_ROBDD_topvar)
|
|
{
|
|
static MR_ROBDD_bitset def_vars;
|
|
int i;
|
|
|
|
MR_ROBDD_BITSET_CLEAR(def_vars);
|
|
|
|
for (i=0; i<MR_ROBDD_topvar; ++i) {
|
|
if (MR_ROBDD_var_entailed(f, i)) {
|
|
MR_ROBDD_BITSET_ADD_ELEMENT(def_vars,i);
|
|
}
|
|
}
|
|
return &def_vars;
|
|
}
|
|
|
|
#elif 0 /* not using this version */
|
|
|
|
int
|
|
MR_ROBDD_topvar(MR_ROBDD_node *f, int n)
|
|
{
|
|
int n1;
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(f)) return n;
|
|
|
|
n1 = MR_ROBDD_topvar(f->tr, f->value);
|
|
if (n1 > n) {
|
|
n = n1;
|
|
}
|
|
return MR_ROBDD_topvar(f->fa, n);
|
|
}
|
|
|
|
MR_ROBDD_bitset *
|
|
MR_ROBDD_vars_entailed(MR_ROBDD_node *f)
|
|
{
|
|
static MR_ROBDD_bitset def_vars;
|
|
int i = MR_ROBDD_topvar(f, 0);
|
|
|
|
MR_ROBDD_BITSET_CLEAR(def_vars);
|
|
|
|
for (; i >= 0; --i) {
|
|
if (MR_ROBDD_var_entailed(f, i)) {
|
|
MR_ROBDD_BITSET_ADD_ELEMENT(def_vars,i);
|
|
}
|
|
}
|
|
return &def_vars;
|
|
}
|
|
|
|
#else /* MR_ROBDD_NEW */
|
|
|
|
/*
|
|
** According to Roberto Bagnara's benchmarking, this version is slower
|
|
** than the simpler version below.
|
|
*/
|
|
|
|
#if defined(OLD_VARS_ENTAILED)
|
|
|
|
/*
|
|
** these variables should be local to both MR_ROBDD_vars_entailed and
|
|
** MR_ROBDD_vars_entailed_aux, but that isn't possible in C, so I have to make
|
|
** them global. They should not be use by any other functions.
|
|
*/
|
|
|
|
static MR_ROBDD_bitset MR_ROBDD_this_path;
|
|
static MR_ROBDD_bitset MR_ROBDD_entailed;
|
|
|
|
void
|
|
MR_ROBDD_vars_entailed_aux(MR_ROBDD_node *f)
|
|
{
|
|
while (!MR_ROBDD_IS_TERMINAL(f)) {
|
|
int word = MR_ROBDD_BITSET_WORD(f->value);
|
|
MR_ROBDD_bitmask mask = MR_ROBDD_BITSET_MASK(f->value);
|
|
|
|
/* turn on bit for then branch */
|
|
MR_ROBDD_BITSET_ADD(MR_ROBDD_this_path,word,mask);
|
|
MR_ROBDD_vars_entailed_aux(f->tr);
|
|
/* turn it off for the else branch */
|
|
MR_ROBDD_BITSET_TOGGLE(MR_ROBDD_this_path,word,mask);
|
|
f = f->fa;
|
|
}
|
|
/* needn't do anything for false terminals */
|
|
if (f == MR_ROBDD_one) {
|
|
MR_ROBDD_BITSET_INTERSECTION(MR_ROBDD_entailed, MR_ROBDD_entailed,
|
|
MR_ROBDD_this_path);
|
|
}
|
|
}
|
|
|
|
/*
|
|
** returns a MR_ROBDD_bitset of all the variables implied by f. A variable i
|
|
** is implied by f iff
|
|
**
|
|
** MR_ROBDD_BITSET_IS_MEMBER(*result, i)
|
|
*/
|
|
|
|
MR_ROBDD_bitset *
|
|
MR_ROBDD_vars_entailed(MR_ROBDD_node *f)
|
|
{
|
|
MR_ROBDD_BITSET_CLEAR(MR_ROBDD_this_path);
|
|
MR_ROBDD_BITSET_UNIVERSE(MR_ROBDD_entailed);
|
|
|
|
MR_ROBDD_vars_entailed_aux(f);
|
|
return &MR_ROBDD_entailed;
|
|
}
|
|
|
|
#else /* MR_ROBDD_NEW && !OLD_VARS_ENTAILED */
|
|
|
|
/*
|
|
** returns a MR_ROBDD_bitset of all the variables implied by f. A variable i
|
|
** is implied by f iff
|
|
**
|
|
** MR_ROBDD_BITSET_IS_MEMBER(*result, i)
|
|
*/
|
|
|
|
MR_ROBDD_bitset *
|
|
MR_ROBDD_vars_entailed(MR_ROBDD_node *f)
|
|
{
|
|
static MR_ROBDD_bitset tmp_bitset;
|
|
MR_ROBDD_DECLARE_UNARY_BITSET_CACHE_ENTRY
|
|
|
|
if (f == MR_ROBDD_zero) {
|
|
MR_ROBDD_BITSET_UNIVERSE(tmp_bitset);
|
|
} else if (f == MR_ROBDD_one) {
|
|
MR_ROBDD_BITSET_CLEAR(tmp_bitset);
|
|
} else {
|
|
MR_ROBDD_bitset bs;
|
|
|
|
MR_ROBDD_TRY_UNARY_BITSET_CACHE(f, MR_ROBDD_vars_entailed);
|
|
tmp_bitset = *MR_ROBDD_vars_entailed(f->tr);
|
|
bs = *MR_ROBDD_vars_entailed(f->fa);
|
|
MR_ROBDD_BITSET_INTERSECTION(tmp_bitset, tmp_bitset, bs);
|
|
if (f->fa == MR_ROBDD_zero) {
|
|
MR_ROBDD_BITSET_ADD_ELEMENT(tmp_bitset, f->value);
|
|
}
|
|
MR_ROBDD_UPDATE_UNARY_BITSET_CACHE(f, tmp_bitset,
|
|
MR_ROBDD_vars_entailed);
|
|
}
|
|
return &tmp_bitset;
|
|
}
|
|
|
|
#endif /* MR_ROBDD_NEW && !OLD_VARS_ENTAILED */
|
|
#endif /* MR_ROBDD_NEW */
|
|
|
|
/****************************************************************
|
|
|
|
Set Sharing Operations
|
|
|
|
****************************************************************/
|
|
#if defined(MR_ROBDD_SHARING)
|
|
|
|
/*
|
|
** returns the Boolean function
|
|
** ~1&~2&...~n | 1&~2&...~n | ~1&2&...~n | ~1&~2&...n
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_init_set_sharing(int n)
|
|
{
|
|
MR_ROBDD_node *result = MR_ROBDD_one;
|
|
MR_ROBDD_node *other = MR_ROBDD_one;
|
|
|
|
while (n>1) {
|
|
other = MR_ROBDD_make_node(n, MR_ROBDD_zero, other);
|
|
result = MR_ROBDD_make_node(--n, other, result);
|
|
}
|
|
|
|
return result;
|
|
}
|
|
|
|
#if defined(MR_ROBDD_NEW)
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete_one_or)
|
|
|
|
/* the same as MR_ROBDD_lub(MR_ROBDD_complete_one(f), prev) */
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_complete_one_or(MR_ROBDD_node *f, MR_ROBDD_node *prev)
|
|
{
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_node *MR_ROBDD_complete_one(MR_ROBDD_node *f);
|
|
MR_ROBDD_DECLARE_ASYM_BIN_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_complete_one_or);
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(prev)) {
|
|
return (prev==MR_ROBDD_one) ? MR_ROBDD_one : MR_ROBDD_complete_one(f);
|
|
}
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return (f==MR_ROBDD_one) ? MR_ROBDD_one : prev;
|
|
}
|
|
|
|
MR_ROBDD_TRY_ASYM_BIN_CACHE(f, prev, MR_ROBDD_complete_one_or);
|
|
|
|
/*
|
|
** we want to return:
|
|
** MR_ROBDD_lub(MR_ROBDD_make_node(f->value,
|
|
** MR_ROBDD_lub(MR_ROBDD_complete_one(f->tr),
|
|
** MR_ROBDD_complete_one(f->fa)),
|
|
** MR_ROBDD_complete_one(f->fa)),
|
|
** prev);
|
|
** but we want to unfold the outer MR_ROBDD_lub call, so we compare
|
|
** prev->value and f->value. Actually, this isn't right when
|
|
** f->value <= prev->value, because the MR_ROBDD_make_node call may return
|
|
** a MR_ROBDD_node whose label is > prev->value, but in that case,
|
|
** MR_ROBDD_lub(that, prev) = MR_ROBDD_make_node(prev->value,
|
|
** MR_ROBDD_lub(that, prev->tr), MR_ROBDD_lub(that, prev->fa))
|
|
*/
|
|
|
|
if (f->value < prev->value) {
|
|
MR_ROBDD_node *cfa = MR_ROBDD_complete_one_or(f->fa, prev);
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_complete_one_or(f->tr, cfa), cfa);
|
|
} else if (f->value == prev->value) {
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_complete_one_or(f->tr,
|
|
MR_ROBDD_complete_one_or(f->fa,
|
|
prev->tr)),
|
|
MR_ROBDD_complete_one_or(f->fa, prev->fa));
|
|
} else {
|
|
result = MR_ROBDD_make_node(prev->value,
|
|
MR_ROBDD_complete_one_or(f, prev->tr),
|
|
MR_ROBDD_complete_one_or(f, prev->fa));
|
|
}
|
|
MR_ROBDD_UPDATE_ASYM_BIN_CACHE(f, prev, result, MR_ROBDD_complete_one_or);
|
|
return result;
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete_one)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_complete_one(MR_ROBDD_node *f)
|
|
{
|
|
MR_ROBDD_node *result, *cfa;
|
|
MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_complete_one);
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f;
|
|
}
|
|
MR_ROBDD_TRY_UNARY_CACHE(f, MR_ROBDD_complete_one);
|
|
cfa = MR_ROBDD_complete_one(f->fa);
|
|
result = MR_ROBDD_make_node(f->value,
|
|
MR_ROBDD_complete_one_or(f->tr, cfa), cfa);
|
|
MR_ROBDD_UPDATE_UNARY_CACHE(f, result, MR_ROBDD_complete_one);
|
|
return result;
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete_or)
|
|
|
|
/* the same as MR_ROBDD_lub(MR_ROBDD_complete(f, g), prev) */
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_complete_or(MR_ROBDD_node *f, MR_ROBDD_node *g, MR_ROBDD_node *prev)
|
|
{
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_node *lo, *hi;
|
|
MR_ROBDD_DECLARE_COMPLETE_OR_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_complete_or);
|
|
|
|
if (prev == MR_ROBDD_one) {
|
|
return MR_ROBDD_one;
|
|
}
|
|
if (f == g) {
|
|
return MR_ROBDD_lub(f, prev);
|
|
}
|
|
if (f == MR_ROBDD_zero || g == MR_ROBDD_zero) {
|
|
return prev;
|
|
}
|
|
|
|
if (f == MR_ROBDD_one) {
|
|
return MR_ROBDD_complete_one_or(g, prev);
|
|
}
|
|
if (g == MR_ROBDD_one) {
|
|
return MR_ROBDD_complete_one_or(f, prev);
|
|
}
|
|
if (prev == MR_ROBDD_zero) {
|
|
return MR_ROBDD_complete(f, g);
|
|
}
|
|
|
|
MR_ROBDD_TRY_COMPLETE_OR_CACHE(f, g, prev);
|
|
|
|
if (f->value > g->value) {
|
|
lo=g;
|
|
hi=f;
|
|
} else {
|
|
lo=f;
|
|
hi=g;
|
|
}
|
|
|
|
if (prev->value < lo->value) {
|
|
result = MR_ROBDD_make_node(prev->value,
|
|
MR_ROBDD_complete_or(lo, hi, prev->tr),
|
|
MR_ROBDD_complete_or(lo, hi, prev->fa));
|
|
} else if (prev->value == lo->value) {
|
|
if (lo->value == hi->value) {
|
|
MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->tr, hi->tr, prev->tr);
|
|
n = MR_ROBDD_complete_or(lo->tr, hi->fa, n);
|
|
n = MR_ROBDD_complete_or(lo->fa, hi->tr, n);
|
|
result = MR_ROBDD_make_node(lo->value, n,
|
|
MR_ROBDD_complete_or(lo->fa, hi->fa, prev->fa));
|
|
} else {
|
|
MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->fa, hi, prev->tr);
|
|
n = MR_ROBDD_complete_or(lo->tr, hi, n);
|
|
result = MR_ROBDD_make_node(lo->value, n,
|
|
MR_ROBDD_complete_or(lo->fa, hi, prev->fa));
|
|
}
|
|
} else if (lo->value == hi->value) {
|
|
MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->tr, hi->tr, prev);
|
|
n = MR_ROBDD_complete_or(lo->tr, hi->fa, n);
|
|
n = MR_ROBDD_complete_or(lo->fa, hi->tr, n);
|
|
result = MR_ROBDD_make_node(lo->value, n,
|
|
MR_ROBDD_complete_or(lo->fa, hi->fa, prev));
|
|
} else {
|
|
MR_ROBDD_node *n = MR_ROBDD_complete_or(lo->fa, hi, prev);
|
|
result = MR_ROBDD_make_node(lo->value,
|
|
MR_ROBDD_complete_or(lo->tr, hi, n), n);
|
|
}
|
|
MR_ROBDD_UPDATE_COMPLETE_OR_CACHE(f, g, prev, result);
|
|
|
|
return result;
|
|
}
|
|
|
|
#else /* !MR_ROBDD_NEW */
|
|
|
|
#define MR_ROBDD_complete_or(x, y, z) \
|
|
MR_ROBDD_lub(MR_ROBDD_complete((x),(y)),(z))
|
|
#endif
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_complete)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_complete(MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
MR_ROBDD_node *result;
|
|
int fvar, gvar;
|
|
MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_complete);
|
|
|
|
if (f == g) {
|
|
return f;
|
|
}
|
|
if (f == MR_ROBDD_zero || g == MR_ROBDD_zero) {
|
|
return MR_ROBDD_zero;
|
|
}
|
|
|
|
MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_complete);
|
|
|
|
fvar = (f == MR_ROBDD_one) ? MR_ROBDD_MAXVAR : f->value;
|
|
gvar = (g == MR_ROBDD_one) ? MR_ROBDD_MAXVAR : g->value;
|
|
if (fvar == gvar) {
|
|
result = MR_ROBDD_make_node(fvar,
|
|
MR_ROBDD_complete_or(f->fa, g->tr,
|
|
MR_ROBDD_complete_or(f->tr, g->tr,
|
|
MR_ROBDD_complete(f->tr,g->fa))),
|
|
MR_ROBDD_complete(f->fa,g->fa));
|
|
} else if (fvar < gvar) {
|
|
MR_ROBDD_node *cfa = MR_ROBDD_complete(f->fa, g);
|
|
|
|
result = MR_ROBDD_make_node(fvar, MR_ROBDD_complete_or(f->tr, g, cfa),
|
|
cfa);
|
|
} else /* fvar > gvar */ {
|
|
MR_ROBDD_node *cfa = MR_ROBDD_complete(f, g->fa);
|
|
|
|
result = MR_ROBDD_make_node(gvar, MR_ROBDD_complete_or(f, g->tr, cfa),
|
|
cfa);
|
|
}
|
|
MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_complete);
|
|
return result;
|
|
}
|
|
|
|
MR_ROBDD_DECLARE_FN_COUNT(MR_ROBDD_upclose)
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_upclose(MR_ROBDD_node *f)
|
|
{
|
|
MR_ROBDD_node *utr, *ufa, *result;
|
|
MR_ROBDD_DECLARE_UNARY_CACHE_ENTRY
|
|
|
|
MR_ROBDD_COUNT_FN(MR_ROBDD_upclose);
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f;
|
|
}
|
|
MR_ROBDD_TRY_UNARY_CACHE(f, MR_ROBDD_upclose);
|
|
utr = MR_ROBDD_upclose(f->tr);
|
|
ufa = MR_ROBDD_upclose(f->fa);
|
|
result = MR_ROBDD_make_node(f->value, MR_ROBDD_complete_or(utr, ufa, utr),
|
|
ufa);
|
|
MR_ROBDD_UPDATE_UNARY_CACHE(f, result, MR_ROBDD_upclose);
|
|
return result;
|
|
}
|
|
|
|
/*
|
|
** MR_ROBDD_bin(f, g)
|
|
**
|
|
** We note that the set of Boolean functions of n variables is
|
|
** isomorphic to the powerset of the set of n variables. Thus we can
|
|
** use a Boolean function to represent a subset of the powerset. We
|
|
** choose to let the *absence* of a variable from the set be indicated
|
|
** by that variable being true in the boolean function.
|
|
**
|
|
** This function computes the set of all possible unions of sets from
|
|
** f and g.
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_bin(MR_ROBDD_node *f, MR_ROBDD_node *g)
|
|
{
|
|
if (f == MR_ROBDD_zero || g == MR_ROBDD_zero) {
|
|
return MR_ROBDD_zero;
|
|
} else if (f == MR_ROBDD_one) {
|
|
return MR_ROBDD_bin_univ(g);
|
|
} else if (g == MR_ROBDD_one) {
|
|
return MR_ROBDD_bin_univ(f);
|
|
} else {
|
|
MR_ROBDD_node *result;
|
|
MR_ROBDD_DECLARE_BIN_CACHE_ENTRY
|
|
|
|
MR_ROBDD_TRY_BIN_CACHE(f, g, MR_ROBDD_bin);
|
|
|
|
if (f->value == g->value) {
|
|
MR_ROBDD_node *th = MR_ROBDD_bin(f->tr, g->tr);
|
|
MR_ROBDD_node *el = MR_ROBDD_bin(f->tr, g->fa);
|
|
|
|
if (el != MR_ROBDD_one) {
|
|
el = MR_ROBDD_lub(el, MR_ROBDD_bin(f->fa, g->tr));
|
|
if (el != MR_ROBDD_one) {
|
|
el = MR_ROBDD_lub(el, MR_ROBDD_bin(f->fa, g->fa));
|
|
}
|
|
}
|
|
result = MR_ROBDD_make_node(f->value, th, el);
|
|
} else {
|
|
MR_ROBDD_node *tmp;
|
|
|
|
if (f->value > g->value) {
|
|
tmp = f; f = g; g = tmp;
|
|
}
|
|
/* now f->value < g->value */
|
|
tmp = MR_ROBDD_bin(f->tr, g);
|
|
if (tmp == MR_ROBDD_one)
|
|
return MR_ROBDD_one;
|
|
result = MR_ROBDD_make_node(f->value, tmp,
|
|
MR_ROBDD_lub(tmp, MR_ROBDD_bin(f->fa, g)));
|
|
}
|
|
MR_ROBDD_UPDATE_BIN_CACHE(f, g, result, MR_ROBDD_bin);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
/*
|
|
** Auxilliary function for MR_ROBDD_bin: special case code for
|
|
** MR_ROBDD_bin(f, MR_ROBDD_one).
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_bin_univ(MR_ROBDD_node *f)
|
|
{
|
|
MR_ROBDD_node *g;
|
|
|
|
if (MR_ROBDD_IS_TERMINAL(f)) {
|
|
return f;
|
|
}
|
|
g = MR_ROBDD_bin_univ(f->tr);
|
|
if (g == MR_ROBDD_one) {
|
|
return MR_ROBDD_one;
|
|
}
|
|
return MR_ROBDD_make_node(f->value, g,
|
|
MR_ROBDD_lub(g, MR_ROBDD_bin_univ(f->fa)));
|
|
}
|
|
|
|
#endif /* MR_ROBDD_SHARING */
|
|
|
|
/****************************************************************
|
|
|
|
Initialization and Cleanup
|
|
|
|
****************************************************************/
|
|
|
|
#if defined(MR_ROBDD_STATISTICS)
|
|
|
|
void
|
|
MR_ROBDD_print_distribution(int array[], int MR_ROBDD_max)
|
|
{
|
|
int count;
|
|
int sum;
|
|
int total, zero_count;
|
|
|
|
for (count=0, total=0; count<=MR_ROBDD_max; ++count) {
|
|
total += array[count];
|
|
}
|
|
zero_count = array[0];
|
|
for (count=0, sum=0; count<=MR_ROBDD_max; ++count) {
|
|
if (array[count] > 0) {
|
|
sum += array[count];
|
|
printf(
|
|
"%5d nodes:%6d %5.2f%% (cum = %6d %5.1f%%, >0 = %6d %5.1f%%)\n",
|
|
count, array[count], MR_ROBDD_PERCENTAGE(array[count],total),
|
|
sum, MR_ROBDD_PERCENTAGE(sum,total), sum-zero_count,
|
|
total == zero_count ? 999.999
|
|
: MR_ROBDD_PERCENTAGE(sum-zero_count, total-zero_count));
|
|
}
|
|
}
|
|
if (array[MR_ROBDD_max+1] > 0) {
|
|
printf(">%4d nodes:%6d %2.2f%%\n",
|
|
MR_ROBDD_max, array[MR_ROBDD_max],
|
|
MR_ROBDD_PERCENTAGE(array[MR_ROBDD_max],total));
|
|
}
|
|
printf("\n");
|
|
}
|
|
#endif /* MR_ROBDD_STATISTICS */
|
|
|
|
void
|
|
MR_ROBDD_initRep(void)
|
|
{
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_make_node);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_variableRep);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_implies);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_lub);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_glb);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_restrict);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_restrictThresh);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_renameArray);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_reverseRenameArray);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_ite);
|
|
#if defined(MR_ROBDD_USE_ITE_CONSTANT)
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_ite_constant);
|
|
#endif /* MR_ROBDD_USE_ITE_CONSTANT */
|
|
MR_ROBDD_INIT_FN_COUNT(iff_conj);
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_ite_var);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_vars_entailed);
|
|
#endif
|
|
#if defined(MR_ROBDD_SHARING)
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete_one_or);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete_one);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete_or);
|
|
#endif /* MR_ROBDD_NEW */
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_complete);
|
|
MR_ROBDD_INIT_FN_COUNT(MR_ROBDD_upclose);
|
|
#endif /* MR_ROBDD_SHARING */
|
|
/*
|
|
** This code clears the unique table and all the computed
|
|
** caches. This should make it possible to time repeated
|
|
** execution of computations without the effect that after the
|
|
** first time the appropriate cache will probably hold the
|
|
** right result, so after the first time through the timing is
|
|
** useless. Even if this isn't the case, after the first time
|
|
** performing a computation no new nodes will ever be created
|
|
** because they will already exist in the unique table.
|
|
**
|
|
** After this, all old pointers to ROBDDs *must* be forgotten,
|
|
** because we free all allocated nodes, thus giving us a fresh
|
|
** start.
|
|
*/
|
|
|
|
MR_ROBDD_INIT_UNIQUE_TABLE;
|
|
|
|
MR_ROBDD_init_caches();
|
|
}
|
|
|
|
void
|
|
MR_ROBDD_init_caches(void)
|
|
{
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_ite);
|
|
#if defined(MR_ROBDD_USE_ITE_CONSTANT)
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_ite_constant);
|
|
#endif /* MR_ROBDD_USE_ITE_CONSTANT */
|
|
#if defined(MR_ROBDD_SHARING)
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_upclose);
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_bin);
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_complete);
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_complete_one);
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_complete_or);
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_complete_one_or);
|
|
#endif /* MR_ROBDD_NEW */
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_bin);
|
|
#endif /* MR_ROBDD_SHARING */
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_glb);
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_lub);
|
|
#if defined(MR_ROBDD_USE_RGLB)
|
|
MR_ROBDD_INIT_CACHE(rglb);
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_var_entailed);
|
|
#endif /* MR_ROBDD_USE_RGLB */
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_ite_var);
|
|
MR_ROBDD_INIT_CACHE(MR_ROBDD_vars_entailed);
|
|
#endif /* MR_ROBDD_NEW */
|
|
}
|
|
|
|
void
|
|
MR_ROBDD_concludeRep(void)
|
|
{
|
|
#if defined(MR_ROBDD_STATISTICS)
|
|
MR_ROBDD_node *ptr;
|
|
int size_count[MR_ROBDD_MAX_COUNT+2];
|
|
|
|
int i, count;
|
|
|
|
printf("\n\n\n================ Operation Counts ================\n\n");
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_make_node);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_variableRep);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_implies);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_lub);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_glb);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_restrict);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_restrictThresh);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_renameArray);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_reverseRenameArray);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_ite);
|
|
#if defined(MR_ROBDD_USE_ITE_CONSTANT)
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_ite_constant);
|
|
#endif /* MR_ROBDD_USE_ITE_CONSTANT */
|
|
MR_ROBDD_PRINT_FN_COUNT(iff_conj);
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_ite_var);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_vars_entailed);
|
|
#endif
|
|
#if defined(MR_ROBDD_SHARING)
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete_one_or);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete_one);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete_or);
|
|
#endif /* MR_ROBDD_NEW */
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_complete);
|
|
MR_ROBDD_PRINT_FN_COUNT(MR_ROBDD_upclose);
|
|
#endif /* MR_ROBDD_SHARING */
|
|
printf("\n================ Cache Performance ================\n\n");
|
|
printf("%d nodes extant\n\n", MR_ROBDD_nodes_in_use());
|
|
printf("Unique table: %d hits, %d misses, %f%% hits\n",
|
|
MR_ROBDD_unique_table_hits, MR_ROBDD_unique_table_misses,
|
|
MR_ROBDD_PERCENTAGE(MR_ROBDD_unique_table_hits,
|
|
MR_ROBDD_unique_table_hits+MR_ROBDD_unique_table_misses));
|
|
MR_memset(size_count, 0, sizeof(size_count));
|
|
for (i=0; i<MR_ROBDD_UNIQUE_TABLE_SIZE; ++i) {
|
|
count = 0;
|
|
ptr=MR_ROBDD_REVEAL_NODE_POINTER(MR_ROBDD_unique_table[i]);
|
|
while (ptr!=NULL) {
|
|
ptr=MR_ROBDD_REVEAL_NODE_POINTER(ptr->unique),++count;
|
|
}
|
|
++size_count[(count <= MR_ROBDD_MAX_COUNT
|
|
? count : MR_ROBDD_MAX_COUNT + 1)];
|
|
}
|
|
MR_ROBDD_print_distribution(size_count, MR_ROBDD_MAX_COUNT);
|
|
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_ite);
|
|
#if defined(MR_ROBDD_USE_ITE_CONSTANT)
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_ite_constant);
|
|
#endif /* MR_ROBDD_USE_ITE_CONSTANT */
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_lub);
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_glb);
|
|
#if defined(MR_ROBDD_SHARING)
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_upclose);
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete);
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete_or);
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete_one_or);
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_complete_one);
|
|
#endif /* MR_ROBDD_NEW */
|
|
#endif /* MR_ROBDD_SHARING */
|
|
#if defined(MR_ROBDD_USE_RGLB)
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(rglb);
|
|
#endif /* MR_ROBDD_USE_RGLB */
|
|
#if defined(MR_ROBDD_NEW)
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_ite_var);
|
|
MR_ROBDD_PRINT_CACHE_PERFORMANCE(MR_ROBDD_vars_entailed);
|
|
#endif /* MR_ROBDD_NEW */
|
|
#endif /* MR_ROBDD_STATISTICS */
|
|
}
|
|
|
|
/****************************************************************
|
|
|
|
Testing Support
|
|
|
|
****************************************************************/
|
|
|
|
/*
|
|
** special version of MR_ROBDD_iff_conj_array() that is the fast version
|
|
** no matter which options are selected. I hope this gives more reliable
|
|
** test times.
|
|
*/
|
|
|
|
MR_ROBDD_node *
|
|
MR_ROBDD_testing_iff_conj_array(int v0, int n, int arr[])
|
|
{
|
|
MR_ROBDD_node *thens = MR_ROBDD_one;
|
|
MR_ROBDD_node *elses = MR_ROBDD_zero;
|
|
int *ptr;
|
|
int vi;
|
|
|
|
/*
|
|
** first build part of graph below v0. For this, we build two
|
|
** subgraphs: MR_ROBDD_one for when v0 is true, and MR_ROBDD_one for false.
|
|
** These are called thens and elses.
|
|
**/
|
|
|
|
for (ptr=&arr[n-1]; ptr>=arr && v0<(vi=*ptr); --ptr) {
|
|
thens = MR_ROBDD_make_node(vi, thens, MR_ROBDD_zero);
|
|
elses = MR_ROBDD_make_node(vi, elses, MR_ROBDD_one);
|
|
}
|
|
|
|
/* make v0 MR_ROBDD_node */
|
|
thens = MR_ROBDD_make_node(v0,thens,elses);
|
|
|
|
/*
|
|
** Finally build part of graph above v0. For this, we build
|
|
** only MR_ROBDD_one graph, whose then branch is the graph we've built
|
|
** so far and whose else branch is ~v0.
|
|
*/
|
|
|
|
if (ptr >= arr) {
|
|
/* make ~v0 */
|
|
elses = MR_ROBDD_make_node(v0,MR_ROBDD_zero,MR_ROBDD_one);
|
|
|
|
do {
|
|
vi = *ptr;
|
|
thens = MR_ROBDD_make_node(vi, thens, elses);
|
|
} while (--ptr >= arr);
|
|
}
|
|
|
|
return thens;
|
|
}
|
|
|
|
static int MR_ROBDD_intcompare(const void *a, const void *b)
|
|
{
|
|
return (* ((int *) a) - * ((int *) b));
|
|
}
|