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