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

update to CLP(QR). Note that CLP(Q) is still unsupported.

Browse Source 
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@2145 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
This commit is contained in:
vsc 2008-03-13 17:16:47 +00:00
parent e59b7fb409
commit 0e45f242d4
43 changed files with 10850 additions and 6599 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
C/init.c
View File

@ -406,6 +406,7 @@ static Opdef Ops[] = {
{"+", fx, 500},
{"-", fx, 500},
{"\\", fx, 500},
{"rdiv", yfx, 400},
{"*", yfx, 400},
{"/", yfx, 400},
{"<<", yfx, 400},

34
GPL/clpqr/ChangeLog Normal file
View File

@ -0,0 +1,34 @@
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.

49
LGPL/clpr/Makefile.in → GPL/clpqr/Makefile.in
View File

@ -16,29 +16,64 @@ 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)/arith_r.pl $(CLPRSOURCEDIR)/bb.pl $(CLPRSOURCEDIR)/bv.pl $(CLPRSOURCEDIR)/class.pl $(CLPRSOURCEDIR)/dump.pl $(CLPRSOURCEDIR)/fourmotz.pl \
$(CLPRSOURCEDIR)/geler.pl $(CLPRSOURCEDIR)/ineq.pl $(CLPRSOURCEDIR)/itf3.pl $(CLPRSOURCEDIR)/nf.pl $(CLPRSOURCEDIR)/nfr.pl $(CLPRSOURCEDIR)/ordering.pl \
$(CLPRSOURCEDIR)/project.pl $(CLPRSOURCEDIR)/redund.pl $(CLPRSOURCEDIR)/store.pl $(CLPRSOURCEDIR)/ugraphs.pl
LIBPL= $(srcdir)/clpr.yap $(srcdir)/clpr.pl
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)
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) $(srcdir)/README $(DESTDIR)$(CLPRDIR)
$(INSTALL_DATA) $(CLPQPRIV) $(DESTDIR)$(CLPQDIR)
$(INSTALL_DATA) $(srcdir)/README $(DESTDIR)$(CLPQRDIR)
rpm-install: install
@ -52,7 +87,7 @@ install-examples::
uninstall:
(cd $(CLPDIR) && rm -f $(LIBPL))
rm -rf $(CLPRDIR)
rm -rf $(CLPQRDIR)
check::
# $(PL) -q -f clpr_test.pl -g test,halt -t 'halt(1)'

9
LGPL/clpr/README → GPL/clpqr/README
View File

@ -1,10 +1,7 @@
SWI-Prolog CLP(R)
-----------------
SWI-Prolog CLP(Q,R)
-------------------
Author: Leslie De Koninck, K.U. Leuven as part of a thesis with supervisor
Bart Demoen and daily advisor Tom Schrijvers. Integrated into
the main SWI-Prolog source by Jan Wielemaker.
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

135
GPL/clpqr/clpq.pl Normal file
View File

@ -0,0 +1,135 @@
/*
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 Normal file
View File

@ -0,0 +1,240 @@
/* $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 Normal file
View File

File diff suppressed because it is too large Load Diff

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

@ -0,0 +1,503 @@
/* $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 Normal file
View File

File diff suppressed because it is too large Load Diff

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

@ -0,0 +1,222 @@
/*
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 Normal file
View File

File diff suppressed because it is too large Load Diff

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

@ -0,0 +1,398 @@
/* $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).

103
LGPL/clpr/clpr/class.pl → GPL/clpqr/clpqr/class.pl
View File

@ -1,20 +1,19 @@
/* $Id: class.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/* $Id: class.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.be
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
Copyright (C): 2006, 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 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
@ -38,69 +37,74 @@
the GNU General Public License.
*/
:- module(class,
[
class_allvars/2,
class_new/4,
class_drop/2,
class_basis/2,
class_basis_add/3,
class_basis_drop/2,
class_basis_pivot/3,
class_get_prio/2,
class_put_prio/2,
ordering/1,
arrangement/2
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
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(La,Lat,ABasis,PrioA),Y) :-
attr_unify_hook(class(CLP,La,Lat,ABasis,PrioA),Y) :-
!,
var(Y),
get_attr(Y,class,class(Lb,Lbt,BBasis,PrioB)),
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(La,Lbt,CBasis,PrioC)).
put_attr(Y,class,class(CLP,La,Lbt,CBasis,PrioC)).
attr_unify_hook(_,_).
class_new(Class,All,AllT,Basis) :-
put_attr(Su,class,class(All,AllT,Basis,[])),
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_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(All,AllT,Basis,_)),
put_attr(Class,class,class(All,AllT,Basis,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(Allvars,Tail,Basis,Priority)),
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(NewAllvars,Tail,NewBasis,Priority)).
put_attr(Class,class,class(CLP,NewAllvars,Tail,NewBasis,Priority)).
class_allvars(Class,All) :- get_attr(Class,class,class(All,_,_,_)).
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(Class,Basis) :- get_attr(Class,class,class(_,_,_,Basis,_)).
% class_basis_add(Class,X,NewBasis)
%
@ -108,19 +112,19 @@ class_basis(Class,Basis) :- get_attr(Class,class,class(_,_,Basis,_)).
class_basis_add(Class,X,NewBasis) :-
NewBasis = [X|Basis],
get_attr(Class,class,class(All,AllT,Basis,Priority)),
put_attr(Class,class,class(All,AllT,NewBasis,Priority)).
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(All,AllT,Basis0,Priority)),
get_attr(Class,class,class(CLP,All,AllT,Basis0,Priority)),
delete_first(Basis0,X,Basis),
Basis0 \== Basis, % anything deleted ?
!,
put_attr(Class,class,class(All,AllT,Basis,Priority)).
put_attr(Class,class,class(CLP,All,AllT,Basis,Priority)).
class_basis_drop(_,_).
% class_basis_pivot(Class,Enter,Leave)
@ -128,9 +132,9 @@ class_basis_drop(_,_).
% 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(All,AllT,Basis0,Priority)),
get_attr(Class,class,class(CLP,All,AllT,Basis0,Priority)),
delete_first(Basis0,Leave,Basis1),
put_attr(Class,class,class(All,AllT,[Enter|Basis1],Priority)).
put_attr(Class,class,class(CLP,All,AllT,[Enter|Basis1],Priority)).
% delete_first(Old,Element,New)
%
@ -144,11 +148,8 @@ delete_first(L,_,Res) :-
Res = L.
delete_first([],_,[]).
delete_first([Y|Ys],X,Res) :-
(
X==Y ->
Res = Ys
;
Res = [Y|Tail],
delete_first( Ys, X, Tail)
( X==Y
-> Res = Ys
; Res = [Y|Tail],
delete_first(Ys,X,Tail)
).

644
LGPL/clpr/clpr/dump.pl → GPL/clpqr/clpqr/dump.pl
View File

@ -1,341 +1,303 @@
/* $Id: dump.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.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(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(itf3,
[
dump_linear/4,
dump_nonzero/4
]).
:- use_module(project,
[
project_attributes/2
]).
:- use_module(ordering,
[ ordering/1
]).
:- dynamic blackboard_copy/1. % replacement of bb_put and bb_delete by dynamic predicate
this_linear_solver(clpr).
% 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
raise_exception(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
(
blackboard_copy(_) ->
retract(blackboard_copy(_)),
assert(blackboard_copy(NewVars/Copy))
;
assert(blackboard_copy(NewVars/Copy))
),
fail % undo projection
;
retract(blackboard_copy(NewVars/Constraints)) % garbage collect
).
:- 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 []
this_linear_solver(Sm), % 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
(
blackboard_copy(_) ->
retract(blackboard_copy(_)),
assert(blackboard_copy(TmpCopy))
;
assert(blackboard_copy(TmpCopy))
),
fail % undo projection
;
retract(blackboard_copy(Copy/Constraints)) % garbage collect
).
% 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 predicate 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,itf3,(_,_,_,_,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
this_linear_solver(Solver),
nonlin_strip(Gs,Solver,Gss).
% nonlin_strip(Gs,Solver,Res)
%
% Removes the goals from Gs that are not from solver Solver.
nonlin_strip([],_,[]).
nonlin_strip([M:What|Gs],Solver,Res) :-
(
M == Solver ->
(
What = {G} ->
Res = [G|Gss]
;
Res = [What|Gss]
)
;
Res = Gss
),
nonlin_strip(Gs,Solver,Gss).
all_attribute_goals([]) --> [].
all_attribute_goals([V|Vs]) -->
dump_linear(V,toplevel),
dump_nonzero(V,toplevel),
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).
end_of_file.
/* $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).

422
LGPL/clpr/clpr/geler.pl → GPL/clpqr/clpqr/geler.pl
View File

@ -1,230 +1,192 @@
/* $Id: geler.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.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(geler_r,
[
geler/2,
project_nonlin/3,
collect_nonlin/3
]).
%:- attribute goals/1, all_nonlin/1.
attribute_goal(X,Goals) :-
get_attr(X,geler_r,g(goals(Gs),_)),
nonexhausted(Gs,Goals,[]),
Goals = [_|_].
attribute_goal(X,Conj) :-
get_attr(X,geler_r,g(_,all_nonlin(Goals))),
l2conj(Goals,Conj).
% 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) :-
(
Xs = [],
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(goals(Gx),_),Y) :-
!,
(
var(Y),
(
% possibly mutual goals. these need to be run. other goals are run
% as well to remove redundant goals.
get_attr(Y,geler_r,g(goals(Gy),Other)) ->
Later = [Gx,Gy],
(
Other = n ->
del_attr(Y,geler_r)
;
put_attr(Y,geler_r,g(n,Other))
)
;
% no goals in Y, so no mutual goals of X and Y, store goals of X in Y
% no need to run any goal.
get_attr(Y,geler_r,g(n,Other)) ->
Later = [],
put_attr(Y,geler_r,g(goals(Gx),Other))
;
Later = [],
put_attr(Y,geler_r,g(goals(Gx),n))
)
;
nonvar(Y),
Later = [Gx]
),
call_list(Later).
attr_unify_hook(_,_). % no goals in X
% call_list(List)
%
% Calls all the goals in List.
call_list([]).
call_list([G|Gs]) :-
call(G),
call_list(Gs).
%
% 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_r,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 (var(Mutex) 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(Vars,Goal) :-
attach(Vars,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],Goal) :-
(
var(V),
get_attr(V,geler_r,g(goals(Gv),Other)) ->
put_attr(V,geler_r,g(goals((Goal,Gv)),Other))
;
get_attr(V,geler_r,(n,Other)) ->
put_attr(V,geler_r,g(goals(Goal),Other))
;
put_attr(V,geler_r,g(goals(Goal),n))
),
attach(Vs,Goal).
/* $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 Normal file
View File

@ -0,0 +1,123 @@
/*
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).

122
LGPL/clpr/clpr/ordering.pl → GPL/clpqr/clpqr/ordering.pl
View File

@ -1,20 +1,19 @@
/* $Id: ordering.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/* $Id: ordering.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Part of CLP(Q) (Constraint Logic Programming over Rationals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.be
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
Copyright (C): 2006, 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 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
@ -41,25 +40,30 @@
:- module(ordering,
[
combine/3,
ordering/1,
arrangement/2
combine/3,
ordering/1,
arrangement/2
]).
:- use_module(class,
[
class_get_prio/2,
class_put_prio/2
class_get_clp/2,
class_get_prio/2,
class_put_prio/2
]).
:- use_module(bv,
:- use_module(itf,
[
var_intern/2
clp_type/2
]).
:- use_module(ugraphs,
:- use_module(library(ugraphs),
[
add_edges/3,
add_vertices/3,
top_sort/2
add_edges/3,
add_vertices/3,
top_sort/2,
ugraph_union/3
]).
:- use_module(library(lists),
[
append/3
]).
ordering(X) :-
@ -81,13 +85,11 @@ ordering(Pb) :-
join_class(Pb,Class),
class_get_prio(Class,Ga),
!,
(
Xs = [],
add_vertices([],Pb,Gb)
;
Xs=[_|_],
gen_edges(Pb,Es,[]),
add_edges([],Es,Gb)
( Xs = [],
add_vertices([],Pb,Gb)
; Xs=[_|_],
gen_edges(Pb,Es,[]),
add_edges([],Es,Gb)
),
combine(Ga,Gb,Gc),
class_put_prio(Class,Gc).
@ -98,16 +100,17 @@ arrangement(Class,Arr) :-
normalize(G,Gn),
top_sort(Gn,Arr),
!.
arrangement(_,_) :- raise_exception(unsatisfiable_ordering).
arrangement(_,_) :- throw(unsatisfiable_ordering).
join_class([],_).
join_class([X|Xs],Class) :-
(
var(X) ->
var_intern(X,Class)
;
true
( 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).
@ -118,7 +121,7 @@ join_class([X|Xs],Class) :-
combine(Ga,Gb,Gc) :-
normalize(Ga,Gan),
normalize(Gb,Gbn),
ugraphs:graph_union(Gan,Gbn,Gc).
ugraph_union(Gan,Gbn,Gc).
%
% both Ga and Gb might have their internal ordering invalidated
@ -134,13 +137,10 @@ normalize(G,Gsgn) :-
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,Xnb,Xnorm)
-> Res = [Xnorm|Xsn],
normalize_vertices(Xs,Xsn)
; normalize_vertices(Xs,Res)
).
% normalize_vertex(X,Nbs,X-Nbss)
@ -160,18 +160,14 @@ normalize_vertex(X,Nbs,X-Nbsss) :-
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
( 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([]) --> [].
@ -194,17 +190,9 @@ group([K-Kl|Ks],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)
( K==L
-> append(Kl,Ll,KLl),
group(Ls,K,KLl,Res)
; Res = [K-Kl|Tail],
group(Ls,L,Ll,Tail)
).

211
LGPL/clpr/clpr/project.pl → GPL/clpqr/clpqr/project.pl
View File

@ -1,20 +1,19 @@
/* $Id: project.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/*
Part of CPL(R) (Constraint Logic Programming over Reals)
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.be
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
Copyright (C): 2006, 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 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
@ -46,41 +45,27 @@
:- module(project,
[
drop_dep/1,
drop_dep_one/1,
make_target_indep/2,
project_attributes/2
drop_dep/1,
drop_dep_one/1,
make_target_indep/2,
project_attributes/2
]).
:- use_module(class,
[
class_allvars/2
class_allvars/2
]).
:- use_module(geler,
[
project_nonlin/3
]).
:- use_module(fourmotz,
[
fm_elim/3
project_nonlin/3
]).
:- use_module(redund,
[
redundancy_vars/1,
systems/3
]).
:- use_module(bv,
[
pivot/4
redundancy_vars/1,
systems/3
]).
:- use_module(ordering,
[
arrangement/2
]).
:- use_module(store,
[
indep/2,
renormalize/2
arrangement/2
]).
%
@ -91,30 +76,45 @@
project_attributes(TargetVars,Cvas) :-
sort(TargetVars,Tvs), % duplicates ?
sort(Cvas,Avs), % duplicates ?
mark_target(Tvs),
project_nonlin(Tvs,Avs,NlReachable),
(
Tvs == [] ->
drop_lin_atts(Avs)
;
redundancy_vars(Avs), % removes redundant bounds (redund.pl)
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(Avs,Tvs,Pivots),
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,itf3,(Ty,St,Li,Or,Cl,Fo,No,_,RAtt)),
put_attr(V,itf3,(Ty,St,Li,Or,Cl,Fo,No,target,RAtt)),
( get_attr(V,itf,Att)
-> setarg(9,Att,target)
; true
),
mark_target(Vs).
% mark_keep(Vars)
%
@ -122,8 +122,8 @@ mark_target([V|Vs]) :-
mark_keep([]).
mark_keep([V|Vs]) :-
get_attr(V,itf3,(Ty,St,Li,Or,Cl,Fo,No,Ta,KI,_)),
put_attr(V,itf3,(Ty,St,Li,Or,Cl,Fo,No,Ta,KI,keep)),
get_attr(V,itf,Att),
setarg(11,Att,keep),
mark_keep(Vs).
%
@ -142,17 +142,19 @@ make_target_indep(Ts,Ps) :- make_target_indep(Ts,[],Ps).
make_target_indep([],Ps,Ps).
make_target_indep([T|Ts],Ps0,Pst) :-
(
get_attr(T,itf3,(type(Type),_,lin(Lin),_)),
Lin = [_,_|H],
nontarget(H,Nt) ->
Ps1 = [T:Nt|Ps0],
get_attr(Nt,itf3,(Ty,St,Li,order(Ord),class(Class),Fo,No,Ta,KI,_)),
put_attr(Nt,itf3,(Ty,St,Li,order(Ord),class(Class),Fo,No,Ta,KI,keep)),
pivot(T,Class,Ord,Type)
;
Ps1 = Ps0
( 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).
@ -163,12 +165,11 @@ make_target_indep([T|Ts],Ps0,Pst) :-
% A nontarget variable has no target attribute and no keep_indep attribute.
nontarget([l(V*_,_)|Vs],Nt) :-
(
get_attr(V,itf3,(_,_,_,_,_,_,_,n,n,_)) ->
Nt = V
;
nontarget(Vs,Nt)
( get_attr(V,itf,Att),
arg(9,Att,n),
arg(10,Att,n)
-> Nt = V
; nontarget(Vs,Nt)
).
% drop_dep(Vars)
@ -190,12 +191,26 @@ drop_dep([V|Vs]) :-
% The linear attributes are: type, strictness, linear equation (lin), class and order.
drop_dep_one(V) :-
get_attr(V,itf3,(type(t_none),_,lin(Lin),order(OrdV),_,Fo,n,n,KI,n)),
\+ indep(Lin,OrdV),
get_attr(V,itf,Att),
Att = t(CLP,type(t_none),_,lin(Lin),order(OrdV),_,_,n,n,_,n),
\+ indep(CLP,Lin,OrdV),
!,
put_attr(V,itf3,(n,n,n,n,n,Fo,n,n,KI,n)).
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.
@ -203,16 +218,18 @@ drop_dep_one(_).
drop_lin_atts([]).
drop_lin_atts([V|Vs]) :-
get_attr(V,itf3,(_,_,_,_,_,RAtt)),
put_attr(V,itf3,(n,n,n,n,n,RAtt)),
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
@ -234,15 +251,13 @@ order(Xs,N,M) :-
N = M.
order([],N,N).
order([X|Xs],N,M) :-
(
get_attr(X,itf3,(_,_,_,order(O),_)),
var(O) ->
O = N,
N1 is N+1,
order(Xs,N1,M)
;
order(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)
@ -254,14 +269,13 @@ renorm_all(Xs) :-
var(Xs),
!.
renorm_all([X|Xs]) :-
(
get_attr(X,itf3,(Ty,St,lin(Lin),RAtt)) ->
renormalize(Lin,New),
put_attr(X,itf3,(Ty,St,lin(New),RAtt)),
renorm_all(Xs)
;
renorm_all(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)
@ -273,14 +287,19 @@ arrange_pivot(Xs) :-
var(Xs),
!.
arrange_pivot([X|Xs]) :-
(
get_attr(X,itf3,(type(t_none),_,lin(Lin),order(OrdX),_)),
Lin = [_,_|[l(Y*_,_)|_]],
get_attr(Y,itf3,(_,_,_,order(OrdY),class(Class),_)),
compare(<,OrdY,OrdX) ->
pivot(X,Class,OrdY,t_none),
arrange_pivot(Xs)
;
arrange_pivot(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)
).

255
LGPL/clpr/clpr/redund.pl → GPL/clpqr/clpqr/redund.pl
View File

@ -1,21 +1,20 @@
/* $Id: redund.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/*
Part of CPL(R) (Constraint Logic Programming over Reals)
Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.be
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
Copyright (C): 2006, 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 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
@ -38,22 +37,15 @@
the GNU General Public License.
*/
:- module(redund,
[
redundancy_vars/1,
systems/3
]).
:- use_module(bv,
[
detach_bounds/1,
intro_at/3
redundancy_vars/1,
systems/3
]).
:- use_module(class,
[
class_allvars/2
class_allvars/2
]).
:- use_module(nf, [{}/1]).
%
% redundancy removal (semantic definition)
@ -70,19 +62,17 @@
systems([],Si,Si).
systems([V|Vs],Si,So) :-
(
var(V),
get_attr(V,itf3,(_,_,_,_,class(C),_)),
not_memq(Si,C) ->
systems(Vs,[C|Si],So)
;
systems(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 (doesn't use unification).
% Succeeds if El is not a member of Lst (does not use unification).
not_memq([],_).
not_memq([Y|Ys],X) :-
@ -124,13 +114,12 @@ redundancy_vs(Vs) :-
!.
redundancy_vs([]).
redundancy_vs([V|Vs]) :-
(
get_attr(V,itf3,(type(Type),strictness(Strict),_)),
redundant(Type,V,Strict) ->
redundancy_vs(Vs)
;
redundancy_vs(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)
@ -141,100 +130,97 @@ redundancy_vs([V|Vs]) :-
% doesn't necessarily mean a redundant bound.
redundant(t_l(L),X,Strict) :-
detach_bounds(X), % drop temporarily
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,L,X),
negate_l(Strict,CLP,L,X),
red_t_l. % negate_l didn't fail, redundant bound
redundant(t_u(U),X,Strict) :-
detach_bounds(X),
negate_u(Strict,U,X),
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,itf3,(_,_,RAtt)),
put_attr(X,itf3,(type(t_u(U)),strictness(Su),RAtt)),
negate_l(Strict,L,X) ->
red_t_l,
(
redundant(t_u(U),X,Strict) ->
true
;
true
)
;
get_attr(X,itf3,(_,_,RAtt)),
put_attr(X,itf3,(type(t_l(L)),strictness(Sl),RAtt)),
negate_u(Strict,U,X) ->
red_t_u
;
true
( 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(X,Bound,t_none), % drop temporarily
detach_bounds(X),
negate_l(Strict,L,X),
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(X,Bound,t_none), % drop temporarily
detach_bounds(X),
negate_u(Strict,U,X),
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,
intro_at(X,Bound,t_u(U)),
get_attr(X,itf3,(Ty,_,RAtt)),
put_attr(X,itf3,(Ty,strictness(Su),RAtt)),
negate_l(Strict,L,X) ->
red_t_l,
(
redundant(t_u(U),X,Strict) ->
true
;
true
)
;
get_attr(X,itf3,(_,_,RAtt)),
put_attr(X,itf3,(type(t_L(L)),strictness(Sl),RAtt)),
negate_u(Strict,U,X) ->
red_t_u
;
true
( 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,itf3,(_,_,RAtt)),
put_attr(X,itf3,(type(t_U(U)),strictness(Su),RAtt)),
negate_l(Strict,L,X) ->
red_t_l,
(
redundant(t_U(U),X,Strict) ->
true
;
true
)
;
Bound is -U,
intro_at(X,Bound,t_l(L)),
get_attr(X,itf3,(Ty,_,RAtt)),
put_attr(X,itf3,(Ty,strictness(Sl),RAtt)),
negate_u(Strict,U,X) ->
red_t_u
;
true
( 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)
@ -252,23 +238,23 @@ strictness_parts(Strict,Lower,Upper) :-
% 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,L,X) :-
{ L > X },
negate_l(0,CLP,L,X) :-
CLP:{L > X},
!,
fail.
negate_l(1,L,X) :-
{ L > X },
negate_l(1,CLP,L,X) :-
CLP:{L > X},
!,
fail.
negate_l(2,L,X) :-
{ L >= X },
negate_l(2,CLP,L,X) :-
CLP:{L >= X},
!,
fail.
negate_l(3,L,X) :-
{ L >= X },
negate_l(3,CLP,L,X) :-
CLP:{L >= X},
!,
fail.
negate_l(_,_,_).
negate_l(_,_,_,_).
% negate_u(Strict,Upperbound,X)
%
@ -276,23 +262,31 @@ negate_l(_,_,_).
% 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,U,X) :-
{ U < X },
negate_u(0,CLP,U,X) :-
CLP:{U < X},
!,
fail.
negate_u(1,U,X) :-
{ U =< X },
negate_u(1,CLP,U,X) :-
CLP:{U =< X},
!,
fail.
negate_u(2,U,X) :-
{ U < X },
negate_u(2,CLP,U,X) :-
CLP:{U < X},
!,
fail.
negate_u(3,U,X) :-
{ U =< X },
negate_u(3,CLP,U,X) :-
CLP:{U =< X},
!,
fail.
negate_u(_,_,_).
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.
@ -300,5 +294,4 @@ negate_u(_,_,_).
red_t_l.
red_t_u.
red_t_L.
red_t_U.
red_t_U.

270
LGPL/clpr/clpr.pl → GPL/clpqr/clpr.pl
View File

@ -1,134 +1,136 @@
/* $Id: clpr.pl,v 1.3 2005-11-01 18:54:06 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.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,
dump/3, projecting_assert/1
]).
%
% 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/arith_r',
'clpr/itf3',
'clpr/store',
'clpr/geler',
'clpr/nfr',
'clpr/class',
'clpr/nf',
'clpr/project',
'clpr/bv',
'clpr/ineq',
'clpr/redund',
'clpr/fourmotz',
'clpr/bb',
'clpr/dump'
],
[ 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,itf3,_)
;
get_attr(Term,geler_r,_)
),
\+ 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)
).
/* $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)
).

173
LGPL/clpr/clpr/bb.pl → GPL/clpqr/clpr/bb_r.pl
View File

@ -1,9 +1,9 @@
/* $Id: bb.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/* $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: Tom.Schrijvers@cs.kuleuven.ac.be
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
@ -38,36 +38,32 @@
the GNU General Public License.
*/
:- module(bb,
:- module(bb_r,
[
bb_inf/3,
bb_inf/5,
vertex_value/2
bb_inf/3,
bb_inf/5,
vertex_value/2
]).
:- use_module(bv,
:- 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
deref/2,
deref_var/2,
determine_active_dec/1,
inf/2,
iterate_dec/2,
sup/2,
var_with_def_assign/2
]).
:- use_module(nf,
[ {}/1,
entailed/1,
nf/2,
nf_constant/2,
repair/2,
wait_linear/3
:- use_module(nf_r,
[
{}/1,
entailed/1,
nf/2,
nf_constant/2,
repair/2,
wait_linear/3
]).
:- dynamic blackboard_incumbent/1.
% bb_inf(Ints,Term,Inf)
%
% Finds the infimum of Term where the variables Ints are to be integers.
@ -91,13 +87,7 @@ bb_inf(Is,Term,Inf,Vertex,Eps) :-
bb_inf_internal(Is,Lin,Eps,_,_) :-
bb_intern(Is,IsNf,Eps),
(
retract(blackboard_incumbent(_)) ->
true
;
true
),
nb_delete(prov_opt),
repair(Lin,LinR), % bb_narrow ...
deref(LinR,Lind),
var_with_def_assign(Dep,Lind),
@ -105,8 +95,9 @@ bb_inf_internal(Is,Lin,Eps,_,_) :-
bb_loop(Dep,IsNf,Eps),
fail.
bb_inf_internal(_,_,_,Inf,Vertex) :-
retract(blackboard_incumbent(InfVal-Vertex)), % GC
{ Inf =:= InfVal }.
catch(nb_getval(prov_opt,InfVal-Vertex),_,fail),
{Inf =:= InfVal},
nb_delete(prov_opt).
% bb_loop(Opt,Is,Eps)
%
@ -118,20 +109,11 @@ 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),
(
retract(blackboard_incumbent(_)) ->
assert(blackboard_incumbent(Inf-RoundVertex))
;
assert(blackboard_incumbent(Inf-RoundVertex))
)
( 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)
@ -152,10 +134,7 @@ bb_reoptimize(Obj,Inf) :-
% Checks if the new infimum Inf is better than the previous one (if such exists).
bb_better_bound(Inf) :-
blackboard_incumbent(Inc-_),
!,
Inf - Inc < -1e-010.
bb_better_bound(_).
catch((nb_getval(prov_opt,Inc-_),Inf - Inc < -1.0e-10),_,true).
% bb_branch(V,U,L)
%
@ -164,31 +143,26 @@ bb_better_bound(_).
bb_branch(V,U,_) :- {V =< U}.
bb_branch(V,_,L) :- {V >= L}.
% vertex_value(Vars,Rhss)
% vertex_value(Vars,Values)
%
% Returns in Rhss, the Rhs values corresponding to the Vars via rhs_value/2.
% 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,Rhs)
% rhs_value(X,Value)
%
% Returns the Rhs value of variable X. This is the value by which the
% variable is actively bounded. If X is a nonvar, the value of X is returned.
% 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
( 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)
@ -199,16 +173,13 @@ rhs_value(Xn,Value) :-
% 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 float(floor(Rhs)),
Ceiling is float(ceiling(Rhs)),
Eps - min(Rhs-Floor,Ceiling-Rhs) < -1e-010 ->
Viol = I,
F = Floor,
C = Ceiling
;
bb_first_nonint(Is,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])
@ -217,7 +188,7 @@ bb_first_nonint([I|Is],[Rhs|Rhss],Eps,Viol,F,C) :-
round_values([],[]).
round_values([X|Xs],[Y|Ys]) :-
Y = float(round(X)),
Y is round(X),
round_values(Xs,Ys).
% bb_intern([X|Xs],[Xi|Xis],Eps)
@ -245,7 +216,7 @@ bb_intern([],X,_,_) :-
bb_intern([v(I,[])],X,_,Eps) :-
!,
X = I,
min(I-float(floor(I)),float(ceiling(I))-I) - Eps < 1e-010.
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,
@ -255,7 +226,7 @@ bb_intern([v(One,[V^1])],X,_,_) :-
bb_narrow_lower(X),
bb_narrow_upper(X).
bb_intern(_,_,Term,_) :-
raise_exception(instantiation_error(bb_inf(Term,_,_),1)).
throw(instantiation_error(bb_inf(Term,_,_),1)).
% bb_narrow_lower(X)
%
@ -265,19 +236,13 @@ bb_intern(_,_,Term,_) :-
% (second integer if X is to be strict larger than the first integer).
bb_narrow_lower(X) :-
(
inf(X,Inf) ->
Bound is float(ceiling(Inf)),
(
entailed(X > Bound) ->
{X >= Bound+1}
;
{X >= Bound}
)
;
true
( inf(X,Inf)
-> Bound is ceiling(Inf-1.0e-10),
( entailed(X > Bound)
-> {X >= Bound+1}
; {X >= Bound}
)
; true
).
% bb_narrow_upper(X)
@ -285,17 +250,11 @@ bb_narrow_lower(X) :-
% See bb_narrow_lower/1. This predicate handles the upper bound.
bb_narrow_upper(X) :-
(
sup(X,Sup) ->
Bound is float(floor(Sup)),
(
entailed(X < Bound) ->
{X =< Bound-1}
;
{X =< Bound}
)
;
true
( 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 Normal file
View File

File diff suppressed because it is too large Load Diff

237
LGPL/clpr/clpr/fourmotz.pl → GPL/clpqr/clpr/fourmotz_r.pl
View File

@ -1,9 +1,9 @@
/* $Id: fourmotz.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/* $Id: fourmotz_r.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Part of CLP(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.be
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
@ -39,39 +39,39 @@
*/
:- module(fourmotz,
:- module(fourmotz_r,
[
fm_elim/3
fm_elim/3
]).
:- use_module(bv,
:- use_module(bv_r,
[
allvars/2,
basis_add/2,
detach_bounds/1,
pivot/4,
var_with_def_intern/4
allvars/2,
basis_add/2,
detach_bounds/1,
pivot/5,
var_with_def_intern/4
]).
:- use_module(class,
:- use_module('../clpqr/class',
[
class_allvars/2
class_allvars/2
]).
:- use_module(project,
:- use_module('../clpqr/project',
[
drop_dep/1,
drop_dep_one/1,
make_target_indep/2
drop_dep/1,
drop_dep_one/1,
make_target_indep/2
]).
:- use_module(redund,
:- use_module('../clpqr/redund',
[
redundancy_vars/1
redundancy_vars/1
]).
:- use_module(store,
:- use_module(store_r,
[
add_linear_11/3,
add_linear_f1/4,
indep/2,
nf_coeff_of/3,
normalize_scalar/2
add_linear_11/3,
add_linear_f1/4,
indep/2,
nf_coeff_of/3,
normalize_scalar/2
]).
@ -87,15 +87,13 @@ fm_elim(Vs,Target,Pivots) :-
prefilter([],[]).
prefilter([V|Vs],Res) :-
(
get_attr(V,itf3,(Ty,St,Li,Or,Cl,Fo,No,n,_,Ke)),
occurs(V) -> % V is a nontarget variable that occurs in a bounded linear equation
Res = [V|Tail],
put_attr(V,itf3,(Ty,St,Li,Or,Cl,Fo,No,n,keep_indep,Ke)),
prefilter(Vs,Tail)
;
prefilter(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)
).
%
@ -106,14 +104,12 @@ 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 = []
( 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).
@ -137,7 +133,10 @@ best(Vs,Best,Rest) :-
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,itf3,(_,_,lin(Lin),order(OrdX),_,_,_,n,_)), % no target variable
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 = [_|_],
@ -185,10 +184,14 @@ elim_min(V,Occ,Target,Pivots,NewPivots) :-
%
reverse_pivot([]).
reverse_pivot([I:D|Ps]) :-
get_attr(D,itf3,(type(Dt),St,Li,Or,Cl,Fo,No,Ta,KI,_)),
put_attr(D,itf3,(type(Dt),St,Li,Or,Cl,Fo,No,Ta,KI,n)), % no longer
get_attr(I,itf3,(_,_,_,order(OrdI),class(ClI),_)),
pivot(D,ClI,OrdI,Dt),
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)
@ -197,8 +200,8 @@ reverse_pivot([I:D|Ps]) :-
unkeep([]).
unkeep([_:D|Ps]) :-
get_attr(D,itf3,(Ty,St,Li,Or,Cl,Fo,No,Ta,KI,_)),
put_attr(D,itf3,(Ty,St,Li,Or,Cl,Fo,No,Ta,KI,n)),
get_attr(D,itf,Att),
setarg(11,Att,n),
drop_dep_one(D),
unkeep(Ps).
@ -218,8 +221,7 @@ fm_detach([V:_|Vs]) :-
activate_crossproduct([]).
activate_crossproduct([lez(Strict,Lin)|News]) :-
Z = 0.0,
var_with_def_intern(t_u(Z),Var,Lin,Strict),
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).
@ -252,26 +254,29 @@ crossproduct([A|As]) -->
crossproduct([],_) --> [].
crossproduct([B:Kb|Bs],A:Ka) -->
{
get_attr(A,itf3,(type(Ta),strictness(Sa),lin(LinA),_)),
get_attr(B,itf3,(type(Tb),strictness(Sb),lin(LinB),_)),
K is -Kb/Ka,
add_linear_f1(LinA,K,LinB,Lin) % Lin doesn't contain the target variable anymore
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
},
(
{ 0.0 - K < -1e-010 } -> % 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)
( { 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).
@ -291,14 +296,13 @@ crossproduct([B:Kb|Bs],A:Ka) -->
cross_lower(Ta,Tb,K,Lin,Strict) -->
{
lower(Ta,La),
lower(Tb,Lb),
!,
L is K*La+Lb,
normalize_scalar(L,Ln),
Mone = -1.0,
add_linear_f1(Lin,Mone,Ln,Lhs),
Sl is Strict >> 1 % normalize to upper bound
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(_,_,_,_,_) --> [].
@ -311,13 +315,13 @@ cross_lower(_,_,_,_,_) --> [].
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
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(_,_,_,_,_) --> [].
@ -385,18 +389,17 @@ cp_card([A|As],Ci,Co) :-
cp_card([],_,Ci,Ci).
cp_card([B:Kb|Bs],A:Ka,Ci,Co) :-
get_attr(A,itf3,(type(Ta),_)),
get_attr(B,itf3,(type(Tb),_)),
get_attr(A,itf,AttA),
arg(2,AttA,type(Ta)),
get_attr(B,itf,AttB),
arg(2,AttB,type(Tb)),
K is -Kb/Ka,
(
0.0- K < -1e-010 -> % 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)
( 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).
@ -431,7 +434,9 @@ cp_card_upper(_,_,Si,Si).
% of V in the linear equation of D.
occurences(V,Occ) :-
get_attr(V,itf3,(_,_,_,order(OrdV),class(C),_)),
get_attr(V,itf,Att),
arg(5,Att,order(OrdV)),
arg(6,Att,class(C)),
class_allvars(C,All),
occurences(All,OrdV,Occ).
@ -445,15 +450,14 @@ occurences(De,_,[]) :-
var(De),
!.
occurences([D|De],OrdV,Occ) :-
(
get_attr(D,itf3,(type(Type),_,lin(Lin),_)),
occ_type_filter(Type),
nf_coeff_of(Lin,OrdV,K) ->
Occ = [D:K|Occt],
occurences(De,OrdV,Occt)
;
occurences(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)
@ -474,7 +478,9 @@ occ_type_filter(t_Lu(_,_)).
% =\= t_none.
occurs(V) :-
get_attr(V,itf3,(_,_,_,order(OrdV),class(C),_)),
get_attr(V,itf,Att),
arg(5,Att,order(OrdV)),
arg(6,Att,class(C)),
class_allvars(C,All),
occurs(All,OrdV).
@ -488,12 +494,11 @@ occurs(De,_) :-
!,
fail.
occurs([D|De],OrdV) :-
(
get_attr(D,itf3,(type(Type),_,lin(Lin),_)),
occ_type_filter(Type),
nf_coeff_of(Lin,OrdV,_) ->
true
;
occurs(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 Normal file
View File

File diff suppressed because it is too large Load Diff

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

@ -0,0 +1,227 @@
/*
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(_,_,_,_).

617
LGPL/clpr/clpr/nf.pl → GPL/clpqr/clpr/nf_r.pl
View File

@ -1,9 +1,9 @@
/* $Id: nf.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/*
Part of CPL(R) (Constraint Logic Programming over Reals)
Part of CLP(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.be
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
@ -39,56 +39,46 @@
*/
:- module(nf,
:- module(nf_r,
[
{}/1,
nf/2,
entailed/1,
split/3,
repair/2,
nf_constant/2,
wait_linear/3,
nf2term/2
{}/1,
nf/2,
entailed/1,
split/3,
repair/2,
nf_constant/2,
wait_linear/3,
nf2term/2
]).
:- use_module(geler,
:- use_module('../clpqr/geler',
[
geler/2
geler/3
]).
:- use_module(bv,
:- use_module(bv_r,
[
export_binding/2,
log_deref/4,
solve/1,
'solve_<'/1,
'solve_=<'/1,
'solve_=\\='/1
export_binding/2,
log_deref/4,
solve/1,
'solve_<'/1,
'solve_=<'/1,
'solve_=\\='/1
]).
:- use_module(ineq,
:- use_module(ineq_r,
[
ineq_one/4,
ineq_one_s_p_0/1,
ineq_one_s_n_0/1,
ineq_one_n_p_0/1,
ineq_one_n_n_0/1
ineq_one/4,
ineq_one_s_p_0/1,
ineq_one_s_n_0/1,
ineq_one_n_p_0/1,
ineq_one_n_n_0/1
]).
:- use_module(store,
:- use_module(store_r,
[
add_linear_11/3,
normalize_scalar/2
]).
:- use_module(nfr,
[
transg/3
]).
:- use_module(arith_r,
[
arith_eps/1,
arith_normalize/2,
integerp/2
add_linear_11/3,
normalize_scalar/2
]).
goal_expansion(geler(X,Y),geler(clpr,X,Y)).
% -------------------------------------------------------------------------
@ -103,12 +93,10 @@
{Rel} :-
var(Rel),
!,
raise_exception(instantiation_error({Rel},1)).
throw(instantiation_error({Rel},1)).
{R,Rs} :-
!,
{R},
!,
{Rs}.
{R},{Rs}.
{R;Rs} :-
!,
({R};{Rs}). % for entailment checking
@ -144,7 +132,7 @@
!,
nf(L-R,Nf),
submit_eq(Nf).
{Rel} :- raise_exception(type_error({Rel},1,'a constraint',Rel)).
{Rel} :- throw(type_error({Rel},1,'a constraint',Rel)).
% entailed(C)
%
@ -165,7 +153,7 @@ entailed(C) :-
negate(Rel,_) :-
var(Rel),
!,
raise_exception(instantiation_error(entailed(Rel),1)).
throw(instantiation_error(entailed(Rel),1)).
negate((A,B),(Na;Nb)) :-
!,
negate(A,Na),
@ -181,7 +169,7 @@ negate(A>=B,A<B) :- !.
negate(A=:=B,A=\=B) :- !.
negate(A=B,A=\=B) :- !.
negate(A=\=B,A=:=B) :- !.
negate(Rel,_) :- raise_exception( type_error(entailed(Rel),1,'a constraint',Rel)).
negate(Rel,_) :- throw( type_error(entailed(Rel),1,'a constraint',Rel)).
% submit_eq(Nf)
%
@ -221,13 +209,11 @@ submit_eq_b(v(_,[X^P])) :-
var(X),
P > 0,
!,
Z = 0.0,
export_binding(X,Z).
export_binding(X,0.0).
% case b2: non-linear is invertible: NL(X) = 0 => X - inv(NL)(0) = 0
submit_eq_b(v(_,[NL^1])) :-
nonvar(NL),
Z = 0.0,
nl_invertible(NL,X,Z,Inv),
nl_invertible(NL,X,0.0,Inv),
!,
nf(-Inv,S),
nf_add(X,S,New),
@ -235,7 +221,7 @@ submit_eq_b(v(_,[NL^1])) :-
% case b4: A is non-linear and not invertible => submit equality to geler
submit_eq_b(Term) :-
term_variables(Term,Vs),
geler(Vs,nf:resubmit_eq([Term])).
geler(Vs,nf_r:resubmit_eq([Term])).
% submit_eq_c(A,B,Rest)
%
@ -262,7 +248,7 @@ submit_eq_c(A,B,Rest) :- % c2
submit_eq_c(A,B,Rest) :-
Norm = [A,B|Rest],
term_variables(Norm,Vs),
geler(Vs,nf:resubmit_eq(Norm)).
geler(Vs,nf_r:resubmit_eq(Norm)).
% submit_eq_c1(Rest,B,K)
%
@ -271,27 +257,23 @@ submit_eq_c(A,B,Rest) :-
% case c11: k+cX^1=0 or k+cX^-1=0
submit_eq_c1([],v(K,[X^P]),I) :-
var(X),
(
P = 1,
!,
Val is -I/K,
export_binding(X,Val)
;
P = -1,
!,
Val is -K/I,
export_binding(X,Val)
( P =:= 1,
!,
Val is -I/K,
export_binding(X,Val)
; P =:= -1,
!,
Val is -K/I,
export_binding(X,Val)
).
% case c12: non-linear, invertible: cNL(X)^1+k=0 => inv(NL)(-k/c) = 0 ;
% cNL(X)^-1+k=0 => inv(NL)(-c/k) = 0
submit_eq_c1([],v(K,[NL^P]),I) :-
nonvar(NL),
(
P = 1,
Y is -I/K
;
P = -1,
Y is -K/I
( P =:= 1,
Y is -I/K
; P =:= -1,
Y is -K/I
),
nl_invertible(NL,X,Y,Inv),
!,
@ -315,7 +297,7 @@ submit_eq_c1(Rest,B,I) :-
submit_eq_c1(Rest,B,I) :-
Norm = [v(I,[]),B|Rest],
term_variables(Norm,Vs),
geler(Vs,nf:resubmit_eq(Norm)).
geler(Vs,nf_r:resubmit_eq(Norm)).
% -----------------------------------------------------------------------
@ -344,22 +326,19 @@ submit_lt([B|Bs],A) :- submit_lt_c(Bs,A,B).
% c < 0
submit_lt_b([],I) :-
!,
I - 0.0 < -1e-010.
I < -1.0e-10.
% cX^1 < 0 : if c < 0 then X > 0, else X < 0
submit_lt_b([X^1],K) :-
var(X),
!,
(
0.0 - K < -1e-010 ->
ineq_one_s_p_0(X) % X is strictly positive
;
ineq_one_s_n_0(X) % X is strictly negative
( K > 1.0e-10
-> ineq_one_s_p_0(X) % X is strictly negative
; ineq_one_s_n_0(X) % X is strictly positive
).
% non-linear => geler
submit_lt_b(P,K) :-
term_variables(P,Vs),
geler(Vs,nf:resubmit_lt([v(K,P)])).
geler(Vs,nf_r:resubmit_lt([v(K,P)])).
% submit_lt_c(Bs,A,B)
%
@ -375,13 +354,10 @@ submit_lt_c([],A,B) :-
% linear < 0 => solve, non-linear < 0 => geler
submit_lt_c(Rest,A,B) :-
Norm = [A,B|Rest],
(
linear(Norm) ->
'solve_<'(Norm)
;
term_variables(Norm,Vs),
geler(Vs,nf:resubmit_lt(Norm))
( linear(Norm)
-> 'solve_<'(Norm)
; term_variables(Norm,Vs),
geler(Vs,nf_r:resubmit_lt(Norm))
).
% submit_le(Nf)
@ -410,22 +386,19 @@ submit_le([B|Bs],A) :- submit_le_c(Bs,A,B).
% c =< 0
submit_le_b([],I) :-
!,
I - 0.0 < 1e-010.
I < 1.0e-10.
% cX^1 =< 0: if c < 0 then X >= 0, else X =< 0
submit_le_b([X^1],K) :-
var(X),
!,
(
0.0 - K < -1e-010 ->
ineq_one_n_p_0(X) % X is non-strictly positive
;
ineq_one_n_n_0(X) % X is non-strictly negative
( K > 1.0e-10
-> ineq_one_n_p_0(X) % X is non-strictly negative
; ineq_one_n_n_0(X) % X is non-strictly positive
).
% cX^P =< 0 => geler
submit_le_b(P,K) :-
term_variables(P,Vs),
geler(Vs,nf:resubmit_le([v(K,P)])).
geler(Vs,nf_r:resubmit_le([v(K,P)])).
% submit_le_c(Bs,A,B)
%
@ -441,13 +414,10 @@ submit_le_c([],A,B) :-
% A, B & Rest are linear => solve, otherwise => geler
submit_le_c(Rest,A,B) :-
Norm = [A,B|Rest],
(
linear(Norm) ->
'solve_=<'(Norm)
;
term_variables(Norm,Vs),
geler(Vs,nf:resubmit_le(Norm))
( linear(Norm)
-> 'solve_=<'(Norm)
; term_variables(Norm,Vs),
geler(Vs,nf_r:resubmit_le(Norm))
).
% submit_ne(Nf)
@ -456,24 +426,12 @@ submit_le_c(Rest,A,B) :-
% if Nf is a constant => check constant = 0, else if Nf is linear => solve else => geler
submit_ne(Norm1) :-
(
nf_constant(Norm1,K) ->
TestK is K - 0.0, % K =\= 0
(
TestK < -1e-010 ->
true
;
TestK > 1e-010
)
;
linear(Norm1) ->
'solve_=\\='(Norm1)
;
term_variables(Norm1,Vs),
geler(Vs,nf:resubmit_ne(Norm1))
( nf_constant(Norm1,K)
-> \+ (K >= -1.0e-10, K =< 1.0e-10) % K =\= 0
; linear(Norm1)
-> 'solve_=\\='(Norm1)
; term_variables(Norm1,Vs),
geler(Vs,nf_r:resubmit_ne(Norm1))
).
% linear(A)
@ -488,7 +446,8 @@ linear([A|As]) :-
% linear_ps(A)
%
% Succeeds when A = V^1 with V a variable. This reflects the linearity of v(_,A).
% Succeeds when A = V^1 with V a variable.
% This reflects the linearity of v(_,A).
linear_ps([]).
linear_ps([V^1]) :- var(V). % excludes sin(_), ...
@ -501,14 +460,11 @@ linear_ps([V^1]) :- var(V). % excludes sin(_), ...
%
wait_linear(Term,Var,Goal) :-
nf(Term,Nf),
(
linear(Nf) ->
Var = Nf,
call(Goal)
;
term_variables(Nf,Vars),
geler(Vars,nf:wait_linear_retry(Nf,Var,Goal))
( linear(Nf)
-> Var = Nf,
call(Goal)
; term_variables(Nf,Vars),
geler(Vars,nf_r:wait_linear_retry(Nf,Var,Goal))
).
%
% geler clients
@ -527,50 +483,35 @@ resubmit_ne(N) :-
submit_ne(Norm).
wait_linear_retry(Nf0,Var,Goal) :-
repair(Nf0,Nf),
(
linear(Nf) ->
Var = Nf,
call(Goal)
;
term_variables(Nf,Vars),
geler(Vars,nf:wait_linear_retry(Nf,Var,Goal))
( linear(Nf)
-> Var = Nf,
call(Goal)
; term_variables(Nf,Vars),
geler(Vars,nf_r:wait_linear_retry(Nf,Var,Goal))
).
% -----------------------------------------------------------------------
% nl_invertible(F,X,Y,Res)
%
% Res is the evaluation of the inverse of nonlinear function F in variable X where X is Y
% Res is the evaluation of the inverse of nonlinear function F in variable X
% where X is Y
nl_invertible(sin(X),X,Y,Res) :- Res is asin(Y).
nl_invertible(cos(X),X,Y,Res) :- Res is acos(Y).
nl_invertible(tan(X),X,Y,Res) :- Res is atan(Y).
nl_invertible(exp(B,C),X,A,Res) :-
(
nf_constant(B,Kb) ->
0.0 - A < -1e-010,
0.0 - Kb < -1e-010,
TestKb is Kb - 1.0,
(
TestKb < -1e-010 ->
true
;
TestKb > 1e-010
),
X = C, % note delayed unification
Res is log(A)/log(Kb)
;
nf_constant(C,Kc),
\+ (
TestA is A - 0.0, % A =:= 0
TestA =< 1e-010,
TestA >= -1e-010,
Kc - 0.0 < 1e-010 % Kc =< 0
),
X = B, % note delayed unification
Res is A**(1.0/Kc)
( nf_constant(B,Kb)
-> A > 1.0e-10,
Kb > 1.0e-10,
TestKb is Kb - 1.0, % Kb =\= 1.0
\+ (TestKb >= -1.0e-10, TestKb =< 1.0e-10),
X = C, % note delayed unification
Res is log(A)/log(Kb)
; nf_constant(C,Kc),
\+ (A >= -1.0e-10, A =< 1.0e-10), % A =\= 0
Kc > 1.0e-10, % Kc > 0
X = B, % note delayed unification
Res is A**(1.0/Kc)
).
% -----------------------------------------------------------------------
@ -586,34 +527,21 @@ nl_invertible(exp(B,C),X,A,Res) :-
nf(X,Norm) :-
var(X),
!,
Norm = [v(One,[X^1])],
One = 1.0.
Norm = [v(1.0,[X^1])].
nf(X,Norm) :-
number(X),
!,
nf_number(X,Norm).
%
nf(rat(N,D),Norm) :-
!,
nf_number(rat(N,D),Norm).
%
nf(#(Const),Norm) :-
monash_constant(Const,Value),
!,
(
rat(1,1) = 1.0 ->
nf_number(Value,Norm) % swallows #(zero) ... ok in Q
;
arith_normalize(Value,N), % in R we want it
Norm = [v(N,[])]
).
Norm = [v(Value,[])].
%
nf(-A,Norm) :-
!,
nf(A,An),
K = -1.0,
nf_mul_factor(v(K,[]),An,Norm).
nf_mul_factor(v(-1.0,[]),An,Norm).
nf(+A,Norm) :-
!,
nf(A,Norm).
@ -654,32 +582,18 @@ nf(Term,Norm) :-
nf_nonlin_2(Skel,A1n,A2n,Sa1,Sa2,Norm).
%
nf(Term,_) :-
raise_exception(type_error(nf(Term,_),1,'a numeric expression',Term)).
throw(type_error(nf(Term,_),1,'a numeric expression',Term)).
% nf_number(N,Res)
%
% If N is a number, N is normalized (in R: n is converted to a float; in Q: n is converted to a normalized rational)
% If N is a number, N is normalized
nf_number(N,Res) :-
nf_number(N),
arith_normalize(N,Normal),
(
TestNormal is Normal - 0.0, % Normal =:= 0
TestNormal =< 1e-010,
TestNormal >= -1e-010 ->
Res = []
;
Res = [v(Normal,[])]
).
% checks whether N is a number (standard Prolog number or rational)
nf_number(N) :-
number(N),
!. /* MC 980507 */
nf_number(N) :-
compound(N),
N=rat(_,_). % sicstus
( (N >= -1.0e-10, N =< 1.0e-10) % N =:= 0
-> Res = []
; Res = [v(N,[])]
).
nonlin_1(abs(X),X,abs(Y),Y).
nonlin_1(sin(X),X,sin(Y),Y).
@ -692,33 +606,23 @@ nonlin_2(pow(A,B),A,B,exp(X,Y),X,Y). % pow->exp
nonlin_2(A^B,A,B,exp(X,Y),X,Y).
nf_nonlin_1(Skel,An,S1,Norm) :-
(
nf_constant(An,S1) ->
nl_eval(Skel,Res),
nf_number(Res,Norm)
;
S1 = An,
One = 1.0,
Norm = [v(One,[Skel^1])]).
( nf_constant(An,S1)
-> nl_eval(Skel,Res),
nf_number(Res,Norm)
; S1 = An,
Norm = [v(1.0,[Skel^1])]).
nf_nonlin_2(Skel,A1n,A2n,S1,S2,Norm) :-
(
nf_constant(A1n,S1),
nf_constant(A2n,S2) ->
nl_eval(Skel,Res),
nf_number(Res,Norm)
;
Skel=exp(_,_),
nf_constant(A2n,Exp),
integerp(Exp,I) ->
nf_power(I,A1n,Norm)
;
S1 = A1n,
S2 = A2n,
One = 1.0,
Norm = [v(One,[Skel^1])]
( nf_constant(A1n,S1),
nf_constant(A2n,S2)
-> nl_eval(Skel,Res),
nf_number(Res,Norm)
; Skel=exp(_,_),
nf_constant(A2n,Exp),
integerp(Exp,I)
-> nf_power(I,A1n,Norm)
; S1 = A1n,
S2 = A2n,
Norm = [v(1.0,[Skel^1])]
).
% evaluates non-linear functions in one variable where the variable is bound
@ -726,7 +630,8 @@ nl_eval(abs(X),R) :- R is abs(X).
nl_eval(sin(X),R) :- R is sin(X).
nl_eval(cos(X),R) :- R is cos(X).
nl_eval(tan(X),R) :- R is tan(X).
% evaluates non-linear functions in two variables where both variables are bound
% evaluates non-linear functions in two variables where both variables are
% bound
nl_eval(min(X,Y),R) :- R is min(X,Y).
nl_eval(max(X,Y),R) :- R is max(X,Y).
nl_eval(exp(X,Y),R) :- R is X**Y.
@ -738,13 +643,13 @@ monash_constant(X,_) :-
monash_constant(p,3.14259265).
monash_constant(pi,3.14259265).
monash_constant(e,2.71828182).
monash_constant(zero,Eps) :- arith_eps(Eps).
monash_constant(zero,1.0e-10).
%
% check if a Nf consists of just a constant
%
nf_constant([],Z) :- Z = 0.0.
nf_constant([],0.0).
nf_constant([v(K,[])],K).
% split(NF,SNF,C)
@ -755,15 +660,12 @@ nf_constant([v(K,[])],K).
%
% this method depends on the polynf ordering, i.e. [] < [X^1] ...
split([],[],Z) :- Z = 0.0.
split([],[],0.0).
split([First|T],H,I) :-
(
First = v(I,[]) ->
H = T
;
I = 0.0,
H = [First|T]
( First = v(I,[])
-> H = T
; I = 0.0,
H = [First|T]
).
% nf_add(A,B,C): merges two normalized additions into a new normalized addition
@ -796,15 +698,10 @@ nf_add_case(>,A,As,Cs,B,Bs,_,_,_) :-
nf_add(Bs,A,As,Rest).
nf_add_case(=,_,As,Cs,_,Bs,Ka,Kb,Pa) :-
Kc is Ka + Kb,
(
TestKc = Kc - 0.0, % Kc =:= 0
TestKc =< 1e-010,
TestKc >= -1e-010 ->
nf_add(As,Bs,Cs)
;
Cs = [v(Kc,Pa)|Rest],
nf_add(As,Bs,Rest)
( (Kc >= -1.0e-10, Kc =< 1.0e-10) % Kc =:= 0.0
-> nf_add(As,Bs,Cs)
; Cs = [v(Kc,Pa)|Rest],
nf_add(As,Bs,Rest)
).
nf_mul(A,B,Res) :-
@ -840,14 +737,9 @@ nf_add_2_case(<,Af,Bf,[Af,Bf],_,_,_).
nf_add_2_case(>,Af,Bf,[Bf,Af],_,_,_).
nf_add_2_case(=,_, _,Res,Ka,Kb,Pa) :-
Kc is Ka + Kb,
(
TestKc is Kc - 0.0, % Kc =:= 0
TestKc =< 1e-010,
TestKc >= -1e-010 ->
Res = []
;
Res=[v(Kc,Pa)]
( (Kc >= -1.0e-10, Kc =< 1.0e-10) % Kc =:= 0
-> Res = []
; Res = [v(Kc,Pa)]
).
% nf_mul_k(A,B,C)
@ -928,13 +820,10 @@ pmerge_case(>,A,As,Res,B,Bs,_,_,_) :-
pmerge(Bs,A,As,Tail).
pmerge_case(=,_,As,Res,_,Bs,Ka,Kb,Xa) :-
Kc is Ka + Kb,
(
Kc=:=0 ->
pmerge(As,Bs,Res)
;
Res = [Xa^Kc|Tail],
pmerge(As,Bs,Tail)
( Kc =:= 0
-> pmerge(As,Bs,Res)
; Res = [Xa^Kc|Tail],
pmerge(As,Bs,Tail)
).
% nf_div(Factor,In,Out)
@ -951,7 +840,7 @@ nf_div([v(K,P)],Sum,Res) :-
Ki is 1.0/K,
mult_exp(P,-1,Pi),
nf_mul_factor(v(Ki,Pi),Sum,Res).
nf_div(D,A,[v(One,[(A/D)^1])]) :- One = 1.0.
nf_div(D,A,[v(1.0,[(A/D)^1])]).
% zero_division
%
@ -975,24 +864,17 @@ mult_exp([X^P|Xs],K,[X^I|Tail]) :-
nf_power(N,Sum,Norm) :-
integer(N),
compare(Rel,N,0),
(
Rel = (<) ->
Pn is -N,
% nf_power_pos(Pn,Sum,Inorm),
binom(Sum,Pn,Inorm),
One = 1.0,
nf_div(Inorm,[v(One,[])],Norm)
;
Rel = (>) ->
% nf_power_pos(N,Sum,Norm)
binom(Sum,N,Norm)
;
Rel = (=) -> % 0^0 is indeterminate but we say 1
One = 1.0,
Norm = [v(One,[])]
( Rel = (<)
-> Pn is -N,
% nf_power_pos(Pn,Sum,Inorm),
binom(Sum,Pn,Inorm),
nf_div(Inorm,[v(1.0,[])],Norm)
; Rel = (>)
-> % nf_power_pos(N,Sum,Norm)
binom(Sum,N,Norm)
; Rel = (=)
-> % 0^0 is indeterminate but we say 1
Norm = [v(1.0,[])]
).
%
% N>0
@ -1014,26 +896,19 @@ binom(Sum,1,Power) :-
Power = Sum.
binom([],_,[]).
binom([A|Bs],N,Power) :-
(
Bs = [] ->
nf_power_factor(A,N,Ap),
Power = [Ap]
;
Bs = [_|_] ->
One = 1.0,
factor_powers(N,A,v(One,[]),Pas),
sum_powers(N,Bs,[v(One,[])],Pbs,[]),
combine_powers(Pas,Pbs,0,N,1,[],Power)
( Bs = []
-> nf_power_factor(A,N,Ap),
Power = [Ap]
; Bs = [_|_]
-> factor_powers(N,A,v(1.0,[]),Pas),
sum_powers(N,Bs,[v(1.0,[])],Pbs,[]),
combine_powers(Pas,Pbs,0,N,1,[],Power)
).
combine_powers([],[],_,_,_,Pi,Pi).
combine_powers([A|As],[B|Bs],L,R,C,Pi,Po) :-
nf_mul(A,B,Ab),
arith_normalize(C,Cn),
nf_mul_k(Ab,Cn,Abc),
nf_mul_k(Ab,C,Abc),
nf_add(Abc,Pi,Pii),
L1 is L+1,
R1 is R-1,
@ -1041,8 +916,7 @@ combine_powers([A|As],[B|Bs],L,R,C,Pi,Po) :-
combine_powers(As,Bs,L1,R1,C1,Pii,Po).
nf_power_factor(v(K,P),N,v(Kn,Pn)) :-
arith_normalize(N,Nn),
Kn is K**Nn,
Kn is K**N,
mult_exp(P,N,Pn).
factor_powers(0,_,Prev,[[Prev]]) :- !.
@ -1078,8 +952,7 @@ repair_log(N,A0,A2,R) :-
repair_term(K,P,Norm) :-
length(P,Len),
One = 1.0,
repair_p_log(Len,P,[],Pr,[v(One,[])],Sum),
repair_p_log(Len,P,[],Pr,[v(1.0,[])],Sum),
nf_mul_factor(v(K,Pr),Sum,Norm).
repair_p_log(0,Ps,Ps,[],L0,L0) :- !.
@ -1110,7 +983,7 @@ repair_p(Term,P,[],L0,L1) :-
% digested -> cuts after repair of args!
%
repair_p_one(Term,TermN) :-
nf_number(Term,TermN), % freq. shortcut for nf/2 case below
nf_number(Term,TermN), % freq. shortcut for nf/2 case below
!.
repair_p_one(A1/A2,TermN) :-
repair(A1,A1n),
@ -1141,7 +1014,7 @@ nf_length([_|R],Li,Lo) :-
% transforms a normal form into a readable term
% empty normal form = 0
nf2term([],Z) :- Z = 0.0.
nf2term([],0.0).
% term is first element (+ next elements)
nf2term([F|Fs],T) :-
f02t(F,T0), % first element
@ -1158,83 +1031,61 @@ yfx([F|Fs],T0,TN) :-
% transforms the first element of the normal form (something of the form v(K,P))
% into a readable term
f02t(v(K,P),T) :-
(
P = [] -> % just a constant
T = K
;
TestK is K - 0.0, % K =:= 0
TestK =< 1e-010,
TestK >= -1e-010 -> % constant = 1,P =\= [], don't show constant
p2term(P,T)
;
TestK is K - -1.0, % K =:= -1
TestK =< 1e-010,
TestK >= -1e-010 ->
T = -Pt, % constant = -1, P =\= [], only show sign (-) p2term(P,Pt)
p2term(P,Pt)
;
T = K*Pt,
p2term(P,Pt)
( % just a constant
P = []
-> T = K
; TestK is K - 1.0, % K =:= 1
(TestK >= -1.0e-10, TestK =< 1.0e-10)
-> p2term(P,T)
; TestK is K + 1.0, % K =:= -1
(TestK >= -1.0e-10, TestK =< 1.0e-10)
-> T = -Pt,
p2term(P,Pt)
; T = K*Pt,
p2term(P,Pt)
).
% f02t(v(K,P),T,Op)
%
% transforms a next element of the normal form (something of the form v(K,P)) into a readable term
% transforms a next element of the normal form (something of the form v(K,P))
% into a readable term
fn2t(v(K,P),Term,Op) :-
(
TestK is K - 1.0, % K =:= 1
TestK =< 1e-010,
TestK >= -1e-010 -> % no constant, Op = +
Term = Pt,
Op = +
;
TestK is K - -1.0, % K =:= -1
TestK =< 1e-010,
TestK >= -1e-010 -> % no constant, Op = -
Term = Pt,
Op = -
;
K - 0.0 < -1e-010 -> % constant, Op = -
Kf is -K,
Term = Kf*Pt,
Op = -
; % constant, Op = +
Term = K*Pt,
Op = +
( TestK is K - 1.0, % K =:= 1
(TestK >= -1.0e-10, TestK =< 1.0e-10)
-> Term = Pt,
Op = +
; TestK is K + 1.0, % K =:= -1
(TestK >= -1.0e-10, TestK =< 1.0e-10)
-> Term = Pt,
Op = -
; K < -1.0e-10 % K < 0
-> Kf is -K,
Term = Kf*Pt,
Op = -
; % K > 0
Term = K*Pt,
Op = +
),
p2term(P,Pt).
% transforms the P part in v(_,P) into a readable term
p2term([X^P|Xs],Term) :-
(
Xs = [] ->
pe2term(X,Xt),
exp2term(P,Xt,Term)
;
Xs = [_|_] ->
Term = Xst*Xtp,
pe2term(X,Xt),
exp2term(P,Xt,Xtp),
p2term(Xs,Xst)
( Xs = []
-> pe2term(X,Xt),
exp2term(P,Xt,Term)
; Xs = [_|_]
-> Term = Xst*Xtp,
pe2term(X,Xt),
exp2term(P,Xt,Xtp),
p2term(Xs,Xst)
).
%
exp2term(1,X,X) :- !.
exp2term(-1,X,One/X) :-
!,
One = 1.0.
exp2term(-1,X,1.0/X) :- !.
exp2term(P,X,Term) :-
arith_normalize(P,Pn),
% Term = exp(X,Pn).
Term = X^Pn.
% Term = exp(X,Pn)
Term = X^P.
pe2term(X,Term) :-
var(X),
@ -1249,3 +1100,47 @@ pe2term_args([],[]).
pe2term_args([A|As],[T|Ts]) :-
nf2term(A,T),
pe2term_args(As,Ts).
% transg(Goal,[OutList|OutListTail],OutListTail)
%
% puts the equalities and inequalities that are implied by the elements in Goal
% in the difference list OutList
%
% called by geler.pl for project.pl
transg(resubmit_eq(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term=Z}].
transg(resubmit_lt(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term<Z}].
transg(resubmit_le(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term=<Z}].
transg(resubmit_ne(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term=\=Z}].
transg(wait_linear_retry(Nf,Res,Goal)) -->
{
nf2term(Nf,Term)
},
[clpr:{Term=Res},Goal].
integerp(X) :-
floor(X)=:=X.
integerp(X,I) :-
floor(X)=:=X,
I is integer(X).

306
LGPL/clpr/clpr/store.pl → GPL/clpqr/clpr/store_r.pl
View File

@ -1,9 +1,9 @@
/* $Id: store.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
/* $Id: store_r.pl,v 1.1 2008-03-13 17:16:43 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Part of CLP(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.be
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
@ -38,36 +38,29 @@
the GNU General Public License.
*/
:- module(store,
:- 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
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
]).
:- use_module(arith_r,
[
arith_normalize/2
]).
% normalize_scalar(S,[N,Z])
%
% Transforms a scalar S into a linear expression [S,0]
normalize_scalar(S,[N,Z]) :-
arith_normalize(S,N),
Z = 0.0.
normalize_scalar(S,[S,0.0]).
% renormalize(List,Lin)
%
@ -77,8 +70,7 @@ normalize_scalar(S,[N,Z]) :-
% the constant part of the linear expression; when a variable X is bound to
% another variable Y, the scalars of both are added)
renormalize(List,Lin) :-
List = [I,R|Hom],
renormalize([I,R|Hom],Lin) :-
length(Hom,Len),
renormalize_log(Len,Hom,[],Lin0),
add_linear_11([I,R],Lin0,Lin).
@ -113,9 +105,9 @@ renormalize_log(N,L0,L2,Lin) :-
renormalize_log_one(X,Term,Res) :-
var(X),
Term = l(X*K,_),
get_attr(X,itf3,(_,_,_,order(OrdX),_)), % Order might have changed
Z = 0.0,
Res = [Z,Z,l(X*K,OrdX)].
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,_),
@ -154,33 +146,23 @@ add_linear_ffh([l(X*Kx,OrdX)|Xs],Ka,Ys,Kb,Zs) :-
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,
(
TestKz is Kz - 0.0, % Kz =:= 0
TestKz =< 1e-010,
TestKz >= -1e-010 ->
!,
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)
( 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)
@ -210,32 +192,22 @@ add_linear_f1h([l(X*Kx,OrdX)|Xs],Ka,Ys,Zs) :-
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,
(
TestKz is Kz - 0.0, % Kz =:= 0
TestKz =< 1e-010,
TestKz >= -1e-010 ->
!,
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)
( 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)
@ -265,31 +237,21 @@ add_linear_11h([l(X*Kx,OrdX)|Xs],Ys,Zs) :-
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,
(
TestKz is Kz - 0.0, % Kz =:= 0
TestKz =< 1e-010,
TestKz >= -1e-010 ->
!,
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)
( 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)
@ -299,8 +261,8 @@ add_linear_11h([l(Y*Ky,OrdY)|Ys],X,Kx,OrdX,Xs,Zs) :-
mult_linear_factor(Lin,K,Mult) :-
TestK is K - 1.0, % K =:= 1
TestK =< 1e-010,
TestK >= -1e-010, % avoid copy
TestK =< 1.0e-10,
TestK >= -1.0e-10, % avoid copy
!,
Mult = Lin.
mult_linear_factor(Lin,K,Res) :-
@ -348,16 +310,12 @@ delete_factor(OrdV,Lin,Res,Coeff) :-
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)
( Rel= (=)
-> RCdr = Cdr,
RKoeff=Koeff
; Rel= (>)
-> RCdr = [Car|RCdr1],
delete_factor_hom(VOrd,Cdr,RCdr1,RKoeff)
).
@ -365,10 +323,8 @@ delete_factor_hom(VOrd,[Car|Cdr],RCdr,RKoeff) :-
%
% Linear expression Lin contains the term l(X*Coeff,OrdX)
nf_coeff_of(Lin,VOrd,Coeff) :-
Lin = [_,_|Hom],
nf_coeff_hom(Hom,VOrd,Coeff),
!.
nf_coeff_of([_,_|Hom],VOrd,Coeff) :-
nf_coeff_hom(Hom,VOrd,Coeff).
% nf_coeff_hom(Lin,OrdX,Coeff)
%
@ -377,14 +333,10 @@ nf_coeff_of(Lin,VOrd,Coeff) :-
nf_coeff_hom([l(_*K,OVar)|Vs],OVid,Coeff) :-
compare(Rel,OVid,OVar),
(
Rel = (=),
!,
Coeff = K
;
Rel = (>),
!,
nf_coeff_hom(Vs,OVid,Coeff)
( Rel = (=)
-> Coeff = K
; Rel = (>)
-> nf_coeff_hom(Vs,OVid,Coeff)
).
% nf_rhs_x(Lin,OrdX,Rhs,K)
@ -413,12 +365,13 @@ isolate(OrdN,Lin,Lin1) :-
indep(Lin,OrdX) :-
Lin = [I,_|[l(_*K,OrdY)]],
OrdX == OrdY,
TestK is K - 1.0, % K =:= 1
TestK =< 1e-010,
TestK >= -1e-010,
TestI is I - 0.0, % I =:= 0
TestI =< 1e-010,
TestI >= -1e-010.
% 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)
%
@ -427,29 +380,23 @@ indep(Lin,OrdX) :-
nf2sum([],I,I).
nf2sum([X|Xs],I,Sum) :-
(
TestI is I - 0.0, % I =:= 0
TestI =< 1e-010,
TestI >= -1e-010 ->
X = l(Var*K,_),
(
TestK is K - 1.0, % K =:= 1
TestK =< 1e-010,
TestK >= -1e-010 ->
hom2sum(Xs,Var,Sum)
;
TestK is K - -1.0, % K =:= -1
TestK =< 1e-010,
TestK >= -1e-010 ->
hom2sum(Xs,-Var,Sum)
;
hom2sum(Xs,K*Var,Sum)
)
;
hom2sum([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)
@ -461,25 +408,20 @@ nf2sum([X|Xs],I,Sum) :-
hom2sum([],Term,Term).
hom2sum([l(Var*K,_)|Cs],Sofar,Term) :-
(
TestK is K - 1.0, % K =:= 1
TestK =< 1e-010,
TestK >= -1e-010 ->
Next = Sofar + Var
;
TestK is K - -1.0, % K =:= -1
TestK =< 1e-010,
TestK >= -1e-010 ->
Next = Sofar - Var
;
K - 0.0 < -1e-010 ->
Ka is -K,
Next = Sofar - Ka*Var
;
Next = Sofar + K*Var
( % 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).

2
LGPL/chr/Makefile.in
View File

@ -44,7 +44,6 @@ LIBPL= $(srcdir)/chr_runtime.pl $(srcdir)/chr_op.pl chr_translate.pl $(srcdir)/
$(srcdir)/chr_compiler_options.pl $(srcdir)/chr_compiler_utility.pl \
$(srcdir)/chr_integertable_store.pl
CHRPL= $(srcdir)/chr_swi.pl
CHRYAP= $(srcdir)/chr.yap
EXAMPLES= $(srcdir)/Benchmarks/chrfreeze.chr $(srcdir)/Benchmarks/fib.chr $(srcdir)/Benchmarks/gcd.chr $(srcdir)/Benchmarks/primes.chr \
$(srcdir)/Benchmarks/bool.chr $(srcdir)/Benchmarks/family.chr $(srcdir)/Benchmarks/fibonacci.chr $(srcdir)/Benchmarks/leq.chr $(srcdir)/Benchmarks/listdom.chr \
$(srcdir)/Benchmarks/chrdif.chr
@ -90,7 +89,6 @@ install: chr_translate.pl guard_entailment.pl
mkdir -p $(DESTDIR)$(CHRDIR)
$(INSTALL) -m 644 $(LIBPL) $(DESTDIR)$(CHRDIR)
$(INSTALL) -m 644 $(CHRPL) $(DESTDIR)$(SHAREDIR)/chr.pl
$(INSTALL) -m 644 $(CHRYAP) $(DESTDIR)$(SHAREDIR)
$(INSTALL) -m 644 $(srcdir)/README $(DESTDIR)$(CHRDIR)
# $(PL) -g make -z halt

2
LGPL/chr/chr.yap
View File

@ -1,6 +1,4 @@
:- load_files(library(swi),[silent(true),if(not_loaded)]).
:- include('chr.pl').

4
LGPL/chr/chr_swi.pl
View File

@ -1,4 +1,4 @@
/* $Id: chr_swi.pl,v 1.3 2008-03-13 14:38:00 vsc Exp $
/* $Id: chr_swi.pl,v 1.4 2008-03-13 17:16:44 vsc Exp $
Part of CHR (Constraint Handling Rules)
@ -53,6 +53,8 @@
chr_leash/1 % +Ports
]).
:- expects_dialect(swi).
:- set_prolog_flag(generate_debug_info, false).
:- multifile user:file_search_path/2.

8
LGPL/clpr/clpr.yap
View File

@ -1,8 +0,0 @@
:- load_files(library(swi),[silent(true),if(not_loaded)]).
:- include('clpr.pl').

85
LGPL/clpr/clpr/arith_r.pl
View File

@ -1,85 +0,0 @@
/* $Id: arith_r.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.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(arith_r,
[
arith_eps/1,
arith_normalize/2,
integerp/1,
integerp/2
]).
arith_eps(1.0e-10). % for Monash #zero expansion 1.0e-12
eps(1.0e-10,-1.0e-10).
arith_normalize(X,Norm) :-
var(X),
!,
raise_exception(instantiation_error(arith_normalize(X,Norm),1)).
arith_normalize(rat(N,D),Norm) :- rat_float(N,D,Norm).
arith_normalize(X,Norm) :-
number(X),
Norm is float(X).
integerp(X) :-
floor(/*float?*/X)=:=X.
integerp(X,I) :-
floor(/*float?*/X)=:=X,
I is integer(X).
% copied from arith.pl.
rat_float(Nx,Dx,F) :-
limit_encoding_length(Nx,Dx,1023,Nxl,Dxl),
F is Nxl / Dxl.
limit_encoding_length(0,D,_,0,D) :- !. % msb ...
limit_encoding_length(N,D,Bits,Nl,Dl) :-
Shift is min(max(msb(abs(N)),msb(D))-Bits,
min(msb(abs(N)),msb(D))),
Shift > 0,
!,
Ns is N>>Shift,
Ds is D>>Shift,
Gcd is gcd(Ns,Ds),
Nl is Ns//Gcd,
Dl is Ds//Gcd.
limit_encoding_length(N,D,_,N,D).

1805
LGPL/clpr/clpr/bv.pl
View File

File diff suppressed because it is too large Load Diff

1530
LGPL/clpr/clpr/ineq.pl
View File

File diff suppressed because it is too large Load Diff

399
LGPL/clpr/clpr/itf3.pl
View File

@ -1,399 +0,0 @@
/* $Id: itf3.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.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.
*/
% attribute = (type(_),strictness(_),lin(_),order(_),class(_),forward(_),nonzero,
% target,keep_indep,keep)
:- module(itf3,
[
dump_linear/4,
dump_nonzero/4
]).
:- use_module(arith_r).
:- use_module(bv,
[
deref/2,
detach_bounds_vlv/5,
dump_var/6,
dump_nz/5,
solve/1,
solve_ord_x/3
]).
:- use_module(nf,
[
nf/2
]).
:- use_module(store,
[
add_linear_11/3,
indep/2,
nf_coeff_of/3
]).
:- use_module(class,
[
class_drop/2
]).
this_linear_solver(clpr).
%
% Parametrize the answer presentation mechanism
% (toplevel,compiler/debugger ...)
%
:- dynamic presentation_context/1.
% replaces the old presentation context by a new one.
presentation_context(Old,New) :-
clause(presentation_context(Current), _),
!,
Current = Old,
retractall(presentation_context(_)),
assert(presentation_context(New)).
presentation_context(toplevel,New) :- assert(presentation_context(New)). %default
%
% attribute_goal( V, V:Atts) :- get_atts( V, Atts).
%
attribute_goal(V,Goal) :-
presentation_context(Cont,Cont),
dump_linear(V,Cont,Goals,Gtail),
dump_nonzero(V,Cont,Gtail,[]),
l2wrapped(Goals,Goal).
l2wrapped([],true).
l2wrapped([X|Xs],Conj) :-
(
Xs = [],
wrap(X,Conj)
;
Xs = [_|_],
wrap(X,Xw),
Conj = (Xw,Xc),
l2wrapped(Xs,Xc)
).
%
% Tests should be pulled out of the loop ...
%
wrap(C,W) :-
prolog_flag(typein_module,Module),
this_linear_solver(Solver),
(
Module == Solver ->
W = {C}
;
predicate_property(Module:{_},imported_from(Solver)) ->
W = {C}
;
W = Solver:{C}
).
dump_linear(V,Context) -->
{
get_attr(V,itf3,(type(Type),_,lin(Lin),_)),
!,
Lin = [I,_|H]
},
%
% This happens if not all target variables can be made independend
% Example: examples/option.pl:
% | ?- go2(S,W).
%
% W = 21/4,
% S>=0,
% S<50 ? ;
%
% W>5,
% S=221/4-W, this line would be missing !!!
% W=<21/4
%
(
{Type=t_none; get_attr(V,itf3,(_,_,_,_,_,_,_,n,_))} ->
[]
;
dump_v(Context,t_none,V,I,H)
),
%
(
{Type=t_none, get_attr(V,itf3,(_,_,_,_,_,_,_,n,_)) } -> % nonzero produces such
[]
;
dump_v(Context,Type,V,I,H)
).
dump_linear(_,_) --> [].
dump_v(toplevel,Type,V,I,H) --> dump_var(Type,V,I,H).
% dump_v(compiler,Type,V,I,H) --> compiler_dump_var(Type,V,I,H).
dump_nonzero(V,Cont) -->
{
get_attr(V,itf3,(_,_,lin(Lin),_,_,_,nonzero,_)),
!,
Lin = [I,_|H]
},
dump_nz(Cont,V,H,I).
dump_nonzero(_,_) --> [].
dump_nz(toplevel,V,H,I) --> dump_nz(V,H,I).
% dump_nz(compiler,V,H,I) --> compiler_dump_nz(V,H,I).
numbers_only(Y) :-
var(Y),
!.
numbers_only(Y) :-
arith_normalize(Y,Y),
!.
numbers_only(Y) :-
this_linear_solver(Solver),
(
Solver == clpr ->
What = 'a real number'
;
Solver == clpq ->
What = 'a rational number'
),
raise_exception(type_error(_X = Y,2,What,Y)).
attr_unify_hook((n,n,n,n,n,n,n,_),_) :- !.
attr_unify_hook((_,_,_,_,_,forward(F),_),Y) :-
!,
fwd_deref(F,Y).
attr_unify_hook((Ty,St,Li,Or,Cl,_,No,_),Y) :-
% numbers_only(Y),
verify_nonzero(No,Y),
verify_type(Ty,St,Y,Later,[]),
verify_lin(Or,Cl,Li,Y),
call_list(Later).
% call_list(List)
%
% Calls all the goals in List.
call_list([]).
call_list([G|Gs]) :-
call(G),
call_list(Gs).
%%%%
fwd_deref(X,Y) :-
nonvar(X),
X = Y.
fwd_deref(X,Y) :-
var(X),
(
get_attr(X,itf3,itf(_,_,_,forward(F),_,_,_,_,_,_)) ->
fwd_deref(F,Y)
;
X = 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,itf3,itf(A,B,C,D,E,F,_,H,I,J)) ->
put_attr(Y,itf3,itf(A,B,C,D,E,F,nonzero,H,I,J))
;
put_attr(Y,itf3,itf(n,n,n,n,n,n,nonzero,n,n,n))
)
;
TestY = Y - 0.0, % Y =\= 0
(
TestY < -1e-010 ->
true
;
TestY > 1e-010
)
).
verify_nonzero(_,_). % 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(_,_,_) --> [].
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,_,_). % no bounds
verify_type_nonvar(t_l(L),Value,S) :- ilb(S,L,Value). % passive lower bound
verify_type_nonvar(t_u(U),Value,S) :- iub(S,U,Value). % passive upper bound
verify_type_nonvar(t_lu(L,U),Value,S) :- % passive lower and upper bound
ilb(S,L,Value),
iub(S,U,Value).
verify_type_nonvar(t_L(L),Value,S) :- ilb(S,L,Value). % active lower bound
verify_type_nonvar(t_U(U),Value,S) :- iub(S,U,Value). % active upper bound
verify_type_nonvar(t_Lu(L,U),Value,S) :- % active lower and passive upper bound
ilb(S,L,Value),
iub(S,U,Value).
verify_type_nonvar(t_lU(L,U),Value,S) :- % passive lower and active upper bound
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 < 1e-010.
ilb(_,L,V) :- L - V < -1e-010.
iub(S,U,V) :-
S /\ 1 =:= 0,
!,
V - U < 1e-010.
iub(_,U,V) :- V - U < -1e-010.
%
% 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,_,_) --> []. % no bounds, no inequalities
verify_type_var(t_l(L),Y,S) --> llb(S,L,Y). % passive lower bound
verify_type_var(t_u(U),Y,S) --> lub(S,U,Y). % passive upper bound
verify_type_var(t_lu(L,U),Y,S) --> % passive lower and upper bound
llb(S,L,Y),
lub(S,U,Y).
verify_type_var(t_L(L),Y,S) --> llb(S,L,Y). % active lower bound
verify_type_var(t_U(U),Y,S) --> lub(S,U,Y). % active upper bound
verify_type_var(t_Lu(L,U),Y,S) --> % active lower and passive upper bound
llb(S,L,Y),
lub(S,U,Y).
verify_type_var(t_lU(L,U),Y,S) --> % passive lower and active upper bound
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},
!,
[{L =< V}].
llb(_,L,V) --> [{L < V}].
lub(S,U,V) -->
{S /\ 1 =:= 0},
!,
[{V =< U}].
lub(_,U,V) --> [{V < U}].
%
% We used to drop X from the class/basis to avoid trouble with subsequent
% put_atts/2 on X. Now we could let these dead but harmless updates happen.
% In R however, exported bindings might conflict, e.g. 0 \== 0.0
%
% If X is indep and we do _not_ solve for it, we are in deep shit
% because the ordering is violated.
%
verify_lin(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(_,_,_,_).

87
LGPL/clpr/clpr/nfr.pl
View File

@ -1,87 +0,0 @@
/* $Id: nfr.pl,v 1.1 2005-10-28 17:51:01 vsc Exp $
Part of CPL(R) (Constraint Logic Programming over Reals)
Author: Leslie De Koninck
E-mail: Tom.Schrijvers@cs.kuleuven.ac.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(nfr,
[
transg/3
]).
:- use_module(nf,
[
nf2term/2
]).
% transg(Goal,[OutList|OutListTail],OutListTail)
%
% puts the equalities and inequalities that are implied by the elements in Goal
% in the difference list OutList
%
% called by geler.pl for project.pl
transg(resubmit_eq(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term=Z}].
transg(resubmit_lt(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term<Z}].
transg(resubmit_le(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term=<Z}].
transg(resubmit_ne(Nf)) -->
{
nf2term([],Z),
nf2term(Nf,Term)
},
[clpr:{Term=\=Z}].
transg(wait_linear_retry(Nf,Res,Goal)) -->
{
nf2term(Nf,Term)
},
[clpr:{Term=Res},Goal].

828
LGPL/clpr/clpr/ugraphs.pl
View File

@ -1,828 +0,0 @@
/* Copyright(C) 1992, Swedish Institute of Computer Science */
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File : UGRAPHS.PL %
% Maintainer : Mats Carlsson %
% New versions of transpose/2, reduce/2, top_sort/2 by Dan Sahlin %
% Updated: 3 September 1999 %
% Purpose: Unweighted graph-processing utilities %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/* Adapted from shared code written by Richard A O'Keefe */
/* An unweighted directed graph (ugraph) is represented as a list of
(vertex-neighbors) pairs, where the pairs are in standard order
(as produced by keysort with unique keys) and the neighbors of
each vertex are also in standard order (as produced by sort), and
every neighbor appears as a vertex even if it has no neighbors
itself.
An undirected graph is represented as a directed graph where for
each edge (U,V) there is a symmetric edge (V,U).
An edge (U,V) is represented as the term U-V.
A vertex can be any term. Two vertices are distinct iff they are
not identical (==).
A path is represented as a list of vertices.
No vertex can appear twice in a path.
*/
:- module(ugraphs, [
vertices_edges_to_ugraph/3,
vertices/2,
edges/2,
add_vertices/3,
del_vertices/3,
add_edges/3,
del_edges/3,
transpose/2,
neighbors/3,
neighbours/3,
complement/2,
compose/3,
transitive_closure/2,
symmetric_closure/2,
top_sort/2,
max_path/5,
min_path/5,
min_paths/3,
path/3,
reduce/2,
reachable/3,
random_ugraph/3,
min_tree/3,
clique/3,
independent_set/3,
coloring/3,
colouring/3
]).
:- use_module(library(ordsets),
[ ord_del_element/3,
ord_add_element/3,
ord_subset/2,
ord_union/3,
ord_union/4,
ord_disjoint/2,
ord_intersection/3
]).
:- use_module(library(lists), [
append/3,
member/2,
reverse/2
]).
:- use_module(library(assoc), [
list_to_assoc/2,
ord_list_to_assoc/2,
get_assoc/3,
get_assoc/5
]).
/*:- use_module(random, [
random/1
]).
*/
% vertices_edges_to_ugraph(+Vertices, +Edges, -Graph)
% is true if Vertices is a list of vertices, Edges is a list of edges,
% and Graph is a graph built from Vertices and Edges. Vertices and
% Edges may be in any order. The vertices mentioned in Edges do not
% have to occur explicitly in Vertices. Vertices may be used to
% specify vertices that are not connected to any edges.
vertices_edges_to_ugraph(Vertices0, Edges, Graph) :-
sort(Vertices0, Vertices1),
sort(Edges, EdgeSet),
edges_vertices(EdgeSet, Bag),
sort(Bag, Vertices2),
ord_union(Vertices1, Vertices2, VertexSet),
group_edges(VertexSet, EdgeSet, Graph).
edges_vertices([], []).
edges_vertices([From-To|Edges], [From,To|Vertices]) :-
edges_vertices(Edges, Vertices).
group_edges([], _, []).
group_edges([Vertex|Vertices], Edges, [Vertex-Neibs|G]) :-
group_edges(Edges, Vertex, Neibs, RestEdges),
group_edges(Vertices, RestEdges, G).
group_edges([V0-X|Edges], V, [X|Neibs], RestEdges) :- V0==V, !,
group_edges(Edges, V, Neibs, RestEdges).
group_edges(Edges, _, [], Edges).
% vertices(+Graph, -Vertices)
% unifies Vertices with the vertices in Graph.
vertices([], []).
vertices([Vertex-_|Graph], [Vertex|Vertices]) :- vertices(Graph, Vertices).
% edges(+Graph, -Edges)
% unifies Edges with the edges in Graph.
edges([], []).
edges([Vertex-Neibs|G], Edges) :-
edges(Neibs, Vertex, Edges, MoreEdges),
edges(G, MoreEdges).
edges([], _, Edges, Edges).
edges([Neib|Neibs], Vertex, [Vertex-Neib|Edges], MoreEdges) :-
edges(Neibs, Vertex, Edges, MoreEdges).
% add_vertices(+Graph1, +Vertices, -Graph2)
% is true if Graph2 is Graph1 with Vertices added to it.
add_vertices(Graph0, Vs0, Graph) :-
sort(Vs0, Vs),
vertex_units(Vs, Graph1),
graph_union(Graph0, Graph1, Graph).
% del_vertices(+Graph1, +Vertices, -Graph2)
% is true if Graph2 is Graph1 with Vertices and all edges to and from
% Vertices removed from it.
del_vertices(Graph0, Vs0, Graph) :-
sort(Vs0, Vs),
graph_del_vertices(Graph0, Vs, Vs, Graph).
% add_edges(+Graph1, +Edges, -Graph2)
% is true if Graph2 is Graph1 with Edges and their "to" and "from"
% vertices added to it.
add_edges(Graph0, Edges0, Graph) :-
sort(Edges0, EdgeSet),
edges_vertices(EdgeSet, Vs0),
sort(Vs0, Vs),
group_edges(Vs, EdgeSet, Graph1),
graph_union(Graph0, Graph1, Graph).
% del_edges(+Graph1, +Edges, -Graph2)
% is true if Graph2 is Graph1 with Edges removed from it.
del_edges(Graph0, Edges0, Graph) :-
sort(Edges0, EdgeSet),
edges_vertices(EdgeSet, Vs0),
sort(Vs0, Vs),
group_edges(Vs, EdgeSet, Graph1),
graph_difference(Graph0, Graph1, Graph).
vertex_units([], []).
vertex_units([V|Vs], [V-[]|Us]) :- vertex_units(Vs, Us).
graph_union(G0, [], G) :- !, G = G0.
graph_union([], G, G).
graph_union([V1-N1|G1], [V2-N2|G2], G) :-
compare(C, V1, V2),
graph_union(C, V1, N1, G1, V2, N2, G2, G).
graph_union(<, V1, N1, G1, V2, N2, G2, [V1-N1|G]) :-
graph_union(G1, [V2-N2|G2], G).
graph_union(=, V, N1, G1, _, N2, G2, [V-N|G]) :-
ord_union(N1, N2, N),
graph_union(G1, G2, G).
graph_union(>, V1, N1, G1, V2, N2, G2, [V2-N2|G]) :-
graph_union([V1-N1|G1], G2, G).
graph_difference(G0, [], G) :- !, G = G0.
graph_difference([], _, []).
graph_difference([V1-N1|G1], [V2-N2|G2], G) :-
compare(C, V1, V2),
graph_difference(C, V1, N1, G1, V2, N2, G2, G).
graph_difference(<, V1, N1, G1, V2, N2, G2, [V1-N1|G]) :-
graph_difference(G1, [V2-N2|G2], G).
graph_difference(=, V, N1, G1, _, N2, G2, [V-N|G]) :-
ord_subtract(N1, N2, N),
graph_difference(G1, G2, G).
graph_difference(>, V1, N1, G1, _, _, G2, G) :-
graph_difference([V1-N1|G1], G2, G).
graph_del_vertices(G1, [], Set, G) :- !,
graph_del_vertices(G1, Set, G).
graph_del_vertices([], _, _, []).
graph_del_vertices([V1-N1|G1], [V2|Vs], Set, G) :-
compare(C, V1, V2),
graph_del_vertices(C, V1, N1, G1, V2, Vs, Set, G).
graph_del_vertices(<, V1, N1, G1, V2, Vs, Set, [V1-N|G]) :-
ord_subtract(N1, Set, N),
graph_del_vertices(G1, [V2|Vs], Set, G).
graph_del_vertices(=, _, _, G1, _, Vs, Set, G) :-
graph_del_vertices(G1, Vs, Set, G).
graph_del_vertices(>, V1, N1, G1, _, Vs, Set, G) :-
graph_del_vertices([V1-N1|G1], Vs, Set, G).
graph_del_vertices([], _, []).
graph_del_vertices([V1-N1|G1], Set, [V1-N|G]) :-
ord_subtract(N1, Set, N),
graph_del_vertices(G1, Set, G).
% transpose(+Graph, -Transpose)
% is true if Transpose is the graph computed by replacing each edge
% (u,v) in Graph by its symmetric edge (v,u). It can only be used
% one way around. The cost is O(N log N).
transpose(Graph, Transpose) :-
transpose_edges(Graph, TEdges, []),
sort(TEdges, TEdges2),
vertices(Graph, Vertices),
group_edges(Vertices, TEdges2, Transpose).
transpose_edges([]) --> [].
transpose_edges([Vertex-Neibs|G]) -->
transpose_edges(Neibs, Vertex),
transpose_edges(G).
transpose_edges([], _) --> [].
transpose_edges([Neib|Neibs], Vertex) --> [Neib-Vertex],
transpose_edges(Neibs, Vertex).
% neighbours(+Vertex, +Graph, -Neighbors)
% neighbors(+Vertex, +Graph, -Neighbors)
% is true if Vertex is a vertex in Graph and Neighbors are its neighbors.
neighbours(Vertex, Graph, Neighbors) :-
neighbors(Vertex, Graph, Neighbors).
neighbors(V, [V0-Neighbors|_], Neighbors) :- V0==V, !.
neighbors(V, [_|Graph], Neighbors) :- neighbors(V, Graph, Neighbors).
% complement(+Graph, -Complement)
% Complement is the complement graph of Graph, i.e. the graph that has
% the same vertices as Graph but only the edges that are not in Graph.
complement(Graph, Complement) :-
vertices(Graph, Vertices),
complement(Graph, Vertices, Complement).
complement([], _, []).
complement([V-Neibs|Graph], Vertices, [V-Others|Complement]) :-
ord_add_element(Neibs, V, Neibs1),
ord_subtract(Vertices, Neibs1, Others),
complement(Graph, Vertices, Complement).
% compose(+G1, +G2, -Composition)
% computes Composition as the composition of two graphs, which need
% not have the same set of vertices.
compose(G1, G2, Composition) :-
vertices(G1, V1),
vertices(G2, V2),
ord_union(V1, V2, V),
compose(V, G1, G2, Composition).
compose([], _, _, []).
compose([V0|Vertices], [V-Neibs|G1], G2, [V-Comp|Composition]) :- V==V0, !,
compose1(Neibs, G2, [], Comp),
compose(Vertices, G1, G2, Composition).
compose([V|Vertices], G1, G2, [V-[]|Composition]) :-
compose(Vertices, G1, G2, Composition).
compose1([V1|Vs1], [V2-N2|G2], SoFar, Comp) :- !,
compare(Rel, V1, V2),
compose1(Rel, V1, Vs1, V2, N2, G2, SoFar, Comp).
compose1(_, _, Comp, Comp).
compose1(<, _, Vs1, V2, N2, G2, SoFar, Comp) :-
compose1(Vs1, [V2-N2|G2], SoFar, Comp).
compose1(>, V1, Vs1, _, _, G2, SoFar, Comp) :-
compose1([V1|Vs1], G2, SoFar, Comp).
compose1(=, V1, Vs1, V1, N2, G2, SoFar, Comp) :-
ord_union(N2, SoFar, Next),
compose1(Vs1, G2, Next, Comp).
% transitive_closure(+Graph, -Closure)
% computes Closure as the transitive closure of Graph in O(N^3) time.
transitive_closure(Graph, Closure) :-
warshall(Graph, Graph, Closure).
warshall([], Closure, Closure).
warshall([V-_|G], E, Closure) :-
neighbors(V, E, Y),
warshall(E, V, Y, NewE),
warshall(G, NewE, Closure).
warshall([], _, _, []).
warshall([X-Neibs|G], V, Y, [X-NewNeibs|NewG]) :-
ord_subset([V], Neibs), !,
ord_del_element(Y, X, Y1),
ord_union(Neibs, Y1, NewNeibs),
warshall(G, V, Y, NewG).
warshall([X-Neibs|G], V, Y, [X-Neibs|NewG]) :-
warshall(G, V, Y, NewG).
% symmetric_closure(+Graph, -Closure)
% computes Closure as the symmetric closure of Graph, i.e. for each
% edge (u,v) in Graph, add its symmetric edge (v,u). Approx O(N log N)
% time. This is useful for making a directed graph undirected.
symmetric_closure(Graph, Closure) :-
transpose(Graph, Transpose),
symmetric_closure(Graph, Transpose, Closure).
symmetric_closure([], [], []).
symmetric_closure([V-Neibs1|Graph], [V-Neibs2|Transpose], [V-Neibs|Closure]) :-
ord_union(Neibs1, Neibs2, Neibs),
symmetric_closure(Graph, Transpose, Closure).
% top_sort(+Graph, -Sorted)
% finds a topological ordering of a Graph and returns the ordering
% as a list of Sorted vertices. Fails iff no ordering exists, i.e.
% iff the graph contains cycles. Approx O(N log N) time.
top_sort(Graph, Sorted) :-
fanin_counts(Graph, Counts),
get_top_elements(Counts, Top, 0, I),
ord_list_to_assoc(Counts, Map),
top_sort(Top, I, Map, Sorted).
top_sort([], 0, _, []).
top_sort([V-VN|Top0], I, Map0, [V|Sorted]) :-
dec_counts(VN, I, J, Map0, Map, Top0, Top),
top_sort(Top, J, Map, Sorted).
dec_counts([], I, I, Map, Map, Top, Top).
dec_counts([N|Ns], I, K, Map0, Map, Top0, Top) :-
get_assoc(N, Map0, NN-C0, Map1, NN-C),
C is C0-1,
(C=:=0 -> J is I-1, Top1 = [N-NN|Top0]; J = I, Top1 = Top0),
dec_counts(Ns, J, K, Map1, Map, Top1, Top).
get_top_elements([], [], I, I).
get_top_elements([V-(VN-C)|Counts], Top0, I, K) :-
(C=:=0 -> J = I, Top0 = [V-VN|Top1]; J is I+1, Top0 = Top1),
get_top_elements(Counts, Top1, J, K).
fanin_counts(Graph, Counts) :-
transpose_edges(Graph, Edges0, []),
keysort(Edges0, Edges),
fanin_counts(Graph, Edges, Counts).
fanin_counts([], [], []).
fanin_counts([V-VN|Graph], Edges, [V-(VN-C)|Counts]) :-
fanin_counts(Edges, V, 0, C, Edges1),
fanin_counts(Graph, Edges1, Counts).
fanin_counts([V-_|Edges0], V0, C0, C, Edges) :-
V==V0, !,
C1 is C0+1,
fanin_counts(Edges0, V0, C1, C, Edges).
fanin_counts(Edges, _, C, C, Edges).
% max_path(+V1, +V2, +Graph, -Path, -Cost)
% is true if Path is a list of vertices constituting a longest path
% of cost Cost from V1 to V2 in Graph, there being no cyclic paths from
% V1 to V2. Takes O(N^2) time.
max_path(Initial, Final, Graph, Path, Cost) :-
transpose(Graph, TGraph),
max_path_init(Initial, Final, Graph, TGraph, TGraph2, Order),
max_path_init(TGraph2, Val0),
max_path(Order, TGraph2, Val0, Val),
max_path_select(Val, Path, Cost).
max_path_init(Initial, Final, Graph, TGraph, TGraph2, Order) :-
reachable(Initial, Graph, InitialReachable),
reachable(Final, TGraph, FinalReachable),
ord_intersection(InitialReachable, FinalReachable, Reachable),
subgraph(TGraph, Reachable, TGraph2),
top_sort(TGraph2, Order).
max_path_init([], []).
max_path_init([V-_|G], [V-([]-0)|Val]) :- max_path_init(G, Val).
max_path_select([V-(Longest-Max)|Val], Path, Cost) :-
max_path_select(Val, V, Longest, Path, Max, Cost).
max_path_select([], V, Path, [V|Path], Cost, Cost).
max_path_select([V1-(Path1-Cost1)|Val], V2, Path2, Path, Cost2, Cost) :-
( Cost1>Cost2 ->
max_path_select(Val, V1, Path1, Path, Cost1, Cost)
; max_path_select(Val, V2, Path2, Path, Cost2, Cost)
).
max_path([], _, Val, Val).
max_path([V|Order], Graph, Val0, Val) :-
neighbors(V, Graph, Neibs),
neighbors(V, Val0, Item),
max_path_update(Neibs, V-Item, Val0, Val1),
max_path(Order, Graph, Val1, Val).
%% [MC] 3.8.6: made determinate
max_path_update([], _, Val, Val).
max_path_update([N|Neibs], Item, [Item0|Val0], Val) :-
Item0 = V0-(_-Cost0),
N==V0, !,
Item = V-(Path-Cost),
Cost1 is Cost+1,
( Cost1>Cost0 -> Val = [V0-([V|Path]-Cost1)|Val1]
; Val = [Item0|Val1]
),
max_path_update(Neibs, Item, Val0, Val1).
max_path_update(Neibs, Item, [X|Val0], [X|Val]) :-
Neibs = [_|_],
max_path_update(Neibs, Item, Val0, Val).
subgraph([], _, []).
subgraph([V-Neibs|Graph], Vs, [V-Neibs1|Subgraph]) :-
ord_subset([V], Vs), !,
ord_intersection(Neibs, Vs, Neibs1),
subgraph(Graph, Vs, Subgraph).
subgraph([_|Graph], Vs, Subgraph) :-
subgraph(Graph, Vs, Subgraph).
% min_path(+V1, +V2, +Graph, -Path, -Length)
% is true if Path is a list of vertices constituting a shortest path
% of length Length from V1 to V2 in Graph. Takes O(N^2) time.
min_path(Initial, Final, Graph, Path, Length) :-
min_path([[Initial]|Q], Q, [Initial], Final, Graph, Rev),
reverse(Rev, Path),
length(Path, N),
Length is N-1.
min_path(Head0, Tail0, Closed0, Final, Graph, Rev) :-
Head0 \== Tail0,
Head0 = [Sofar|Head],
Sofar = [V|_],
( V==Final -> Rev = Sofar
; neighbors(V, Graph, Neibs),
ord_union(Closed0, Neibs, Closed, Neibs1),
enqueue(Neibs1, Sofar, Tail0, Tail),
min_path(Head, Tail, Closed, Final, Graph, Rev)
).
enqueue([], _) --> [].
enqueue([V|Vs], Sofar) --> [[V|Sofar]], enqueue(Vs, Sofar).
% min_paths(+Vertex, +Graph, -Tree)
% is true if Tree is a tree of all the shortest paths from Vertex to
% every other vertex in Graph. This is the single-source shortest
% paths problem. The algorithm is straightforward.
min_paths(Vertex, Graph, Tree) :-
min_paths([Vertex], Graph, [Vertex], List),
keysort(List, Tree).
min_paths([], _, _, []).
min_paths([Q|R], Graph, Reach0, [Q-New|List]) :-
neighbors(Q, Graph, Neibs),
ord_union(Reach0, Neibs, Reach, New),
append(R, New, S),
min_paths(S, Graph, Reach, List).
% path(+Vertex, +Graph, -Path)
% is given a Graph and a Vertex of that Graph, and returns a maximal
% Path rooted at Vertex, enumerating more Paths on backtracking.
path(Initial, Graph, Path) :-
path([Initial], [], Graph, Path).
path(Q, Not, Graph, Path) :-
Q = [Qhead|_],
neighbors(Qhead, Graph, Neibs),
ord_subtract(Neibs, Not, Neibs1),
( Neibs1 = [] -> reverse(Q, Path)
; ord_add_element(Not, Qhead, Not1),
member(N, Neibs1),
path([N|Q], Not1, Graph, Path)
).
% reduce(+Graph, -Reduced)
% is true if Reduced is the reduced graph for Graph. The vertices of
% the reduced graph are the strongly connected components of Graph.
% There is an edge in Reduced from u to v iff there is an edge in
% Graph from one of the vertices in u to one of the vertices in v. A
% strongly connected component is a maximal set of vertices where
% each vertex has a path to every other vertex.
% Algorithm from "Algorithms" by Sedgewick, page 482, Tarjan's algorithm.
% Approximately linear in the maximum of arcs and nodes (O(N log N)).
reduce(Graph, Reduced) :-
strong_components(Graph, SCCS, Map),
reduced_vertices_edges(Graph, Vertices, Map, Edges, []),
sort(Vertices, Vertices1),
sort(Edges, Edges1),
group_edges(Vertices1, Edges1, Reduced),
sort(SCCS, Vertices1).
strong_components(Graph, SCCS, A) :-
nodeinfo(Graph, Nodeinfo, Vertices),
ord_list_to_assoc(Nodeinfo, A0),
visit(Vertices, 0, _, A0, A, 0, _, [], _, SCCS, []).
visit([], Min, Min, A, A, I, I, Stk, Stk) --> [].
visit([V|Vs], Min0, Min, A0, A, I, M, Stk0, Stk) -->
{get_assoc(V, A0, node(Ns,J,Eq), A1, node(Ns,K,Eq))},
( {J>0} ->
{J=K, J=Min1, A1=A3, I=L, Stk0=Stk2}
; {K is I+1},
visit(Ns, K, Min1, A1, A2, K, L, [V|Stk0], Stk1),
( {K>Min1} -> {A2=A3, Stk1=Stk2}
; pop(V, Eq, A2, A3, Stk1, Stk2, [])
)
),
{Min2 is min(Min0,Min1)},
visit(Vs, Min2, Min, A3, A, L, M, Stk2, Stk).
pop(V, Eq, A0, A, [V1|Stk0], Stk, SCC0) -->
{get_assoc(V1, A0, node(Ns,_,Eq), A1, node(Ns,16'100000,Eq))},
( {V==V1} -> [SCC], {A1=A, Stk0=Stk, sort([V1|SCC0], SCC)}
; pop(V, Eq, A1, A, Stk0, Stk, [V1|SCC0])
).
nodeinfo([], [], []).
nodeinfo([V-Ns|G], [V-node(Ns,0,_)|Nodeinfo], [V|Vs]) :-
nodeinfo(G, Nodeinfo, Vs).
reduced_vertices_edges([], [], _) --> [].
reduced_vertices_edges([V-Neibs|Graph], [V1|Vs], Map) -->
{get_assoc(V, Map, N), N=node(_,_,V1)},
reduced_edges(Neibs, V1, Map),
reduced_vertices_edges(Graph, Vs, Map).
reduced_edges([], _, _) --> [].
reduced_edges([V|Vs], V1, Map) -->
{get_assoc(V, Map, N), N=node(_,_,V2)},
({V1==V2} -> []; [V1-V2]),
reduced_edges(Vs, V1, Map).
% reachable(+Vertex, +Graph, -Reachable)
% is given a Graph and a Vertex of that Graph, and returns the set
% of vertices that are Reachable from that Vertex. Takes O(N^2)
% time.
reachable(Initial, Graph, Reachable) :-
reachable([Initial], Graph, [Initial], Reachable).
reachable([], _, Reachable, Reachable).
reachable([Q|R], Graph, Reach0, Reachable) :-
neighbors(Q, Graph, Neighbors),
ord_union(Reach0, Neighbors, Reach1, New),
append(R, New, S),
reachable(S, Graph, Reach1, Reachable).
% random_ugraph(+P, +N, -Graph)
% where P is a probability, unifies Graph with a random graph of N
% vertices where each possible edge is included with probability P.
random_ugraph(P, N, Graph) :-
( float(P), P >= 0.0, P =< 1.0 -> true
; prolog:illarg(domain(float,between(0.0,1.0)),
random_ugraph(P,N,Graph), 1)
),
( integer(N), N >= 0 -> true
; prolog:illarg(domain(integer,>=(0)),
random_ugraph(P,N,Graph), 2)
),
random_ugraph(0, N, P, Graph).
random_ugraph(N, N, _, Graph) :- !, Graph = [].
random_ugraph(I, N, P, [J-List|Graph]) :-
J is I+1,
random_neighbors(N, J, P, List, []),
random_ugraph(J, N, P, Graph).
random_neighbors(0, _, _, S0, S) :- !, S = S0.
random_neighbors(N, J, P, S0, S) :-
( N==J -> S1 = S
; random(X), X > P -> S1 = S
; S1 = [N|S]
),
M is N-1,
random_neighbors(M, J, P, S0, S1).
random(X) :- % JW: was undefined. Assume
X is random(10000)/10000. % we need 0<=X<=1
% min_tree(+Graph, -Tree, -Cost)
% is true if Tree is a spanning tree of an *undirected* Graph with
% cost Cost, if it exists. Using a version of Prim's algorithm.
min_tree([V-Neibs|Graph], Tree, Cost) :-
length(Graph, Cost),
prim(Cost, Neibs, Graph, [V], Edges),
vertices_edges_to_ugraph([], Edges, Tree).
%% [MC] 3.8.6: made determinate
prim(0, [], _, _, []) :- !.
prim(I, [V|Vs], Graph, Reach, [V-W,W-V|Edges]) :-
neighbors(V, Graph, Neibs),
ord_subtract(Neibs, Reach, Neibs1),
ord_subtract(Neibs, Neibs1, [W|_]),
ord_add_element(Reach, V, Reach1),
ord_union(Vs, Neibs1, Vs1),
J is I-1,
prim(J, Vs1, Graph, Reach1, Edges).
% clique(+Graph, +K, -Clique)
% is true if Clique is a maximal clique (complete subgraph) of N
% vertices of an *undirected* Graph, where N>=K. Adapted from
% Algorithm 457, "Finding All Cliques of an Undirected Graph [H]",
% Version 1, by Coen Bron and Joep Kerbosch, CACM vol. 6 no. 9 pp.
% 575-577, Sept. 1973.
clique(Graph, K, Clique) :-
( integer(K), K >= 0 -> true
; prolog:illarg(domain(integer,>=(0)),
clique(Graph,K,Clique), 2)
),
J is K-1,
prune(Graph, [], J, Graph1),
clique1(Graph1, J, Clique).
clique1([], J, []) :- J < 0.
clique1([C-Neibs|Graph], J, [C|Clique]) :-
neighbor_graph(Graph, Neibs, C, Vs, Graph1),
J1 is J-1,
prune(Graph1, Vs, J1, Graph2),
clique1(Graph2, J1, Clique).
clique1([C-Neibs|Graph], J, Clique) :-
prune(Graph, [C], J, Graph2),
clique1(Graph2, J, Clique),
\+ ord_subset(Clique, Neibs).
neighbor_graph([], _, _, [], []).
neighbor_graph([V0-Neibs0|Graph0], [V|Vs], W, Del, [V-Neibs|Graph]) :-
V0==V, !,
ord_del_element(Neibs0, W, Neibs),
neighbor_graph(Graph0, Vs, W, Del, Graph).
neighbor_graph([V-_|Graph0], Vs, W, [V|Del], Graph) :-
neighbor_graph(Graph0, Vs, W, Del, Graph).
prune(Graph0, [], K, Graph) :- K =< 0, !, Graph = Graph0.
prune(Graph0, Vs0, K, Graph) :-
prune(Graph0, Vs0, K, Graph1, Vs1),
( Vs1==[] -> Graph = Graph1
; prune(Graph1, Vs1, K, Graph)
).
prune([], _, _, [], []).
prune([V-Ns0|Graph0], Vs1, K, [V-Ns|Graph], Vs2) :-
ord_disjoint([V], Vs1),
ord_subtract(Ns0, Vs1, Ns),
length(Ns, I),
I >= K, !,
prune(Graph0, Vs1, K, Graph, Vs2).
prune([V-_|Graph0], Vs1, K, Graph, Vs2) :-
( ord_disjoint([V], Vs1) -> Vs2 = [V|Vs3]
; Vs2 = Vs3
),
prune(Graph0, Vs1, K, Graph, Vs3).
% independent_set(+Graph, +K, -Set)
% is true if Set is a maximal independent (unconnected) set of N
% vertices of an *undirected* Graph, where N>=K.
independent_set(Graph, K, Set) :-
complement(Graph, Complement),
clique(Complement, K, Set).
% colouring(+Graph, +K, -Coloring)
% coloring(+Graph, +K, -Coloring)
% is true if Coloring is a mapping from vertices to colors 1..N of
% an *undirected* Graph such that all edges have distinct end colors,
% where N=<K. Adapted from "New Methods to Color the Vertices of a
% Graph", by D. Brelaz, CACM vol. 4 no. 22 pp. 251-256, April 1979.
% Augmented with ideas from Matula's smallest-last ordering.
colouring(Graph, K, Coloring) :-
coloring(Graph, K, Coloring).
coloring(Graph, K, Coloring) :-
( integer(K), K >= 0 -> true
; prolog:illarg(domain(integer,>=(0)),
coloring(Graph,K,Coloring), 2)
),
color_map(Graph, Coloring),
color_map(Graph, Graph1, Coloring, Coloring),
coloring(Graph1, K, 0, [], Stack),
color_stack(Stack).
coloring([], _, _, Stk0, Stk) :- !, Stk0 = Stk.
coloring(Graph, K, InUse, Stk0, Stk) :-
select_vertex(Graph, K, Compare, -, 0+0, V-Ns),
graph_del_vertices(Graph, [V], [V], Graph1),
( Compare = < ->
coloring(Graph1, K, InUse, [V-Ns|Stk0], Stk)
; M is min(K,InUse+1),
vertex_color(Ns, 1, M, V),
add_color(Graph1, Ns, V, Graph2),
InUse1 is max(V,InUse),
coloring(Graph2, K, InUse1, Stk0, Stk)
).
% select_vertex(+Graph, +K, -Comp, +Pair0, +Rank, -Pair)
% return any vertex with degree<K right away (Comp = <) else return
% vertex with max. saturation degree (Comp = >=), break ties using
% max. degree
select_vertex([], _, >=, Pair, _, Pair).
select_vertex([V-Neibs|Graph], K, Comp, Pair0, Rank0, Pair) :-
evaluate_vertex(Neibs, 0, Rank),
( Rank < K -> Comp = <, Pair = V-Neibs
; Rank @> Rank0 ->
select_vertex(Graph, K, Comp, V-Neibs, Rank, Pair)
; select_vertex(Graph, K, Comp, Pair0, Rank0, Pair)
).
evaluate_vertex([V|Neibs], Deg, Rank) :- var(V), !,
Deg1 is Deg+1,
evaluate_vertex(Neibs, Deg1, Rank).
evaluate_vertex(Neibs, Deg, Sat+Deg) :-
prolog:length(Neibs, 0, Sat).
add_color([], _, _, []).
add_color([V-Neibs|Graph], [W|Vs], C, [V-Neibs1|Graph1]) :- V==W, !,
ord_add_element(Neibs, C, Neibs1),
add_color(Graph, Vs, C, Graph1).
add_color([Pair|Graph], Vs, C, [Pair|Graph1]) :-
add_color(Graph, Vs, C, Graph1).
vertex_color([V|Vs], I, M, Color) :- V@<I, !,
vertex_color(Vs, I, M, Color).
vertex_color([I|Vs], I, M, Color) :- !,
I<M, J is I+1, vertex_color(Vs, J, M, Color).
vertex_color(_, I, _, I).
vertex_color(Vs, I, M, Color) :-
I<M, J is I+1, vertex_color(Vs, J, M, Color).
color_stack([]).
color_stack([V-Neibs|Stk]) :- sort(Neibs, Set), color_stack(Set, 1, V, Stk).
color_stack([I|Is], I, V, Stk) :- !, J is I+1, color_stack(Is, J, V, Stk).
color_stack(_, V, V, Stk) :- color_stack(Stk).
color_map([], []).
color_map([V-_|Graph], [V-_|Coloring]) :- color_map(Graph, Coloring).
color_map([], [], [], _).
color_map([V-Ns|Graph], [C-Ns1|Graph1], [V-C|Cols], Coloring) :-
map_colors(Ns, Coloring, Ns1),
color_map(Graph, Graph1, Cols, Coloring).
map_colors([], _, []).
map_colors(Ns, Coloring, Ns1) :-
Ns = [X|_],
Coloring = [V-_|_],
compare(C, X, V),
map_colors(C, Ns, Coloring, Ns1).
map_colors(=, [_|Xs], [_-Y|Coloring], [Y|Ns1]) :-
map_colors(Xs, Coloring, Ns1).
map_colors(>, Ns, [_|Coloring], Ns1) :-
map_colors(Ns, Coloring, Ns1).

2
Makefile.in
View File

@ -650,7 +650,7 @@ install_data:
$(INSTALL_DATA) $(srcdir)/LGPL/pillow/pillow.pl $(DESTDIR)$(SHAREDIR)/Yap/
# (cd CLPQR ; make install)
@INSTALLCLP@(cd LGPL/clp ; make install)
@INSTALLCLP@(cd LGPL/clpr ; make install)
@INSTALLCLP@(cd GPL/clpqr ; make install)
# (cd CHR ; make install)
@INSTALLCLP@(cd LGPL/chr ; make install)
@INSTALLCLP@(cd CLPBN ; make install)

6
configure vendored
View File

@ -16138,13 +16138,13 @@ mkdir -p LGPL/JPL/java/jpl/fli
mkdir -p LGPL/JPL/java/jpl/test
mkdir -p LGPL/JPL/src
mkdir -p LGPL/clp
mkdir -p LGPL/clpr
mkdir -p LGPL/chr
mkdir -p GPL
mkdir -p GPL/clpqr
mkdir -p GPL/http
mkdir -p cplint
ac_config_files="$ac_config_files Makefile library/matrix/Makefile library/matlab/Makefile library/regex/Makefile library/system/Makefile library/random/Makefile library/yap2swi/Makefile library/mpi/Makefile .depend library/Makefile LGPL/Makefile LGPL/chr/Makefile LGPL/chr/chr_swi_bootstrap.yap CLPBN/Makefile LGPL/clp/Makefile LGPL/clpr/Makefile library/lammpi/Makefile library/tries/Makefile LGPL/JPL/Makefile LGPL/JPL/src/Makefile LGPL/JPL/java/Makefile LGPL/JPL/jpl_paths.yap GPL/http/Makefile GPL/Makefile cplint/Makefile"
ac_config_files="$ac_config_files Makefile library/matrix/Makefile library/matlab/Makefile library/regex/Makefile library/system/Makefile library/random/Makefile library/yap2swi/Makefile library/mpi/Makefile .depend library/Makefile LGPL/Makefile LGPL/chr/Makefile LGPL/chr/chr_swi_bootstrap.yap CLPBN/Makefile LGPL/clp/Makefile GPL/clpqr/Makefile library/lammpi/Makefile library/tries/Makefile LGPL/JPL/Makefile LGPL/JPL/src/Makefile LGPL/JPL/java/Makefile LGPL/JPL/jpl_paths.yap GPL/http/Makefile GPL/Makefile cplint/Makefile"
cat >confcache <<\_ACEOF
# This file is a shell script that caches the results of configure
@ -16715,7 +16715,7 @@ do
"LGPL/chr/chr_swi_bootstrap.yap") CONFIG_FILES="$CONFIG_FILES LGPL/chr/chr_swi_bootstrap.yap" ;;
"CLPBN/Makefile") CONFIG_FILES="$CONFIG_FILES CLPBN/Makefile" ;;
"LGPL/clp/Makefile") CONFIG_FILES="$CONFIG_FILES LGPL/clp/Makefile" ;;
"LGPL/clpr/Makefile") CONFIG_FILES="$CONFIG_FILES LGPL/clpr/Makefile" ;;
"GPL/clpqr/Makefile") CONFIG_FILES="$CONFIG_FILES GPL/clpqr/Makefile" ;;
"library/lammpi/Makefile") CONFIG_FILES="$CONFIG_FILES library/lammpi/Makefile" ;;
"library/tries/Makefile") CONFIG_FILES="$CONFIG_FILES library/tries/Makefile" ;;
"LGPL/JPL/Makefile") CONFIG_FILES="$CONFIG_FILES LGPL/JPL/Makefile" ;;

4
configure.in
View File

@ -1400,13 +1400,13 @@ mkdir -p LGPL/JPL/java/jpl/fli
mkdir -p LGPL/JPL/java/jpl/test
mkdir -p LGPL/JPL/src
mkdir -p LGPL/clp
mkdir -p LGPL/clpr
mkdir -p LGPL/chr
mkdir -p GPL
mkdir -p GPL/clpqr
mkdir -p GPL/http
mkdir -p cplint
AC_OUTPUT(Makefile library/matrix/Makefile library/matlab/Makefile library/regex/Makefile library/system/Makefile library/random/Makefile library/yap2swi/Makefile library/mpi/Makefile .depend library/Makefile LGPL/Makefile LGPL/chr/Makefile LGPL/chr/chr_swi_bootstrap.yap CLPBN/Makefile LGPL/clp/Makefile LGPL/clpr/Makefile library/lammpi/Makefile library/tries/Makefile LGPL/JPL/Makefile LGPL/JPL/src/Makefile LGPL/JPL/java/Makefile LGPL/JPL/jpl_paths.yap GPL/http/Makefile GPL/Makefile cplint/Makefile)
AC_OUTPUT(Makefile library/matrix/Makefile library/matlab/Makefile library/regex/Makefile library/system/Makefile library/random/Makefile library/yap2swi/Makefile library/mpi/Makefile .depend library/Makefile LGPL/Makefile LGPL/chr/Makefile LGPL/chr/chr_swi_bootstrap.yap CLPBN/Makefile LGPL/clp/Makefile GPL/clpqr/Makefile library/lammpi/Makefile library/tries/Makefile LGPL/JPL/Makefile LGPL/JPL/src/Makefile LGPL/JPL/java/Makefile LGPL/JPL/jpl_paths.yap GPL/http/Makefile GPL/Makefile cplint/Makefile)
make depend

55
library/ugraphs.yap
View File

@ -30,23 +30,25 @@
s_transpose transposes a graph in S-form, cost O(|V|^2).
*/
:- module(ugraphs, [
add_vertices/3,
add_edges/3,
complement/2,
compose/3,
del_edges/3,
del_vertices/3,
edges/2,
neighbours/3,
neighbors/3,
reachable/3,
top_sort/2,
top_sort/3,
transitive_closure/2,
transpose/2,
vertices/2,
vertices_edges_to_ugraph/3
:- module(ugraphs,
[
add_vertices/3,
add_edges/3,
complement/2,
compose/3,
del_edges/3,
del_vertices/3,
edges/2,
neighbours/3,
neighbors/3,
reachable/3,
top_sort/2,
top_sort/3,
transitive_closure/2,
transpose/2,
vertices/2,
vertices_edges_to_ugraph/3,
ugraph_union/3
]).
:- use_module(library(lists), [
@ -550,3 +552,22 @@ reachable([N|Ns], G, Rs0, RsF) :-
append(Ns, D, Nsi),
reachable(Nsi, G, Rs1, RsF).
%% ugraph_union(+Set1, +Set2, ?Union)
%
% Is true when Union is the union of Set1 and Set2. This code is a
% copy of set union
ugraph_union(Set1, [], Set1) :- !.
ugraph_union([], Set2, Set2) :- !.
ugraph_union([Head1-E1|Tail1], [Head2-E2|Tail2], Union) :-
compare(Order, Head1, Head2),
ugraph_union(Order, Head1-E1, Tail1, Head2-E2, Tail2, Union).
ugraph_union(=, Head-E1, Tail1, _-E2, Tail2, [Head-Es|Union]) :-
ord_union(E1, E2, Es),
ugraph_union(Tail1, Tail2, Union).
ugraph_union(<, Head1, Tail1, Head2, Tail2, [Head1|Union]) :-
ugraph_union(Tail1, [Head2|Tail2], Union).
ugraph_union(>, Head1, Tail1, Head2, Tail2, [Head2|Union]) :-
ugraph_union([Head1|Tail1], Tail2, Union).

2
pl/boot.yap
View File

@ -634,6 +634,8 @@ true :- true.
write_term(user_error,B,Opts) ;
format(user_error,'~w',[B])
).
'$write_goal_output'(nl, First, NG, First, NG) :- !,
format(user_error,'~n',[]).
'$write_goal_output'(Format-G, First, NG, Next, IG) :-
G = [_|_], !,
% dump on string first so that we can check whether we actually

6
pl/directives.yap
View File

@ -24,6 +24,7 @@
'$directive'(G).
'$directive'(multifile(_)).
'$directive'(expects_dialect(_)).
'$directive'(discontiguous(_)).
'$directive'(initialization(_)).
'$directive'(include(_)).
@ -73,6 +74,8 @@
'$discontiguous'(D,M).
'$exec_directive'(initialization(D), _, M) :-
'$initialization'(M:D).
'$exec_directive'(expects_dialect(D), _, _) :-
'$expects_dialect'(D).
'$exec_directive'(encoding(Enc), _, _) :-
'$set_encoding'(Enc).
'$exec_directive'(parallel, _, _) :-
@ -1043,3 +1046,6 @@ user_defined_flag(Atom) :-
'$user_flag_value'(F, Val) :-
'$do_error'(type_error(atomic,Val),yap_flag(F,Val)).
'$expects_dialect'(swi) :-
load_files(library(swi),[silent(true),if(not_loaded)]).