Merge branch 'master' of /home/vitor/yap-6.3

This commit is contained in:
Vitor Santos Costa 2012-04-20 16:44:27 -05:00
commit 3aee05ae9e
3 changed files with 214 additions and 71 deletions

View File

@ -53,6 +53,10 @@ Va <- P*X1*Y1 + Q*X2*Y2 + ...
:- use_module(library(bdd)).
:- use_module(library(ddnnf)).
:- use_module(library(simpbool)).
:- use_module(library(rbtrees)).
:- use_module(library(bhash)).
@ -63,6 +67,9 @@ Va <- P*X1*Y1 + Q*X2*Y2 + ...
:- attribute order/1.
:- dynamic bdds/1.
bdds(ddnnf).
check_if_bdd_done(_Var).
bdd([[]],_,_) :- !.
@ -271,7 +278,7 @@ avg_tree( _PVars, P, _, Im, IM, _Size, O, H0, H0) :-
b_hash_lookup(k(P,Im,IM), O=_Exp, H0), !.
avg_tree([], _P, _Max, _Im, _IM, _Size, 1, H, H).
avg_tree([Vals|PVars], P, Max, Im, IM, Size, O, H0, HF) :-
b_hash_insert(H0, k(P,Im,IM), O=Simp, HI),
b_hash_insert(H0, k(P,Im,IM), O=Simp*1, HI),
MaxI is Max-(Size-1),
avg_exp(Vals, PVars, 0, P, MaxI, Size, Im, IM, HI, HF, Exp),
simplify_exp(Exp, Simp).
@ -732,7 +739,6 @@ run_bdd_solver([[V]], LPs, bdd(Term, _Leaves, Nodes)) :-
build_out_node(Nodes, Node),
findall(Prob, get_prob(Term, Node, V, Prob),TermProbs),
sumlist(TermProbs, Sum),
writeln(TermProbs:Sum),
normalise(TermProbs, Sum, LPs).
build_out_node([_Top], []).
@ -744,7 +750,12 @@ build_out_node2([T,T1|Tops], T*Top) :-
build_out_node2(T1.Tops, Top).
get_prob(Term, _Node, V, SP) :-
bdds(ddnnf), !,
all_cnfs(Term, CNF, IVs, Indics, V, AllParms, AllParmValues),
build_cnf(CNF, IVs, Indics, AllParms, AllParmValues, SP).
get_prob(Term, Node, V, SP) :-
bdds(bdd), !,
bind_all(Term, Node, Bindings, V, AllParms, AllParmValues),
% reverse(AllParms, RAllParms),
term_variables(AllParms, NVs),
@ -754,25 +765,25 @@ get_prob(Term, Node, V, SP) :-
build_bdd(Bindings, NVs, VTheta, Theta, Bdd) :-
bdd_from_list(Bindings, NVs, Bdd),
bdd_size(Bdd, Len),
number_codes(Len,Codes),
atom_codes(Name,Codes),
bdd_print(Bdd, Name),
writeln(length=Len),
% bdd_size(Bdd, Len),
% number_codes(Len,Codes),
% atom_codes(Name,Codes),
% bdd_print(Bdd, Name),
% writeln(length=Len),
VTheta = Theta.
bind_all([], End, End, _V, [], []).
bind_all(info(V, _Tree, Ev, _Values, Formula, ParmVars, Parms).Term, End, BindsF, V0, ParmVars.AllParms, Parms.AllTheta) :-
bind_all([info(V, _Tree, Ev, _Values, Formula, ParmVars, Parms)|Term], End, BindsF, V0, ParmVars.AllParms, Parms.AllTheta) :-
V0 == V, !,
set_to_one_zeros(Ev),
bind_formula(Formula, BindsF, BindsI),
bind_all(Term, End, BindsI, V0, AllParms, AllTheta).
bind_all(info(_V, _Tree, Ev, _Values, Formula, ParmVars, Parms).Term, End, BindsF, V0, ParmVars.AllParms, Parms.AllTheta) :-
bind_all([info(_V, _Tree, Ev, _Values, Formula, ParmVars, Parms)|Term], End, BindsF, V0, ParmVars.AllParms, Parms.AllTheta) :-
set_to_ones(Ev),!,
bind_formula(Formula, BindsF, BindsI),
bind_all(Term, End, BindsI, V0, AllParms, AllTheta).
% evidence: no need to add any stuff.
bind_all(info(_V, _Tree, _Ev, _Values, Formula, ParmVars, Parms).Term, End, BindsF, V0, ParmVars.AllParms, Parms.AllTheta) :-
bind_all([info(_V, _Tree, _Ev, _Values, Formula, ParmVars, Parms)|Term], End, BindsF, V0, ParmVars.AllParms, Parms.AllTheta) :-
bind_formula(Formula, BindsF, BindsI),
bind_all(Term, End, BindsI, V0, AllParms, AllTheta).
@ -800,3 +811,103 @@ normalise(P.TermProbs, Sum, NP.LPs) :-
finalize_bdd_solver(_).
all_cnfs([], [], [], [], _V, [], []).
all_cnfs([info(V, Tree, Ev, Values, Formula, ParmVars, Parms)|Term], BindsF, IVars, Indics, V0, AllParmsF, AllThetaF) :-
%writeln(f:Formula),
V0 == V, !,
set_to_one_zeros(Ev),
all_indicators(Values, BindsF, Binds0),
indicators(Values, [], Ev, IVars, IVarsI, Indics, IndicsI, Binds0, Binds1),
parms( ParmVars, Parms, AllParmsF, AllThetaF, AllParms, AllTheta),
parameters(Formula, Tree, Binds1, BindsI),
all_cnfs(Term, BindsI, IVarsI, IndicsI, V0, AllParms, AllTheta).
all_cnfs([info(_V, Tree, Ev, Values, Formula, ParmVars, Parms)|Term], BindsF, IVars, Indics, V0, AllParmsF, AllThetaF) :-
set_to_ones(Ev),!,
all_indicators(Values, BindsF, Binds0),
indicators(Values, [], Ev, IVars, IVarsI, Indics, IndicsI, Binds0, Binds1),
parms( ParmVars, Parms, AllParmsF, AllThetaF, AllParms, AllTheta),
parameters(Formula, Tree, Binds1, BindsI),
all_cnfs(Term, BindsI, IVarsI, IndicsI, V0, AllParms, AllTheta).
% evidence: no need to add any stuff.
all_cnfs([info(_V, Tree, Ev, Values, Formula, ParmVars, Parms)|Term], BindsF, IVars, Indics, V0, AllParmsF, AllThetaF) :-
all_indicators(Values, BindsF, Binds0),
indicators(Values, [], Ev, IVars, IVarsI, Indics, IndicsI, Binds0, Binds1),
parms( ParmVars, Parms, AllParmsF, AllThetaF, AllParms, AllTheta),
parameters(Formula, Tree, Binds1, BindsI),
all_cnfs(Term, BindsI, IVarsI, IndicsI, V0, AllParms, AllTheta).
all_indicators(Values) -->
{ values_to_disj(Values, Disj) },
[Disj].
values_to_disj([V], V) :- !.
values_to_disj([V|Values], V+Disj) :-
values_to_disj(Values, Disj).
indicators([V|Vars], SeenVs, [E|Ev], [V|IsF], IsI, [E|Inds], Inds0) -->
generate_exclusions(SeenVs, V),
indicators(Vars, [V|SeenVs], Ev, IsF, IsI, Inds, Inds0).
indicators([], _SeenVs, [], IsF, IsF, Inds, Inds) --> [].
parms([], [], AllParms, AllTheta, AllParms, AllTheta).
parms([V|ParmVars], [P|Parms], [V|AllParmsF], [P|AllThetaF], AllParms, AllTheta) :-
parms( ParmVars, Parms, AllParmsF, AllThetaF, AllParms, AllTheta).
parameters([], _) --> [].
% ignore disj, only useful to BDDs
parameters([(T=_)|Formula], Tree) -->
{ Tree == T }, !,
parameters(Formula, Tree).
parameters([(V0=Disj*_I0)|Formula], Tree) -->
conj(Disj, V0),
parameters(Formula, Tree).
% transform V0<- A*B+C*(D+not(E))
% [V0+not(A)+not(B),V0+not(C)+not(D),V0+not(C)+E]
conj(Disj, V0) -->
{ conj2(Disj, [[V0]], LVs) },
to_disjs(LVs).
conj2(A, L0, LF) :- var(A), !,
add(not(A), L0, LF).
conj2((A*B), L0, LF) :-
conj2(A, L0, LI),
conj2(B, LI, LF).
conj2((A+B), L0, LF) :-
conj2(A, L0, L1),
conj2(B, L0, L2),
append(L1, L2, LF).
conj2(not(A), L0, LF) :-
add(A, L0, LF).
add(_, [], []).
add(Head, [H|L], [[Head|H]|NL]) :-
add(Head, L, NL).
to_disjs([]) --> [].
to_disjs([[H|L]|LVs]) -->
mkdisj(L, H),
to_disjs(LVs).
mkdisj([], Disj) --> [Disj].
mkdisj([H|L], Disj) -->
mkdisj(L, (H+Disj)).
%
% add formula for V \== V0 -> V or V0 and not(V) or not(V0)
%
generate_exclusions([], _V) --> [].
generate_exclusions([V0|SeenVs], V) -->
[(not(V0)+not(V))],
generate_exclusions(SeenVs, V).
build_cnf(CNF, IVs, Indics, AllParms, AllParmValues, Val) :-
%(numbervars(CNF,1,_), writeln(cnf_to_ddnnf(CNF, Vars, IVs, [], F)), fail ; true ),
cnf_to_ddnnf(CNF, AllParms, F),
AllParms = AllParmValues,
IVs = Indics,
term_variables(CNF, Extra),
set_to_ones(Extra),
ddnnf_is(F, Val).

View File

@ -244,7 +244,9 @@ get_dist_domain_size(Id, DSize) :-
recorded(clpbn_dist_db, db(Id, _, _, _, _, _, DSize), _).
get_dist_domain(Id, Domain) :-
recorded(clpbn_dist_db, db(Id, _, _, _, Domain, _, _), _).
recorded(clpbn_dist_db, db(Id, _, _, _, Domain, _, _), _), !.
get_dist_domain(avg(Domain), Domain) :-
recorded(clpbn_dist_db, db(Id, _, _, _, Domain, _, _), _), !.
get_dist_key(Id, Key) :-
use_parfactors(on), !,

View File

@ -1,13 +1,9 @@
:- module(ddnnf,
[assignments_to_ddnnf/4,
[cnf_to_ddnnf/3,
ddnnf/3,
ddnnf_is/2]).
:- source.
:- style_check(all).
:- use_module(library(lists)).
:- use_module(library(readutil)).
:- use_module(library(lineutils)).
@ -15,35 +11,46 @@
:- use_module(library(cnf)).
:- use_module(library(simpbool)).
assignments_to_ddnnf(List, Vars, LVars, DDNNF) :-
list2cnfs(List, CNF, []),
% (numbervars(CNF,1,_), writeln(Vars:CNF), fail ; true),
open(dimacs, write, S),
%
% convert a CNF as list with Variables Vars and Existential variables
% in DDNNF, Exs \in LVars into DDNNF with extra existential vars
%
cnf_to_ddnnf(CNF0, PVs, DDNNF) :-
term_variables(CNF0, Vars),
list2cnf(CNF0, CNF, []),
new_variables_in_term(Vars, CNF, LVars),
append(Vars, LVars, MVars),
cnf_to_file(CNF, MVars, S),
append(Vars, LVars, AllVars),
% (numbervars(CNF,1,_), writeln(CNF), fail ; true),
open(dimacs, write, S),
cnf_to_file(CNF, AllVars, S),
close(S),
% execute c2d at this point, but we're lazy
unix(system('c2d -dt_method 3 -in dimacs')),
% execute c2d at this point, but we're lazy%
% unix(system('c2d -dt_method 3 -in dimacs')),
unix(system('c2d -visualize -in dimacs')),
open('dimacs.nnf',read,R),
SVars =.. [v|MVars],
SVars =.. [v|AllVars],
% ones(LVars),
input_ddnnf(R, SVars, DDNNF),
input_ddnnf(R, SVars, PVs, DDNNF),
% writeln(DDNNF),
close(R).
list2cnfs([]) --> [].
list2cnfs([(O=Impl)|Impls]) --> !,
{cvt(O,FO)},
disj2cnf(Impl, FO),
list2cnfs(Impls).
list2cnfs([CNF|Impls]) -->
list2cnf([]) --> [].
list2cnf([(O=A)|Impls]) --> !,
{cvt(O,FO,NO),
and2cnf(A,Conj,[]) },
[[FO|Conj]],
disj(A, NO),
list2cnf(Impls).
list2cnf([CNF|Impls]) -->
{ to_format(CNF, Format, []) },
[Format],
list2cnfs(Impls).
list2cnf(Impls).
cvt(O,O) :- var(O), !.
cvt(not(O),-O).
cvt(O,O,-O) :- var(O), !.
cvt(not(O),-O,O).
neg(O,-O) :- var(O), !.
neg(-O,O).
to_format(A) -->
{ var(A) },
@ -60,18 +67,6 @@ to_format(A) -->
[A].
disj2cnf(B, O) -->
{ var(B) }, !,
[[O|R]],
{ and2cnf(B, R, []) }.
disj2cnf(A+B, O) -->
!,
disj2cnf(A, O),
disj2cnf(B, O).
disj2cnf(B, O) -->
[[O|R]],
{ and2cnf(B, R, []) }.
and2cnf(A) -->
{ var(A) },
!,
@ -87,26 +82,43 @@ and2cnf(A) -->
!,
[-A].
ddnnf(List, Vars, DDNNF) :-
disj(A, NO) -->
{ var(A) }, !,
[[NO,A]].
disj(A*B, NO) --> !,
disj(A, NO),
disj(B, NO).
disj(A, NO) -->
[[NO,A]].
%
% convert a boolean expression with Variables Vars and Existential variables
% in DDNNF, Exs \in LVars into DDNNF with extra existential vars
%
% ex: (A*B+not(B))*(C=B) into something complicated
%
ddnnf(List, PVs, DDNNF) :-
exps2conj(List, Conj),
once(cnf(Conj, CNF)),
(numbervars(CNF,1,_), writeln(Vars:CNF), fail ; true),
cnf(Conj, CNF),
% (numbervars(CNF,1,_), writeln(Vars:CNF), fail ; true),
open(dimacs, write, S),
new_variables_in_term(Vars, CNF, LVars),
append(Vars, LVars, MVars),
cnf_to_file(CNF, MVars, S),
variables_in_term(PVs, CNF, LVars),
append(PVs, LVars, AllVars),
cnf_to_file(CNF, AllVars, S),
close(S),
% execute c2d at this point, but we're lazy
unix(system('c2d -in dimacs')),
open('dimacs.nnf',read,R),
SVars =.. [v|MVars],
SVars =.. [v|AllVars],
% ones(LVars),
input_ddnnf(R, SVars, DDNNF),
input_ddnnf(R, SVars, PVs, DDNNF),
close(R).
exps2conj([Conj], Conj) :- !.
exps2conj([Head|List], Head*Conj) :-
exps2conj(List, Conj).
exps2conj((C1,C2), CC1*CC2) :- !,
exps2conj(C1, CC1),
exps2conj(C2, CC2).
exps2conj((Conj), CConj) :-
cvt_el(Conj, CConj).
cvt_el(V, V) :- var(V), !.
cvt_el(not(X), -X1) :- !,
@ -117,6 +129,9 @@ cvt_el(X+Y, X1+Y1) :- !,
cvt_el(X*Y, X1*Y1) :- !,
cvt_el(X, X1),
cvt_el(Y, Y1).
cvt_el(X=Y, X1==Y1) :- !,
cvt_el(X, X1),
cvt_el(Y, Y1).
cvt_el(X, X).
cnf_to_file(List, Vars, S) :-
@ -147,39 +162,47 @@ output_cnf([V|CNF], S) :-
format(S, '~d ',[V]),
output_cnf(CNF, S).
input_ddnnf(Stream, SVars, ddnnf(Out, SVars, Result)) :-
input_ddnnf(Stream, SVars, PVs, ddnnf(Out, SVars, Result)) :-
read_line_to_codes(Stream, Header),
split(Header, ["nnf",VS,_ES,_NS]),
number_codes(NVs, VS),
functor(TempResults, nnf, NVs),
process_nnf_lines(Stream, SVars, 1, TempResults, Out, Last),
process_nnf_lines(Stream, SVars, PVs, 1, TempResults, Out, Last),
Last1 is Last-1,
arg(Last1, TempResults, Result).
process_nnf_lines(Stream, SVars, LineNumber, TempResults, O, LL) :-
process_nnf_lines(Stream, SVars, PVs, LineNumber, TempResults, O, LL) :-
read_line_to_codes(Stream, Codes),
( Codes = end_of_file -> O = [], LL = LineNumber ;
% (LineNumber > 1 -> N is LineNumber-1, arg(N,TempResults,P), format("~w ",[P]);true),
% format("~s~n",[Codes]),
arg(LineNumber, TempResults, P),
process_nnf_line(SVars, TempResults, Exp0, Codes, []),
process_nnf_line(SVars, PVs, TempResults, Exp0, Codes, []),
simplify_line(P=Exp0, Lines, O),
NewLine is LineNumber+1,
process_nnf_lines(Stream, SVars, NewLine, TempResults, Lines, LL)
process_nnf_lines(Stream, SVars, PVs, NewLine, TempResults, Lines, LL)
).
process_nnf_line(SVars, _TempResults, Exp) --> "L ",
nnf_leaf(SVars, Exp).
process_nnf_line(_SVars, TempResults, Exp) --> "A ",
process_nnf_line(SVars, PVs, _TempResults, Exp) --> "L ",
nnf_leaf(SVars, PVs, Exp).
process_nnf_line(_SVars, _, TempResults, Exp) --> "A ",
nnf_and_node(TempResults, Exp).
process_nnf_line(_SVars, TempResults, Exp) --> "O ",
process_nnf_line(_SVars, _, TempResults, Exp) --> "O ",
nnf_or_node(TempResults, Exp).
nnf_leaf(SVars, Prob, Codes, []) :-
nnf_leaf(SVars, PVs, Prob, Codes, []) :-
number_codes(Number, Codes),
Abs is abs(Number),
arg(Abs, SVars, Node),
(Number < 0 -> Prob = (1-Node) ; Prob = Node).
(Number < 0 ->
(parameter(Node,PVs) -> Prob = 1-Node ; Prob = 1 )
;
Prob = Node
).
parameter(F,[F1|_Exs]) :- F == F1, !.
parameter(F,[_|Exs]) :-
parameter(F, Exs).
nnf_and_node(TempResults, Product, Codes, []) :-
split(Codes, [_|NumberAsStrings]),
@ -218,12 +241,19 @@ propagate_constants(0, 0, Lines, Lines) :- !.
propagate_constants(1, 1, Lines, Lines) :- !.
propagate_constants(Exp, A, Lines, [(A=Exp)|Lines]).
ddnnf_is(ddnnf(F, _Vs, Out), Out) :-
%
% compute the value of a SP
%
%
ddnnf_is(ddnnf(F, Vs, Out), Out) :-
term_variables(Vs,LVs),
ones(LVs),
%(numbervars(F,1,_),writeln(F),fail;true),
ddnnf_is_acc(F).
%ddnnf_is_acc([H=Exp|_]) :- writeln((H=Exp)),fail.
ddnnf_is_acc([]).
ddnnf_is_acc([H=Exp|Attrs]) :-
% term_variables(Exp, Vs), ones(Vs),
H is Exp,
%writeln(Exp:H),
ddnnf_is_acc(Attrs).