sldnf.1.2.pl

Contenuto del file

% TODO:
% stop when 1st solution found
% stop negation when 1st solution found
% CLP? Minimize?s

% Version 1.2: stops at a given depth
% Deals with cut.
% prints infixed operators

% Note that it does not handle correctly the cut in the resolvent, but only
% in a clause. Please, no do 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.

draw_goal(G,FileName):-
    open(FileName,write,File),
    term_length(G,Length),
    conv_sq_list(G,GSq),
    init_cuts,
    (draw(GSq,File,Length) ; true),
    close(File).

draw(R,F,Longest):-
    draw(R,F,Longest,30,[]).  % Default Max depth: 30

% 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([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([!|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.    

% Built-in Predicate
draw([G|R],F,LongestIn,Depth,OpenCuts):-
    Depth1 is Depth-1,
    not(G = not(_)),
    built_in(G),
    term_length([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(built_in(G)),
    term_length([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),
    %write(F,"\\chunk{fail}"),
    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 there exists no reached cut after
% the last open cut.
%clause_is_not_cut([]):-!,
%    not(reached(_)).
%clause_is_not_cut(OpenCuts):-
%    OpenCuts = [_|_],
%    last_cut(OpenCuts,Last),
%    not(
%        (reached(Cut), follows(Cut,Last))
%    ).

% With counters: the 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([],[cut(C)],cut(C),C).
%push_cut([cut(N)|T],[cut(N1),cut(N)|T],cut(N1)):-
%    N1 is N+1.
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.
%retract_cut_on_backtracking([]):-
%    retract(reached(_)), fail.
%retract_cut_on_backtracking(OpenCuts):-
%    OpenCuts = [_|_],
%    last_cut(OpenCuts,Last),
%    reached(Cut), follows(Cut,Last),
%    retract(reached(Cut)), 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 %%%%%%%%%%%%%%

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).

var_name(X,N):-
    open(string(""),write,Stream),
    write(Stream,X),
    get_stream_info(Stream, name, N),
    close(Stream).

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(F,B), write(F,"/"), write_term_no_sqbrack(F,A), 
    (T=[] -> true
        ; write(F,", "), print_binding1(F,T)).

% Writes a term replacing the symbols "[" and "]"
% with \lbrack and \rbrack, because you cannot use "["
% inside a label of an arc.
write_term_no_sqbrack(F,A):-
    var(A), !, write(F,A).
write_term_no_sqbrack(F,[]):- !,
    write(F,"\\lbrack\\rbrack ").
write_term_no_sqbrack(F,[H|T]):- !,
    write(F,"\\lbrack "),
    print_list_no_sqbrack(F,[H|T]),
    write(F,"\\rbrack ").
write_term_no_sqbrack(F,T):- 
    T =.. [Fun], !,
    write(F,Fun).
% infixed operators
write_term_no_sqbrack(F,T):-
    T =.. [Fun,ArgX,ArgY],
    current_op(_,Associativity,Fun),
    (Associativity = xfy ; Associativity = yfx ; Associativity = xfx),!,
    write_term_no_sqbrack(F,ArgX),
    pretty_write_op(F,Fun),
    write_term_no_sqbrack(F,ArgY).
write_term_no_sqbrack(F,T):- !,
    T =.. [Fun|Arg],
    write(F,Fun),
    write(F,"("),
    print_list_no_sqbrack(F,Arg),
    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(F,V):-
    var(V), !,
    write_term_no_sqbrack(F,V).
print_list_no_sqbrack(F,[H|T]):-
    var(T),!,
    write_term_no_sqbrack(F,H),
    write(F,"$|$"),
    write_term_no_sqbrack(F,T).
print_list_no_sqbrack(F,[H]):- !,
    write_term_no_sqbrack(F,H).
print_list_no_sqbrack(F,[H1,H2|T]):-
    write_term_no_sqbrack(F,H1),write(F,","),
    print_list_no_sqbrack(F,[H2|T]).

pretty_write_op(F,<):- !,
    write(F,$<$).
pretty_write_op(F,>):- !,
    write(F,$>$).
pretty_write_op(F,Op):- !,
    write(F,Op).

print_resolvent(F,X):-
    (begin_resolvent(S) -> write(F,S); true),
    print_list(F,X),
    (end_resolvent(Send) -> write(F,Send) ; true).

print_list(F,[H]):- !,
    write_term_no_sqbrack(F,H).
print_list(F,[H1,H2|T]):-
    write_term_no_sqbrack(F,H1),write(F,","),
    print_list(F,[H2|T]).

print_fail(F,Longest):-
    write(F,"\\chunk{"),
    print_string_spaces(F,Longest,"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_string(G,S), string_length(S,Length).

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).