From 4d3d9c408d9630feaa9e9a1fe6fc4b21821a8fdf Mon Sep 17 00:00:00 2001 From: vscosta Date: Tue, 5 Apr 2016 02:52:50 +0100 Subject: [PATCH] adds --- Eclipse/packages/bdd/cudd_config.h | 32 - Eclipse/packages/raptor/raptor_config.h | 2 - Eclipse/packages/real/rconfig.h | 26 - .../library/system/sys_config.h | 2 +- {Eclipse => cmake}/os/YapIOConfig.h | 24 +- packages/bdd/cmake/FindCUDD.cmake | 183 --- packages/bdd/cudd.c | 585 ++++--- .../approx/simplecuddLPADs/simplecudd.c | 1368 ++++++++++------- .../approx/simplecuddLPADs/simplecudd.h | 149 +- packages/swig/android/JavaYap.java | 9 +- pl/boot.yap | 6 + 11 files changed, 1161 insertions(+), 1225 deletions(-) delete mode 100644 Eclipse/packages/bdd/cudd_config.h delete mode 100644 Eclipse/packages/raptor/raptor_config.h delete mode 100644 Eclipse/packages/real/rconfig.h rename {Eclipse => cmake}/library/system/sys_config.h (95%) rename {Eclipse => cmake}/os/YapIOConfig.h (85%) delete mode 100644 packages/bdd/cmake/FindCUDD.cmake diff --git a/Eclipse/packages/bdd/cudd_config.h b/Eclipse/packages/bdd/cudd_config.h deleted file mode 100644 index efdb27e2e..000000000 --- a/Eclipse/packages/bdd/cudd_config.h +++ /dev/null @@ -1,32 +0,0 @@ -// cmake template file - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_CUDDINT_H -/* #undef HAVE_CUDDINT_H */ -#endif - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_CUDD_CUDDINT_H -#define HAVE_CUDD_CUDDINT_H 1 -#endif - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_CUDD_CUDD_H -#define HAVE_CUDD_CUDD_H 1 -#endif - -/*Define to 1 if you have the header file. */ -#ifndef HAVE_CUDD_H -/* #undef HAVE_CUDD_H */ -#endif - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_CUDD_UTIL_H -#define HAVE_CUDD_UTIL_H 1 -#endif - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_UTIL_H -#define HAVE_UTIL_H 1 -#endif - diff --git a/Eclipse/packages/raptor/raptor_config.h b/Eclipse/packages/raptor/raptor_config.h deleted file mode 100644 index e8ac59e6c..000000000 --- a/Eclipse/packages/raptor/raptor_config.h +++ /dev/null @@ -1,2 +0,0 @@ -#define HAVE_RAPTOR2_RAPTOR2_H 1 -/* #undef HAVE_RAPTOR_H */ diff --git a/Eclipse/packages/real/rconfig.h b/Eclipse/packages/real/rconfig.h deleted file mode 100644 index e6f63dbbe..000000000 --- a/Eclipse/packages/real/rconfig.h +++ /dev/null @@ -1,26 +0,0 @@ -/*-------------------------------------------------------------------------- -* This file is autogenerated from rconfig.h.cmake -* during the cmake configuration of your project. If you need to make changes -* edit the original file NOT THIS FILE. -* --------------------------------------------------------------------------*/ -#ifndef RCONFIG_H -#define RCONFIG_H - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_R_H -#define HAVE_R_H 1 -#endif - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_R_EMBEDDED_H -#define HAVE_R_EMBEDDED_H 1 -#endif - -/* Define to 1 if you have the header file. */ -#ifndef HAVE_R_INTERFACE_H -#define HAVE_R_INTERFACE_H 1 -#endif - - -#endif - diff --git a/Eclipse/library/system/sys_config.h b/cmake/library/system/sys_config.h similarity index 95% rename from Eclipse/library/system/sys_config.h rename to cmake/library/system/sys_config.h index 17e29d49d..ace898575 100644 --- a/Eclipse/library/system/sys_config.h +++ b/cmake/library/system/sys_config.h @@ -5,7 +5,7 @@ /* Define to 1 if you have the header file. */ #ifndef HAVE_APR_1_APR_MD5_H -#define HAVE_APR_1_APR_MD5_H 1 +/* #undef HAVE_APR_1_APR_MD5_H */ #endif diff --git a/Eclipse/os/YapIOConfig.h b/cmake/os/YapIOConfig.h similarity index 85% rename from Eclipse/os/YapIOConfig.h rename to cmake/os/YapIOConfig.h index e59ba1707..6345636f0 100644 --- a/Eclipse/os/YapIOConfig.h +++ b/cmake/os/YapIOConfig.h @@ -1,16 +1,16 @@ /* Define if you have libreadline */ #ifndef HAVE_LIBREADLINE -#define HAVE_LIBREADLINE 1 +/* #undef HAVE_LIBREADLINE */ #endif /* Define to 1 if you have the header file. */ #ifndef HAVE_READLINE_HISTORY_H -#define HAVE_READLINE_HISTORY_H 1 +/* #undef HAVE_READLINE_HISTORY_H */ #endif /* Define to 1 if you have the header file. */ #ifndef HAVE_READLINE_READLINE_H -#define HAVE_READLINE_READLINE_H 1 +/* #undef HAVE_READLINE_READLINE_H */ #endif #if defined(HAVE_LIBREADLINE) && defined(HAVE_READLINE_READLINE_H) @@ -43,12 +43,12 @@ you don't. */ /* Define to 1 if you have the `rl_begin_undo_group' function. */ #ifndef HAVE_RL_BEGIN_UNDO_GROUP -#define HAVE_RL_BEGIN_UNDO_GROUP 1 +/* #undef HAVE_RL_BEGIN_UNDO_GROUP */ #endif /* Define to 1 if you have the `rl_clear_pending_input' function. */ #ifndef HAVE_RL_CLEAR_PENDING_INPUT -#define HAVE_RL_CLEAR_PENDING_INPUT 1 +/* #undef HAVE_RL_CLEAR_PENDING_INPUT */ #endif /* Define to 1 if the system has the type `rl_completion_func_t'). */ @@ -68,7 +68,7 @@ you don't. */ /* Define to 1 if you have the `rl_discard_argument' function. */ #ifndef HAVE_RL_DISCARD_ARGUMENT -#define HAVE_RL_DISCARD_ARGUMENT 1 +/* #undef HAVE_RL_DISCARD_ARGUMENT */ #endif /* Define to 1 if you have the `rl_done' variable. */ @@ -78,12 +78,12 @@ you don't. */ /* Define to 1 if you have the `rl_filename_completion_function' function. */ #ifndef HAVE_RL_FILENAME_COMPLETION_FUNCTION -#define HAVE_RL_FILENAME_COMPLETION_FUNCTION 1 +#define HAVE_RL_FILENAME_COMPLETION_FUNCTION #endif /* Define to 1 if you have the `rl_free_line_state' function. */ #ifndef HAVE_RL_FREE_LINE_STATE -#define HAVE_RL_FREE_LINE_STATE 1 +/* #undef HAVE_RL_FREE_LINE_STATE */ #endif /* Define to 1 if the system has the type `rl_hook_func_t'. */ @@ -93,20 +93,20 @@ you don't. */ /* Define to 1 if you have the `rl_insert_close' function. */ #ifndef HAVE_RL_INSERT_CLOSE -#define HAVE_RL_INSERT_CLOSE 1 +/* #undef HAVE_RL_INSERT_CLOSE */ #endif /* Define to 1 if you have the `rl_reset_after_signal' function. */ #ifndef HAVE_RL_RESET_AFTER_SIGNAL -#define HAVE_RL_RESET_AFTER_SIGNAL 1 +/* #undef HAVE_RL_RESET_AFTER_SIGNAL */ #endif /* Define to 1 if you have the `rl_set_keyboard_input_timeout' function. */ #ifndef HAVE_RL_SET_KEYBOARD_INPUT_TIMEOUT -#define HAVE_RL_SET_KEYBOARD_INPUT_TIMEOUT 1 +/* #undef HAVE_RL_SET_KEYBOARD_INPUT_TIMEOUT */ #endif /* Define to 1 if you have the `rl_set_prompt' function. */ #ifndef HAVE_RL_SET_PROMPT -#define HAVE_RL_SET_PROMPT 1 +/* #undef HAVE_RL_SET_PROMPT */ #endif diff --git a/packages/bdd/cmake/FindCUDD.cmake b/packages/bdd/cmake/FindCUDD.cmake deleted file mode 100644 index 99fe30be4..000000000 --- a/packages/bdd/cmake/FindCUDD.cmake +++ /dev/null @@ -1,183 +0,0 @@ -# - Try to find the CUD BDD RDF parsing library (http://librdf.org/CUDD /) -# Once done this will define -# -# CUDD_FOUND - system has CUDD -# CUDD_LIBRARIES - Link these to use CUDD -# CUDD_INCLUDE_DIR - Include directory for using CUDD -# -# -# Based on FindFontconfig Copyright (c) 2006,2007 Laurent Montel, -# -# Redistribution and use is allowed according to the terms of the BSD license. -# For details see the accompanying COPYING-CMAKE-SCRIPTS file. - - -MACRO ( FIND_CUDD ) - -ENDMACRO () - - - -# Check if we have cached results in case the last round was successful. -if ( NOT( CUDD_INCLUDE_DIR AND CUDD_LIBRARIES ) OR NOT CUDD_FOUND ) - - set( CUDD_LDFLAGS ) - - find_package(PkgConfig) - - - find_path(CUDD_INCLUDE_DIR - NAMES cudd.h cudd.cudd.h - $ENV{CUDD_DIR}/include - $ENV{CUDD_DIR} - /usr/local/yap/include - /usr/local/Yap/include - ~/Library/Frameworks - /Library/Frameworks - /usr/local/include - /usr/include/ - /sw/include # Fink - /opt/local/include # MacPorts - /opt/csw/include # Blastwave - /opt/include - /usr/freeware/include - NO_DEFAULT_PATHS - - ) - - find_path(CUDD_INCLUDE_DIR - NAMES cudd.h - ) - - find_library(CUDD_INTERFACE_LIBRARY - NAMES cudd - PATHS - $ENV{CUDD_DIR}/lib - $ENV{CUDD_DIR}/lib64 - $ENV{CUDD_DIR}/lib-dbg - $ENV{CUDD_DIR} - $ENV{CUDD_DIR}/cudd - /usr/local/yap/lib - /usr/local/Yap/lib - ~/Library/Frameworks - /Library/Frameworks - /usr/local/lib - /usr/local/lib64 - /usr/lib - /usr/lib64 - /usr/local/lib/cudd - /usr/local/lib64/cudd - /usr/lib/cudd - /usr/lib64/cudd - /usr/freeware/lib64 - ) - - if ( CUDD_INTERFACE_LIBRARY AND CUDD_INCLUDE_DIR ) - set( CUDD_FOUND ON ) - list( APPEND CUDD_LIBRARIES ${CUDD_INTERFACE_LIBRARY} ) - endif () - - find_library(CUDD_UTIL_LIBRARY - NAMES cuddutil util - PATHS - $ENV{CUDD_DIR}/lib - $ENV{CUDD_DIR}/lib64 - $ENV{CUDD_DIR}/lib-dbg - $ENV{CUDD_DIR} - $ENV{CUDD_DIR}/util - /usr/local/yap/lib - /usr/local/Yap/lib - ~/Library/Frameworks - /Library/Frameworks - /usr/local/lib - /usr/local/lib64 - /usr/lib - /usr/lib64 - /usr/local/lib/util - /usr/local/lib64/util - /usr/lib/util - /usr/lib64/util - /usr/freeware/lib64 - ) - - if ( CUDD_UTIL_LIBRARY ) - list( APPEND CUDD_LIBRARIES ${CUDD_UTIL_LIBRARY} ) - endif () - - find_library(CUDD_ST_LIBRARY - NAMES cuddst st - PATHS - $ENV{CUDD_DIR}/lib - $ENV{CUDD_DIR}/lib64 - $ENV{CUDD_DIR}/lib-dbg - $ENV{CUDD_DIR} - $ENV{CUDD_DIR}/st - /usr/local/yap/lib - /usr/local/Yap/lib - ~/Library/Frameworks - /Library/Frameworks - /usr/local/lib - /usr/local/lib64 - /usr/lib - /usr/lib64 - /usr/lib/st - /usr/lib64/st - /usr/freeware/lib64 - ) - - if ( CUDD_ST_LIBRARY ) - list( APPEND CUDD_LIBRARIES ${CUDD_ST_LIBRARY} ) - endif () - - find_library(CUDD_EPD_LIBRARY - NAMES epd - PATHS - $ENV{CUDD_DIR}/lib - $ENV{CUDD_DIR}/lib64 - $ENV{CUDD_DIR}/lib-dbg - $ENV{CUDD_DIR} - $ENV{CUDD_DIR}/epd - /usr/local/yap/lib - /usr/local/Yap/lib - ~/Library/Frameworks - /Library/Frameworks - /usr/local/lib - /usr/local/lib64 - /usr/lib - /usr/lib64 - /usr/lib/epd - /usr/lib64/epd - /usr/freeware/lib64 - ) - - if ( CUDD_MTR_LIBRARY ) - list( APPEND CUDD_LIBRARIES ${CUDD_MTR_LIBRARY} ) - endif () - - find_library(CUDD_MTR_LIBRARY - NAMES mtr - PATHS - $ENV{CUDD_DIR}/lib - $ENV{CUDD_DIR}/lib64 - $ENV{CUDD_DIR}/lib-dbg - $ENV{CUDD_DIR} - $ENV{CUDD_DIR}/mtr - /usr/local/yap/lib - /usr/local/Yap/lib - ~/Library/Frameworks - /Library/Frameworks - /usr/local/lib - /usr/local/lib64 - /usr/lib - /usr/lib64 - /usr/lib/mtr - /usr/lib64/mtr - /usr/freeware/lib64 - ) - - if ( CUDD_MTR_LIBRARY ) - list( APPEND CUDD_LIBRARIES ${CUDD_MTR_LIBRARY} ) - endif () - - -endif () # Check for cached values diff --git a/packages/bdd/cudd.c b/packages/bdd/cudd.c index 4bbfb7d2b..e92b13128 100644 --- a/packages/bdd/cudd.c +++ b/packages/bdd/cudd.c @@ -4,7 +4,10 @@ @brief Interface to the CUDD Library - CUDD represents a BDD as a tree of DdNode structures. Each tree has a manager DdManager and a list of booleaan variables, also represented as DdNode structures. Mapping from an Prolog tree to a ground BDD involves the following steps: + CUDD represents a BDD as a tree of DdNode structures. Each tree has a manager +DdManager and a list of booleaan variables, also represented as DdNode +structures. Mapping from an Prolog tree to a ground BDD involves the following +steps: 1. Collect all logical variables in the Prolog term, and map each variable $V$ to a boolean variable $i$ in the BDD. This is easily done @@ -37,9 +40,9 @@ CUDD will generate better/faster code. */ #include +#include "YapInterface.h" #include "config.h" #include "cudd_config.h" -#include "YapInterface.h" #if HAVE_CUDD_UTIL_H #include @@ -52,83 +55,59 @@ CUDD will generate better/faster code. #include "cudd.h" #endif -static YAP_Functor FunctorDollarVar, - FunctorCudd, - FunctorAnd, - FunctorAnd4, - FunctorOr, - FunctorOr4, - FunctorLAnd, - FunctorLOr, - FunctorNot, - FunctorMinus1, - FunctorXor, - FunctorNand, - FunctorNor, - FunctorTimes, - FunctorImplies, - FunctorPlus, - FunctorMinus, - FunctorTimes4, - FunctorPlus4, - FunctorOutAdd, - FunctorOutPos, - FunctorOutNeg; +static YAP_Functor FunctorDollarVar, FunctorCudd, FunctorAnd, FunctorAnd4, + FunctorOr, FunctorOr4, FunctorLAnd, FunctorLOr, FunctorNot, FunctorMinus1, + FunctorXor, FunctorNand, FunctorNor, FunctorTimes, FunctorImplies, + FunctorPlus, FunctorMinus, FunctorTimes4, FunctorPlus4, FunctorOutAdd, + FunctorOutPos, FunctorOutNeg; static YAP_Term TermMinusOne, TermZero, TermPlusOne, TermTrue, TermFalse; void init_cudd(void); -static DdNode * -cudd_and(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +static DdNode *cudd_and(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddAnd(manager, bdd1, bdd2); Cudd_Ref(tmp); return tmp; } -static DdNode * -cudd_nand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +static DdNode *cudd_nand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddNand(manager, bdd1, bdd2); Cudd_Ref(tmp); return tmp; } -static DdNode * -cudd_or(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +static DdNode *cudd_or(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddOr(manager, bdd1, bdd2); Cudd_Ref(tmp); return tmp; } -static DdNode * -cudd_nor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +static DdNode *cudd_nor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddNor(manager, bdd1, bdd2); Cudd_Ref(tmp); return tmp; } -static DdNode * -cudd_xor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +static DdNode *cudd_xor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddXor(manager, bdd1, bdd2); Cudd_Ref(tmp); return tmp; } -static DdNode * -term_to_cudd(DdManager *manager, YAP_Term t) -{ +static DdNode *term_to_cudd(DdManager *manager, YAP_Term t) { if (YAP_IsApplTerm(t)) { YAP_Functor f = YAP_FunctorOfTerm(t); if (f == FunctorDollarVar) { - int i = YAP_IntOfTerm(YAP_ArgOfTerm(1,t)); - DdNode *var = Cudd_bddIthVar(manager,i); + int i = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)); + DdNode *var = Cudd_bddIthVar(manager, i); if (!var) - return NULL; + return NULL; Cudd_Ref(var); return var; } else if (f == FunctorAnd || f == FunctorLAnd || f == FunctorTimes) { @@ -136,30 +115,30 @@ term_to_cudd(DdManager *manager, YAP_Term t) DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp; if (!x1 || !x2) - return NULL; + return NULL; tmp = cudd_and(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorAnd4) { YAP_Term t1 = YAP_ArgOfTerm(2, t); if (YAP_IsVarTerm(t1)) { - YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; - DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t)); - DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t)); - DdNode *tmp; - if (!x1 || !x2) - return NULL; - tmp = cudd_and(manager, x1, x2); - for (i=0 ; i < refs; i++) { - Cudd_Ref(tmp); - } - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); - YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); - return tmp; + YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; + DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t)); + DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t)); + DdNode *tmp; + if (!x1 || !x2) + return NULL; + tmp = cudd_and(manager, x1, x2); + for (i = 0; i < refs; i++) { + Cudd_Ref(tmp); + } + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); + YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); + return tmp; } else { - return (DdNode *)YAP_IntOfTerm(t1); + return (DdNode *)YAP_IntOfTerm(t1); } } else if (f == FunctorCudd) { YAP_Term t1 = YAP_ArgOfTerm(1, t); @@ -171,64 +150,64 @@ term_to_cudd(DdManager *manager, YAP_Term t) DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp; if (!x1 || !x2) - return NULL; + return NULL; tmp = cudd_or(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorXor) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp; if (!x1 || !x2) - return NULL; + return NULL; tmp = cudd_xor(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorOr4) { YAP_Term t1 = YAP_ArgOfTerm(2, t); if (YAP_IsVarTerm(t1)) { - YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; - DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t)); - DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t)); - DdNode *tmp; - if (!x1 || !x2) - return NULL; - tmp = cudd_or(manager, x1, x2); - for (i=0 ; i < refs; i++) { - Cudd_Ref(tmp); - } - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); - YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); - return tmp; + YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; + DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t)); + DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t)); + DdNode *tmp; + if (!x1 || !x2) + return NULL; + tmp = cudd_or(manager, x1, x2); + for (i = 0; i < refs; i++) { + Cudd_Ref(tmp); + } + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); + YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); + return tmp; } else { - return (DdNode *)YAP_IntOfTerm(t1); + return (DdNode *)YAP_IntOfTerm(t1); } } else if (f == FunctorNor) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp; if (!x1 || !x2) - return NULL; + return NULL; tmp = cudd_nor(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorNand) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); if (!x1 || !x2) - return NULL; + return NULL; DdNode *tmp = cudd_nand(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorNot || FunctorMinus1) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); if (!x1) - return NULL; + return NULL; return Cudd_Not(x1); } else { YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported operator in CUDD"); @@ -238,7 +217,7 @@ term_to_cudd(DdManager *manager, YAP_Term t) YAP_Int i = YAP_IntOfTerm(t); if (i == 0) return Cudd_ReadLogicZero(manager); - else if (i==1) + else if (i == 1) return Cudd_ReadOne(manager); else { YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD"); @@ -248,7 +227,7 @@ term_to_cudd(DdManager *manager, YAP_Term t) YAP_Int i = YAP_FloatOfTerm(t); if (i == 0.0) return Cudd_ReadLogicZero(manager); - else if (i==1.0) + else if (i == 1.0) return Cudd_ReadOne(manager); else { YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD"); @@ -260,10 +239,11 @@ term_to_cudd(DdManager *manager, YAP_Term t) else if (t == TermTrue) return Cudd_ReadOne(manager); else { - YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported atom %s in CUDD", YAP_AtomName(YAP_AtomOfTerm(t))); + YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported atom %s in CUDD", + YAP_AtomName(YAP_AtomOfTerm(t))); return NULL; } - } else if (YAP_IsVarTerm(t)) { + } else if (YAP_IsVarTerm(t)) { YAP_Error(INSTANTIATION_ERROR, t, "unsupported unbound term in CUDD"); return NULL; } @@ -271,15 +251,13 @@ term_to_cudd(DdManager *manager, YAP_Term t) return NULL; } -static YAP_Bool -p_term_to_cudd(void) -{ +static YAP_Bool p_term_to_cudd(void) { DdManager *manager; DdNode *t; if (YAP_IsVarTerm(YAP_ARG2)) { - manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); - //Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT); + manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); + // Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT); if (!YAP_Unify(YAP_ARG2, YAP_MkIntTerm((YAP_Int)manager))) return FALSE; } else { @@ -288,144 +266,131 @@ p_term_to_cudd(void) t = term_to_cudd(manager, YAP_ARG1); if (!t) return FALSE; - return - YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t)); + return YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t)); } -static DdNode * -add_times(DdManager *manager, DdNode *x1, DdNode *x2) -{ +static DdNode *add_times(DdManager *manager, DdNode *x1, DdNode *x2) { DdNode *tmp; - tmp = Cudd_addApply(manager,Cudd_addTimes,x2,x1); + tmp = Cudd_addApply(manager, Cudd_addTimes, x2, x1); Cudd_Ref(tmp); return tmp; } -static DdNode * -add_implies(DdManager *manager, DdNode *x1, DdNode *x2) -{ +static DdNode *add_implies(DdManager *manager, DdNode *x1, DdNode *x2) { DdNode *tmp; - tmp = Cudd_addConst(manager,Cudd_addLeq(manager,x1,x2)); + tmp = Cudd_addConst(manager, Cudd_addLeq(manager, x1, x2)); Cudd_Ref(tmp); return tmp; } -static DdNode * -add_plus(DdManager *manager, DdNode *x1, DdNode *x2) -{ +static DdNode *add_plus(DdManager *manager, DdNode *x1, DdNode *x2) { DdNode *tmp; - tmp = Cudd_addApply(manager,Cudd_addPlus,x2,x1); + tmp = Cudd_addApply(manager, Cudd_addPlus, x2, x1); Cudd_Ref(tmp); return tmp; } -static DdNode * -add_minus(DdManager *manager, DdNode *x1, DdNode *x2) -{ +static DdNode *add_minus(DdManager *manager, DdNode *x1, DdNode *x2) { DdNode *tmp; - tmp = Cudd_addApply(manager,Cudd_addMinus,x1,x2); + tmp = Cudd_addApply(manager, Cudd_addMinus, x1, x2); Cudd_Ref(tmp); return tmp; } -static DdNode * -add_lor(DdManager *manager, DdNode *x1, DdNode *x2) -{ +static DdNode *add_lor(DdManager *manager, DdNode *x1, DdNode *x2) { DdNode *tmp; - tmp = Cudd_addApply(manager,Cudd_addOr,x1,x2); + tmp = Cudd_addApply(manager, Cudd_addOr, x1, x2); Cudd_Ref(tmp); return tmp; } -static DdNode * -term_to_add(DdManager *manager, YAP_Term t) -{ +static DdNode *term_to_add(DdManager *manager, YAP_Term t) { if (YAP_IsApplTerm(t)) { YAP_Functor f = YAP_FunctorOfTerm(t); if (f == FunctorDollarVar) { - int i = YAP_IntOfTerm(YAP_ArgOfTerm(1,t)); - DdNode *var = Cudd_addIthVar(manager,i); + int i = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)); + DdNode *var = Cudd_addIthVar(manager, i); return var; } else if (f == FunctorTimes) { DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp = add_times(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorTimes4) { YAP_Term t1 = YAP_ArgOfTerm(2, t); if (YAP_IsVarTerm(t1)) { - YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; - DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(3, t)); - DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t)); - DdNode *tmp = add_times(manager, x1, x2); + YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; + DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(3, t)); + DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t)); + DdNode *tmp = add_times(manager, x1, x2); - for (i=0 ; i < refs; i++) { - Cudd_Ref(tmp); - } - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); - YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); - return tmp; + for (i = 0; i < refs; i++) { + Cudd_Ref(tmp); + } + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); + YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); + return tmp; } else { - return (DdNode *)YAP_IntOfTerm(t1); + return (DdNode *)YAP_IntOfTerm(t1); } } else if (f == FunctorPlus) { DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp = add_plus(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorLOr || f == FunctorOr) { DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp = add_lor(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorMinus) { DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp = add_minus(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorImplies) { DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *tmp = add_implies(manager, x1, x2); - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); return tmp; } else if (f == FunctorTimes4) { YAP_Term t1 = YAP_ArgOfTerm(2, t); if (YAP_IsVarTerm(t1)) { - YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; - DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(3, t)); - DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t)); - DdNode *tmp = add_plus(manager, x1, x2); + YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; + DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(3, t)); + DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t)); + DdNode *tmp = add_plus(manager, x1, x2); - for (i=0 ; i < refs; i++) { - Cudd_Ref(tmp); - } - Cudd_RecursiveDeref(manager,x1); - Cudd_RecursiveDeref(manager,x2); - YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); - return tmp; + for (i = 0; i < refs; i++) { + Cudd_Ref(tmp); + } + Cudd_RecursiveDeref(manager, x1); + Cudd_RecursiveDeref(manager, x2); + YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); + return tmp; } else { - return (DdNode *)YAP_IntOfTerm(t1); + return (DdNode *)YAP_IntOfTerm(t1); } } } else if (YAP_IsIntTerm(t)) { @@ -444,53 +409,45 @@ term_to_add(DdManager *manager, YAP_Term t) return NULL; } -static YAP_Bool -p_term_to_add(void) -{ - DdManager *manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); +static YAP_Bool p_term_to_add(void) { + DdManager *manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); int sz = YAP_IntOfTerm(YAP_ARG2), i; DdNode *t; - for (i = sz-1; i >= 0; i--) { + for (i = sz - 1; i >= 0; i--) { Cudd_addIthVar(manager, i); } t = term_to_add(manager, YAP_ARG1); return YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)manager)) && - YAP_Unify(YAP_ARG4, YAP_MkIntTerm((YAP_Int)t)); + YAP_Unify(YAP_ARG4, YAP_MkIntTerm((YAP_Int)t)); } -static YAP_Bool complement(int i) -{ - return i == 0 ? 1 : 0; +static YAP_Bool complement(int i) { return i == 0 ? 1 : 0; } + +static YAP_Bool var(DdManager *manager, DdNode *n, YAP_Int *vals) { + return (int)vals[Cudd_ReadPerm(manager, Cudd_NodeReadIndex(n))]; } -static YAP_Bool var(DdManager *manager, DdNode *n, YAP_Int *vals ) { - return (int)vals[Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n))]; -} - -static YAP_Bool -cudd_eval(DdManager *manager, DdNode *n, YAP_Int *vals ) -{ +static YAP_Bool cudd_eval(DdManager *manager, DdNode *n, YAP_Int *vals) { if (Cudd_IsConstant(n)) { // fprintf(stderr,"v=%f\n",Cudd_V(n)); return Cudd_V(n); } else { - // fprintf(stderr,"%x %d->%d %d\n",n->index,var(manager, n, vals),(Cudd_IsComplement(Cudd_E(n))!=0)); + // fprintf(stderr,"%x %d->%d %d\n",n->index,var(manager, n, + // vals),(Cudd_IsComplement(Cudd_E(n))!=0)); if (var(manager, n, vals) == 1) return cudd_eval(manager, Cudd_T(n), vals); else { DdNode *r = Cudd_E(n); if (Cudd_IsComplement(r)) { - return complement(cudd_eval(manager, Cudd_Regular(r), vals)); + return complement(cudd_eval(manager, Cudd_Regular(r), vals)); } else { - return cudd_eval(manager, r, vals); + return cudd_eval(manager, r, vals); } } } } -static YAP_Bool -cudd_eval_top(DdManager *manager, DdNode *n, YAP_Int *vals ) -{ +static YAP_Bool cudd_eval_top(DdManager *manager, DdNode *n, YAP_Int *vals) { if (Cudd_IsComplement(n)) { return complement(cudd_eval(manager, Cudd_Regular(n), vals)); } else { @@ -498,23 +455,22 @@ cudd_eval_top(DdManager *manager, DdNode *n, YAP_Int *vals ) } } -static YAP_Bool -p_eval_cudd(void) -{ +static YAP_Bool p_eval_cudd(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n = (DdNode *)YAP_IntOfTerm(YAP_ARG2); - size_t sz = YAP_ArityOfFunctor(YAP_FunctorOfTerm(YAP_ARG3)); + size_t sz = YAP_ArityOfFunctor(YAP_FunctorOfTerm(YAP_ARG3)); int val; YAP_Int *ar; YAP_Term t = YAP_ARG3; YAP_Int i; - if (sz <= 0) return FALSE; - ar = (YAP_Int*)malloc(sz*sizeof(YAP_Int)); + if (sz <= 0) + return FALSE; + ar = (YAP_Int *)malloc(sz * sizeof(YAP_Int)); if (!ar) return FALSE; - for (i= 0; i< sz; i++) { - YAP_Term tj = YAP_ArgOfTerm(i+1, t); + for (i = 0; i < sz; i++) { + YAP_Term tj = YAP_ArgOfTerm(i + 1, t); if (!YAP_IsIntTerm(tj)) return FALSE; ar[i] = YAP_IntOfTerm(tj); @@ -524,9 +480,7 @@ p_eval_cudd(void) return YAP_Unify(YAP_ARG4, YAP_MkIntTerm(val)); } -static double -add_eval(DdManager *manager, DdNode *n, YAP_Int *vals ) -{ +static double add_eval(DdManager *manager, DdNode *n, YAP_Int *vals) { if (Cudd_IsConstant(n)) { return Cudd_V(n); } else { @@ -538,23 +492,22 @@ add_eval(DdManager *manager, DdNode *n, YAP_Int *vals ) } } -static YAP_Bool -p_eval_add(void) -{ +static YAP_Bool p_eval_add(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n = (DdNode *)YAP_IntOfTerm(YAP_ARG2); - size_t sz = YAP_ArityOfFunctor(YAP_FunctorOfTerm(YAP_ARG3)); + size_t sz = YAP_ArityOfFunctor(YAP_FunctorOfTerm(YAP_ARG3)); double val; YAP_Int *ar; YAP_Term t = YAP_ARG3; YAP_Int i; - if (sz <= 0) return FALSE; - ar = (YAP_Int*)malloc(sz*sizeof(YAP_Int)); + if (sz <= 0) + return FALSE; + ar = (YAP_Int *)malloc(sz * sizeof(YAP_Int)); if (!ar) return FALSE; - for (i= 0; i< sz; i++) { - YAP_Term tj = YAP_ArgOfTerm(i+1, t); + for (i = 0; i < sz; i++) { + YAP_Term tj = YAP_ArgOfTerm(i + 1, t); if (!YAP_IsIntTerm(tj)) return FALSE; ar[i] = YAP_IntOfTerm(tj); @@ -569,41 +522,40 @@ typedef struct { YAP_Term val; } hash_table_entry; -static void -insert(hash_table_entry *p,DdNode *key, YAP_Term val, size_t sz) -{ - size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz; +static void insert(hash_table_entry *p, DdNode *key, YAP_Term val, size_t sz) { + size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz; while (p[el].key) { - el = (el+1)%sz; + el = (el + 1) % sz; } p[el].key = key; p[el].val = val; } -static YAP_Term lookup(hash_table_entry *p, DdNode *key, size_t sz) -{ - size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz; +static YAP_Term lookup(hash_table_entry *p, DdNode *key, size_t sz) { + size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz; while (p[el].key != key) { - el = (el+1)%sz; + el = (el + 1) % sz; } return p[el].val; } -static YAP_Term -build_prolog_cudd(DdManager *manager, DdNode *n, YAP_Term *ar, hash_table_entry *hash, YAP_Term t0, size_t sz) -{ +static YAP_Term build_prolog_cudd(DdManager *manager, DdNode *n, YAP_Term *ar, + hash_table_entry *hash, YAP_Term t0, + size_t sz) { if (Cudd_IsConstant(n)) { YAP_Term t = YAP_MkIntTerm(Cudd_V(n)); insert(hash, n, t, sz); return t0; } else { - //fprintf(stderr,"%x %d->%d %d\n",n->index, Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n)),var(manager, n, vals),Cudd_IsComplement(Cudd_E(n))); + // fprintf(stderr,"%x %d->%d %d\n",n->index, + // Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n)),var(manager, n, + // vals),Cudd_IsComplement(Cudd_E(n))); YAP_Term t[4], nt; YAP_Functor f; - //fprintf(stderr,"refs=%d\n", n->ref); + // fprintf(stderr,"refs=%d\n", n->ref); t[0] = YAP_MkVarTerm(); - t[1] = ar[Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n))]; + t[1] = ar[Cudd_ReadPerm(manager, Cudd_NodeReadIndex(n))]; t[2] = lookup(hash, Cudd_T(n), sz); t[3] = lookup(hash, Cudd_Regular(Cudd_E(n)), sz); if (Cudd_IsComplement(Cudd_E(n))) { @@ -613,53 +565,44 @@ build_prolog_cudd(DdManager *manager, DdNode *n, YAP_Term *ar, hash_table_entry } nt = YAP_MkApplTerm(f, 4, t); insert(hash, n, t[0], sz); - return YAP_MkPairTerm(nt,t0); + return YAP_MkPairTerm(nt, t0); } } -static inline int -max(int a, int b) -{ - return aref); + // fprintf(stderr,"refs=%d\n", n->ref); t[0] = YAP_MkVarTerm(); - t[1] = ar[Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n))]; + t[1] = ar[Cudd_ReadPerm(manager, Cudd_NodeReadIndex(n))]; t[2] = lookup(hash, Cudd_T(n), sz); t[3] = lookup(hash, Cudd_E(n), sz); f = FunctorOutAdd; nt = YAP_MkApplTerm(f, 4, t); insert(hash, n, t[0], sz); - return YAP_MkPairTerm(nt,t0); + return YAP_MkPairTerm(nt, t0); } } -static YAP_Bool -p_add_to_term(void) -{ +static YAP_Bool p_add_to_term(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node; YAP_Term t, t3 = YAP_ARG3; YAP_Int i, vars = get_vars(t3); - int nodes = max(0,Cudd_ReadNodeCount(manager))+vars+1; - size_t sz = nodes*4; + int nodes = max(0, Cudd_ReadNodeCount(manager)) + vars + 1; + size_t sz = nodes * 4; DdGen *dgen = Cudd_FirstNode(manager, n0, &node); - hash_table_entry *hash = (hash_table_entry *)calloc(sz,sizeof(hash_table_entry)); + hash_table_entry *hash = + (hash_table_entry *)calloc(sz, sizeof(hash_table_entry)); YAP_Term *ar; if (!dgen) return FALSE; - ar = (YAP_Term *)malloc(vars*sizeof(YAP_Term)); + ar = (YAP_Term *)malloc(vars * sizeof(YAP_Term)); if (!ar) return FALSE; - restart: +restart: t = YAP_TermNil(); - for (i= 0; i< vars; i++) { - ar[i] = YAP_ArgOfTerm(i+1, t3); + for (i = 0; i < vars; i++) { + ar[i] = YAP_ArgOfTerm(i + 1, t3); } while (node) { /* ensure we have enough memory */ @@ -737,7 +679,7 @@ p_add_to_term(void) Cudd_GenFree(dgen); t3 = YAP_ARG3; dgen = Cudd_FirstNode(manager, n0, &node); - bzero(hash, sizeof(hash_table_entry)*sz); + bzero(hash, sizeof(hash_table_entry) * sz); goto restart; } t = build_prolog_add(manager, node, ar, hash, t, sz); @@ -750,9 +692,7 @@ p_add_to_term(void) return YAP_Unify(YAP_ARG4, t); } -static YAP_Bool -p_cudd_size(void) -{ +static YAP_Bool p_cudd_size(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node; YAP_Int i = 0; @@ -774,67 +714,64 @@ typedef struct { double val; } hash_table_entry_dbl; -static void -insert2(hash_table_entry_dbl *p,DdNode *key, double val, size_t sz) -{ - size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz; +static void insert2(hash_table_entry_dbl *p, DdNode *key, double val, + size_t sz) { + size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz; while (p[el].key) { - el = (el+1)%sz; + el = (el + 1) % sz; } p[el].key = key; p[el].val = val; } -static double -lookup2(hash_table_entry_dbl *p, DdNode *key, size_t sz) -{ - size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz; +static double lookup2(hash_table_entry_dbl *p, DdNode *key, size_t sz) { + size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz; while (p[el].key != key) { - el = (el+1)%sz; + el = (el + 1) % sz; } return p[el].val; } -static double -build_sp_cudd(DdManager *manager, DdNode *n, double *ar, hash_table_entry_dbl *hash, size_t sz) -{ +static double build_sp_cudd(DdManager *manager, DdNode *n, double *ar, + hash_table_entry_dbl *hash, size_t sz) { if (Cudd_IsConstant(n)) { insert2(hash, n, Cudd_V(n), sz); return Cudd_V(n); } else { - //fprintf(stderr,"%x %d->%d %d\n",n->index, Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n)),var(manager, n, vals),Cudd_IsComplement(Cudd_E(n))); + // fprintf(stderr,"%x %d->%d %d\n",n->index, + // Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n)),var(manager, n, + // vals),Cudd_IsComplement(Cudd_E(n))); double pl, pr, p, prob; - prob = ar[Cudd_ReadPerm(manager,Cudd_NodeReadIndex(n))]; + prob = ar[Cudd_ReadPerm(manager, Cudd_NodeReadIndex(n))]; pl = lookup2(hash, Cudd_T(n), sz); pr = lookup2(hash, Cudd_Regular(Cudd_E(n)), sz); if (Cudd_IsComplement(Cudd_E(n))) { - p = prob*pl+(1-prob)*(1-pr); + p = prob * pl + (1 - prob) * (1 - pr); } else { - p = prob*pl+(1-prob)*pr; + p = prob * pl + (1 - prob) * pr; } insert2(hash, n, p, sz); return p; } } -static YAP_Bool -p_cudd_to_p(void) -{ +static YAP_Bool p_cudd_to_p(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node; YAP_Term t3 = YAP_ARG3; double p = 0.0; YAP_Int vars = YAP_ListLength(t3); - int nodes = max(Cudd_ReadNodeCount(manager),0)+vars+1; - size_t sz = nodes*4; + int nodes = max(Cudd_ReadNodeCount(manager), 0) + vars + 1; + size_t sz = nodes * 4; DdGen *dgen = Cudd_FirstNode(manager, n0, &node); - hash_table_entry_dbl *hash = (hash_table_entry_dbl *)calloc(sz,sizeof(hash_table_entry_dbl)); + hash_table_entry_dbl *hash = + (hash_table_entry_dbl *)calloc(sz, sizeof(hash_table_entry_dbl)); double *ar; if (!dgen) return FALSE; - ar = (double *)malloc(vars*sizeof(double)); + ar = (double *)malloc(vars * sizeof(double)); if (!ar) return FALSE; if (YAP_ListToFloats(t3, ar, vars) < 0) @@ -845,7 +782,7 @@ p_cudd_to_p(void) break; } if (node != n0 && Cudd_IsComplement(n0)) { - p = 1-p; + p = 1 - p; } Cudd_GenFree(dgen); free(hash); @@ -853,63 +790,67 @@ p_cudd_to_p(void) return YAP_Unify(YAP_ARG4, YAP_MkFloatTerm(p)); } -static YAP_Bool -p_cudd_print(void) -{ +static YAP_Bool p_cudd_print(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2); const char *s = YAP_AtomName(YAP_AtomOfTerm(YAP_ARG3)); FILE *f; - if (!strcmp(s, "user_output")) f = stdout; - else if (!strcmp(s, "user_error")) f = stderr; - else if (!strcmp(s, "user")) f = stdout; - else f = fopen(s, "w"); + if (!strcmp(s, "user_output")) + f = stdout; + else if (!strcmp(s, "user_error")) + f = stderr; + else if (!strcmp(s, "user")) + f = stdout; + else + f = fopen(s, "w"); Cudd_DumpDot(manager, 1, &n0, NULL, NULL, f); if (f != stdout && f != stderr) fclose(f); return TRUE; } -static YAP_Bool -p_cudd_print_with_names(void) -{ +static YAP_Bool p_cudd_print_with_names(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2); const char *s = YAP_AtomName(YAP_AtomOfTerm(YAP_ARG3)); - const char **namesp; + char **namesp; YAP_Term names = YAP_ARG4; FILE *f; YAP_Int len; - YAP_Int i = 0; + YAP_Int i = 0; - if (!strcmp(s, "user_output")) f = stdout; - else if (!strcmp(s, "user_error")) f = stderr; - else if (!strcmp(s, "user")) f = stdout; - else f = fopen(s, "w"); + if (!strcmp(s, "user_output")) + f = stdout; + else if (!strcmp(s, "user_error")) + f = stderr; + else if (!strcmp(s, "user")) + f = stdout; + else + f = fopen(s, "w"); if ((len = YAP_ListLength(names)) < 0) return FALSE; - if ((namesp = malloc(sizeof(const char *)*len)) == NULL) + if ((namesp = malloc(sizeof(const char *) * len)) == NULL) return FALSE; while (YAP_IsPairTerm(names)) { - YAP_Term hd = YAP_HeadOfTerm( names); - const char *f; - + YAP_Term hd = YAP_HeadOfTerm(names); + char *f; + if (YAP_IsAtomTerm(hd)) { - const char * s = YAP_AtomName(YAP_AtomOfTerm(hd)); - char *ns = malloc(strlen(s)+1); - strncpy(ns, s, strlen(s)+1); + const char *s = YAP_AtomName(YAP_AtomOfTerm(hd)); + char *ns = malloc(strlen(s) + 1); + strncpy(ns, s, strlen(s) + 1); f = ns; } else { - size_t sz =256; - char *s = malloc(sz+256); - while( !YAP_WriteBuffer(hd, s, sz-1, 0) ) { - sz+=1024; - s = realloc(s, sz); + size_t sz = 256; + char *s = malloc(sz + 256); + while (!YAP_WriteBuffer(hd, s, sz - 1, 0)) { + sz += 1024; + s = realloc(s, sz); } f = s; } - names = YAP_TailOfTerm( names); - namesp[i++] = f; + names = YAP_TailOfTerm(names); + namesp[i++] = f; } Cudd_DumpDot(manager, 1, &n0, namesp, NULL, f); if (f != stdout && f != stderr) @@ -918,30 +859,24 @@ p_cudd_print_with_names(void) i--; free((void *)namesp[i]); } - free( namesp ); + free(namesp); return TRUE; } -static YAP_Bool -p_cudd_die(void) -{ +static YAP_Bool p_cudd_die(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); Cudd_Quit(manager); return TRUE; } -static YAP_Bool -p_cudd_release_node(void) -{ +static YAP_Bool p_cudd_release_node(void) { DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2); - Cudd_RecursiveDeref(manager,n0); + Cudd_RecursiveDeref(manager, n0); return TRUE; } -void -init_cudd(void) -{ +void init_cudd(void) { FunctorDollarVar = YAP_MkFunctor(YAP_LookupAtom("$VAR"), 1); FunctorAnd = YAP_MkFunctor(YAP_LookupAtom("/\\"), 2); @@ -966,8 +901,8 @@ init_cudd(void) FunctorOutAdd = YAP_MkFunctor(YAP_LookupAtom("add"), 4); FunctorCudd = YAP_MkFunctor(YAP_LookupAtom("cudd"), 1); TermMinusOne = YAP_MkIntTerm(-1); - TermPlusOne = YAP_MkIntTerm(+1); - TermZero = YAP_MkIntTerm(0); + TermPlusOne = YAP_MkIntTerm(+1); + TermZero = YAP_MkIntTerm(0); TermFalse = YAP_MkAtomTerm(YAP_LookupAtom("false")); TermTrue = YAP_MkAtomTerm(YAP_LookupAtom("true")); YAP_UserCPredicate("term_to_cudd", p_term_to_cudd, 3); @@ -978,7 +913,7 @@ init_cudd(void) YAP_UserCPredicate("add_to_term", p_add_to_term, 4); YAP_UserCPredicate("cudd_to_probability_sum_product", p_cudd_to_p, 4); YAP_UserCPredicate("cudd_size", p_cudd_size, 3); - YAP_UserCPredicate("cudd_die", p_cudd_die, 1); + YAP_UserCPredicate("cudd_die", p_cudd_die, 1); YAP_UserCPredicate("cudd_reorder", p_cudd_reorder, 2); YAP_UserCPredicate("cudd_release_node", p_cudd_release_node, 2); YAP_UserCPredicate("cudd_print", p_cudd_print, 3); diff --git a/packages/cplint/approx/simplecuddLPADs/simplecudd.c b/packages/cplint/approx/simplecuddLPADs/simplecudd.c index 126ebfb3a..aef782f31 100644 --- a/packages/cplint/approx/simplecuddLPADs/simplecudd.c +++ b/packages/cplint/approx/simplecuddLPADs/simplecudd.c @@ -185,7 +185,7 @@ \******************************************************************************/ /* modified by Fabrizio Riguzzi in 2009 for dealing with multivalued variables -instead of variables or their negation, the script can contain equations of the +instead of variables or their negation, the script can contain equations of the form variable=value */ @@ -196,42 +196,48 @@ variable=value int _debug = 0; int _RapidLoad = 0; int _maxbufsize = 0; -int boolVars=0; +int boolVars = 0; -DdManager* simpleBDDinit(int varcnt) { +DdManager *simpleBDDinit(int varcnt) { DdManager *temp; temp = Cudd_Init(varcnt, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); Cudd_AutodynEnable(temp, CUDD_REORDER_GROUP_SIFT); - Cudd_SetMaxCacheHard(temp, 1024*1024*1024); - Cudd_SetLooseUpTo(temp, 1024*1024*512); - if (_debug) - Cudd_EnableReorderingReporting(temp); + Cudd_SetMaxCacheHard(temp, 1024 * 1024 * 1024); + Cudd_SetLooseUpTo(temp, 1024 * 1024 * 512); + if (_debug) + Cudd_EnableReorderingReporting(temp); return temp; } /* BDD tree travesrsing */ -DdNode* HighNodeOf(DdManager *manager, DdNode *node) { +DdNode *HighNodeOf(DdManager *manager, DdNode *node) { DdNode *tmp; - if (IsHigh(manager, node)) return HIGH(manager); - if (IsLow(manager, node)) return LOW(manager); + if (IsHigh(manager, node)) + return HIGH(manager); + if (IsLow(manager, node)) + return LOW(manager); tmp = Cudd_Regular(node); - if (Cudd_IsComplement(node)) return NOT(tmp->type.kids.T); + if (Cudd_IsComplement(node)) + return NOT(tmp->type.kids.T); return tmp->type.kids.T; } -DdNode* LowNodeOf(DdManager *manager, DdNode *node) { +DdNode *LowNodeOf(DdManager *manager, DdNode *node) { DdNode *tmp; - if (IsHigh(manager, node)) return HIGH(manager); - if (IsLow(manager, node)) return LOW(manager); + if (IsHigh(manager, node)) + return HIGH(manager); + if (IsLow(manager, node)) + return LOW(manager); tmp = Cudd_Regular(node); - if (Cudd_IsComplement(node)) return NOT(tmp->type.kids.E); + if (Cudd_IsComplement(node)) + return NOT(tmp->type.kids.E); return tmp->type.kids.E; } /* BDD tree generation */ -DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +DdNode *D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddAnd(manager, bdd1, bdd2); Cudd_Ref(tmp); @@ -239,7 +245,7 @@ DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { return tmp; } -DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +DdNode *D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddNand(manager, bdd1, bdd2); Cudd_Ref(tmp); @@ -247,7 +253,7 @@ DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { return tmp; } -DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +DdNode *D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddOr(manager, bdd1, bdd2); Cudd_Ref(tmp); @@ -255,7 +261,7 @@ DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { return tmp; } -DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +DdNode *D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddNor(manager, bdd1, bdd2); Cudd_Ref(tmp); @@ -263,7 +269,7 @@ DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { return tmp; } -DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +DdNode *D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddXor(manager, bdd1, bdd2); Cudd_Ref(tmp); @@ -271,7 +277,7 @@ DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { return tmp; } -DdNode* D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { +DdNode *D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { DdNode *tmp; tmp = Cudd_bddXnor(manager, bdd1, bdd2); Cudd_Ref(tmp); @@ -299,53 +305,60 @@ bddfileheader ReadFileHeader(char *filename) { if (!feof(temp.inputfile)) { header = freadline(temp.inputfile); temp.version = CheckFileVersion(header); - if (temp.version > -1) temp.filetype = (strlen(header) == 5) * BDDFILE_SCRIPT + (strlen(header) == 7) * BDDFILE_NODEDUMP; + if (temp.version > -1) + temp.filetype = (strlen(header) == 5) * BDDFILE_SCRIPT + + (strlen(header) == 7) * BDDFILE_NODEDUMP; free(header); switch (temp.filetype) { - case BDDFILE_SCRIPT: - switch (temp.version) { - case 1: - fscanf(temp.inputfile, "%i\n", &temp.varcnt); - fscanf(temp.inputfile, "%i\n", &temp.bvarcnt); - fscanf(temp.inputfile, "%i\n", &temp.varstart); - fscanf(temp.inputfile, "%i\n", &temp.intercnt); - break; - default: - fclose(temp.inputfile); - temp.inputfile = NULL; - break; - } - break; - case BDDFILE_NODEDUMP: - switch (temp.version) { - case 1: - fscanf(temp.inputfile, "%i\n", &temp.varcnt); - fscanf(temp.inputfile, "%i\n", &temp.varstart); - break; - default: - fclose(temp.inputfile); - temp.inputfile = NULL; - break; - } - break; - case BDDFILE_OTHER: - fclose(temp.inputfile); - temp.inputfile = NULL; + case BDDFILE_SCRIPT: + switch (temp.version) { + case 1: + fscanf(temp.inputfile, "%i\n", &temp.varcnt); + fscanf(temp.inputfile, "%i\n", &temp.bvarcnt); + fscanf(temp.inputfile, "%i\n", &temp.varstart); + fscanf(temp.inputfile, "%i\n", &temp.intercnt); break; default: fclose(temp.inputfile); temp.inputfile = NULL; break; + } + break; + case BDDFILE_NODEDUMP: + switch (temp.version) { + case 1: + fscanf(temp.inputfile, "%i\n", &temp.varcnt); + fscanf(temp.inputfile, "%i\n", &temp.varstart); + break; + default: + fclose(temp.inputfile); + temp.inputfile = NULL; + break; + } + break; + case BDDFILE_OTHER: + fclose(temp.inputfile); + temp.inputfile = NULL; + break; + default: + fclose(temp.inputfile); + temp.inputfile = NULL; + break; } } return temp; } int CheckFileVersion(const char *version) { - if (strlen(version) < 5) return -1; - if (strlen(version) == 5 && version[0] == '@' && version[1] == 'B' && version[2] == 'D' && version[3] == 'D') return atoi(version + 4); - if (strlen(version) == 7 && version[0] == '@' && version[1] == 'N' && version[2] == 'O' && version[3] == 'D' - && version[4] == 'E' && version[5] == 'S') return atoi(version + 6); + if (strlen(version) < 5) + return -1; + if (strlen(version) == 5 && version[0] == '@' && version[1] == 'B' && + version[2] == 'D' && version[3] == 'D') + return atoi(version + 4); + if (strlen(version) == 7 && version[0] == '@' && version[1] == 'N' && + version[2] == 'O' && version[3] == 'D' && version[4] == 'E' && + version[5] == 'S') + return atoi(version + 6); return -1; } @@ -364,7 +377,8 @@ int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename) { return ret; } -int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename) { +int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, + char *filename) { DdNode *f[1]; int ret; FILE *fd; @@ -379,7 +393,8 @@ int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char return ret; } -int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename) { +int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, + char *filename) { hisqueue *Nodes; FILE *outputfile; int i; @@ -387,20 +402,25 @@ int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filena perror(filename); return -1; } - fprintf(outputfile, "%s\n%i\n%i\n", "@NODES1", varmap.varcnt, varmap.varstart); + fprintf(outputfile, "%s\n%i\n%i\n", "@NODES1", varmap.varcnt, + varmap.varstart); Nodes = InitHistory(varmap.varcnt); for (i = 0; i < varmap.varcnt; i++) fprintf(outputfile, "%s\t%i\n", varmap.vars[i], Cudd_ReadPerm(manager, i)); - if (bdd == HIGH(manager)) fprintf(outputfile, "TRUE\t0\tTRUE\t0\tTRUE\t0\n"); - else if (bdd == LOW(manager)) fprintf(outputfile, "FALSE\t0\tFALSE\t0\tFALSE\t0\n"); - else SaveExpand(manager, varmap, Nodes, bdd, outputfile); + if (bdd == HIGH(manager)) + fprintf(outputfile, "TRUE\t0\tTRUE\t0\tTRUE\t0\n"); + else if (bdd == LOW(manager)) + fprintf(outputfile, "FALSE\t0\tFALSE\t0\tFALSE\t0\n"); + else + SaveExpand(manager, varmap, Nodes, bdd, outputfile); ReInitHistory(Nodes, varmap.varcnt); free(Nodes); fclose(outputfile); return 0; } -void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile) { +void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, + DdNode *Current, FILE *outputfile) { DdNode *h, *l; hisnode *Found; char *curnode; @@ -421,7 +441,8 @@ void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *C } else if (h == LOW(manager)) { fprintf(outputfile, "FALSE\t0\t"); } else { - if (GetNode(Nodes, varmap.varstart, h) == NULL) AddNode(Nodes, varmap.varstart, h, 0.0, 0, NULL); + if (GetNode(Nodes, varmap.varstart, h) == NULL) + AddNode(Nodes, varmap.varstart, h, 0.0, 0, NULL); curnode = GetNodeVarNameDisp(manager, varmap, h); inode = GetNodeIndex(Nodes, varmap.varstart, h); fprintf(outputfile, "%s\t%i\t", curnode, inode); @@ -432,7 +453,8 @@ void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *C } else if (l == LOW(manager)) { fprintf(outputfile, "FALSE\t0\n"); } else { - if (GetNode(Nodes, varmap.varstart, l) == NULL) AddNode(Nodes, varmap.varstart, l, 0.0, 0, NULL); + if (GetNode(Nodes, varmap.varstart, l) == NULL) + AddNode(Nodes, varmap.varstart, l, 0.0, 0, NULL); curnode = GetNodeVarNameDisp(manager, varmap, l); inode = GetNodeIndex(Nodes, varmap.varstart, l); fprintf(outputfile, "%s\t%i\n", curnode, inode); @@ -443,13 +465,13 @@ void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *C } } -DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile) { +DdNode *LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile) { hisqueue *Nodes; nodeline temp; DdNode *ret; int i, pos, *perm; char *varnam; - perm = (int *) malloc(sizeof(int) * varmap.varcnt); + perm = (int *)malloc(sizeof(int) * varmap.varcnt); Nodes = InitHistory(varmap.varcnt); for (i = 0; i < varmap.varcnt; i++) { varnam = freadstr(inputfile, "\t"); @@ -472,17 +494,22 @@ DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile) { free(Nodes); Cudd_Ref(ret); Cudd_ShuffleHeap(manager, perm); - for (i = 0; i < varmap.varcnt; i++) varmap.ivalue[i] = 0; + for (i = 0; i < varmap.varcnt; i++) + varmap.ivalue[i] = 0; return ret; } -DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current) { +DdNode *LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, + FILE *inputfile, nodeline current) { nodeline temp; DdNode *newnode, *truenode, *falsenode; int index; - newnode = GetIfExists(manager, varmap, Nodes, current.varname, current.nodenum); - if (newnode != NULL) return newnode; - falsenode = GetIfExists(manager, varmap, Nodes, current.falsevar, current.falsenode); + newnode = + GetIfExists(manager, varmap, Nodes, current.varname, current.nodenum); + if (newnode != NULL) + return newnode; + falsenode = + GetIfExists(manager, varmap, Nodes, current.falsevar, current.falsenode); if (falsenode == NULL) { temp.varname = freadstr(inputfile, "\t"); fscanf(inputfile, "%i\t", &temp.nodenum); @@ -495,7 +522,8 @@ DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE free(temp.truevar); free(temp.falsevar); } - truenode = GetIfExists(manager, varmap, Nodes, current.truevar, current.truenode); + truenode = + GetIfExists(manager, varmap, Nodes, current.truevar, current.truenode); if (truenode == NULL) { temp.varname = freadstr(inputfile, "\t"); fscanf(inputfile, "%i\t", &temp.nodenum); @@ -512,8 +540,8 @@ DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE if (!varmap.ivalue[index]) { varmap.ivalue[index] = 1; newnode = GetVar(manager, varmap.varstart + index); - //Cudd_RecursiveDeref(manager, newnode->type.kids.T); - //Cudd_RecursiveDeref(manager, newnode->type.kids.E); + // Cudd_RecursiveDeref(manager, newnode->type.kids.T); + // Cudd_RecursiveDeref(manager, newnode->type.kids.E); newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); Cudd_Ref(newnode->type.kids.T); @@ -524,22 +552,29 @@ DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE newnode = cuddAllocNode(manager); if (newnode != NULL) { newnode->index = varmap.varstart + index; - newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); - newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); + newnode->type.kids.T = + Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); + newnode->type.kids.E = + Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); Cudd_Ref(newnode->type.kids.T); Cudd_Ref(newnode->type.kids.E); Cudd_Ref(newnode); } } else { - newnode = cuddUniqueInter(manager, varmap.varstart + index, Cudd_NotCond(truenode, Cudd_IsComplement(truenode)), Cudd_NotCond(falsenode, Cudd_IsComplement(truenode))); + newnode = + cuddUniqueInter(manager, varmap.varstart + index, + Cudd_NotCond(truenode, Cudd_IsComplement(truenode)), + Cudd_NotCond(falsenode, Cudd_IsComplement(truenode))); if (newnode != NULL) { Cudd_Ref(newnode); } else { newnode = cuddAllocNode(manager); if (newnode != NULL) { newnode->index = varmap.varstart + index; - newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); - newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); + newnode->type.kids.T = + Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); + newnode->type.kids.E = + Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); Cudd_Ref(newnode->type.kids.T); Cudd_Ref(newnode->type.kids.E); Cudd_Ref(newnode); @@ -548,16 +583,20 @@ DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE } } if (newnode != NULL) { - Nodes[index].thenode[current.nodenum].key = Cudd_NotCond(newnode, Cudd_IsComplement(truenode)); + Nodes[index].thenode[current.nodenum].key = + Cudd_NotCond(newnode, Cudd_IsComplement(truenode)); return Cudd_NotCond(newnode, Cudd_IsComplement(truenode)); } return NULL; } -DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum) { +DdNode *GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, + char *varname, int nodenum) { int index; - if (strcmp(varname, "TRUE") == 0) return HIGH(manager); - if (strcmp(varname, "FALSE") == 0) return LOW(manager); + if (strcmp(varname, "TRUE") == 0) + return HIGH(manager); + if (strcmp(varname, "FALSE") == 0) + return LOW(manager); index = GetNamedVarIndex(varmap, varname); if (index == -1 * varmap.varcnt) { fprintf(stderr, "Error: more variables requested than initialized.\n"); @@ -567,14 +606,17 @@ DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char index = AddNamedVar(varmap, varname); } ExpandNodes(Nodes, index, nodenum); - if (Nodes[index].thenode[nodenum].key != NULL) return Nodes[index].thenode[nodenum].key; + if (Nodes[index].thenode[nodenum].key != NULL) + return Nodes[index].thenode[nodenum].key; return NULL; } void ExpandNodes(hisqueue *Nodes, int index, int nodenum) { int i; - if (Nodes[index].cnt > nodenum) return; - Nodes[index].thenode = (hisnode *) realloc(Nodes[index].thenode, (nodenum + 1) * sizeof(hisnode)); + if (Nodes[index].cnt > nodenum) + return; + Nodes[index].thenode = + (hisnode *)realloc(Nodes[index].thenode, (nodenum + 1) * sizeof(hisnode)); for (i = Nodes[index].cnt; i < nodenum + 1; i++) { Nodes[index].thenode[i].key = NULL; Nodes[index].thenode[i].ivalue = 0; @@ -594,22 +636,24 @@ int LoadVariableData(namedvars varmap, char *filename) { perror("fopen"); return -1; } - printf("filename %s\n",filename); - dataread = (char *) malloc(sizeof(char) * maxbufsize); - while(!feof(data)) { - index++; - printf("index %d\n",index); - fscanf(data,"@%s\n",dataread); + printf("filename %s\n", filename); + dataread = (char *)malloc(sizeof(char) * maxbufsize); + while (!feof(data)) { + index++; + printf("index %d\n", index); + fscanf(data, "@%s\n", dataread); + + varname = (char *)malloc(sizeof(char) * strlen(dataread)); + strcpy(varname, dataread); + varmap.vars[index] = varname; + fscanf(data, "%di\n", &values); + varmap.mvars[index].nVal = values; + varmap.mvars[index].nBit = (int)ceil(log(values) / log(2)); + varmap.mvars[index].probabilities = + (double *)malloc(sizeof(double) * values); + varmap.mvars[index].booleanVars = + (int *)malloc(sizeof(int) * varmap.mvars[index].nBit); - varname = (char *) malloc(sizeof(char) * strlen(dataread)); - strcpy(varname, dataread); - varmap.vars[index]=varname; - fscanf(data, "%di\n", &values); - varmap.mvars[index].nVal=values; - varmap.mvars[index].nBit=(int)ceil(log(values)/log(2)); - varmap.mvars[index].probabilities=(double *)malloc(sizeof(double)*values); - varmap.mvars[index].booleanVars=(int *)malloc(sizeof(int)*varmap.mvars[index].nBit); - free(varname); } fclose(data); @@ -617,38 +661,39 @@ int LoadVariableData(namedvars varmap, char *filename) { return 0; } -int LoadMultiVariableData(DdManager * mgr,namedvars varmap, char *filename) { +int LoadMultiVariableData(DdManager *mgr, namedvars varmap, char *filename) { FILE *data; char *dataread, *varname, *dynvalue; - int values, maxbufsize = 10, index = -1,i; + int values, maxbufsize = 10, index = -1, i; dynvalue = NULL; if ((data = fopen(filename, "r")) == NULL) { perror("fopen"); return -1; } - dataread = (char *) malloc(sizeof(char) * maxbufsize); - while(!feof(data)) { - index++; - if(fscanf(data,"@%s\n",dataread)<1) break; - varname = (char *) malloc(sizeof(char) * strlen(dataread)); - strcpy(varname, dataread); - varmap.vars[index]=varname; + dataread = (char *)malloc(sizeof(char) * maxbufsize); + while (!feof(data)) { + index++; + if (fscanf(data, "@%s\n", dataread) < 1) + break; + varname = (char *)malloc(sizeof(char) * strlen(dataread)); + strcpy(varname, dataread); + varmap.vars[index] = varname; + + fscanf(data, "%d\n", &values); + varmap.loaded[index] = 1; + varmap.mvars[index].init = 0; + varmap.mvars[index].nVal = values; + varmap.mvars[index].nBit = (int)ceil(log(values) / log(2)); + varmap.mvars[index].probabilities = + (double *)malloc(sizeof(double) * values); + varmap.mvars[index].booleanVars = + (DdNode **)malloc(sizeof(DdNode *) * varmap.mvars[index].nBit); + for (i = 0; i < values - 1; i++) { + fscanf(data, "%lf", &varmap.mvars[index].probabilities[i]); + } + fscanf(data, "%lf\n", &varmap.mvars[index].probabilities[values - 1]); + } - fscanf(data, "%d\n", &values); - varmap.loaded[index] = 1; - varmap.mvars[index].init=0; - varmap.mvars[index].nVal=values; - varmap.mvars[index].nBit=(int)ceil(log(values)/log(2)); - varmap.mvars[index].probabilities=(double *)malloc(sizeof(double)*values); - varmap.mvars[index].booleanVars=(DdNode **)malloc(sizeof(DdNode *)*varmap.mvars[index].nBit); - for (i=0;ivars = (char **) realloc(varmap->vars, sizeof(char *) * newvarcnt); - varmap->loaded = (int *) realloc(varmap->loaded, sizeof(int) * newvarcnt); - varmap->dvalue = (double *) realloc(varmap->dvalue, sizeof(double) * newvarcnt); - varmap->ivalue = (int *) realloc(varmap->ivalue, sizeof(int) * newvarcnt); - varmap->dynvalue = (void **) realloc(varmap->dynvalue, sizeof(int) * newvarcnt); + varmap->vars = (char **)realloc(varmap->vars, sizeof(char *) * newvarcnt); + varmap->loaded = (int *)realloc(varmap->loaded, sizeof(int) * newvarcnt); + varmap->dvalue = + (double *)realloc(varmap->dvalue, sizeof(double) * newvarcnt); + varmap->ivalue = (int *)realloc(varmap->ivalue, sizeof(int) * newvarcnt); + varmap->dynvalue = + (void **)realloc(varmap->dynvalue, sizeof(int) * newvarcnt); for (i = varmap->varcnt; i < newvarcnt; i++) { varmap->vars[i] = NULL; varmap->loaded[i] = 0; @@ -799,85 +854,85 @@ void EnlargeNamedVars(namedvars *varmap, int newvarcnt) { int AddNamedVarAt(namedvars varmap, const char *varname, int index) { if (varmap.varcnt > index) { - varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); + varmap.vars[index] = (char *)malloc(sizeof(char) * (strlen(varname) + 1)); strcpy(varmap.vars[index], varname); return index; } return -1; } -int AddNamedMultiVar(DdManager *mgr,namedvars varmap, const char *varname, int *value) { - - int index,i,l,nBit; +int AddNamedMultiVar(DdManager *mgr, namedvars varmap, const char *varname, + int *value) { + + int index, i, l, nBit; int *booleanVars; - char * vname; - l=strlen(varname); - i=0; - while (varname[i]!='-') - { - i++; - } - vname=(char *)malloc(sizeof(char)*(l+1)); - strncpy(vname,varname,i); - vname[i]='\0'; - sscanf(varname+i+1,"%d",value); - index= GetNamedVarIndex(varmap, vname); + char *vname; + l = strlen(varname); + i = 0; + while (varname[i] != '-') { + i++; + } + vname = (char *)malloc(sizeof(char) * (l + 1)); + strncpy(vname, varname, i); + vname[i] = '\0'; + sscanf(varname + i + 1, "%d", value); + index = GetNamedVarIndex(varmap, vname); if (index == -1 * varmap.varcnt) { return -1; } else if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) { index *= -1; - varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); + varmap.vars[index] = (char *)malloc(sizeof(char) * (strlen(varname) + 1)); + } + if (varmap.mvars[index].init == 0) { + nBit = varmap.mvars[index].nBit; + booleanVars = varmap.mvars[index].booleanVars; + for (i = 0; i < nBit; i++) { + booleanVars[i] = boolVars; + varmap.bVar2mVar[boolVars] = index; + boolVars = boolVars + 1; + } + varmap.mvars[index].init = 1; } - if (varmap.mvars[index].init==0){ - nBit=varmap.mvars[index].nBit; - booleanVars= varmap.mvars[index].booleanVars; - for (i=0;ivars[varmap->varcnt - 1] == NULL) - varmap->varcnt--; - return varmap->varcnt; + while (varmap->vars[varmap->varcnt - 1] == NULL) + varmap->varcnt--; + return varmap->varcnt; } int all_loaded(namedvars varmap, int disp) { @@ -924,7 +987,11 @@ int all_loaded(namedvars varmap, int disp) { for (i = 0; i < varmap.varcnt; i++) { if (varmap.loaded[i] == 0) { res = 0; - if (disp) fprintf(stderr, "The variable: %s was not loaded with values.\n", varmap.vars[i]); else return 0; + if (disp) + fprintf(stderr, "The variable: %s was not loaded with values.\n", + varmap.vars[i]); + else + return 0; } } return res; @@ -932,17 +999,19 @@ int all_loaded(namedvars varmap, int disp) { /* Parser */ -DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader) { - int icomment, maxlinesize, icur, iline, curinter, iequal ; +DdNode *FileGenerateBDD(DdManager *manager, namedvars varmap, + bddfileheader fileheader) { + int icomment, maxlinesize, icur, iline, curinter, iequal; DdNode *Line, **inter; char buf, *inputline, *filename; bddfileheader interfileheader; - long startAt, endAt; - double secs; + long startAt, endAt; + double secs; // Initialization of intermediate steps - inter = (DdNode **) malloc(sizeof(DdNode *) * fileheader.intercnt); - for (icur = 0; icur < fileheader.intercnt; icur++) inter[icur] = NULL; + inter = (DdNode **)malloc(sizeof(DdNode *) * fileheader.intercnt); + for (icur = 0; icur < fileheader.intercnt; icur++) + inter[icur] = NULL; // Read file data interfileheader.inputfile = NULL; filename = NULL; // For nested files @@ -951,24 +1020,30 @@ DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader file iline = 5; // Current file line (first after header) icomment = 0; // Flag for comments maxlinesize = 80; // inputline starting buffer size - inputline = (char *) malloc(sizeof(char) * maxlinesize); - while(!feof(fileheader.inputfile)) { + inputline = (char *)malloc(sizeof(char) * maxlinesize); + while (!feof(fileheader.inputfile)) { fread(&buf, 1, 1, fileheader.inputfile); - if (buf == ';' || buf == '%' || buf == '$') icomment = 1; + if (buf == ';' || buf == '%' || buf == '$') + icomment = 1; if (buf == '\n') { - if (icomment) icomment = 0; - /* if (iequal > 1) { - fprintf(stderr, "Error at line: %i. Line contains more than 1 equal(=) signs.\n", iline); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } else*/ + if (icomment) + icomment = 0; + /* if (iequal > 1) { + fprintf(stderr, "Error at line: %i. Line contains more than 1 + equal(=) signs.\n", iline); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } else*/ iequal = 0; if (icur > 0) { inputline[icur] = '\0'; if (inputline[0] != 'L') { - fprintf(stderr, "Error at line: %i. Intermediate results should start with L.\n", iline); + fprintf( + stderr, + "Error at line: %i. Intermediate results should start with L.\n", + iline); fclose(fileheader.inputfile); free(inter); free(inputline); @@ -978,35 +1053,45 @@ DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader file if (curinter == -1) { if (inputline[0] == 'L' && IsPosNumber(inputline + 1)) { curinter = atoi(inputline + 1) - 1; - if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] != NULL) { - if (_debug) fprintf(stderr, "Returned: %s\n", inputline); + if (curinter > -1 && curinter < fileheader.intercnt && + inter[curinter] != NULL) { + if (_debug) + fprintf(stderr, "Returned: %s\n", inputline); fclose(fileheader.inputfile); Line = inter[curinter]; free(inter); free(inputline); return Line; } else { - fprintf(stderr, "Error at line: %i. Return result asked doesn't exist.\n", iline); + fprintf(stderr, + "Error at line: %i. Return result asked doesn't exist.\n", + iline); fclose(fileheader.inputfile); free(inter); free(inputline); return NULL; } } else { - fprintf(stderr, "Error at line: %i. Invalid intermediate result format.\n", iline); + fprintf(stderr, + "Error at line: %i. Invalid intermediate result format.\n", + iline); fclose(fileheader.inputfile); free(inter); free(inputline); return NULL; } - } else if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] == NULL) { - if (_debug) fprintf(stderr, "%i %s\n", curinter, inputline); + } else if (curinter > -1 && curinter < fileheader.intercnt && + inter[curinter] == NULL) { + if (_debug) + fprintf(stderr, "%i %s\n", curinter, inputline); filename = getFileName(inputline); if (filename == NULL) { - startAt = clock(); - Line = LineParser(manager, varmap, inter, fileheader.intercnt, inputline, iline); - endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC)*1000; + startAt = clock(); + Line = LineParser(manager, varmap, inter, fileheader.intercnt, + inputline, iline); + endAt = clock(); + secs = + ((double)(endAt - startAt)) / ((double)CLOCKS_PER_SEC) * 1000; } else { interfileheader = ReadFileHeader(filename); if (interfileheader.inputfile == NULL) { @@ -1014,7 +1099,10 @@ DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader file } else { Line = FileGenerateBDD(manager, varmap, interfileheader); } - if (Line == NULL) fprintf(stderr, "Error at line: %i. Error in nested BDD file: %s.\n", iline, filename); + if (Line == NULL) + fprintf(stderr, + "Error at line: %i. Error in nested BDD file: %s.\n", + iline, filename); free(filename); filename = NULL; interfileheader.inputfile = NULL; @@ -1027,14 +1115,21 @@ DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader file } inter[curinter] = Line; icur = 0; - } else if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] != NULL) { - fprintf(stderr, "Error at line: %i. Intermediate results can't be overwritten.\n", iline); + } else if (curinter > -1 && curinter < fileheader.intercnt && + inter[curinter] != NULL) { + fprintf( + stderr, + "Error at line: %i. Intermediate results can't be overwritten.\n", + iline); fclose(fileheader.inputfile); free(inter); free(inputline); return NULL; } else { - fprintf(stderr, "Error at line: %i. Intermediate result asked doesn't exist.\n", iline); + fprintf( + stderr, + "Error at line: %i. Intermediate result asked doesn't exist.\n", + iline); fclose(fileheader.inputfile); free(inter); free(inputline); @@ -1043,11 +1138,13 @@ DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader file } iline++; } else if (buf != ' ' && buf != '\t' && !icomment) { - if (buf == '=') iequal++; + if (buf == '=') + iequal++; inputline[icur] = buf; icur += 1; if (icur == _maxbufsize) { - fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); + fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", + _maxbufsize); fclose(fileheader.inputfile); free(inter); free(inputline); @@ -1055,24 +1152,24 @@ DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader file } while (icur > maxlinesize - 1) { maxlinesize *= 2; - inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); + inputline = (char *)realloc(inputline, sizeof(char) * maxlinesize); } } } - fprintf(stderr, "Error, file either doesn't end with a blank line or no return result was asked.\n"); + fprintf(stderr, "Error, file either doesn't end with a blank line or no " + "return result was asked.\n"); fclose(fileheader.inputfile); free(inter); free(inputline); return NULL; } - int getInterBDD(char *function) { int i, ret; char *inter; for (i = 0; i < strlen(function); i++) { if (function[i] == '=') { - inter = (char *) malloc(sizeof(char) * i); + inter = (char *)malloc(sizeof(char) * i); strncpy(inter, function + 1, i - 1); inter[i - 1] = '\0'; if (IsPosNumber(inter)) { @@ -1088,14 +1185,15 @@ int getInterBDD(char *function) { return -1; } -char* getFileName(const char *function) { +char *getFileName(const char *function) { int i = 0; char *filename; - while(function[i] != '=' && (i + 1) < strlen(function)) i++; + while (function[i] != '=' && (i + 1) < strlen(function)) + i++; if ((i + 1) < strlen(function)) { i++; if (function[i] == '<' && function[strlen(function) - 1] == '>') { - filename = (char *) malloc(sizeof(char) * strlen(function) - i); + filename = (char *)malloc(sizeof(char) * strlen(function) - i); strcpy(filename, function + i + 1); filename[strlen(function) - i - 2] = '\0'; return filename; @@ -1104,8 +1202,9 @@ char* getFileName(const char *function) { return NULL; } -DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline) { - int istart, iend, ilength, i, symbol, ivar, inegvar, inegoper, iconst,value; +DdNode *LineParser(DdManager *manager, namedvars varmap, DdNode **inter, + int maxinter, char *function, int iline) { + int istart, iend, ilength, i, symbol, ivar, inegvar, inegoper, iconst, value; long startAt, endAt; double secs; DdNode *bdd; @@ -1129,17 +1228,22 @@ DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int max ilength = iend - i; iend = i - 1; if (ilength > 0 && !(ilength == 1 && function[istart] == '~')) { - term = (char *) malloc(sizeof(char) * (ilength + 1)); + term = (char *)malloc(sizeof(char) * (ilength + 1)); strncpy(term, function + istart, ilength); term[ilength] = '\0'; } else { - fprintf(stderr, "Line Parser Error at line: %i. An operator was encounter with no term at its right side.\n", iline); + fprintf(stderr, "Line Parser Error at line: %i. An operator was " + "encounter with no term at its right side.\n", + iline); free(term); return NULL; } } if (symbol != -1) { - if (term[0] == '~') inegvar = 1; else inegvar = 0; + if (term[0] == '~') + inegvar = 1; + else + inegvar = 0; if (term[0 + inegvar] != 'L') { // Term is a variable if (strcmp(term + inegvar, "TRUE") == 0) { @@ -1149,87 +1253,113 @@ DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int max inegvar = 1; } else { iconst = 0; - ivar = AddNamedMultiVar(manager,varmap, term + inegvar,&value); + ivar = AddNamedMultiVar(manager, varmap, term + inegvar, &value); if (ivar == -1) { - fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term); + fprintf(stderr, "Line Parser Error at line: %i. More BDD variables " + "than the reserved term: %s.\n", + iline, term); free(term); return NULL; } } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug && !iconst) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(GetVar(manager, ivar + varmap.varstart)), - Cudd_CountPath(GetVar(manager, ivar + varmap.varstart)), - Cudd_DagSize(GetVar(manager, ivar + varmap.varstart)) ); + if (_debug) + fprintf(stderr, "%s\n", term); + if (_debug && !iconst) + fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), Cudd_CountPath(bdd), + Cudd_DagSize(bdd), Cudd_CountPathsToNonZero(GetVar( + manager, ivar + varmap.varstart)), + Cudd_CountPath(GetVar(manager, ivar + varmap.varstart)), + Cudd_DagSize(GetVar(manager, ivar + varmap.varstart))); startAt = clock(); if (!iconst) { - if (inegvar) bdd = BDD_Operator(manager, NOT(GetMVar(manager, ivar + varmap.varstart,value,varmap)), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, GetMVar(manager, ivar + varmap.varstart,value,varmap), bdd, curoper, inegoper); + if (inegvar) + bdd = BDD_Operator( + manager, + NOT(GetMVar(manager, ivar + varmap.varstart, value, varmap)), + bdd, curoper, inegoper); + else + bdd = BDD_Operator(manager, GetMVar(manager, ivar + varmap.varstart, + value, varmap), + bdd, curoper, inegoper); } else { - switch(curoper) { - case '+': - if (inegvar ^ inegoper) ; else { - bdd = HIGH(manager); - Cudd_Ref(bdd); - } - break; - case '*': - if (inegvar ^ inegoper) { - bdd = LOW(manager); - Cudd_Ref(bdd); - } - break; - case '#': - if (inegvar ^ inegoper) ; else bdd = NOT(bdd); - break; + switch (curoper) { + case '+': + if (inegvar ^ inegoper) + ; + else { + bdd = HIGH(manager); + Cudd_Ref(bdd); + } + break; + case '*': + if (inegvar ^ inegoper) { + bdd = LOW(manager); + Cudd_Ref(bdd); + } + break; + case '#': + if (inegvar ^ inegoper) + ; + else + bdd = NOT(bdd); + break; } } endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + secs = ((double)(endAt - startAt)) / ((double)CLOCKS_PER_SEC); + if (_debug) + fprintf(stderr, "term: %s of line: %i took: %li\n", term, iline, + endAt - startAt); + // if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + fprintf(stderr, "Line Parser Error at line: %i. Error using operator " + "%c on term: %s.\n", + iline, curoper, term); free(term); return NULL; } } else { // Term is an intermediate result - if (IsPosNumber(term + inegvar + 1)) - { - ivar = atoi(term + inegvar + 1) - 1; - } - else { - fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate result format term: %s.\n", iline, term); + if (IsPosNumber(term + inegvar + 1)) { + ivar = atoi(term + inegvar + 1) - 1; + } else { + fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate " + "result format term: %s.\n", + iline, term); free(term); return NULL; } if (ivar < 0 || ivar > maxinter || inter[ivar] == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared intermediate result term: %s.\n", iline, term); + fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared " + "intermediate result term: %s.\n", + iline, term); free(term); return NULL; } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(inter[ivar]), - Cudd_CountPath(inter[ivar]), - Cudd_DagSize(inter[ivar]) ); + if (_debug) + fprintf(stderr, "%s\n", term); + if (_debug) + fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), Cudd_CountPath(bdd), + Cudd_DagSize(bdd), Cudd_CountPathsToNonZero(inter[ivar]), + Cudd_CountPath(inter[ivar]), Cudd_DagSize(inter[ivar])); startAt = clock(); - if (inegvar) bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); + if (inegvar) + bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); + else + bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %li\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + secs = ((double)(endAt - startAt)) / ((double)CLOCKS_PER_SEC); + if (_debug) + fprintf(stderr, "term: %s of line: %i took: %li\n", term, iline, + endAt - startAt); + // if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + fprintf(stderr, "Line Parser Error at line: %i. Error using operator " + "%c on term: %s.\n", + iline, curoper, term); free(term); return NULL; } @@ -1237,7 +1367,8 @@ DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int max free(term); term = NULL; curoper = function[symbol]; - if (curoper == '=') return bdd; + if (curoper == '=') + return bdd; if (function[symbol - 1] == '~') { inegoper = 1; i--; @@ -1251,35 +1382,43 @@ DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int max return NULL; } -DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper) { +DdNode *BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, + char Operator, int inegoper) { switch (Operator) { - case '+': - if (inegoper) return D_BDDNor(manager, bdd1, bdd2); - else return D_BDDOr(manager, bdd1, bdd2); - break; - case '*': - if (inegoper) return D_BDDNand(manager, bdd1, bdd2); - else return D_BDDAnd(manager, bdd1, bdd2); - break; - case '#': - if (inegoper) return D_BDDXnor(manager, bdd1, bdd2); - else return D_BDDXor(manager, bdd1, bdd2); - break; - default: - return NULL; - break; + case '+': + if (inegoper) + return D_BDDNor(manager, bdd1, bdd2); + else + return D_BDDOr(manager, bdd1, bdd2); + break; + case '*': + if (inegoper) + return D_BDDNand(manager, bdd1, bdd2); + else + return D_BDDAnd(manager, bdd1, bdd2); + break; + case '#': + if (inegoper) + return D_BDDXnor(manager, bdd1, bdd2); + else + return D_BDDXor(manager, bdd1, bdd2); + break; + default: + return NULL; + break; } } -DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { +DdNode *OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { int icomment, maxlinesize, icur, iline, curinter, iequal, iinters, itmp, i; DdNode *Line, **inter; char buf, *inputline, *filename; bddfileheader interfileheader; // Initialization of intermediate steps iinters = 1; - inter = (DdNode **) malloc(sizeof(DdNode *) * iinters); - for (icur = 0; icur < iinters; icur++) inter[icur] = NULL; + inter = (DdNode **)malloc(sizeof(DdNode *) * iinters); + for (icur = 0; icur < iinters; icur++) + inter[icur] = NULL; // Read file data interfileheader.inputfile = NULL; filename = NULL; // For nested files @@ -1288,19 +1427,25 @@ DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { iline = 1; // Current file line (first after header) icomment = 0; // Flag for comments maxlinesize = 80; // inputline starting buffer size - inputline = (char *) malloc(sizeof(char) * maxlinesize); + inputline = (char *)malloc(sizeof(char) * maxlinesize); do { buf = fgetc(stdin); - if (buf == ';' || buf == '%' || buf == '$') icomment = 1; + if (buf == ';' || buf == '%' || buf == '$') + icomment = 1; if (buf == '\n') { - if (icomment) icomment = 0; + if (icomment) + icomment = 0; if (iequal > 1) { - fprintf(stderr, "Error at line: %i. Line contains more than 1 equal(=) signs.\n", iline); + fprintf( + stderr, + "Error at line: %i. Line contains more than 1 equal(=) signs.\n", + iline); free(inter); free(inputline); return NULL; - } else iequal = 0; + } else + iequal = 0; if (icur > 0) { inputline[icur] = '\0'; if (inputline[0] == '@') { @@ -1314,15 +1459,18 @@ DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { EnlargeNamedVars(varmap, itmp); itmp = GetParam(inputline, 2); if (itmp > iinters) { - inter = (DdNode **) realloc(inter, sizeof(DdNode *) * itmp); - for (i = iinters; i < itmp; i++) inter[i] = NULL; + inter = (DdNode **)realloc(inter, sizeof(DdNode *) * itmp); + for (i = iinters; i < itmp; i++) + inter[i] = NULL; iinters = itmp; } } icur = 0; } else { if (inputline[0] != 'L') { - fprintf(stderr, "Error at line: %i. Intermediate results should start with L.\n", iline); + fprintf(stderr, "Error at line: %i. Intermediate results should " + "start with L.\n", + iline); free(inter); free(inputline); return NULL; @@ -1331,44 +1479,59 @@ DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { if (curinter == -1) { if (inputline[0] == 'L' && IsPosNumber(inputline + 1)) { curinter = atoi(inputline + 1) - 1; - if (curinter > -1 && curinter < iinters && inter[curinter] != NULL) { - if (_debug) fprintf(stderr, "Returned: %s\n", inputline); + if (curinter > -1 && curinter < iinters && + inter[curinter] != NULL) { + if (_debug) + fprintf(stderr, "Returned: %s\n", inputline); Line = inter[curinter]; free(inter); free(inputline); return Line; } else { - fprintf(stderr, "Error at line: %i. Return result asked doesn't exist.\n", iline); + fprintf( + stderr, + "Error at line: %i. Return result asked doesn't exist.\n", + iline); free(inter); free(inputline); return NULL; } } else { - fprintf(stderr, "Error at line: %i. Invalid intermediate result format.\n", iline); + fprintf( + stderr, + "Error at line: %i. Invalid intermediate result format.\n", + iline); free(inter); free(inputline); return NULL; } } else if (curinter > -1) { if (curinter >= iinters) { - inter = (DdNode **) realloc(inter, sizeof(DdNode *) * (curinter + 1)); - for (i = iinters; i < curinter + 1; i++) inter[i] = NULL; + inter = + (DdNode **)realloc(inter, sizeof(DdNode *) * (curinter + 1)); + for (i = iinters; i < curinter + 1; i++) + inter[i] = NULL; iinters = curinter + 1; } if (inter[curinter] == NULL) { - if (_debug) fprintf(stderr, "%i %s\n", curinter, inputline); + if (_debug) + fprintf(stderr, "%i %s\n", curinter, inputline); filename = getFileName(inputline); if (filename == NULL) { - Line = OnlineLineParser(manager, varmap, inter, iinters, inputline, iline); + Line = OnlineLineParser(manager, varmap, inter, iinters, + inputline, iline); } else { interfileheader = ReadFileHeader(filename); if (interfileheader.inputfile == NULL) { - //Line = simpleBDDload(manager, varmap, filename); + // Line = simpleBDDload(manager, varmap, filename); Line = NULL; } else { Line = FileGenerateBDD(manager, *varmap, interfileheader); } - if (Line == NULL) fprintf(stderr, "Error at line: %i. Error in nested BDD file: %s.\n", iline, filename); + if (Line == NULL) + fprintf(stderr, + "Error at line: %i. Error in nested BDD file: %s.\n", + iline, filename); free(filename); filename = NULL; interfileheader.inputfile = NULL; @@ -1381,13 +1544,18 @@ DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { inter[curinter] = Line; icur = 0; } else if (inter[curinter] != NULL) { - fprintf(stderr, "Error at line: %i. Intermediate results can't be overwritten.\n", iline); + fprintf(stderr, "Error at line: %i. Intermediate results can't " + "be overwritten.\n", + iline); free(inter); free(inputline); return NULL; } } else { - fprintf(stderr, "Error at line: %i. Intermediate result asked doesn't exist.\n", iline); + fprintf( + stderr, + "Error at line: %i. Intermediate result asked doesn't exist.\n", + iline); free(inter); free(inputline); return NULL; @@ -1396,28 +1564,32 @@ DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { } iline++; } else if (buf != ' ' && buf != '\t' && !icomment) { - if (buf == '=') iequal++; + if (buf == '=') + iequal++; inputline[icur] = buf; icur += 1; if (icur == _maxbufsize) { - fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); + fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", + _maxbufsize); free(inter); free(inputline); return NULL; } while (icur > maxlinesize - 1) { maxlinesize *= 2; - inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); + inputline = (char *)realloc(inputline, sizeof(char) * maxlinesize); } } - } while(1); - fprintf(stderr, "Error, file either doesn't end with a blank line or no return result was asked.\n"); + } while (1); + fprintf(stderr, "Error, file either doesn't end with a blank line or no " + "return result was asked.\n"); free(inter); free(inputline); return NULL; } -DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline) { +DdNode *OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, + int maxinter, char *function, int iline) { int istart, iend, ilength, i, symbol, ivar, inegvar, inegoper, iconst; long startAt, endAt; double secs; @@ -1442,22 +1614,27 @@ DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, ilength = iend - i; iend = i - 1; if (ilength > 0 && !(ilength == 1 && function[istart] == '~')) { - term = (char *) malloc(sizeof(char) * (ilength + 1)); + term = (char *)malloc(sizeof(char) * (ilength + 1)); strncpy(term, function + istart, ilength); term[ilength] = '\0'; } else { - fprintf(stderr, "Line Parser Error at line: %i. An operator was encounter with no term at its right side.\n", iline); + fprintf(stderr, "Line Parser Error at line: %i. An operator was " + "encounter with no term at its right side.\n", + iline); free(term); return NULL; } } if (symbol != -1) { - if (term[0] == '~') inegvar = 1; else inegvar = 0; + if (term[0] == '~') + inegvar = 1; + else + inegvar = 0; if (term[0 + inegvar] != 'L') { // Term is a variable - if (strcmp(term , "TRUE") == 0) { + if (strcmp(term, "TRUE") == 0) { iconst = 1; - } else if (strcmp(term , "FALSE") == 0) { + } else if (strcmp(term, "FALSE") == 0) { iconst = 1; inegvar = 1; } else { @@ -1468,80 +1645,109 @@ DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, ivar = AddNamedVar(*varmap, term + inegvar); } if (ivar == -1) { - fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term); + fprintf(stderr, "Line Parser Error at line: %i. More BDD variables " + "than the reserved term: %s.\n", + iline, term); free(term); return NULL; } } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug && !iconst) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(GetVar(manager, ivar + varmap->varstart)), - Cudd_CountPath(GetVar(manager, ivar + varmap->varstart)), - Cudd_DagSize(GetVar(manager, ivar + varmap->varstart)) ); + if (_debug) + fprintf(stderr, "%s\n", term); + if (_debug && !iconst) + fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), Cudd_CountPath(bdd), + Cudd_DagSize(bdd), Cudd_CountPathsToNonZero(GetVar( + manager, ivar + varmap->varstart)), + Cudd_CountPath(GetVar(manager, ivar + varmap->varstart)), + Cudd_DagSize(GetVar(manager, ivar + varmap->varstart))); startAt = clock(); if (!iconst) { - if (inegvar) bdd = BDD_Operator(manager, NOT(GetVar(manager, ivar + varmap->varstart)), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, GetVar(manager, ivar + varmap->varstart), bdd, curoper, inegoper); + if (inegvar) + bdd = BDD_Operator(manager, + NOT(GetVar(manager, ivar + varmap->varstart)), + bdd, curoper, inegoper); + else + bdd = + BDD_Operator(manager, GetVar(manager, ivar + varmap->varstart), + bdd, curoper, inegoper); } else { - switch(curoper) { - case '+': - if (inegvar ^ inegoper) ; else { - bdd = HIGH(manager); - Cudd_Ref(bdd); - } - break; - case '*': - if (inegvar ^ inegoper) { - bdd = LOW(manager); - Cudd_Ref(bdd); - } - break; - case '#': - if (inegvar ^ inegoper) ; else bdd = NOT(bdd); - break; + switch (curoper) { + case '+': + if (inegvar ^ inegoper) + ; + else { + bdd = HIGH(manager); + Cudd_Ref(bdd); + } + break; + case '*': + if (inegvar ^ inegoper) { + bdd = LOW(manager); + Cudd_Ref(bdd); + } + break; + case '#': + if (inegvar ^ inegoper) + ; + else + bdd = NOT(bdd); + break; } } endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + secs = ((double)(endAt - startAt)) / ((double)CLOCKS_PER_SEC); + if (_debug) + fprintf(stderr, "term: %s of line: %i took: %li\n", term, iline, + endAt - startAt); + // if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + fprintf(stderr, "Line Parser Error at line: %i. Error using operator " + "%c on term: %s.\n", + iline, curoper, term); free(term); return NULL; } } else { // Term is an intermediate result - if (IsPosNumber(term + inegvar + 1)) ivar = atoi(term + inegvar + 1) - 1; else { - fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate result format term: %s.\n", iline, term); + if (IsPosNumber(term + inegvar + 1)) + ivar = atoi(term + inegvar + 1) - 1; + else { + fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate " + "result format term: %s.\n", + iline, term); free(term); return NULL; } if (ivar < 0 || ivar > maxinter || inter[ivar] == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared intermediate result term: %s.\n", iline, term); + fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared " + "intermediate result term: %s.\n", + iline, term); free(term); return NULL; } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(inter[ivar]), - Cudd_CountPath(inter[ivar]), - Cudd_DagSize(inter[ivar]) ); + if (_debug) + fprintf(stderr, "%s\n", term); + if (_debug) + fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), Cudd_CountPath(bdd), + Cudd_DagSize(bdd), Cudd_CountPathsToNonZero(inter[ivar]), + Cudd_CountPath(inter[ivar]), Cudd_DagSize(inter[ivar])); startAt = clock(); - if (inegvar) bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); + if (inegvar) + bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); + else + bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + secs = ((double)(endAt - startAt)) / ((double)CLOCKS_PER_SEC); + if (_debug) + fprintf(stderr, "term: %s of line: %i took: %li\n", term, iline, + endAt - startAt); + // if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + fprintf(stderr, "Line Parser Error at line: %i. Error using operator " + "%c on term: %s.\n", + iline, curoper, term); free(term); return NULL; } @@ -1549,7 +1755,8 @@ DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, free(term); term = NULL; curoper = function[symbol]; - if (curoper == '=') return bdd; + if (curoper == '=') + return bdd; if (function[symbol - 1] == '~') { inegoper = 1; i--; @@ -1569,10 +1776,10 @@ int GetParam(char *inputline, int iParam) { istart = 1; icoma = istart; iend = strlen(inputline); - while((inputline[icoma] != ',') && (icoma < iend)) + while ((inputline[icoma] != ',') && (icoma < iend)) icoma++; if (iParam == 1) { - numb = (char *) malloc(sizeof(char) * icoma); + numb = (char *)malloc(sizeof(char) * icoma); strncpy(numb, inputline + 1, icoma - 1); numb[icoma - 1] = '\0'; if (IsPosNumber(numb)) { @@ -1580,8 +1787,8 @@ int GetParam(char *inputline, int iParam) { free(numb); return ret; } - } else if(iParam == 2) { - numb = (char *) malloc(sizeof(char) * (iend - icoma + 1)); + } else if (iParam == 2) { + numb = (char *)malloc(sizeof(char) * (iend - icoma + 1)); strncpy(numb, inputline + icoma + 1, iend - icoma); numb[iend - icoma] = '\0'; if (IsPosNumber(numb)) { @@ -1593,7 +1800,8 @@ int GetParam(char *inputline, int iParam) { return 0; } -void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, DdNode *bdd) { +void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, + DdNode *bdd) { char buf, *inputline; int icur, maxlinesize, iline, index, iloop, iQsize, i, inQ; DdNode **Q, **Q2, *h_node, *l_node, *curnode; @@ -1603,109 +1811,131 @@ void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, Dd icur = 0; // Pointer for inputline buffer location iline = 1; // Current file line (first after header) maxlinesize = 80; // inputline starting buffer size - inputline = (char *) malloc(sizeof(char) * maxlinesize); + inputline = (char *)malloc(sizeof(char) * maxlinesize); curnode = bdd; iQsize = 0; - Q = (DdNode **) malloc(sizeof(DdNode *) * iQsize); + Q = (DdNode **)malloc(sizeof(DdNode *) * iQsize); Q2 = NULL; his = InitHistory(varmap.varcnt); do { buf = fgetc(stdin); if (buf == '\n') { inputline[icur] = '\0'; - if ((icur > 0) && (inputline[0] == '@') && (inputline[2] == ',' || inputline[2] == '\0')) { - switch(inputline[1]) { - case 'c': - printf("bdd_temp_value('%s', %i).\n", GetNodeVarNameDisp(manager, varmap, curnode), iQsize); - break; - case 'n': - if (curnode != HIGH(manager) && curnode != LOW(manager) && (hnode = GetNode(his, varmap.varstart, curnode)) == NULL) { - AddNode(his, varmap.varstart, curnode, 0.0, 0, NULL); - l_node = LowNodeOf(manager, curnode); - h_node = HighNodeOf(manager, curnode); - inQ = 0; - for(i = 0; (i < iQsize / 2) && (inQ < 3); i++) - inQ = (Q[i] == l_node) || (Q[iQsize - i] == l_node) + 2 * (Q[i] == h_node) || (Q[iQsize - i] == h_node); - if ((inQ & 1) == 0) inQ = inQ + (GetNode(his, varmap.varstart, l_node) != NULL); - if ((inQ & 2) == 0) inQ = inQ + 2 * (GetNode(his, varmap.varstart, h_node) != NULL); - if ((inQ & 1) == 1) inQ = inQ - (l_node == HIGH(manager) || l_node == LOW(manager)); - if ((inQ & 2) == 2) inQ = inQ - 2 * (h_node == HIGH(manager) || h_node == LOW(manager)); - switch(inQ) { - case 0: - iQsize += 2; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - Q[iQsize - 2] = l_node; - Q[iQsize - 1] = h_node; - break; - case 1: - iQsize++; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - Q[iQsize - 1] = h_node; - break; - case 2: - iQsize++; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - Q[iQsize - 1] = l_node; - break; - case 3: - break; - default: - break; - } + if ((icur > 0) && (inputline[0] == '@') && + (inputline[2] == ',' || inputline[2] == '\0')) { + switch (inputline[1]) { + case 'c': + printf("bdd_temp_value('%s', %i).\n", + GetNodeVarNameDisp(manager, varmap, curnode), iQsize); + break; + case 'n': + if (curnode != HIGH(manager) && curnode != LOW(manager) && + (hnode = GetNode(his, varmap.varstart, curnode)) == NULL) { + AddNode(his, varmap.varstart, curnode, 0.0, 0, NULL); + l_node = LowNodeOf(manager, curnode); + h_node = HighNodeOf(manager, curnode); + inQ = 0; + for (i = 0; (i < iQsize / 2) && (inQ < 3); i++) + inQ = (Q[i] == l_node) || + (Q[iQsize - i] == l_node) + 2 * (Q[i] == h_node) || + (Q[iQsize - i] == h_node); + if ((inQ & 1) == 0) + inQ = inQ + (GetNode(his, varmap.varstart, l_node) != NULL); + if ((inQ & 2) == 0) + inQ = inQ + 2 * (GetNode(his, varmap.varstart, h_node) != NULL); + if ((inQ & 1) == 1) + inQ = inQ - (l_node == HIGH(manager) || l_node == LOW(manager)); + if ((inQ & 2) == 2) + inQ = + inQ - 2 * (h_node == HIGH(manager) || h_node == LOW(manager)); + switch (inQ) { + case 0: + iQsize += 2; + Q = (DdNode **)realloc(Q, sizeof(DdNode *) * iQsize); + Q[iQsize - 2] = l_node; + Q[iQsize - 1] = h_node; + break; + case 1: + iQsize++; + Q = (DdNode **)realloc(Q, sizeof(DdNode *) * iQsize); + Q[iQsize - 1] = h_node; + break; + case 2: + iQsize++; + Q = (DdNode **)realloc(Q, sizeof(DdNode *) * iQsize); + Q[iQsize - 1] = l_node; + break; + case 3: + break; + default: + break; } - if (inputline[2] == '\0' || strcmp(inputline + 3, "DFS") == 0) { - if (iQsize > 0) { - iQsize--; - curnode = Q[iQsize]; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - } - } else if (strcmp(inputline + 3, "BFS") == 0) { - if (iQsize > 0) { - iQsize--; - curnode = Q[0]; - Q2 = (DdNode **) malloc(sizeof(DdNode *) * iQsize); - for(i = 0; i < iQsize; i++) - Q2[i] = Q[i + 1]; - free(Q); - Q = Q2; - } - } else { - fprintf(stderr, "Error: Could not find method: %s, Correct syntax @n,[DFS, BFS].\n", inputline + 3); + } + if (inputline[2] == '\0' || strcmp(inputline + 3, "DFS") == 0) { + if (iQsize > 0) { + iQsize--; + curnode = Q[iQsize]; + Q = (DdNode **)realloc(Q, sizeof(DdNode *) * iQsize); + } + } else if (strcmp(inputline + 3, "BFS") == 0) { + if (iQsize > 0) { + iQsize--; + curnode = Q[0]; + Q2 = (DdNode **)malloc(sizeof(DdNode *) * iQsize); + for (i = 0; i < iQsize; i++) + Q2[i] = Q[i + 1]; free(Q); - free(inputline); - exit(-1); + Q = Q2; } - break; - case 'h': - printf("bdd_temp_value('%s').\n", GetNodeVarNameDisp(manager, varmap, HighNodeOf(manager, curnode))); - break; - case 'l': - printf("bdd_temp_value('%s').\n", GetNodeVarNameDisp(manager, varmap, LowNodeOf(manager, curnode))); - break; - case 'v': - index = GetNamedVarIndex(varmap, inputline + 3); - if (index >= 0) { - fprintf(stdout, "bdd_temp_value([%f,%i,%s]).\n", varmap.dvalue[index], varmap.ivalue[index], (char *) varmap.dynvalue[index]); - } else { - fprintf(stderr, "Error: Could not find variable: %s, Correct syntax @v,[variable name].\n", inputline + 3); - free(Q); - free(inputline); - exit(-1); - } - break; - case 'e': - iloop = 0; - break; - default: - fprintf(stderr, "Error: Not recognizable instruction: %s.\n", inputline); + } else { + fprintf(stderr, "Error: Could not find method: %s, Correct syntax " + "@n,[DFS, BFS].\n", + inputline + 3); free(Q); free(inputline); exit(-1); - break; + } + break; + case 'h': + printf("bdd_temp_value('%s').\n", + GetNodeVarNameDisp(manager, varmap, + HighNodeOf(manager, curnode))); + break; + case 'l': + printf( + "bdd_temp_value('%s').\n", + GetNodeVarNameDisp(manager, varmap, LowNodeOf(manager, curnode))); + break; + case 'v': + index = GetNamedVarIndex(varmap, inputline + 3); + if (index >= 0) { + fprintf(stdout, "bdd_temp_value([%f,%i,%s]).\n", + varmap.dvalue[index], varmap.ivalue[index], + (char *)varmap.dynvalue[index]); + } else { + fprintf(stderr, "Error: Could not find variable: %s, Correct " + "syntax @v,[variable name].\n", + inputline + 3); + free(Q); + free(inputline); + exit(-1); + } + break; + case 'e': + iloop = 0; + break; + default: + fprintf(stderr, "Error: Not recognizable instruction: %s.\n", + inputline); + free(Q); + free(inputline); + exit(-1); + break; } icur = 0; } else { - fprintf(stderr, "Error: Not recognizable instruction: %s.\n", inputline); + fprintf(stderr, "Error: Not recognizable instruction: %s.\n", + inputline); free(Q); free(inputline); exit(-1); @@ -1715,66 +1945,56 @@ void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, Dd inputline[icur] = buf; icur += 1; if (icur == _maxbufsize) { - fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); + fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", + _maxbufsize); free(Q); free(inputline); exit(-1); } while (icur > maxlinesize - 1) { maxlinesize *= 2; - inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); + inputline = (char *)realloc(inputline, sizeof(char) * maxlinesize); } } - } while(iloop); + } while (iloop); free(Q); free(inputline); } -DdNode * equality(DdManager *mgr,int varIndex,int value,namedvars varmap) -{ +DdNode *equality(DdManager *mgr, int varIndex, int value, namedvars varmap) { - int i; - int bit,*booleanVars,booleanVar; - variable v; - DdNode * node, * tmp; + int i; + int bit, *booleanVars, booleanVar; + variable v; + DdNode *node, *tmp; + v = varmap.mvars[varIndex]; + booleanVars = v.booleanVars; + i = v.nBit - 1; + booleanVar = booleanVars[i]; + bit = value & 01; + if (bit) { + node = Cudd_bddIthVar(mgr, booleanVar); + } else { + node = Cudd_Not(Cudd_bddIthVar(mgr, booleanVar)); + } + value = value >> 1; + i--; - v=varmap.mvars[varIndex]; - booleanVars=v.booleanVars; - i=v.nBit-1; - booleanVar=booleanVars[i]; - bit=value & 01; - if (bit) - { - node=Cudd_bddIthVar(mgr, booleanVar); - } - else - { - node=Cudd_Not(Cudd_bddIthVar(mgr, booleanVar)); - } - value=value>>1; - i--; - - while (i>=0) { - booleanVar=booleanVars[i]; - bit=value & 01; - if (bit) - { - tmp=Cudd_bddAnd(mgr,node,Cudd_bddIthVar(mgr, booleanVar)); - Cudd_Ref(tmp); - } - else - { - tmp=Cudd_bddAnd(mgr,node,Cudd_Not(Cudd_bddIthVar(mgr, booleanVar))); - Cudd_Ref(tmp); - } - value=value>>1; - i--; - Cudd_RecursiveDeref(mgr,node); - node=tmp; - } -return node; + while (i >= 0) { + booleanVar = booleanVars[i]; + bit = value & 01; + if (bit) { + tmp = Cudd_bddAnd(mgr, node, Cudd_bddIthVar(mgr, booleanVar)); + Cudd_Ref(tmp); + } else { + tmp = Cudd_bddAnd(mgr, node, Cudd_Not(Cudd_bddIthVar(mgr, booleanVar))); + Cudd_Ref(tmp); + } + value = value >> 1; + i--; + Cudd_RecursiveDeref(mgr, node); + node = tmp; + } + return node; } - - - diff --git a/packages/cplint/approx/simplecuddLPADs/simplecudd.h b/packages/cplint/approx/simplecuddLPADs/simplecudd.h index e11da0422..96b31188f 100644 --- a/packages/cplint/approx/simplecuddLPADs/simplecudd.h +++ b/packages/cplint/approx/simplecuddLPADs/simplecudd.h @@ -185,19 +185,18 @@ \******************************************************************************/ /* modified by Fabrizio Riguzzi in 2009 for dealing with multivalued variables -instead of variables or their negation, the script can contain equations of the +instead of variables or their negation, the script can contain equations of the form variable=value */ - +#include "config.h" +#include "cudd_config.h" +#include #include #include #include -#include #include -#include "config.h" -#include "cudd_config.h" #if HAVE_UTIL_H #include #endif @@ -218,26 +217,27 @@ variable=value #endif #include "general.h" -#define IsHigh(manager, node) HIGH(manager) == node -#define IsLow(manager, node) LOW(manager) == node -#define HIGH(manager) Cudd_ReadOne(manager) -#define LOW(manager) Cudd_Not(Cudd_ReadOne(manager)) -#define NOT(node) Cudd_Not(node) -#define GetIndex(node) Cudd_NodeReadIndex(node) -#define GetMVar(manager, index, value, varmap) equality(manager,index,value,varmap)//Cudd_bddIthVar(manager, index) +#define IsHigh(manager, node) HIGH(manager) == node +#define IsLow(manager, node) LOW(manager) == node +#define HIGH(manager) Cudd_ReadOne(manager) +#define LOW(manager) Cudd_Not(Cudd_ReadOne(manager)) +#define NOT(node) Cudd_Not(node) +#define GetIndex(node) Cudd_NodeReadIndex(node) +#define GetMVar(manager, index, value, varmap) \ + equality(manager, index, value, varmap) // Cudd_bddIthVar(manager, index) #define GetVar(manager, index) Cudd_bddIthVar(manager, index) -#define NewVar(manager) Cudd_bddNewVar(manager) -#define KillBDD(manager) Cudd_Quit(manager) -#define GetVarCount(manager) Cudd_ReadSize(manager) -#define DEBUGON _debug = 1 -#define DEBUGOFF _debug = 0 -#define RAPIDLOADON _RapidLoad = 1 -#define RAPIDLOADOFF _RapidLoad = 0 -#define SETMAXBUFSIZE(size) _maxbufsize = size -#define BDDFILE_ERROR -1 -#define BDDFILE_OTHER 0 -#define BDDFILE_SCRIPT 1 -#define BDDFILE_NODEDUMP 2 +#define NewVar(manager) Cudd_bddNewVar(manager) +#define KillBDD(manager) Cudd_Quit(manager) +#define GetVarCount(manager) Cudd_ReadSize(manager) +#define DEBUGON _debug = 1 +#define DEBUGOFF _debug = 0 +#define RAPIDLOADON _RapidLoad = 1 +#define RAPIDLOADOFF _RapidLoad = 0 +#define SETMAXBUFSIZE(size) _maxbufsize = size +#define BDDFILE_ERROR -1 +#define BDDFILE_OTHER 0 +#define BDDFILE_SCRIPT 1 +#define BDDFILE_NODEDUMP 2 extern int _RapidLoad; extern int _debug; @@ -253,11 +253,10 @@ typedef struct _bddfileheader { int filetype; } bddfileheader; -typedef struct - { -int nVal,nBit,init; -double * probabilities; -int * booleanVars; +typedef struct { + int nVal, nBit, init; + double *probabilities; + int *booleanVars; } variable; typedef struct _namedvars { @@ -268,11 +267,10 @@ typedef struct _namedvars { double *dvalue; int *ivalue; void **dynvalue; - variable * mvars; - int * bVar2mVar; + variable *mvars; + int *bVar2mVar; } namedvars; - typedef struct _hisnode { DdNode *key; double dvalue; @@ -296,27 +294,31 @@ typedef struct _nodeline { /* Initialization */ -DdManager* simpleBDDinit(int varcnt); +DdManager *simpleBDDinit(int varcnt); /* BDD Generation */ -DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2); -DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2); -DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2); -DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2); -DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2); -DdNode* D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2); +DdNode *D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2); +DdNode *D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2); +DdNode *D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2); +DdNode *D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2); +DdNode *D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2); +DdNode *D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2); -DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader); -DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap); -DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline); -DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline); -DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper); +DdNode *FileGenerateBDD(DdManager *manager, namedvars varmap, + bddfileheader fileheader); +DdNode *OnlineGenerateBDD(DdManager *manager, namedvars *varmap); +DdNode *LineParser(DdManager *manager, namedvars varmap, DdNode **inter, + int maxinter, char *function, int iline); +DdNode *OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, + int maxinter, char *function, int iline); +DdNode *BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, + char Operator, int inegoper); int getInterBDD(char *function); -char* getFileName(const char *function); +char *getFileName(const char *function); int GetParam(char *inputline, int iParam); int LoadVariableData(namedvars varmap, char *filename); -int LoadMultiVariableData(DdManager * mgr,namedvars varmap, char *filename); +int LoadMultiVariableData(DdManager *mgr, namedvars varmap, char *filename); /* Named variables */ @@ -325,48 +327,61 @@ namedvars InitNamedMultiVars(int varcnt, int varstart, int bvarcnt); void EnlargeNamedVars(namedvars *varmap, int newvarcnt); int AddNamedVarAt(namedvars varmap, const char *varname, int index); int AddNamedVar(namedvars varmap, const char *varname); -int AddNamedMultiVar(DdManager *mgr,namedvars varmap, const char *varnamei, int *value); -void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, void *dynvalue); -int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int ivalue, void *dynvalue); +int AddNamedMultiVar(DdManager *mgr, namedvars varmap, const char *varnamei, + int *value); +void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, + void *dynvalue); +int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, + int ivalue, void *dynvalue); int GetNamedVarIndex(const namedvars varmap, const char *varname); int RepairVarcnt(namedvars *varmap); -char* GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node); -char* GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node); +char *GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node); +char *GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node); int all_loaded(namedvars varmap, int disp); /* Traversal */ -DdNode* HighNodeOf(DdManager *manager, DdNode *node); -DdNode* LowNodeOf(DdManager *manager, DdNode *node); +DdNode *HighNodeOf(DdManager *manager, DdNode *node); +DdNode *LowNodeOf(DdManager *manager, DdNode *node); /* Traversal - History */ -hisqueue* InitHistory(int varcnt); +hisqueue *InitHistory(int varcnt); void ReInitHistory(hisqueue *HisQueue, int varcnt); -void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue); -hisnode* GetNode(hisqueue *HisQueue, int varstart, DdNode *node); +void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, + int ivalue, void *dynvalue); +hisnode *GetNode(hisqueue *HisQueue, int varstart, DdNode *node); int GetNodeIndex(hisqueue *HisQueue, int varstart, DdNode *node); -void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, DdNode *bdd); +void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, + DdNode *bdd); /* Save-load */ bddfileheader ReadFileHeader(char *filename); int CheckFileVersion(const char *version); -DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile); -DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current); -DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum); +DdNode *LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile); +DdNode *LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, + FILE *inputfile, nodeline current); +DdNode *GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, + char *varname, int nodenum); -int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename); -void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile); +int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, + char *filename); +void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, + DdNode *Current, FILE *outputfile); void ExpandNodes(hisqueue *Nodes, int index, int nodenum); /* Export */ int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename); -int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename); +int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, + char *filename); -DdNode * equality(DdManager *mgr,int varIndex,int value,namedvars varmap); -hisnode* GetNodei1(int *bVar2mVar,hisqueue *HisQueue, int varstart, DdNode *node); -void AddNode1(int *bVar2mVar, hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue); -hisnode* GetNode1(int *bVar2mVar,hisqueue *HisQueue, int varstart, DdNode *node); +DdNode *equality(DdManager *mgr, int varIndex, int value, namedvars varmap); +hisnode *GetNodei1(int *bVar2mVar, hisqueue *HisQueue, int varstart, + DdNode *node); +void AddNode1(int *bVar2mVar, hisqueue *HisQueue, int varstart, DdNode *node, + double dvalue, int ivalue, void *dynvalue); +hisnode *GetNode1(int *bVar2mVar, hisqueue *HisQueue, int varstart, + DdNode *node); diff --git a/packages/swig/android/JavaYap.java b/packages/swig/android/JavaYap.java index 4f35f20d1..5f1ed79be 100644 --- a/packages/swig/android/JavaYap.java +++ b/packages/swig/android/JavaYap.java @@ -1,4 +1,3 @@ -package pt.up.fc.dcc.yap; /**** using sqlite For example,the following: @@ -25,6 +24,9 @@ The SQLiteStatement.simpleQueryForBlobFileDescriptor() API is not available. The ****/ +import pt.up.fc.dcc.Yap.*; + + import android.app.Activity; import android.os.Bundle; import android.view.View; @@ -45,12 +47,14 @@ import org.sqlite.database.sqlite.SQLiteOpenHelper; import org.sqlite.database.SQLException; import org.sqlite.database.DatabaseErrorHandler; + class DoNotDeleteErrorHandler implements DatabaseErrorHandler { private static final String TAG = "DoNotDeleteErrorHandler"; public void onCorruption(SQLiteDatabase dbObj) { Log.e(TAG, "Corruption reported by sqlite on database: " + dbObj.getPath()); } } + public class JavaYap extends Activity { TextView outputText = null; @@ -242,8 +246,7 @@ public class JavaYap extends Activity System.loadLibrary("android"); System.loadLibrary("log"); System.loadLibrary("gmp"); - System.loadLibrary("sqliteX"); - System.loadLibrary("example"); + System.loadLibrary("YapDroid"); } private static native void load(AssetManager mgr); diff --git a/pl/boot.yap b/pl/boot.yap index 4aa439bc8..eaa54c263 100644 --- a/pl/boot.yap +++ b/pl/boot.yap @@ -1360,6 +1360,12 @@ not(G) :- \+ '$execute'(G). '$check_callable'(_,_). +'$bootstrap' :- + bootstrap('init.yap'). + module(user), + '$live'. + + bootstrap(F) :- % '$open'(F, '$csult', Stream, 0, 0, F), % '$file_name'(Stream,File),