9
10
11:- module(proof_util, [
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
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
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
151setSCV(X) :-
152 assert(scv(X)).
153
154
155
156
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
186
187count_happened(HPattern, N) :-
188 findall_constraints(HPattern, List),
189 length(List, N)