From 295cf24f5c27f833ca6d89a1967d0e09ab2c6103 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?V=C3=ADtor=20Santos=20Costa?= Date: Tue, 27 Mar 2012 14:57:43 +0100 Subject: [PATCH] extend functionality. --- packages/bdd/bdd.yap | 45 ++++++++++++++++++++++++++++++++++++++++++++ packages/bdd/cudd.c | 41 +++++++++++++++++++++++++++++++++------- 2 files changed, 79 insertions(+), 7 deletions(-) diff --git a/packages/bdd/bdd.yap b/packages/bdd/bdd.yap index 22e157f85..8c14f1df5 100644 --- a/packages/bdd/bdd.yap +++ b/packages/bdd/bdd.yap @@ -1,6 +1,7 @@ :- module(bdd, [bdd_new/2, bdd_new/3, + bdd_from_list/3, mtbdd_new/2, mtbdd_new/3, bdd_eval/2, @@ -24,6 +25,11 @@ bdd_new(T, Vars, cudd(M,X,VS,TrueVars)) :- VS =.. [vs|TrueVars], findall(Manager-Cudd, set_bdd(T, VS, Manager, Cudd), [M-X]). +bdd_from_list(List, Vars, cudd(M,X,VS,TrueVars)) :- + term_variables(Vars, TrueVars), + VS =.. [vs|TrueVars], + findall(Manager-Cudd, set_bdd_from_list(List, VS, Manager, Cudd), [M-X]). + set_bdd(T, VS, Manager, Cudd) :- numbervars(VS,0,_), ( ground(T) @@ -33,6 +39,45 @@ set_bdd(T, VS, Manager, Cudd) :- writeln(throw(error(instantiation_error,T))) ). +set_bdd_from_list(T, VS, Manager, Cudd) :- + numbervars(VS,0,_), +% writeln_list(T), + list_to_cudd(T,Manager,_Cudd0,Cudd). + +writeln_list([]). +writeln_list(B.Bindings) :- + writeln(B), + writeln_list(Bindings). + +%list_to_cudd(H.List,_Manager,Cudd,Cudd) :- writeln(l:H), fail. +list_to_cudd([],_Manager,Cudd,Cudd) :- writeln('.'). +list_to_cudd((V=0*_Par).T, Manager, _Cudd0, CuddF) :- !, + write('0'), flush_output, + term_to_cudd(0, Manager, Cudd), + V = cudd(Cudd), + list_to_cudd(T, Manager, Cudd, CuddF). +list_to_cudd((V=0).T, Manager, _Cudd0, CuddF) :- !, + write('0'), flush_output, + term_to_cudd(0, Manager, Cudd), + V = cudd(Cudd), + list_to_cudd(T, Manager, Cudd, CuddF). +list_to_cudd((V=_Tree*0).T, Manager, _Cudd0, CuddF) :- !, + write('0'), flush_output, + term_to_cudd(0, Manager, Cudd), + V = cudd(Cudd), + list_to_cudd(T, Manager, Cudd, CuddF). +list_to_cudd((V=Tree*1).T, Manager, _Cudd0, CuddF) :- !, + write('.'), flush_output, + term_to_cudd(Tree, Manager, Cudd), + V = cudd(Cudd), + list_to_cudd(T, Manager, Cudd, CuddF). +list_to_cudd((V=Tree).T, Manager, _Cudd0, CuddF) :- + write('.'), flush_output, + ( ground(Tree) -> true ; throw(error(instantiation_error(Tree))) ), + term_to_cudd(Tree, Manager, Cudd), + V = cudd(Cudd), + list_to_cudd(T, Manager, Cudd, CuddF). + mtbdd_new(T, Mtbdd) :- term_variables(T, Vars), mtbdd_new(T, Vars, Mtbdd). diff --git a/packages/bdd/cudd.c b/packages/bdd/cudd.c index 867e82e69..585824d75 100644 --- a/packages/bdd/cudd.c +++ b/packages/bdd/cudd.c @@ -5,14 +5,15 @@ #include "cudd.h" static YAP_Functor FunctorDollarVar, + FunctorCudd, FunctorAnd, FunctorAnd4, FunctorOr, FunctorOr4, FunctorLAnd, FunctorLOr, + FunctorNot, FunctorXor, - FunctorNot, FunctorNand, FunctorNor, FunctorTimes, @@ -76,6 +77,7 @@ 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); + Cudd_Ref(var); return var; } else if (f == FunctorAnd || f == FunctorLAnd || f == FunctorTimes) { DdNode *x1 = term_to_cudd(manager, YAP_ArgOfTerm(1, t)); @@ -101,6 +103,11 @@ term_to_cudd(DdManager *manager, YAP_Term t) } else { return (DdNode *)YAP_IntOfTerm(t1); } + } else if (f == FunctorCudd) { + YAP_Term t1 = YAP_ArgOfTerm(1, t); + DdNode *tmp = (DdNode *)YAP_IntOfTerm(t1); + Cudd_Ref(tmp); + return tmp; } 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)); @@ -171,9 +178,19 @@ term_to_cudd(DdManager *manager, YAP_Term t) static int p_term_to_cudd(void) { - DdManager *manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); - DdNode *t = term_to_cudd(manager, YAP_ARG1); - return YAP_Unify(YAP_ARG2, YAP_MkIntTerm((YAP_Int)manager)) && + 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); + if (!YAP_Unify(YAP_ARG2, YAP_MkIntTerm((YAP_Int)manager))) + return FALSE; + } else { + manager = (DdManager *)YAP_IntOfTerm(YAP_ARG2); + } + t = term_to_cudd(manager, YAP_ARG1); + return YAP_Unify(YAP_ARG3, YAP_MkIntTerm((YAP_Int)t)); } @@ -484,18 +501,27 @@ build_prolog_cudd(DdManager *manager, DdNode *n, YAP_Term *ar, hash_table_entry } } -static inline max(int a, int b) +static inline int +max(int a, int b) { return a