181 lines
6.6 KiB
TeX
181 lines
6.6 KiB
TeX
@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
|
|
|