From 1c9167a6c5a4c9434034f260143fe7b0cbb90e7c Mon Sep 17 00:00:00 2001 From: Vitor Santos Costa Date: Thu, 3 Oct 2013 11:28:09 +0100 Subject: [PATCH] small fixes --- docs/yap.tex | 8 +-- library/gecode/clp_examples/sudoku.yap | 4 +- packages/bdd/bdd.yap | 15 +++--- packages/bdd/cudd.c | 68 +++++++++++++++++++++----- 4 files changed, 72 insertions(+), 23 deletions(-) diff --git a/docs/yap.tex b/docs/yap.tex index d504810bd..f3f29c7ca 100644 --- a/docs/yap.tex +++ b/docs/yap.tex @@ -884,12 +884,12 @@ All the arguments and flags are optional and have the following meaning: @item -? print a short error message. @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. @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} -allocate @var{Size} K bytes for the trail stack +allocate @var{Size} KBytes for the trail stack @item -L@var{Size} 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} @@ -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 box in Fedora, but can easily be ported to other Linux 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: @table @code diff --git a/library/gecode/clp_examples/sudoku.yap b/library/gecode/clp_examples/sudoku.yap index e22ebe92f..34b5735d9 100644 --- a/library/gecode/clp_examples/sudoku.yap +++ b/library/gecode/clp_examples/sudoku.yap @@ -18,9 +18,9 @@ problem(Ex, Els) :- Els ins 1..9, M <== matrix( Els, [dim=[9,9]] ), % select rows - foreach( I in 0..8 , all_different(M[I,*]) ), + foreach( I in 0..8 , all_different(M[I,_]) ), % select cols - foreach( J in 0..8, all_different(M[*,J]) ), + foreach( J in 0..8, all_different(M[_,J]) ), % select squares foreach( [I,J] ins 0..2 , all_different(M[I*3+(0..2),J*3+(0..2)]) ), diff --git a/packages/bdd/bdd.yap b/packages/bdd/bdd.yap index 29fb1d695..fa5163b10 100644 --- a/packages/bdd/bdd.yap +++ b/packages/bdd/bdd.yap @@ -16,6 +16,8 @@ :- use_module(library(lists)). +:- use_module(library(maplist)). + :- use_module(library(rbtrees)). :- use_module(library(simpbool)). @@ -25,6 +27,8 @@ tell_warning :- :- catch(load_foreign_files([cudd], [], init_cudd),_,fail) -> true ; tell_warning. + +% create a new BDD from a tree. bdd_new(T, Bdd) :- term_variables(T, Vars), bdd_new(T, Vars, Bdd). @@ -34,6 +38,7 @@ bdd_new(T, Vars, cudd(M,X,VS,TrueVars)) :- VS =.. [vs|TrueVars], 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)) :- term_variables(Vars, TrueVars), VS =.. [vs|TrueVars], @@ -76,7 +81,7 @@ add_variables([V|Vs], RB0, RR0, M, RBF, RRF) :- writeln_list([]). -writeln_list(B.Bindings) :- +writeln_list([B|Bindings]) :- writeln(B), writeln_list(Bindings). @@ -130,14 +135,12 @@ bdd_eval(add(M, X, Vars, _), Val) :- mtbdd_eval(add(M,X, Vars, _), Val) :- add_eval(M, X, Vars, Val). -bdd_tree(cudd(M, X, Vars, _Vs), bdd(Dir, Tree, Vars)) :- - cudd_to_term(M, X, Vars, Dir, Tree). +% get the BDD as a Prolog list from the CUDD C object +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)) :- 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) :- cudd_to_probability_sum_product(M, X, Probs, Prob). diff --git a/packages/bdd/cudd.c b/packages/bdd/cudd.c index a795f47a0..e443b43a6 100644 --- a/packages/bdd/cudd.c +++ b/packages/bdd/cudd.c @@ -26,6 +26,7 @@ static YAP_Functor FunctorDollarVar, FunctorLAnd, FunctorLOr, FunctorNot, + FunctorMinus1, FunctorXor, FunctorNand, FunctorNor, @@ -90,12 +91,17 @@ term_to_cudd(DdManager *manager, YAP_Term t) if (f == FunctorDollarVar) { int i = YAP_IntOfTerm(YAP_ArgOfTerm(1,t)); DdNode *var = Cudd_bddIthVar(manager,i); + if (!var) + return NULL; Cudd_Ref(var); return var; } else if (f == FunctorAnd || f == FunctorLAnd || f == FunctorTimes) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, 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,x2); return tmp; @@ -105,7 +111,10 @@ term_to_cudd(DdManager *manager, YAP_Term t) 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 = cudd_and(manager, x1, x2); + DdNode *tmp; + if (!x1 || !x2) + return NULL; + tmp = cudd_and(manager, x1, x2); for (i=0 ; i < refs; i++) { Cudd_Ref(tmp); } @@ -124,14 +133,20 @@ term_to_cudd(DdManager *manager, YAP_Term t) } else if (f == FunctorOr || f == FunctorLOr || f == FunctorPlus) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, 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,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 = 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,x2); return tmp; @@ -141,7 +156,10 @@ term_to_cudd(DdManager *manager, YAP_Term t) 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 = cudd_or(manager, x1, x2); + DdNode *tmp; + if (!x1 || !x2) + return NULL; + tmp = cudd_or(manager, x1, x2); for (i=0 ; i < refs; i++) { Cudd_Ref(tmp); } @@ -155,20 +173,30 @@ term_to_cudd(DdManager *manager, YAP_Term t) } 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 = 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,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; DdNode *tmp = cudd_nand(manager, x1, x2); Cudd_RecursiveDeref(manager,x1); Cudd_RecursiveDeref(manager,x2); return tmp; - } else if (f == FunctorNot) { + } else if (f == FunctorNot || FunctorMinus1) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); + if (!x1) + return NULL; return Cudd_Not(x1); + } else { + YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported operator in CUDD"); + return NULL; } } else if (YAP_IsIntTerm(t)) { YAP_Int i = YAP_IntOfTerm(t); @@ -176,15 +204,25 @@ term_to_cudd(DdManager *manager, YAP_Term t) return Cudd_ReadLogicZero(manager); else if (i==1) return Cudd_ReadOne(manager); + else { + YAP_Error(DOMAIN_ERROR_OUT_OF_RANGE, t, "unsupported number in CUDD"); + return NULL; + } } else if (YAP_IsFloatTerm(t)) { YAP_Int i = YAP_FloatOfTerm(t); if (i == 0.0) return Cudd_ReadLogicZero(manager); else if (i==1.0) return Cudd_ReadOne(manager); - } else if (YAP_IsVarTerm(t)) { - fprintf(stderr,"Unbound Variable should not be input argument to BDD\n"); + else { + 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; } @@ -203,6 +241,8 @@ p_term_to_cudd(void) manager = (DdManager *)YAP_IntOfTerm(YAP_ARG2); } t = term_to_cudd(manager, YAP_ARG1); + if (!t) + return FALSE; return YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t)); } @@ -749,9 +789,14 @@ 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 = 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); - fclose(f); + if (f != stdout && f != stderr) + fclose(f); return TRUE; } @@ -792,6 +837,7 @@ init_cudd(void) FunctorTimes4 = YAP_MkFunctor(YAP_LookupAtom("*"), 4); FunctorPlus4 = YAP_MkFunctor(YAP_LookupAtom("+"), 4); FunctorNot = YAP_MkFunctor(YAP_LookupAtom("not"), 1); + FunctorMinus1 = YAP_MkFunctor(YAP_LookupAtom("-"), 1); FunctorOutPos = YAP_MkFunctor(YAP_LookupAtom("pp"), 4); FunctorOutNeg = YAP_MkFunctor(YAP_LookupAtom("pn"), 4); FunctorOutAdd = YAP_MkFunctor(YAP_LookupAtom("add"), 4);