diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

adds

Browse Source
This commit is contained in:
vscosta 2016-04-05 02:52:50 +01:00
parent a5951daea9
commit 4d3d9c408d
11 changed files with 1161 additions and 1225 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
Eclipse/packages/bdd/cudd_config.h
View File

@ -1,32 +0,0 @@
// cmake template file
/* Define to 1 if you have the <cuddInt.h> header file. */
#ifndef HAVE_CUDDINT_H
/* #undef HAVE_CUDDINT_H */
#endif
/* Define to 1 if you have the <cudd/cuddInt.h> header file. */
#ifndef HAVE_CUDD_CUDDINT_H
#define HAVE_CUDD_CUDDINT_H 1
#endif
/* Define to 1 if you have the <cudd/cudd.h> header file. */
#ifndef HAVE_CUDD_CUDD_H
#define HAVE_CUDD_CUDD_H 1
#endif
/*Define to 1 if you have the <cudd.h> header file. */
#ifndef HAVE_CUDD_H
/* #undef HAVE_CUDD_H */
#endif
/* Define to 1 if you have the <cudd/util.h> header file. */
#ifndef HAVE_CUDD_UTIL_H
#define HAVE_CUDD_UTIL_H 1
#endif
/* Define to 1 if you have the <util.h> header file. */
#ifndef HAVE_UTIL_H
#define HAVE_UTIL_H 1
#endif

2
Eclipse/packages/raptor/raptor_config.h
View File

@ -1,2 +0,0 @@
#define HAVE_RAPTOR2_RAPTOR2_H 1
/* #undef HAVE_RAPTOR_H */

26
Eclipse/packages/real/rconfig.h
View File

@ -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 <alloca.h> header file. */
#ifndef HAVE_R_H
#define HAVE_R_H 1
#endif
/* Define to 1 if you have the <alloca.h> header file. */
#ifndef HAVE_R_EMBEDDED_H
#define HAVE_R_EMBEDDED_H 1
#endif
/* Define to 1 if you have the <alloca.h> header file. */
#ifndef HAVE_R_INTERFACE_H
#define HAVE_R_INTERFACE_H 1
#endif
#endif

2
Eclipse/library/system/sys_config.h → cmake/library/system/sys_config.h
View File

@ -5,7 +5,7 @@
/* Define to 1 if you have the <openssl/ripemd.h> header file. */ /* Define to 1 if you have the <openssl/ripemd.h> header file. */
#ifndef HAVE_APR_1_APR_MD5_H #ifndef HAVE_APR_1_APR_MD5_H
#define HAVE_APR_1_APR_MD5_H 1 /* #undef HAVE_APR_1_APR_MD5_H */
#endif #endif

24
Eclipse/os/YapIOConfig.h → cmake/os/YapIOConfig.h
View File

@ -1,16 +1,16 @@
/* Define if you have libreadline */ /* Define if you have libreadline */
#ifndef HAVE_LIBREADLINE #ifndef HAVE_LIBREADLINE
#define HAVE_LIBREADLINE 1 /* #undef HAVE_LIBREADLINE */
#endif #endif
/* Define to 1 if you have the <readline/history.h> header file. */ /* Define to 1 if you have the <readline/history.h> header file. */
#ifndef HAVE_READLINE_HISTORY_H #ifndef HAVE_READLINE_HISTORY_H
#define HAVE_READLINE_HISTORY_H 1 /* #undef HAVE_READLINE_HISTORY_H */
#endif #endif
/* Define to 1 if you have the <readline/readline.h> header file. */ /* Define to 1 if you have the <readline/readline.h> header file. */
#ifndef HAVE_READLINE_READLINE_H #ifndef HAVE_READLINE_READLINE_H
#define HAVE_READLINE_READLINE_H 1 /* #undef HAVE_READLINE_READLINE_H */
#endif #endif
#if defined(HAVE_LIBREADLINE) && defined(HAVE_READLINE_READLINE_H) #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. */ /* Define to 1 if you have the `rl_begin_undo_group' function. */
#ifndef HAVE_RL_BEGIN_UNDO_GROUP #ifndef HAVE_RL_BEGIN_UNDO_GROUP
#define HAVE_RL_BEGIN_UNDO_GROUP 1 /* #undef HAVE_RL_BEGIN_UNDO_GROUP */
#endif #endif
/* Define to 1 if you have the `rl_clear_pending_input' function. */ /* Define to 1 if you have the `rl_clear_pending_input' function. */
#ifndef HAVE_RL_CLEAR_PENDING_INPUT #ifndef HAVE_RL_CLEAR_PENDING_INPUT
#define HAVE_RL_CLEAR_PENDING_INPUT 1 /* #undef HAVE_RL_CLEAR_PENDING_INPUT */
#endif #endif
/* Define to 1 if the system has the type `rl_completion_func_t'). */ /* 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. */ /* Define to 1 if you have the `rl_discard_argument' function. */
#ifndef HAVE_RL_DISCARD_ARGUMENT #ifndef HAVE_RL_DISCARD_ARGUMENT
#define HAVE_RL_DISCARD_ARGUMENT 1 /* #undef HAVE_RL_DISCARD_ARGUMENT */
#endif #endif
/* Define to 1 if you have the `rl_done' variable. */ /* 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. */ /* Define to 1 if you have the `rl_filename_completion_function' function. */
#ifndef HAVE_RL_FILENAME_COMPLETION_FUNCTION #ifndef HAVE_RL_FILENAME_COMPLETION_FUNCTION
#define HAVE_RL_FILENAME_COMPLETION_FUNCTION 1 #define HAVE_RL_FILENAME_COMPLETION_FUNCTION
#endif #endif
/* Define to 1 if you have the `rl_free_line_state' function. */ /* Define to 1 if you have the `rl_free_line_state' function. */
#ifndef HAVE_RL_FREE_LINE_STATE #ifndef HAVE_RL_FREE_LINE_STATE
#define HAVE_RL_FREE_LINE_STATE 1 /* #undef HAVE_RL_FREE_LINE_STATE */
#endif #endif
/* Define to 1 if the system has the type `rl_hook_func_t'. */ /* 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. */ /* Define to 1 if you have the `rl_insert_close' function. */
#ifndef HAVE_RL_INSERT_CLOSE #ifndef HAVE_RL_INSERT_CLOSE
#define HAVE_RL_INSERT_CLOSE 1 /* #undef HAVE_RL_INSERT_CLOSE */
#endif #endif
/* Define to 1 if you have the `rl_reset_after_signal' function. */ /* Define to 1 if you have the `rl_reset_after_signal' function. */
#ifndef HAVE_RL_RESET_AFTER_SIGNAL #ifndef HAVE_RL_RESET_AFTER_SIGNAL
#define HAVE_RL_RESET_AFTER_SIGNAL 1 /* #undef HAVE_RL_RESET_AFTER_SIGNAL */
#endif #endif
/* Define to 1 if you have the `rl_set_keyboard_input_timeout' function. */ /* Define to 1 if you have the `rl_set_keyboard_input_timeout' function. */
#ifndef HAVE_RL_SET_KEYBOARD_INPUT_TIMEOUT #ifndef HAVE_RL_SET_KEYBOARD_INPUT_TIMEOUT
#define HAVE_RL_SET_KEYBOARD_INPUT_TIMEOUT 1 /* #undef HAVE_RL_SET_KEYBOARD_INPUT_TIMEOUT */
#endif #endif
/* Define to 1 if you have the `rl_set_prompt' function. */ /* Define to 1 if you have the `rl_set_prompt' function. */
#ifndef HAVE_RL_SET_PROMPT #ifndef HAVE_RL_SET_PROMPT
#define HAVE_RL_SET_PROMPT 1 /* #undef HAVE_RL_SET_PROMPT */
#endif #endif

183
packages/bdd/cmake/FindCUDD.cmake
View File

@ -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, <montel@kde.org>
#
# 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

461
packages/bdd/cudd.c
View File

@ -4,7 +4,10 @@
@brief Interface to the CUDD Library @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 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 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 <stdio.h> #include <stdio.h>
#include "YapInterface.h"
#include "config.h" #include "config.h"
#include "cudd_config.h" #include "cudd_config.h"
#include "YapInterface.h"
#if HAVE_CUDD_UTIL_H #if HAVE_CUDD_UTIL_H
#include <cudd/util.h> #include <cudd/util.h>
@ -52,81 +55,57 @@ CUDD will generate better/faster code.
#include "cudd.h" #include "cudd.h"
#endif #endif
static YAP_Functor FunctorDollarVar, static YAP_Functor FunctorDollarVar, FunctorCudd, FunctorAnd, FunctorAnd4,
FunctorCudd, FunctorOr, FunctorOr4, FunctorLAnd, FunctorLOr, FunctorNot, FunctorMinus1,
FunctorAnd, FunctorXor, FunctorNand, FunctorNor, FunctorTimes, FunctorImplies,
FunctorAnd4, FunctorPlus, FunctorMinus, FunctorTimes4, FunctorPlus4, FunctorOutAdd,
FunctorOr, FunctorOutPos, FunctorOutNeg;
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; static YAP_Term TermMinusOne, TermZero, TermPlusOne, TermTrue, TermFalse;
void init_cudd(void); void init_cudd(void);
static DdNode * static DdNode *cudd_and(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
cudd_and(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
DdNode *tmp; DdNode *tmp;
tmp = Cudd_bddAnd(manager, bdd1, bdd2); tmp = Cudd_bddAnd(manager, bdd1, bdd2);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *cudd_nand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
cudd_nand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
DdNode *tmp; DdNode *tmp;
tmp = Cudd_bddNand(manager, bdd1, bdd2); tmp = Cudd_bddNand(manager, bdd1, bdd2);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *cudd_or(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
cudd_or(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
DdNode *tmp; DdNode *tmp;
tmp = Cudd_bddOr(manager, bdd1, bdd2); tmp = Cudd_bddOr(manager, bdd1, bdd2);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *cudd_nor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
cudd_nor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
DdNode *tmp; DdNode *tmp;
tmp = Cudd_bddNor(manager, bdd1, bdd2); tmp = Cudd_bddNor(manager, bdd1, bdd2);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *cudd_xor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
cudd_xor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) {
DdNode *tmp; DdNode *tmp;
tmp = Cudd_bddXor(manager, bdd1, bdd2); tmp = Cudd_bddXor(manager, bdd1, bdd2);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *term_to_cudd(DdManager *manager, YAP_Term t) {
term_to_cudd(DdManager *manager, YAP_Term t)
{
if (YAP_IsApplTerm(t)) { if (YAP_IsApplTerm(t)) {
YAP_Functor f = YAP_FunctorOfTerm(t); YAP_Functor f = YAP_FunctorOfTerm(t);
if (f == FunctorDollarVar) { if (f == FunctorDollarVar) {
int i = YAP_IntOfTerm(YAP_ArgOfTerm(1,t)); int i = YAP_IntOfTerm(YAP_ArgOfTerm(1, t));
DdNode *var = Cudd_bddIthVar(manager,i); DdNode *var = Cudd_bddIthVar(manager, i);
if (!var) if (!var)
return NULL; return NULL;
Cudd_Ref(var); Cudd_Ref(var);
@ -138,8 +117,8 @@ term_to_cudd(DdManager *manager, YAP_Term t)
if (!x1 || !x2) if (!x1 || !x2)
return NULL; return NULL;
tmp = cudd_and(manager, x1, x2); tmp = cudd_and(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorAnd4) { } else if (f == FunctorAnd4) {
YAP_Term t1 = YAP_ArgOfTerm(2, t); YAP_Term t1 = YAP_ArgOfTerm(2, t);
@ -151,11 +130,11 @@ term_to_cudd(DdManager *manager, YAP_Term t)
if (!x1 || !x2) if (!x1 || !x2)
return NULL; return NULL;
tmp = cudd_and(manager, x1, x2); tmp = cudd_and(manager, x1, x2);
for (i=0 ; i < refs; i++) { for (i = 0; i < refs; i++) {
Cudd_Ref(tmp); Cudd_Ref(tmp);
} }
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp));
return tmp; return tmp;
} else { } else {
@ -173,8 +152,8 @@ term_to_cudd(DdManager *manager, YAP_Term t)
if (!x1 || !x2) if (!x1 || !x2)
return NULL; return NULL;
tmp = cudd_or(manager, x1, x2); tmp = cudd_or(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorXor) { } else if (f == FunctorXor) {
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t));
@ -183,8 +162,8 @@ term_to_cudd(DdManager *manager, YAP_Term t)
if (!x1 || !x2) if (!x1 || !x2)
return NULL; return NULL;
tmp = cudd_xor(manager, x1, x2); tmp = cudd_xor(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorOr4) { } else if (f == FunctorOr4) {
YAP_Term t1 = YAP_ArgOfTerm(2, t); YAP_Term t1 = YAP_ArgOfTerm(2, t);
@ -196,11 +175,11 @@ term_to_cudd(DdManager *manager, YAP_Term t)
if (!x1 || !x2) if (!x1 || !x2)
return NULL; return NULL;
tmp = cudd_or(manager, x1, x2); tmp = cudd_or(manager, x1, x2);
for (i=0 ; i < refs; i++) { for (i = 0; i < refs; i++) {
Cudd_Ref(tmp); Cudd_Ref(tmp);
} }
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp));
return tmp; return tmp;
} else { } else {
@ -213,8 +192,8 @@ term_to_cudd(DdManager *manager, YAP_Term t)
if (!x1 || !x2) if (!x1 || !x2)
return NULL; return NULL;
tmp = cudd_nor(manager, x1, x2); tmp = cudd_nor(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorNand) { } else if (f == FunctorNand) {
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t));
@ -222,8 +201,8 @@ term_to_cudd(DdManager *manager, YAP_Term t)
if (!x1 || !x2) if (!x1 || !x2)
return NULL; return NULL;
DdNode *tmp = cudd_nand(manager, x1, x2); DdNode *tmp = cudd_nand(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorNot || FunctorMinus1) { } else if (f == FunctorNot || FunctorMinus1) {
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t));
@ -238,7 +217,7 @@ term_to_cudd(DdManager *manager, YAP_Term t)
YAP_Int i = YAP_IntOfTerm(t); YAP_Int i = YAP_IntOfTerm(t);
if (i == 0) if (i == 0)
return Cudd_ReadLogicZero(manager); return Cudd_ReadLogicZero(manager);
else if (i==1) else if (i == 1)
return Cudd_ReadOne(manager); return Cudd_ReadOne(manager);
else { else {
YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD"); 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); YAP_Int i = YAP_FloatOfTerm(t);
if (i == 0.0) if (i == 0.0)
return Cudd_ReadLogicZero(manager); return Cudd_ReadLogicZero(manager);
else if (i==1.0) else if (i == 1.0)
return Cudd_ReadOne(manager); return Cudd_ReadOne(manager);
else { else {
YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD"); YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD");
@ -260,7 +239,8 @@ term_to_cudd(DdManager *manager, YAP_Term t)
else if (t == TermTrue) else if (t == TermTrue)
return Cudd_ReadOne(manager); return Cudd_ReadOne(manager);
else { 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; return NULL;
} }
} else if (YAP_IsVarTerm(t)) { } else if (YAP_IsVarTerm(t)) {
@ -271,15 +251,13 @@ term_to_cudd(DdManager *manager, YAP_Term t)
return NULL; return NULL;
} }
static YAP_Bool static YAP_Bool p_term_to_cudd(void) {
p_term_to_cudd(void)
{
DdManager *manager; DdManager *manager;
DdNode *t; DdNode *t;
if (YAP_IsVarTerm(YAP_ARG2)) { if (YAP_IsVarTerm(YAP_ARG2)) {
manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
//Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT); // Cudd_AutodynEnable(manager, CUDD_REORDER_SIFT);
if (!YAP_Unify(YAP_ARG2, YAP_MkIntTerm((YAP_Int)manager))) if (!YAP_Unify(YAP_ARG2, YAP_MkIntTerm((YAP_Int)manager)))
return FALSE; return FALSE;
} else { } else {
@ -288,76 +266,63 @@ p_term_to_cudd(void)
t = term_to_cudd(manager, YAP_ARG1); t = term_to_cudd(manager, YAP_ARG1);
if (!t) if (!t)
return FALSE; return FALSE;
return return YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t));
YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t));
} }
static DdNode * static DdNode *add_times(DdManager *manager, DdNode *x1, DdNode *x2) {
add_times(DdManager *manager, DdNode *x1, DdNode *x2)
{
DdNode *tmp; DdNode *tmp;
tmp = Cudd_addApply(manager,Cudd_addTimes,x2,x1); tmp = Cudd_addApply(manager, Cudd_addTimes, x2, x1);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *add_implies(DdManager *manager, DdNode *x1, DdNode *x2) {
add_implies(DdManager *manager, DdNode *x1, DdNode *x2)
{
DdNode *tmp; DdNode *tmp;
tmp = Cudd_addConst(manager,Cudd_addLeq(manager,x1,x2)); tmp = Cudd_addConst(manager, Cudd_addLeq(manager, x1, x2));
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *add_plus(DdManager *manager, DdNode *x1, DdNode *x2) {
add_plus(DdManager *manager, DdNode *x1, DdNode *x2)
{
DdNode *tmp; DdNode *tmp;
tmp = Cudd_addApply(manager,Cudd_addPlus,x2,x1); tmp = Cudd_addApply(manager, Cudd_addPlus, x2, x1);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *add_minus(DdManager *manager, DdNode *x1, DdNode *x2) {
add_minus(DdManager *manager, DdNode *x1, DdNode *x2)
{
DdNode *tmp; DdNode *tmp;
tmp = Cudd_addApply(manager,Cudd_addMinus,x1,x2); tmp = Cudd_addApply(manager, Cudd_addMinus, x1, x2);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *add_lor(DdManager *manager, DdNode *x1, DdNode *x2) {
add_lor(DdManager *manager, DdNode *x1, DdNode *x2)
{
DdNode *tmp; DdNode *tmp;
tmp = Cudd_addApply(manager,Cudd_addOr,x1,x2); tmp = Cudd_addApply(manager, Cudd_addOr, x1, x2);
Cudd_Ref(tmp); Cudd_Ref(tmp);
return tmp; return tmp;
} }
static DdNode * static DdNode *term_to_add(DdManager *manager, YAP_Term t) {
term_to_add(DdManager *manager, YAP_Term t)
{
if (YAP_IsApplTerm(t)) { if (YAP_IsApplTerm(t)) {
YAP_Functor f = YAP_FunctorOfTerm(t); YAP_Functor f = YAP_FunctorOfTerm(t);
if (f == FunctorDollarVar) { if (f == FunctorDollarVar) {
int i = YAP_IntOfTerm(YAP_ArgOfTerm(1,t)); int i = YAP_IntOfTerm(YAP_ArgOfTerm(1, t));
DdNode *var = Cudd_addIthVar(manager,i); DdNode *var = Cudd_addIthVar(manager, i);
return var; return var;
} else if (f == FunctorTimes) { } else if (f == FunctorTimes) {
DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t));
DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = add_times(manager, x1, x2); DdNode *tmp = add_times(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorTimes4) { } else if (f == FunctorTimes4) {
YAP_Term t1 = YAP_ArgOfTerm(2, t); YAP_Term t1 = YAP_ArgOfTerm(2, t);
@ -367,11 +332,11 @@ term_to_add(DdManager *manager, YAP_Term t)
DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t));
DdNode *tmp = add_times(manager, x1, x2); DdNode *tmp = add_times(manager, x1, x2);
for (i=0 ; i < refs; i++) { for (i = 0; i < refs; i++) {
Cudd_Ref(tmp); Cudd_Ref(tmp);
} }
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp));
return tmp; return tmp;
} else { } else {
@ -382,32 +347,32 @@ term_to_add(DdManager *manager, YAP_Term t)
DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = add_plus(manager, x1, x2); DdNode *tmp = add_plus(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorLOr || f == FunctorOr) { } else if (f == FunctorLOr || f == FunctorOr) {
DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t));
DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = add_lor(manager, x1, x2); DdNode *tmp = add_lor(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorMinus) { } else if (f == FunctorMinus) {
DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t));
DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = add_minus(manager, x1, x2); DdNode *tmp = add_minus(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorImplies) { } else if (f == FunctorImplies) {
DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_add(manager, YAP_ArgOfTerm(1, t));
DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = add_implies(manager, x1, x2); DdNode *tmp = add_implies(manager, x1, x2);
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
return tmp; return tmp;
} else if (f == FunctorTimes4) { } else if (f == FunctorTimes4) {
YAP_Term t1 = YAP_ArgOfTerm(2, t); YAP_Term t1 = YAP_ArgOfTerm(2, t);
@ -417,11 +382,11 @@ term_to_add(DdManager *manager, YAP_Term t)
DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t)); DdNode *x2 = term_to_add(manager, YAP_ArgOfTerm(4, t));
DdNode *tmp = add_plus(manager, x1, x2); DdNode *tmp = add_plus(manager, x1, x2);
for (i=0 ; i < refs; i++) { for (i = 0; i < refs; i++) {
Cudd_Ref(tmp); Cudd_Ref(tmp);
} }
Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager, x1);
Cudd_RecursiveDeref(manager,x2); Cudd_RecursiveDeref(manager, x2);
YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp)); YAP_Unify(t1, YAP_MkIntTerm((YAP_Int)tmp));
return tmp; return tmp;
} else { } else {
@ -444,13 +409,11 @@ term_to_add(DdManager *manager, YAP_Term t)
return NULL; return NULL;
} }
static YAP_Bool static YAP_Bool p_term_to_add(void) {
p_term_to_add(void) DdManager *manager = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
{
DdManager *manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0);
int sz = YAP_IntOfTerm(YAP_ARG2), i; int sz = YAP_IntOfTerm(YAP_ARG2), i;
DdNode *t; DdNode *t;
for (i = sz-1; i >= 0; i--) { for (i = sz - 1; i >= 0; i--) {
Cudd_addIthVar(manager, i); Cudd_addIthVar(manager, i);
} }
t = term_to_add(manager, YAP_ARG1); t = term_to_add(manager, YAP_ARG1);
@ -458,23 +421,19 @@ p_term_to_add(void)
YAP_Unify(YAP_ARG4, YAP_MkIntTerm((YAP_Int)t)); YAP_Unify(YAP_ARG4, YAP_MkIntTerm((YAP_Int)t));
} }
static YAP_Bool complement(int i) static YAP_Bool complement(int i) { return i == 0 ? 1 : 0; }
{
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 ) { static YAP_Bool cudd_eval(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 )
{
if (Cudd_IsConstant(n)) { if (Cudd_IsConstant(n)) {
// fprintf(stderr,"v=%f\n",Cudd_V(n)); // fprintf(stderr,"v=%f\n",Cudd_V(n));
return Cudd_V(n); return Cudd_V(n);
} else { } 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) if (var(manager, n, vals) == 1)
return cudd_eval(manager, Cudd_T(n), vals); return cudd_eval(manager, Cudd_T(n), vals);
else { else {
@ -488,9 +447,7 @@ cudd_eval(DdManager *manager, DdNode *n, YAP_Int *vals )
} }
} }
static YAP_Bool static YAP_Bool cudd_eval_top(DdManager *manager, DdNode *n, YAP_Int *vals) {
cudd_eval_top(DdManager *manager, DdNode *n, YAP_Int *vals )
{
if (Cudd_IsComplement(n)) { if (Cudd_IsComplement(n)) {
return complement(cudd_eval(manager, Cudd_Regular(n), vals)); return complement(cudd_eval(manager, Cudd_Regular(n), vals));
} else { } else {
@ -498,9 +455,7 @@ cudd_eval_top(DdManager *manager, DdNode *n, YAP_Int *vals )
} }
} }
static YAP_Bool static YAP_Bool p_eval_cudd(void) {
p_eval_cudd(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n = (DdNode *)YAP_IntOfTerm(YAP_ARG2); 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));
@ -509,12 +464,13 @@ p_eval_cudd(void)
YAP_Term t = YAP_ARG3; YAP_Term t = YAP_ARG3;
YAP_Int i; YAP_Int i;
if (sz <= 0) return FALSE; if (sz <= 0)
ar = (YAP_Int*)malloc(sz*sizeof(YAP_Int)); return FALSE;
ar = (YAP_Int *)malloc(sz * sizeof(YAP_Int));
if (!ar) if (!ar)
return FALSE; return FALSE;
for (i= 0; i< sz; i++) { for (i = 0; i < sz; i++) {
YAP_Term tj = YAP_ArgOfTerm(i+1, t); YAP_Term tj = YAP_ArgOfTerm(i + 1, t);
if (!YAP_IsIntTerm(tj)) if (!YAP_IsIntTerm(tj))
return FALSE; return FALSE;
ar[i] = YAP_IntOfTerm(tj); ar[i] = YAP_IntOfTerm(tj);
@ -524,9 +480,7 @@ p_eval_cudd(void)
return YAP_Unify(YAP_ARG4, YAP_MkIntTerm(val)); return YAP_Unify(YAP_ARG4, YAP_MkIntTerm(val));
} }
static double static double add_eval(DdManager *manager, DdNode *n, YAP_Int *vals) {
add_eval(DdManager *manager, DdNode *n, YAP_Int *vals )
{
if (Cudd_IsConstant(n)) { if (Cudd_IsConstant(n)) {
return Cudd_V(n); return Cudd_V(n);
} else { } else {
@ -538,9 +492,7 @@ add_eval(DdManager *manager, DdNode *n, YAP_Int *vals )
} }
} }
static YAP_Bool static YAP_Bool p_eval_add(void) {
p_eval_add(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n = (DdNode *)YAP_IntOfTerm(YAP_ARG2); 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));
@ -549,12 +501,13 @@ p_eval_add(void)
YAP_Term t = YAP_ARG3; YAP_Term t = YAP_ARG3;
YAP_Int i; YAP_Int i;
if (sz <= 0) return FALSE; if (sz <= 0)
ar = (YAP_Int*)malloc(sz*sizeof(YAP_Int)); return FALSE;
ar = (YAP_Int *)malloc(sz * sizeof(YAP_Int));
if (!ar) if (!ar)
return FALSE; return FALSE;
for (i= 0; i< sz; i++) { for (i = 0; i < sz; i++) {
YAP_Term tj = YAP_ArgOfTerm(i+1, t); YAP_Term tj = YAP_ArgOfTerm(i + 1, t);
if (!YAP_IsIntTerm(tj)) if (!YAP_IsIntTerm(tj))
return FALSE; return FALSE;
ar[i] = YAP_IntOfTerm(tj); ar[i] = YAP_IntOfTerm(tj);
@ -569,41 +522,40 @@ typedef struct {
YAP_Term val; YAP_Term val;
} hash_table_entry; } hash_table_entry;
static void static void insert(hash_table_entry *p, DdNode *key, YAP_Term val, size_t sz) {
insert(hash_table_entry *p,DdNode *key, YAP_Term val, size_t sz) size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz;
{
size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz;
while (p[el].key) { while (p[el].key) {
el = (el+1)%sz; el = (el + 1) % sz;
} }
p[el].key = key; p[el].key = key;
p[el].val = val; p[el].val = val;
} }
static YAP_Term lookup(hash_table_entry *p, DdNode *key, size_t sz) static YAP_Term lookup(hash_table_entry *p, DdNode *key, size_t sz) {
{ size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz;
size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz;
while (p[el].key != key) { while (p[el].key != key) {
el = (el+1)%sz; el = (el + 1) % sz;
} }
return p[el].val; return p[el].val;
} }
static YAP_Term static YAP_Term build_prolog_cudd(DdManager *manager, DdNode *n, YAP_Term *ar,
build_prolog_cudd(DdManager *manager, DdNode *n, YAP_Term *ar, hash_table_entry *hash, YAP_Term t0, size_t sz) hash_table_entry *hash, YAP_Term t0,
{ size_t sz) {
if (Cudd_IsConstant(n)) { if (Cudd_IsConstant(n)) {
YAP_Term t = YAP_MkIntTerm(Cudd_V(n)); YAP_Term t = YAP_MkIntTerm(Cudd_V(n));
insert(hash, n, t, sz); insert(hash, n, t, sz);
return t0; return t0;
} else { } 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_Term t[4], nt;
YAP_Functor f; YAP_Functor f;
//fprintf(stderr,"refs=%d\n", n->ref); // fprintf(stderr,"refs=%d\n", n->ref);
t[0] = YAP_MkVarTerm(); 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[2] = lookup(hash, Cudd_T(n), sz);
t[3] = lookup(hash, Cudd_Regular(Cudd_E(n)), sz); t[3] = lookup(hash, Cudd_Regular(Cudd_E(n)), sz);
if (Cudd_IsComplement(Cudd_E(n))) { 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); nt = YAP_MkApplTerm(f, 4, t);
insert(hash, n, t[0], sz); insert(hash, n, t[0], sz);
return YAP_MkPairTerm(nt,t0); return YAP_MkPairTerm(nt, t0);
} }
} }
static inline int static inline int max(int a, int b) { return a < b ? b : a; }
max(int a, int b)
{
return a<b ? b : a;
}
static YAP_Int static YAP_Int get_vars(YAP_Term t3) {
get_vars(YAP_Term t3)
{
if (YAP_IsAtomTerm(t3)) if (YAP_IsAtomTerm(t3))
return 0; return 0;
return YAP_ArityOfFunctor(YAP_FunctorOfTerm(t3)); return YAP_ArityOfFunctor(YAP_FunctorOfTerm(t3));
} }
static YAP_Bool static YAP_Bool p_cudd_reorder(void) {
p_cudd_reorder(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
return Cudd_ReduceHeap( manager, CUDD_REORDER_EXACT, 1); return Cudd_ReduceHeap(manager, CUDD_REORDER_EXACT, 1);
} }
static YAP_Bool static YAP_Bool p_cudd_to_term(void) {
p_cudd_to_term(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node; DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node;
YAP_Term t, t3 = YAP_ARG3, td; YAP_Term t, t3 = YAP_ARG3, td;
YAP_Int i, vars = get_vars(t3); YAP_Int i, vars = get_vars(t3);
int nodes = max(0,Cudd_ReadNodeCount(manager))+vars+1; int nodes = max(0, Cudd_ReadNodeCount(manager)) + vars + 1;
size_t sz = nodes*4; size_t sz = nodes * 4;
DdGen *dgen = Cudd_FirstNode(manager, n0, &node); 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; YAP_Term *ar;
if (!dgen || !hash) if (!dgen || !hash)
return FALSE; return FALSE;
ar = (YAP_Term *)malloc(vars*sizeof(YAP_Term)); ar = (YAP_Term *)malloc(vars * sizeof(YAP_Term));
if (!ar) if (!ar)
return FALSE; return FALSE;
restart: restart:
t = YAP_TermNil(); t = YAP_TermNil();
for (i= 0; i< vars; i++) { for (i = 0; i < vars; i++) {
ar[i] = YAP_ArgOfTerm(i+1, t3); ar[i] = YAP_ArgOfTerm(i + 1, t3);
} }
while (node) { while (node) {
/* ensure we have enough memory */ /* ensure we have enough memory */
@ -667,7 +610,7 @@ p_cudd_to_term(void)
Cudd_GenFree(dgen); Cudd_GenFree(dgen);
t3 = YAP_ARG3; t3 = YAP_ARG3;
dgen = Cudd_FirstNode(manager, n0, &node); dgen = Cudd_FirstNode(manager, n0, &node);
bzero(hash, sizeof(hash_table_entry)*sz); bzero(hash, sizeof(hash_table_entry) * sz);
goto restart; goto restart;
} }
t = build_prolog_cudd(manager, node, ar, hash, t, sz); t = build_prolog_cudd(manager, node, ar, hash, t, sz);
@ -685,9 +628,9 @@ p_cudd_to_term(void)
return YAP_Unify(YAP_ARG4, td) && YAP_Unify(YAP_ARG5, t); return YAP_Unify(YAP_ARG4, td) && YAP_Unify(YAP_ARG5, t);
} }
static YAP_Term static YAP_Term build_prolog_add(DdManager *manager, DdNode *n, YAP_Term *ar,
build_prolog_add(DdManager *manager, DdNode *n, YAP_Term *ar, hash_table_entry *hash, YAP_Term t0, size_t sz) hash_table_entry *hash, YAP_Term t0,
{ size_t sz) {
if (Cudd_IsConstant(n)) { if (Cudd_IsConstant(n)) {
YAP_Term t = YAP_MkFloatTerm(Cudd_V(n)); YAP_Term t = YAP_MkFloatTerm(Cudd_V(n));
insert(hash, n, t, sz); insert(hash, n, t, sz);
@ -696,40 +639,39 @@ build_prolog_add(DdManager *manager, DdNode *n, YAP_Term *ar, hash_table_entry *
YAP_Term t[4], nt; YAP_Term t[4], nt;
YAP_Functor f; YAP_Functor f;
//fprintf(stderr,"refs=%d\n", n->ref); // fprintf(stderr,"refs=%d\n", n->ref);
t[0] = YAP_MkVarTerm(); 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[2] = lookup(hash, Cudd_T(n), sz);
t[3] = lookup(hash, Cudd_E(n), sz); t[3] = lookup(hash, Cudd_E(n), sz);
f = FunctorOutAdd; f = FunctorOutAdd;
nt = YAP_MkApplTerm(f, 4, t); nt = YAP_MkApplTerm(f, 4, t);
insert(hash, n, t[0], sz); insert(hash, n, t[0], sz);
return YAP_MkPairTerm(nt,t0); return YAP_MkPairTerm(nt, t0);
} }
} }
static YAP_Bool static YAP_Bool p_add_to_term(void) {
p_add_to_term(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node; DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node;
YAP_Term t, t3 = YAP_ARG3; YAP_Term t, t3 = YAP_ARG3;
YAP_Int i, vars = get_vars(t3); YAP_Int i, vars = get_vars(t3);
int nodes = max(0,Cudd_ReadNodeCount(manager))+vars+1; int nodes = max(0, Cudd_ReadNodeCount(manager)) + vars + 1;
size_t sz = nodes*4; size_t sz = nodes * 4;
DdGen *dgen = Cudd_FirstNode(manager, n0, &node); 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; YAP_Term *ar;
if (!dgen) if (!dgen)
return FALSE; return FALSE;
ar = (YAP_Term *)malloc(vars*sizeof(YAP_Term)); ar = (YAP_Term *)malloc(vars * sizeof(YAP_Term));
if (!ar) if (!ar)
return FALSE; return FALSE;
restart: restart:
t = YAP_TermNil(); t = YAP_TermNil();
for (i= 0; i< vars; i++) { for (i = 0; i < vars; i++) {
ar[i] = YAP_ArgOfTerm(i+1, t3); ar[i] = YAP_ArgOfTerm(i + 1, t3);
} }
while (node) { while (node) {
/* ensure we have enough memory */ /* ensure we have enough memory */
@ -737,7 +679,7 @@ p_add_to_term(void)
Cudd_GenFree(dgen); Cudd_GenFree(dgen);
t3 = YAP_ARG3; t3 = YAP_ARG3;
dgen = Cudd_FirstNode(manager, n0, &node); dgen = Cudd_FirstNode(manager, n0, &node);
bzero(hash, sizeof(hash_table_entry)*sz); bzero(hash, sizeof(hash_table_entry) * sz);
goto restart; goto restart;
} }
t = build_prolog_add(manager, node, ar, hash, t, sz); 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); return YAP_Unify(YAP_ARG4, t);
} }
static YAP_Bool static YAP_Bool p_cudd_size(void) {
p_cudd_size(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node; DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node;
YAP_Int i = 0; YAP_Int i = 0;
@ -774,67 +714,64 @@ typedef struct {
double val; double val;
} hash_table_entry_dbl; } hash_table_entry_dbl;
static void static void insert2(hash_table_entry_dbl *p, DdNode *key, double val,
insert2(hash_table_entry_dbl *p,DdNode *key, double val, size_t sz) size_t sz) {
{ size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz;
size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz;
while (p[el].key) { while (p[el].key) {
el = (el+1)%sz; el = (el + 1) % sz;
} }
p[el].key = key; p[el].key = key;
p[el].val = val; p[el].val = val;
} }
static double static double lookup2(hash_table_entry_dbl *p, DdNode *key, size_t sz) {
lookup2(hash_table_entry_dbl *p, DdNode *key, size_t sz) size_t el = (((YAP_Term)key) / sizeof(DdNode *)) % sz;
{
size_t el = (((YAP_Term)key)/sizeof(DdNode *)) % sz;
while (p[el].key != key) { while (p[el].key != key) {
el = (el+1)%sz; el = (el + 1) % sz;
} }
return p[el].val; return p[el].val;
} }
static double static double build_sp_cudd(DdManager *manager, DdNode *n, double *ar,
build_sp_cudd(DdManager *manager, DdNode *n, double *ar, hash_table_entry_dbl *hash, size_t sz) hash_table_entry_dbl *hash, size_t sz) {
{
if (Cudd_IsConstant(n)) { if (Cudd_IsConstant(n)) {
insert2(hash, n, Cudd_V(n), sz); insert2(hash, n, Cudd_V(n), sz);
return Cudd_V(n); return Cudd_V(n);
} else { } 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; 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); pl = lookup2(hash, Cudd_T(n), sz);
pr = lookup2(hash, Cudd_Regular(Cudd_E(n)), sz); pr = lookup2(hash, Cudd_Regular(Cudd_E(n)), sz);
if (Cudd_IsComplement(Cudd_E(n))) { if (Cudd_IsComplement(Cudd_E(n))) {
p = prob*pl+(1-prob)*(1-pr); p = prob * pl + (1 - prob) * (1 - pr);
} else { } else {
p = prob*pl+(1-prob)*pr; p = prob * pl + (1 - prob) * pr;
} }
insert2(hash, n, p, sz); insert2(hash, n, p, sz);
return p; return p;
} }
} }
static YAP_Bool static YAP_Bool p_cudd_to_p(void) {
p_cudd_to_p(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node; DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node;
YAP_Term t3 = YAP_ARG3; YAP_Term t3 = YAP_ARG3;
double p = 0.0; double p = 0.0;
YAP_Int vars = YAP_ListLength(t3); YAP_Int vars = YAP_ListLength(t3);
int nodes = max(Cudd_ReadNodeCount(manager),0)+vars+1; int nodes = max(Cudd_ReadNodeCount(manager), 0) + vars + 1;
size_t sz = nodes*4; size_t sz = nodes * 4;
DdGen *dgen = Cudd_FirstNode(manager, n0, &node); 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; double *ar;
if (!dgen) if (!dgen)
return FALSE; return FALSE;
ar = (double *)malloc(vars*sizeof(double)); ar = (double *)malloc(vars * sizeof(double));
if (!ar) if (!ar)
return FALSE; return FALSE;
if (YAP_ListToFloats(t3, ar, vars) < 0) if (YAP_ListToFloats(t3, ar, vars) < 0)
@ -845,7 +782,7 @@ p_cudd_to_p(void)
break; break;
} }
if (node != n0 && Cudd_IsComplement(n0)) { if (node != n0 && Cudd_IsComplement(n0)) {
p = 1-p; p = 1 - p;
} }
Cudd_GenFree(dgen); Cudd_GenFree(dgen);
free(hash); free(hash);
@ -853,62 +790,66 @@ p_cudd_to_p(void)
return YAP_Unify(YAP_ARG4, YAP_MkFloatTerm(p)); return YAP_Unify(YAP_ARG4, YAP_MkFloatTerm(p));
} }
static YAP_Bool static YAP_Bool p_cudd_print(void) {
p_cudd_print(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2);
const char *s = YAP_AtomName(YAP_AtomOfTerm(YAP_ARG3)); const char *s = YAP_AtomName(YAP_AtomOfTerm(YAP_ARG3));
FILE *f; FILE *f;
if (!strcmp(s, "user_output")) f = stdout; if (!strcmp(s, "user_output"))
else if (!strcmp(s, "user_error")) f = stderr; f = stdout;
else if (!strcmp(s, "user")) f = stdout; else if (!strcmp(s, "user_error"))
else f = fopen(s, "w"); f = stderr;
else if (!strcmp(s, "user"))
f = stdout;
else
f = fopen(s, "w");
Cudd_DumpDot(manager, 1, &n0, NULL, NULL, f); Cudd_DumpDot(manager, 1, &n0, NULL, NULL, f);
if (f != stdout && f != stderr) if (f != stdout && f != stderr)
fclose(f); fclose(f);
return TRUE; return TRUE;
} }
static YAP_Bool static YAP_Bool p_cudd_print_with_names(void) {
p_cudd_print_with_names(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2);
const char *s = YAP_AtomName(YAP_AtomOfTerm(YAP_ARG3)); const char *s = YAP_AtomName(YAP_AtomOfTerm(YAP_ARG3));
const char **namesp; char **namesp;
YAP_Term names = YAP_ARG4; YAP_Term names = YAP_ARG4;
FILE *f; FILE *f;
YAP_Int len; YAP_Int len;
YAP_Int i = 0; YAP_Int i = 0;
if (!strcmp(s, "user_output")) f = stdout; if (!strcmp(s, "user_output"))
else if (!strcmp(s, "user_error")) f = stderr; f = stdout;
else if (!strcmp(s, "user")) f = stdout; else if (!strcmp(s, "user_error"))
else f = fopen(s, "w"); f = stderr;
else if (!strcmp(s, "user"))
f = stdout;
else
f = fopen(s, "w");
if ((len = YAP_ListLength(names)) < 0) if ((len = YAP_ListLength(names)) < 0)
return FALSE; return FALSE;
if ((namesp = malloc(sizeof(const char *)*len)) == NULL) if ((namesp = malloc(sizeof(const char *) * len)) == NULL)
return FALSE; return FALSE;
while (YAP_IsPairTerm(names)) { while (YAP_IsPairTerm(names)) {
YAP_Term hd = YAP_HeadOfTerm( names); YAP_Term hd = YAP_HeadOfTerm(names);
const char *f; char *f;
if (YAP_IsAtomTerm(hd)) { if (YAP_IsAtomTerm(hd)) {
const char * s = YAP_AtomName(YAP_AtomOfTerm(hd)); const char *s = YAP_AtomName(YAP_AtomOfTerm(hd));
char *ns = malloc(strlen(s)+1); char *ns = malloc(strlen(s) + 1);
strncpy(ns, s, strlen(s)+1); strncpy(ns, s, strlen(s) + 1);
f = ns; f = ns;
} else { } else {
size_t sz =256; size_t sz = 256;
char *s = malloc(sz+256); char *s = malloc(sz + 256);
while( !YAP_WriteBuffer(hd, s, sz-1, 0) ) { while (!YAP_WriteBuffer(hd, s, sz - 1, 0)) {
sz+=1024; sz += 1024;
s = realloc(s, sz); s = realloc(s, sz);
} }
f = s; f = s;
} }
names = YAP_TailOfTerm( names); names = YAP_TailOfTerm(names);
namesp[i++] = f; namesp[i++] = f;
} }
Cudd_DumpDot(manager, 1, &n0, namesp, NULL, f); Cudd_DumpDot(manager, 1, &n0, namesp, NULL, f);
@ -918,30 +859,24 @@ p_cudd_print_with_names(void)
i--; i--;
free((void *)namesp[i]); free((void *)namesp[i]);
} }
free( namesp ); free(namesp);
return TRUE; return TRUE;
} }
static YAP_Bool static YAP_Bool p_cudd_die(void) {
p_cudd_die(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
Cudd_Quit(manager); Cudd_Quit(manager);
return TRUE; return TRUE;
} }
static YAP_Bool static YAP_Bool p_cudd_release_node(void) {
p_cudd_release_node(void)
{
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1); DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2); DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2);
Cudd_RecursiveDeref(manager,n0); Cudd_RecursiveDeref(manager, n0);
return TRUE; return TRUE;
} }
void void init_cudd(void) {
init_cudd(void)
{
FunctorDollarVar = YAP_MkFunctor(YAP_LookupAtom("$VAR"), 1); FunctorDollarVar = YAP_MkFunctor(YAP_LookupAtom("$VAR"), 1);
FunctorAnd = YAP_MkFunctor(YAP_LookupAtom("/\\"), 2); FunctorAnd = YAP_MkFunctor(YAP_LookupAtom("/\\"), 2);

1014
packages/cplint/approx/simplecuddLPADs/simplecudd.c
View File

File diff suppressed because it is too large Load Diff

111
packages/cplint/approx/simplecuddLPADs/simplecudd.h
View File

@ -190,14 +190,13 @@ form
variable=value variable=value
*/ */
#include "config.h"
#include "cudd_config.h"
#include <math.h>
#include <stdio.h> #include <stdio.h>
#include <stdlib.h> #include <stdlib.h>
#include <string.h> #include <string.h>
#include <math.h>
#include <time.h> #include <time.h>
#include "config.h"
#include "cudd_config.h"
#if HAVE_UTIL_H #if HAVE_UTIL_H
#include <util.h> #include <util.h>
#endif #endif
@ -224,7 +223,8 @@ variable=value
#define LOW(manager) Cudd_Not(Cudd_ReadOne(manager)) #define LOW(manager) Cudd_Not(Cudd_ReadOne(manager))
#define NOT(node) Cudd_Not(node) #define NOT(node) Cudd_Not(node)
#define GetIndex(node) Cudd_NodeReadIndex(node) #define GetIndex(node) Cudd_NodeReadIndex(node)
#define GetMVar(manager, index, value, varmap) equality(manager,index,value,varmap)//Cudd_bddIthVar(manager, index) #define GetMVar(manager, index, value, varmap) \
equality(manager, index, value, varmap) // Cudd_bddIthVar(manager, index)
#define GetVar(manager, index) Cudd_bddIthVar(manager, index) #define GetVar(manager, index) Cudd_bddIthVar(manager, index)
#define NewVar(manager) Cudd_bddNewVar(manager) #define NewVar(manager) Cudd_bddNewVar(manager)
#define KillBDD(manager) Cudd_Quit(manager) #define KillBDD(manager) Cudd_Quit(manager)
@ -253,11 +253,10 @@ typedef struct _bddfileheader {
int filetype; int filetype;
} bddfileheader; } bddfileheader;
typedef struct typedef struct {
{ int nVal, nBit, init;
int nVal,nBit,init; double *probabilities;
double * probabilities; int *booleanVars;
int * booleanVars;
} variable; } variable;
typedef struct _namedvars { typedef struct _namedvars {
@ -268,11 +267,10 @@ typedef struct _namedvars {
double *dvalue; double *dvalue;
int *ivalue; int *ivalue;
void **dynvalue; void **dynvalue;
variable * mvars; variable *mvars;
int * bVar2mVar; int *bVar2mVar;
} namedvars; } namedvars;
typedef struct _hisnode { typedef struct _hisnode {
DdNode *key; DdNode *key;
double dvalue; double dvalue;
@ -296,27 +294,31 @@ typedef struct _nodeline {
/* Initialization */ /* Initialization */
DdManager* simpleBDDinit(int varcnt); DdManager *simpleBDDinit(int varcnt);
/* BDD Generation */ /* BDD Generation */
DdNode* D_BDDAnd(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_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDOr(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_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDXor(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_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader); DdNode *FileGenerateBDD(DdManager *manager, namedvars varmap,
DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap); bddfileheader fileheader);
DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline); DdNode *OnlineGenerateBDD(DdManager *manager, namedvars *varmap);
DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline); DdNode *LineParser(DdManager *manager, namedvars varmap, DdNode **inter,
DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper); 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); int getInterBDD(char *function);
char* getFileName(const char *function); char *getFileName(const char *function);
int GetParam(char *inputline, int iParam); int GetParam(char *inputline, int iParam);
int LoadVariableData(namedvars varmap, char *filename); int LoadVariableData(namedvars varmap, char *filename);
int LoadMultiVariableData(DdManager * mgr,namedvars varmap, char *filename); int LoadMultiVariableData(DdManager *mgr, namedvars varmap, char *filename);
/* Named variables */ /* Named variables */
@ -325,48 +327,61 @@ namedvars InitNamedMultiVars(int varcnt, int varstart, int bvarcnt);
void EnlargeNamedVars(namedvars *varmap, int newvarcnt); void EnlargeNamedVars(namedvars *varmap, int newvarcnt);
int AddNamedVarAt(namedvars varmap, const char *varname, int index); int AddNamedVarAt(namedvars varmap, const char *varname, int index);
int AddNamedVar(namedvars varmap, const char *varname); int AddNamedVar(namedvars varmap, const char *varname);
int AddNamedMultiVar(DdManager *mgr,namedvars varmap, const char *varnamei, int *value); int AddNamedMultiVar(DdManager *mgr, namedvars varmap, const char *varnamei,
void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, void *dynvalue); int *value);
int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int ivalue, void *dynvalue); 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 GetNamedVarIndex(const namedvars varmap, const char *varname);
int RepairVarcnt(namedvars *varmap); int RepairVarcnt(namedvars *varmap);
char* GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node); char *GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node);
char* GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node); char *GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node);
int all_loaded(namedvars varmap, int disp); int all_loaded(namedvars varmap, int disp);
/* Traversal */ /* Traversal */
DdNode* HighNodeOf(DdManager *manager, DdNode *node); DdNode *HighNodeOf(DdManager *manager, DdNode *node);
DdNode* LowNodeOf(DdManager *manager, DdNode *node); DdNode *LowNodeOf(DdManager *manager, DdNode *node);
/* Traversal - History */ /* Traversal - History */
hisqueue* InitHistory(int varcnt); hisqueue *InitHistory(int varcnt);
void ReInitHistory(hisqueue *HisQueue, int varcnt); void ReInitHistory(hisqueue *HisQueue, int varcnt);
void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue); void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue,
hisnode* GetNode(hisqueue *HisQueue, int varstart, DdNode *node); int ivalue, void *dynvalue);
hisnode *GetNode(hisqueue *HisQueue, int varstart, DdNode *node);
int GetNodeIndex(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 */ /* Save-load */
bddfileheader ReadFileHeader(char *filename); bddfileheader ReadFileHeader(char *filename);
int CheckFileVersion(const char *version); int CheckFileVersion(const char *version);
DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile); DdNode *LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile);
DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current); DdNode *LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes,
DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum); 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); int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd,
void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile); char *filename);
void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes,
DdNode *Current, FILE *outputfile);
void ExpandNodes(hisqueue *Nodes, int index, int nodenum); void ExpandNodes(hisqueue *Nodes, int index, int nodenum);
/* Export */ /* Export */
int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename); 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); DdNode *equality(DdManager *mgr, int varIndex, int value, namedvars varmap);
hisnode* GetNodei1(int *bVar2mVar,hisqueue *HisQueue, int varstart, DdNode *node); hisnode *GetNodei1(int *bVar2mVar, hisqueue *HisQueue, int varstart,
void AddNode1(int *bVar2mVar, hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue); DdNode *node);
hisnode* GetNode1(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);

9
packages/swig/android/JavaYap.java
View File

@ -1,4 +1,3 @@
package pt.up.fc.dcc.yap;
/**** using sqlite /**** using sqlite
For example,the following: 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.app.Activity;
import android.os.Bundle; import android.os.Bundle;
import android.view.View; import android.view.View;
@ -45,12 +47,14 @@ import org.sqlite.database.sqlite.SQLiteOpenHelper;
import org.sqlite.database.SQLException; import org.sqlite.database.SQLException;
import org.sqlite.database.DatabaseErrorHandler; import org.sqlite.database.DatabaseErrorHandler;
class DoNotDeleteErrorHandler implements DatabaseErrorHandler { class DoNotDeleteErrorHandler implements DatabaseErrorHandler {
private static final String TAG = "DoNotDeleteErrorHandler"; private static final String TAG = "DoNotDeleteErrorHandler";
public void onCorruption(SQLiteDatabase dbObj) { public void onCorruption(SQLiteDatabase dbObj) {
Log.e(TAG, "Corruption reported by sqlite on database: " + dbObj.getPath()); Log.e(TAG, "Corruption reported by sqlite on database: " + dbObj.getPath());
} }
} }
public class JavaYap extends Activity public class JavaYap extends Activity
{ {
TextView outputText = null; TextView outputText = null;
@ -242,8 +246,7 @@ public class JavaYap extends Activity
System.loadLibrary("android"); System.loadLibrary("android");
System.loadLibrary("log"); System.loadLibrary("log");
System.loadLibrary("gmp"); System.loadLibrary("gmp");
System.loadLibrary("sqliteX"); System.loadLibrary("YapDroid");
System.loadLibrary("example");
} }
private static native void load(AssetManager mgr); private static native void load(AssetManager mgr);

6
pl/boot.yap
View File

@ -1360,6 +1360,12 @@ not(G) :- \+ '$execute'(G).
'$check_callable'(_,_). '$check_callable'(_,_).
'$bootstrap' :-
bootstrap('init.yap').
module(user),
'$live'.
bootstrap(F) :- bootstrap(F) :-
% '$open'(F, '$csult', Stream, 0, 0, F), % '$open'(F, '$csult', Stream, 0, 0, F),
% '$file_name'(Stream,File), % '$file_name'(Stream,File),