1%----------------------------------------------------------
    2% Utilities for Java/Sicstus interfacing
    3% 
    4% Marco ALberti
    5% Federico Chesani
    6% Creation: 1 September 2003
    7% Last modification: 30 August 2005
    8%----------------------------------------------------------
    9
   10
   11:- module(proof_util, [
   12%        printConstraints/0,
   13%        printConstraints/1,
   14        setSCV/1,
   15        latest_happened/2,
   16        scv/1,
   17        crea_lista_chars/2
   18    ]).   19        
   20:- dynamic scv/1.   21
   22
   23
   24
   25
   26:- use_module( library(chr)).   27:- use_module(library(system)).   28:- use_module( library(lists)).   29:- use_module(prolog_version).   30:- (is_dialect(swi) -> true
   31   ; use_module( library(codesio))).   32:- use_module( library(terms)).   33:- use_module( library(clpfd)).   34:- use_module( print_clp_constraints).   35
   36
   37
   38
   39
   40
   41
   42%------------------------------------------------------------------------------
   43crea_lista_chars([], []) :- !.
   44crea_lista_chars([H|T], Result) :-
   45    crea_lista_chars_vincolo(H, Res1),
   46    crea_lista_chars(T, Res2),
   47    append(Res1, Res2, Result).
   48
   49crea_lista_chars_vincolo(H, Result) :-
   50    H=..[_A,B,C],
   51    converti(C, LC),
   52    converti(B, LB),
   53    append(LC, "     ", R1),
   54    append(R1, LB, R2),
   55    append(R2, "\n", Result).
   56    
   57converti(X, LX) :-
   58    X=..[suspension, N |_],
   59    !,
   60    number(N),
   61    number_to_chars(N, R1),
   62    append("<c", R1, R2),
   63    append(R2, ">", LX).
   64converti(X, L) :-
   65    X = pending(_),
   66    !,
   67    write_to_chars(X, LX),
   68    term_variables_bag(X, XVAR),
   69    create_diseq(XVAR, LCLP),
   70    append(LX, LCLP, L).
   71converti(X, L) :-
   72    X = gt_current_time(_,_),
   73    !,
   74    write_to_chars(X, LX),
   75    term_variables_bag(X, XVAR),
   76    create_diseq(XVAR, LCLP),
   77    append(LX, LCLP, L).
   78converti(X, L) :-
   79    X = inconsistent(_,_),
   80    !,
   81    write_to_chars(X, LX),
   82    term_variables_bag(X, XVAR),
   83    create_diseq(XVAR, LCLP),
   84    append(LX, LCLP, L).
   85converti(X, L) :-
   86    X = viol(_),
   87    !,
   88    write_to_chars(X, LX),
   89    term_variables_bag(X, XVAR),
   90    create_diseq(XVAR, LCLP),
   91    append(LX, LCLP, L).
   92converti(X, LX) :-
   93    write_to_chars(X, LX).
   94
   95
   96
   97create_diseq([], []) :-
   98    !.
   99create_diseq([H|T], LL) :-
  100    create_max(H, LMAX),
  101    create_min(H, LMIN),
  102    append(LMIN, LMAX, LH),
  103    create_diseq(T, LT),
  104    append(LH, LT, LL).
  105
  106create_max(X, []) :-
  107    fd_max(X, sup),
  108    !.
  109create_max(X, L) :-
  110    fd_max(X, N),
  111    write_to_chars(X, LX),
  112    append(", ", LX, L1),
  113    append(L1, " <= ", L2),
  114    number_to_chars(N, N1),
  115    append(L2, N1, L).
  116
  117create_min(X, []) :-
  118    fd_min(X, inf),
  119    !.
  120create_min(X, L) :-
  121    fd_min(X, N),
  122    write_to_chars(X, LX),
  123    append(", ", LX, L1),
  124    append(L1, " >= ", L2),
  125    number_to_chars(N, N1),
  126    append(L2, N1, L).
  127
  128
  129
  130
  131
  132
  133%------------------------------------------------------------------------------
  134% PRINTING UTILITIES THROUGH STANDARD OUTPUT
  135%------------------------------------------------------------------------------
  136stampa_lista_vincoli([]) :- !.
  137stampa_lista_vincoli([H|T]):-
  138        stampa_vincolo(H),
  139        stampa_lista_vincoli(T).
  140
  141stampa_vincolo(H) :-
  142    H=..[_A,B,C],
  143    print(C),
  144    write('     '),
  145    write(B),
  146    nl.
  147
  148%------------------------------------------------------------------------------
  149% UTILITY FOR HOOKING JAVA
  150%------------------------------------------------------------------------------
  151setSCV(X) :-
  152    assert(scv(X)).
  153    
  154
  155
  156
  157%------------------------------------------------------------------------------
  158% ACCESSING THE LATEST HAPPENED FACT...
  159%------------------------------------------------------------------------------
  160
  161
  162latest_happened(HPattern, HLatest) :-
  163	findall_constraints(HPattern, HList),
  164	latest(HList, HLatest).
  165
  166latest([], _) :- !.
  167latest([HTerm#_Id| Tail], HLatest) :-
  168	latest(Tail, HTerm, HLatest).
  169
  170latest([], HLatest, HLatest) :- !.
  171latest([HTerm#_Id| Tail], Partial, HLatest) :-
  172	get_time(HTerm, T1),
  173	get_time(Partial, T2),
  174	T2 > T1, !,
  175	latest(Tail, Partial, HLatest).
  176latest([HTerm#_Id| Tail], _Partial, HLatest) :-
  177	latest(Tail, HTerm, HLatest).
  178
  179get_time(h(_, T), T).
  180
  181
  182
  183%------------------------------------------------------------------------------
  184% COUNTING THE HAPPENED FACTS
  185%------------------------------------------------------------------------------
  186
  187count_happened(HPattern, N) :-
  188	findall_constraints(HPattern, List),
  189	length(List, N)