extend functionality.

This commit is contained in:
Vítor Santos Costa 2012-03-27 14:57:43 +01:00
parent cd45c64dcc
commit 295cf24f5c
2 changed files with 79 additions and 7 deletions

View File

@ -1,6 +1,7 @@
:- module(bdd, [bdd_new/2, :- module(bdd, [bdd_new/2,
bdd_new/3, bdd_new/3,
bdd_from_list/3,
mtbdd_new/2, mtbdd_new/2,
mtbdd_new/3, mtbdd_new/3,
bdd_eval/2, bdd_eval/2,
@ -24,6 +25,11 @@ 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]).
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) :- set_bdd(T, VS, Manager, Cudd) :-
numbervars(VS,0,_), numbervars(VS,0,_),
( ground(T) ( ground(T)
@ -33,6 +39,45 @@ set_bdd(T, VS, Manager, Cudd) :-
writeln(throw(error(instantiation_error,T))) 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) :- mtbdd_new(T, Mtbdd) :-
term_variables(T, Vars), term_variables(T, Vars),
mtbdd_new(T, Vars, Mtbdd). mtbdd_new(T, Vars, Mtbdd).

View File

@ -5,14 +5,15 @@
#include "cudd.h" #include "cudd.h"
static YAP_Functor FunctorDollarVar, static YAP_Functor FunctorDollarVar,
FunctorCudd,
FunctorAnd, FunctorAnd,
FunctorAnd4, FunctorAnd4,
FunctorOr, FunctorOr,
FunctorOr4, FunctorOr4,
FunctorLAnd, FunctorLAnd,
FunctorLOr, FunctorLOr,
FunctorXor,
FunctorNot, FunctorNot,
FunctorXor,
FunctorNand, FunctorNand,
FunctorNor, FunctorNor,
FunctorTimes, FunctorTimes,
@ -76,6 +77,7 @@ 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);
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));
@ -101,6 +103,11 @@ term_to_cudd(DdManager *manager, YAP_Term t)
} else { } else {
return (DdNode *)YAP_IntOfTerm(t1); 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) { } 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));
@ -171,9 +178,19 @@ term_to_cudd(DdManager *manager, YAP_Term t)
static int static int
p_term_to_cudd(void) p_term_to_cudd(void)
{ {
DdManager *manager = Cudd_Init(0,0,CUDD_UNIQUE_SLOTS,CUDD_CACHE_SLOTS,0); DdManager *manager;
DdNode *t = term_to_cudd(manager, YAP_ARG1); DdNode *t;
return YAP_Unify(YAP_ARG2, YAP_MkIntTerm((YAP_Int)manager)) &&
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)); 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<b ? b : a; return a<b ? b : a;
} }
static YAP_Int
get_vars(YAP_Term t3)
{
if (YAP_IsAtomTerm(t3))
return 0;
return YAP_ArityOfFunctor(YAP_FunctorOfTerm(t3));
}
static int static int
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 = YAP_ArityOfFunctor(YAP_FunctorOfTerm(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);
@ -556,7 +582,7 @@ 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 = YAP_ArityOfFunctor(YAP_FunctorOfTerm(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);
@ -698,6 +724,7 @@ init_cudd(void)
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);
FunctorCudd = YAP_MkFunctor(YAP_LookupAtom("cudd"), 1);
TermMinusOne = YAP_MkIntTerm(-1); TermMinusOne = YAP_MkIntTerm(-1);
TermPlusOne = YAP_MkIntTerm(-1); TermPlusOne = YAP_MkIntTerm(-1);
YAP_UserCPredicate("term_to_cudd", p_term_to_cudd, 3); YAP_UserCPredicate("term_to_cudd", p_term_to_cudd, 3);