[buddy] Restrict the number of exported symbols.
* src/bdd.h, src/bvec.h, src/fdd.h: Declare all exported symbols using BUDDY_API, a new macro that sets visibility=default. * src/Makefile.am: Compile with -fvisibility=hidden by default, and compile the C++ part with -fvisibility-inlines-hidden as well.
This commit is contained in:
Alexandre Duret-Lutz
parent
9ed2d7a1dc
commit
b5710663f4
5 changed files with 269 additions and 216 deletions
|
|
@ -1,3 +1,12 @@
|
|||
2013-06-23 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
Restrict the number of exported symbols.
|
||||
|
||||
* src/bdd.hh, src/bvec.hh, src/fdd.hh: Declare all exported
|
||||
symbols using BUDDY_API, a new macro that sets visibility=default.
|
||||
* src/Makefile.am: Compile with -fvisibility=hidden by default,
|
||||
and compile the C++ part with -fvisibility-inlines-hidden as well.
|
||||
|
||||
2012-06-20 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
Fix the recent Automake workaround for VPATH builds.
|
||||
|
|
|
|||
|
|
@ -1,17 +1,29 @@
|
|||
# For
|
||||
AM_CPPFLAGS = -I$(top_builddir) -DVERSION=23
|
||||
|
||||
include_HEADERS = bdd.h fdd.h bvec.h
|
||||
|
||||
BUDDY_FLAGS = -I$(top_builddir) -DVERSION=23 \
|
||||
-fvisibility=hidden -DBUDDY_DLL_EXPORTS -DBUDDY_DLL
|
||||
|
||||
# Compile the C++ part of the library with
|
||||
# -fvisibility-inlines-hidden, this option is not valid for C.
|
||||
lib_LTLIBRARIES = libbdd.la
|
||||
libbdd_la_SOURCES = \
|
||||
libbdd_la_CPPFLAGS = $(BUDDY_FLAGS) -fvisibility-inlines-hidden
|
||||
libbdd_la_SOURCES = cppext.cxx
|
||||
libbdd_la_LIBADD = libbdd_c.la
|
||||
# See the `Updating version info' node of the Libtool manual before
|
||||
# changing this.
|
||||
libbdd_la_LDFLAGS = -no-undefined -version-info 0:0:0
|
||||
|
||||
# The C part of the library.
|
||||
noinst_LTLIBRARIES = libbdd_c.la
|
||||
libbdd_c_la_CPPFLAGS = $(BUDDY_FLAGS)
|
||||
libbdd_c_la_SOURCES = \
|
||||
bddio.c \
|
||||
bddop.c \
|
||||
bddtree.h \
|
||||
bvec.c \
|
||||
cache.c \
|
||||
cache.h \
|
||||
cppext.cxx \
|
||||
fdd.c \
|
||||
imatrix.c \
|
||||
imatrix.h \
|
||||
|
|
@ -23,10 +35,7 @@ libbdd_la_SOURCES = \
|
|||
reorder.c \
|
||||
tree.c
|
||||
|
||||
# See the `Updating version info' node of the Libtool manual before
|
||||
# changing this.
|
||||
libbdd_la_LDFLAGS = -no-undefined -version-info 0:0:0
|
||||
|
||||
check_PROGRAMS = bddtest
|
||||
bddtest_SOURCES = bddtest.cxx
|
||||
bddtest_CPPFLAGS = -I$(top_builddir)
|
||||
bddtest_LDADD = ./libbdd.la
|
||||
|
|
|
|||
328
buddy/src/bdd.h
328
buddy/src/bdd.h
|
|
@ -52,6 +52,38 @@
|
|||
#define __unlikely(expr) (expr)
|
||||
#endif
|
||||
|
||||
#if defined _WIN32 || defined __CYGWIN__
|
||||
#define BUDDY_HELPER_DLL_IMPORT __declspec(dllimport)
|
||||
#define BUDDY_HELPER_DLL_EXPORT __declspec(dllexport)
|
||||
#define BUDDY_HELPER_DLL_LOCAL
|
||||
#else
|
||||
#if __GNUC__ >= 4
|
||||
#define BUDDY_HELPER_DLL_IMPORT __attribute__ ((visibility ("default")))
|
||||
#define BUDDY_HELPER_DLL_EXPORT __attribute__ ((visibility ("default")))
|
||||
#define BUDDY_HELPER_DLL_LOCAL __attribute__ ((visibility ("hidden")))
|
||||
#else
|
||||
#define BUDDY_HELPER_DLL_IMPORT
|
||||
#define BUDDY_HELPER_DLL_EXPORT
|
||||
#define BUDDY_HELPER_DLL_LOCAL
|
||||
#endif
|
||||
#endif
|
||||
|
||||
// BUDDY_API is used for the public API symbols. It either DLL imports
|
||||
// or DLL exports (or does nothing for static build) BUDDY_LOCAL is
|
||||
// used for non-api symbols.
|
||||
#ifdef BUDDY_DLL
|
||||
#ifdef BUDDY_DLL_EXPORTS
|
||||
#define BUDDY_API BUDDY_HELPER_DLL_EXPORT
|
||||
#else
|
||||
#define BUDDY_API BUDDY_HELPER_DLL_IMPORT
|
||||
#endif
|
||||
#define BUDDY_LOCAL BUDDY_HELPER_DLL_LOCAL
|
||||
#else
|
||||
#define BUDDY_API
|
||||
#define BUDDY_LOCAL
|
||||
#endif
|
||||
#define BUDDY_API_VAR extern BUDDY_API
|
||||
|
||||
/* Allow this headerfile to define C++ constructs if requested */
|
||||
#ifdef __cplusplus
|
||||
#define CPLUSPLUS
|
||||
|
|
@ -235,149 +267,149 @@ typedef int (*bddsizehandler)(void);
|
|||
typedef void (*bddfilehandler)(FILE *, int);
|
||||
typedef void (*bddallsathandler)(char*, int);
|
||||
|
||||
extern bddinthandler bdd_error_hook(bddinthandler);
|
||||
extern bddgbchandler bdd_gbc_hook(bddgbchandler);
|
||||
extern bdd2inthandler bdd_resize_hook(bdd2inthandler);
|
||||
extern bddinthandler bdd_reorder_hook(bddinthandler);
|
||||
extern bddfilehandler bdd_file_hook(bddfilehandler);
|
||||
BUDDY_API bddinthandler bdd_error_hook(bddinthandler);
|
||||
BUDDY_API bddgbchandler bdd_gbc_hook(bddgbchandler);
|
||||
BUDDY_API bdd2inthandler bdd_resize_hook(bdd2inthandler);
|
||||
BUDDY_API bddinthandler bdd_reorder_hook(bddinthandler);
|
||||
BUDDY_API bddfilehandler bdd_file_hook(bddfilehandler);
|
||||
|
||||
extern int bdd_init(int, int);
|
||||
extern void bdd_done(void);
|
||||
extern int bdd_setvarnum(int);
|
||||
extern int bdd_extvarnum(int);
|
||||
extern int bdd_isrunning(void) __purefn;
|
||||
extern int bdd_setmaxnodenum(int);
|
||||
extern int bdd_setmaxincrease(int);
|
||||
extern int bdd_setminfreenodes(int);
|
||||
extern int bdd_getnodenum(void) __purefn;
|
||||
extern int bdd_getallocnum(void) __purefn;
|
||||
extern char* bdd_versionstr(void) __purefn;
|
||||
extern int bdd_versionnum(void) __constfn;
|
||||
extern void bdd_stats(bddStat *);
|
||||
extern void bdd_cachestats(bddCacheStat *);
|
||||
extern void bdd_fprintstat(FILE *);
|
||||
extern void bdd_printstat(void);
|
||||
extern void bdd_default_gbchandler(int, bddGbcStat *);
|
||||
extern void bdd_default_errhandler(int) __noreturnfn;
|
||||
extern const char *bdd_errstring(int) __constfn;
|
||||
extern void bdd_clear_error(void);
|
||||
BUDDY_API int bdd_init(int, int);
|
||||
BUDDY_API void bdd_done(void);
|
||||
BUDDY_API int bdd_setvarnum(int);
|
||||
BUDDY_API int bdd_extvarnum(int);
|
||||
BUDDY_API int bdd_isrunning(void) __purefn;
|
||||
BUDDY_API int bdd_setmaxnodenum(int);
|
||||
BUDDY_API int bdd_setmaxincrease(int);
|
||||
BUDDY_API int bdd_setminfreenodes(int);
|
||||
BUDDY_API int bdd_getnodenum(void) __purefn;
|
||||
BUDDY_API int bdd_getallocnum(void) __purefn;
|
||||
BUDDY_API char* bdd_versionstr(void) __purefn;
|
||||
BUDDY_API int bdd_versionnum(void) __constfn;
|
||||
BUDDY_API void bdd_stats(bddStat *);
|
||||
BUDDY_API void bdd_cachestats(bddCacheStat *);
|
||||
BUDDY_API void bdd_fprintstat(FILE *);
|
||||
BUDDY_API void bdd_printstat(void);
|
||||
BUDDY_API void bdd_default_gbchandler(int, bddGbcStat *);
|
||||
BUDDY_API void bdd_default_errhandler(int) __noreturnfn;
|
||||
BUDDY_API const char *bdd_errstring(int) __constfn;
|
||||
BUDDY_API void bdd_clear_error(void);
|
||||
#ifndef CPLUSPLUS
|
||||
extern BDD bdd_true(void) __constfn;
|
||||
extern BDD bdd_false(void) __constfn;
|
||||
BUDDY_API BDD bdd_true(void) __constfn;
|
||||
BUDDY_API BDD bdd_false(void) __constfn;
|
||||
#endif
|
||||
extern int bdd_varnum(void) __purefn;
|
||||
extern BDD bdd_ithvar(int) __purefn;
|
||||
extern BDD bdd_nithvar(int) __purefn;
|
||||
extern int bdd_var(BDD) __purefn;
|
||||
extern BDD bdd_low(BDD) __purefn;
|
||||
extern BDD bdd_high(BDD) __purefn;
|
||||
extern int bdd_varlevel(int) __purefn;
|
||||
extern BDD bdd_addref_nc(BDD);
|
||||
extern BDD bdd_addref(BDD);
|
||||
extern BDD bdd_delref_nc(BDD);
|
||||
extern BDD bdd_delref(BDD);
|
||||
extern void bdd_gbc(void);
|
||||
extern int bdd_scanset(BDD, int**, int*);
|
||||
extern BDD bdd_makeset(int *, int);
|
||||
extern bddPair* bdd_copypair(bddPair*);
|
||||
extern bddPair* bdd_mergepairs(bddPair*, bddPair*);
|
||||
extern bddPair* bdd_newpair(void);
|
||||
extern int bdd_setpair(bddPair*, int, int);
|
||||
extern int bdd_setpairs(bddPair*, int*, int*, int);
|
||||
extern int bdd_setbddpair(bddPair*, int, BDD);
|
||||
extern int bdd_setbddpairs(bddPair*, int*, BDD*, int);
|
||||
extern void bdd_resetpair(bddPair *);
|
||||
extern void bdd_freepair(bddPair*);
|
||||
BUDDY_API int bdd_varnum(void) __purefn;
|
||||
BUDDY_API BDD bdd_ithvar(int) __purefn;
|
||||
BUDDY_API BDD bdd_nithvar(int) __purefn;
|
||||
BUDDY_API int bdd_var(BDD) __purefn;
|
||||
BUDDY_API BDD bdd_low(BDD) __purefn;
|
||||
BUDDY_API BDD bdd_high(BDD) __purefn;
|
||||
BUDDY_API int bdd_varlevel(int) __purefn;
|
||||
BUDDY_API BDD bdd_addref_nc(BDD);
|
||||
BUDDY_API BDD bdd_addref(BDD);
|
||||
BUDDY_API BDD bdd_delref_nc(BDD);
|
||||
BUDDY_API BDD bdd_delref(BDD);
|
||||
BUDDY_API void bdd_gbc(void);
|
||||
BUDDY_API int bdd_scanset(BDD, int**, int*);
|
||||
BUDDY_API BDD bdd_makeset(int *, int);
|
||||
BUDDY_API bddPair* bdd_copypair(bddPair*);
|
||||
BUDDY_API bddPair* bdd_mergepairs(bddPair*, bddPair*);
|
||||
BUDDY_API bddPair* bdd_newpair(void);
|
||||
BUDDY_API int bdd_setpair(bddPair*, int, int);
|
||||
BUDDY_API int bdd_setpairs(bddPair*, int*, int*, int);
|
||||
BUDDY_API int bdd_setbddpair(bddPair*, int, BDD);
|
||||
BUDDY_API int bdd_setbddpairs(bddPair*, int*, BDD*, int);
|
||||
BUDDY_API void bdd_resetpair(bddPair *);
|
||||
BUDDY_API void bdd_freepair(bddPair*);
|
||||
|
||||
/* In bddop.c */
|
||||
|
||||
extern int bdd_setcacheratio(int);
|
||||
extern BDD bdd_buildcube(int, int, BDD *);
|
||||
extern BDD bdd_ibuildcube(int, int, int *);
|
||||
extern BDD bdd_not(BDD);
|
||||
extern BDD bdd_apply(BDD, BDD, int);
|
||||
extern BDD bdd_and(BDD, BDD);
|
||||
extern BDD bdd_or(BDD, BDD);
|
||||
extern BDD bdd_xor(BDD, BDD);
|
||||
extern BDD bdd_imp(BDD, BDD);
|
||||
extern BDD bdd_biimp(BDD, BDD);
|
||||
extern BDD bdd_setxor(BDD, BDD);
|
||||
extern int bdd_implies(BDD, BDD);
|
||||
extern BDD bdd_ite(BDD, BDD, BDD);
|
||||
extern BDD bdd_restrict(BDD, BDD);
|
||||
extern BDD bdd_constrain(BDD, BDD);
|
||||
extern BDD bdd_replace(BDD, bddPair*);
|
||||
extern BDD bdd_compose(BDD, BDD, BDD);
|
||||
extern BDD bdd_veccompose(BDD, bddPair*);
|
||||
extern BDD bdd_simplify(BDD, BDD);
|
||||
extern BDD bdd_exist(BDD, BDD);
|
||||
extern BDD bdd_existcomp(BDD, BDD);
|
||||
extern BDD bdd_forall(BDD, BDD);
|
||||
extern BDD bdd_forallcomp(BDD, BDD);
|
||||
extern BDD bdd_unique(BDD, BDD);
|
||||
extern BDD bdd_uniquecomp(BDD, BDD);
|
||||
extern BDD bdd_appex(BDD, BDD, int, BDD);
|
||||
extern BDD bdd_appexcomp(BDD, BDD, int, BDD);
|
||||
extern BDD bdd_appall(BDD, BDD, int, BDD);
|
||||
extern BDD bdd_appallcomp(BDD, BDD, int, BDD);
|
||||
extern BDD bdd_appuni(BDD, BDD, int, BDD);
|
||||
extern BDD bdd_appunicomp(BDD, BDD, int, BDD);
|
||||
extern BDD bdd_support(BDD);
|
||||
extern BDD bdd_satone(BDD);
|
||||
extern BDD bdd_satoneset(BDD, BDD, BDD);
|
||||
extern BDD bdd_fullsatone(BDD);
|
||||
extern BDD bdd_satprefix(BDD *);
|
||||
extern void bdd_allsat(BDD r, bddallsathandler handler);
|
||||
extern double bdd_satcount(BDD);
|
||||
extern double bdd_satcountset(BDD, BDD);
|
||||
extern double bdd_satcountln(BDD);
|
||||
extern double bdd_satcountlnset(BDD, BDD);
|
||||
extern int bdd_nodecount(BDD);
|
||||
extern int bdd_anodecount(BDD *, int);
|
||||
extern int* bdd_varprofile(BDD);
|
||||
extern double bdd_pathcount(BDD);
|
||||
BUDDY_API int bdd_setcacheratio(int);
|
||||
BUDDY_API BDD bdd_buildcube(int, int, BDD *);
|
||||
BUDDY_API BDD bdd_ibuildcube(int, int, int *);
|
||||
BUDDY_API BDD bdd_not(BDD);
|
||||
BUDDY_API BDD bdd_apply(BDD, BDD, int);
|
||||
BUDDY_API BDD bdd_and(BDD, BDD);
|
||||
BUDDY_API BDD bdd_or(BDD, BDD);
|
||||
BUDDY_API BDD bdd_xor(BDD, BDD);
|
||||
BUDDY_API BDD bdd_imp(BDD, BDD);
|
||||
BUDDY_API BDD bdd_biimp(BDD, BDD);
|
||||
BUDDY_API BDD bdd_setxor(BDD, BDD);
|
||||
BUDDY_API int bdd_implies(BDD, BDD);
|
||||
BUDDY_API BDD bdd_ite(BDD, BDD, BDD);
|
||||
BUDDY_API BDD bdd_restrict(BDD, BDD);
|
||||
BUDDY_API BDD bdd_constrain(BDD, BDD);
|
||||
BUDDY_API BDD bdd_replace(BDD, bddPair*);
|
||||
BUDDY_API BDD bdd_compose(BDD, BDD, BDD);
|
||||
BUDDY_API BDD bdd_veccompose(BDD, bddPair*);
|
||||
BUDDY_API BDD bdd_simplify(BDD, BDD);
|
||||
BUDDY_API BDD bdd_exist(BDD, BDD);
|
||||
BUDDY_API BDD bdd_existcomp(BDD, BDD);
|
||||
BUDDY_API BDD bdd_forall(BDD, BDD);
|
||||
BUDDY_API BDD bdd_forallcomp(BDD, BDD);
|
||||
BUDDY_API BDD bdd_unique(BDD, BDD);
|
||||
BUDDY_API BDD bdd_uniquecomp(BDD, BDD);
|
||||
BUDDY_API BDD bdd_appex(BDD, BDD, int, BDD);
|
||||
BUDDY_API BDD bdd_appexcomp(BDD, BDD, int, BDD);
|
||||
BUDDY_API BDD bdd_appall(BDD, BDD, int, BDD);
|
||||
BUDDY_API BDD bdd_appallcomp(BDD, BDD, int, BDD);
|
||||
BUDDY_API BDD bdd_appuni(BDD, BDD, int, BDD);
|
||||
BUDDY_API BDD bdd_appunicomp(BDD, BDD, int, BDD);
|
||||
BUDDY_API BDD bdd_support(BDD);
|
||||
BUDDY_API BDD bdd_satone(BDD);
|
||||
BUDDY_API BDD bdd_satoneset(BDD, BDD, BDD);
|
||||
BUDDY_API BDD bdd_fullsatone(BDD);
|
||||
BUDDY_API BDD bdd_satprefix(BDD *);
|
||||
BUDDY_API void bdd_allsat(BDD r, bddallsathandler handler);
|
||||
BUDDY_API double bdd_satcount(BDD);
|
||||
BUDDY_API double bdd_satcountset(BDD, BDD);
|
||||
BUDDY_API double bdd_satcountln(BDD);
|
||||
BUDDY_API double bdd_satcountlnset(BDD, BDD);
|
||||
BUDDY_API int bdd_nodecount(BDD);
|
||||
BUDDY_API int bdd_anodecount(BDD *, int);
|
||||
BUDDY_API int* bdd_varprofile(BDD);
|
||||
BUDDY_API double bdd_pathcount(BDD);
|
||||
|
||||
|
||||
/* In file "bddio.c" */
|
||||
|
||||
extern void bdd_printall(void);
|
||||
extern void bdd_fprintall(FILE *);
|
||||
extern void bdd_fprinttable(FILE *, BDD);
|
||||
extern void bdd_printtable(BDD);
|
||||
extern void bdd_fprintset(FILE *, BDD);
|
||||
extern void bdd_printset(BDD);
|
||||
extern int bdd_fnprintdot(char *, BDD);
|
||||
extern void bdd_fprintdot(FILE *, BDD);
|
||||
extern void bdd_printdot(BDD);
|
||||
extern int bdd_fnsave(char *, BDD);
|
||||
extern int bdd_save(FILE *, BDD);
|
||||
extern int bdd_fnload(char *, BDD *);
|
||||
extern int bdd_load(FILE *ifile, BDD *);
|
||||
BUDDY_API void bdd_printall(void);
|
||||
BUDDY_API void bdd_fprintall(FILE *);
|
||||
BUDDY_API void bdd_fprinttable(FILE *, BDD);
|
||||
BUDDY_API void bdd_printtable(BDD);
|
||||
BUDDY_API void bdd_fprintset(FILE *, BDD);
|
||||
BUDDY_API void bdd_printset(BDD);
|
||||
BUDDY_API int bdd_fnprintdot(char *, BDD);
|
||||
BUDDY_API void bdd_fprintdot(FILE *, BDD);
|
||||
BUDDY_API void bdd_printdot(BDD);
|
||||
BUDDY_API int bdd_fnsave(char *, BDD);
|
||||
BUDDY_API int bdd_save(FILE *, BDD);
|
||||
BUDDY_API int bdd_fnload(char *, BDD *);
|
||||
BUDDY_API int bdd_load(FILE *ifile, BDD *);
|
||||
|
||||
/* In file reorder.c */
|
||||
|
||||
extern int bdd_swapvar(int v1, int v2);
|
||||
extern void bdd_default_reohandler(int);
|
||||
extern void bdd_reorder(int);
|
||||
extern int bdd_reorder_gain(void) __purefn;
|
||||
extern bddsizehandler bdd_reorder_probe(bddsizehandler);
|
||||
extern void bdd_clrvarblocks(void);
|
||||
extern int bdd_addvarblock(BDD, int);
|
||||
extern int bdd_intaddvarblock(int, int, int);
|
||||
extern void bdd_varblockall(void);
|
||||
extern bddfilehandler bdd_blockfile_hook(bddfilehandler);
|
||||
extern int bdd_autoreorder(int);
|
||||
extern int bdd_autoreorder_times(int, int);
|
||||
extern int bdd_var2level(int);
|
||||
extern int bdd_level2var(int);
|
||||
extern int bdd_getreorder_times(void) __purefn;
|
||||
extern int bdd_getreorder_method(void) __purefn;
|
||||
extern void bdd_enable_reorder(void);
|
||||
extern void bdd_disable_reorder(void);
|
||||
extern int bdd_reorder_verbose(int);
|
||||
extern void bdd_setvarorder(int *);
|
||||
extern void bdd_printorder(void);
|
||||
extern void bdd_fprintorder(FILE *);
|
||||
BUDDY_API int bdd_swapvar(int v1, int v2);
|
||||
BUDDY_API void bdd_default_reohandler(int);
|
||||
BUDDY_API void bdd_reorder(int);
|
||||
BUDDY_API int bdd_reorder_gain(void) __purefn;
|
||||
BUDDY_API bddsizehandler bdd_reorder_probe(bddsizehandler);
|
||||
BUDDY_API void bdd_clrvarblocks(void);
|
||||
BUDDY_API int bdd_addvarblock(BDD, int);
|
||||
BUDDY_API int bdd_intaddvarblock(int, int, int);
|
||||
BUDDY_API void bdd_varblockall(void);
|
||||
BUDDY_API bddfilehandler bdd_blockfile_hook(bddfilehandler);
|
||||
BUDDY_API int bdd_autoreorder(int);
|
||||
BUDDY_API int bdd_autoreorder_times(int, int);
|
||||
BUDDY_API int bdd_var2level(int);
|
||||
BUDDY_API int bdd_level2var(int);
|
||||
BUDDY_API int bdd_getreorder_times(void) __purefn;
|
||||
BUDDY_API int bdd_getreorder_method(void) __purefn;
|
||||
BUDDY_API void bdd_enable_reorder(void);
|
||||
BUDDY_API void bdd_disable_reorder(void);
|
||||
BUDDY_API int bdd_reorder_verbose(int);
|
||||
BUDDY_API void bdd_setvarorder(int *);
|
||||
BUDDY_API void bdd_printorder(void);
|
||||
BUDDY_API void bdd_fprintorder(FILE *);
|
||||
|
||||
#ifdef CPLUSPLUS
|
||||
}
|
||||
|
|
@ -388,8 +420,8 @@ extern void bdd_fprintorder(FILE *);
|
|||
|
||||
#ifndef CPLUSPLUS
|
||||
|
||||
extern const BDD bddfalse;
|
||||
extern const BDD bddtrue;
|
||||
BUDDY_API_VAR const BDD bddfalse;
|
||||
BUDDY_API_VAR const BDD bddtrue;
|
||||
|
||||
#endif /* CPLUSPLUS */
|
||||
|
||||
|
|
@ -449,9 +481,9 @@ extern const BDD bddtrue;
|
|||
|
||||
/*=== User BDD class ===================================================*/
|
||||
|
||||
class bvec;
|
||||
class BUDDY_API bvec;
|
||||
|
||||
class bdd
|
||||
class BUDDY_API bdd
|
||||
{
|
||||
public:
|
||||
|
||||
|
|
@ -588,15 +620,15 @@ private:
|
|||
|
||||
/*=== BDD constants ====================================================*/
|
||||
|
||||
extern const bdd bddfalsepp;
|
||||
extern const bdd bddtruepp;
|
||||
BUDDY_API_VAR const bdd bddfalsepp;
|
||||
BUDDY_API_VAR const bdd bddtruepp;
|
||||
|
||||
#define bddtrue bddtruepp
|
||||
#define bddfalse bddfalsepp
|
||||
|
||||
/*=== C++ interface ====================================================*/
|
||||
|
||||
extern int bdd_cpp_init(int, int);
|
||||
BUDDY_API int bdd_cpp_init(int, int);
|
||||
|
||||
inline void bdd_stats(bddStat& s)
|
||||
{ bdd_stats(&s); }
|
||||
|
|
@ -891,31 +923,31 @@ inline bdd bdd_false(void)
|
|||
|
||||
/*=== Iostream printing ================================================*/
|
||||
|
||||
class bdd_ioformat
|
||||
class BUDDY_API bdd_ioformat
|
||||
{
|
||||
public:
|
||||
bdd_ioformat(int f) { format=f; }
|
||||
private:
|
||||
bdd_ioformat(void) { }
|
||||
BUDDY_LOCAL bdd_ioformat(void) { }
|
||||
int format;
|
||||
static int curformat;
|
||||
BUDDY_LOCAL static int curformat;
|
||||
|
||||
friend std::ostream &operator<<(std::ostream &, const bdd_ioformat &);
|
||||
friend std::ostream &operator<<(std::ostream &, const bdd &);
|
||||
};
|
||||
|
||||
std::ostream &operator<<(std::ostream &, const bdd &);
|
||||
std::ostream &operator<<(std::ostream &, const bdd_ioformat &);
|
||||
BUDDY_API std::ostream &operator<<(std::ostream &, const bdd &);
|
||||
BUDDY_API std::ostream &operator<<(std::ostream &, const bdd_ioformat &);
|
||||
|
||||
extern bdd_ioformat bddset;
|
||||
extern bdd_ioformat bddtable;
|
||||
extern bdd_ioformat bdddot;
|
||||
extern bdd_ioformat bddall;
|
||||
extern bdd_ioformat fddset;
|
||||
BUDDY_API_VAR bdd_ioformat bddset;
|
||||
BUDDY_API_VAR bdd_ioformat bddtable;
|
||||
BUDDY_API_VAR bdd_ioformat bdddot;
|
||||
BUDDY_API_VAR bdd_ioformat bddall;
|
||||
BUDDY_API_VAR bdd_ioformat fddset;
|
||||
|
||||
typedef void (*bddstrmhandler)(std::ostream &, int);
|
||||
|
||||
extern bddstrmhandler bdd_strm_hook(bddstrmhandler);
|
||||
BUDDY_API bddstrmhandler bdd_strm_hook(bddstrmhandler);
|
||||
|
||||
#endif /* CPLUSPLUS */
|
||||
|
||||
|
|
|
|||
|
|
@ -74,39 +74,39 @@ extern "C" {
|
|||
#endif
|
||||
|
||||
/* Prototypes for bvec.c */
|
||||
extern BVEC bvec_copy(BVEC v);
|
||||
extern BVEC bvec_true(int bitnum);
|
||||
extern BVEC bvec_false(int bitnum);
|
||||
extern BVEC bvec_con(int bitnum, int val);
|
||||
extern BVEC bvec_var(int bitnum, int offset, int step);
|
||||
extern BVEC bvec_varfdd(int var);
|
||||
extern BVEC bvec_varvec(int bitnum, int *var);
|
||||
extern BVEC bvec_coerce(int bitnum, BVEC v);
|
||||
extern int bvec_isconst(BVEC e) __purefn;
|
||||
extern int bvec_val(BVEC e) __purefn;
|
||||
extern void bvec_free(BVEC v);
|
||||
extern BVEC bvec_addref(BVEC v);
|
||||
extern BVEC bvec_delref(BVEC v);
|
||||
extern BVEC bvec_map1(BVEC a, BDD (*fun)(BDD));
|
||||
extern BVEC bvec_map2(BVEC a, BVEC b, BDD (*fun)(BDD,BDD));
|
||||
extern BVEC bvec_map3(BVEC a, BVEC b, BVEC c, BDD (*fun)(BDD,BDD,BDD));
|
||||
extern BVEC bvec_add(BVEC left, BVEC right);
|
||||
extern BVEC bvec_sub(BVEC left, BVEC right);
|
||||
extern BVEC bvec_mulfixed(BVEC e, int c);
|
||||
extern BVEC bvec_mul(BVEC left, BVEC right);
|
||||
extern int bvec_divfixed(BVEC e, int c, BVEC *res, BVEC *rem);
|
||||
extern int bvec_div(BVEC left, BVEC right, BVEC *res, BVEC *rem);
|
||||
extern BVEC bvec_ite(BDD a, BVEC b, BVEC c);
|
||||
extern BVEC bvec_shlfixed(BVEC e, int pos, BDD c);
|
||||
extern BVEC bvec_shl(BVEC l, BVEC r, BDD c);
|
||||
extern BVEC bvec_shrfixed(BVEC e, int pos, BDD c);
|
||||
extern BVEC bvec_shr(BVEC l, BVEC r, BDD c);
|
||||
extern BDD bvec_lth(BVEC left, BVEC right);
|
||||
extern BDD bvec_lte(BVEC left, BVEC right);
|
||||
extern BDD bvec_gth(BVEC left, BVEC right);
|
||||
extern BDD bvec_gte(BVEC left, BVEC right);
|
||||
extern BDD bvec_equ(BVEC left, BVEC right);
|
||||
extern BDD bvec_neq(BVEC left, BVEC right);
|
||||
BUDDY_API BVEC bvec_copy(BVEC v);
|
||||
BUDDY_API BVEC bvec_true(int bitnum);
|
||||
BUDDY_API BVEC bvec_false(int bitnum);
|
||||
BUDDY_API BVEC bvec_con(int bitnum, int val);
|
||||
BUDDY_API BVEC bvec_var(int bitnum, int offset, int step);
|
||||
BUDDY_API BVEC bvec_varfdd(int var);
|
||||
BUDDY_API BVEC bvec_varvec(int bitnum, int *var);
|
||||
BUDDY_API BVEC bvec_coerce(int bitnum, BVEC v);
|
||||
BUDDY_API int bvec_isconst(BVEC e) __purefn;
|
||||
BUDDY_API int bvec_val(BVEC e) __purefn;
|
||||
BUDDY_API void bvec_free(BVEC v);
|
||||
BUDDY_API BVEC bvec_addref(BVEC v);
|
||||
BUDDY_API BVEC bvec_delref(BVEC v);
|
||||
BUDDY_API BVEC bvec_map1(BVEC a, BDD (*fun)(BDD));
|
||||
BUDDY_API BVEC bvec_map2(BVEC a, BVEC b, BDD (*fun)(BDD,BDD));
|
||||
BUDDY_API BVEC bvec_map3(BVEC a, BVEC b, BVEC c, BDD (*fun)(BDD,BDD,BDD));
|
||||
BUDDY_API BVEC bvec_add(BVEC left, BVEC right);
|
||||
BUDDY_API BVEC bvec_sub(BVEC left, BVEC right);
|
||||
BUDDY_API BVEC bvec_mulfixed(BVEC e, int c);
|
||||
BUDDY_API BVEC bvec_mul(BVEC left, BVEC right);
|
||||
BUDDY_API int bvec_divfixed(BVEC e, int c, BVEC *res, BVEC *rem);
|
||||
BUDDY_API int bvec_div(BVEC left, BVEC right, BVEC *res, BVEC *rem);
|
||||
BUDDY_API BVEC bvec_ite(BDD a, BVEC b, BVEC c);
|
||||
BUDDY_API BVEC bvec_shlfixed(BVEC e, int pos, BDD c);
|
||||
BUDDY_API BVEC bvec_shl(BVEC l, BVEC r, BDD c);
|
||||
BUDDY_API BVEC bvec_shrfixed(BVEC e, int pos, BDD c);
|
||||
BUDDY_API BVEC bvec_shr(BVEC l, BVEC r, BDD c);
|
||||
BUDDY_API BDD bvec_lth(BVEC left, BVEC right);
|
||||
BUDDY_API BDD bvec_lte(BVEC left, BVEC right);
|
||||
BUDDY_API BDD bvec_gth(BVEC left, BVEC right);
|
||||
BUDDY_API BDD bvec_gte(BVEC left, BVEC right);
|
||||
BUDDY_API BDD bvec_equ(BVEC left, BVEC right);
|
||||
BUDDY_API BDD bvec_neq(BVEC left, BVEC right);
|
||||
|
||||
#ifdef CPLUSPLUS
|
||||
}
|
||||
|
|
@ -121,7 +121,7 @@ extern BDD bvec_neq(BVEC left, BVEC right);
|
|||
|
||||
/*=== User BVEC class ==================================================*/
|
||||
|
||||
class bvec
|
||||
class BUDDY_API bvec
|
||||
{
|
||||
public:
|
||||
|
||||
|
|
@ -152,10 +152,13 @@ private:
|
|||
friend int bvec_isconst(const bvec &e);
|
||||
friend int bvec_val(const bvec &e);
|
||||
friend bvec bvec_copy(const bvec &v);
|
||||
BUDDY_API
|
||||
friend bvec bvec_map1(const bvec &a,
|
||||
bdd (*fun)(const bdd &));
|
||||
BUDDY_API
|
||||
friend bvec bvec_map2(const bvec &a, const bvec &b,
|
||||
bdd (*fun)(const bdd &, const bdd &));
|
||||
BUDDY_API
|
||||
friend bvec bvec_map3(const bvec &a, const bvec &b, const bvec &c,
|
||||
bdd (*fun)(const bdd &, const bdd &, const bdd &));
|
||||
friend bvec bvec_add(const bvec &left, const bvec &right);
|
||||
|
|
@ -197,7 +200,7 @@ public:
|
|||
bdd operator!=(const bvec &a) const { return bvec_neq(*this, a); }
|
||||
};
|
||||
|
||||
std::ostream &operator<<(std::ostream &, const bvec &);
|
||||
BUDDY_API std::ostream &operator<<(std::ostream &, const bvec &);
|
||||
|
||||
inline bvec bvec_truepp(int bitnum)
|
||||
{ return bvec_true(bitnum); }
|
||||
|
|
|
|||
|
|
@ -47,30 +47,30 @@ extern "C" {
|
|||
|
||||
/* In file fdd.c */
|
||||
|
||||
extern int fdd_extdomain(int*, int);
|
||||
extern int fdd_overlapdomain(int, int);
|
||||
extern void fdd_clearall(void);
|
||||
extern int fdd_domainnum(void);
|
||||
extern int fdd_domainsize(int);
|
||||
extern int fdd_varnum(int);
|
||||
extern int* fdd_vars(int);
|
||||
extern BDD fdd_ithvar(int, int);
|
||||
extern int fdd_scanvar(BDD, int);
|
||||
extern int* fdd_scanallvar(BDD);
|
||||
extern BDD fdd_ithset(int);
|
||||
extern BDD fdd_domain(int);
|
||||
extern BDD fdd_equals(int, int);
|
||||
extern bddfilehandler fdd_file_hook(bddfilehandler);
|
||||
BUDDY_API int fdd_extdomain(int*, int);
|
||||
BUDDY_API int fdd_overlapdomain(int, int);
|
||||
BUDDY_API void fdd_clearall(void);
|
||||
BUDDY_API int fdd_domainnum(void);
|
||||
BUDDY_API int fdd_domainsize(int);
|
||||
BUDDY_API int fdd_varnum(int);
|
||||
BUDDY_API int* fdd_vars(int);
|
||||
BUDDY_API BDD fdd_ithvar(int, int);
|
||||
BUDDY_API int fdd_scanvar(BDD, int);
|
||||
BUDDY_API int* fdd_scanallvar(BDD);
|
||||
BUDDY_API BDD fdd_ithset(int);
|
||||
BUDDY_API BDD fdd_domain(int);
|
||||
BUDDY_API BDD fdd_equals(int, int);
|
||||
BUDDY_API bddfilehandler fdd_file_hook(bddfilehandler);
|
||||
#ifdef CPLUSPLUS
|
||||
extern bddstrmhandler fdd_strm_hook(bddstrmhandler);
|
||||
BUDDY_API bddstrmhandler fdd_strm_hook(bddstrmhandler);
|
||||
#endif
|
||||
extern void fdd_printset(BDD);
|
||||
extern void fdd_fprintset(FILE*, BDD);
|
||||
extern int fdd_scanset(BDD, int**, int*);
|
||||
extern BDD fdd_makeset(int*, int);
|
||||
extern int fdd_intaddvarblock(int, int, int);
|
||||
extern int fdd_setpair(bddPair*, int, int);
|
||||
extern int fdd_setpairs(bddPair*, int*, int*, int);
|
||||
BUDDY_API void fdd_printset(BDD);
|
||||
BUDDY_API void fdd_fprintset(FILE*, BDD);
|
||||
BUDDY_API int fdd_scanset(BDD, int**, int*);
|
||||
BUDDY_API BDD fdd_makeset(int*, int);
|
||||
BUDDY_API int fdd_intaddvarblock(int, int, int);
|
||||
BUDDY_API int fdd_setpair(bddPair*, int, int);
|
||||
BUDDY_API int fdd_setpairs(bddPair*, int*, int*, int);
|
||||
|
||||
#ifdef CPLUSPLUS
|
||||
}
|
||||
|
|
@ -121,8 +121,8 @@ inline bdd* fdd_conpp(int bitnum, int var)
|
|||
inline bdd* fdd_varpp(int bitnum, int var)
|
||||
{ return fdd_transfer( bitnum, fdd_var(bitnum, var) ); }
|
||||
|
||||
extern int fdd_isconst(int bitnum, bdd *e);
|
||||
extern int fdd_val(int bitnum, bdd *e);
|
||||
BUDDY_API int fdd_isconst(int bitnum, bdd *e);
|
||||
BUDDY_API int fdd_val(int bitnum, bdd *e);
|
||||
|
||||
inline bdd* fdd_add(int bitnum, bdd *left, bdd *right)
|
||||
{ return fdd_termopr(bitnum, left, right,bdd::fddAdd); }
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue