sldnf.pl
sldnf.pl
—
text/x-perl,
13 kB (14147 bytes)
Contenuto del file
% SLDNF Draw
% Produces a LaTeX drawing of an SLDNF tree
% Author: Marco Gavanelli
% http://www.ing.unife.it/docenti/MarcoGavanelli/sldnfDraw/
% Version 1.4
% Does not crash when printing infinite terms
% Uses lib(var_names) for pretty printing the names of variables.
% Version 1.5
% If the resolvent is too long (over max_resolvent_length/1 characters), prints it in two or more rows
sldnf_version(1.5).
% TODO:
% stop when 1st solution found
% stop negation when 1st solution found
% CLP? Minimize?
:- lib(var_name).
% Note that it does not handle correctly the cut in the resolvent, but only
% in a clause. Please, do not write ?- p,!. but define e new predicate
% callp:- p,!.
% Given a clause a:-b,!,c, we have that:
% 1.the scope of the cut is a:-b, in the sense that it will cut the
% alternatives to a and b. This is represented with the list
% of OpenCuts: it contains all the cuts that are in a clause that
% has been selected.
% 2.The cut has an effect when it is reached, and its effect lasts
% until the backtracking goes back to a. Thus, the information about
% reaching a cut is saved with assert(reached(Cut)).
% Each cut has a unique name, given by a counter.
:- dynamic begin_resolvent/1, end_resolvent/1, begin_binding/1, end_binding/1, counter/1, reached/1, maxdepth/1.
:- dynamic my_clause/2.
% Maximum length of the resolvent, in chars (very approximate)
% If the length exceeds this length, the resolvent will be printed on two (or more) lines
:- dynamic max_resolvent_length/1.
max_resolvent_length(25).
set_depth(D):-
retract(maxdepth(_)),
assert(maxdepth(D)).
maxdepth(20). % Default max depth: 20
d(G):- draw_goal(G,"tree.tex").
draw_goal(G,FileName):-
init_file(FileName,write,File),
term_length_chopped(G,Length),
conv_sq_list(G,GSq),
init_cuts,
(draw(GSq,File,Length) ; true),
close(File).
draw(R,F,Longest):-
maxdepth(Depth),
draw(R,F,Longest,Depth,[]).
% draw(+Resolvent,+Stream,MaxLenghtOfResolvent,MaxDepth,OpenCuts)
draw([],F,Longest,_,_):-
print_string_spaces(F,Longest,"true"),
fail.
draw(_,F,Longest,0,_):- !,
print_string_spaces(F,Longest,"..."),
fail.
draw([not G|R],F,LongestIn,Depth,OpenCuts):-
Depth1 is Depth-1,
write(F,"\\begin{bundle}{"),
print_resolvent(F,[not G|R]),
writeln(F,"}\n\\chunk{"),
% NOTA: forse in questo caso non conviene metterlo, cosi` il box diventa giusto.
% pero` non si assicura che sia giusto il figlio del box...
% Compute the maximum length
term_length_chopped([not G|R],ResLen), Length is max(LongestIn,ResLen),
write(F,"\\begin{bundle}{\\framebox{"),
(draw([G],F,0,Depth1,[]) ; true),
write(F,"}}"),
(vanilla(G)
-> print_fail(F,ResLen)
; write(F,"\\chunk{"),
(draw(R,F,Length,Depth1,OpenCuts); true), write(F,"}")
),
writeln(F,"\\end{bundle}}\\end{bundle}"),
fail.
% Cut !
draw([!|R],F,LongestIn,Depth,[LastCut|OpenCuts]):- !,
Depth1 is Depth-1,
term_length_chopped([!|R],ResLen), Length is max(LongestIn,ResLen),
write(F,"\\begin{bundle}{"),
print_resolvent(F,[!|R]),
writeln(F,"}"),
assert(reached(LastCut)),
(print_builtin_children(true,R,F,Length,Depth1,OpenCuts); writeln(F,"\\end{bundle}")),
fail.
% Conjunction of goals: may occur inside another predicate, like not((G1,G2)).
draw([(G1,G2)|R],F,LongestIn,Depth,OpenCuts):-
draw([G1,G2|R],F,LongestIn,Depth,OpenCuts).
% Built-in Predicate
draw([G|R],F,LongestIn,Depth,OpenCuts):-
Depth1 is Depth-1,
not(G = not(_)),
not(G=(_,_)),
built_in(G),
term_length_chopped([G|R],ResLen), Length is max(LongestIn,ResLen),
write(F,"\\begin{bundle}{"),
print_resolvent(F,[G|R]),
writeln(F,"}"),
(print_builtin_children(G,R,F,Length,Depth1,OpenCuts); writeln(F,"\\end{bundle}")),
fail.
% User defined predicate
draw([G|R],F,LongestIn,Depth,OpenCuts):-
Depth1 is Depth-1,
not(G = not(_)),
not(G=(_,_)),
not(built_in(G)),
term_length_chopped([G|R],ResLen), Length is max(LongestIn,ResLen),
write(F,"\\begin{bundle}{"),
print_resolvent(F,[G|R]),
writeln(F,"}"),
(print_children(G,R,F,Length,Depth1,OpenCuts); writeln(F,"\\end{bundle}")),
fail.
print_children(G,R,F,Length,Depth,OpenCuts):-
Depth1 is Depth-1,
term_variables(G,Vars),
vars_names(Vars,VarNames),
count_children(G,NumChildren),
(NumChildren = 1 -> Len = Length ; Len=0),
increase_counter, get_counter(C),
% Unique name for the node: if a cut is reached, it will have this name
% First part: the cut may cut the alternatives for the clause
retract_cut_on_backtracking(C),
clausola(G,B),
(clause_is_not_cut(C)
-> true
; write(F,"\\chunk{(cut)}"), fail),
(check_body_contains_cut(B,OpenCuts,NewCuts,_AddedCut,C)
-> % retract_cut_on_backtracking(AddedCut)
true
; NewCuts=OpenCuts),
% Second part: takes care of the alternatives of the predicates
% in the body
( (member(Cut,OpenCuts),reached(Cut))
-> write(F,"\\chunk{(cut)}"), fail
; write(F,"\\chunk"),
print_binding(F,VarNames),
write(F,"{"),
append(B,R,Ris),
(draw(Ris,F,Len,Depth1,NewCuts) ; write(F,"}"), fail)
).
print_children(G,_,F,Length,_Depth,_):-
not(clausola(G,_)),
print_fail(F,Length),
fail.
print_builtin_children(G,R,F,Length,Depth,OpenCuts):-
Depth1 is Depth-1,
term_variables(G,Vars),
vars_names(Vars,VarNames),
findall(G,call(G),L),length(L,NumChildren),
(NumChildren = 1 -> Len = Length ; Len=0),
call(G),
write(F,"\\chunk"),
print_binding(F,VarNames),
write(F,"{"),
(draw(R,F,Len,Depth1,OpenCuts) ; write(F,"}"), fail).
print_builtin_children(G,_,F,Length,_Depth,_OpenCuts):-
not(call(G)),
print_fail(F,Length),
fail.
%%%%%%%%%%%%%%%% Predicates fot cut handling %%%%%%%%%%%%%%%%%
%check_body_contains_cut(+Body,++OpenCuts,-NewCuts,-AddedCut,++Counter)
check_body_contains_cut(B,OpenCuts,NewCuts,AddedCut,Counter):-
memberchk(!,B),push_cut(OpenCuts,NewCuts,AddedCut,Counter).
% A clause is not cut if the cut of the current
% node has not been reached.
clause_is_not_cut(C):-
not reached(cut(C)).
push_cut(L,[cut(C)|L],cut(C),C).
% On backtracking, remove the information about the reached cuts
% that are not open
retract_cut_on_backtracking(_).
retract_cut_on_backtracking(C):-
retract(reached(C)), fail.
follows(cut(N),cut(N1)):-
N>N1.
last_cut([C],C):-!.
last_cut([Cut|Cuts],C):-
last_cut(Cuts,LastSoFar),
(follows(LastSoFar,Cut)
-> C=LastSoFar
; C=Cut).
init_cuts:- retract_all(reached(_)),
reset_counter.
increase_counter:-
counter(C), retract(counter(C)), C1 is C+1,
assert(counter(C1)).
get_counter(C):- counter(C).
reset_counter:- retract_all(counter(_)),
assert(counter(0)).
%%%%%%%%%%%%%%% End predicates for cut handling %%%%%%%%%%%%%%
%%%%%%%%%%%%%%% Utilities %%%%%%%%%%%%%%
count_children(G,NumChildren):-
findall(B,clausola(G,B),L),
length(L,NumChildren).
vars_names([],[]).
vars_names([X|T],[b(X,N)|TN]):-
var_name(X,N),
vars_names(T,TN).
term_to_string(Term,String):-
open(string(""),write,Stream),
write(Stream,Term),
get_stream_info(Stream, name, String),
close(Stream).
var_name(X,N):-
get_var_name(X,N),!.
var_name(X,NewName):-
term_to_string(X,N),
(var(X)
-> % if the variable name starts with underscore, set X as its name
(string_list(N,[95|_]) -> set_var_name(X,'X')
; set_var_name(X,N)),
get_var_name(X,NewName)
; NewName=N).
print_binding(F,X):-
write(F,"["),
(begin_binding(S) -> write(F,S); true),
print_binding1(F,X),
(end_binding(Send) -> write(F,Send) ; true),
write(F,"]").
print_binding1(_F,[]).
print_binding1(F,[b(A,B)|T]):-
var_name(A,Name),
Name = B, !,
% Avoid writing "X=X" as a binding...
print_binding1(F,T).
print_binding1(F,[b(A,B)|T]):-
write_var(F,B), write(F,"/"),
(acyclic_term(A)
-> write_term_no_sqbrack(F,A,1000)
; maxdepth(D), write_term_no_sqbrack(F,A,D)
),
(T=[] -> true
; write(F,", "), print_binding1(F,T)).
write_var(F,V):-
var(V),
var_name(V,VarName),!,
split_string(VarName,"#","",[Name,Number]),
write(F,"$"),
write(F,Name),
write(F,"_{"),
write(F,Number),
write(F,"}$").
write_var(F,VarName):-
string(VarName),
split_string(VarName,"#","",[Name,Number]),!,
write(F,"$"),
write(F,Name),
write(F,"_{"),
write(F,Number),
write(F,"}$").
% Writes a term replacing the symbols "[" and "]"
% with \lbrack and \rbrack, because you cannot use "["
% inside a label of an arc.
% Stops at depth Depth
% write_term_no_sqbrack(File,Term,Depth):-
write_term_no_sqbrack(F,_,0):- !,
write(F,"\\dots").
write_term_no_sqbrack(F,A,_):-
% Named Variables
var(A), !,
write_var(F,A).
write_term_no_sqbrack(F,[],_):- !,
write(F,"\\lbrack\\rbrack ").
write_term_no_sqbrack(F,[H|T],N):- !,
write(F,"\\lbrack "),
print_list_no_sqbrack(F,[H|T],N),
write(F,"\\rbrack ").
write_term_no_sqbrack(F,T,_):-
T =.. [Fun], !,
write(F,Fun).
% infixed operators
write_term_no_sqbrack(F,T,N):-
T =.. [Fun,ArgX,ArgY],
N1 is N-1,
current_op(_,Associativity,Fun),
(Associativity = xfy ; Associativity = yfx ; Associativity = xfx),!,
write_term_no_sqbrack(F,ArgX,N1),
pretty_write_op(F,Fun),
write_term_no_sqbrack(F,ArgY,N1).
write_term_no_sqbrack(F,T,N):- !,
N1 is N-1,
T =.. [Fun|Arg],
write(F,Fun),
write(F,"("),
print_list_no_sqbrack(F,Arg,N1),
write(F,")").
% If the list is a difference list, we also have the
% case in which the rest is a variable.
%print_list_no_sqbrack(File,Term,Depth)
print_list_no_sqbrack(F,V,N):-
var(V), !,
write_term_no_sqbrack(F,V,N).
print_list_no_sqbrack(F,[H|T],N):-
var(T),!,
write_term_no_sqbrack(F,H,N),
write(F,"$|$"),
write_term_no_sqbrack(F,T,N).
print_list_no_sqbrack(F,[H],N):- !,
write_term_no_sqbrack(F,H,N).
print_list_no_sqbrack(F,[H1,H2|T],N):-
N1 is N-1,
write_term_no_sqbrack(F,H1,N1),write(F,","),
print_list_no_sqbrack(F,[H2|T],N1).
pretty_write_op(F,<):- !,
write(F,$<$).
pretty_write_op(F,=<):- !,
write(F,$=<$).
pretty_write_op(F,>=):- !,
write(F,$>=$).
pretty_write_op(F,>):- !,
write(F,$>$).
pretty_write_op(F,is):- !,
write(F," is ").
pretty_write_op(F,\=):- !,
write(F,"$\\backslash=$").
pretty_write_op(F,Op):- !,
write(F,Op).
print_resolvent(F,X):-
(begin_resolvent(S) -> write(F,S); true),
term_length(X,Len),
max_resolvent_length(MaxLength),
(X=[_,_|_], Len>MaxLength
-> write(F,"\\begin{tabular}{c}"),
print_list_tabular(F,X),
writeln(F,"\\end{tabular}")
; print_list(F,X)
),
(end_resolvent(Send) -> write(F,Send) ; true).
% Prints a list in a tabular environment, without exceeding max_resolvent_length in each row
print_list_tabular(F,[A]):-!, print_list(F,[A]).
print_list_tabular(F,X):-
append2(First,Rest,X),
(First = [_]
-> true
; term_length(First,Len1),
max_resolvent_length(MaxLength),
Len1<MaxLength,!
),
(Rest=[] -> true
; print_list(F,First),write(F,",\\\\"),
print_list_tabular(F,Rest)
).
% Like append, but provides the solutions in the opposite order
% i.e., if the third argument is ground and the others are not,
% first provides the longest lists as first aruments
append2([H|T],X,[H|S]):-
append2(T,X,S).
append2([],X,X).
print_list(F,[H]):- !,
maxdepth(D),
write_term_no_sqbrack(F,H,D).
print_list(F,[H1,H2|T]):-
maxdepth(D),
write_term_no_sqbrack(F,H1,D),write(F,","),
print_list(F,[H2|T]).
print_fail(F,Longest):-
write(F,"\\chunk{"),
max_resolvent_length(MaxLength),
(Longest < MaxLength
-> print_string_spaces(F,Longest,"false")
; print_string_spaces(F,MaxLength,"false")
),
write(F,"}").
% Prints a string adding "Longest" spaces.
print_string_spaces(F,Longest,String):-
NumSpace is Longest//2,
print_n_spaces(F,NumSpace),
write(F,String), writeln(F,"\n"),
print_n_spaces(F,NumSpace).
print_n_spaces(_,0):- !.
print_n_spaces(F,N):-
number(N), N>0,
write(F,"~"),
N1 is N-1,
print_n_spaces(F,N1).
vanilla([]).
vanilla([A|B]) :- !, vanilla(A), vanilla(B).
vanilla(not X) :- !,
(vanilla(X) -> fail ; true).
vanilla(X) :-
built_in(X), call(X).
vanilla(X) :-
clausola(X,Body),
vanilla(Body).
term_length(G,Length):-
term_to_string(G,S),
string_length(S,Length).
term_length_chopped(G,L):-
max_resolvent_length(MaxTermLength),
term_length(G,Length),
(Length=<MaxTermLength
-> L=Length
; L=MaxTermLength
).
remove_char(Sin,Char,Sout):-
split_string(Sin,Char,"",SubStrings),
concat_string(SubStrings,Sout).
clausola(H,BSq):-
functor(H,F,A), current_predicate(F/A),
clause(H,B),
conv_sq_list(B,BSq).
clausola(H,BSq):-
my_clause(H,BSq).
conv_sq_list((A,B),[A|Bsq]):- !,
conv_sq_list(B,Bsq).
conv_sq_list(true,[]):- !.
conv_sq_list(X,[X]).
built_in(G):-
functor(G,F,A),
current_built_in(F/A).
init_file(FileName,write,File):-
open(FileName,write,File),
write(File,"% File created by SLDNF Draw version "),
sldnf_version(Ver),
writeln(File,Ver),
writeln(File,"% http://www.ing.unife.it/docenti/MarcoGavanelli/sldnfDraw/"),
nl(File).
