1/*
2
3    Part of CLP(R) (Constraint Logic Programming over Reals)
4
5    Author:        Leslie De Koninck
6    E-mail:        Leslie.DeKoninck@cs.kuleuven.be
7    WWW:           http://www.swi-prolog.org
8		   http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
9    Copyright (C): 2004, K.U. Leuven and
10		   1992-1995, Austrian Research Institute for
11		              Artificial Intelligence (OFAI),
12			      Vienna, Austria
13
14    This software is part of Leslie De Koninck's master thesis, supervised
15    by Bart Demoen and daily advisor Tom Schrijvers.  It is based on CLP(Q,R)
16    by Christian Holzbaur for SICStus Prolog and distributed under the
17    license details below with permission from all mentioned authors.
18
19    This program is free software; you can redistribute it and/or
20    modify it under the terms of the GNU General Public License
21    as published by the Free Software Foundation; either version 2
22    of the License, or (at your option) any later version.
23
24    This program is distributed in the hope that it will be useful,
25    but WITHOUT ANY WARRANTY; without even the implied warranty of
26    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
27    GNU General Public License for more details.
28
29    You should have received a copy of the GNU Lesser General Public
30    License along with this library; if not, write to the Free Software
31    Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
32
33    As a special exception, if you link this library with other files,
34    compiled with a Free Software compiler, to produce an executable, this
35    library does not by itself cause the resulting executable to be covered
36    by the GNU General Public License. This exception does not however
37    invalidate any other reasons why the executable file might be covered by
38    the GNU General Public License.
39*/
40
41:- module(itf_r,
42	[
43	    do_checks/8
44	]).
45:- use_module(library(apply), [maplist/2]).
46:- use_module(bv_r,
47	[
48	    deref/2,
49	    detach_bounds_vlv/5,
50	    solve/1,
51	    solve_ord_x/3
52	]).
53:- use_module(nf_r,
54	[
55	    nf/2
56	]).
57:- use_module(store_r,
58	[
59	    add_linear_11/3,
60	    indep/2,
61	    nf_coeff_of/3
62	]).
63:- use_module('../clpqr/class',
64	[
65	    class_drop/2
66	]).
67
68do_checks(Y,Ty,St,Li,Or,Cl,No,Later) :-
69	numbers_only(Y),
70	verify_nonzero(No,Y),
71	verify_type(Ty,St,Y,Later,[]),
72	verify_lin(Or,Cl,Li,Y),
73	maplist(call,Later).
74
75numbers_only(Y) :-
76	(   var(Y)
77	;   integer(Y)
78	;   float(Y)
79	;   throw(type_error(_X = Y,2,'a real number',Y))
80	),
81	!.
82
83% verify_nonzero(Nonzero,Y)
84%
85% if Nonzero = nonzero, then verify that Y is not zero
86% (if possible, otherwise set Y to be nonzero)
87
88verify_nonzero(nonzero,Y) :-
89	(   var(Y)
90	->  (   get_attr(Y,itf,Att)
91	    ->  setarg(8,Att,nonzero)
92	    ;   put_attr(Y,itf,t(clpr,n,n,n,n,n,n,nonzero,n,n,n))
93	    )
94	;   (   Y < -1.0e-10
95	    ->	true
96	    ;	Y > 1.0e-10
97	    )
98	).
99verify_nonzero(n,_). % X is not nonzero
100
101% verify_type(type(Type),strictness(Strict),Y,[OL|OLT],OLT)
102%
103% if possible verifies whether Y satisfies the type and strictness of X
104% if not possible to verify, then returns the constraints that follow from
105% the type and strictness
106
107verify_type(type(Type),strictness(Strict),Y) -->
108	verify_type2(Y,Type,Strict).
109verify_type(n,n,_) --> [].
110
111verify_type2(Y,TypeX,StrictX) -->
112	{var(Y)},
113	!,
114	verify_type_var(TypeX,Y,StrictX).
115verify_type2(Y,TypeX,StrictX) -->
116	{verify_type_nonvar(TypeX,Y,StrictX)}.
117
118% verify_type_nonvar(Type,Nonvar,Strictness)
119%
120% verifies whether the type and strictness are satisfied with the Nonvar
121
122verify_type_nonvar(t_none,_,_).
123verify_type_nonvar(t_l(L),Value,S) :- ilb(S,L,Value).
124verify_type_nonvar(t_u(U),Value,S) :- iub(S,U,Value).
125verify_type_nonvar(t_lu(L,U),Value,S) :-
126	ilb(S,L,Value),
127	iub(S,U,Value).
128verify_type_nonvar(t_L(L),Value,S) :- ilb(S,L,Value).
129verify_type_nonvar(t_U(U),Value,S) :- iub(S,U,Value).
130verify_type_nonvar(t_Lu(L,U),Value,S) :-
131	ilb(S,L,Value),
132	iub(S,U,Value).
133verify_type_nonvar(t_lU(L,U),Value,S) :-
134	ilb(S,L,Value),
135	iub(S,U,Value).
136
137% ilb(Strict,Lower,Value) & iub(Strict,Upper,Value)
138%
139% check whether Value is satisfiable with the given lower/upper bound and
140% strictness.
141% strictness is encoded as follows:
142% 2 = strict lower bound
143% 1 = strict upper bound
144% 3 = strict lower and upper bound
145% 0 = no strict bounds
146
147ilb(S,L,V) :-
148	S /\ 2 =:= 0,
149	!,
150	L - V < 1.0e-10. % non-strict
151ilb(_,L,V) :- L - V < -1.0e-10. % strict
152
153iub(S,U,V) :-
154	S /\ 1 =:= 0,
155	!,
156	V - U < 1.0e-10. % non-strict
157iub(_,U,V) :- V - U < -1.0e-10. % strict
158
159%
160% Running some goals after X=Y simplifies the coding. It should be possible
161% to run the goals here and taking care not to put_atts/2 on X ...
162%
163
164% verify_type_var(Type,Var,Strictness,[OutList|OutListTail],OutListTail)
165%
166% returns the inequalities following from a type and strictness satisfaction
167% test with Var
168
169verify_type_var(t_none,_,_) --> [].
170verify_type_var(t_l(L),Y,S) --> llb(S,L,Y).
171verify_type_var(t_u(U),Y,S) --> lub(S,U,Y).
172verify_type_var(t_lu(L,U),Y,S) -->
173	llb(S,L,Y),
174	lub(S,U,Y).
175verify_type_var(t_L(L),Y,S) --> llb(S,L,Y).
176verify_type_var(t_U(U),Y,S) --> lub(S,U,Y).
177verify_type_var(t_Lu(L,U),Y,S) -->
178	llb(S,L,Y),
179	lub(S,U,Y).
180verify_type_var(t_lU(L,U),Y,S) -->
181	llb(S,L,Y),
182	lub(S,U,Y).
183
184% llb(Strict,Lower,Value,[OL|OLT],OLT) and lub(Strict,Upper,Value,[OL|OLT],OLT)
185%
186% returns the inequalities following from the lower and upper bounds and the
187% strictness see also lb and ub
188llb(S,L,V) -->
189	{S /\ 2 =:= 0},
190	!,
191	[clpr:{L =< V}].
192llb(_,L,V) --> [clpr:{L < V}].
193
194lub(S,U,V) -->
195	{S /\ 1 =:= 0},
196	!,
197	[clpr:{V =< U}].
198lub(_,U,V) -->	[clpr:{V < U}].
199
200%
201% We used to drop X from the class/basis to avoid trouble with subsequent
202% put_atts/2 on X. Now we could let these dead but harmless updates happen.
203% In R however, exported bindings might conflict, e.g. 0 \== 0.0
204%
205% If X is indep and we do _not_ solve for it, we are in deep shit
206% because the ordering is violated.
207%
208verify_lin(order(OrdX),class(Class),lin(LinX),Y) :-
209	!,
210	(   indep(LinX,OrdX)
211	->  detach_bounds_vlv(OrdX,LinX,Class,Y,NewLinX),
212	    % if there were bounds, they are requeued already
213	    class_drop(Class,Y),
214	    nf(-Y,NfY),
215	    deref(NfY,LinY),
216	    add_linear_11(NewLinX,LinY,Lind),
217	    (   nf_coeff_of(Lind,OrdX,_)
218	    ->	% X is element of Lind
219		solve_ord_x(Lind,OrdX,Class)
220	    ;	solve(Lind)	% X is gone, can safely solve Lind
221	    )
222	;   class_drop(Class,Y),
223	    nf(-Y,NfY),
224	    deref(NfY,LinY),
225	    add_linear_11(LinX,LinY,Lind),
226	    solve(Lind)
227	).
228verify_lin(_,_,_,_).
229