diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

clpqr is now a separate package.

Browse Source
This commit is contained in:
Vitor Santos Costa 2009-04-24 10:01:27 -05:00
parent 13f66957b6
commit ad617951ec
29 changed files with 3 additions and 13253 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
GPL/clpqr/ChangeLog
View File

@ -1,34 +0,0 @@
Sep 10, 2006
* JW: Removed dependency on C/3.
Mar 31, 2006
* JW: Removed SICStus ugraphs.pl and replaced by new SWI-Prolog library
Oct 17, 2005
* LDK: Changed floor and ceiling operators to cope with
inaccurate floats.
Feb 25, 2005
* TS: Fix for Bugzilla Bug 19 by Leslie De Koninck.
Feb 21, 2005
* JW: Fixed various module imports and expanded SWI-Prolog
library(ordsets) to support all of the clp(R) library.
Dec 16, 2004
* JW: Make loading parts silent
* TS: Fixed bug toplevel printing. Now only pass different
variables to dump/3.
Dec 15, 2004
* JW: Added version to CVS, updated copyright notices, etc.
* TS: Added automatic printing of constraints on variables
in toplevel query.

106
GPL/clpqr/Makefile.in
View File

@ -1,106 +0,0 @@
#
# default base directory for YAP installation
# (EROOT for architecture-dependent files)
#
prefix = @prefix@
ROOTDIR = $(prefix)
EROOTDIR = @exec_prefix@
SHELL=@SHELL@
PLBASE=@PLBASE@
PLARCH=@PLARCH@
PL=@PL@
XPCEBASE=$(PLBASE)/xpce
PKGDOC=$(PLBASE)/doc/packages
PCEHOME=../../xpce
LIBDIR=$(PLBASE)/library
SHAREDIR=$(ROOTDIR)/share/Yap
CLPRDIR=$(SHAREDIR)/clpr
CLPQDIR=$(SHAREDIR)/clpq
CLPQRDIR=$(SHAREDIR)/clpqr
EXDIR=$(PKGDOC)/examples/clpr
DESTDIR=
srcdir=@srcdir@
CLPQSOURCEDIR=$(srcdir)/clpq
CLPRSOURCEDIR=$(srcdir)/clpr
CLPQRSOURCEDIR=$(srcdir)/clpqr
INSTALL=@INSTALL@
INSTALL_PROGRAM=@INSTALL_PROGRAM@
INSTALL_DATA=@INSTALL_DATA@
CLPRPRIV= \
$(CLPRSOURCEDIR)/bb_r.pl \
$(CLPRSOURCEDIR)/bv_r.pl \
$(CLPRSOURCEDIR)/fourmotz_r.pl \
$(CLPRSOURCEDIR)/ineq_r.pl \
$(CLPRSOURCEDIR)/itf_r.pl \
$(CLPRSOURCEDIR)/nf_r.pl \
$(CLPRSOURCEDIR)/store_r.pl
CLPQPRIV= \
$(CLPQSOURCEDIR)/bb_q.pl \
$(CLPQSOURCEDIR)/bv_q.pl \
$(CLPQSOURCEDIR)/fourmotz_q.pl \
$(CLPQSOURCEDIR)/ineq_q.pl \
$(CLPQSOURCEDIR)/itf_q.pl \
$(CLPQSOURCEDIR)/nf_q.pl \
$(CLPQSOURCEDIR)/store_q.pl
CLPQRPRIV= \
$(CLPQRSOURCEDIR)/class.pl \
$(CLPQRSOURCEDIR)/dump.pl \
$(CLPQRSOURCEDIR)/geler.pl \
$(CLPQRSOURCEDIR)/itf.pl \
$(CLPQRSOURCEDIR)/ordering.pl \
$(CLPQRSOURCEDIR)/project.pl \
$(CLPQRSOURCEDIR)/redund.pl
LIBPL= \
$(srcdir)/clpr.pl \
$(srcdir)/clpq.pl
EXAMPLES=
all::
@echo "Nothing to be done for this package"
install: $(LIBPL) $(CLPQRPRIV) $(CLPRPRIV) $(CLPQPRIV)
mkdir -p $(DESTDIR)$(CLPQRDIR)
mkdir -p $(DESTDIR)$(CLPRDIR)
mkdir -p $(DESTDIR)$(CLPQDIR)
$(INSTALL_DATA) $(LIBPL) $(DESTDIR)$(SHAREDIR)
$(INSTALL_DATA) $(CLPQRPRIV) $(DESTDIR)$(CLPQRDIR)
$(INSTALL_DATA) $(CLPRPRIV) $(DESTDIR)$(CLPRDIR)
$(INSTALL_DATA) $(CLPQPRIV) $(DESTDIR)$(CLPQDIR)
$(INSTALL_DATA) $(srcdir)/README $(DESTDIR)$(CLPQRDIR)
rpm-install: install
pdf-install: install-examples
html-install: install-examples
install-examples::
# mkdir -p $(DESTDIR)$(EXDIR)
# (cd Examples && $(INSTALL_DATA) $(EXAMPLES) $(DESTDIR)$(EXDIR))
uninstall:
(cd $(CLPDIR) && rm -f $(LIBPL))
rm -rf $(CLPQRDIR)
check::
# $(PL) -q -f clpr_test.pl -g test,halt -t 'halt(1)'
################################################################
# Clean
################################################################
clean:
rm -f *~ *% config.log
distclean: clean
rm -f config.h config.cache config.status Makefile
rm -rf autom4te.cache

19
GPL/clpqr/README
View File

@ -1,19 +0,0 @@
SWI-Prolog CLP(Q,R)
-------------------
Author: Leslie De Koninck, K.U.Leuven
This software is based on the CLP(Q,R) implementation by Christian
Holzbauer and released with permission from all above mentioned authors
and Christian Holzbauer under the standard SWI-Prolog license schema:
GPL-2 + statement to allow linking with proprietary software.
The sources of this package are maintained in packages/clpr in the
SWI-Prolog source distribution. The documentation source is in
man/lib/clpr.doc as part of the overall SWI-Prolog documentation.
Full documentation on CLP(Q,R) can be found at
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09

135
GPL/clpqr/clpq.pl
View File

@ -1,135 +0,0 @@
/*
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(clpq,
[
{}/1,
maximize/1,
minimize/1,
inf/2, inf/4, sup/2, sup/4,
bb_inf/3,
bb_inf/4,
ordering/1,
entailed/1,
clp_type/2,
dump/3%, projecting_assert/1
]).
:- expects_dialect(swi).
%
% Don't report export of private predicates from clpq
%
:- multifile
user:portray_message/2.
:- dynamic
user:portray_message/2.
%
user:portray_message(warning,import(_,_,clpq,private)).
:- load_files(
[
'clpq/bb_q',
'clpq/bv_q',
'clpq/fourmotz_q',
'clpq/ineq_q',
'clpq/itf_q',
'clpq/nf_q',
'clpq/store_q',
'clpqr/class',
'clpqr/dump',
'clpqr/geler',
'clpqr/itf',
'clpqr/ordering',
'clpqr/project',
'clpqr/redund',
library(ugraphs)
],
[
if(not_loaded),
silent(true)
]).
/*******************************
* TOPLEVEL PRINTING *
*******************************/
:- multifile
prolog:message/3.
% prolog:message(query(YesNo)) --> !,
% ['~@'-[chr:print_all_stores]],
% '$messages':prolog_message(query(YesNo)).
prolog:message(query(YesNo,Bindings)) --> !,
{dump_toplevel_bindings(Bindings,Constraints)},
{dump_format(Constraints,Format)},
Format,
'$messages':prolog_message(query(YesNo,Bindings)).
dump_toplevel_bindings(Bindings,Constraints) :-
dump_vars_names(Bindings,[],Vars,Names),
dump(Vars,Names,Constraints).
dump_vars_names([],_,[],[]).
dump_vars_names([Name=Term|Rest],Seen,Vars,Names) :-
( var(Term),
( get_attr(Term,itf,_)
; get_attr(Term,geler,_)
),
\+ memberchk_eq(Term,Seen)
-> Vars = [Term|RVars],
Names = [Name|RNames],
NSeen = [Term|Seen]
; Vars = RVars,
Names = RNames,
Seen = NSeen
),
dump_vars_names(Rest,NSeen,RVars,RNames).
dump_format([],[]).
dump_format([X|Xs],['{~w}'-[X],nl|Rest]) :-
dump_format(Xs,Rest).
memberchk_eq(X,[Y|Ys]) :-
( X == Y
-> true
; memberchk_eq(X,Ys)
).

240
GPL/clpqr/clpq/bb_q.pl
View File

@ -1,240 +0,0 @@
/* $Id: bb_q.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(bb_q,
[
bb_inf/3,
bb_inf/4,
vertex_value/2
]).
:- use_module(bv_q,
[
deref/2,
deref_var/2,
determine_active_dec/1,
inf/2,
iterate_dec/2,
sup/2,
var_with_def_assign/2
]).
:- use_module(nf_q,
[
{}/1,
entailed/1,
nf/2,
nf_constant/2,
repair/2,
wait_linear/3
]).
% bb_inf(Ints,Term,Inf)
%
% Finds the infimum of Term where the variables Ints are to be integers.
% The infimum is stored in Inf.
bb_inf(Is,Term,Inf) :-
bb_inf(Is,Term,Inf,_).
bb_inf(Is,Term,Inf,Vertex) :-
wait_linear(Term,Nf,bb_inf_internal(Is,Nf,Inf,Vertex)).
% ---------------------------------------------------------------------
% bb_inf_internal(Is,Lin,Inf,Vertex)
%
% Finds an infimum <Inf> for linear expression in normal form <Lin>, where
% all variables in <Is> are to be integers.
bb_inf_internal(Is,Lin,_,_) :-
bb_intern(Is,IsNf),
nb_delete(prov_opt),
repair(Lin,LinR), % bb_narrow ...
deref(LinR,Lind),
var_with_def_assign(Dep,Lind),
determine_active_dec(Lind),
bb_loop(Dep,IsNf),
fail.
bb_inf_internal(_,_,Inf,Vertex) :-
catch(nb_getval(prov_opt,InfVal-Vertex),_,fail),
{Inf =:= InfVal},
nb_delete(prov_opt).
% bb_loop(Opt,Is)
%
% Minimizes the value of Opt where variables Is have to be integer values.
bb_loop(Opt,Is) :-
bb_reoptimize(Opt,Inf),
bb_better_bound(Inf),
vertex_value(Is,Ivs),
( bb_first_nonint(Is,Ivs,Viol,Floor,Ceiling)
-> bb_branch(Viol,Floor,Ceiling),
bb_loop(Opt,Is)
; nb_setval(prov_opt,Inf-Ivs) % new provisional optimum
).
% bb_reoptimize(Obj,Inf)
%
% Minimizes the value of Obj and puts the result in Inf.
% This new minimization is necessary as making a bound integer may yield a
% different optimum. The added inequalities may also have led to binding.
bb_reoptimize(Obj,Inf) :-
var(Obj),
iterate_dec(Obj,Inf).
bb_reoptimize(Obj,Inf) :-
nonvar(Obj),
Inf = Obj.
% bb_better_bound(Inf)
%
% Checks if the new infimum Inf is better than the previous one (if such exists).
bb_better_bound(Inf) :-
catch((nb_getval(prov_opt,Inc-_),Inf < Inc),_,true).
% bb_branch(V,U,L)
%
% Stores that V =< U or V >= L, can be used for different strategies within
% bb_loop/3.
bb_branch(V,U,_) :- {V =< U}.
bb_branch(V,_,L) :- {V >= L}.
% vertex_value(Vars,Values)
%
% Returns in <Values> the current values of the variables in <Vars>.
vertex_value([],[]).
vertex_value([X|Xs],[V|Vs]) :-
rhs_value(X,V),
vertex_value(Xs,Vs).
% rhs_value(X,Value)
%
% Returns in <Value> the current value of variable <X>.
rhs_value(Xn,Value) :-
( nonvar(Xn)
-> Value = Xn
; var(Xn)
-> deref_var(Xn,Xd),
Xd = [I,R|_],
Value is R+I
).
% bb_first_nonint(Ints,Rhss,Eps,Viol,Floor,Ceiling)
%
% Finds the first variable in Ints which doesn't have an active integer bound.
% Rhss contain the Rhs (R + I) values corresponding to the variables.
% The first variable that hasn't got an active integer bound, is returned in
% Viol. The floor and ceiling of its actual bound is returned in Floor and Ceiling.
bb_first_nonint([I|Is],[Rhs|Rhss],Viol,F,C) :-
( integer(Rhs)
-> bb_first_nonint(Is,Rhss,Viol,F,C)
; Viol = I,
F is floor(Rhs),
C is ceiling(Rhs)
).
% bb_intern([X|Xs],[Xi|Xis])
%
% Turns the elements of the first list into integers into the second
% list via bb_intern/3.
bb_intern([],[]).
bb_intern([X|Xs],[Xi|Xis]) :-
nf(X,Xnf),
bb_intern(Xnf,Xi,X),
bb_intern(Xs,Xis).
% bb_intern(Nf,X,Term)
%
% Makes sure that Term which is normalized into Nf, is integer.
% X contains the possibly changed Term. If Term is a variable,
% then its bounds are hightened or lowered to the next integer.
% Otherwise, it is checked it Term is integer.
bb_intern([],X,_) :-
!,
X = 0.
bb_intern([v(I,[])],X,_) :-
!,
integer(I),
X = I.
bb_intern([v(1,[V^1])],X,_) :-
!,
V = X,
bb_narrow_lower(X),
bb_narrow_upper(X).
bb_intern(_,_,Term) :-
throw(instantiation_error(bb_inf(Term,_),1)).
% bb_narrow_lower(X)
%
% Narrows the lower bound so that it is an integer bound.
% We do this by finding the infimum of X and asserting that X
% is larger than the first integer larger or equal to the infimum
% (second integer if X is to be strict larger than the first integer).
bb_narrow_lower(X) :-
( inf(X,Inf)
-> Bound is ceiling(Inf),
( entailed(X > Bound)
-> {X >= Bound+1}
; {X >= Bound}
)
; true
).
% bb_narrow_upper(X)
%
% See bb_narrow_lower/1. This predicate handles the upper bound.
bb_narrow_upper(X) :-
( sup(X,Sup)
-> Bound is floor(Sup),
( entailed(X < Bound)
-> {X =< Bound-1}
; {X =< Bound}
)
; true
).

1760
GPL/clpqr/clpq/bv_q.pl
View File

File diff suppressed because it is too large Load Diff

503
GPL/clpqr/clpq/fourmotz_q.pl
View File

@ -1,503 +0,0 @@
/* $Id: fourmotz_q.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(fourmotz_q,
[
fm_elim/3
]).
:- use_module(bv_q,
[
allvars/2,
basis_add/2,
detach_bounds/1,
pivot/5,
var_with_def_intern/4
]).
:- use_module('../clpqr/class',
[
class_allvars/2
]).
:- use_module('../clpqr/project',
[
drop_dep/1,
drop_dep_one/1,
make_target_indep/2
]).
:- use_module('../clpqr/redund',
[
redundancy_vars/1
]).
:- use_module(store_q,
[
add_linear_11/3,
add_linear_f1/4,
indep/2,
nf_coeff_of/3,
normalize_scalar/2
]).
fm_elim(Vs,Target,Pivots) :-
prefilter(Vs,Vsf),
fm_elim_int(Vsf,Target,Pivots).
% prefilter(Vars,Res)
%
% filters out target variables and variables that do not occur in bounded linear equations.
% Stores that the variables in Res are to be kept independent.
prefilter([],[]).
prefilter([V|Vs],Res) :-
( get_attr(V,itf,Att),
arg(9,Att,n),
occurs(V)
-> % V is a nontarget variable that occurs in a bounded linear equation
Res = [V|Tail],
setarg(10,Att,keep_indep),
prefilter(Vs,Tail)
; prefilter(Vs,Res)
).
%
% the target variables are marked with an attribute, and we get a list
% of them as an argument too
%
fm_elim_int([],_,Pivots) :- % done
unkeep(Pivots).
fm_elim_int(Vs,Target,Pivots) :-
Vs = [_|_],
( best(Vs,Best,Rest)
-> occurences(Best,Occ),
elim_min(Best,Occ,Target,Pivots,NewPivots)
; % give up
NewPivots = Pivots,
Rest = []
),
fm_elim_int(Rest,Target,NewPivots).
% best(Vs,Best,Rest)
%
% Finds the variable with the best result (lowest Delta) in fm_cp_filter
% and returns the other variables in Rest.
best(Vs,Best,Rest) :-
findall(Delta-N,fm_cp_filter(Vs,Delta,N),Deltas),
keysort(Deltas,[_-N|_]),
select_nth(Vs,N,Best,Rest).
% fm_cp_filter(Vs,Delta,N)
%
% For an indepenent variable V in Vs, which is the N'th element in Vs,
% find how many inequalities are generated when this variable is eliminated.
% Note that target variables and variables that only occur in unbounded equations
% should have been removed from Vs via prefilter/2
fm_cp_filter(Vs,Delta,N) :-
length(Vs,Len), % Len = number of variables in Vs
mem(Vs,X,Vst), % Selects a variable X in Vs, Vst is the list of elements after X in Vs
get_attr(X,itf,Att),
arg(4,Att,lin(Lin)),
arg(5,Att,order(OrdX)),
arg(9,Att,n), % no target variable
indep(Lin,OrdX), % X is an independent variable
occurences(X,Occ),
Occ = [_|_],
cp_card(Occ,0,Lnew),
length(Occ,Locc),
Delta is Lnew-Locc,
length(Vst,Vstl),
N is Len-Vstl. % X is the Nth element in Vs
% mem(Xs,X,XsT)
%
% If X is a member of Xs, XsT is the list of elements after X in Xs.
mem([X|Xs],X,Xs).
mem([_|Ys],X,Xs) :- mem(Ys,X,Xs).
% select_nth(List,N,Nth,Others)
%
% Selects the N th element of List, stores it in Nth and returns the rest of the list in Others.
select_nth(List,N,Nth,Others) :-
select_nth(List,1,N,Nth,Others).
select_nth([X|Xs],N,N,X,Xs) :- !.
select_nth([Y|Ys],M,N,X,[Y|Xs]) :-
M1 is M+1,
select_nth(Ys,M1,N,X,Xs).
%
% fm_detach + reverse_pivot introduce indep t_none, which
% invalidates the invariants
%
elim_min(V,Occ,Target,Pivots,NewPivots) :-
crossproduct(Occ,New,[]),
activate_crossproduct(New),
reverse_pivot(Pivots),
fm_detach(Occ),
allvars(V,All),
redundancy_vars(All), % only for New \== []
make_target_indep(Target,NewPivots),
drop_dep(All).
%
% restore NF by reverse pivoting
%
reverse_pivot([]).
reverse_pivot([I:D|Ps]) :-
get_attr(D,itf,AttD),
arg(2,AttD,type(Dt)),
setarg(11,AttD,n), % no longer
get_attr(I,itf,AttI),
arg(2,AttI,type(It)),
arg(5,AttI,order(OrdI)),
arg(6,AttI,class(ClI)),
pivot(D,ClI,OrdI,Dt,It),
reverse_pivot(Ps).
% unkeep(Pivots)
%
%
unkeep([]).
unkeep([_:D|Ps]) :-
get_attr(D,itf,Att),
setarg(11,Att,n),
drop_dep_one(D),
unkeep(Ps).
%
% All we drop are bounds
%
fm_detach( []).
fm_detach([V:_|Vs]) :-
detach_bounds(V),
fm_detach(Vs).
% activate_crossproduct(Lst)
%
% For each inequality Lin =< 0 (or Lin < 0) in Lst, a new variable is created:
% Var = Lin and Var =< 0 (or Var < 0). Var is added to the basis.
activate_crossproduct([]).
activate_crossproduct([lez(Strict,Lin)|News]) :-
var_with_def_intern(t_u(0),Var,Lin,Strict),
% Var belongs to same class as elements in Lin
basis_add(Var,_),
activate_crossproduct(News).
% ------------------------------------------------------------------------------
% crossproduct(Lst,Res,ResTail)
%
% See crossproduct/4
% This predicate each time puts the next element of Lst as First in crossproduct/4
% and lets the rest be Next.
crossproduct([]) --> [].
crossproduct([A|As]) -->
crossproduct(As,A),
crossproduct(As).
% crossproduct(Next,First,Res,ResTail)
%
% Eliminates a variable in linear equations First + Next and stores the generated
% inequalities in Res.
% Let's say A:K1 = First and B:K2 = first equation in Next.
% A = ... + K1*V + ...
% B = ... + K2*V + ...
% Let K = -K2/K1
% then K*A + B = ... + 0*V + ...
% from the bounds of A and B, via cross_lower/7 and cross_upper/7, new inequalities
% are generated. Then the same is done for B:K2 = next element in Next.
crossproduct([],_) --> [].
crossproduct([B:Kb|Bs],A:Ka) -->
{
get_attr(A,itf,AttA),
arg(2,AttA,type(Ta)),
arg(3,AttA,strictness(Sa)),
arg(4,AttA,lin(LinA)),
get_attr(B,itf,AttB),
arg(2,AttB,type(Tb)),
arg(3,AttB,strictness(Sb)),
arg(4,AttB,lin(LinB)),
K is -Kb rdiv Ka,
add_linear_f1(LinA,K,LinB,Lin) % Lin doesn't contain the target variable anymore
},
( { K > 0 } % K > 0: signs were opposite
-> { Strict is Sa \/ Sb },
cross_lower(Ta,Tb,K,Lin,Strict),
cross_upper(Ta,Tb,K,Lin,Strict)
; % La =< A =< Ua -> -Ua =< -A =< -La
{
flip(Ta,Taf),
flip_strict(Sa,Saf),
Strict is Saf \/ Sb
},
cross_lower(Taf,Tb,K,Lin,Strict),
cross_upper(Taf,Tb,K,Lin,Strict)
),
crossproduct(Bs,A:Ka).
% cross_lower(Ta,Tb,K,Lin,Strict,Res,ResTail)
%
% Generates a constraint following from the bounds of A and B.
% When A = LinA and B = LinB then Lin = K*LinA + LinB. Ta is the type
% of A and Tb is the type of B. Strict is the union of the strictness
% of A and B. If K is negative, then Ta should have been flipped (flip/2).
% The idea is that if La =< A =< Ua and Lb =< B =< Ub (=< can also be <)
% then if K is positive, K*La + Lb =< K*A + B =< K*Ua + Ub.
% if K is negative, K*Ua + Lb =< K*A + B =< K*La + Ub.
% This predicate handles the first inequality and adds it to Res in the form
% lez(Sl,Lhs) meaning K*La + Lb - (K*A + B) =< 0 or K*Ua + Lb - (K*A + B) =< 0
% with Sl being the strictness and Lhs the lefthandside of the equation.
% See also cross_upper/7
cross_lower(Ta,Tb,K,Lin,Strict) -->
{
lower(Ta,La),
lower(Tb,Lb),
!,
L is K*La+Lb,
normalize_scalar(L,Ln),
add_linear_f1(Lin,-1,Ln,Lhs),
Sl is Strict >> 1 % normalize to upper bound
},
[ lez(Sl,Lhs) ].
cross_lower(_,_,_,_,_) --> [].
% cross_upper(Ta,Tb,K,Lin,Strict,Res,ResTail)
%
% See cross_lower/7
% This predicate handles the second inequality:
% -(K*Ua + Ub) + K*A + B =< 0 or -(K*La + Ub) + K*A + B =< 0
cross_upper(Ta,Tb,K,Lin,Strict) -->
{
upper(Ta,Ua),
upper(Tb,Ub),
!,
U is -(K*Ua+Ub),
normalize_scalar(U,Un),
add_linear_11(Un,Lin,Lhs),
Su is Strict /\ 1 % normalize to upper bound
},
[ lez(Su,Lhs) ].
cross_upper(_,_,_,_,_) --> [].
% lower(Type,Lowerbound)
%
% Returns the lowerbound of type Type if it has one.
% E.g. if type = t_l(L) then Lowerbound is L,
% if type = t_lU(L,U) then Lowerbound is L,
% if type = t_u(U) then fails
lower(t_l(L),L).
lower(t_lu(L,_),L).
lower(t_L(L),L).
lower(t_Lu(L,_),L).
lower(t_lU(L,_),L).
% upper(Type,Upperbound)
%
% Returns the upperbound of type Type if it has one.
% See lower/2
upper(t_u(U),U).
upper(t_lu(_,U),U).
upper(t_U(U),U).
upper(t_Lu(_,U),U).
upper(t_lU(_,U),U).
% flip(Type,FlippedType)
%
% Flips the lower and upperbound, so the old lowerbound becomes the new upperbound and
% vice versa.
flip(t_l(X),t_u(X)).
flip(t_u(X),t_l(X)).
flip(t_lu(X,Y),t_lu(Y,X)).
flip(t_L(X),t_u(X)).
flip(t_U(X),t_l(X)).
flip(t_lU(X,Y),t_lu(Y,X)).
flip(t_Lu(X,Y),t_lu(Y,X)).
% flip_strict(Strict,FlippedStrict)
%
% Does what flip/2 does, but for the strictness.
flip_strict(0,0).
flip_strict(1,2).
flip_strict(2,1).
flip_strict(3,3).
% cp_card(Lst,CountIn,CountOut)
%
% Counts the number of bounds that may generate an inequality in
% crossproduct/3
cp_card([],Ci,Ci).
cp_card([A|As],Ci,Co) :-
cp_card(As,A,Ci,Cii),
cp_card(As,Cii,Co).
% cp_card(Next,First,CountIn,CountOut)
%
% Counts the number of bounds that may generate an inequality in
% crossproduct/4.
cp_card([],_,Ci,Ci).
cp_card([B:Kb|Bs],A:Ka,Ci,Co) :-
get_attr(A,itf,AttA),
arg(2,AttA,type(Ta)),
get_attr(B,itf,AttB),
arg(2,AttB,type(Tb)),
( sign(Ka) =\= sign(Kb)
-> cp_card_lower(Ta,Tb,Ci,Cii),
cp_card_upper(Ta,Tb,Cii,Ciii)
; flip(Ta,Taf),
cp_card_lower(Taf,Tb,Ci,Cii),
cp_card_upper(Taf,Tb,Cii,Ciii)
),
cp_card(Bs,A:Ka,Ciii,Co).
% cp_card_lower(TypeA,TypeB,SIn,SOut)
%
% SOut = SIn + 1 if both TypeA and TypeB have a lowerbound.
cp_card_lower(Ta,Tb,Si,So) :-
lower(Ta,_),
lower(Tb,_),
!,
So is Si+1.
cp_card_lower(_,_,Si,Si).
% cp_card_upper(TypeA,TypeB,SIn,SOut)
%
% SOut = SIn + 1 if both TypeA and TypeB have an upperbound.
cp_card_upper(Ta,Tb,Si,So) :-
upper(Ta,_),
upper(Tb,_),
!,
So is Si+1.
cp_card_upper(_,_,Si,Si).
% ------------------------------------------------------------------------------
% occurences(V,Occ)
%
% Returns in Occ the occurrences of variable V in the linear equations of dependent variables
% with bound =\= t_none in the form of D:K where D is a dependent variable and K is the scalar
% of V in the linear equation of D.
occurences(V,Occ) :-
get_attr(V,itf,Att),
arg(5,Att,order(OrdV)),
arg(6,Att,class(C)),
class_allvars(C,All),
occurences(All,OrdV,Occ).
% occurences(De,OrdV,Occ)
%
% Returns in Occ the occurrences of variable V with order OrdV in the linear equations of
% dependent variables De with bound =\= t_none in the form of D:K where D is a dependent
% variable and K is the scalar of V in the linear equation of D.
occurences(De,_,[]) :-
var(De),
!.
occurences([D|De],OrdV,Occ) :-
( get_attr(D,itf,Att),
arg(2,Att,type(Type)),
arg(4,Att,lin(Lin)),
occ_type_filter(Type),
nf_coeff_of(Lin,OrdV,K)
-> Occ = [D:K|Occt],
occurences(De,OrdV,Occt)
; occurences(De,OrdV,Occ)
).
% occ_type_filter(Type)
%
% Succeeds when Type is any other type than t_none. Is used in occurences/3 and occurs/2
occ_type_filter(t_l(_)).
occ_type_filter(t_u(_)).
occ_type_filter(t_lu(_,_)).
occ_type_filter(t_L(_)).
occ_type_filter(t_U(_)).
occ_type_filter(t_lU(_,_)).
occ_type_filter(t_Lu(_,_)).
% occurs(V)
%
% Checks whether variable V occurs in a linear equation of a dependent variable with a bound
% =\= t_none.
occurs(V) :-
get_attr(V,itf,Att),
arg(5,Att,order(OrdV)),
arg(6,Att,class(C)),
class_allvars(C,All),
occurs(All,OrdV).
% occurs(De,OrdV)
%
% Checks whether variable V with order OrdV occurs in a linear equation of any dependent variable
% in De with a bound =\= t_none.
occurs(De,_) :-
var(De),
!,
fail.
occurs([D|De],OrdV) :-
( get_attr(D,itf,Att),
arg(2,Att,type(Type)),
arg(4,Att,lin(Lin)),
occ_type_filter(Type),
nf_coeff_of(Lin,OrdV,_)
-> true
; occurs(De,OrdV)
).

1275
GPL/clpqr/clpq/ineq_q.pl
View File

File diff suppressed because it is too large Load Diff

222
GPL/clpqr/clpq/itf_q.pl
View File

@ -1,222 +0,0 @@
/*
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(itf_q,
[
do_checks/8
]).
:- use_module(bv_q,
[
deref/2,
detach_bounds_vlv/5,
solve/1,
solve_ord_x/3
]).
:- use_module(nf_q,
[
nf/2
]).
:- use_module(store_q,
[
add_linear_11/3,
indep/2,
nf_coeff_of/3
]).
:- use_module('../clpqr/class',
[
class_drop/2
]).
do_checks(Y,Ty,St,Li,Or,Cl,No,Later) :-
numbers_only(Y),
verify_nonzero(No,Y),
verify_type(Ty,St,Y,Later,[]),
verify_lin(Or,Cl,Li,Y),
maplist(call,Later).
numbers_only(Y) :-
( var(Y)
; rational(Y)
; throw(type_error(_X = Y,2,'a rational number',Y))
),
!.
% verify_nonzero(Nonzero,Y)
%
% if Nonzero = nonzero, then verify that Y is not zero
% (if possible, otherwise set Y to be nonzero)
verify_nonzero(nonzero,Y) :-
( var(Y)
-> ( get_attr(Y,itf,Att)
-> setarg(8,Att,nonzero)
; put_attr(Y,itf,t(clpq,n,n,n,n,n,n,nonzero,n,n,n))
)
; Y =\= 0
).
verify_nonzero(n,_). % X is not nonzero
% verify_type(type(Type),strictness(Strict),Y,[OL|OLT],OLT)
%
% if possible verifies whether Y satisfies the type and strictness of X
% if not possible to verify, then returns the constraints that follow from
% the type and strictness
verify_type(type(Type),strictness(Strict),Y) -->
verify_type2(Y,Type,Strict).
verify_type(n,n,_) --> [].
verify_type2(Y,TypeX,StrictX) -->
{var(Y)},
!,
verify_type_var(TypeX,Y,StrictX).
verify_type2(Y,TypeX,StrictX) -->
{verify_type_nonvar(TypeX,Y,StrictX)}.
% verify_type_nonvar(Type,Nonvar,Strictness)
%
% verifies whether the type and strictness are satisfied with the Nonvar
verify_type_nonvar(t_none,_,_).
verify_type_nonvar(t_l(L),Value,S) :- ilb(S,L,Value).
verify_type_nonvar(t_u(U),Value,S) :- iub(S,U,Value).
verify_type_nonvar(t_lu(L,U),Value,S) :-
ilb(S,L,Value),
iub(S,U,Value).
verify_type_nonvar(t_L(L),Value,S) :- ilb(S,L,Value).
verify_type_nonvar(t_U(U),Value,S) :- iub(S,U,Value).
verify_type_nonvar(t_Lu(L,U),Value,S) :-
ilb(S,L,Value),
iub(S,U,Value).
verify_type_nonvar(t_lU(L,U),Value,S) :-
ilb(S,L,Value),
iub(S,U,Value).
% ilb(Strict,Lower,Value) & iub(Strict,Upper,Value)
%
% check whether Value is satisfiable with the given lower/upper bound and
% strictness.
% strictness is encoded as follows:
% 2 = strict lower bound
% 1 = strict upper bound
% 3 = strict lower and upper bound
% 0 = no strict bounds
ilb(S,L,V) :-
S /\ 2 =:= 0,
!,
L =< V. % non-strict
ilb(_,L,V) :- L < V. % strict
iub(S,U,V) :-
S /\ 1 =:= 0,
!,
V =< U. % non-strict
iub(_,U,V) :- V < U. % strict
%
% 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(Type,Var,Strictness,[OutList|OutListTail],OutListTail)
%
% returns the inequalities following from a type and strictness satisfaction
% test with Var
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(Strict,Lower,Value,[OL|OLT],OLT) and lub(Strict,Upper,Value,[OL|OLT],OLT)
%
% returns the inequalities following from the lower and upper bounds and the
% strictness see also lb and ub
llb(S,L,V) -->
{S /\ 2 =:= 0},
!,
[clpq:{L =< V}].
llb(_,L,V) --> [clpq:{L < V}].
lub(S,U,V) -->
{S /\ 1 =:= 0},
!,
[clpq:{V =< U}].
lub(_,U,V) --> [clpq:{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(order(OrdX),class(Class),lin(LinX),Y) :-
!,
( indep(LinX,OrdX)
-> detach_bounds_vlv(OrdX,LinX,Class,Y,NewLinX),
% if there were bounds, they are requeued already
class_drop(Class,Y),
nf(-Y,NfY),
deref(NfY,LinY),
add_linear_11(NewLinX,LinY,Lind),
( nf_coeff_of(Lind,OrdX,_)
-> % X is element of Lind
solve_ord_x(Lind,OrdX,Class)
; solve(Lind) % X is gone, can safely solve Lind
)
; class_drop(Class,Y),
nf(-Y,NfY),
deref(NfY,LinY),
add_linear_11(LinX,LinY,Lind),
solve(Lind)
).
verify_lin(_,_,_,_).

1118
GPL/clpqr/clpq/nf_q.pl
View File

File diff suppressed because it is too large Load Diff

398
GPL/clpqr/clpq/store_q.pl
View File

@ -1,398 +0,0 @@
/* $Id: store_q.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(store_q,
[
add_linear_11/3,
add_linear_f1/4,
add_linear_ff/5,
normalize_scalar/2,
delete_factor/4,
mult_linear_factor/3,
nf_rhs_x/4,
indep/2,
isolate/3,
nf_substitute/4,
mult_hom/3,
nf2sum/3,
nf_coeff_of/3,
renormalize/2
]).
% normalize_scalar(S,[N,Z])
%
% Transforms a scalar S into a linear expression [S,0]
normalize_scalar(S,[S,0]).
% renormalize(List,Lin)
%
% Renormalizes the not normalized linear expression in List into
% a normalized one. It does so to take care of unifications.
% (e.g. when a variable X is bound to a constant, the constant is added to
% the constant part of the linear expression; when a variable X is bound to
% another variable Y, the scalars of both are added)
renormalize([I,R|Hom],Lin) :-
length(Hom,Len),
renormalize_log(Len,Hom,[],Lin0),
add_linear_11([I,R],Lin0,Lin).
% renormalize_log(Len,Hom,HomTail,Lin)
%
% Logarithmically renormalizes the homogene part of a not normalized
% linear expression. See also renormalize/2.
renormalize_log(1,[Term|Xs],Xs,Lin) :-
!,
Term = l(X*_,_),
renormalize_log_one(X,Term,Lin).
renormalize_log(2,[A,B|Xs],Xs,Lin) :-
!,
A = l(X*_,_),
B = l(Y*_,_),
renormalize_log_one(X,A,LinA),
renormalize_log_one(Y,B,LinB),
add_linear_11(LinA,LinB,Lin).
renormalize_log(N,L0,L2,Lin) :-
P is N>>1,
Q is N-P,
renormalize_log(P,L0,L1,Lp),
renormalize_log(Q,L1,L2,Lq),
add_linear_11(Lp,Lq,Lin).
% renormalize_log_one(X,Term,Res)
%
% Renormalizes a term in X: if X is a nonvar, the term becomes a scalar.
renormalize_log_one(X,Term,Res) :-
var(X),
Term = l(X*K,_),
get_attr(X,itf,Att),
arg(5,Att,order(OrdX)), % Order might have changed
Res = [0,0,l(X*K,OrdX)].
renormalize_log_one(X,Term,Res) :-
nonvar(X),
Term = l(X*K,_),
Xk is X*K,
normalize_scalar(Xk,Res).
% ----------------------------- sparse vector stuff ---------------------------- %
% add_linear_ff(LinA,Ka,LinB,Kb,LinC)
%
% Linear expression LinC is the result of the addition of the 2 linear expressions
% LinA and LinB, each one multiplied by a scalar (Ka for LinA and Kb for LinB).
add_linear_ff(LinA,Ka,LinB,Kb,LinC) :-
LinA = [Ia,Ra|Ha],
LinB = [Ib,Rb|Hb],
LinC = [Ic,Rc|Hc],
Ic is Ia*Ka+Ib*Kb,
Rc is Ra*Ka+Rb*Kb,
add_linear_ffh(Ha,Ka,Hb,Kb,Hc).
% add_linear_ffh(Ha,Ka,Hb,Kb,Hc)
%
% Homogene part Hc is the result of the addition of the 2 homogene parts Ha and Hb,
% each one multiplied by a scalar (Ka for Ha and Kb for Hb)
add_linear_ffh([],_,Ys,Kb,Zs) :- mult_hom(Ys,Kb,Zs).
add_linear_ffh([l(X*Kx,OrdX)|Xs],Ka,Ys,Kb,Zs) :-
add_linear_ffh(Ys,X,Kx,OrdX,Xs,Zs,Ka,Kb).
% add_linear_ffh(Ys,X,Kx,OrdX,Xs,Zs,Ka,Kb)
%
% Homogene part Zs is the result of the addition of the 2 homogene parts Ys and
% [l(X*Kx,OrdX)|Xs], each one multiplied by a scalar (Ka for [l(X*Kx,OrdX)|Xs] and Kb for Ys)
add_linear_ffh([],X,Kx,OrdX,Xs,Zs,Ka,_) :- mult_hom([l(X*Kx,OrdX)|Xs],Ka,Zs).
add_linear_ffh([l(Y*Ky,OrdY)|Ys],X,Kx,OrdX,Xs,Zs,Ka,Kb) :-
compare(Rel,OrdX,OrdY),
( Rel = (=)
-> Kz is Kx*Ka+Ky*Kb,
( Kz =:= 0
-> add_linear_ffh(Xs,Ka,Ys,Kb,Zs)
; Zs = [l(X*Kz,OrdX)|Ztail],
add_linear_ffh(Xs,Ka,Ys,Kb,Ztail)
)
; Rel = (<)
-> Zs = [l(X*Kz,OrdX)|Ztail],
Kz is Kx*Ka,
add_linear_ffh(Xs,Y,Ky,OrdY,Ys,Ztail,Kb,Ka)
; Rel = (>)
-> Zs = [l(Y*Kz,OrdY)|Ztail],
Kz is Ky*Kb,
add_linear_ffh(Ys,X,Kx,OrdX,Xs,Ztail,Ka,Kb)
).
% add_linear_f1(LinA,Ka,LinB,LinC)
%
% special case of add_linear_ff with Kb = 1
add_linear_f1(LinA,Ka,LinB,LinC) :-
LinA = [Ia,Ra|Ha],
LinB = [Ib,Rb|Hb],
LinC = [Ic,Rc|Hc],
Ic is Ia*Ka+Ib,
Rc is Ra*Ka+Rb,
add_linear_f1h(Ha,Ka,Hb,Hc).
% add_linear_f1h(Ha,Ka,Hb,Hc)
%
% special case of add_linear_ffh/5 with Kb = 1
add_linear_f1h([],_,Ys,Ys).
add_linear_f1h([l(X*Kx,OrdX)|Xs],Ka,Ys,Zs) :-
add_linear_f1h(Ys,X,Kx,OrdX,Xs,Zs,Ka).
% add_linear_f1h(Ys,X,Kx,OrdX,Xs,Zs,Ka)
%
% special case of add_linear_ffh/8 with Kb = 1
add_linear_f1h([],X,Kx,OrdX,Xs,Zs,Ka) :- mult_hom([l(X*Kx,OrdX)|Xs],Ka,Zs).
add_linear_f1h([l(Y*Ky,OrdY)|Ys],X,Kx,OrdX,Xs,Zs,Ka) :-
compare(Rel,OrdX,OrdY),
( Rel = (=)
-> Kz is Kx*Ka+Ky,
( Kz =:= 0
-> add_linear_f1h(Xs,Ka,Ys,Zs)
; Zs = [l(X*Kz,OrdX)|Ztail],
add_linear_f1h(Xs,Ka,Ys,Ztail)
)
; Rel = (<)
-> Zs = [l(X*Kz,OrdX)|Ztail],
Kz is Kx*Ka,
add_linear_f1h(Xs,Ka,[l(Y*Ky,OrdY)|Ys],Ztail)
; Rel = (>)
-> Zs = [l(Y*Ky,OrdY)|Ztail],
add_linear_f1h(Ys,X,Kx,OrdX,Xs,Ztail,Ka)
).
% add_linear_11(LinA,LinB,LinC)
%
% special case of add_linear_ff with Ka = 1 and Kb = 1
add_linear_11(LinA,LinB,LinC) :-
LinA = [Ia,Ra|Ha],
LinB = [Ib,Rb|Hb],
LinC = [Ic,Rc|Hc],
Ic is Ia+Ib,
Rc is Ra+Rb,
add_linear_11h(Ha,Hb,Hc).
% add_linear_11h(Ha,Hb,Hc)
%
% special case of add_linear_ffh/5 with Ka = 1 and Kb = 1
add_linear_11h([],Ys,Ys).
add_linear_11h([l(X*Kx,OrdX)|Xs],Ys,Zs) :-
add_linear_11h(Ys,X,Kx,OrdX,Xs,Zs).
% add_linear_11h(Ys,X,Kx,OrdX,Xs,Zs)
%
% special case of add_linear_ffh/8 with Ka = 1 and Kb = 1
add_linear_11h([],X,Kx,OrdX,Xs,[l(X*Kx,OrdX)|Xs]).
add_linear_11h([l(Y*Ky,OrdY)|Ys],X,Kx,OrdX,Xs,Zs) :-
compare(Rel,OrdX,OrdY),
( Rel = (=)
-> Kz is Kx+Ky,
( Kz =:= 0
-> add_linear_11h(Xs,Ys,Zs)
; Zs = [l(X*Kz,OrdX)|Ztail],
add_linear_11h(Xs,Ys,Ztail)
)
; Rel = (<)
-> Zs = [l(X*Kx,OrdX)|Ztail],
add_linear_11h(Xs,Y,Ky,OrdY,Ys,Ztail)
; Rel = (>)
-> Zs = [l(Y*Ky,OrdY)|Ztail],
add_linear_11h(Ys,X,Kx,OrdX,Xs,Ztail)
).
% mult_linear_factor(Lin,K,Res)
%
% Linear expression Res is the result of multiplication of linear
% expression Lin by scalar K
mult_linear_factor(Lin,K,Mult) :-
K =:= 1,
!,
Mult = Lin.
mult_linear_factor(Lin,K,Res) :-
Lin = [I,R|Hom],
Res = [Ik,Rk|Mult],
Ik is I*K,
Rk is R*K,
mult_hom(Hom,K,Mult).
% mult_hom(Hom,K,Res)
%
% Homogene part Res is the result of multiplication of homogene part
% Hom by scalar K
mult_hom([],_,[]).
mult_hom([l(A*Fa,OrdA)|As],F,[l(A*Fan,OrdA)|Afs]) :-
Fan is F*Fa,
mult_hom(As,F,Afs).
% nf_substitute(Ord,Def,Lin,Res)
%
% Linear expression Res is the result of substitution of Var in
% linear expression Lin, by its definition in the form of linear
% expression Def
nf_substitute(OrdV,LinV,LinX,LinX1) :-
delete_factor(OrdV,LinX,LinW,K),
add_linear_f1(LinV,K,LinW,LinX1).
% delete_factor(Ord,Lin,Res,Coeff)
%
% Linear expression Res is the result of the deletion of the term
% Var*Coeff where Var has ordering Ord from linear expression Lin
delete_factor(OrdV,Lin,Res,Coeff) :-
Lin = [I,R|Hom],
Res = [I,R|Hdel],
delete_factor_hom(OrdV,Hom,Hdel,Coeff).
% delete_factor_hom(Ord,Hom,Res,Coeff)
%
% Homogene part Res is the result of the deletion of the term
% Var*Coeff from homogene part Hom
delete_factor_hom(VOrd,[Car|Cdr],RCdr,RKoeff) :-
Car = l(_*Koeff,Ord),
compare(Rel,VOrd,Ord),
( Rel= (=)
-> RCdr = Cdr,
RKoeff=Koeff
; Rel= (>)
-> RCdr = [Car|RCdr1],
delete_factor_hom(VOrd,Cdr,RCdr1,RKoeff)
).
% nf_coeff_of(Lin,OrdX,Coeff)
%
% Linear expression Lin contains the term l(X*Coeff,OrdX)
nf_coeff_of([_,_|Hom],VOrd,Coeff) :-
nf_coeff_hom(Hom,VOrd,Coeff).
% nf_coeff_hom(Lin,OrdX,Coeff)
%
% Linear expression Lin contains the term l(X*Coeff,OrdX) where the
% order attribute of X = OrdX
nf_coeff_hom([l(_*K,OVar)|Vs],OVid,Coeff) :-
compare(Rel,OVid,OVar),
( Rel = (=)
-> Coeff = K
; Rel = (>)
-> nf_coeff_hom(Vs,OVid,Coeff)
).
% nf_rhs_x(Lin,OrdX,Rhs,K)
%
% Rhs = R + I where Lin = [I,R|Hom] and l(X*K,OrdX) is a term of Hom
nf_rhs_x(Lin,OrdX,Rhs,K) :-
Lin = [I,R|Tail],
nf_coeff_hom(Tail,OrdX,K),
Rhs is R+I. % late because X may not occur in H
% isolate(OrdN,Lin,Lin1)
%
% Linear expression Lin1 is the result of the transformation of linear expression
% Lin = 0 which contains the term l(New*K,OrdN) into an equivalent expression Lin1 = New.
isolate(OrdN,Lin,Lin1) :-
delete_factor(OrdN,Lin,Lin0,Coeff),
K is -1 rdiv Coeff,
mult_linear_factor(Lin0,K,Lin1).
% indep(Lin,OrdX)
%
% succeeds if Lin = [0,_|[l(X*1,OrdX)]]
indep(Lin,OrdX) :-
Lin = [I,_|[l(_*K,OrdY)]],
OrdX == OrdY,
K =:= 1,
I =:= 0.
% nf2sum(Lin,Sofar,Term)
%
% Transforms a linear expression into a sum
% (e.g. the expression [5,_,[l(X*2,OrdX),l(Y*-1,OrdY)]] gets transformed into 5 + 2*X - Y)
nf2sum([],I,I).
nf2sum([X|Xs],I,Sum) :-
( I =:= 0
-> X = l(Var*K,_),
( K =:= 1
-> hom2sum(Xs,Var,Sum)
; K =:= -1
-> hom2sum(Xs,-Var,Sum)
; hom2sum(Xs,K*Var,Sum)
)
; hom2sum([X|Xs],I,Sum)
).
% hom2sum(Hom,Sofar,Term)
%
% Transforms a linear expression into a sum
% this predicate handles all but the first term
% (the first term does not need a concatenation symbol + or -)
% see also nf2sum/3
hom2sum([],Term,Term).
hom2sum([l(Var*K,_)|Cs],Sofar,Term) :-
( K =:= 1
-> Next = Sofar + Var
; K =:= -1
-> Next = Sofar - Var
; K < 0
-> Ka is -K,
Next = Sofar - Ka*Var
; Next = Sofar + K*Var
),
hom2sum(Cs,Next,Term).

155
GPL/clpqr/clpqr/class.pl
View File

@ -1,155 +0,0 @@
/* $Id: class.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(class,
[
class_allvars/2,
class_new/5,
class_drop/2,
class_basis/2,
class_basis_add/3,
class_basis_drop/2,
class_basis_pivot/3,
class_get_clp/2,
class_get_prio/2,
class_put_prio/2,
ordering/1,
arrangement/2
]).
:- use_module(ordering,
[
combine/3,
ordering/1,
arrangement/2
]).
:- use_module(library(lists),
[ append/3
]).
% called when two classes are unified: the allvars lists are appended to eachother, as well as the basis
% lists.
%
% note: La=[A,B,...,C|Lat], Lb=[D,E,...,F|Lbt], so new La = [A,B,...,C,D,E,...,F|Lbt]
attr_unify_hook(class(CLP,La,Lat,ABasis,PrioA),Y) :-
!,
var(Y),
get_attr(Y,class,class(CLP,Lb,Lbt,BBasis,PrioB)),
Lat = Lb,
append(ABasis,BBasis,CBasis),
combine(PrioA,PrioB,PrioC),
put_attr(Y,class,class(CLP,La,Lbt,CBasis,PrioC)).
attr_unify_hook(_,_).
class_new(Class,CLP,All,AllT,Basis) :-
put_attr(Su,class,class(CLP,All,AllT,Basis,[])),
Su = Class.
class_get_prio(Class,Priority) :-
get_attr(Class,class,class(_,_,_,_,Priority)).
class_get_clp(Class,CLP) :-
get_attr(Class,class,class(CLP,_,_,_,_)).
class_put_prio(Class,Priority) :-
get_attr(Class,class,class(CLP,All,AllT,Basis,_)),
put_attr(Class,class,class(CLP,All,AllT,Basis,Priority)).
class_drop(Class,X) :-
get_attr(Class,class,class(CLP,Allvars,Tail,Basis,Priority)),
delete_first(Allvars,X,NewAllvars),
delete_first(Basis,X,NewBasis),
put_attr(Class,class,class(CLP,NewAllvars,Tail,NewBasis,Priority)).
class_allvars(Class,All) :- get_attr(Class,class,class(_,All,_,_,_)).
% class_basis(Class,Basis)
%
% Returns the basis of class Class.
class_basis(Class,Basis) :- get_attr(Class,class,class(_,_,_,Basis,_)).
% class_basis_add(Class,X,NewBasis)
%
% adds X in front of the basis and returns the new basis
class_basis_add(Class,X,NewBasis) :-
NewBasis = [X|Basis],
get_attr(Class,class,class(CLP,All,AllT,Basis,Priority)),
put_attr(Class,class,class(CLP,All,AllT,NewBasis,Priority)).
% class_basis_drop(Class,X)
%
% removes the first occurence of X from the basis (if exists)
class_basis_drop(Class,X) :-
get_attr(Class,class,class(CLP,All,AllT,Basis0,Priority)),
delete_first(Basis0,X,Basis),
Basis0 \== Basis, % anything deleted ?
!,
put_attr(Class,class,class(CLP,All,AllT,Basis,Priority)).
class_basis_drop(_,_).
% class_basis_pivot(Class,Enter,Leave)
%
% removes first occurence of Leave from the basis and adds Enter in front of the basis
class_basis_pivot(Class,Enter,Leave) :-
get_attr(Class,class,class(CLP,All,AllT,Basis0,Priority)),
delete_first(Basis0,Leave,Basis1),
put_attr(Class,class,class(CLP,All,AllT,[Enter|Basis1],Priority)).
% delete_first(Old,Element,New)
%
% removes the first occurence of Element from Old and returns the result in New
%
% note: test via syntactic equality, not unifiability
delete_first(L,_,Res) :-
var(L),
!,
Res = L.
delete_first([],_,[]).
delete_first([Y|Ys],X,Res) :-
( X==Y
-> Res = Ys
; Res = [Y|Tail],
delete_first(Ys,X,Tail)
).

303
GPL/clpqr/clpqr/dump.pl
View File

@ -1,303 +0,0 @@
/* $Id: dump.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(dump,
[
dump/3,
projecting_assert/1
]).
:- use_module(class,
[
class_allvars/2
]).
:- use_module(geler,
[
collect_nonlin/3
]).
:- use_module(library(assoc),
[
empty_assoc/1,
get_assoc/3,
put_assoc/4,
assoc_to_list/2
]).
:- use_module(itf,
[
dump_linear/3,
dump_nonzero/3
]).
:- use_module(project,
[
project_attributes/2
]).
:- use_module(ordering,
[
ordering/1
]).
% dump(Target,NewVars,Constraints)
%
% Returns in <Constraints>, the constraints that currently hold on Target where
% all variables in <Target> are copied to new variables in <NewVars> and the
% constraints are given on these new variables. In short, you can safely
% manipulate <NewVars> and <Constraints> without changing the constraints on
% <Target>.
dump([],[],[]) :- !.
dump(Target,NewVars,Constraints) :-
( ( proper_varlist(Target)
-> true
; % Target is not a list of variables
throw(instantiation_error(dump(Target,NewVars,Constraints),1))
),
ordering(Target),
related_linear_vars(Target,All), % All contains all variables of the classes of Target variables.
nonlin_crux(All,Nonlin),
project_attributes(Target,All),
related_linear_vars(Target,Again), % project drops/adds vars
all_attribute_goals(Again,Gs,Nonlin),
empty_assoc(D0),
mapping(Target,NewVars,D0,D1), % late (AVL suffers from put_atts)
copy(Gs,Copy,D1,_), % strip constraints
nb_setval(clpqr_dump,NewVars/Copy),
fail % undo projection
; catch(nb_getval(clpqr_dump,NewVars/Constraints),_,fail),
nb_delete(clpqr_dump)
).
:- meta_predicate projecting_assert(:).
projecting_assert(QClause) :-
strip_module(QClause, Module, Clause), % JW: SWI-Prolog not always qualifies the term!
copy_term(Clause,Copy,Constraints),
l2c(Constraints,Conj), % fails for []
( Sm = clpq
; Sm = clpr
), % proper module for {}/1
!,
( Copy = (H:-B)
-> % former rule
Module:assert((H:-Sm:{Conj},B))
; % former fact
Module:assert((Copy:-Sm:{Conj}))
).
projecting_assert(Clause) :- % not our business
assert(Clause).
copy_term(Term,Copy,Constraints) :-
( term_variables(Term,Target), % get all variables in Term
related_linear_vars(Target,All), % get all variables of the classes of the variables in Term
nonlin_crux(All,Nonlin), % get a list of all the nonlinear goals of these variables
project_attributes(Target,All),
related_linear_vars(Target,Again), % project drops/adds vars
all_attribute_goals(Again,Gs,Nonlin),
empty_assoc(D0),
copy(Term/Gs,TmpCopy,D0,_), % strip constraints
nb_setval(clpqr_dump,TmpCopy),
fail
; catch(nb_getval(clpqr_dump,Copy/Constraints),_,fail),
nb_delete(clpqr_copy_term)
).
% l2c(Lst,Conj)
%
% converts a list to a round list: [a,b,c] -> (a,b,c) and [a] becomes a
l2c([X|Xs],Conj) :-
( Xs = []
-> Conj = X
; Conj = (X,Xc),
l2c(Xs,Xc)
).
% proper_varlist(List)
%
% Returns whether Lst is a list of variables.
% First clause is to avoid unification of a variable with a list.
proper_varlist(X) :-
var(X),
!,
fail.
proper_varlist([]).
proper_varlist([X|Xs]) :-
var(X),
proper_varlist(Xs).
% related_linear_vars(Vs,All)
%
% Generates a list of all variables that are in the classes of the variables in
% Vs.
related_linear_vars(Vs,All) :-
empty_assoc(S0),
related_linear_sys(Vs,S0,Sys),
related_linear_vars(Sys,All,[]).
% related_linear_sys(Vars,Assoc,List)
%
% Generates in List, a list of all to classes to which variables in Vars
% belong.
% Assoc should be an empty association list and is used internally.
% List contains elements of the form C-C where C is a class and both C's are
% equal.
related_linear_sys([],S0,L0) :- assoc_to_list(S0,L0).
related_linear_sys([V|Vs],S0,S2) :-
( get_attr(V,itf,Att),
arg(6,Att,class(C))
-> put_assoc(C,S0,C,S1)
; S1 = S0
),
related_linear_sys(Vs,S1,S2).
% related_linear_vars(Classes,[Vars|VarsTail],VarsTail)
%
% Generates a difference list of all variables in the classes in Classes.
% Classes contains elements of the form C-C where C is a class and both C's are
% equal.
related_linear_vars([]) --> [].
related_linear_vars([S-_|Ss]) -->
{
class_allvars(S,Otl)
},
cpvars(Otl),
related_linear_vars(Ss).
% cpvars(Vars,Out,OutTail)
%
% Makes a new difference list of the difference list Vars.
% All nonvars are removed.
cpvars(Xs) --> {var(Xs)}, !.
cpvars([X|Xs]) -->
( { var(X) }
-> [X]
; []
),
cpvars(Xs).
% nonlin_crux(All,Gss)
%
% Collects all pending non-linear constraints of variables in All.
% This marks all nonlinear goals of the variables as run and cannot
% be reversed manually.
nonlin_crux(All,Gss) :-
collect_nonlin(All,Gs,[]), % collect the nonlinear goals of variables All
% this marks the goals as run and cannot be reversed manually
nonlin_strip(Gs,Gss).
% nonlin_strip(Gs,Solver,Res)
%
% Removes the goals from Gs that are not from solver Solver.
nonlin_strip([],[]).
nonlin_strip([_:What|Gs],Res) :-
( What = {G}
-> Res = [G|Gss]
; Res = [What|Gss]
),
nonlin_strip(Gs,Gss).
all_attribute_goals([]) --> [].
all_attribute_goals([V|Vs]) -->
dump_linear(V),
dump_nonzero(V),
all_attribute_goals(Vs).
% mapping(L1,L2,AssocIn,AssocOut)
%
% Makes an association mapping of lists L1 and L2:
% L1 = [L1H|L1T] and L2 = [L2H|L2T] then the association L1H-L2H is formed
% and the tails are mapped similarly.
mapping([],[],D0,D0).
mapping([T|Ts],[N|Ns],D0,D2) :-
put_assoc(T,D0,N,D1),
mapping(Ts,Ns,D1,D2).
% copy(Term,Copy,AssocIn,AssocOut)
%
% Makes a copy of Term by changing all variables in it to new ones and
% building an association between original variables and the new ones.
% E.g. when Term = test(A,B,C), Copy = test(D,E,F) and an association between
% A and D, B and E and C and F is formed in AssocOut. AssocIn is input
% association.
copy(Term,Copy,D0,D1) :-
var(Term),
( get_assoc(Term,D0,New)
-> Copy = New,
D1 = D0
; put_assoc(Term,D0,Copy,D1)
).
copy(Term,Copy,D0,D1) :-
nonvar(Term), % Term is a functor
functor(Term,N,A),
functor(Copy,N,A), % Copy is new functor with the same name and arity as Term
copy(A,Term,Copy,D0,D1).
% copy(Nb,Term,Copy,AssocIn,AssocOut)
%
% Makes a copy of the Nb arguments of Term by changing all variables in it to
% new ones and building an association between original variables and the new
% ones.
% See also copy/4
copy(0,_,_,D0,D0) :- !.
copy(1,T,C,D0,D1) :- !,
arg(1,T,At1),
arg(1,C,Ac1),
copy(At1,Ac1,D0,D1).
copy(2,T,C,D0,D2) :- !,
arg(1,T,At1),
arg(1,C,Ac1),
copy(At1,Ac1,D0,D1),
arg(2,T,At2),
arg(2,C,Ac2),
copy(At2,Ac2,D1,D2).
copy(N,T,C,D0,D2) :-
arg(N,T,At),
arg(N,C,Ac),
copy(At,Ac,D0,D1),
N1 is N-1,
copy(N1,T,C,D1,D2).

192
GPL/clpqr/clpqr/geler.pl
View File

@ -1,192 +0,0 @@
/* $Id: geler.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(geler,
[
geler/3,
project_nonlin/3,
collect_nonlin/3
]).
% l2conj(List,Conj)
%
% turns a List into a conjunction of the form (El,Conj) where Conj
% is of the same form recursively and El is an element of the list
l2conj([X|Xs],Conj) :-
( X = [],
Conj = X
; Xs = [_|_],
Conj = (X,Xc),
l2conj(Xs,Xc)
).
% nonexhausted(Goals,OutList,OutListTail)
%
% removes the goals that have already run from Goals
% and puts the result in the difference list OutList
nonexhausted(run(Mutex,G)) -->
( { var(Mutex) }
-> [G]
; []
).
nonexhausted((A,B)) -->
nonexhausted(A),
nonexhausted(B).
attr_unify_hook(g(CLP,goals(Gx),_),Y) :-
!,
( var(Y),
( get_attr(Y,geler,g(A,B,C))
-> ignore((CLP \== A,throw(error(permission_error(
'apply CLP(Q) constraints on','CLP(R) variable',Y),
context(_))))),
( % possibly mutual goals. these need to be run.
% other goals are run as well to remove redundant goals.
B = goals(Gy)
-> Later = [Gx,Gy],
( C = n
-> del_attr(Y,geler)
; put_attr(Y,geler,g(CLP,n,C))
)
; % no goals in Y, so no mutual goals of X and Y, store
% goals of X in Y
% no need to run any goal.
Later = [],
put_attr(Y,geler,g(CLP,goals(Gx),C))
)
; Later = [],
put_attr(Y,geler,g(CLP,goals(Gx),n))
)
; nonvar(Y),
Later = [Gx]
),
maplist(call,Later).
attr_unify_hook(_,_). % no goals in X
%
% called from project.pl
%
project_nonlin(_,Cvas,Reachable) :-
collect_nonlin(Cvas,L,[]),
sort(L,Ls),
term_variables(Ls,Reachable).
%put_attr(_,all_nonlin(Ls)).
collect_nonlin([]) --> [].
collect_nonlin([X|Xs]) -->
( { get_attr(X,geler,g(_,goals(Gx),_)) }
-> trans(Gx),
collect_nonlin(Xs)
; collect_nonlin(Xs)
).
% trans(Goals,OutList,OutListTail)
%
% transforms the goals (of the form run(Mutex,Goal)
% that are in Goals (in the conjunction form, see also l2conj)
% that have not been run (Mutex = variable) into a readable output format
% and notes that they're done (Mutex = 'done'). Because of the Mutex
% variable, each goal is only added once (so not for each variable).
trans((A,B)) -->
trans(A),
trans(B).
trans(run(Mutex,Gs)) -->
( { var(Mutex) }
-> { Mutex = done },
transg(Gs)
; []
).
transg((A,B)) -->
!,
transg(A),
transg(B).
transg(M:G) -->
!,
M:transg(G).
transg(G) --> [G].
% run(Mutex,G)
%
% Calls goal G if it has not yet run (Mutex is still variable)
% and stores that it has run (Mutex = done). This is done so
% that when X = Y and X and Y are in the same goal, that goal
% is called only once.
run(Mutex,_) :- nonvar(Mutex).
run(Mutex,G) :-
var(Mutex),
Mutex = done,
call(G).
% geler(Vars,Goal)
%
% called by nf.pl when an unsolvable non-linear expression is found
% Vars contain the variables of the expression, Goal contains the predicate of
% nf.pl to be called when the variables are bound.
geler(CLP,Vars,Goal) :-
attach(Vars,CLP,run(_Mutex,Goal)).
% one goal gets the same mutex on every var, so it is run only once
% attach(Vars,Goal)
%
% attaches a new goal to be awoken when the variables get bounded.
% when the old value of the attribute goals = OldGoal, then the new value =
% (Goal,OldGoal)
attach([],_,_).
attach([V|Vs],CLP,Goal) :-
var(V),
( get_attr(V,geler,g(A,B,C))
-> ( CLP \== A
-> throw(error(permission_error('apply CLP(Q) constraints on',
'CLP(R) variable',V),context(_)))
; ( B = goals(Goals)
-> put_attr(V,geler,g(A,goals((Goal,Goals)),C))
; put_attr(V,geler,g(A,goals(Goal),C))
)
)
; put_attr(V,geler,g(CLP,goals(Goal),n))
),
attach(Vs,CLP,Goal).

123
GPL/clpqr/clpqr/itf.pl
View File

@ -1,123 +0,0 @@
/*
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
% attribute = t(CLP,type(_),strictness(_),lin(_),order(_),class(_),forward(_),
% nonzero,target,keep_indep,keep)
:- module(itf,
[
dump_linear/3,
dump_nonzero/3,
clp_type/2
]).
clp_type(Var,Type) :-
( get_attr(Var,itf,Att)
-> arg(1,Att,Type)
; get_attr(Var,geler,Att)
-> arg(1,Att,Type)
).
dump_linear(V) -->
{
get_attr(V,itf,Att),
arg(1,Att,CLP),
arg(2,Att,type(Type)),
arg(4,Att,lin(Lin)),
!,
Lin = [I,_|H]
},
( {
Type=t_none
; arg(9,Att,n)
}
-> []
; dump_v(CLP,t_none,V,I,H)
),
( {
Type=t_none,
arg(9,Att,n) % attribute should not have changed by dump_v...
}
-> % nonzero produces such
[]
; dump_v(CLP,Type,V,I,H)
).
dump_linear(_) --> [].
dump_v(clpq,Type,V,I,H) --> bv_q:dump_var(Type,V,I,H).
dump_v(clpr,Type,V,I,H) --> bv_r:dump_var(Type,V,I,H).
dump_nonzero(V) -->
{
get_attr(V,itf,Att),
arg(1,Att,CLP),
arg(4,Att,lin(Lin)),
arg(8,Att,nonzero),
!,
Lin = [I,_|H]
},
dump_nz(CLP,V,H,I).
dump_nonzero(_) --> [].
dump_nz(clpq,V,H,I) --> bv_q:dump_nz(V,H,I).
dump_nz(clpr,V,H,I) --> bv_r:dump_nz(V,H,I).
attr_unify_hook(t(CLP,n,n,n,n,n,n,n,_,_,_),Y) :-
!,
( get_attr(Y,itf,AttY),
\+ arg(1,AttY,CLP)
-> throw(error(permission_error('mix CLP(Q) variables with',
'CLP(R) variables:',Y),context(_)))
; true
).
attr_unify_hook(t(CLP,Ty,St,Li,Or,Cl,_,No,_,_,_),Y) :-
( get_attr(Y,itf,AttY),
\+ arg(1,AttY,CLP)
-> throw(error(permission_error('mix CLP(Q) variables with',
'CLP(R) variables:',Y),context(_)))
; true
),
do_checks(CLP,Y,Ty,St,Li,Or,Cl,No,Later),
maplist(call,Later).
do_checks(clpq,Y,Ty,St,Li,Or,Cl,No,Later) :-
itf_q:do_checks(Y,Ty,St,Li,Or,Cl,No,Later).
do_checks(clpr,Y,Ty,St,Li,Or,Cl,No,Later) :-
itf_r:do_checks(Y,Ty,St,Li,Or,Cl,No,Later).

198
GPL/clpqr/clpqr/ordering.pl
View File

@ -1,198 +0,0 @@
/* $Id: ordering.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(ordering,
[
combine/3,
ordering/1,
arrangement/2
]).
:- use_module(class,
[
class_get_clp/2,
class_get_prio/2,
class_put_prio/2
]).
:- use_module(itf,
[
clp_type/2
]).
:- use_module(library(ugraphs),
[
add_edges/3,
add_vertices/3,
top_sort/2,
ugraph_union/3
]).
:- use_module(library(lists),
[
append/3
]).
ordering(X) :-
var(X),
!,
fail.
ordering(A>B) :-
!,
ordering(B<A).
ordering(A<B) :-
join_class([A,B],Class),
class_get_prio(Class,Ga),
!,
add_edges([],[A-B],Gb),
combine(Ga,Gb,Gc),
class_put_prio(Class,Gc).
ordering(Pb) :-
Pb = [_|Xs],
join_class(Pb,Class),
class_get_prio(Class,Ga),
!,
( Xs = [],
add_vertices([],Pb,Gb)
; Xs=[_|_],
gen_edges(Pb,Es,[]),
add_edges([],Es,Gb)
),
combine(Ga,Gb,Gc),
class_put_prio(Class,Gc).
ordering(_).
arrangement(Class,Arr) :-
class_get_prio(Class,G),
normalize(G,Gn),
top_sort(Gn,Arr),
!.
arrangement(_,_) :- throw(unsatisfiable_ordering).
join_class([],_).
join_class([X|Xs],Class) :-
( var(X)
-> clp_type(X,CLP),
( CLP = clpr
-> bv_r:var_intern(X,Class)
; bv_q:var_intern(X,Class)
)
; true
),
join_class(Xs,Class).
% combine(Ga,Gb,Gc)
%
% Combines the vertices of Ga and Gb into Gc.
combine(Ga,Gb,Gc) :-
normalize(Ga,Gan),
normalize(Gb,Gbn),
ugraph_union(Gan,Gbn,Gc).
%
% both Ga and Gb might have their internal ordering invalidated
% because of bindings and aliasings
%
normalize([],[]) :- !.
normalize(G,Gsgn) :-
G = [_|_],
keysort(G,Gs), % sort vertices on key
group(Gs,Gsg), % concatenate vertices with the same key
normalize_vertices(Gsg,Gsgn). % normalize
normalize_vertices([],[]).
normalize_vertices([X-Xnb|Xs],Res) :-
( normalize_vertex(X,Xnb,Xnorm)
-> Res = [Xnorm|Xsn],
normalize_vertices(Xs,Xsn)
; normalize_vertices(Xs,Res)
).
% normalize_vertex(X,Nbs,X-Nbss)
%
% Normalizes a vertex X-Nbs into X-Nbss by sorting Nbs, removing duplicates (also of X)
% and removing non-vars.
normalize_vertex(X,Nbs,X-Nbsss) :-
var(X),
sort(Nbs,Nbss),
strip_nonvar(Nbss,X,Nbsss).
% strip_nonvar(Nbs,X,Res)
%
% Turns vertext X-Nbs into X-Res by removing occurrences of X from Nbs and removing
% non-vars. This to normalize after bindings have occurred. See also normalize_vertex/3.
strip_nonvar([],_,[]).
strip_nonvar([X|Xs],Y,Res) :-
( X==Y % duplicate of Y
-> strip_nonvar(Xs,Y,Res)
; var(X) % var: keep
-> Res = [X|Stripped],
strip_nonvar(Xs,Y,Stripped)
; % nonvar: remove
nonvar(X),
Res = [] % because Vars<anything
).
gen_edges([]) --> [].
gen_edges([X|Xs]) -->
gen_edges(Xs,X),
gen_edges(Xs).
gen_edges([],_) --> [].
gen_edges([Y|Ys],X) -->
[X-Y],
gen_edges(Ys,X).
% group(Vert,Res)
%
% Concatenates vertices with the same key.
group([],[]).
group([K-Kl|Ks],Res) :-
group(Ks,K,Kl,Res).
group([],K,Kl,[K-Kl]).
group([L-Ll|Ls],K,Kl,Res) :-
( K==L
-> append(Kl,Ll,KLl),
group(Ls,K,KLl,Res)
; Res = [K-Kl|Tail],
group(Ls,L,Ll,Tail)
).

305
GPL/clpqr/clpqr/project.pl
View File

@ -1,305 +0,0 @@
/*
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
%
% Answer constraint projection
%
%:- public project_attributes/2. % xref.pl
:- module(project,
[
drop_dep/1,
drop_dep_one/1,
make_target_indep/2,
project_attributes/2
]).
:- use_module(class,
[
class_allvars/2
]).
:- use_module(geler,
[
project_nonlin/3
]).
:- use_module(redund,
[
redundancy_vars/1,
systems/3
]).
:- use_module(ordering,
[
arrangement/2
]).
%
% interface predicate
%
% May be destructive (either acts on a copy or in a failure loop)
%
project_attributes(TargetVars,Cvas) :-
sort(TargetVars,Tvs), % duplicates ?
sort(Cvas,Avs), % duplicates ?
get_clp(TargetVars,CLP),
( nonvar(CLP)
-> mark_target(Tvs),
project_nonlin(Tvs,Avs,NlReachable),
( Tvs == []
-> drop_lin_atts(Avs)
; redundancy_vars(Avs), % removes redundant bounds (redund.pl)
make_target_indep(Tvs,Pivots), % pivot partners are marked to be kept during elim.
mark_target(NlReachable), % after make_indep to express priority
drop_dep(Avs),
fm_elim(CLP,Avs,Tvs,Pivots),
impose_ordering(Avs)
)
; true
).
fm_elim(clpq,Avs,Tvs,Pivots) :- fourmotz_q:fm_elim(Avs,Tvs,Pivots).
fm_elim(clpr,Avs,Tvs,Pivots) :- fourmotz_r:fm_elim(Avs,Tvs,Pivots).
get_clp([],_).
get_clp([H|T],CLP) :-
( get_attr(H,itf,Att)
-> arg(1,Att,CLP)
; true
),
get_clp(T,CLP).
% mark_target(Vars)
%
% Marks the variables in Vars as target variables.
mark_target([]).
mark_target([V|Vs]) :-
( get_attr(V,itf,Att)
-> setarg(9,Att,target)
; true
),
mark_target(Vs).
% mark_keep(Vars)
%
% Mark the variables in Vars to be kept during elimination.
mark_keep([]).
mark_keep([V|Vs]) :-
get_attr(V,itf,Att),
setarg(11,Att,keep),
mark_keep(Vs).
%
% Collect the pivots in reverse order
% We have to protect the target variables pivot partners
% from redundancy eliminations triggered by fm_elim,
% in order to allow for reverse pivoting.
%
make_target_indep(Ts,Ps) :- make_target_indep(Ts,[],Ps).
% make_target_indep(Targets,Pivots,PivotsTail)
%
% Tries to make as many targetvariables independent by pivoting them with a non-target
% variable. The pivots are stored as T:NT where T is a target variable and NT a non-target
% variable. The non-target variables are marked to be kept during redundancy eliminations.
make_target_indep([],Ps,Ps).
make_target_indep([T|Ts],Ps0,Pst) :-
( get_attr(T,itf,AttT),
arg(1,AttT,CLP),
arg(2,AttT,type(Type)),
arg(4,AttT,lin([_,_|H])),
nontarget(H,Nt)
-> Ps1 = [T:Nt|Ps0],
get_attr(Nt,itf,AttN),
arg(2,AttN,type(IndAct)),
arg(5,AttN,order(Ord)),
arg(6,AttN,class(Class)),
setarg(11,AttN,keep),
pivot(CLP,T,Class,Ord,Type,IndAct)
; Ps1 = Ps0
),
make_target_indep(Ts,Ps1,Pst).
% nontarget(Hom,Nt)
%
% Finds a nontarget variable in homogene part Hom.
% Hom contains elements of the form l(V*K,OrdV).
% A nontarget variable has no target attribute and no keep_indep attribute.
nontarget([l(V*_,_)|Vs],Nt) :-
( get_attr(V,itf,Att),
arg(9,Att,n),
arg(10,Att,n)
-> Nt = V
; nontarget(Vs,Nt)
).
% drop_dep(Vars)
%
% Does drop_dep_one/1 on each variable in Vars.
drop_dep(Vs) :-
var(Vs),
!.
drop_dep([]).
drop_dep([V|Vs]) :-
drop_dep_one(V),
drop_dep(Vs).
% drop_dep_one(V)
%
% If V is an unbounded dependent variable that isn't a target variable, shouldn't be kept
% and is not nonzero, drops all linear attributes of V.
% The linear attributes are: type, strictness, linear equation (lin), class and order.
drop_dep_one(V) :-
get_attr(V,itf,Att),
Att = t(CLP,type(t_none),_,lin(Lin),order(OrdV),_,_,n,n,_,n),
\+ indep(CLP,Lin,OrdV),
!,
setarg(2,Att,n),
setarg(3,Att,n),
setarg(4,Att,n),
setarg(5,Att,n),
setarg(6,Att,n).
drop_dep_one(_).
indep(clpq,Lin,OrdV) :- store_q:indep(Lin,OrdV).
indep(clpr,Lin,OrdV) :- store_r:indep(Lin,OrdV).
pivot(clpq,T,Class,Ord,Type,IndAct) :- bv_q:pivot(T,Class,Ord,Type,IndAct).
pivot(clpr,T,Class,Ord,Type,IndAct) :- bv_r:pivot(T,Class,Ord,Type,IndAct).
renormalize(clpq,Lin,New) :- store_q:renormalize(Lin,New).
renormalize(clpr,Lin,New) :- store_r:renormalize(Lin,New).
% drop_lin_atts(Vs)
%
% Removes the linear attributes of the variables in Vs.
% The linear attributes are type, strictness, linear equation (lin), order and class.
drop_lin_atts([]).
drop_lin_atts([V|Vs]) :-
get_attr(V,itf,Att),
setarg(2,Att,n),
setarg(3,Att,n),
setarg(4,Att,n),
setarg(5,Att,n),
setarg(6,Att,n),
drop_lin_atts(Vs).
impose_ordering(Cvas) :-
systems(Cvas,[],Sys),
impose_ordering_sys(Sys).
impose_ordering_sys([]).
impose_ordering_sys([S|Ss]) :-
arrangement(S,Arr), % ordering.pl
arrange(Arr,S),
impose_ordering_sys(Ss).
arrange([],_).
arrange(Arr,S) :-
Arr = [_|_],
class_allvars(S,All),
order(Arr,1,N),
order(All,N,_),
renorm_all(All),
arrange_pivot(All).
order(Xs,N,M) :-
var(Xs),
!,
N = M.
order([],N,N).
order([X|Xs],N,M) :-
( get_attr(X,itf,Att),
arg(5,Att,order(O)),
var(O)
-> O = N,
N1 is N+1,
order(Xs,N1,M)
; order(Xs,N,M)
).
% renorm_all(Vars)
%
% Renormalizes all linear equations of the variables in difference list Vars to reflect
% their new ordering.
renorm_all(Xs) :-
var(Xs),
!.
renorm_all([X|Xs]) :-
( get_attr(X,itf,Att),
arg(1,Att,CLP),
arg(4,Att,lin(Lin))
-> renormalize(CLP,Lin,New),
setarg(4,Att,lin(New)),
renorm_all(Xs)
; renorm_all(Xs)
).
% arrange_pivot(Vars)
%
% If variable X of Vars has type t_none and has a higher order than the first element of
% its linear equation, then it is pivoted with that element.
arrange_pivot(Xs) :-
var(Xs),
!.
arrange_pivot([X|Xs]) :-
( get_attr(X,itf,AttX),
%arg(8,AttX,n), % not for nonzero
arg(1,AttX,CLP),
arg(2,AttX,type(t_none)),
arg(4,AttX,lin(Lin)),
arg(5,AttX,order(OrdX)),
Lin = [_,_,l(Y*_,_)|_],
get_attr(Y,itf,AttY),
arg(2,AttY,type(IndAct)),
arg(5,AttY,order(OrdY)),
arg(6,AttY,class(Class)),
compare(>,OrdY,OrdX)
-> pivot(CLP,X,Class,OrdY,t_none,IndAct),
arrange_pivot(Xs)
; arrange_pivot(Xs)
).

297
GPL/clpqr/clpqr/redund.pl
View File

@ -1,297 +0,0 @@
/*
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2006, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
Prolog and distributed under the license details below with permission from
all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(redund,
[
redundancy_vars/1,
systems/3
]).
:- use_module(class,
[
class_allvars/2
]).
%
% redundancy removal (semantic definition)
%
% done:
% +) deal with active bounds
% +) indep t_[lu] -> t_none invalidates invariants (fixed)
%
% systems(Vars,SystemsIn,SystemsOut)
%
% Returns in SystemsOut the different classes to which variables in Vars
% belong. Every class only appears once in SystemsOut.
systems([],Si,Si).
systems([V|Vs],Si,So) :-
( var(V),
get_attr(V,itf,Att),
arg(6,Att,class(C)),
not_memq(Si,C)
-> systems(Vs,[C|Si],So)
; systems(Vs,Si,So)
).
% not_memq(Lst,El)
%
% Succeeds if El is not a member of Lst (does not use unification).
not_memq([],_).
not_memq([Y|Ys],X) :-
X \== Y,
not_memq(Ys,X).
% redundancy_systems(Classes)
%
% Does redundancy removal via redundancy_vs/1 on all variables in the classes Classes.
redundancy_systems([]).
redundancy_systems([S|Sys]) :-
class_allvars(S,All),
redundancy_vs(All),
redundancy_systems(Sys).
% redundancy_vars(Vs)
%
% Does the same thing as redundancy_vs/1 but has some extra timing facilities that
% may be used.
redundancy_vars(Vs) :-
!,
redundancy_vs(Vs).
redundancy_vars(Vs) :-
statistics(runtime,[Start|_]),
redundancy_vs(Vs),
statistics(runtime,[End|_]),
Duration is End-Start,
format(user_error,"% Redundancy elimination took ~d msec~n",Duration).
% redundancy_vs(Vs)
%
% Removes redundant bounds from the variables in Vs via redundant/3
redundancy_vs(Vs) :-
var(Vs),
!.
redundancy_vs([]).
redundancy_vs([V|Vs]) :-
( get_attr(V,itf,Att),
arg(2,Att,type(Type)),
arg(3,Att,strictness(Strict)),
redundant(Type,V,Strict)
-> redundancy_vs(Vs)
; redundancy_vs(Vs)
).
% redundant(Type,Var,Strict)
%
% Removes redundant bounds from variable Var with type Type and strictness Strict.
% A redundant bound is one that is satisfied anyway (so adding the inverse of the bound
% makes the system infeasible. This predicate can either fail or succeed but a success
% doesn't necessarily mean a redundant bound.
redundant(t_l(L),X,Strict) :-
get_attr(X,itf,Att),
arg(1,Att,CLP),
detach_bounds(CLP,X), % drop temporarily
% if not redundant, backtracking will restore bound
negate_l(Strict,CLP,L,X),
red_t_l. % negate_l didn't fail, redundant bound
redundant(t_u(U),X,Strict) :-
get_attr(X,itf,Att),
arg(1,Att,CLP),
detach_bounds(CLP,X),
negate_u(Strict,CLP,U,X),
red_t_u.
redundant(t_lu(L,U),X,Strict) :-
strictness_parts(Strict,Sl,Su),
( get_attr(X,itf,Att),
arg(1,Att,CLP),
setarg(2,Att,type(t_u(U))),
setarg(3,Att,strictness(Su)),
negate_l(Strict,CLP,L,X)
-> red_t_l,
( redundant(t_u(U),X,Strict)
-> true
; true
)
; get_attr(X,itf,Att),
arg(1,Att,CLP),
setarg(2,Att,type(t_l(L))),
setarg(3,Att,strictness(Sl)),
negate_u(Strict,CLP,U,X)
-> red_t_u
; true
).
redundant(t_L(L),X,Strict) :-
get_attr(X,itf,Att),
arg(1,Att,CLP),
Bound is -L,
intro_at(CLP,X,Bound,t_none), % drop temporarily
detach_bounds(CLP,X),
negate_l(Strict,CLP,L,X),
red_t_L.
redundant(t_U(U),X,Strict) :-
get_attr(X,itf,Att),
arg(1,Att,CLP),
Bound is -U,
intro_at(CLP,X,Bound,t_none), % drop temporarily
detach_bounds(CLP,X),
negate_u(Strict,CLP,U,X),
red_t_U.
redundant(t_Lu(L,U),X,Strict) :-
strictness_parts(Strict,Sl,Su),
( Bound is -L,
get_attr(X,itf,Att),
arg(1,Att,CLP),
intro_at(CLP,X,Bound,t_u(U)),
get_attr(X,itf,Att2), % changed?
setarg(3,Att2,strictness(Su)),
negate_l(Strict,CLP,L,X)
-> red_t_l,
( redundant(t_u(U),X,Strict)
-> true
; true
)
; get_attr(X,itf,Att),
arg(1,Att,CLP),
setarg(2,Att,type(t_L(L))),
setarg(3,Att,strictness(Sl)),
negate_u(Strict,CLP,U,X)
-> red_t_u
; true
).
redundant(t_lU(L,U),X,Strict) :-
strictness_parts(Strict,Sl,Su),
( get_attr(X,itf,Att),
arg(1,Att,CLP),
setarg(2,Att,type(t_U(U))),
setarg(3,Att,strictness(Su)),
negate_l(Strict,CLP,L,X)
-> red_t_l,
( redundant(t_U(U),X,Strict)
-> true
; true
)
; get_attr(X,itf,Att),
arg(1,Att,CLP),
Bound is -U,
intro_at(CLP,X,Bound,t_l(L)),
get_attr(X,itf,Att2), % changed?
setarg(3,Att2,strictness(Sl)),
negate_u(Strict,CLP,U,X)
-> red_t_u
; true
).
% strictness_parts(Strict,Lower,Upper)
%
% Splits strictness Strict into two parts: one related to the lowerbound and
% one related to the upperbound.
strictness_parts(Strict,Lower,Upper) :-
Lower is Strict /\ 2,
Upper is Strict /\ 1.
% negate_l(Strict,Lowerbound,X)
%
% Fails if X does not necessarily satisfy the lowerbound and strictness
% In other words: if adding the inverse of the lowerbound (X < L or X =< L)
% does not result in a failure, this predicate fails.
negate_l(0,CLP,L,X) :-
CLP:{L > X},
!,
fail.
negate_l(1,CLP,L,X) :-
CLP:{L > X},
!,
fail.
negate_l(2,CLP,L,X) :-
CLP:{L >= X},
!,
fail.
negate_l(3,CLP,L,X) :-
CLP:{L >= X},
!,
fail.
negate_l(_,_,_,_).
% negate_u(Strict,Upperbound,X)
%
% Fails if X does not necessarily satisfy the upperbound and strictness
% In other words: if adding the inverse of the upperbound (X > U or X >= U)
% does not result in a failure, this predicate fails.
negate_u(0,CLP,U,X) :-
CLP:{U < X},
!,
fail.
negate_u(1,CLP,U,X) :-
CLP:{U =< X},
!,
fail.
negate_u(2,CLP,U,X) :-
CLP:{U < X},
!,
fail.
negate_u(3,CLP,U,X) :-
CLP:{U =< X},
!,
fail.
negate_u(_,_,_,_).
% CLP(Q,R)
detach_bounds(clpq,X) :- bv_q:detach_bounds(X).
detach_bounds(clpr,X) :- bv_r:detach_bounds(X).
intro_at(clpq,A,B,C) :- bv_q:intro_at(A,B,C).
intro_at(clpr,A,B,C) :- bv_r:intro_at(A,B,C).
% Profiling: these predicates are called during redundant and can be used
% to count the number of redundant bounds.
red_t_l.
red_t_u.
red_t_L.
red_t_U.

136
GPL/clpqr/clpr.pl
View File

@ -1,136 +0,0 @@
/* $Id: clpr.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2004, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is part of Leslie De Koninck's master thesis, supervised
by Bart Demoen and daily advisor Tom Schrijvers. It is based on CLP(Q,R)
by Christian Holzbaur for SICStus Prolog and distributed under the
license details below with permission from all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(clpr,
[
{}/1,
maximize/1,
minimize/1,
inf/2, inf/4, sup/2, sup/4,
bb_inf/3,
bb_inf/5,
ordering/1,
entailed/1,
clp_type/2,
dump/3%, projecting_assert/1
]).
:- expects_dialect(swi).
%
% Don't report export of private predicates from clpr
%
:- multifile
user:portray_message/2.
:- dynamic
user:portray_message/2.
%
user:portray_message(warning,import(_,_,clpr,private)).
:- load_files(
[
'clpr/bb_r',
'clpr/bv_r',
'clpr/fourmotz_r',
'clpr/ineq_r',
'clpr/itf_r',
'clpr/nf_r',
'clpr/store_r',
'clpqr/class',
'clpqr/dump',
'clpqr/geler',
'clpqr/itf',
'clpqr/ordering',
'clpqr/project',
'clpqr/redund',
library(ugraphs)
],
[
if(not_loaded),
silent(true)
]).
/*******************************
* TOPLEVEL PRINTING *
*******************************/
:- multifile
prolog:message/3.
% prolog:message(query(YesNo)) --> !,
% ['~@'-[chr:print_all_stores]],
% '$messages':prolog_message(query(YesNo)).
prolog:message(query(YesNo,Bindings)) --> !,
{dump_toplevel_bindings(Bindings,Constraints)},
{dump_format(Constraints,Format)},
Format,
'$messages':prolog_message(query(YesNo,Bindings)).
dump_toplevel_bindings(Bindings,Constraints) :-
dump_vars_names(Bindings,[],Vars,Names),
dump(Vars,Names,Constraints).
dump_vars_names([],_,[],[]).
dump_vars_names([Name=Term|Rest],Seen,Vars,Names) :-
( var(Term),
( get_attr(Term,itf,_)
; get_attr(Term,geler,_)
),
\+ memberchk_eq(Term,Seen)
-> Vars = [Term|RVars],
Names = [Name|RNames],
NSeen = [Term|Seen]
; Vars = RVars,
Names = RNames,
Seen = NSeen
),
dump_vars_names(Rest,NSeen,RVars,RNames).
dump_format([],[]).
dump_format([X|Xs],['{~w}'-[X],nl|Rest]) :-
dump_format(Xs,Rest).
memberchk_eq(X,[Y|Ys]) :-
( X == Y
-> true
; memberchk_eq(X,Ys)
).

260
GPL/clpqr/clpr/bb_r.pl
View File

@ -1,260 +0,0 @@
/* $Id: bb_r.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2004, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is part of Leslie De Koninck's master thesis, supervised
by Bart Demoen and daily advisor Tom Schrijvers. It is based on CLP(Q,R)
by Christian Holzbaur for SICStus Prolog and distributed under the
license details below with permission from all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(bb_r,
[
bb_inf/3,
bb_inf/5,
vertex_value/2
]).
:- use_module(bv_r,
[
deref/2,
deref_var/2,
determine_active_dec/1,
inf/2,
iterate_dec/2,
sup/2,
var_with_def_assign/2
]).
:- use_module(nf_r,
[
{}/1,
entailed/1,
nf/2,
nf_constant/2,
repair/2,
wait_linear/3
]).
% bb_inf(Ints,Term,Inf)
%
% Finds the infimum of Term where the variables Ints are to be integers.
% The infimum is stored in Inf.
bb_inf(Is,Term,Inf) :-
bb_inf(Is,Term,Inf,_,0.001).
bb_inf(Is,Term,Inf,Vertex,Eps) :-
nf(Eps,ENf),
nf_constant(ENf,EpsN),
wait_linear(Term,Nf,bb_inf_internal(Is,Nf,EpsN,Inf,Vertex)).
% ---------------------------------------------------------------------
% bb_inf_internal(Is,Lin,Eps,Inf,Vertex)
%
% Finds an infimum Inf for linear expression in normal form Lin, where
% all variables in Is are to be integers. Eps denotes the margin in which
% we accept a number as an integer (to deal with rounding errors etc.).
bb_inf_internal(Is,Lin,Eps,_,_) :-
bb_intern(Is,IsNf,Eps),
nb_delete(prov_opt),
repair(Lin,LinR), % bb_narrow ...
deref(LinR,Lind),
var_with_def_assign(Dep,Lind),
determine_active_dec(Lind),
bb_loop(Dep,IsNf,Eps),
fail.
bb_inf_internal(_,_,_,Inf,Vertex) :-
catch(nb_getval(prov_opt,InfVal-Vertex),_,fail),
{Inf =:= InfVal},
nb_delete(prov_opt).
% bb_loop(Opt,Is,Eps)
%
% Minimizes the value of Opt where variables Is have to be integer values.
% Eps denotes the rounding error that is acceptable. This predicate can be
% backtracked to try different strategies.
bb_loop(Opt,Is,Eps) :-
bb_reoptimize(Opt,Inf),
bb_better_bound(Inf),
vertex_value(Is,Ivs),
( bb_first_nonint(Is,Ivs,Eps,Viol,Floor,Ceiling)
-> bb_branch(Viol,Floor,Ceiling),
bb_loop(Opt,Is,Eps)
; round_values(Ivs,RoundVertex),
nb_setval(prov_opt,Inf-RoundVertex) % new provisional optimum
).
% bb_reoptimize(Obj,Inf)
%
% Minimizes the value of Obj and puts the result in Inf.
% This new minimization is necessary as making a bound integer may yield a
% different optimum. The added inequalities may also have led to binding.
bb_reoptimize(Obj,Inf) :-
var(Obj),
iterate_dec(Obj,Inf).
bb_reoptimize(Obj,Inf) :-
nonvar(Obj),
Inf = Obj.
% bb_better_bound(Inf)
%
% Checks if the new infimum Inf is better than the previous one (if such exists).
bb_better_bound(Inf) :-
catch((nb_getval(prov_opt,Inc-_),Inf - Inc < -1.0e-10),_,true).
% bb_branch(V,U,L)
%
% Stores that V =< U or V >= L, can be used for different strategies within bb_loop/3.
bb_branch(V,U,_) :- {V =< U}.
bb_branch(V,_,L) :- {V >= L}.
% vertex_value(Vars,Values)
%
% Returns in <Values> the current values of the variables in <Vars>.
vertex_value([],[]).
vertex_value([X|Xs],[V|Vs]) :-
rhs_value(X,V),
vertex_value(Xs,Vs).
% rhs_value(X,Value)
%
% Returns in <Value> the current value of variable <X>.
rhs_value(Xn,Value) :-
( nonvar(Xn)
-> Value = Xn
; var(Xn)
-> deref_var(Xn,Xd),
Xd = [I,R|_],
Value is R+I
).
% bb_first_nonint(Ints,Rhss,Eps,Viol,Floor,Ceiling)
%
% Finds the first variable in Ints which doesn't have an active integer bound.
% Rhss contain the Rhs (R + I) values corresponding to the variables.
% The first variable that hasn't got an active integer bound, is returned in
% Viol. The floor and ceiling of its actual bound is returned in Floor and Ceiling.
bb_first_nonint([I|Is],[Rhs|Rhss],Eps,Viol,F,C) :-
( Floor is floor(Rhs+1.0e-10),
Ceiling is ceiling(Rhs-1.0e-10),
Eps - min(Rhs-Floor,Ceiling-Rhs) < -1.0e-10
-> Viol = I,
F = Floor,
C = Ceiling
; bb_first_nonint(Is,Rhss,Eps,Viol,F,C)
).
% round_values([X|Xs],[Xr|Xrs])
%
% Rounds of the values of the first list into the second list.
round_values([],[]).
round_values([X|Xs],[Y|Ys]) :-
Y is round(X),
round_values(Xs,Ys).
% bb_intern([X|Xs],[Xi|Xis],Eps)
%
% Turns the elements of the first list into integers into the second
% list via bb_intern/4.
bb_intern([],[],_).
bb_intern([X|Xs],[Xi|Xis],Eps) :-
nf(X,Xnf),
bb_intern(Xnf,Xi,X,Eps),
bb_intern(Xs,Xis,Eps).
% bb_intern(Nf,X,Term,Eps)
%
% Makes sure that Term which is normalized into Nf, is integer.
% X contains the possibly changed Term. If Term is a variable,
% then its bounds are hightened or lowered to the next integer.
% Otherwise, it is checked it Term is integer.
bb_intern([],X,_,_) :-
!,
X = 0.0.
bb_intern([v(I,[])],X,_,Eps) :-
!,
X = I,
min(I-floor(I+1e-010),ceiling(I-1e-010)-I) - Eps < 1e-010.
bb_intern([v(One,[V^1])],X,_,_) :-
Test is One - 1.0,
Test =< 1e-010,
Test >= -1e-010,
!,
V = X,
bb_narrow_lower(X),
bb_narrow_upper(X).
bb_intern(_,_,Term,_) :-
throw(instantiation_error(bb_inf(Term,_,_),1)).
% bb_narrow_lower(X)
%
% Narrows the lower bound so that it is an integer bound.
% We do this by finding the infimum of X and asserting that X
% is larger than the first integer larger or equal to the infimum
% (second integer if X is to be strict larger than the first integer).
bb_narrow_lower(X) :-
( inf(X,Inf)
-> Bound is ceiling(Inf-1.0e-10),
( entailed(X > Bound)
-> {X >= Bound+1}
; {X >= Bound}
)
; true
).
% bb_narrow_upper(X)
%
% See bb_narrow_lower/1. This predicate handles the upper bound.
bb_narrow_upper(X) :-
( sup(X,Sup)
-> Bound is floor(Sup+1.0e-10),
( entailed(X < Bound)
-> {X =< Bound-1}
; {X =< Bound}
)
; true
).

1786
GPL/clpqr/clpr/bv_r.pl
View File

File diff suppressed because it is too large Load Diff

504
GPL/clpqr/clpr/fourmotz_r.pl
View File

@ -1,504 +0,0 @@
/* $Id: fourmotz_r.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2004, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is part of Leslie De Koninck's master thesis, supervised
by Bart Demoen and daily advisor Tom Schrijvers. It is based on CLP(Q,R)
by Christian Holzbaur for SICStus Prolog and distributed under the
license details below with permission from all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(fourmotz_r,
[
fm_elim/3
]).
:- use_module(bv_r,
[
allvars/2,
basis_add/2,
detach_bounds/1,
pivot/5,
var_with_def_intern/4
]).
:- use_module('../clpqr/class',
[
class_allvars/2
]).
:- use_module('../clpqr/project',
[
drop_dep/1,
drop_dep_one/1,
make_target_indep/2
]).
:- use_module('../clpqr/redund',
[
redundancy_vars/1
]).
:- use_module(store_r,
[
add_linear_11/3,
add_linear_f1/4,
indep/2,
nf_coeff_of/3,
normalize_scalar/2
]).
fm_elim(Vs,Target,Pivots) :-
prefilter(Vs,Vsf),
fm_elim_int(Vsf,Target,Pivots).
% prefilter(Vars,Res)
%
% filters out target variables and variables that do not occur in bounded linear equations.
% Stores that the variables in Res are to be kept independent.
prefilter([],[]).
prefilter([V|Vs],Res) :-
( get_attr(V,itf,Att),
arg(9,Att,n),
occurs(V) % V is a nontarget variable that occurs in a bounded linear equation
-> Res = [V|Tail],
setarg(10,Att,keep_indep),
prefilter(Vs,Tail)
; prefilter(Vs,Res)
).
%
% the target variables are marked with an attribute, and we get a list
% of them as an argument too
%
fm_elim_int([],_,Pivots) :- % done
unkeep(Pivots).
fm_elim_int(Vs,Target,Pivots) :-
Vs = [_|_],
( best(Vs,Best,Rest)
-> occurences(Best,Occ),
elim_min(Best,Occ,Target,Pivots,NewPivots)
; % give up
NewPivots = Pivots,
Rest = []
),
fm_elim_int(Rest,Target,NewPivots).
% best(Vs,Best,Rest)
%
% Finds the variable with the best result (lowest Delta) in fm_cp_filter
% and returns the other variables in Rest.
best(Vs,Best,Rest) :-
findall(Delta-N,fm_cp_filter(Vs,Delta,N),Deltas),
keysort(Deltas,[_-N|_]),
select_nth(Vs,N,Best,Rest).
% fm_cp_filter(Vs,Delta,N)
%
% For an indepenent variable V in Vs, which is the N'th element in Vs,
% find how many inequalities are generated when this variable is eliminated.
% Note that target variables and variables that only occur in unbounded equations
% should have been removed from Vs via prefilter/2
fm_cp_filter(Vs,Delta,N) :-
length(Vs,Len), % Len = number of variables in Vs
mem(Vs,X,Vst), % Selects a variable X in Vs, Vst is the list of elements after X in Vs
get_attr(X,itf,Att),
arg(4,Att,lin(Lin)),
arg(5,Att,order(OrdX)),
arg(9,Att,n), % no target variable
indep(Lin,OrdX), % X is an independent variable
occurences(X,Occ),
Occ = [_|_],
cp_card(Occ,0,Lnew),
length(Occ,Locc),
Delta is Lnew-Locc,
length(Vst,Vstl),
N is Len-Vstl. % X is the Nth element in Vs
% mem(Xs,X,XsT)
%
% If X is a member of Xs, XsT is the list of elements after X in Xs.
mem([X|Xs],X,Xs).
mem([_|Ys],X,Xs) :- mem(Ys,X,Xs).
% select_nth(List,N,Nth,Others)
%
% Selects the N th element of List, stores it in Nth and returns the rest of the list in Others.
select_nth(List,N,Nth,Others) :-
select_nth(List,1,N,Nth,Others).
select_nth([X|Xs],N,N,X,Xs) :- !.
select_nth([Y|Ys],M,N,X,[Y|Xs]) :-
M1 is M+1,
select_nth(Ys,M1,N,X,Xs).
%
% fm_detach + reverse_pivot introduce indep t_none, which
% invalidates the invariants
%
elim_min(V,Occ,Target,Pivots,NewPivots) :-
crossproduct(Occ,New,[]),
activate_crossproduct(New),
reverse_pivot(Pivots),
fm_detach(Occ),
allvars(V,All),
redundancy_vars(All), % only for New \== []
make_target_indep(Target,NewPivots),
drop_dep(All).
%
% restore NF by reverse pivoting
%
reverse_pivot([]).
reverse_pivot([I:D|Ps]) :-
get_attr(D,itf,AttD),
arg(2,AttD,type(Dt)),
setarg(11,AttD,n), % no longer
get_attr(I,itf,AttI),
arg(2,AttI,type(It)),
arg(5,AttI,order(OrdI)),
arg(6,AttI,class(ClI)),
pivot(D,ClI,OrdI,Dt,It),
reverse_pivot(Ps).
% unkeep(Pivots)
%
%
unkeep([]).
unkeep([_:D|Ps]) :-
get_attr(D,itf,Att),
setarg(11,Att,n),
drop_dep_one(D),
unkeep(Ps).
%
% All we drop are bounds
%
fm_detach( []).
fm_detach([V:_|Vs]) :-
detach_bounds(V),
fm_detach(Vs).
% activate_crossproduct(Lst)
%
% For each inequality Lin =< 0 (or Lin < 0) in Lst, a new variable is created:
% Var = Lin and Var =< 0 (or Var < 0). Var is added to the basis.
activate_crossproduct([]).
activate_crossproduct([lez(Strict,Lin)|News]) :-
var_with_def_intern(t_u(0.0),Var,Lin,Strict),
% Var belongs to same class as elements in Lin
basis_add(Var,_),
activate_crossproduct(News).
% ------------------------------------------------------------------------------
% crossproduct(Lst,Res,ResTail)
%
% See crossproduct/4
% This predicate each time puts the next element of Lst as First in crossproduct/4
% and lets the rest be Next.
crossproduct([]) --> [].
crossproduct([A|As]) -->
crossproduct(As,A),
crossproduct(As).
% crossproduct(Next,First,Res,ResTail)
%
% Eliminates a variable in linear equations First + Next and stores the generated
% inequalities in Res.
% Let's say A:K1 = First and B:K2 = first equation in Next.
% A = ... + K1*V + ...
% B = ... + K2*V + ...
% Let K = -K2/K1
% then K*A + B = ... + 0*V + ...
% from the bounds of A and B, via cross_lower/7 and cross_upper/7, new inequalities
% are generated. Then the same is done for B:K2 = next element in Next.
crossproduct([],_) --> [].
crossproduct([B:Kb|Bs],A:Ka) -->
{
get_attr(A,itf,AttA),
arg(2,AttA,type(Ta)),
arg(3,AttA,strictness(Sa)),
arg(4,AttA,lin(LinA)),
get_attr(B,itf,AttB),
arg(2,AttB,type(Tb)),
arg(3,AttB,strictness(Sb)),
arg(4,AttB,lin(LinB)),
K is -Kb/Ka,
add_linear_f1(LinA,K,LinB,Lin) % Lin doesn't contain the target variable anymore
},
( { K > 1.0e-10 } % K > 0: signs were opposite
-> { Strict is Sa \/ Sb },
cross_lower(Ta,Tb,K,Lin,Strict),
cross_upper(Ta,Tb,K,Lin,Strict)
; % La =< A =< Ua -> -Ua =< -A =< -La
{
flip(Ta,Taf),
flip_strict(Sa,Saf),
Strict is Saf \/ Sb
},
cross_lower(Taf,Tb,K,Lin,Strict),
cross_upper(Taf,Tb,K,Lin,Strict)
),
crossproduct(Bs,A:Ka).
% cross_lower(Ta,Tb,K,Lin,Strict,Res,ResTail)
%
% Generates a constraint following from the bounds of A and B.
% When A = LinA and B = LinB then Lin = K*LinA + LinB. Ta is the type
% of A and Tb is the type of B. Strict is the union of the strictness
% of A and B. If K is negative, then Ta should have been flipped (flip/2).
% The idea is that if La =< A =< Ua and Lb =< B =< Ub (=< can also be <)
% then if K is positive, K*La + Lb =< K*A + B =< K*Ua + Ub.
% if K is negative, K*Ua + Lb =< K*A + B =< K*La + Ub.
% This predicate handles the first inequality and adds it to Res in the form
% lez(Sl,Lhs) meaning K*La + Lb - (K*A + B) =< 0 or K*Ua + Lb - (K*A + B) =< 0
% with Sl being the strictness and Lhs the lefthandside of the equation.
% See also cross_upper/7
cross_lower(Ta,Tb,K,Lin,Strict) -->
{
lower(Ta,La),
lower(Tb,Lb),
!,
L is K*La+Lb,
normalize_scalar(L,Ln),
add_linear_f1(Lin,-1.0,Ln,Lhs),
Sl is Strict >> 1 % normalize to upper bound
},
[ lez(Sl,Lhs) ].
cross_lower(_,_,_,_,_) --> [].
% cross_upper(Ta,Tb,K,Lin,Strict,Res,ResTail)
%
% See cross_lower/7
% This predicate handles the second inequality:
% -(K*Ua + Ub) + K*A + B =< 0 or -(K*La + Ub) + K*A + B =< 0
cross_upper(Ta,Tb,K,Lin,Strict) -->
{
upper(Ta,Ua),
upper(Tb,Ub),
!,
U is -(K*Ua+Ub),
normalize_scalar(U,Un),
add_linear_11(Un,Lin,Lhs),
Su is Strict /\ 1 % normalize to upper bound
},
[ lez(Su,Lhs) ].
cross_upper(_,_,_,_,_) --> [].
% lower(Type,Lowerbound)
%
% Returns the lowerbound of type Type if it has one.
% E.g. if type = t_l(L) then Lowerbound is L,
% if type = t_lU(L,U) then Lowerbound is L,
% if type = t_u(U) then fails
lower(t_l(L),L).
lower(t_lu(L,_),L).
lower(t_L(L),L).
lower(t_Lu(L,_),L).
lower(t_lU(L,_),L).
% upper(Type,Upperbound)
%
% Returns the upperbound of type Type if it has one.
% See lower/2
upper(t_u(U),U).
upper(t_lu(_,U),U).
upper(t_U(U),U).
upper(t_Lu(_,U),U).
upper(t_lU(_,U),U).
% flip(Type,FlippedType)
%
% Flips the lower and upperbound, so the old lowerbound becomes the new upperbound and
% vice versa.
flip(t_l(X),t_u(X)).
flip(t_u(X),t_l(X)).
flip(t_lu(X,Y),t_lu(Y,X)).
flip(t_L(X),t_u(X)).
flip(t_U(X),t_l(X)).
flip(t_lU(X,Y),t_lu(Y,X)).
flip(t_Lu(X,Y),t_lu(Y,X)).
% flip_strict(Strict,FlippedStrict)
%
% Does what flip/2 does, but for the strictness.
flip_strict(0,0).
flip_strict(1,2).
flip_strict(2,1).
flip_strict(3,3).
% cp_card(Lst,CountIn,CountOut)
%
% Counts the number of bounds that may generate an inequality in
% crossproduct/3
cp_card([],Ci,Ci).
cp_card([A|As],Ci,Co) :-
cp_card(As,A,Ci,Cii),
cp_card(As,Cii,Co).
% cp_card(Next,First,CountIn,CountOut)
%
% Counts the number of bounds that may generate an inequality in
% crossproduct/4.
cp_card([],_,Ci,Ci).
cp_card([B:Kb|Bs],A:Ka,Ci,Co) :-
get_attr(A,itf,AttA),
arg(2,AttA,type(Ta)),
get_attr(B,itf,AttB),
arg(2,AttB,type(Tb)),
K is -Kb/Ka,
( K > 1.0e-10 % K > 0: signs were opposite
-> cp_card_lower(Ta,Tb,Ci,Cii),
cp_card_upper(Ta,Tb,Cii,Ciii)
; flip(Ta,Taf),
cp_card_lower(Taf,Tb,Ci,Cii),
cp_card_upper(Taf,Tb,Cii,Ciii)
),
cp_card(Bs,A:Ka,Ciii,Co).
% cp_card_lower(TypeA,TypeB,SIn,SOut)
%
% SOut = SIn + 1 if both TypeA and TypeB have a lowerbound.
cp_card_lower(Ta,Tb,Si,So) :-
lower(Ta,_),
lower(Tb,_),
!,
So is Si+1.
cp_card_lower(_,_,Si,Si).
% cp_card_upper(TypeA,TypeB,SIn,SOut)
%
% SOut = SIn + 1 if both TypeA and TypeB have an upperbound.
cp_card_upper(Ta,Tb,Si,So) :-
upper(Ta,_),
upper(Tb,_),
!,
So is Si+1.
cp_card_upper(_,_,Si,Si).
% ------------------------------------------------------------------------------
% occurences(V,Occ)
%
% Returns in Occ the occurrences of variable V in the linear equations of dependent variables
% with bound =\= t_none in the form of D:K where D is a dependent variable and K is the scalar
% of V in the linear equation of D.
occurences(V,Occ) :-
get_attr(V,itf,Att),
arg(5,Att,order(OrdV)),
arg(6,Att,class(C)),
class_allvars(C,All),
occurences(All,OrdV,Occ).
% occurences(De,OrdV,Occ)
%
% Returns in Occ the occurrences of variable V with order OrdV in the linear equations of
% dependent variables De with bound =\= t_none in the form of D:K where D is a dependent
% variable and K is the scalar of V in the linear equation of D.
occurences(De,_,[]) :-
var(De),
!.
occurences([D|De],OrdV,Occ) :-
( get_attr(D,itf,Att),
arg(2,Att,type(Type)),
arg(4,Att,lin(Lin)),
occ_type_filter(Type),
nf_coeff_of(Lin,OrdV,K)
-> Occ = [D:K|Occt],
occurences(De,OrdV,Occt)
; occurences(De,OrdV,Occ)
).
% occ_type_filter(Type)
%
% Succeeds when Type is any other type than t_none. Is used in occurences/3 and occurs/2
occ_type_filter(t_l(_)).
occ_type_filter(t_u(_)).
occ_type_filter(t_lu(_,_)).
occ_type_filter(t_L(_)).
occ_type_filter(t_U(_)).
occ_type_filter(t_lU(_,_)).
occ_type_filter(t_Lu(_,_)).
% occurs(V)
%
% Checks whether variable V occurs in a linear equation of a dependent variable with a bound
% =\= t_none.
occurs(V) :-
get_attr(V,itf,Att),
arg(5,Att,order(OrdV)),
arg(6,Att,class(C)),
class_allvars(C,All),
occurs(All,OrdV).
% occurs(De,OrdV)
%
% Checks whether variable V with order OrdV occurs in a linear equation of any dependent variable
% in De with a bound =\= t_none.
occurs(De,_) :-
var(De),
!,
fail.
occurs([D|De],OrdV) :-
( get_attr(D,itf,Att),
arg(2,Att,type(Type)),
arg(4,Att,lin(Lin)),
occ_type_filter(Type),
nf_coeff_of(Lin,OrdV,_)
-> true
; occurs(De,OrdV)
).

1384
GPL/clpqr/clpr/ineq_r.pl
View File

File diff suppressed because it is too large Load Diff

227
GPL/clpqr/clpr/itf_r.pl
View File

@ -1,227 +0,0 @@
/*
Part of CLP(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2004, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is part of Leslie De Koninck's master thesis, supervised
by Bart Demoen and daily advisor Tom Schrijvers. It is based on CLP(Q,R)
by Christian Holzbaur for SICStus Prolog and distributed under the
license details below with permission from all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(itf_r,
[
do_checks/8
]).
:- use_module(bv_r,
[
deref/2,
detach_bounds_vlv/5,
solve/1,
solve_ord_x/3
]).
:- use_module(nf_r,
[
nf/2
]).
:- use_module(store_r,
[
add_linear_11/3,
indep/2,
nf_coeff_of/3
]).
:- use_module('../clpqr/class',
[
class_drop/2
]).
do_checks(Y,Ty,St,Li,Or,Cl,No,Later) :-
numbers_only(Y),
verify_nonzero(No,Y),
verify_type(Ty,St,Y,Later,[]),
verify_lin(Or,Cl,Li,Y),
maplist(call,Later).
numbers_only(Y) :-
( var(Y)
; integer(Y)
; float(Y)
; throw(type_error(_X = Y,2,'a real number',Y))
),
!.
% verify_nonzero(Nonzero,Y)
%
% if Nonzero = nonzero, then verify that Y is not zero
% (if possible, otherwise set Y to be nonzero)
verify_nonzero(nonzero,Y) :-
( var(Y)
-> ( get_attr(Y,itf,Att)
-> setarg(8,Att,nonzero)
; put_attr(Y,itf,t(clpr,n,n,n,n,n,n,nonzero,n,n,n))
)
; ( Y < -1.0e-10
-> true
; Y > 1.0e-10
)
).
verify_nonzero(n,_). % X is not nonzero
% verify_type(type(Type),strictness(Strict),Y,[OL|OLT],OLT)
%
% if possible verifies whether Y satisfies the type and strictness of X
% if not possible to verify, then returns the constraints that follow from
% the type and strictness
verify_type(type(Type),strictness(Strict),Y) -->
verify_type2(Y,Type,Strict).
verify_type(n,n,_) --> [].
verify_type2(Y,TypeX,StrictX) -->
{var(Y)},
!,
verify_type_var(TypeX,Y,StrictX).
verify_type2(Y,TypeX,StrictX) -->
{verify_type_nonvar(TypeX,Y,StrictX)}.
% verify_type_nonvar(Type,Nonvar,Strictness)
%
% verifies whether the type and strictness are satisfied with the Nonvar
verify_type_nonvar(t_none,_,_).
verify_type_nonvar(t_l(L),Value,S) :- ilb(S,L,Value).
verify_type_nonvar(t_u(U),Value,S) :- iub(S,U,Value).
verify_type_nonvar(t_lu(L,U),Value,S) :-
ilb(S,L,Value),
iub(S,U,Value).
verify_type_nonvar(t_L(L),Value,S) :- ilb(S,L,Value).
verify_type_nonvar(t_U(U),Value,S) :- iub(S,U,Value).
verify_type_nonvar(t_Lu(L,U),Value,S) :-
ilb(S,L,Value),
iub(S,U,Value).
verify_type_nonvar(t_lU(L,U),Value,S) :-
ilb(S,L,Value),
iub(S,U,Value).
% ilb(Strict,Lower,Value) & iub(Strict,Upper,Value)
%
% check whether Value is satisfiable with the given lower/upper bound and
% strictness.
% strictness is encoded as follows:
% 2 = strict lower bound
% 1 = strict upper bound
% 3 = strict lower and upper bound
% 0 = no strict bounds
ilb(S,L,V) :-
S /\ 2 =:= 0,
!,
L - V < 1.0e-10. % non-strict
ilb(_,L,V) :- L - V < -1.0e-10. % strict
iub(S,U,V) :-
S /\ 1 =:= 0,
!,
V - U < 1.0e-10. % non-strict
iub(_,U,V) :- V - U < -1.0e-10. % strict
%
% 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(Type,Var,Strictness,[OutList|OutListTail],OutListTail)
%
% returns the inequalities following from a type and strictness satisfaction
% test with Var
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(Strict,Lower,Value,[OL|OLT],OLT) and lub(Strict,Upper,Value,[OL|OLT],OLT)
%
% returns the inequalities following from the lower and upper bounds and the
% strictness see also lb and ub
llb(S,L,V) -->
{S /\ 2 =:= 0},
!,
[clpr:{L =< V}].
llb(_,L,V) --> [clpr:{L < V}].
lub(S,U,V) -->
{S /\ 1 =:= 0},
!,
[clpr:{V =< U}].
lub(_,U,V) --> [clpr:{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(order(OrdX),class(Class),lin(LinX),Y) :-
!,
( indep(LinX,OrdX)
-> detach_bounds_vlv(OrdX,LinX,Class,Y,NewLinX),
% if there were bounds, they are requeued already
class_drop(Class,Y),
nf(-Y,NfY),
deref(NfY,LinY),
add_linear_11(NewLinX,LinY,Lind),
( nf_coeff_of(Lind,OrdX,_)
-> % X is element of Lind
solve_ord_x(Lind,OrdX,Class)
; solve(Lind) % X is gone, can safely solve Lind
)
; class_drop(Class,Y),
nf(-Y,NfY),
deref(NfY,LinY),
add_linear_11(LinX,LinY,Lind),
solve(Lind)
).
verify_lin(_,_,_,_).

1146
GPL/clpqr/clpr/nf_r.pl
View File

File diff suppressed because it is too large Load Diff

427
GPL/clpqr/clpr/store_r.pl
View File

@ -1,427 +0,0 @@
/* $Id: store_r.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CLP(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Leslie.DeKoninck@cs.kuleuven.be
WWW: http://www.swi-prolog.org
http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
Copyright (C): 2004, K.U. Leuven and
1992-1995, Austrian Research Institute for
Artificial Intelligence (OFAI),
Vienna, Austria
This software is part of Leslie De Koninck's master thesis, supervised
by Bart Demoen and daily advisor Tom Schrijvers. It is based on CLP(Q,R)
by Christian Holzbaur for SICStus Prolog and distributed under the
license details below with permission from all mentioned authors.
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
As a special exception, if you link this library with other files,
compiled with a Free Software compiler, to produce an executable, this
library does not by itself cause the resulting executable to be covered
by the GNU General Public License. This exception does not however
invalidate any other reasons why the executable file might be covered by
the GNU General Public License.
*/
:- module(store_r,
[
add_linear_11/3,
add_linear_f1/4,
add_linear_ff/5,
normalize_scalar/2,
delete_factor/4,
mult_linear_factor/3,
nf_rhs_x/4,
indep/2,
isolate/3,
nf_substitute/4,
mult_hom/3,
nf2sum/3,
nf_coeff_of/3,
renormalize/2
]).
% normalize_scalar(S,[N,Z])
%
% Transforms a scalar S into a linear expression [S,0]
normalize_scalar(S,[S,0.0]).
% renormalize(List,Lin)
%
% Renormalizes the not normalized linear expression in List into
% a normalized one. It does so to take care of unifications.
% (e.g. when a variable X is bound to a constant, the constant is added to
% the constant part of the linear expression; when a variable X is bound to
% another variable Y, the scalars of both are added)
renormalize([I,R|Hom],Lin) :-
length(Hom,Len),
renormalize_log(Len,Hom,[],Lin0),
add_linear_11([I,R],Lin0,Lin).
% renormalize_log(Len,Hom,HomTail,Lin)
%
% Logarithmically renormalizes the homogene part of a not normalized
% linear expression. See also renormalize/2.
renormalize_log(1,[Term|Xs],Xs,Lin) :-
!,
Term = l(X*_,_),
renormalize_log_one(X,Term,Lin).
renormalize_log(2,[A,B|Xs],Xs,Lin) :-
!,
A = l(X*_,_),
B = l(Y*_,_),
renormalize_log_one(X,A,LinA),
renormalize_log_one(Y,B,LinB),
add_linear_11(LinA,LinB,Lin).
renormalize_log(N,L0,L2,Lin) :-
P is N>>1,
Q is N-P,
renormalize_log(P,L0,L1,Lp),
renormalize_log(Q,L1,L2,Lq),
add_linear_11(Lp,Lq,Lin).
% renormalize_log_one(X,Term,Res)
%
% Renormalizes a term in X: if X is a nonvar, the term becomes a scalar.
renormalize_log_one(X,Term,Res) :-
var(X),
Term = l(X*K,_),
get_attr(X,itf,Att),
arg(5,Att,order(OrdX)), % Order might have changed
Res = [0.0,0.0,l(X*K,OrdX)].
renormalize_log_one(X,Term,Res) :-
nonvar(X),
Term = l(X*K,_),
Xk is X*K,
normalize_scalar(Xk,Res).
% ----------------------------- sparse vector stuff ---------------------------- %
% add_linear_ff(LinA,Ka,LinB,Kb,LinC)
%
% Linear expression LinC is the result of the addition of the 2 linear expressions
% LinA and LinB, each one multiplied by a scalar (Ka for LinA and Kb for LinB).
add_linear_ff(LinA,Ka,LinB,Kb,LinC) :-
LinA = [Ia,Ra|Ha],
LinB = [Ib,Rb|Hb],
LinC = [Ic,Rc|Hc],
Ic is Ia*Ka+Ib*Kb,
Rc is Ra*Ka+Rb*Kb,
add_linear_ffh(Ha,Ka,Hb,Kb,Hc).
% add_linear_ffh(Ha,Ka,Hb,Kb,Hc)
%
% Homogene part Hc is the result of the addition of the 2 homogene parts Ha and Hb,
% each one multiplied by a scalar (Ka for Ha and Kb for Hb)
add_linear_ffh([],_,Ys,Kb,Zs) :- mult_hom(Ys,Kb,Zs).
add_linear_ffh([l(X*Kx,OrdX)|Xs],Ka,Ys,Kb,Zs) :-
add_linear_ffh(Ys,X,Kx,OrdX,Xs,Zs,Ka,Kb).
% add_linear_ffh(Ys,X,Kx,OrdX,Xs,Zs,Ka,Kb)
%
% Homogene part Zs is the result of the addition of the 2 homogene parts Ys and
% [l(X*Kx,OrdX)|Xs], each one multiplied by a scalar (Ka for [l(X*Kx,OrdX)|Xs] and Kb for Ys)
add_linear_ffh([],X,Kx,OrdX,Xs,Zs,Ka,_) :- mult_hom([l(X*Kx,OrdX)|Xs],Ka,Zs).
add_linear_ffh([l(Y*Ky,OrdY)|Ys],X,Kx,OrdX,Xs,Zs,Ka,Kb) :-
compare(Rel,OrdX,OrdY),
( Rel = (=)
-> Kz is Kx*Ka+Ky*Kb,
( % Kz =:= 0
Kz =< 1.0e-10,
Kz >= -1.0e-10
-> add_linear_ffh(Xs,Ka,Ys,Kb,Zs)
; Zs = [l(X*Kz,OrdX)|Ztail],
add_linear_ffh(Xs,Ka,Ys,Kb,Ztail)
)
; Rel = (<)
-> Zs = [l(X*Kz,OrdX)|Ztail],
Kz is Kx*Ka,
add_linear_ffh(Xs,Y,Ky,OrdY,Ys,Ztail,Kb,Ka)
; Rel = (>)
-> Zs = [l(Y*Kz,OrdY)|Ztail],
Kz is Ky*Kb,
add_linear_ffh(Ys,X,Kx,OrdX,Xs,Ztail,Ka,Kb)
).
% add_linear_f1(LinA,Ka,LinB,LinC)
%
% special case of add_linear_ff with Kb = 1
add_linear_f1(LinA,Ka,LinB,LinC) :-
LinA = [Ia,Ra|Ha],
LinB = [Ib,Rb|Hb],
LinC = [Ic,Rc|Hc],
Ic is Ia*Ka+Ib,
Rc is Ra*Ka+Rb,
add_linear_f1h(Ha,Ka,Hb,Hc).
% add_linear_f1h(Ha,Ka,Hb,Hc)
%
% special case of add_linear_ffh/5 with Kb = 1
add_linear_f1h([],_,Ys,Ys).
add_linear_f1h([l(X*Kx,OrdX)|Xs],Ka,Ys,Zs) :-
add_linear_f1h(Ys,X,Kx,OrdX,Xs,Zs,Ka).
% add_linear_f1h(Ys,X,Kx,OrdX,Xs,Zs,Ka)
%
% special case of add_linear_ffh/8 with Kb = 1
add_linear_f1h([],X,Kx,OrdX,Xs,Zs,Ka) :- mult_hom([l(X*Kx,OrdX)|Xs],Ka,Zs).
add_linear_f1h([l(Y*Ky,OrdY)|Ys],X,Kx,OrdX,Xs,Zs,Ka) :-
compare(Rel,OrdX,OrdY),
( Rel = (=)
-> Kz is Kx*Ka+Ky,
( % Kz =:= 0.0
Kz =< 1.0e-10,
Kz >= -1.0e-10
-> add_linear_f1h(Xs,Ka,Ys,Zs)
; Zs = [l(X*Kz,OrdX)|Ztail],
add_linear_f1h(Xs,Ka,Ys,Ztail)
)
; Rel = (<)
-> Zs = [l(X*Kz,OrdX)|Ztail],
Kz is Kx*Ka,
add_linear_f1h(Xs,Ka,[l(Y*Ky,OrdY)|Ys],Ztail)
; Rel = (>)
-> Zs = [l(Y*Ky,OrdY)|Ztail],
add_linear_f1h(Ys,X,Kx,OrdX,Xs,Ztail,Ka)
).
% add_linear_11(LinA,LinB,LinC)
%
% special case of add_linear_ff with Ka = 1 and Kb = 1
add_linear_11(LinA,LinB,LinC) :-
LinA = [Ia,Ra|Ha],
LinB = [Ib,Rb|Hb],
LinC = [Ic,Rc|Hc],
Ic is Ia+Ib,
Rc is Ra+Rb,
add_linear_11h(Ha,Hb,Hc).
% add_linear_11h(Ha,Hb,Hc)
%
% special case of add_linear_ffh/5 with Ka = 1 and Kb = 1
add_linear_11h([],Ys,Ys).
add_linear_11h([l(X*Kx,OrdX)|Xs],Ys,Zs) :-
add_linear_11h(Ys,X,Kx,OrdX,Xs,Zs).
% add_linear_11h(Ys,X,Kx,OrdX,Xs,Zs)
%
% special case of add_linear_ffh/8 with Ka = 1 and Kb = 1
add_linear_11h([],X,Kx,OrdX,Xs,[l(X*Kx,OrdX)|Xs]).
add_linear_11h([l(Y*Ky,OrdY)|Ys],X,Kx,OrdX,Xs,Zs) :-
compare(Rel,OrdX,OrdY),
( Rel = (=)
-> Kz is Kx+Ky,
( % Kz =:= 0.0
Kz =< 1.0e-10,
Kz >= -1.0e-10
-> add_linear_11h(Xs,Ys,Zs)
; Zs = [l(X*Kz,OrdX)|Ztail],
add_linear_11h(Xs,Ys,Ztail)
)
; Rel = (<)
-> Zs = [l(X*Kx,OrdX)|Ztail],
add_linear_11h(Xs,Y,Ky,OrdY,Ys,Ztail)
; Rel = (>)
-> Zs = [l(Y*Ky,OrdY)|Ztail],
add_linear_11h(Ys,X,Kx,OrdX,Xs,Ztail)
).
% mult_linear_factor(Lin,K,Res)
%
% Linear expression Res is the result of multiplication of linear
% expression Lin by scalar K
mult_linear_factor(Lin,K,Mult) :-
TestK is K - 1.0, % K =:= 1
TestK =< 1.0e-10,
TestK >= -1.0e-10, % avoid copy
!,
Mult = Lin.
mult_linear_factor(Lin,K,Res) :-
Lin = [I,R|Hom],
Res = [Ik,Rk|Mult],
Ik is I*K,
Rk is R*K,
mult_hom(Hom,K,Mult).
% mult_hom(Hom,K,Res)
%
% Homogene part Res is the result of multiplication of homogene part
% Hom by scalar K
mult_hom([],_,[]).
mult_hom([l(A*Fa,OrdA)|As],F,[l(A*Fan,OrdA)|Afs]) :-
Fan is F*Fa,
mult_hom(As,F,Afs).
% nf_substitute(Ord,Def,Lin,Res)
%
% Linear expression Res is the result of substitution of Var in
% linear expression Lin, by its definition in the form of linear
% expression Def
nf_substitute(OrdV,LinV,LinX,LinX1) :-
delete_factor(OrdV,LinX,LinW,K),
add_linear_f1(LinV,K,LinW,LinX1).
% delete_factor(Ord,Lin,Res,Coeff)
%
% Linear expression Res is the result of the deletion of the term
% Var*Coeff where Var has ordering Ord from linear expression Lin
delete_factor(OrdV,Lin,Res,Coeff) :-
Lin = [I,R|Hom],
Res = [I,R|Hdel],
delete_factor_hom(OrdV,Hom,Hdel,Coeff).
% delete_factor_hom(Ord,Hom,Res,Coeff)
%
% Homogene part Res is the result of the deletion of the term
% Var*Coeff from homogene part Hom
delete_factor_hom(VOrd,[Car|Cdr],RCdr,RKoeff) :-
Car = l(_*Koeff,Ord),
compare(Rel,VOrd,Ord),
( Rel= (=)
-> RCdr = Cdr,
RKoeff=Koeff
; Rel= (>)
-> RCdr = [Car|RCdr1],
delete_factor_hom(VOrd,Cdr,RCdr1,RKoeff)
).
% nf_coeff_of(Lin,OrdX,Coeff)
%
% Linear expression Lin contains the term l(X*Coeff,OrdX)
nf_coeff_of([_,_|Hom],VOrd,Coeff) :-
nf_coeff_hom(Hom,VOrd,Coeff).
% nf_coeff_hom(Lin,OrdX,Coeff)
%
% Linear expression Lin contains the term l(X*Coeff,OrdX) where the
% order attribute of X = OrdX
nf_coeff_hom([l(_*K,OVar)|Vs],OVid,Coeff) :-
compare(Rel,OVid,OVar),
( Rel = (=)
-> Coeff = K
; Rel = (>)
-> nf_coeff_hom(Vs,OVid,Coeff)
).
% nf_rhs_x(Lin,OrdX,Rhs,K)
%
% Rhs = R + I where Lin = [I,R|Hom] and l(X*K,OrdX) is a term of Hom
nf_rhs_x(Lin,OrdX,Rhs,K) :-
Lin = [I,R|Tail],
nf_coeff_hom(Tail,OrdX,K),
Rhs is R+I. % late because X may not occur in H
% isolate(OrdN,Lin,Lin1)
%
% Linear expression Lin1 is the result of the transformation of linear expression
% Lin = 0 which contains the term l(New*K,OrdN) into an equivalent expression Lin1 = New.
isolate(OrdN,Lin,Lin1) :-
delete_factor(OrdN,Lin,Lin0,Coeff),
K is -1.0/Coeff,
mult_linear_factor(Lin0,K,Lin1).
% indep(Lin,OrdX)
%
% succeeds if Lin = [0,_|[l(X*1,OrdX)]]
indep(Lin,OrdX) :-
Lin = [I,_|[l(_*K,OrdY)]],
OrdX == OrdY,
% K =:= 1.0
TestK is K - 1.0,
TestK =< 1.0e-10,
TestK >= -1.0e-10,
% I =:= 0
I =< 1.0e-10,
I >= -1.0e-10.
% nf2sum(Lin,Sofar,Term)
%
% Transforms a linear expression into a sum
% (e.g. the expression [5,_,[l(X*2,OrdX),l(Y*-1,OrdY)]] gets transformed into 5 + 2*X - Y)
nf2sum([],I,I).
nf2sum([X|Xs],I,Sum) :-
( % I =:= 0.0
I =< 1.0e-10,
I >= -1.0e-10
-> X = l(Var*K,_),
( % K =:= 1.0
TestK is K - 1.0,
TestK =< 1.0e-10,
TestK >= -1.0e-10
-> hom2sum(Xs,Var,Sum)
; % K =:= -1.0
TestK is K + 1.0,
TestK =< 1.0e-10,
TestK >= -1.0e-10
-> hom2sum(Xs,-Var,Sum)
; hom2sum(Xs,K*Var,Sum)
)
; hom2sum([X|Xs],I,Sum)
).
% hom2sum(Hom,Sofar,Term)
%
% Transforms a linear expression into a sum
% this predicate handles all but the first term
% (the first term does not need a concatenation symbol + or -)
% see also nf2sum/3
hom2sum([],Term,Term).
hom2sum([l(Var*K,_)|Cs],Sofar,Term) :-
( % K =:= 1.0
TestK is K - 1.0,
TestK =< 1.0e-10,
TestK >= -1.0e-10
-> Next = Sofar + Var
; % K =:= -1.0
TestK is K + 1.0,
TestK =< 1.0e-10,
TestK >= -1.0e-10
-> Next = Sofar - Var
; % K < 0.0
K < -1.0e-10
-> Ka is -K,
Next = Sofar - Ka*Var
; Next = Sofar + K*Var
),
hom2sum(Cs,Next,Term).

1
packages/chr Submodule

@ -0,0 +1 @@
Subproject commit cba31e06301d475e572a2f377061c7b5014b4254

1
packages/clpqr Submodule

@ -0,0 +1 @@
Subproject commit 3cda12359a93d7d9e337cc564b7bfacf40fc8cb5

1
packages/jpl Submodule

@ -0,0 +1 @@
Subproject commit 8843002483df3078583ca8495630a1b864a7999f