This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/docs/clpr.tex

181 lines
6.6 KiB
TeX
Raw Normal View History

@chapter Constraint Logic Programming over Reals
YAP now uses the CLP(R) package developed by @emph{Leslie De Koninck},
K.U. Leuven as part of a thesis with supervisor Bart Demoen and daily
advisor Tom Schrijvers, and distributed with SWI-Prolog.
This CLP(R) system is a port of the CLP(Q,R) system of Sicstus Prolog
and YAP by Christian Holzbaur: Holzbaur C.: OFAI clp(q,r) Manual,
Edition 1.3.3, Austrian Research Institute for Artificial
Intelligence, Vienna, TR-95-09, 1995,
@url{http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09} This
port only contains the part concerning real arithmetics. This manual
is roughly based on the manual of the above mentioned @strong{CLP(QR)}
implementation.
Please note that the @file{clpr} library is @emph{not} an
@code{autoload} library and therefore this library must be loaded
explicitely before using it:
@example
:- use_module(library(clpr)).
@end example
@node CLPR Solver Predicates, CLPR Syntax , , CLPR
@section Solver Predicates
@c =============================
The following predicates are provided to work with constraints:
@table @code
@item @{+@var{Constraints}@}
Adds the constraints given by @var{Constraints} to the constraint store.
@item entailed(+@var{Constraint})
Succeeds if @var{Constraint} is necessarily true within the current
constraint store. This means that adding the negation of the constraint
to the store results in failure.
@item inf(+@var{Expression},-@var{Inf})
Computes the infimum of @var{Expression} within the current state of the
constraint store and returns that infimum in @var{Inf}. This predicate
does not change the constraint store.
@item inf(+@var{Expression},-@var{Sup})
Computes the supremum of @var{Expression} within the current state of
the constraint store and returns that supremum in @var{Sup}. This
predicate does not change the constraint store.
@item min(+@var{Expression})
Minimizes @var{Expression} within the current constraint store. This is
the same as computing the infimum and equation the expression to that
infimum.
@item max(+@var{Expression})
Maximizes @var{Expression} within the current constraint store. This is
the same as computing the supremum and equating the expression to that
supremum.
@item bb_inf(+@var{Ints},+@var{Expression},-@var{Inf},-@var{Vertext},+@var{Eps})
Computes the infimum of @var{Expression} within the current constraint
store, with the additional constraint that in that infimum, all
variables in @var{Ints} have integral values. @var{Vertex} will contain
the values of @var{Ints} in the infimum. @var{Eps} denotes how much a
value may differ from an integer to be considered an integer. E.g. when
@var{Eps} = 0.001, then X = 4.999 will be considered as an integer (5 in
this case). @var{Eps} should be between 0 and 0.5.
@item bb_inf(+@var{Ints},+@var{Expression},-@var{Inf})
The same as bb_inf/5 but without returning the values of the integers
and with an eps of 0.001.
@item dump(+@var{Target},+@var{Newvars},-@var{CodedAnswer})
Returns the constraints on @var{Target} in the list @var{CodedAnswer}
where all variables of @var{Target} have veen replaced by @var{NewVars}.
This operation does not change the constraint store. E.g. in
@example
dump([X,Y,Z],[x,y,z],Cons)
@end example
@var{Cons} will contain the constraints on @var{X}, @var{Y} and
@var{Z} where these variables have been replaced by atoms @code{x}, @code{y} and @code{z}.
@end table
@node CLPR Syntax, CLPR Unification, CLPR Solver Predicates, CLPR
@section Syntax of the predicate arguments
@c =============================================
The arguments of the predicates defined in the subsection above are
defined in the following table. Failing to meet the syntax rules will
result in an exception.
@example
<Constraints> ---> <Constraint> \\ single constraint \\
| <Constraint> , <Constraints> \\ conjunction \\
| <Constraint> ; <Constraints> \\ disjunction \\
<Constraint> ---> <Expression> @{<@} <Expression> \\ less than \\
| <Expression> @{>@} <Expression> \\ greater than \\
| <Expression> @{=<@} <Expression> \\ less or equal \\
| @{<=@}(<Expression>, <Expression>) \\ less or equal \\
| <Expression> @{>=@} <Expression> \\ greater or equal \\
| <Expression> @{=\=@} <Expression> \\ not equal \\
| <Expression> =:= <Expression> \\ equal \\
| <Expression> = <Expression> \\ equal \\
<Expression> ---> <Variable> \\ Prolog variable \\
| <Number> \\ Prolog number (float, integer) \\
| +<Expression> \\ unary plus \\
| -<Expression> \\ unary minus \\
| <Expression> + <Expression> \\ addition \\
| <Expression> - <Expression> \\ substraction \\
| <Expression> * <Expression> \\ multiplication \\
| <Expression> / <Expression> \\ division \\
| abs(<Expression>) \\ absolute value \\
| sin(<Expression>) \\ sine \\
| cos(<Expression>) \\ cosine \\
| tan(<Expression>) \\ tangent \\
| exp(<Expression>) \\ exponent \\
| pow(<Expression>) \\ exponent \\
| <Expression> @{^@} <Expression> \\ exponent \\
| min(<Expression>, <Expression>) \\ minimum \\
| max(<Expression>, <Expression>) \\ maximum \\
@end example
@node CLPR Unification, CLPR Non-linear Constraints, CLPR Syntax, CLPR
@section Use of unification
Instead of using the @code{@{@}/1} predicate, you can also use the standard
unification mechanism to store constraints. The following code samples
are equivalent:
@table @option
@item Unification with a variable
@example
@{X =:= Y@}
@{X = Y@}
X = Y
@end example
@item Unification with a number
@example
@{X =:= 5.0@}
@{X = 5.0@}
X = 5.0
@end example
@end table
@node CLPR Non-linear Constraints, , CLPR Unification, CLPR
@section Non-Linear Constraints
@c ==================================
In this version, non-linear constraints do not get solved until certain
conditions are satisfied. We call these conditions the isolation axioms.
They are given in the following table.
@example
A = B * C when B or C is ground or // A = 5 * C or A = B * 4 \\
A and (B or C) are ground // 20 = 5 * C or 20 = B * 4 \\
A = B / C when C is ground or // A = B / 3
A and B are ground // 4 = 12 / C
X = min(Y,Z) when Y and Z are ground or // X = min(4,3)
X = max(Y,Z) Y and Z are ground // X = max(4,3)
X = abs(Y) Y is ground // X = abs(-7)
X = pow(Y,Z) when X and Y are ground or // 8 = 2 ^ Z
X = exp(Y,Z) X and Z are ground // 8 = Y ^ 3
X = Y ^ Z Y and Z are ground // X = 2 ^ 3
X = sin(Y) when X is ground or // 1 = sin(Y)
X = cos(Y) Y is ground // X = sin(1.5707)
X = tan(Y)
@end example