<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">@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
&lt;Constraints&gt; ---&gt; &lt;Constraint&gt;				\\ single constraint \\
	      | &lt;Constraint&gt; , &lt;Constraints&gt;		\\ conjunction \\
	      | &lt;Constraint&gt; ; &lt;Constraints&gt;		\\ disjunction \\

&lt;Constraint&gt; ---&gt; &lt;Expression&gt; @{&lt;@} &lt;Expression&gt;		\\ less than \\
	     | &lt;Expression&gt; @{&gt;@} &lt;Expression&gt;		\\ greater than \\
	     | &lt;Expression&gt; @{=&lt;@} &lt;Expression&gt;	\\ less or equal \\
	     | @{&lt;=@}(&lt;Expression&gt;, &lt;Expression&gt;)	\\ less or equal \\
	     | &lt;Expression&gt; @{&gt;=@} &lt;Expression&gt;	\\ greater or equal \\
	     | &lt;Expression&gt; @{=\=@} &lt;Expression&gt;	\\ not equal \\
	     | &lt;Expression&gt; =:= &lt;Expression&gt;		\\ equal \\
	     | &lt;Expression&gt; = &lt;Expression&gt;		\\ equal \\

&lt;Expression&gt; ---&gt;  &lt;Variable&gt;				\\ Prolog variable \\
	     | &lt;Number&gt;				\\ Prolog number (float, integer) \\
	     | +&lt;Expression&gt;				\\ unary plus \\
	     | -&lt;Expression&gt;				\\ unary minus \\
	     | &lt;Expression&gt; + &lt;Expression&gt;		\\ addition \\
	     | &lt;Expression&gt; - &lt;Expression&gt;		\\ substraction \\
	     | &lt;Expression&gt; * &lt;Expression&gt;		\\ multiplication \\
	     | &lt;Expression&gt; / &lt;Expression&gt;		\\ division \\
	     | abs(&lt;Expression&gt;)			\\ absolute value \\
	     | sin(&lt;Expression&gt;)			\\ sine \\
	     | cos(&lt;Expression&gt;)			\\ cosine \\
	     | tan(&lt;Expression&gt;)			\\ tangent \\
	     | exp(&lt;Expression&gt;)			\\ exponent \\
	     | pow(&lt;Expression&gt;)			\\ exponent \\
	     | &lt;Expression&gt; @{^@} &lt;Expression&gt;		\\ exponent \\
	     | min(&lt;Expression&gt;, &lt;Expression&gt;)	\\ minimum \\
	     | max(&lt;Expression&gt;, &lt;Expression&gt;)	\\ 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

</pre></body></html>