small fixes

This commit is contained in:
Vitor Santos Costa 2013-10-03 11:28:09 +01:00
parent 94619d2a32
commit 1c9167a6c5
4 changed files with 72 additions and 23 deletions

View File

@ -884,12 +884,12 @@ All the arguments and flags are optional and have the following meaning:
@item -? @item -?
print a short error message. print a short error message.
@item -s@var{Size} @item -s@var{Size}
allocate @var{Size} K bytes for local and global stacks. The user may allocate @var{Size} KBytes for local and global stacks. The user may
specify @t{M} bytes. specify @t{M} bytes.
@item -h@var{Size} @item -h@var{Size}
allocate @var{Size} K bytes for heap and auxiliary stacks allocate @var{Size} KBytes for heap and auxiliary stacks
@item -t@var{Size} @item -t@var{Size}
allocate @var{Size} K bytes for the trail stack allocate @var{Size} KBytes for the trail stack
@item -L@var{Size} @item -L@var{Size}
SWI-compatible option to allocate @var{Size} K bytes for local and global stacks, the local stack SWI-compatible option to allocate @var{Size} K bytes for local and global stacks, the local stack
cannot be expanded. To avoid confusion with the load option, @var{Size} cannot be expanded. To avoid confusion with the load option, @var{Size}
@ -14083,7 +14083,7 @@ This library provides an interface to the BDD package CUDD. It requires
CUDD compiled as a dynamic library. In Linux this is available out of CUDD compiled as a dynamic library. In Linux this is available out of
box in Fedora, but can easily be ported to other Linux box in Fedora, but can easily be ported to other Linux
distributions. CUDD is available in the ports OSX package, and in distributions. CUDD is available in the ports OSX package, and in
cygwin. To use it, call @code{:-use_module(library(block_diagram))}. cygwin. To use it, call @code{:-use_module(library(bdd))}.
The following predicates construct a BDD: The following predicates construct a BDD:
@table @code @table @code

View File

@ -18,9 +18,9 @@ problem(Ex, Els) :-
Els ins 1..9, Els ins 1..9,
M <== matrix( Els, [dim=[9,9]] ), M <== matrix( Els, [dim=[9,9]] ),
% select rows % select rows
foreach( I in 0..8 , all_different(M[I,*]) ), foreach( I in 0..8 , all_different(M[I,_]) ),
% select cols % select cols
foreach( J in 0..8, all_different(M[*,J]) ), foreach( J in 0..8, all_different(M[_,J]) ),
% select squares % select squares
foreach( [I,J] ins 0..2 , foreach( [I,J] ins 0..2 ,
all_different(M[I*3+(0..2),J*3+(0..2)]) ), all_different(M[I*3+(0..2),J*3+(0..2)]) ),

View File

@ -16,6 +16,8 @@
:- use_module(library(lists)). :- use_module(library(lists)).
:- use_module(library(maplist)).
:- use_module(library(rbtrees)). :- use_module(library(rbtrees)).
:- use_module(library(simpbool)). :- use_module(library(simpbool)).
@ -25,6 +27,8 @@ tell_warning :-
:- catch(load_foreign_files([cudd], [], init_cudd),_,fail) -> true ; tell_warning. :- catch(load_foreign_files([cudd], [], init_cudd),_,fail) -> true ; tell_warning.
% create a new BDD from a tree.
bdd_new(T, Bdd) :- bdd_new(T, Bdd) :-
term_variables(T, Vars), term_variables(T, Vars),
bdd_new(T, Vars, Bdd). bdd_new(T, Vars, Bdd).
@ -34,6 +38,7 @@ bdd_new(T, Vars, cudd(M,X,VS,TrueVars)) :-
VS =.. [vs|TrueVars], VS =.. [vs|TrueVars],
findall(Manager-Cudd, set_bdd(T, VS, Manager, Cudd), [M-X]). findall(Manager-Cudd, set_bdd(T, VS, Manager, Cudd), [M-X]).
% create a new BDD from a list.
bdd_from_list(List, Vars, cudd(M,X,VS,TrueVars)) :- bdd_from_list(List, Vars, cudd(M,X,VS,TrueVars)) :-
term_variables(Vars, TrueVars), term_variables(Vars, TrueVars),
VS =.. [vs|TrueVars], VS =.. [vs|TrueVars],
@ -76,7 +81,7 @@ add_variables([V|Vs], RB0, RR0, M, RBF, RRF) :-
writeln_list([]). writeln_list([]).
writeln_list(B.Bindings) :- writeln_list([B|Bindings]) :-
writeln(B), writeln(B),
writeln_list(Bindings). writeln_list(Bindings).
@ -130,14 +135,12 @@ bdd_eval(add(M, X, Vars, _), Val) :-
mtbdd_eval(add(M,X, Vars, _), Val) :- mtbdd_eval(add(M,X, Vars, _), Val) :-
add_eval(M, X, Vars, Val). add_eval(M, X, Vars, Val).
bdd_tree(cudd(M, X, Vars, _Vs), bdd(Dir, Tree, Vars)) :- % get the BDD as a Prolog list from the CUDD C object
cudd_to_term(M, X, Vars, Dir, Tree). bdd_tree(cudd(M, X, Vars, _Vs), bdd(Dir, List, Vars)) :-
cudd_to_term(M, X, Vars, Dir, List).
bdd_tree(add(M, X, Vars, _), mtbdd(Tree, Vars)) :- bdd_tree(add(M, X, Vars, _), mtbdd(Tree, Vars)) :-
add_to_term(M, X, Vars, Tree). add_to_term(M, X, Vars, Tree).
mtbdd_tree(add(M,X,Vars, _), mtbdd(Dir, Tree, Vars)) :-
add_to_term(M, X, Vars, Dir, Tree).
bdd_to_probability_sum_product(cudd(M,X,_,Probs), Prob) :- bdd_to_probability_sum_product(cudd(M,X,_,Probs), Prob) :-
cudd_to_probability_sum_product(M, X, Probs, Prob). cudd_to_probability_sum_product(M, X, Probs, Prob).

View File

@ -26,6 +26,7 @@ static YAP_Functor FunctorDollarVar,
FunctorLAnd, FunctorLAnd,
FunctorLOr, FunctorLOr,
FunctorNot, FunctorNot,
FunctorMinus1,
FunctorXor, FunctorXor,
FunctorNand, FunctorNand,
FunctorNor, FunctorNor,
@ -90,12 +91,17 @@ term_to_cudd(DdManager *manager, YAP_Term 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)
return NULL;
Cudd_Ref(var); Cudd_Ref(var);
return var; return var;
} else if (f == FunctorAnd || f == FunctorLAnd || f == FunctorTimes) { } else if (f == FunctorAnd || f == FunctorLAnd || f == FunctorTimes) {
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t));
DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = cudd_and(manager, x1, x2); DdNode *tmp;
if (!x1 || !x2)
return NULL;
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;
@ -105,7 +111,10 @@ term_to_cudd(DdManager *manager, YAP_Term t)
YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i;
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t));
DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t));
DdNode *tmp = cudd_and(manager, x1, x2); DdNode *tmp;
if (!x1 || !x2)
return NULL;
tmp = cudd_and(manager, x1, x2);
for (i=0 ; i < refs; i++) { for (i=0 ; i < refs; i++) {
Cudd_Ref(tmp); Cudd_Ref(tmp);
} }
@ -124,14 +133,20 @@ term_to_cudd(DdManager *manager, YAP_Term t)
} else if (f == FunctorOr || f == FunctorLOr || f == FunctorPlus) { } else if (f == FunctorOr || f == FunctorLOr || f == FunctorPlus) {
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t));
DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = cudd_or(manager, x1, x2); DdNode *tmp;
if (!x1 || !x2)
return NULL;
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));
DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = cudd_xor(manager, x1, x2); DdNode *tmp;
if (!x1 || !x2)
return NULL;
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;
@ -141,7 +156,10 @@ term_to_cudd(DdManager *manager, YAP_Term t)
YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i; YAP_Int refs = YAP_IntOfTerm(YAP_ArgOfTerm(1, t)), i;
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(3, t));
DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(4, t));
DdNode *tmp = cudd_or(manager, x1, x2); DdNode *tmp;
if (!x1 || !x2)
return NULL;
tmp = cudd_or(manager, x1, x2);
for (i=0 ; i < refs; i++) { for (i=0 ; i < refs; i++) {
Cudd_Ref(tmp); Cudd_Ref(tmp);
} }
@ -155,20 +173,30 @@ term_to_cudd(DdManager *manager, YAP_Term t)
} else if (f == FunctorNor) { } else if (f == FunctorNor) {
DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t));
DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t));
DdNode *tmp = cudd_nor(manager, x1, x2); DdNode *tmp;
if (!x1 || !x2)
return NULL;
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));
DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t)); DdNode *x2 = term_to_cudd(manager, YAP_ArgOfTerm(2, t));
if (!x1 || !x2)
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) { } 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));
if (!x1)
return NULL;
return Cudd_Not(x1); return Cudd_Not(x1);
} else {
YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported operator in CUDD");
return NULL;
} }
} else if (YAP_IsIntTerm(t)) { } else if (YAP_IsIntTerm(t)) {
YAP_Int i = YAP_IntOfTerm(t); YAP_Int i = YAP_IntOfTerm(t);
@ -176,15 +204,25 @@ term_to_cudd(DdManager *manager, YAP_Term t)
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 {
YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD");
return NULL;
}
} else if (YAP_IsFloatTerm(t)) { } else if (YAP_IsFloatTerm(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 if (YAP_IsVarTerm(t)) { else {
fprintf(stderr,"Unbound Variable should not be input argument to BDD\n"); YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD");
return NULL;
}
} else if (YAP_IsVarTerm(t)) {
YAP_Error(INSTANTIATION_ERROR, t, "unsupported unbound term in CUDD");
return NULL;
} }
YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD");
return NULL; return NULL;
} }
@ -203,6 +241,8 @@ p_term_to_cudd(void)
manager = (DdManager *)YAP_IntOfTerm(YAP_ARG2); manager = (DdManager *)YAP_IntOfTerm(YAP_ARG2);
} }
t = term_to_cudd(manager, YAP_ARG1); t = term_to_cudd(manager, YAP_ARG1);
if (!t)
return FALSE;
return return
YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t)); YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t));
} }
@ -749,9 +789,14 @@ 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 = fopen(s, "w"); 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");
Cudd_DumpDot(manager, 1, &n0, NULL, NULL, f); Cudd_DumpDot(manager, 1, &n0, NULL, NULL, f);
fclose(f); if (f != stdout && f != stderr)
fclose(f);
return TRUE; return TRUE;
} }
@ -792,6 +837,7 @@ init_cudd(void)
FunctorTimes4 = YAP_MkFunctor(YAP_LookupAtom("*"), 4); FunctorTimes4 = YAP_MkFunctor(YAP_LookupAtom("*"), 4);
FunctorPlus4 = YAP_MkFunctor(YAP_LookupAtom("+"), 4); FunctorPlus4 = YAP_MkFunctor(YAP_LookupAtom("+"), 4);
FunctorNot = YAP_MkFunctor(YAP_LookupAtom("not"), 1); FunctorNot = YAP_MkFunctor(YAP_LookupAtom("not"), 1);
FunctorMinus1 = YAP_MkFunctor(YAP_LookupAtom("-"), 1);
FunctorOutPos = YAP_MkFunctor(YAP_LookupAtom("pp"), 4); FunctorOutPos = YAP_MkFunctor(YAP_LookupAtom("pp"), 4);
FunctorOutNeg = YAP_MkFunctor(YAP_LookupAtom("pn"), 4); FunctorOutNeg = YAP_MkFunctor(YAP_LookupAtom("pn"), 4);
FunctorOutAdd = YAP_MkFunctor(YAP_LookupAtom("add"), 4); FunctorOutAdd = YAP_MkFunctor(YAP_LookupAtom("add"), 4);