iextend bdd support.
This commit is contained in:
parent
88411f4b40
commit
3d216cf9db
@ -7,10 +7,16 @@
|
|||||||
bdd_eval/2,
|
bdd_eval/2,
|
||||||
mtbdd_eval/2,
|
mtbdd_eval/2,
|
||||||
bdd_tree/2,
|
bdd_tree/2,
|
||||||
|
bdd_size/2,
|
||||||
|
bdd_print/2,
|
||||||
bdd_to_probability_sum_product/2,
|
bdd_to_probability_sum_product/2,
|
||||||
bdd_close/1,
|
bdd_close/1,
|
||||||
mtbdd_close/1]).
|
mtbdd_close/1]).
|
||||||
|
|
||||||
|
:- use_module(library(lists)).
|
||||||
|
|
||||||
|
:- use_module(library(rbtrees)).
|
||||||
|
|
||||||
tell_warning :-
|
tell_warning :-
|
||||||
print_message(warning,functionality(cudd)).
|
print_message(warning,functionality(cudd)).
|
||||||
|
|
||||||
@ -39,18 +45,44 @@ 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) :-
|
set_bdd_from_list(T0, VS, Manager, Cudd) :-
|
||||||
numbervars(VS,0,_),
|
numbervars(VS,0,_),
|
||||||
|
% generate_releases(T0, Manager, T),
|
||||||
|
T0 = T,
|
||||||
% writeln_list(T),
|
% writeln_list(T),
|
||||||
list_to_cudd(T,Manager,_Cudd0,Cudd).
|
list_to_cudd(T,Manager,_Cudd0,Cudd).
|
||||||
|
|
||||||
|
generate_releases(T0, Manager, T) :-
|
||||||
|
rb_empty(RB0),
|
||||||
|
reverse(T0, [H|R]),
|
||||||
|
add_releases(R, RB0, [H], Manager, T).
|
||||||
|
|
||||||
|
add_releases([], _, RR, _M, RR).
|
||||||
|
add_releases([(X = Ts)|R], RB0, RR0, M, RR) :-
|
||||||
|
term_variables(Ts, Vs), !,
|
||||||
|
add_variables(Vs, RB0, RR0, M, RBF, RRI),
|
||||||
|
add_releases(R, RBF, [(X=Ts)|RRI], M, RR).
|
||||||
|
|
||||||
|
add_variables([], RB, RR, _M, RB, RR).
|
||||||
|
add_variables([V|Vs], RB0, RR0, M, RBF, RRF) :-
|
||||||
|
rb_lookup(V, _, RB0), !,
|
||||||
|
add_variables(Vs, RB0, RR0, M, RBF, RRF).
|
||||||
|
add_variables([V|Vs], RB0, RR0, M, RBF, RRF) :-
|
||||||
|
rb_insert(RB0, V, _, RB1),
|
||||||
|
add_variables(Vs, RB1, [release_node(M,V)|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).
|
||||||
|
|
||||||
%list_to_cudd(H.List,_Manager,Cudd,Cudd) :- writeln(l:H), fail.
|
%list_to_cudd(H._List,_Manager,_Cudd0,_CuddF) :- writeln(l:H), fail.
|
||||||
list_to_cudd([],_Manager,Cudd,Cudd) :- writeln('.').
|
list_to_cudd([],_Manager,Cudd,Cudd) :- writeln('X').
|
||||||
|
list_to_cudd(release_node(M,cudd(V)).T, Manager, Cudd0, CuddF) :- !,
|
||||||
|
write('-'), flush_output,
|
||||||
|
cudd_release_node(M,V),
|
||||||
|
list_to_cudd(T, Manager, Cudd0, CuddF).
|
||||||
list_to_cudd((V=0*_Par).T, Manager, _Cudd0, CuddF) :- !,
|
list_to_cudd((V=0*_Par).T, Manager, _Cudd0, CuddF) :- !,
|
||||||
write('0'), flush_output,
|
write('0'), flush_output,
|
||||||
term_to_cudd(0, Manager, Cudd),
|
term_to_cudd(0, Manager, Cudd),
|
||||||
@ -111,6 +143,16 @@ bdd_close(cudd(M,_,_Vars, _)) :-
|
|||||||
bdd_close(add(M,_,_Vars, _)) :-
|
bdd_close(add(M,_,_Vars, _)) :-
|
||||||
cudd_die(M).
|
cudd_die(M).
|
||||||
|
|
||||||
|
bdd_size(cudd(M,Top,_Vars, _), Sz) :-
|
||||||
|
cudd_size(M,Top,Sz).
|
||||||
|
bdd_size(add(M,Top,_Vars, _), Sz) :-
|
||||||
|
cudd_size(M,Top,Sz).
|
||||||
|
|
||||||
|
bdd_print(cudd(M,Top,_Vars, _), File) :-
|
||||||
|
cudd_print(M, Top, File).
|
||||||
|
bdd_print(add(M,Top,_Vars, _), File) :-
|
||||||
|
cudd_print(M, Top, File).
|
||||||
|
|
||||||
mtbdd_close(add(M,_,_Vars,_)) :-
|
mtbdd_close(add(M,_,_Vars,_)) :-
|
||||||
cudd_die(M).
|
cudd_die(M).
|
||||||
|
|
||||||
|
@ -1,4 +1,6 @@
|
|||||||
|
|
||||||
|
#include <stdio.h>
|
||||||
|
|
||||||
#include "YapInterface.h"
|
#include "YapInterface.h"
|
||||||
|
|
||||||
#include "util.h"
|
#include "util.h"
|
||||||
@ -600,14 +602,23 @@ p_add_to_term(void)
|
|||||||
|
|
||||||
if (!dgen)
|
if (!dgen)
|
||||||
return FALSE;
|
return FALSE;
|
||||||
t = YAP_TermNil();
|
|
||||||
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:
|
||||||
|
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 */
|
||||||
|
if (YAP_RequiresExtraStack(0)) {
|
||||||
|
Cudd_GenFree(dgen);
|
||||||
|
t3 = YAP_ARG3;
|
||||||
|
dgen = Cudd_FirstNode(manager, n0, &node);
|
||||||
|
bzero(hash, sizeof(hash_table_entry)*sz);
|
||||||
|
goto restart;
|
||||||
|
}
|
||||||
t = build_prolog_add(manager, node, ar, hash, t, sz);
|
t = build_prolog_add(manager, node, ar, hash, t, sz);
|
||||||
if (!Cudd_NextNode(dgen, &node))
|
if (!Cudd_NextNode(dgen, &node))
|
||||||
break;
|
break;
|
||||||
@ -618,6 +629,25 @@ p_add_to_term(void)
|
|||||||
return YAP_Unify(YAP_ARG4, t);
|
return YAP_Unify(YAP_ARG4, t);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
static int
|
||||||
|
p_cudd_size(void)
|
||||||
|
{
|
||||||
|
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
|
||||||
|
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2), *node;
|
||||||
|
YAP_Int i = 0;
|
||||||
|
DdGen *dgen = Cudd_FirstNode(manager, n0, &node);
|
||||||
|
|
||||||
|
if (!dgen)
|
||||||
|
return FALSE;
|
||||||
|
while (node) {
|
||||||
|
i++;
|
||||||
|
if (!Cudd_NextNode(dgen, &node))
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
Cudd_GenFree(dgen);
|
||||||
|
return YAP_Unify(YAP_ARG3, YAP_MkIntTerm(i));
|
||||||
|
}
|
||||||
|
|
||||||
typedef struct {
|
typedef struct {
|
||||||
DdNode *key;
|
DdNode *key;
|
||||||
double val;
|
double val;
|
||||||
@ -702,6 +732,18 @@ p_cudd_to_p(void)
|
|||||||
return YAP_Unify(YAP_ARG4, YAP_MkFloatTerm(p));
|
return YAP_Unify(YAP_ARG4, YAP_MkFloatTerm(p));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
static int
|
||||||
|
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");
|
||||||
|
Cudd_DumpDot(manager, 1, &n0, NULL, NULL, f);
|
||||||
|
fclose(f);
|
||||||
|
return TRUE;
|
||||||
|
}
|
||||||
|
|
||||||
static int
|
static int
|
||||||
p_cudd_die(void)
|
p_cudd_die(void)
|
||||||
{
|
{
|
||||||
@ -710,6 +752,15 @@ p_cudd_die(void)
|
|||||||
return TRUE;
|
return TRUE;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
static int
|
||||||
|
p_cudd_release_node(void)
|
||||||
|
{
|
||||||
|
DdManager *manager = (DdManager *)YAP_IntOfTerm(YAP_ARG1);
|
||||||
|
DdNode *n0 = (DdNode *)YAP_IntOfTerm(YAP_ARG2);
|
||||||
|
Cudd_RecursiveDeref(manager,n0);
|
||||||
|
return TRUE;
|
||||||
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
init_cudd(void)
|
init_cudd(void)
|
||||||
{
|
{
|
||||||
@ -743,6 +794,9 @@ init_cudd(void)
|
|||||||
YAP_UserCPredicate("cudd_to_term", p_cudd_to_term, 5);
|
YAP_UserCPredicate("cudd_to_term", p_cudd_to_term, 5);
|
||||||
YAP_UserCPredicate("add_to_term", p_add_to_term, 4);
|
YAP_UserCPredicate("add_to_term", p_add_to_term, 4);
|
||||||
YAP_UserCPredicate("cudd_to_probability_sum_product", p_cudd_to_p, 4);
|
YAP_UserCPredicate("cudd_to_probability_sum_product", p_cudd_to_p, 4);
|
||||||
|
YAP_UserCPredicate("cudd_size", p_cudd_size, 3);
|
||||||
YAP_UserCPredicate("cudd_die", p_cudd_die, 1);
|
YAP_UserCPredicate("cudd_die", p_cudd_die, 1);
|
||||||
|
YAP_UserCPredicate("cudd_release_node", p_cudd_release_node, 2);
|
||||||
|
YAP_UserCPredicate("cudd_print", p_cudd_print, 3);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Reference in New Issue
Block a user