yap-6.3/docs/clpr.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 bb_inf(+@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