274 lines
7.2 KiB
Perl
274 lines
7.2 KiB
Perl
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||
|
|
% clp(q,r) version 1.3.3 %
|
||
|
|
% %
|
||
|
|
% (c) Copyright 1992,1993,1994,1995 %
|
||
|
|
% Austrian Research Institute for Artificial Intelligence (OFAI) %
|
||
|
|
% Schottengasse 3 %
|
||
|
|
% A-1010 Vienna, Austria %
|
||
|
|
% %
|
||
|
|
% File: itf3.pl %
|
||
|
|
% Author: Christian Holzbaur christian@ai.univie.ac.at %
|
||
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||
|
|
|
||
|
|
|
||
|
|
%
|
||
|
|
% interface to attribute encoding and hooks
|
||
|
|
%
|
||
|
|
|
||
|
|
:- use_module( library(atts)).
|
||
|
|
|
||
|
|
:- attribute class/1, order/1, lin/1, forward/1,
|
||
|
|
type/1, strictness/1, nonzero/0,
|
||
|
|
target/0, keep_indep/0, keep/0. % project.pl
|
||
|
|
|
||
|
|
/* Moved here from store.pl to break cyclic dependencies. --Mats C. */
|
||
|
|
%
|
||
|
|
% critical impact on the backsubstitution effort
|
||
|
|
% AND precision in clp(r)
|
||
|
|
%
|
||
|
|
% nf_ordering( A, B, Rel) :-
|
||
|
|
% get_atts( A, order( Oa)),
|
||
|
|
% get_atts( B, order( Ob)),
|
||
|
|
% compare( Rel, Oa, Ob).
|
||
|
|
|
||
|
|
:- multifile
|
||
|
|
user:goal_expansion/3.
|
||
|
|
|
||
|
|
:- dynamic
|
||
|
|
user:goal_expansion/3.
|
||
|
|
%
|
||
|
|
user:goal_expansion( nf_ordering(A,B,Rel), Module, Exp) :-
|
||
|
|
clpqr( Module),
|
||
|
|
Exp = (
|
||
|
|
get_atts( A, order(Oa)),
|
||
|
|
get_atts( B, order(Ob)),
|
||
|
|
compare( Rel, Oa, Ob)
|
||
|
|
).
|
||
|
|
|
||
|
|
user:goal_expansion( decompose(Lin,H,R,I), Module, Lin=[I,R|H]) :-
|
||
|
|
clpqr( Module).
|
||
|
|
|
||
|
|
clpqr( clpq).
|
||
|
|
clpqr( clpr).
|
||
|
|
/* End of code from store.pl */
|
||
|
|
|
||
|
|
%
|
||
|
|
% Parametrize the answer presentation mechanism
|
||
|
|
% (toplevel,compiler/debugger ...)
|
||
|
|
%
|
||
|
|
:- dynamic presentation_context/1.
|
||
|
|
|
||
|
|
presentation_context( Old, New) :-
|
||
|
|
clause( presentation_context(Current), _),
|
||
|
|
!,
|
||
|
|
Current = Old,
|
||
|
|
retractall( presentation_context(_)),
|
||
|
|
assert( presentation_context( New)).
|
||
|
|
presentation_context( toplevel, New) :- % default
|
||
|
|
assert( presentation_context( New)).
|
||
|
|
|
||
|
|
%
|
||
|
|
% attribute_goal( V, V:Atts) :- get_atts( V, Atts).
|
||
|
|
%
|
||
|
|
attribute_goal( V, Goal) :-
|
||
|
|
presentation_context( Cont, Cont),
|
||
|
|
dump_linear( V, Cont, Goals, Gtail),
|
||
|
|
dump_nonzero( V, Cont, Gtail, []),
|
||
|
|
l2wrapped( Goals, Goal).
|
||
|
|
|
||
|
|
l2wrapped( [], true).
|
||
|
|
l2wrapped( [X|Xs], Conj) :-
|
||
|
|
( Xs = [], wrap( X, Conj)
|
||
|
|
; Xs = [_|_], wrap( X, Xw),
|
||
|
|
Conj = (Xw,Xc),
|
||
|
|
l2wrapped( Xs, Xc)
|
||
|
|
).
|
||
|
|
|
||
|
|
%
|
||
|
|
% Tests should be pulled out of the loop ...
|
||
|
|
%
|
||
|
|
wrap( C, W) :-
|
||
|
|
prolog_flag(typein_module, Module),
|
||
|
|
this_linear_solver( Solver),
|
||
|
|
( Module == Solver ->
|
||
|
|
W = {C}
|
||
|
|
; predicate_property( Module:{_}, imported_from(Solver)) ->
|
||
|
|
W = {C}
|
||
|
|
;
|
||
|
|
W = Solver:{C}
|
||
|
|
).
|
||
|
|
|
||
|
|
dump_linear( V, Context) -->
|
||
|
|
{
|
||
|
|
get_atts( V, [lin(Lin),type(Type)]),
|
||
|
|
!,
|
||
|
|
decompose( Lin, H, _, I)
|
||
|
|
},
|
||
|
|
%
|
||
|
|
% This happens if not all target variables can be made independend
|
||
|
|
% Example: examples/option.pl:
|
||
|
|
% | ?- go2(S,W).
|
||
|
|
%
|
||
|
|
% W = 21/4,
|
||
|
|
% S>=0,
|
||
|
|
% S<50 ? ;
|
||
|
|
%
|
||
|
|
% W>5,
|
||
|
|
% S=221/4-W, this line would be missing !!!
|
||
|
|
% W=<21/4
|
||
|
|
%
|
||
|
|
( { Type=t_none ; get_atts( V, -target) } -> [] ; dump_v( Context, t_none, V, I, H) ),
|
||
|
|
%
|
||
|
|
( {Type=t_none, get_atts( V, -target) } -> % nonzero produces such
|
||
|
|
[]
|
||
|
|
;
|
||
|
|
dump_v( Context, Type, V, I, H)
|
||
|
|
).
|
||
|
|
dump_linear( _, _) --> [].
|
||
|
|
|
||
|
|
dump_v( toplevel, Type, V, I, H) --> dump_var( Type, V, I, H).
|
||
|
|
dump_v( compiler, Type, V, I, H) --> compiler_dump_var( Type, V, I, H).
|
||
|
|
|
||
|
|
dump_nonzero( V, Cont) -->
|
||
|
|
{
|
||
|
|
get_atts( V, [nonzero,lin(Lin)]),
|
||
|
|
!,
|
||
|
|
decompose( Lin, H, _, I)
|
||
|
|
},
|
||
|
|
dump_nz( Cont, V, H, I).
|
||
|
|
dump_nonzero( _, _) --> [].
|
||
|
|
|
||
|
|
dump_nz( toplevel, V, H, I) --> dump_nz( V, H, I).
|
||
|
|
dump_nz( compiler, V, H, I) --> compiler_dump_nz( V, H, I).
|
||
|
|
|
||
|
|
numbers_only( Y, _) :- var(Y), !.
|
||
|
|
numbers_only( Y, _) :- arith_normalize( Y, Y), !.
|
||
|
|
numbers_only( Y, X) :-
|
||
|
|
this_linear_solver( Solver),
|
||
|
|
( Solver==clpr ->
|
||
|
|
What = 'a real number'
|
||
|
|
; Solver==clpq ->
|
||
|
|
What = 'a rational number'
|
||
|
|
),
|
||
|
|
raise_exception( type_error(X=Y,2,What,Y)).
|
||
|
|
|
||
|
|
verify_attributes( X, _, []) :-
|
||
|
|
get_atts(X, [-class(_),-order(_),-lin(_),-forward(_),-type(_),-strictness(_),
|
||
|
|
-nonzero]),
|
||
|
|
!.
|
||
|
|
verify_attributes( X, Y, []) :-
|
||
|
|
get_atts( X, forward(F)),
|
||
|
|
!,
|
||
|
|
fwd_deref( F, Y).
|
||
|
|
verify_attributes( X, Y, Later) :-
|
||
|
|
numbers_only( Y, X),
|
||
|
|
put_atts( X, forward(Y)),
|
||
|
|
verify_nonzero( X, Y),
|
||
|
|
verify_type( X, Y, Later, []),
|
||
|
|
verify_lin( X, Y).
|
||
|
|
|
||
|
|
fwd_deref( X, Y) :- nonvar(X), X=Y.
|
||
|
|
fwd_deref( X, Y) :- var(X),
|
||
|
|
( get_atts( X, forward(F)) ->
|
||
|
|
fwd_deref( F, Y)
|
||
|
|
;
|
||
|
|
X = Y
|
||
|
|
).
|
||
|
|
|
||
|
|
verify_nonzero( X, Y) :-
|
||
|
|
get_atts( X, nonzero),
|
||
|
|
!,
|
||
|
|
( var(Y) ->
|
||
|
|
put_atts( Y, nonzero)
|
||
|
|
;
|
||
|
|
arith_eval( Y =\= 0)
|
||
|
|
).
|
||
|
|
verify_nonzero( _, _).
|
||
|
|
|
||
|
|
verify_type( X, Y) -->
|
||
|
|
{
|
||
|
|
get_atts( X, [type(Type),strictness(Strict)])
|
||
|
|
},
|
||
|
|
!,
|
||
|
|
verify_type( Y, Type, Strict).
|
||
|
|
verify_type( _, _) --> [].
|
||
|
|
|
||
|
|
verify_type( Y, TypeX, StrictX) --> {var(Y)}, !,
|
||
|
|
verify_type_var( TypeX, Y, StrictX).
|
||
|
|
verify_type( Y, TypeX, StrictX) -->
|
||
|
|
{
|
||
|
|
verify_type_nonvar( TypeX, Y, StrictX)
|
||
|
|
}.
|
||
|
|
|
||
|
|
verify_type_nonvar( t_none, _, _).
|
||
|
|
verify_type_nonvar( t_l(L), Value, S) :- lb( S, L, Value).
|
||
|
|
verify_type_nonvar( t_u(U), Value, S) :- ub( S, U, Value).
|
||
|
|
verify_type_nonvar( t_lu(L,U), Value, S) :- lb( S, L, Value), ub( S, U, Value).
|
||
|
|
verify_type_nonvar( t_L(L), Value, S) :- lb( S, L, Value).
|
||
|
|
verify_type_nonvar( t_U(U), Value, S) :- ub( S, U, Value).
|
||
|
|
verify_type_nonvar( t_Lu(L,U), Value, S) :- lb( S, L, Value), ub( S, U, Value).
|
||
|
|
verify_type_nonvar( t_lU(L,U), Value, S) :- lb( S, L, Value), ub( S, U, Value).
|
||
|
|
|
||
|
|
lb( S, L, V) :- S /\ 2'10 =:= 0, !, arith_eval( L =< V).
|
||
|
|
lb( _, L, V) :- arith_eval( L < V).
|
||
|
|
|
||
|
|
ub( S, U, V) :- S /\ 2'01 =:= 0, !, arith_eval( V =< U).
|
||
|
|
ub( _, U, V) :- arith_eval( V < U).
|
||
|
|
|
||
|
|
|
||
|
|
%
|
||
|
|
% Running some goals after X=Y simplifies the coding. It should be possible
|
||
|
|
% to run the goals here and taking care not to put_atts/2 on X ...
|
||
|
|
%
|
||
|
|
verify_type_var( t_none, _, _) --> [].
|
||
|
|
verify_type_var( t_l(L), Y, S) --> llb( S, L, Y).
|
||
|
|
verify_type_var( t_u(U), Y, S) --> lub( S, U, Y).
|
||
|
|
verify_type_var( t_lu(L,U), Y, S) --> llb( S, L, Y), lub( S, U, Y).
|
||
|
|
verify_type_var( t_L(L), Y, S) --> llb( S, L, Y).
|
||
|
|
verify_type_var( t_U(U), Y, S) --> lub( S, U, Y).
|
||
|
|
verify_type_var( t_Lu(L,U), Y, S) --> llb( S, L, Y), lub( S, U, Y).
|
||
|
|
verify_type_var( t_lU(L,U), Y, S) --> llb( S, L, Y), lub( S, U, Y).
|
||
|
|
|
||
|
|
llb( S, L, V) --> {S /\ 2'10 =:= 0}, !, [ {L =< V} ].
|
||
|
|
llb( _, L, V) --> [ {L < V} ].
|
||
|
|
|
||
|
|
lub( S, U, V) --> {S /\ 2'01 =:= 0}, !, [ {V =< U} ].
|
||
|
|
lub( _, U, V) --> [ {V < U} ].
|
||
|
|
|
||
|
|
|
||
|
|
%
|
||
|
|
% We used to drop X from the class/basis to avoid trouble with subsequent
|
||
|
|
% put_atts/2 on X. Now we could let these dead but harmless updates happen.
|
||
|
|
% In R however, exported bindings might conflict, e.g. 0 \== 0.0
|
||
|
|
%
|
||
|
|
% If X is indep and we do _not_ solve for it, we are in deep shit
|
||
|
|
% because the ordering is violated.
|
||
|
|
%
|
||
|
|
verify_lin( X, Y) :-
|
||
|
|
get_atts( X, [class(Class),lin(LinX)]),
|
||
|
|
!,
|
||
|
|
( indep( LinX, X) ->
|
||
|
|
detach_bounds( X), % if there were bounds, they are requeued already
|
||
|
|
class_drop( Class, X),
|
||
|
|
nf( X-Y, Lin),
|
||
|
|
deref( Lin, Lind),
|
||
|
|
( nf_coeff_of( Lind, X, _) ->
|
||
|
|
solve_x( Lind, X)
|
||
|
|
;
|
||
|
|
solve( Lind)
|
||
|
|
)
|
||
|
|
;
|
||
|
|
class_drop( Class, X),
|
||
|
|
nf( X-Y, Lin),
|
||
|
|
deref( Lin, Lind),
|
||
|
|
solve( Lind)
|
||
|
|
).
|
||
|
|
verify_lin( _, _).
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
|