From 5cfad07c92ff198065157c792147be3d91f325b8 Mon Sep 17 00:00:00 2001
From: vsc <vsc@b08c6af1-5177-4d33-ba66-4b1c6b8b522a>
Date: Tue, 1 Nov 2005 18:19:44 +0000
Subject: [PATCH] update documentation.

git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1434 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
---
 CLPBN/clpbn/utils.yap |   29 +-
 CLPBN/clpbn/vel.yap   |    2 +-
 Makefile.in           |   11 +-
 changes-5.1.html      |    2 +
 docs/chr.tex          |  597 +++++++
 docs/clpr.tex         |  180 +++
 docs/swi.tex          |  495 ++++++
 docs/yap.tex          | 3492 +----------------------------------------
 8 files changed, 1361 insertions(+), 3447 deletions(-)
 create mode 100644 docs/chr.tex
 create mode 100644 docs/clpr.tex
 create mode 100644 docs/swi.tex

diff --git a/CLPBN/clpbn/utils.yap b/CLPBN/clpbn/utils.yap
index 7f4b607c0..d0f942233 100644
--- a/CLPBN/clpbn/utils.yap
+++ b/CLPBN/clpbn/utils.yap
@@ -37,10 +37,10 @@ clpbn_not_var_member([V1|Vs], V) :- V1 \== V,
 	clpbn_not_var_member(Vs, V).
 
 
-sort_vars_by_key(AVars, SortedAVars, Keys) :-
+sort_vars_by_key(AVars, SortedAVars, UnifiableVars) :-
 	get_keys(AVars, KeysVars),
 	keysort(KeysVars, KVars),
-	merge_same_key(KVars, SortedAVars, Keys).
+	merge_same_key(KVars, SortedAVars, [], UnifiableVars).
 
 get_keys([], []).
 get_keys([V|AVars], [K-V|KeysVars]) :-
@@ -49,15 +49,24 @@ get_keys([V|AVars], [K-V|KeysVars]) :-
 get_keys([_|AVars], KeysVars) :-  % may be non-CLPBN vars.
 	get_keys(AVars, KeysVars).
 
-merge_same_key([], [], []).
-merge_same_key([K1-V1|KVs], [V1|Vs], [K1|Ks]) :-
-	eat_same_key(KVs,K1,V1,RKVs),
-	merge_same_key(RKVs, Vs, Ks).
-
-eat_same_key([K-V|KVs],K,V,RKVs) :- !,
-	eat_same_key(KVs,K,V,RKVs).
-eat_same_key(KVs,_,_,KVs).
+merge_same_key([], [], _, []).
+merge_same_key([K1-V1,K2-V2|Vs], SortedAVars, Ks, UnifiableVars) :-
+	K1 == K2, !, V1 = V2,
+	merge_same_key([K1-V1|Vs], SortedAVars, Ks, UnifiableVars).
+merge_same_key([K1-V1,K2-V2|Vs], [V1|SortedAVars], Ks, [K1|UnifiableVars]) :-
+	(in_keys(K1, Ks) ; \+ \+ K1 == K2), !, 
+	add_to_keys(K1, Ks, NKs),
+	merge_same_key([K2-V2|Vs], SortedAVars, NKs, UnifiableVars).
+merge_same_key([K-V|Vs], [V|SortedAVars], Ks, UnifiableVars) :-
+	add_to_keys(K, Ks, NKs),
+	merge_same_key(Vs, SortedAVars, NKs, UnifiableVars).
 
+in_keys(K1,[K|_]) :- \+ \+ K1 = K, !.
+in_keys(K1,[_|Ks]) :- 
+	in_keys(K1,Ks).
+	
+add_to_keys(K1, Ks, Ks) :- ground(K1), !.
+add_to_keys(K1, Ks, [K1|Ks]).
 
 sort_vars_by_key_and_parents(AVars, SortedAVars, UnifiableVars) :-
 	get_keys_and_parents(AVars, KeysVars),
diff --git a/CLPBN/clpbn/vel.yap b/CLPBN/clpbn/vel.yap
index 2bd337d9b..d9a42efdd 100644
--- a/CLPBN/clpbn/vel.yap
+++ b/CLPBN/clpbn/vel.yap
@@ -297,7 +297,7 @@ divide_by_sum([P|Ps0],Sum,[PN|Ps]) :-
 % what is actually output
 %
 attribute_goal(V, G) :-
-	get_atts(V, [posterior(Vs,Vals,Ps,AllDiffs)]), !,
+	get_atts(V, [posterior(Vs,Vals,Ps,AllDiffs)]),
 	massage_out(Vs, Vals, Ps, G, AllDiffs, V).
 
 massage_out([], Ev, _, V=Ev, _, V) :- !.
diff --git a/Makefile.in b/Makefile.in
index 6d64dc2f9..6140f0ec8 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -184,6 +184,9 @@ PL_SOURCES= \
 	$(srcdir)/pl/utils.yap \
 	$(srcdir)/pl/yapor.yap $(srcdir)/pl/yio.yap
 
+YAPDOCS=$(srcdir)/docs/yap.tex $(srcdir)/docs/chr.tex \
+	$(srcdir)/docs/clpr.tex $(srcdir)/docs/swi.tex 
+
 ENGINE_OBJECTS = \
 	agc.o absmi.o adtdefs.o alloc.o amasm.o analyst.o arrays.o \
 	arith0.o arith1.o arith2.o attvar.o bb.o \
@@ -616,7 +619,7 @@ install_info:
 
 info: yap.info
 
-yap.info: $(srcdir)/docs/yap.tex 
+yap.info: $(YAPDOCS)
 	$(MAKEINFO) $(srcdir)/docs/yap.tex
 
 html: yap.html
@@ -626,17 +629,17 @@ yap.html: $(srcdir)/docs/yap.tex
 
 dvi: yap.dvi
 
-yap.dvi: $(srcdir)/docs/yap.tex
+yap.dvi: $(YAPDOCS)
 	$(TEXI2DVI) $(srcdir)/docs/yap.tex
 
 ps:	yap.ps
 
-yap.ps: $(srcdir)/docs/yap.dvi
+yap.ps:  $(YAPDOCS)
 	dvips -o yap.ps $(srcdir)/docs/yap
 
 pdf: yap.pdf
 
-yap.pdf: $(srcdir)/docs/yap.tex
+yap.pdf:  $(YAPDOCS)
 	$(TEXI2PDF) $(srcdir)/docs/yap.tex
 
 clean_docs:
diff --git a/changes-5.1.html b/changes-5.1.html
index c8a8f5177..92732a06b 100644
--- a/changes-5.1.html
+++ b/changes-5.1.html
@@ -16,6 +16,8 @@
 
 <h2>Yap-5.1.0:</h2>
 <ul>
+<li> NEW: update documentation to support new CLP(R) and CHR packages. </li>
+<li> FIXED: regression in clpbn/utils.yap. </li>
 <li> NEW: put_attrs/2. </li>
 <li> FIXED: don't install CLP unless coroutining && rational trees are
   active. </li>
diff --git a/docs/chr.tex b/docs/chr.tex
new file mode 100644
index 000000000..f0e1fc39b
--- /dev/null
+++ b/docs/chr.tex
@@ -0,0 +1,597 @@
+@chapter CHR: Constraint Handling Rules 
+@c 		\label{sec:chr}
+
+This chapter is written by Tom Schrijvers, K.U. Leuven for the hProlog
+system. Adjusted by Jan Wielemaker to fit the SWI-Prolog documentation
+infrastructure and remove hProlog specific references.
+
+The CHR system of SWI-Prolog is the K.U.Leuven CHR system.  The runtime
+environment is written by Christian Holzbaur and Tom Schrijvers while the
+compiler is written by Tom Schrijvers. Both are integrated with SWI-Prolog
+and licenced under compatible conditions with permission from the authors.
+
+The main reference for SWI-Prolog's CHR system is:
+@itemize
+@item T. Schrijvers, and B. Demoen, @emph{The K.U.Leuven CHR System: Implementation
+and Application}, First Workshop on Constraint Handling Rules: Selected
+Contributions (Fruwirth, T. and Meister, M., eds.), pp. 1--5, 2004.
+@end itemize
+
+@node CHR Introduction, CHR Syntax and Semantics, , CHR
+@section Introduction
+@c =====================
+
+Constraint Handling Rules (CHR) is a committed-choice bottom-up language
+embedded in Prolog. It is designed for writing constraint solvers and is
+particularily useful for providing application-specific constraints.
+It has been used in many kinds of applications, like scheduling,
+model checking, abduction, type checking among many others.
+
+CHR has previously been implemented in other Prolog systems (SICStus,
+Eclipse, Yap), Haskell and Java. This CHR system is based on the
+compilation scheme and runtime environment of CHR in SICStus.
+
+In this documentation we restrict ourselves to giving a short overview
+of CHR in general and mainly focus on elements specific to this
+implementation. For a more thorough review of CHR we refer the reader to
+[Freuhwirth:98]. More background on CHR can be found at the CHR web site.
+
+@c \secref{SyntaxAndSemantics} we present the syntax of CHR in Prolog and
+@c explain informally its operational semantics. Next, \secref{practical}
+@c deals with practical issues of writing and compiling hProlog programs
+@c containing CHR. \Secref{debugging} explains the currently primitive CHR
+@c debugging facilities. \Secref{predicates} provides a few useful predicates
+@c to inspect the constraint store and \secref{examples} illustrates CHR with
+@c two example programs. In \secref{sicstus-chr} some compatibility issues with
+@c SICStus CHR are listed. Finally, \secref{guidelines} concludes with a few
+@c practical guidelines for using CHR.
+
+
+@node CHR Syntax and Semantics, CHR in YAP Programs, CHR Introduction, CHR
+@section Syntax and Semantics
+@c		\label{sec:SyntaxAndSemantics}
+@c=============================
+
+@subsection Syntax
+@c -----------------
+
+The syntax of CHR rules in hProlog is the following:
+
+@example
+rules --> rule, rules.
+rules --> [].
+
+rule --> name, actual_rule, pragma, [atom('.')].
+
+name --> atom, [atom('@')].
+name --> [].
+
+actual_rule --> simplification_rule.
+actual_rule --> propagation_rule.
+actual_rule --> simpagation_rule.
+
+simplification_rule --> constraints, [atom('<=>')], guard, body.
+propagation_rule --> constraints, [atom('==>')], guard, body.
+simpagation_rule --> constraints, [atom('\')], constraints, [atom('<=>')], 
+                     guard, body.
+
+constraints --> constraint, constraint_id.
+constraints --> constraint, [atom(',')], constraints.
+
+constraint --> compound_term.
+
+constraint_id --> [].
+constraint_id --> [atom('#')], variable.
+
+guard --> [].
+guard --> goal, [atom('|')].
+
+body --> goal.
+
+pragma --> [].
+pragma --> [atom('pragma')], actual_pragmas.
+
+actual_pragmas --> actual_pragma.
+actual_pragmas --> actual_pragma, [atom(',')], actual_pragmas.
+
+actual_pragma --> [atom('passive(')], variable, [atom(')')].
+
+@end example
+
+Additional syntax-related terminology:
+
+@itemize
+@item @strong{head:} the constraints in an @code{actual_rule} before
+                     the arrow (either @code{<=>} or @code{==>})
+@end itemize
+
+@subsection Semantics
+@c --------------------
+
+In this subsection the operational semantics of CHR in Prolog are presented
+informally. They do not differ essentially from other CHR systems.
+
+When a constraint is called, it is considered an active constraint and
+the system will try to apply the rules to it. Rules are tried and executed
+sequentially in the order they are written. 
+
+A rule is conceptually tried for an active constraint in the following
+way. The active constraint is matched with a constraint in the head of
+the rule. If more constraints appear in the head they are looked for
+among the suspended constraints, which are called passive constraints in
+this context. If the necessary passive constraints can be found and all
+match with the head of the rule and the guard of the rule succeeds, then
+the rule is committed and the body of the rule executed. If not all the
+necessary passive constraint can be found, the matching fails or the
+guard fails, then the body is not executed and the process of trying and
+executing simply continues with the following rules. If for a rule,
+there are multiple constraints in the head, the active constraint will
+try the rule sequentially multiple times, each time trying to match with
+another constraint.
+
+This process ends either when the active constraint disappears, i.e. it
+is removed by some rule, or after the last rule has been processed. In
+the latter case the active constraint becomes suspended.
+
+A suspended constraint is eligible as a passive constraint for an active
+constraint. The other way it may interact again with the rules, is when
+a variable appearing in the constraint becomes bound to either a nonvariable
+or another variable involved in one or more constraints. In that case the
+constraint is triggered, i.e. it becomes an active constraint and all
+the rules are tried.
+
+@unnumberedsubsubsec Rule Types
+@c - - - - - - - - - - 
+
+There are three different kinds of rules, each with their specific semantics:
+
+@table @code
+@item simplification
+The simplification rule removes the constraints in its head and calls its body.
+
+@item propagation
+The propagation rule calls its body exactly once for the constraints in
+its head.
+
+@item simpagation
+The simpagation rule removes the constraints in its head after the
+@code{\} and then calls its body. It is an optimization of
+simplification rules of the form: \[constraints_1, constraints_2 <=>
+constraints_1, body \] Namely, in the simpagation form: 
+
+@example
+constraints1 \ constraints2 <=> body
+@end example
+@noindent
+@var{constraints1}
+constraints are not called in the body.
+@end table
+
+@unnumberedsubsubsec Rule Names
+@c - - - - - - - - - - 
+Naming a rule is optional and has no semantical meaning. It only functions
+as documentation for the programmer.
+
+@unnumberedsubsubsec Pragmas
+@c - - - - - - - - -
+The semantics of the pragmas are:
+
+@table @option
+@item passive(Identifier)
+The constraint in the head of a rule @var{Identifier} can only act as a
+passive constraint in that rule.
+@end table
+
+Additional pragmas may be released in the future.
+
+@unnumberedsubsubsec Options
+@c - - - - - - - - -
+It is possible to specify options that apply to all the CHR rules in the module.
+Options are specified with the @code{option/2} declaration:
+
+@example
+                option(Option,Value).
+@end example
+
+Available options are:
+@table @code
+        @item check_guard_bindings
+This option controls whether guards should be checked for illegal
+variable bindings or not. Possible values for this option are
+@code{on}, to enable the checks, and @code{off}, to disable the
+checks.
+
+        @item optimize
+This is an experimental option controlling the degree of optimization.
+Possible values are @code{full}, to enable all available
+optimizations, and @code{off} (default), to disable all optimizations.  
+The default is derived from the SWI-Prolog flag @code{optimise}, where
+@code{true} is mapped to @code{full}.  Therefore the commandline
+option @option{-O} provides full CHR optimization.
+If optimization is enabled, debugging should be disabled.
+
+	@item debug
+This options enables or disables the possibility to debug the CHR code.
+Possible values are @code{on} (default) and @code{off}. See
+@option{debugging} for more details on debugging.  The default is
+derived from the prolog flag @code{generate_debug_info}, which
+is @code{true} by default.  See @option{-nodebug}.
+If debugging is enabled, optimization should be disabled.
+
+	@item mode
+This option specifies the mode for a particular constraint. The
+value is a term with functor and arity equal to that of a constraint.
+The arguments can be one of @code{-}, @code{+} or @code{?}.
+The latter is the default. The meaning is the following:
+	@table @code
+	@item -
+         The corresponding argument of every occurrence
+	of the constraint is always unbound.
+	@item + 
+        The corresponding argument of every occurrence
+	of the constraint is always ground.
+	@item ?
+         The corresponding argument of every occurrence
+	of the constraint can have any instantiation, which may change
+	over time. This is the default value.
+	@end table
+The declaration is used by the compiler for various optimizations. 
+Note that it is up to the user the ensure that the mode declaration
+is correct with respect to the use of the constraint.
+This option may occur once for each constraint.
+
+	@item type_declaration
+This option specifies the argument types for a particular constraint. The
+value is a term with functor and arity equal to that of a constraint.
+The arguments can be a user-defined type or one of
+the built-in types:
+    @table @code
+	@item int
+         The corresponding argument of every occurrence
+	of the constraint is an integer number.
+	@item float
+         @dots{} a floating point number.
+	@item number
+         @dots{} a number.
+	@item natural
+         @dots{} a positive integer.
+	@item any
+         The corresponding argument of every occurrence
+	of the constraint can have any type. This is the default value.
+   @end table
+
+Currently, type declarations are only used to improve certain
+optimizations (guard simplification, occurrence subsumption, @dots{}).
+
+	@item type_definition
+This option defines a new user-defined type which can be used in
+type declarations. The value is a term of the form
+@code{type(}@var{name}@code{,}@var{list}@code{)}, where
+@var{name} is a term and @var{list} is a list of alternatives.
+Variables can be used to define generic types. Recursive definitions
+are allowed. Examples are 
+
+@example
+type(bool,[true,false]).
+type(complex_number,[float + float * i]).
+type(binary_tree(T),[ leaf(T) | node(binary_tree(T),binary_tree(T)) ]).
+type(list(T),[ [] | [T | list(T)]).
+@end example
+
+
+@end table
+
+The mode, type_declaration and type_definition options are provided
+for backward compatibility. The new syntax is described below.
+
+@node CHR in YAP Programs, CHR Debugging, CHR Syntax and Semantics, CHR
+@section CHR in YAP Programs	
+@c	\label{sec:practical}
+@c===========================
+
+
+@subsection Embedding in Prolog Programs
+
+The CHR constraints defined in a particulary @file{chr} file are
+associated with a module. The default module is @code{user}. One should
+never load different @file{chr} files with the same CHR module name.
+
+@subsection Constraint declaration
+
+Every constraint used in CHR rules has to be declared.
+There are two ways to do this. The old style is as follows:
+
+@example
+option(type_definition,type(list(T),[ [] , [T|list(T)] ]).
+option(mode,foo(+,?)).
+option(type_declaration,foo(list(int),float)).
+:- constraints foo/2, bar/0.
+@end example
+
+The new style is as follows:
+
+@example
+:- chr_type list(T) ---> [] ; [T|list(T)].
+:- constraints foo(+list(int),?float), bar.
+@end example
+
+
+@subsection Compilation
+
+The SWI-Prolog CHR compiler exploits term_expansion/2 rules to translate
+the constraint handling rules to plain Prolog. These rules are loaded
+from the library @file{chr}.   They are activated if the compiled file
+has the @file{chr} extension or after finding a declaration of the
+format below.
+
+@example
+:- constraints ...
+@end example
+
+It is adviced to define CHR rules in a module file, where the module
+declaration is immediately followed by including the @file{chr}
+library as examplified below:
+
+@example
+:- module(zebra, [ zebra/0 ]).
+:- use_module(library(chr)).
+
+:- constraints ...
+@end example
+
+Using this style CHR rules can be defined in ordinary Prolog
+@file{pl} files and the operator definitions required by CHR do not
+leak into modules where they might cause conflicts.
+
+
+@node CHR Debugging, CHR Examples,CHR in YAP Programs, CHR
+@section Debugging
+@c			\label{sec:debugging}
+@c=================
+
+The CHR debugging facilities are currently rather limited. Only tracing
+is currently available. To use the CHR debugging facilities for a CHR
+file it must be compiled for debugging. Generating debug info is
+controlled by the CHR option @code{debug}, whose default is derived
+from the SWI-Prolog flag @code{generate_debug_info}.  Therefore debug
+info is provided unless the @option{-nodebug} is used.
+
+
+@subsection Ports
+@c				\label{sec:chrports
+@c===============
+
+For CHR constraints the four standard ports are defined:
+
+@table @code
+	@item call
+A new constraint is called and becomes active.
+	@item exit
+An active constraint exits: it has either been inserted in the store after
+trying all rules or has been removed from the constraint store.
+	@item fail
+An active constraint fails.
+	@item redo
+An active constraint starts looking for an alternative solution.
+@end table
+
+In addition to the above ports, CHR constraints have five additional
+ports:
+
+@table @code
+@item wake
+A suspended constraint is woken and becomes active.
+@item insert
+An active constraint has tried all rules and is suspended in
+the constraint store.
+@item remove
+An active or passive constraint is removed from the constraint
+store, if it had been inserted.
+@item try
+	An active constraints tries a rule with possibly
+	some passive constraints. The try port is entered
+	just before committing to the rule.
+@item apply
+	An active constraints commits to a rule with possibly
+	some passive constraints. The apply port is entered
+	just after committing to the rule.
+@end table
+
+@subsection Tracing
+@c=================
+
+Tracing is enabled with the chr_trace/0 predicate
+and disabled with the chr_notrace/0 predicate.
+
+When enabled the tracer will step through the @code{call},
+@code{exit}, @code{fail}, @code{wake} and @code{apply} ports,
+accepting debug commands, and simply write out the other ports.
+
+The following debug commans are currently supported:
+
+@example
+        CHR debug options:
+
+                <cr>    creep           c       creep
+		s	skip
+		g	ancestors
+                n       nodebug
+		b	break
+                a       abort
+                f       fail
+                ?       help            h       help
+@end example
+
+Their meaning is:
+
+@table @code
+@item creep
+Step to the next port.
+@item skip
+Skip to exit port of this call or wake port.
+@item ancestors
+Print list of ancestor call and wake ports.
+@item nodebug
+Disable the tracer.
+@item break
+Enter a recursive Prolog toplevel.  See break/0.
+@item abort
+Exit to the toplevel.  See abort/0.
+@item fail
+Insert failure in execution.
+@item help
+Print the above available debug options.
+@end table
+
+@subsection CHR Debugging Predicates
+@c 		\label{sec:predicates
+@c====================================
+
+The @file{chr} module contains several predicates that allow
+inspecting and printing the content of the constraint store.
+
+@table @code
+    @item chr_trace/0
+Activate the CHR tracer.  By default the CHR tracer is activated and
+deactivated automatically by the Prolog predicates trace/0 and
+notrace/0.
+
+    @item chr_notrace/0
+De-activate the CHR tracer.  By default the CHR tracer is activated and
+deactivated automatically by the Prolog predicates trace/0 and
+notrace/0.
+    
+    @item chr_leash/0 
+
+Define the set of CHR ports on which the CHR
+tracer asks for user intervention (i.e. stops). @var{Spec} is either a
+list of ports or a predefined `alias'. Defined aliases are:
+@code{full} to stop at all ports, @code{none} or @code{off} to never
+stop, and @code{default} to stop at the @code{call}, @code{exit},
+@code{fail}, @code{wake} and @code{apply} ports.  See also leash/1.
+
+    @item chr_show_store(+@var{Mod})
+Prints all suspended constraints of module @var{Mod} to the standard
+output. This predicate is automatically called by the SWI-Prolog toplevel at
+the end of each query for every CHR module currently loaded.  The prolog-flag
+@code{chr_toplevel_show_store} controls whether the toplevel shows the
+constraint stores. The value @code{true} enables it.  Any other value
+disables it.
+
+
+@end table
+
+
+@node CHR Examples, CHR Compatibility,CHR Debugging, CHR
+@section Examples
+@c			\label{sec:examples}
+@c================
+
+Here are two example constraint solvers written in CHR.
+
+@itemize
+ @item
+The program below defines a solver with one constraint, 
+@code{leq/2}, which is a less-than-or-equal constraint.
+
+@example
+:- module(leq,[cycle/3, leq/2]).
+:- use_module(library(chr)).
+
+:- constraints leq/2.
+reflexivity  @ leq(X,X) <=> true.
+antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y.
+idempotence  @ leq(X,Y) \ leq(X,Y) <=> true.
+transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).
+
+cycle(X,Y,Z):-
+        leq(X,Y),
+        leq(Y,Z),
+        leq(Z,X).
+@end example
+
+    @item
+The program below implements a simple finite domain
+constraint solver.
+
+@example
+:- module(dom,[dom/2]).
+:- use_module(library(chr)).
+
+:- constraints dom/2. 
+
+dom(X,[]) <=> fail.
+dom(X,[Y]) <=> X = Y.
+dom(X,L1), dom(X,L2) <=> intersection(L1,L2,L3), dom(X,L3).
+
+intersection([],_,[]).
+intersection([H|T],L2,[H|L3]) :-
+        member(H,L2), !,
+        intersection(T,L2,L3).
+intersection([_|T],L2,L3) :-
+        intersection(T,L2,L3).
+@end example
+		
+@end itemize
+
+@node CHR Compatibility, CHR Guidelines,CHR Examples, CHR
+@section Compatibility with SICStus CHR
+@c 		\label{sec:sicstus-chr}
+@c==================
+
+There are small differences between CHR in SWI-Prolog and newer
+YAPs and SICStus and older versions of YAP.  Besides differences in
+available options and pragmas, the following differences should be
+noted:
+
+@table @code
+        @item [The handler/1 declaration]
+In SICStus every CHR module requires a @code{handler/1}
+declaration declaring a unique handler name. This declaration is valid
+syntax in SWI-Prolog, but will have no effect. A warning will be given
+during compilation.
+
+        @item [The rules/1 declaration]
+In SICStus, for every CHR module it is possible to only enable a subset
+of the available rules through the @code{rules/1} declaration. The
+declaration is valid syntax in SWI-Prolog, but has no effect. A
+warning is given during compilation.
+
+	@item [Sourcefile naming]
+SICStus uses a two-step compiler, where @file{chr} files are
+first translated into @file{pl} files.  For SWI-Prolog CHR
+rules may be defined in a file with any extension.
+@end table
+
+
+@node CHR Guidelines, ,CHR Compatibility, CHR
+@section Guidelines
+@c 			\label{sec:guidelines}
+@c ==================
+
+In this section we cover several guidelines on how to use CHR to write
+constraint solvers and how to do so efficiently.
+
+@table @code
+    @item [Set semantics]
+The CHR system allows the presence of identical constraints, i.e.
+multiple constraints with the same functor, arity and arguments. For
+most constraint solvers, this is not desirable: it affects efficiency
+and possibly termination. Hence appropriate simpagation rules should be
+added of the form:
+
+@example
+@{constraint \ constraint <=> true@}.
+@end example
+
+    @item [Multi-headed rules]
+Multi-headed rules are executed more efficiently when the constraints
+share one or more variables.
+
+    @item [Mode and type declarations]
+Provide mode and type declarations to get more efficient program execution.
+Make sure to disable debug (@option{-nodebug}) and enable optimization
+(@option{-O}).
+@end table
+
+
diff --git a/docs/clpr.tex b/docs/clpr.tex
new file mode 100644
index 000000000..48715c57b
--- /dev/null
+++ b/docs/clpr.tex
@@ -0,0 +1,180 @@
+@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
+
diff --git a/docs/swi.tex b/docs/swi.tex
new file mode 100644
index 000000000..cdf64cbd0
--- /dev/null
+++ b/docs/swi.tex
@@ -0,0 +1,495 @@
+@chapter SWI-Prolog Emulation
+
+This library provides a number of SWI-Prolog builtins that are not by
+default in YAP. This library is loaded with the
+@code{use_module(library(swi))} command.
+
+@table @code
+
+@item append(?@var{List1},?@var{List2},?@var{List3})
+@findex append/3
+@snindex append/3
+@cnindex append/3
+Succeeds when @var{List3} unifies with the concatenation of @var{List1}
+and @var{List2}. The predicate can be used with any instantiation
+pattern (even three variables).
+
+@item between(+@var{Low},+@var{High},?@var{Value})
+@findex between/3
+@snindex between/3
+@cnindex between/3
+
+@var{Low} and @var{High} are integers, @var{High} less or equal than
+@var{Low}. If @var{Value} is an integer, @var{Low} less or equal than
+@var{Value} less or equal than @var{High}.  When @var{Value} is a
+variable it is successively bound to all integers between @var{Low} and
+@var{High}.  If @var{High} is @code{inf}, @code{between/3} is true iff
+@var{Value} less or equal than @var{Low}, a feature that is particularly
+interesting for generating integers from a certain value.
+
+@item chdir(+@var{Dir})
+@findex chdir/1
+@snindex chdir/1
+@cnindex chdir/1
+
+Compatibility predicate.  New code should use @code{working_directory/2}.
+
+@item concat_atom(+@var{List},-@var{Atom})
+@findex concat_atom/2
+@snindex concat_atom/2
+@cnindex concat_atom/2
+
+@var{List} is a list of atoms, integers or floating point numbers. Succeeds
+if @var{Atom} can be unified with the concatenated elements of @var{List}. If
+@var{List} has exactly 2 elements it is equivalent to @code{atom_concat/3},
+allowing for variables in the list.
+
+@item concat_atom(?@var{List},+@var{Separator},?@var{Atom})
+@findex concat_atom/3
+@snindex concat_atom/3
+@cnindex concat_atom/3
+
+Creates an atom just like concat_atom/2, but inserts @var{Separator}
+between each pair of atoms.  For example:
+\@example
+?- concat_atom([gnu, gnat], ', ', A).
+
+A = 'gnu, gnat'
+@end example
+
+(Unimplemented) This predicate can also be used to split atoms by
+instantiating @var{Separator} and @var{Atom}:
+
+@example
+?- concat_atom(L, -, 'gnu-gnat').
+
+L = [gnu, gnat]
+@end example
+
+@item nth1(+@var{Index},?@var{List},?@var{Elem})
+@findex nth1/3
+@snindex nth1/3
+@cnindex nth1/3
+Succeeds when the @var{Index}-th element of @var{List} unifies with
+@var{Elem}. Counting starts at 1.
+
+Set environment variable.  @var{Name} and @var{Value} should be
+instantiated to atoms or integers.  The environment variable will be
+passed to @code{shell/[0-2]} and can be requested using @code{getenv/2}.
+They also influence @code{expand_file_name/2}.
+
+@item setenv(+@var{Name},+@var{Value})
+@findex setenv/2
+@snindex setenv/2
+@cnindex setenv/2
+Set environment variable.  @var{Name} and @var{Value} should be
+instantiated to atoms or integers.  The environment variable will be
+passed to @code{shell/[0-2]} and can be requested using @code{getenv/2}.
+They also influence @code{expand_file_name/2}.
+
+@item term_to_atom(?@var{Term},?@var{Atom})
+@findex term_to_atom/2
+@snindex term_to_atom/2
+@cnindex term_to_atom/2
+Succeeds if @var{Atom} describes a term that unifies with @var{Term}. When
+@var{Atom} is instantiated @var{Atom} is converted and then unified with
+@var{Term}.  If @var{Atom} has no valid syntax, a @code{syntax_error}
+exception is raised. Otherwise @var{Term} is ``written'' on @var{Atom}
+using @code{write/1}.
+
+@item working_directory(-@var{Old},+@var{New})
+@findex working_directory/2
+@snindex working_directory/2
+@cnindex working_directory/2
+
+Unify @var{Old} with an absolute path to the current working directory
+and change working directory to @var{New}.  Use the pattern
+@code{working_directory(CWD, CWD)} to get the current directory.  See
+also @code{absolute_file_name/2} and @code{chdir/1}.
+
+@end table
+
+@node Invoking Predicates on all Members of a List,Forall, , SWI-Prolog
+@section Invoking Predicates on all Members of a List
+@c \label{sec:applylist}
+
+All the predicates in this section call a predicate on all members of a
+list or until the predicate called fails.  The predicate is called via
+@code{call/[2..]}, which implies common arguments can be put in
+front of the arguments obtained from the list(s). For example:
+
+@example
+?- maplist(plus(1), [0, 1, 2], X).
+
+X = [1, 2, 3]
+@end example
+
+we will phrase this as ``@var{Predicate} is applied on ...''
+
+@table @code
+
+@item maplist(+@var{Pred},+@var{List})
+@findex maplist/2
+@snindex maplist/2
+@cnindex maplist/2
+@var{Pred} is applied successively on each element of @var{List} until
+the end of the list or @var{Pred} fails. In the latter case 
+@code{maplist/2} fails.
+
+@item maplist(+@var{Pred},+@var{List1},+@var{List2})
+@findex maplist/3
+@snindex maplist/3
+@cnindex maplist/3
+Apply @var{Pred} on all successive triples of elements from
+@var{List1} and
+@var{List2}. Fails if @var{Pred} can not be applied to a
+pair. See the example above.
+
+@item maplist(+@var{Pred},+@var{List1},+@var{List2},+@var{List4})
+@findex maplist/4
+@snindex maplist/4
+@cnindex maplist/4
+Apply @var{Pred} on all successive triples of elements from @var{List1},
+@var{List2} and @var{List3}. Fails if @var{Pred} can not be applied to a
+triple. See the example above.
+
+@c @item findlist(+@var{Pred},+@var{List1},?@var{List2})
+@c @findex findlist/3
+@c @snindex findlist/3
+@c @cnindex findlist/3
+@c Unify @var{List2} with a list of all elements of @var{List1} to which
+@c @var{Pred} applies.
+@end table
+
+@node Forall,hProlog and SWI-Prolog Attributed Variables,Invoking Predicates on all Members of a List, SWI-Prolog
+@section Forall			
+@c \label{sec:forall2}
+
+@table @code
+@item forall(+@var{Cond},+@var{Action})
+@findex forall/2
+@snindex forall/2
+@cnindex forall/2
+
+For all alternative bindings of @var{Cond} @var{Action} can be proven.
+The next example verifies that all arithmetic statements in the list
+@var{L} are correct. It does not say which is wrong if one proves wrong.
+
+@example
+?- forall(member(Result = Formula, [2 = 1 + 1, 4 = 2 * 2]),
+                 Result =:= Formula).
+@end example
+
+@end table
+
+@node hProlog and SWI-Prolog Attributed Variables, SWI-Prolog Global Variables, Forall,SWI-Prolog
+@section hProlog and SWI-Prolog Attributed Variables
+@cindex hProlog Attributed Variables
+
+Attributed variables
+@c @ref{Attributed variables}
+provide a technique for extending the
+Prolog unification algorithm by hooking the binding of attributed
+variables. There is little consensus in the Prolog community on the
+exact definition and interface to attributed variables.  Yap Prolog
+traditionally implements a SICStus-like interface, but to enable
+SWI-compatibility we have implemented the SWI-Prolog interface,
+identical to the one realised by Bart Demoen for hProlog.
+
+Binding an attributed variable schedules a goal to be executed at the
+first possible opportunity. In the current implementation the hooks are
+executed immediately after a successful unification of the clause-head
+or successful completion of a foreign language (builtin) predicate. Each
+attribute is associated to a module and the hook (attr_unify_hook/2) is
+executed in this module.  The example below realises a very simple and
+incomplete finite domain reasoner.
+
+@example
+:- module(domain,
+	  [ domain/2			% Var, ?Domain
+	  ]).
+:- use_module(library(oset)).
+
+domain(X, Dom) :-
+	var(Dom), !,
+	get_attr(X, domain, Dom).
+domain(X, List) :-
+	sort(List, Domain),
+	put_attr(Y, domain, Domain),
+	X = Y.
+
+%	An attributed variable with attribute value Domain has been
+%	assigned the value Y
+
+attr_unify_hook(Domain, Y) :-
+	(   get_attr(Y, domain, Dom2)
+	->  oset_int(Domain, Dom2, NewDomain),
+	    (   NewDomain == []
+	    ->	fail
+	    ;	NewDomain = [Value]
+	    ->	Y = Value
+	    ;	put_attr(Y, domain, NewDomain)
+	    )
+	;   var(Y)
+	->  put_attr( Y, domain, Domain )
+	;   memberchk(Y, Domain)
+	).
+@end example
+
+
+Before explaining the code we give some example queries:
+
+@table @code
+@item ?- domain(X, [a,b]), X = c		     
+no
+@item ?- domain(X, [a,b]), domain(X, [a,c]).   
+      X = a
+@item ?- domain(X, [a,b,c]), domain(X, [a,c]). 
+  X = _D0
+@end table
+
+The predicate @code{domain/2} fetches (first clause) or assigns
+(second clause) the variable a @emph{domain}, a set of values it can
+be unified with.  In the second clause first associates the domain
+with a fresh variable and then unifies X to this variable to deal
+with the possibility that X already has a domain. The
+predicate @code{attr_unify_hook/2} is a hook called after a variable with
+a domain is assigned a value.  In the simple case where the variable
+is bound to a concrete value we simply check whether this value is in
+the domain. Otherwise we take the intersection of the domains and either
+fail if the intersection is empty (first example), simply assign the
+value if there is only one value in the intersection (second example) or
+assign the intersection as the new domain of the variable (third
+example).
+
+
+@table @code
+
+@item put_attr(+@var{Var},+@var{Module},+@var{Value})
+@findex put_attr/3
+@snindex put_attr/3
+@cnindex put_attr/3
+If @var{Var} is a variable or attributed variable, set the value for the
+attribute named @var{Module} to @var{Value}. If an attribute with this
+name is already associated with @var{Var}, the old value is replaced.
+Backtracking will restore the old value (i.e. an attribute is a mutable
+term. See also @code{setarg/3}). This predicate raises a type error if
+@var{Var} is not a variable or @var{Module} is not an atom.
+
+@item get_attr(+@var{Var},+@var{Module},+@var{Value})
+@findex get_attr/3
+@snindex get_attr/3
+@cnindex get_attr/3
+Request the current @var{value} for the attribute named @var{Module}.  If
+@var{Var} is not an attributed variable or the named attribute is not
+associated to @var{Var} this predicate fails silently.  If @var{Module}
+is not an atom, a type error is raised.
+
+@item del_attr(+@var{Var},+@var{Module})
+@findex del_attr/2
+@snindex del_attr/2
+@cnindex del_attr/2
+Delete the named attribute.  If @var{Var} loses its last attribute it
+is transformed back into a traditional Prolog variable.  If @var{Module}
+is not an atom, a type error is raised. In all other cases this
+predicate succeeds regarless whether or not the named attribute is
+present.
+
+@item attr_unify_hook(+@var{AttValue},+@var{VarValue})
+@findex attr_unify_hook/2
+@snindex attr_unify_hook/2
+@cnindex attr_unify_hook/2
+Hook that must be defined in the module an attributed variable refers
+to. Is is called @emph{after} the attributed variable has been
+unified with a non-var term, possibly another attributed variable.
+@var{AttValue} is the attribute that was associated to the variable
+in this module and @var{VarValue} is the new value of the variable.
+Normally this predicate fails to veto binding the variable to
+@var{VarValue}, forcing backtracking to undo the binding.  If
+@var{VarValue} is another attributed variable the hook often combines
+the two attribute and associates the combined attribute with 
+@var{VarValue} using @code{put_attr/3}.
+
+@c     \predicate{attr_portray_hook}{2}{+AttValue, +Var}
+@c Called by write_term/2 and friends for each attribute if the option
+@c \term{attributes}{portray} is in effect.  If the hook succeeds the
+@c attribute is considered printed.  Otherwise \exam{Module = ...} is
+@c printed to indicate the existence of a variable.
+@end table
+
+@subsection Special Purpose SWI Predicates for Attributes
+
+Normal user code should deal with @code{put_attr/3}, @code{get_attr/3}
+and @code{del_attr/2}.  The routines in this section fetch or set the
+entire attribute list of a variables. Use of these predicates is
+anticipated to be restricted to printing and other special purpose
+operations.
+
+@table @code
+@item get_attrs(+@var{Var},-@var{Attributes})
+@findex get_attrs/2
+@snindex get_attrs/2
+@cnindex get_attrs/2
+Get all attributes of @var{Var}. @var{Attributes} is a term of the form
+@code{att(Module, Value, MoreAttributes)}, where @var{MoreAttributes} is
+@code{[]} for the last attribute.
+
+@item put_attrs(+@var{Var},+@var{Attributes})
+@findex put_attrs/2
+@snindex put_attrs/2
+@cnindex put_attrs/2
+Set all attributes of @var{Var}.  See get_attrs/2 for a description of
+@var{Attributes}.
+
+@item copy_term_nat(?@var{TI},-@var{TF})
+@findex copy_term_nat/2
+@snindex copy_term_nat/2
+@cnindex copy_term_nat/2
+As @code{copy_term/2}.  Attributes however, are @emph{not} copied but replaced
+by fresh variables.
+@end table
+
+
+@node SWI-Prolog Global Variables,  ,hProlog and SWI-Prolog Attributed Variables,SWI-Prolog
+@section SWI Global variables
+@c		\label{sec:gvar}
+
+SWI-Prolog global variables are associations between names (atoms) and
+terms.  They differ in various ways from storing information using
+@code{assert/1} or @code{recorda/3}.
+
+@itemize @bullet
+@item The value lives on the Prolog (global) stack.  This implies 
+          that lookup time is independent from the size of the term.
+	  This is particulary interesting for large data structures
+	  such as parsed XML documents or the CHR global constraint
+	  store.
+
+@item They support both global assignment using @code{nb_setval/2} and
+          backtrackable assignment using @code{b_setval/2}.
+
+@item Only one value (which can be an arbitrary complex Prolog
+   	  term) can be associated to a variable at a time.
+
+@item Their value cannot be shared among threads.  Each thread
+          has its own namespace and values for global variables.
+
+@item Currently global variables are scoped globally.  We may
+          consider module scoping in future versions.
+@end itemize
+
+Both @code{b_setval/2} and @code{nb_setval/2} implicitely create a variable if the
+referenced name does not already refer to a variable.
+
+Global variables may be initialised from directives to make them
+available during the program lifetime, but some considerations are
+necessary for saved-states and threads. Saved-states to not store global
+variables, which implies they have to be declared with @code{initialization/1}
+to recreate them after loading the saved state.  Each thread has
+its own set of global variables, starting with an empty set.  Using
+@code{thread_inititialization/1} to define a global variable it will be
+defined, restored after reloading a saved state and created in all
+threads that are created @emph{after} the registration.
+
+
+@table @code
+@item b_setval(+@var{Name},+@var{Value})
+@findex b_setval/2
+@snindex b_setval/2
+@cnindex b_setval/2
+Associate the term @var{Value} with the atom @var{Name} or replaces
+the currently associated value with @var{Value}.  If @var{Name} does
+not refer to an existing global variable a variable with initial value
+@code{[]} is created (the empty list).  On backtracking the
+assignment is reversed.
+
+@item b_getval(+@var{Name},-@var{Value})
+@findex b_getval/2
+@snindex b_getval/2
+@cnindex b_getval/2
+Get the value associated with the global variable @var{Name} and unify
+it with @var{Value}. Note that this unification may further instantiate
+the value of the global variable. If this is undesirable the normal
+precautions (double negation or @code{copy_term/2}) must be taken. The
+@code{b_getval/2} predicate generates errors if @var{Name} is not an atom or
+the requested variable does not exist.
+@end table
+
+@table @code
+
+@item nb_setval(+@var{Name},+@var{Value})
+@findex nb_setval/2
+@snindex nb_setval/2
+@cnindex nb_setval/2
+Associates a copy of @var{Value} created with @code{duplicate_term/2}
+with the atom @var{Name}.  Note that this can be used to set an
+initial value other than @code{[]} prior to backtrackable assignment.
+
+@item nb_getval(+@var{Name},-@var{Value})
+@findex nb_getval/2
+@snindex nb_getval/2
+@cnindex nb_getval/2
+The @code{nb_getval/2} predicate is a synonym for b_getval/2, introduced for
+compatibility and symetry.  As most scenarios will use a particular
+global variable either using non-backtracable or backtrackable
+assignment, using @code{nb_getval/2} can be used to document that the 
+variable is used non-backtracable.
+
+@c     \predicate{nb_linkval}{2}{+Name, +Value}
+@c Associates the term @var{Value} with the atom @var{Name} without copying
+@c it. This is a fast special-purpose variation of nb_setval/2 intended for
+@c expert users only because the semantics on backtracking to a point
+@c before creating the link are poorly defined for compound terms. The
+@c principal term is always left untouched, but backtracking behaviour on
+@c arguments is undone if the orginal assignment was \jargon{trailed} and
+@c left alone otherwise, which implies that the history that created the
+@c term affects the behaviour on backtracking. Please consider the
+@c following example:
+
+@c \begin{code}
+@c demo_nb_linkval :-
+@c 	T = nice(N),
+@c 	(   N = world,
+@c 	    nb_linkval(myvar, T),
+@c 	    fail
+@c 	;   nb_getval(myvar, V),
+@c 	    writeln(V)
+@c 	).
+@c \end{code}
+
+@item nb_current(?@var{Name},?@var{Value})
+@findex nb_current/2
+@snindex nb_current/2
+@cnindex nb_current/2
+Enumerate all defined variables with their value. The order of
+enumeration is undefined.
+
+@item nb_delete(?@var{Name})
+@findex nb_delete/1
+@snindex nb_delete/1
+@cnindex nb_delete/1
+Delete the named global variable.
+@end table
+
+@subsection Compatibility of SWI-Prolog Global Variables
+
+Global variables have been introduced by various Prolog
+implementations recently.  The implementation of them in SWI-Prolog is
+based on hProlog by Bart Demoen. In discussion with Bart it was
+decided that the semantics if hProlog @code{nb_setval/2}, which is
+equivalent to @code{nb_linkval/2} is not acceptable for normal Prolog
+users as the behaviour is influenced by how builtin predicates
+constructing terms (@code{read/1}, @code{=../2}, etc.) are implemented.
+
+GNU-Prolog provides a rich set of global variables, including arrays.
+Arrays can be implemented easily in SWI-Prolog using @code{functor/3} and
+@code{setarg/3} due to the unrestricted arity of compound terms.
+
+
+@node Extensions,Debugging,SWI-Prolog,Top 
+@chapter Extensions to Prolog
+
+YAP includes several extensions that are not enabled by
+default, but that can be used to extend the functionality of the
+system. These options can be set at compilation time by enabling the
+related compilation flag, as explained in the @code{Makefile}
diff --git a/docs/yap.tex b/docs/yap.tex
index 20cd489a3..86f7ee2e5 100644
--- a/docs/yap.tex
+++ b/docs/yap.tex
@@ -77,44 +77,6 @@ Machine), with several optimizations for better performance. YAP follows
 the Edinburgh tradition, and is largely compatible with DEC-10 Prolog,
 Quintus Prolog, and especially with C-Prolog.
 
-This file contains the CLP(Q,R) manual as distributed by the Austrian
-Research Institute for Artificial Intelligence (OFAI). Permission on
-this document follows the following license:
-
-Copyright @copyright{} 1992,1993,1994,1995 OFAI Austrian Research
-Institute for Artificial Intelligence (OFAI) Schottengasse 3 A-1010
-Vienna, Austria
-
-Permission is granted to make and distribute verbatim copies of this
-manual provided the copyright notice and this permission notice are
-preserved on all copies.
-
-Permission is granted to copy and distribute modified versions of this
-manual under the conditions for verbatim copying, provided that the
-entire resulting derived work is distributed under the terms of a
-permission notice identical to this one.
-
-Permission is granted to copy and distribute translations of this
-manual into another language, under the above conditions for modified
-versions, except that this permission notice may be stated in a
-translation approved by the OFAI.
-
-This file contains a chapter on CHR. This package is distributed under
-license from LMU (Ludwig-Maximilians-University), Munich, Germany:
-
-Permission is granted to copy and distribute modified versions of this
-chapter under the conditions for verbatim copying, provided that the entire
-resulting derived work is distributed under the terms of a permission
-notice identical to this one.
-
-Permission is granted to copy and distribute translations of this chapter
-into another language, under the above conditions for modified versions,
-except that this permission notice may be stated in a translation approved
-by LMU.
-
-Copyright @copyright{} 1996-98 LMU (Ludwig-Maximilians-University)@*
-Munich, Germany
-
 This file contains extracts of the SWI-Prolog manual, as written by Jan
 Wielemaker. Our thanks to the author for his kind permission in allowing
 us to include his text in this document.
@@ -133,7 +95,7 @@ us to include his text in this document.
 * Rational Trees:: Working with Rational Trees
 * Coroutining:: Changing the Execution of Goals
 * Attributed Variables:: Using attributed Variables
-* CLPQR:: The CLP(Q,R) System
+* CLPR:: The CLP(R) System
 * CHR:: The CHR System
 * Logtalk:: The Logtalk Object-Oriented System
 * Threads:: Thread Library
@@ -262,42 +224,47 @@ Subnodes of SWI-Prolog
 * hProlog and SWI-Prolog Attributed Variables :: Emulating SWI-like attributed variables
 * SWI-Prolog Global Variables :: Emulating SWI-like attributed variables
 
-Subnodes of CLP(Q,R)
-* Introduction to CLPQR:: The CLP(Q,R) System
-* Referencing CLPQR:: How to Reference CLP(Q,R)
-* CLPQR Acknowledgments:: Acknowledgments for CLP(Q,R)
-* Solver Interface:: Using the CLP(Q,R) System
-* Notational Conventions:: The CLP(Q,R) Notation
-* Solver Predicates:: The CLP(Q,R) Interface Predicates
-* Unification:: Unification and CLP(Q,R)
-* Feedback and Bindings:: Information flow in CLP(Q,R)
-* Linearity and Nonlinear Residues:: Linear and Nonlinear Constraints
-* How Nonlinear Residues are made to disappear:: Handling Nonlinear Residues
-* Isolation Axioms:: Isolating the Variable to be Solved
-* Numerical Precision and Rationals:: Reals and Rationals
-* Projection and Redundancy Elimination:: Presenting Bindings for Query Variables
-* Variable Ordering:: Linear Relationships between Variables
-* Turning Answers into Terms:: using @code{call_residue/2}
-* Projecting Inequalities:: How to project linear inequations
-* Why Disequations:: Using Disequations in CLP(Q,R)
-* Syntactic Sugar:: An easier syntax
-* Monash Examples:: The Monash Library
-* Compatibility Notes:: CLP(Q,R) and the clp(R) interpreter
-* A Mixed Integer Linear Optimization Example:: MIP models
-* Implementation Architecture:: CLP(Q,R) Components
-* Fragments and Bits:: Final Last Words on CLP(Q,R)
-* CLPQR Bugs:: Bugs in CLP(Q,R)
-* CLPQR References:: References for CLP(Q,R)
+@c Subnodes of CLP(Q,R)
+@c * Introduction to CLPQ:: The CLP(Q,R) System
+@c * Referencing CLPQR:: How to Reference CLP(Q,R)
+@c * CLPQR Acknowledgments:: Acknowledgments for CLP(Q,R)
+@c * Solver Interface:: Using the CLP(Q,R) System
+@c * Notational Conventions:: The CLP(Q,R) Notation
+@c * Solver Predicates:: The CLP(Q,R) Interface Predicates
+@c * Unification:: Unification and CLP(Q,R)
+@c * Feedback and Bindings:: Information flow in CLP(Q,R)
+@c * Linearity and Nonlinear Residues:: Linear and Nonlinear Constraints
+@c * How Nonlinear Residues are made to disappear:: Handling Nonlinear Residues
+@c * Isolation Axioms:: Isolating the Variable to be Solved
+@c * Numerical Precision and Rationals:: Reals and Rationals
+@c * Projection and Redundancy Elimination:: Presenting Bindings for Query Variables
+@c * Variable Ordering:: Linear Relationships between Variables
+@c * Turning Answers into Terms:: using @code{call_residue/2}
+@c * Projecting Inequalities:: How to project linear inequations
+@c * Why Disequations:: Using Disequations in CLP(Q,R)
+@c * Syntactic Sugar:: An easier syntax
+@c * Monash Examples:: The Monash Library
+@c * Compatibility Notes:: CLP(Q,R) and the clp(R) interpreter
+@c * A Mixed Integer Linear Optimization Example:: MIP models
+@c * Implementation Architecture:: CLP(Q,R) Components
+@c * Fragments and Bits:: Final Last Words on CLP(Q,R)
+@c * CLPQR Bugs:: Bugs in CLP(Q,R)
+@c * CLPQR References:: References for CLP(Q,R)
+
+Subnodes of CLPR
+* CLPR Solver Predicates::
+* CLPR Syntax::
+* CLPR Unification::
+* CLPR Non-linear Constraints::               
 
 Subnodes of CHR
-* CHR Copyright::               
 * CHR Introduction::            
-* CHR Introductory Examples::   
-* CHR Library::                 
+* CHR Syntax and Semantics::
+* CHR in YAP Programs::
 * CHR Debugging::               
-* CHR Programming Hints::       
-* CHR Constraint Handlers::     
-* CHR Backward Compatibility::  
+* CHR Examples::       
+* CHR Compatibility::     
+* CHR Guidelines::  
 
 Subnodes of C-Interface
 * Manipulating Terms:: Primitives available to the C programmer
@@ -413,46 +380,12 @@ authorization to include these packages.
 The packages are, in alphabetical order:
 
 @itemize @bullet
-@item The CHR package developed at TUM by
-Ludwig-Maximilians-Universitaet Muenchen (LMU) by Dr. Fruehwirth Thom
-and by Dr. Christian Holzbaur. The package is distributed under license
-from LMU (Ludwig-Maximilians-University), Munich, Germany:
+@item The CHR package developed by Tom Schrijvers,
+Christian Holzbaur, and Jan Wielemaker.
 
-Permission is granted to copy and distribute modified versions of this
-chapter under the conditions for verbatim copying, provided that the entire
-resulting derived work is distributed under the terms of a permission
-notice identical to this one.
-
-Permission is granted to copy and distribute translations of this chapter
-into another language, under the above conditions for modified versions,
-except that this permission notice may be stated in a translation approved
-by LMU.
-
-Copyright @copyright{} 1996-98 LMU (Ludwig-Maximilians-University)@*
-Munich, Germany
-
-@item The CLP(Q,R) package developed at OFAI Austrian Research
-Institute for Artificial Intelligence by Christian Holzbaur. The package
-is distributed under the OFAI license. Documentation on this package is
-a chapter of this manual, which is covered by the OFAI license:
-
-Copyright @copyright{} 1992,1993,1994,1995 OFAI Austrian Research
-Institute for Artificial Intelligence (OFAI) Schottengasse 3 A-1010
-Vienna, Austria
-
-Permission is granted to make and distribute verbatim copies of this
-manual provided the copyright notice and this permission notice are
-preserved on all copies.
-
-Permission is granted to copy and distribute modified versions of this
-manual under the conditions for verbatim copying, provided that the
-entire resulting derived work is distributed under the terms of a
-permission notice identical to this one.
-
-Permission is granted to copy and distribute translations of this
-manual into another language, under the above conditions for modified
-versions, except that this permission notice may be stated in a
-translation approved by the OFAI.
+@item The CLP(R) package developed Leslie De Koninck, Bart Demoen, Tom
+Schrijvers and Jan Wielemaker and based on the CLP(Q,R) implementation
+by Christian Holzbauer.
 
 @item The Logtalk Object-Oriented system is developed at the University 
 of Beira Interior, Portugal, by Paulo Moura.
@@ -470,7 +403,7 @@ yap.tex.
 @item The yap2swi library implements some of the functionality of
 SWI's PL interface. Please do refer to the SWI-Prolog home page:
 
-@code{http://www.swi-prolog.org}
+@url{http://www.swi-prolog.org}
 
 for more information on SWI-Prolog and for a detailed description of its
 foreign interface.
@@ -8816,7 +8749,6 @@ V = [1,3,5]
 @end table
 
 @node SWI-Prolog, Extensions, Library, Top
-@chapter SWI-Prolog Emulation
 @cindex SWI-Prolog
 
 @menu SWI-Prolog Emulation
@@ -8827,499 +8759,7 @@ Subnodes of SWI-Prolog
 * SWI-Prolog Global Variables :: Emulating SWI-like attributed variables
 @end menu
 
-This library provides a number of SWI-Prolog builtins that are not by
-default in YAP. This library is loaded with the
-@code{use_module(library(swi))} command.
-
-@table @code
-
-@item append(?@var{List1},?@var{List2},?@var{List3})
-@findex append/3
-@snindex append/3
-@cnindex append/3
-Succeeds when @var{List3} unifies with the concatenation of @var{List1}
-and @var{List2}. The predicate can be used with any instantiation
-pattern (even three variables).
-
-@item between(+@var{Low},+@var{High},?@var{Value})
-@findex between/3
-@snindex between/3
-@cnindex between/3
-
-@var{Low} and @var{High} are integers, @var{High} less or equal than
-@var{Low}. If @var{Value} is an integer, @var{Low} less or equal than
-@var{Value} less or equal than @var{High}.  When @var{Value} is a
-variable it is successively bound to all integers between @var{Low} and
-@var{High}.  If @var{High} is @code{inf}, @code{between/3} is true iff
-@var{Value} less or equal than @var{Low}, a feature that is particularly
-interesting for generating integers from a certain value.
-
-@item chdir(+@var{Dir})
-@findex chdir/1
-@snindex chdir/1
-@cnindex chdir/1
-
-Compatibility predicate.  New code should use @code{working_directory/2}.
-
-@item concat_atom(+@var{List},-@var{Atom})
-@findex concat_atom/2
-@snindex concat_atom/2
-@cnindex concat_atom/2
-
-@var{List} is a list of atoms, integers or floating point numbers. Succeeds
-if @var{Atom} can be unified with the concatenated elements of @var{List}. If
-@var{List} has exactly 2 elements it is equivalent to @code{atom_concat/3},
-allowing for variables in the list.
-
-@item concat_atom(?@var{List},+@var{Separator},?@var{Atom})
-@findex concat_atom/3
-@snindex concat_atom/3
-@cnindex concat_atom/3
-
-Creates an atom just like concat_atom/2, but inserts @var{Separator}
-between each pair of atoms.  For example:
-\@example
-?- concat_atom([gnu, gnat], ', ', A).
-
-A = 'gnu, gnat'
-@end example
-
-(Unimplemented) This predicate can also be used to split atoms by
-instantiating @var{Separator} and @var{Atom}:
-
-@example
-?- concat_atom(L, -, 'gnu-gnat').
-
-L = [gnu, gnat]
-@end example
-
-@item nth1(+@var{Index},?@var{List},?@var{Elem})
-@findex nth1/3
-@snindex nth1/3
-@cnindex nth1/3
-Succeeds when the @var{Index}-th element of @var{List} unifies with
-@var{Elem}. Counting starts at 1.
-
-Set environment variable.  @var{Name} and @var{Value} should be
-instantiated to atoms or integers.  The environment variable will be
-passed to @code{shell/[0-2]} and can be requested using @code{getenv/2}.
-They also influence @code{expand_file_name/2}.
-
-@item setenv(+@var{Name},+@var{Value})
-@findex setenv/2
-@snindex setenv/2
-@cnindex setenv/2
-Set environment variable.  @var{Name} and @var{Value} should be
-instantiated to atoms or integers.  The environment variable will be
-passed to @code{shell/[0-2]} and can be requested using @code{getenv/2}.
-They also influence @code{expand_file_name/2}.
-
-@item term_to_atom(?@var{Term},?@var{Atom})
-@findex term_to_atom/2
-@snindex term_to_atom/2
-@cnindex term_to_atom/2
-Succeeds if @var{Atom} describes a term that unifies with @var{Term}. When
-@var{Atom} is instantiated @var{Atom} is converted and then unified with
-@var{Term}.  If @var{Atom} has no valid syntax, a @code{syntax_error}
-exception is raised. Otherwise @var{Term} is ``written'' on @var{Atom}
-using @code{write/1}.
-
-@item working_directory(-@var{Old},+@var{New})
-@findex working_directory/2
-@snindex working_directory/2
-@cnindex working_directory/2
-
-Unify @var{Old} with an absolute path to the current working directory
-and change working directory to @var{New}.  Use the pattern
-@code{working_directory(CWD, CWD)} to get the current directory.  See
-also @code{absolute_file_name/2} and @code{chdir/1}.
-
-@end table
-
-@node Invoking Predicates on all Members of a List,Forall, , SWI-Prolog
-@section Invoking Predicates on all Members of a List
-@c \label{sec:applylist}
-
-All the predicates in this section call a predicate on all members of a
-list or until the predicate called fails.  The predicate is called via
-@code{call/[2..]}, which implies common arguments can be put in
-front of the arguments obtained from the list(s). For example:
-
-@example
-?- maplist(plus(1), [0, 1, 2], X).
-
-X = [1, 2, 3]
-@end example
-
-we will phrase this as ``@var{Predicate} is applied on ...''
-
-@table @code
-
-@item maplist(+@var{Pred},+@var{List})
-@findex maplist/2
-@snindex maplist/2
-@cnindex maplist/2
-@var{Pred} is applied successively on each element of @var{List} until
-the end of the list or @var{Pred} fails. In the latter case 
-@code{maplist/2} fails.
-
-@item maplist(+@var{Pred},+@var{List1},+@var{List2})
-@findex maplist/3
-@snindex maplist/3
-@cnindex maplist/3
-Apply @var{Pred} on all successive triples of elements from
-@var{List1} and
-@var{List2}. Fails if @var{Pred} can not be applied to a
-pair. See the example above.
-
-@item maplist(+@var{Pred},+@var{List1},+@var{List2},+@var{List4})
-@findex maplist/4
-@snindex maplist/4
-@cnindex maplist/4
-Apply @var{Pred} on all successive triples of elements from @var{List1},
-@var{List2} and @var{List3}. Fails if @var{Pred} can not be applied to a
-triple. See the example above.
-
-@c @item findlist(+@var{Pred},+@var{List1},?@var{List2})
-@c @findex findlist/3
-@c @snindex findlist/3
-@c @cnindex findlist/3
-@c Unify @var{List2} with a list of all elements of @var{List1} to which
-@c @var{Pred} applies.
-@end table
-
-@node Forall,hProlog and SWI-Prolog Attributed Variables,Invoking Predicates on all Members of a List, SWI-Prolog
-@section Forall			
-@c \label{sec:forall2}
-
-@table @code
-@item forall(+@var{Cond},+@var{Action})
-@findex forall/2
-@snindex forall/2
-@cnindex forall/2
-
-For all alternative bindings of @var{Cond} @var{Action} can be proven.
-The next example verifies that all arithmetic statements in the list
-@var{L} are correct. It does not say which is wrong if one proves wrong.
-
-@example
-?- forall(member(Result = Formula, [2 = 1 + 1, 4 = 2 * 2]),
-                 Result =:= Formula).
-@end example
-
-@end table
-
-@node hProlog and SWI-Prolog Attributed Variables, SWI-Prolog Global Variables, Forall,SWI-Prolog
-@section hProlog and SWI-Prolog Attributed Variables
-@cindex hProlog Attributed Variables
-
-Attributed variables
-@c @ref{Attributed variables}
-provide a technique for extending the
-Prolog unification algorithm by hooking the binding of attributed
-variables. There is little consensus in the Prolog community on the
-exact definition and interface to attributed variables.  Yap Prolog
-traditionally implements a SICStus-like interface, but to enable
-SWI-compatibility we have implemented the SWI-Prolog interface,
-identical to the one realised by Bart Demoen for hProlog.
-
-Binding an attributed variable schedules a goal to be executed at the
-first possible opportunity. In the current implementation the hooks are
-executed immediately after a successful unification of the clause-head
-or successful completion of a foreign language (builtin) predicate. Each
-attribute is associated to a module and the hook (attr_unify_hook/2) is
-executed in this module.  The example below realises a very simple and
-incomplete finite domain reasoner.
-
-@example
-:- module(domain,
-	  [ domain/2			% Var, ?Domain
-	  ]).
-:- use_module(library(oset)).
-
-domain(X, Dom) :-
-	var(Dom), !,
-	get_attr(X, domain, Dom).
-domain(X, List) :-
-	sort(List, Domain),
-	put_attr(Y, domain, Domain),
-	X = Y.
-
-%	An attributed variable with attribute value Domain has been
-%	assigned the value Y
-
-attr_unify_hook(Domain, Y) :-
-	(   get_attr(Y, domain, Dom2)
-	->  oset_int(Domain, Dom2, NewDomain),
-	    (   NewDomain == []
-	    ->	fail
-	    ;	NewDomain = [Value]
-	    ->	Y = Value
-	    ;	put_attr(Y, domain, NewDomain)
-	    )
-	;   var(Y)
-	->  put_attr( Y, domain, Domain )
-	;   memberchk(Y, Domain)
-	).
-@end example
-
-
-Before explaining the code we give some example queries:
-
-@table @code
-@item ?- domain(X, [a,b]), X = c		     
-no
-@item ?- domain(X, [a,b]), domain(X, [a,c]).   
-      X = a
-@item ?- domain(X, [a,b,c]), domain(X, [a,c]). 
-  X = _D0
-@end table
-
-The predicate @code{domain/2} fetches (first clause) or assigns
-(second clause) the variable a @emph{domain}, a set of values it can
-be unified with.  In the second clause first associates the domain
-with a fresh variable and then unifies X to this variable to deal
-with the possibility that X already has a domain. The
-predicate @code{attr_unify_hook/2} is a hook called after a variable with
-a domain is assigned a value.  In the simple case where the variable
-is bound to a concrete value we simply check whether this value is in
-the domain. Otherwise we take the intersection of the domains and either
-fail if the intersection is empty (first example), simply assign the
-value if there is only one value in the intersection (second example) or
-assign the intersection as the new domain of the variable (third
-example).
-
-
-@table @code
-
-@item put_attr(+@var{Var},+@var{Module},+@var{Value})
-@findex put_attr/3
-@snindex put_attr/3
-@cnindex put_attr/3
-If @var{Var} is a variable or attributed variable, set the value for the
-attribute named @var{Module} to @var{Value}. If an attribute with this
-name is already associated with @var{Var}, the old value is replaced.
-Backtracking will restore the old value (i.e. an attribute is a mutable
-term. See also @code{setarg/3}). This predicate raises a type error if
-@var{Var} is not a variable or @var{Module} is not an atom.
-
-@item get_attr(+@var{Var},+@var{Module},+@var{Value})
-@findex get_attr/3
-@snindex get_attr/3
-@cnindex get_attr/3
-Request the current @var{value} for the attribute named @var{Module}.  If
-@var{Var} is not an attributed variable or the named attribute is not
-associated to @var{Var} this predicate fails silently.  If @var{Module}
-is not an atom, a type error is raised.
-
-@item del_attr(+@var{Var},+@var{Module})
-@findex del_attr/2
-@snindex del_attr/2
-@cnindex del_attr/2
-Delete the named attribute.  If @var{Var} loses its last attribute it
-is transformed back into a traditional Prolog variable.  If @var{Module}
-is not an atom, a type error is raised. In all other cases this
-predicate succeeds regarless whether or not the named attribute is
-present.
-
-@item attr_unify_hook(+@var{AttValue},+@var{VarValue})
-@findex attr_unify_hook/2
-@snindex attr_unify_hook/2
-@cnindex attr_unify_hook/2
-Hook that must be defined in the module an attributed variable refers
-to. Is is called @emph{after} the attributed variable has been
-unified with a non-var term, possibly another attributed variable.
-@var{AttValue} is the attribute that was associated to the variable
-in this module and @var{VarValue} is the new value of the variable.
-Normally this predicate fails to veto binding the variable to
-@var{VarValue}, forcing backtracking to undo the binding.  If
-@var{VarValue} is another attributed variable the hook often combines
-the two attribute and associates the combined attribute with 
-@var{VarValue} using @code{put_attr/3}.
-
-@c     \predicate{attr_portray_hook}{2}{+AttValue, +Var}
-@c Called by write_term/2 and friends for each attribute if the option
-@c \term{attributes}{portray} is in effect.  If the hook succeeds the
-@c attribute is considered printed.  Otherwise \exam{Module = ...} is
-@c printed to indicate the existence of a variable.
-@end table
-
-@subsection Special Purpose SWI Predicates for Attributes
-
-Normal user code should deal with @code{put_attr/3}, @code{get_attr/3}
-and @code{del_attr/2}.  The routines in this section fetch or set the
-entire attribute list of a variables. Use of these predicates is
-anticipated to be restricted to printing and other special purpose
-operations.
-
-@table @code
-@item get_attrs(+@var{Var},-@var{Attributes})
-@findex get_attrs/2
-@snindex get_attrs/2
-@cnindex get_attrs/2
-Get all attributes of @var{Var}. @var{Attributes} is a term of the form
-@code{att(Module, Value, MoreAttributes)}, where @var{MoreAttributes} is
-@code{[]} for the last attribute.
-
-@item put_attrs(+@var{Var},+@var{Attributes})
-@findex put_attrs/2
-@snindex put_attrs/2
-@cnindex put_attrs/2
-Set all attributes of @var{Var}.  See get_attrs/2 for a description of
-@var{Attributes}.
-
-@item copy_term_nat(?@var{TI},-@var{TF})
-@findex copy_term_nat/2
-@snindex copy_term_nat/2
-@cnindex copy_term_nat/2
-As @code{copy_term/2}.  Attributes however, are @emph{not} copied but replaced
-by fresh variables.
-@end table
-
-
-@node SWI-Prolog Global Variables,  ,hProlog and SWI-Prolog Attributed Variables,SWI-Prolog
-@section SWI Global variables
-@c		\label{sec:gvar}
-
-SWI-Prolog global variables are associations between names (atoms) and
-terms.  They differ in various ways from storing information using
-@code{assert/1} or @code{recorda/3}.
-
-@itemize @bullet
-@item The value lives on the Prolog (global) stack.  This implies 
-          that lookup time is independent from the size of the term.
-	  This is particulary interesting for large data structures
-	  such as parsed XML documents or the CHR global constraint
-	  store.
-
-@item They support both global assignment using @code{nb_setval/2} and
-          backtrackable assignment using @code{b_setval/2}.
-
-@item Only one value (which can be an arbitrary complex Prolog
-   	  term) can be associated to a variable at a time.
-
-@item Their value cannot be shared among threads.  Each thread
-          has its own namespace and values for global variables.
-
-@item Currently global variables are scoped globally.  We may
-          consider module scoping in future versions.
-@end itemize
-
-Both @code{b_setval/2} and @code{nb_setval/2} implicitely create a variable if the
-referenced name does not already refer to a variable.
-
-Global variables may be initialised from directives to make them
-available during the program lifetime, but some considerations are
-necessary for saved-states and threads. Saved-states to not store global
-variables, which implies they have to be declared with @code{initialization/1}
-to recreate them after loading the saved state.  Each thread has
-its own set of global variables, starting with an empty set.  Using
-@code{thread_inititialization/1} to define a global variable it will be
-defined, restored after reloading a saved state and created in all
-threads that are created @emph{after} the registration.
-
-
-@table @code
-@item b_setval(+@var{Name},+@var{Value})
-@findex b_setval/2
-@snindex b_setval/2
-@cnindex b_setval/2
-Associate the term @var{Value} with the atom @var{Name} or replaces
-the currently associated value with @var{Value}.  If @var{Name} does
-not refer to an existing global variable a variable with initial value
-@code{[]} is created (the empty list).  On backtracking the
-assignment is reversed.
-
-@item b_getval(+@var{Name},-@var{Value})
-@findex b_getval/2
-@snindex b_getval/2
-@cnindex b_getval/2
-Get the value associated with the global variable @var{Name} and unify
-it with @var{Value}. Note that this unification may further instantiate
-the value of the global variable. If this is undesirable the normal
-precautions (double negation or @code{copy_term/2}) must be taken. The
-@code{b_getval/2} predicate generates errors if @var{Name} is not an atom or
-the requested variable does not exist.
-@end table
-
-@table @code
-
-@item nb_setval(+@var{Name},+@var{Value})
-@findex nb_setval/2
-@snindex nb_setval/2
-@cnindex nb_setval/2
-Associates a copy of @var{Value} created with @code{duplicate_term/2}
-with the atom @var{Name}.  Note that this can be used to set an
-initial value other than @code{[]} prior to backtrackable assignment.
-
-@item nb_getval(+@var{Name},-@var{Value})
-@findex nb_getval/2
-@snindex nb_getval/2
-@cnindex nb_getval/2
-The @code{nb_getval/2} predicate is a synonym for b_getval/2, introduced for
-compatibility and symetry.  As most scenarios will use a particular
-global variable either using non-backtracable or backtrackable
-assignment, using @code{nb_getval/2} can be used to document that the 
-variable is used non-backtracable.
-
-@c     \predicate{nb_linkval}{2}{+Name, +Value}
-@c Associates the term @var{Value} with the atom @var{Name} without copying
-@c it. This is a fast special-purpose variation of nb_setval/2 intended for
-@c expert users only because the semantics on backtracking to a point
-@c before creating the link are poorly defined for compound terms. The
-@c principal term is always left untouched, but backtracking behaviour on
-@c arguments is undone if the orginal assignment was \jargon{trailed} and
-@c left alone otherwise, which implies that the history that created the
-@c term affects the behaviour on backtracking. Please consider the
-@c following example:
-
-@c \begin{code}
-@c demo_nb_linkval :-
-@c 	T = nice(N),
-@c 	(   N = world,
-@c 	    nb_linkval(myvar, T),
-@c 	    fail
-@c 	;   nb_getval(myvar, V),
-@c 	    writeln(V)
-@c 	).
-@c \end{code}
-
-@item nb_current(?@var{Name},?@var{Value})
-@findex nb_current/2
-@snindex nb_current/2
-@cnindex nb_current/2
-Enumerate all defined variables with their value. The order of
-enumeration is undefined.
-
-@item nb_delete(?@var{Name})
-@findex nb_delete/1
-@snindex nb_delete/1
-@cnindex nb_delete/1
-Delete the named global variable.
-@end table
-
-@subsection Compatibility of SWI-Prolog Global Variables
-
-Global variables have been introduced by various Prolog
-implementations recently.  The implementation of them in SWI-Prolog is
-based on hProlog by Bart Demoen. In discussion with Bart it was
-decided that the semantics if hProlog @code{nb_setval/2}, which is
-equivalent to @code{nb_linkval/2} is not acceptable for normal Prolog
-users as the behaviour is influenced by how builtin predicates
-constructing terms (@code{read/1}, @code{=../2}, etc.) are implemented.
-
-GNU-Prolog provides a rich set of global variables, including arrays.
-Arrays can be implemented easily in SWI-Prolog using @code{functor/3} and
-@code{setarg/3} due to the unrestricted arity of compound terms.
-
-
-@node Extensions,Debugging,SWI-Prolog,Top 
-@chapter Extensions to Prolog
-
-YAP includes several extensions that are not enabled by
-default, but that can be used to extend the functionality of the
-system. These options can be set at compilation time by enabling the
-related compilation flag, as explained in the @code{Makefile}
+@include swi.tex
 
 @menu
 Extensions to Traditional Prolog
@@ -9327,7 +8767,7 @@ Extensions to Traditional Prolog
 * Rational Trees:: Working with Rational Trees
 * Coroutining:: Changing the Execution of Goals
 * Attributed Variables:: Using attributed Variables
-* CLPQR:: The CLP(Q,R) System
+* CLPR:: The CLP(R) System
 * Logtalk:: The Logtalk Object-Oriented system
 * Threads:: Thread Library
 * Parallelism:: Running in Or-Parallel
@@ -9465,7 +8905,7 @@ suspended.
 
 @end table
 
-@node Attributed Variables, CLPQR, Coroutining, Extensions
+@node Attributed Variables, CLPR, Coroutining, Extensions
 @chapter Attributed Variables
 @cindex attributed variables
 
@@ -9862,2844 +9302,32 @@ in more sophisticated solvers.  The corresponding
 attributes from other known solvers/modules via the module prefix in
 @code{@var{Module}:get_atts/2}.
 
-@node CLPQR, CHR, Attributed Variables, Extensions
-@chapter CLP(Q,R) Manual
+@node CLPR, CHR, Attributed Variables, Extensions
 @cindex CLPQ
 @cindex CLPR
 
 @menu
-CLP(Q,R)
-* Introduction to CLPQR:: The CLP(Q,R) System
-* Referencing CLPQR:: How to Reference CLP(Q,R)
-* CLPQR Acknowledgments:: Acknowledgments for CLP(Q,R)
-* Solver Interface:: Using the CLP(Q,R) System
-* Notational Conventions:: The CLP(Q,R) Notation
-* Solver Predicates:: The CLP(Q,R) Interface Predicates
-* Unification:: Unification and CLP(Q,R)
-* Feedback and Bindings:: Information flow in CLP(Q,R)
-* Linearity and Nonlinear Residues:: Linear and Nonlinear Constraints
-* How Nonlinear Residues are made to disappear:: Handling Nonlinear Residues
-* Isolation Axioms:: Isolating the Variable to be Solved
-* Numerical Precision and Rationals:: Reals and Rationals
-* Projection and Redundancy Elimination:: Presenting Bindings for Query Variables
-* Variable Ordering:: Linear Relationships between Variables
-* Turning Answers into Terms:: using @code{call_residue/2}
-* Projecting Inequalities:: How to project linear inequations
-* Why Disequations:: Using Disequations in CLP(Q,R)
-* Syntactic Sugar:: An easier syntax
-* Monash Examples:: The Monash Library
-* Compatibility Notes:: CLP(Q,R) and the clp(R) interpreter
-* A Mixed Integer Linear Optimization Example:: MIP models
-* Implementation Architecture:: CLP(Q,R) Components
-* Fragments and Bits:: Final Last Words on CLP(Q,R)
-* CLPQR Bugs:: Bugs in CLP(Q,R)
-* CLPQR References:: References for CLP(Q,R)
+* CLPR Solver Predicates::
+* CLPR Syntax::
+* CLPR Unification::
+* CLPR Non-linear Constraints::               
 @end menu
 
-This Manual documents a Prolog implementation of clp(Q,R), based on
-SICStus featuring extensible unification via attributed variables.
+@include clpr.tex
 
-Edition 1.3.3 December 1995
-
-Christian Holzbaur @code{christian@@ai.univie.ac.at}
-
-Copyright @copyright{} 1992,1993,1994,1995 OFAI Austrian Research
-Institute for Artificial Intelligence (OFAI) Schottengasse 3 A-1010
-Vienna, Austria
-
-Permission is granted to make and distribute verbatim copies of this
-manual provided the copyright notice and this permission notice are
-preserved on all copies.
-
-Permission is granted to copy and distribute modified versions of this
-manual under the conditions for verbatim copying, provided that the
-entire resulting derived work is distributed under the terms of a
-permission notice identical to this one.
-
-Permission is granted to copy and distribute translations of this
-manual into another language, under the above conditions for modified
-versions, except that this permission notice may be stated in a
-translation approved by the OFAI.
-
-@node Introduction to CLPQR, Referencing CLPQR, , CLPQR
-@section Introduction to CLP(Q,R)
-
-The clp(Q,R) system described in this document is an instance of the
-general Constraint Logic Programming scheme introduced by [Jaffar &
-Michaylov 87].
-
-The implementation is at least as complete as other existing clp(R)
-implementations: It solves linear equations over rational or real
-valued variables, covers the lazy treatment of nonlinear equations,
-features a decision algorithm for linear inequalities that detects
-implied equations, removes redundancies, performs projections
-(quantifier elimination), allows for linear dis-equations, and
-provides for linear optimization.
-
-The full clp(Q,R) distribution, including a stand-alone manual and an
-examples directory that is possibly more up to date than the version
-in the SICStus Prolog distribution, is available from:
-http://www.ai.univie.ac.at/clpqr/.
-
-@node Referencing CLPQR, CLPQR Acknowledgments, Introduction to CLPQR, CLPQR
-@section  Referencing CLP(Q,R)
-
-When referring to this implementation of clp(Q,R) in publications, you
-should use the following reference:
-
-Holzbaur C.: OFAI clp(q,r) Manual, Edition 1.3.3, Austrian Research
-Institute for Artificial Intelligence, Vienna, TR-95-09, 1995.
-
-@node CLPQR Acknowledgments, Solver Interface, Referencing CLPQR, CLPQR
-@section  CLP(QR) Acknowledgments
-Acknowledgments
-
-The development of this software was supported by the Austrian Fonds
-zur Foerderung der Wissenschaftlichen Forschung under grant
-P9426-PHY. Financial support for the Austrian Research Institute for
-Artificial Intelligence is provided by the Austrian Federal Ministry
-for Science and Research.
-
-We include a collection of examples that has been distributed with the
-Monash University version of clp(R) [Heintze et al. 87], and its
-inclusion into this distribution was kindly permitted by Roland Yap.
-
-@node Solver Interface, Notational Conventions, CLPQR Acknowledgments, CLPQR
-@section Solver Interface
-
-Rational numbers are not first class citizens in SICStus Prolog, so
-rational arithmetics has to be emulated. Because of the emulation it
-is too expensive to support arithmetics with automatic coercion
-between all sorts of numbers, like you find it in CommonLisp, for
-example.
-
-You must choose whether you want to operate in the field of Q
-(Rationals) or R (Reals):
-
-@example
- ?- use_module(library(clpq)).
-@end example
-
- or
-@example
- ?- use_module(library(clpr)).
-@end example
-
-@node Notational Conventions, Solver Predicates, Solver Interface, CLPQR
-@section Notational Conventions
-
-Throughout this chapter, the prompts @code{clp(q) ?-} and @code{clp(r)
-?-} are used to differentiate between clp(Q) and clp(R) in exemplary
-interactions.
-
-In general there are many ways to express the same linear
-relationship. This degree of freedom is manifest in the fact that the
-printed manual and an actual interaction with the current version of
-clp(Q,R) may show syntactically different answer constraints, despite
-the fact the same semantic relationship is being expressed. There are
-means to control the presentation, see @pxref{Variable Ordering}. The
-approximative nature of floating point numbers may also produce
-numerical differences between the text in this manual and the actual
-results of clp(R), for a given edition of the software.
-
-@node Solver Predicates, Unification, Notational Conventions, CLPQR
-@section Solver Predicates
-
-The solver interface for both Q and R consists of the following
-predicates which are exported from module(linear).
-
-@table @code
-@item @{+@var{Constraint}@}
-
-@var{Constraint} is a term accepted by the the grammar below. The
-corresponding constraint is added to the current constraint store and
-checked for satisfiability. If you want to overload @{@}/1 with other
-solvers, you can avoid its importation via: @code{use_module(clpq, [])}.
-
-@example
-@var{Constraint} --> @var{C}
-            | @var{C} , @var{C}                 conjunction
-
-@var{C} -->          @var{Expr} =:= @var{Expr}         equation
-            | @var{Expr} = @var{Expr}           equation
-            | @var{Expr} < @var{Expr}           strict inequation
-            | @var{Expr} > @var{Expr}           strict inequation
-            | @var{Expr} =< @var{Expr}          nonstrict inequation
-            | @var{Expr} >= @var{Expr}          nonstrict inequation
-            | @var{Expr} =\= @var{Expr}         disequation
-
-@var{Expr} -->       variable             Prolog variable
-            | number                floating point or integer
-            | + @var{Expr}                unary plus
-            | - @var{Expr}                unary minus
-            | @var{Expr} + @var{Expr}           addition
-            | @var{Expr} - @var{Expr}           subtraction
-            | @var{Expr} * @var{Expr}           multiplication
-            | @var{Expr} / @var{Expr}           division
-            | abs(@var{Expr})             absolute value
-            | sin(@var{Expr})             trigonometric sine
-            | cos(@var{Expr})             trigonometric cosine
-            | tan(@var{Expr})             trigonometric tangent
-            | pow(@var{Expr},@var{Expr})        raise to the power
-            | exp(@var{Expr},@var{Expr})        raise to the power
-            | min(@var{Expr},@var{Expr})        minimum of the two
-                                                arguments
-            | max(@var{Expr},@var{Expr})        maximum of the two
-                                                arguments
-            | #(Const)              symbolic numerical
-                                                constant
-@end example
-
-Conjunctive constraints @t{@{-C,C@}} have been made part of the syntax
-in order to enable grouped submission of constraints, which could be
-exploited by future versions of this software. Symbolic numerical
-constants are provided for compatibility only, see @pxref{Monash Examples}.
-
-@item entailed(+@var{Constraint})
-
-Succeeds iff the linear @var{Constraint} is entailed by the current
-constraint store. This predicate does not change the state of the
-constraint store.
-
-@example
-clp(q) ?- @{A =< 4@}, entailed(A=\=5).
-
-@{A=<4@}
-yes
-
-clp(q) ?- @{A =< 4@}, entailed(A=\=3).
-no
-@end example
-
-@item inf(+@var{Expr}, -@var{Inf} )
-Computes the infimum of the linear expression @var{Expr} and unifies it
-with @var{Inf}. Failure indicates unboundedness.
-
-@item sup(+@var{Expr}, -@var{Sup})
-
-Computes the supremum of the linear expression @var{Expr} and unifies it
-with @var{Sup}. Failure indicates unboundedness.
-
-@example
-clp(q) ?- @{ 2*X+Y =< 16, X+2*Y =< 11,
-             X+3*Y =< 15, Z = 30*X+50*Y
-          @}, sup(Z, Sup).
-
-Sup = 310,
-@{Z=30*X+50*Y@},
-@{X+1/2*Y=<8@}
-
-@{X+3*Y=<15@},
-@{X+2*Y=<11@}
-@end example
-
-@item minimize(+@var{Expr})
-
-Computes the infimum of the linear expression @var{Expr} and equates it
-with the expression, i.e. as if defined as:
-
-@example
-minimize(Expr) :- inf(Expr, Expr).
-@end example
-
-@item maximize(+@var{Expr})
-
-Computes the supremum of the linear expression @var{Expr} and equates it
-with the expression.
-
-@example
-clp(q) ?- @{ 2*X+Y =< 16, X+2*Y =< 11,
-             X+3*Y =< 15, Z = 30*X+50*Y
-          @}, maximize(Z).
-
-X = 7,
-Y = 2,
-Z = 310
-@end example
-
-@item bb_inf(+@var{Ints}, +@var{Expr}, -@var{Inf})
-
-Computes the infimum of the linear expression @var{Expr} under the
-additional constraint that all of variables in the list @var{Ints}
-assume integral values at the infimum. This allows for the solution of
-mixed integer linear optimization problems, see @pxref{A Mixed Integer
-Linear Optimization Example}.
-
-@item ordering(+@var{Spec})
-
-Provides a means to control one aspect of the presentation of the answer
-constraints, see @pxref{Variable Ordering}.
-@end table
-
-@node Unification, Feedback and Bindings, Solver Predicates, CLPQR
-@section Unification
-
-Equality constraints are added to the store implicitly each time
-variables that have been mentioned in explicit constraints are bound -
-either to another such variable or to a number.
-
-@example
-clp(r) ?- @{2*A+3*B=C/2@}, C=10.0, A=B.
-
-A = 1.0,
-B = 1.0,
-C = 10.0
-@end example
-
-Is equivalent modulo rounding errors to
-
-@example
-clp(r) ?- @{2*A+3*B=C/2, C=10, A=B@}.
-
-A = 1.0,
-B = 0.9999999999999999,
-C = 10.0
-@end example
-
-The shortcut bypassing the use of @{@}q/1 is allowed and makes sense
-because the interpretation of this equality in Prolog and clp(R)
-coincides. In general, equations involving interpreted functors,
-@code{+/2} in this case, must be fed to the solver explicitly:
-
-@example
-clp(r) ?- X=3.0+1.0, X=4.0.
-
-no
-@end example
-
-Further, variables known by clp(R) may be bound directly to floats
-only. Likewise, variables known by clp(Q) may be bound directly to
-rational numbers only, see @pxref{Numerical Precision and
-Rationals}. Failing to do so is rewarded with an exception:
-
-@example
-clp(q) ?- @{2*A+3*B=C/2@}, C=10.0, A=B.
-
-[ERROR: not.normalized(10.0)]
-@end example
-
-This is because 10.0 is not a rational constant. To make clp(Q) happy
-you have to say:
-
-@example
-clp(q) ?- @{2*A+3*B=C/2@}, C=rat(10,1), A=B.
-
-A = 1,
-B = 1,
-C = 10
-@end example
-
-If you use @code{@{@}/1}, you don't have to worry about such
-details. Alternatively, you may use the automatic expansion facility,
-check @pxref{Syntactic Sugar}.
-
-@node Feedback and Bindings, Linearity and Nonlinear Residues,Unification, CLPQR
-@section Feedback and Bindings
-
-What was covered so far was how the user populates the constraint
-store. The other direction of the information flow consists of the
-success and failure of the above predicates and the binding of variables
-to numerical values and the aliasing of variables. Example:
-
-@example
-clp(r) ?- @{A-B+C=10, C=5+5@}.
-
-B = A,
-C = 10.0
-@end example
-
-The linear constraints imply @code{A=B} and the solver consequently
-exports this binding to the Prolog world, which is manifest in the fact
-that the test @code{A==B} will succeed. More about answer presentation
-in @pxref{Projection and Redundancy Elimination}.
-
-@node Linearity and Nonlinear Residues, How Nonlinear Residues are made to disappear,Feedback and Bindings, CLPQR
-@section Linearity and Nonlinear Residues
-
-The clp(Q,R) system is restricted to deal with linear constraints
-because the decision algorithms for general nonlinear constraints are
-prohibitively expensive to run. If you need this functionality badly,
-you should look into symbolic algebra packages. Although the clp(Q,R)
-system cannot solve nonlinear constraints, it will collect them
-faithfully in the hope that through the addition of further (linear)
-constraints they might get simple enough to solve eventually. If an
-answer contains constraints, you have to be aware of the fact that
-success is qualified modulo the existence of a solution to the system of
-residual (nonlinear) constraints:
-
-@example
-clp(r) ?- @{sin(X) = cos(X)@}.
-
-nonlin:@{sin(X)-cos(X)=0.0@}
-@end example
-
-There are indeed infinitely many solutions to this constraint (@code{X =
-0.785398 + n*Pi}), but clp(Q,R) has no direct means to find and
-represent them.
-
-The systems goes through some lengths to recognize linear expressions as
-such. The method is based on a normal form for multivariate
-polynomials. In addition, some simple isolation axioms, that can be used
-in equality constraints, have been added. The current major limitation
-of the method is that full polynomial division has not been implemented.
-
-This is an example where the isolation axioms are sufficient to
-determine the value of X.
-
-@example
-clp(r) ?- @{sin(cos(X)) = 1/2@}.
-
-X = 1.0197267436954502
-@end example
-
-If we change the equation into an inequation, clp(Q,R) gives up:
-
-@example
-clp(r) ?- @{sin(cos(X)) < 1/2@}.
-
-nonlin:@{sin(cos(X))-0.5!0.0@}
-@end example
-
-The following is easy again:
-
-@example
-clp(r) ?- @{sin(X+2+2)/sin(4+X) = Y@}.
-
-Y = 1.0
-@end example
-
-And so is this:
-
-@example
-clp(r) ?- @{(X+Y)*(Y+X)/X = Y*Y/X+99@}.
-
-@{Y=49.5-0.5*X@}
-@end example
-
-An ancient symbol manipulation benchmark consists in rising the
-expression @code{X+Y+Z+1} to the 15th power:
-
-@example
-clp(q) ?- @{exp(X+Y+Z+1,15)=0@}.
-
-nonlin:@{Z^15+Z^14*15+Z^13*105+Z^12*455+Z^11*1365+Z^10*3003+...
-         ... polynomial continues for a few pages ...
-         =0@}
-@end example
-
-Computing its roots is another story. 
-
-@node How Nonlinear Residues are made to disappear, Isolation Axioms,Linearity and Nonlinear Residues, CLPQR
-@section How Nonlinear Residues are made to disappear
-
-Binding variables that appear in nonlinear residues will reduce the
-complexity of the nonlinear expressions and eventually results in linear
-expressions:
-
-@example
-clp(q) ?- @{exp(X+Y+1,2) = 3*X*X+Y*Y@}.
-
-nonlin:@{Y*2-X^2*2+Y*X*2+X*2+1=0@}
-@end example
-
-Equating X and Y collapses the expression completely and even determines
-the values of the two variables:
-
-@example
-clp(q) ?- @{exp(X+Y+1,2) = 3*X*X+Y*Y@}, X=Y.
-
-X = -1/4,
-Y = -1/4
-@end example
-
-@node Isolation Axioms, Numerical Precision and Rationals,How Nonlinear Residues are made to disappear, CLPQR
-@section Isolation Axioms
-
-These axioms are used to rewrite equations such that the variable to be
-solved for is moved to the left hand side and the result of the
-evaluation of the right hand side can be assigned to the variable. This
-allows, for example, to use the exponentiation operator for the
-computation of roots and logarithms, see below.
-
-@table @code
-@item @var{A} = @var{B} * @var{C}
- Residuates unless @var{B} or @var{C} is ground or @var{A} and @var{B}
-or @var{C} are ground.
-
-@item @var{A} = @var{B} / @var{C}
-Residuates unless @var{C} is ground or @var{A} and @var{B} are ground. 
-
-@item @var{X} = min(@var{Y},@var{Z})
-Residuates unless @var{Y} and @var{Z} are ground.
-
-@item @var{X} = max(@var{Y},@var{Z})
-Residuates unless @var{Y} and @var{Z} are ground.
-
-@item @var{X} = abs(@var{Y})
-Residuates unless @var{Y} is ground.
-
-@item @var{X} = pow(@var{Y},@var{Z}), @var{X} = exp(@var{Y},@var{Z})
-Residuates unless any pair of two of the three variables is ground. Example:
-
-@example
-clp(r) ?- @{ 12=pow(2,X) @}.
-
-X = 3.5849625007211565
-
-clp(r) ?- @{ 12=pow(X,3.585) @}.
-
-X = 1.9999854993443926
-
-clp(r) ?- @{ X=pow(2,3.585) @}.
-
-X = 12.000311914286545
-@end example
-
-@item  @var{X} = sin(@var{Y})
-Residuates unless @var{X} or @var{Y} is ground. Example:
-
-@example
-clp(r) ?- @{ 1/2 = sin(X) @}.
-
-X = 0.5235987755982989
-@end example
-
-@item @var{X} = cos(@var{Y})
-Residuates unless @var{X} or @var{Y} is ground.
-
-@item @var{X} = tan(@var{Y})
-Residuates unless @var{X} or @var{Y} is ground.
-@end table
-
-@node Numerical Precision and Rationals, Projection and Redundancy Elimination,Isolation Axioms, CLPQR
-@section Numerical Precision and Rationals
-
-The fact that you can switch between clp(R) and clp(Q) should solve most
-of your numerical problems regarding precision. Within clp(Q), floating
-point constants will be coerced into rational numbers
-automatically. Transcendental functions will be approximated with
-rationals. The precision of the approximation is limited by the floating
-point precision. These two provisions allow you to switch between clp(R)
-and clp(Q) without having to change your programs.
-
-What is to be kept in mind however is the fact that it may take quite
-big rationals to accommodate the required precision. High levels of
-precision are for example required if your linear program is
-ill-conditioned, i.e., in a full rank system the determinant of the
-coefficient matrix is close to zero. Another situation that may call for
-elevated levels of precision is when a linear optimization problem
-requires exceedingly many pivot steps before the optimum is reached.
-
-If your application approximates irrational numbers, you may be out of
-space particularly soon. The following program implements N steps of
-Newton's approximation for the square root function at point 2.
-
-@example
-%
-% from file: library('clpqr/examples/root')
-%
-
-root(N, R) :-
-  root(N, 1, R).
-
-root(0, S, R) :- !, S=R.
-root(N, S, R) :-
-  N1 is N-1,
-  @{ S1 = S/2 + 1/S @},
-  root(N1, S1, R).
-@end example
-
-It is known that this approximation converges quadratically, which means
-that the number of correct digits in the decimal expansion roughly
-doubles with each iteration. Therefore the numerator and denominator of
-the rational approximation have to grow likewise:
-
-@example
-clp(q) ?- use_module(library('clpqr/examples/root')).
-clp(q) ?- root(3,R),print_decimal(R,70).
-1.4142156862 7450980392 1568627450 9803921568 6274509803 9215686274
-5098039215
-
-R = 577/408
-
-clp(q) ?- root(4,R),print_decimal(R,70).
-1.4142135623 7468991062 6295578890 1349101165 5962211574 4044584905
-0192000543
-
-R = 665857/470832
-
-clp(q) ?- root(5,R),print_decimal(R,70).
-
-1.4142135623 7309504880 1689623502 5302436149 8192577619 7428498289
-4986231958
-
-R = 886731088897/627013566048
-
-clp(q) ?- root(6,R),print_decimal(R,70).
-
-1.4142135623 7309504880 1688724209 6980785696 7187537723 4001561013
-1331132652
-
-R = 1572584048032918633353217/1111984844349868137938112
-
-clp(q) ?- root(7,R),print_decimal(R,70).
-
-1.4142135623 7309504880 1688724209 6980785696 7187537694 8073176679
-7379907324
-
-R = 4946041176255201878775086487573351061418968498177 /
-    3497379255757941172020851852070562919437964212608
-@end example
-
-Iterating for 8 steps produces no further change in the first 70 decimal
-digits of @code{sqrt(2)}. After 15 steps the approximating rational
-number has a numerator and a denominator with 12543 digits each, and the
-next step runs out of memory.
-
-Another irrational number that is easily computed is @code{e}. The
-following program implements an alternating series for @code{1/e}, where
-the absolute value of last term is an upper bound on the error.
-
-@example
-%
-% from file: library('clpqr/examples/root')
-%
-
-e(N, E) :-
-  @{ Err =:= exp(10,-(N+2)), Half =:= 1/2 @},
-  inv_e_series(Half, Half, 3, Err, Inv.E),
-  @{ E =:= 1/Inv_E @}.
-
-inv_e_series(Term, S0, ., Err, Sum) :-
-  @{ abs(Term) =< Err @}, !,
-  S0 = Sum.
-
-inv_e_series(Term, S0, N, Err, Sum) :-
-  N1 is N+1,
-  @{ Term1 =:= -Term/N, S1 =:= Term1+S0 @},
-  inv_e_series(Term1, S1, N1, Err, Sum).
-@end example
-
-The computation of the rational number @var{E} that approximates
-@code{e} up to at least 1000 digits in its decimal expansion requires
-the evaluation of 450 terms of the series, i.e. 450 calls of
-inv.e. series/5.
-
-@example
-clp(q) ?- e(1000,E).
-
-E = 7149056228932760213666809592072842334290744221392610955845565494
-    3708750229467761730471738895197792271346693089326102132000338192
-    0131874187833985420922688804220167840319199699494193852403223700
-    5853832741544191628747052136402176941963825543565900589161585723
-    4023097417605004829991929283045372355639145644588174733401360176
-    9953973706537274133283614740902771561159913069917833820285608440
-    3104966899999651928637634656418969027076699082888742481392304807
-    9484725489080844360397606199771786024695620205344042765860581379
-    3538290451208322129898069978107971226873160872046731879753034549
-    3130492167474809196348846916421782850086985668680640425192038155
-    4902863298351349469211627292865440876581064873866786120098602898
-    8799130098877372097360065934827751120659213470528793143805903554
-    7928682131082164366007016698761961066948371407368962539467994627
-    1374858249110795976398595034606994740186040425117101588480000000
-    0000000000000000000000000000000000000000000000000000000000000000
-    00000000000000000000000000000000000000
-    /
-    2629990810403002651095959155503002285441272170673105334466808931
-    6863103901346024240326549035084528682487048064823380723787110941
-    6809235187356318780972302796570251102928552003708556939314795678
-    1978390674393498540663747334079841518303636625888963910391440709
-    0887345797303470959207883316838346973393937778363411195624313553
-    8835644822353659840936818391050630360633734935381528275392050975
-    7271468992840907541350345459011192466892177866882264242860412188
-    0652112744642450404625763019639086944558899249788084559753723892
-    1643188991444945360726899532023542969572584363761073528841147012
-    2634218045463494055807073778490814692996517359952229262198396182
-    1838930043528583109973872348193806830382584040536394640895148751
-    0766256738740729894909630785260101721285704616818889741995949666
-    6303289703199393801976334974240815397920213059799071915067856758
-    6716458821062645562512745336709063396510021681900076680696945309
-    3660590933279867736747926648678738515702777431353845466199680991
-    73361873421152165477774911660108200059
-@end example
-
-The decimal expansion itself looks like this:
-
-@example
-clp(q) ?- e(1000, E), print_decimal(E, 1000).
-2.
-7182818284 5904523536 0287471352 6624977572 4709369995 9574966967
-6277240766 3035354759 4571382178 5251664274 2746639193 2003059921
-8174135966 2904357290 0334295260 5956307381 3232862794 3490763233
-8298807531 9525101901 1573834187 9307021540 8914993488 4167509244
-7614606680 8226480016 8477411853 7423454424 3710753907 7744992069
-5517027618 3860626133 1384583000 7520449338 2656029760 6737113200
-7093287091 2744374704 7230696977 2093101416 9283681902 5515108657
-4637721112 5238978442 5056953696 7707854499 6996794686 4454905987
-9316368892 3009879312 7736178215 4249992295 7635148220 8269895193
-6680331825 2886939849 6465105820 9392398294 8879332036 2509443117
-3012381970 6841614039 7019837679 3206832823 7646480429 5311802328
-7825098194 5581530175 6717361332 0698112509 9618188159 3041690351
-5988885193 4580727386 6738589422 8792284998 9208680582 5749279610
-4841984443 6346324496 8487560233 6248270419 7862320900 2160990235
-3043699418 4914631409 3431738143 6405462531 5209618369 0888707016
-7683964243 7814059271 4563549061 3031072085 1038375051 0115747704
-1718986106 8739696552 1267154688 9570350354
-@end example
-
-@node Projection and Redundancy Elimination, Variable Ordering,Numerical Precision and Rationals, CLPQR
-@section Projection and Redundancy Elimination
-
-Once a derivation succeeds, the Prolog system presents the bindings for
-the variables in the query. In a CLP system, the set of answer
-constraints is presented in analogy. A complication in the CLP context
-are variables and associated constraints that were not mentioned in the
-query. A motivating example is the familiar mortgage relation:
-
-@example
-%
-% from file: library('clpqr/examples/mg')
-%
-
-mg(P,T,I,B,MP):-
-  @{ 
-    T = 1,
-    B + MP = P * (1 + I)
-  @}.
-mg(P,T,I,B,MP):-
-  @{
-    T > 1,
-    P1 = P * (1 + I) - MP,
-    T1 = T - 1
-  @}, mg(P1, T1, I, B, MP).
-@end example
-
-A sample query yields:
-
-@example
-clp(r) ?- use_module(library('clpqr/examples/mg')).
-
-clp(r) ?- mg(P,12,0.01,B,Mp).
-
-@{B=1.1268250301319698*P-12.682503013196973*Mp@}
-@end example
-
-Without projection of the answer constraints onto the query variables we
-would observe the following interaction:
-
-@example
-clp(r) ?- mg(P,12,0.01,B,Mp).
-
-@{B=12.682503013196973*_A-11.682503013196971*P@},
-@{Mp= -(_A)+1.01*P@},
-@{_B=2.01*_A-1.01*P@}
-@{_C=3.0301*_A-2.0301*P@},
-@{_D=4.060401000000001*_A-3.0604009999999997*P@},
-@{_E=5.101005010000001*_A-4.10100501*P@},
-@{_F=6.152015060100001*_A-5.152015060099999*P@},
-@{_G=7.213535210701001*_A-6.213535210700999*P@},
-@{_H=8.285670562808011*_A-7.285670562808009*P@},
-@{_I=9.368527268436091*_A-8.36852726843609*P@},
-@{_J=10.462212541120453*_A-9.46221254112045*P@},
-@{_K=11.566834666531657*_A-10.566834666531655*P@}
-@end example
-
-The variables @var{_A ... _K} are not part of the query, they originate
-from the mortgage program proper. Although the latter answer is
-equivalent to the former in terms of linear algebra, most users would
-prefer the former.
-
-@node Variable Ordering, Turning Answers into Terms,Projection and Redundancy Elimination, CLPQR
-@section Variable Ordering
-
-In general, there are many ways to express the same linear relationship
-between variables. clp(Q,R) does not care to distinguish between them,
-but the user might. The predicate ordering(+@var{Spec}) gives you some
-control over the variable ordering. Suppose that instead of @var{B}, you
-want @var{Mp} to be the defined variable:
-
-@example
-clp(r) ?- mg(P,12,0.01,B,Mp).
-
-@{B=1.1268250301319698*P-12.682503013196973*Mp@}
-@end example
-
-This is achieved with:
-
-@example
-clp(r) ?- mg(P,12,0.01,B,Mp), ordering([Mp]).
-
-@{Mp= -0.0788487886783417*B+0.08884878867834171*P@}
-@end example
-
-One could go one step further and require @var{P} to appear before (to
-the left of) @var{B} in a addition:
-
-@example
-clp(r) ?- mg(P,12,0.01,B,Mp), ordering([Mp,P]).
-
-@{Mp=0.08884878867834171*P-0.0788487886783417*B@}
-@end example
-
-@var{Spec} in ordering(+@var{Spec}) is either a list of variables with
-the intended ordering, or of the form @code{@var{A}<@var{B}}. The latter
-form means that @var{A} goes to the left of @var{B}. In fact,
-@code{ordering([@var{A},@var{B},@var{C},@var{D}])} is shorthand for:
-
-@example
-ordering(A < B), ordering(A < C), ordering(A < D),
-ordering(B < C), ordering(B < D),
-ordering(C < D)
-@end example
-
-The ordering specification only affects the final presentation of the
-constraints. For all other operations of clp(Q,R), the ordering is
-immaterial. Note that ordering/1 acts like a constraint: you can put it
-anywhere in the computation, and you can submit multiple specifications.
-
-@example
-clp(r) ?- ordering(B < Mp), mg(P,12,0.01,B,Mp).
-
-@{B= -12.682503013196973*Mp+1.1268250301319698*P@}
-
-yes
-clp(r) ?- ordering(B < Mp), mg(P,12,0.01,B,Mp), ordering(P < Mp).
-
-@{P=0.8874492252651537*B+11.255077473484631*Mp@}
-@end example
-
-@node Turning Answers into Terms, Projecting Inequalities,Variable Ordering, CLPQR
-@section Turning Answers into Terms
-
-In meta-programming applications one needs to get a grip on the results
-computed by the clp(Q,R) solver. The SISCtus Prolog predicate
-@code{call_residue/2} provides this functionality:
-
-@example
-clp(r) ?- call_residue(@{2*A+B+C=10,C-D=E,A<10@}, Constraints).
-
-Constraints = [
-               [A]-@{A<10.0@},
-               [B]-@{B=10.0-2.0*A-C@},
-               [D]-@{D=C-E@}
-              ]
-@end example
-
-@node Projecting Inequalities, Why Disequations,Turning Answers into Terms, CLPQR
-@section  Projecting Inequalities
-
-As soon as linear inequations are involved, projection gets more
-demanding complexity wise. The current clp(Q,R) version uses a
-Fourier-Motzkin algorithm for the projection of linear inequalities. The
-choice of a suitable algorithm is somewhat dependent on the number of
-variables to be eliminated, the total number of variables, and other
-factors. It is quite easy to produce problems of moderate size where the
-elimination step takes some time. For example, when the dimension of the
-projection is 1, you might be better off computing the supremum and the
-infimum of the remaining variable instead of eliminating n-1 variables
-via implicit projection.
-
-In order to make answers as concise as possible, redundant constraints
-are removed by the system as well. In the following set of inequalities,
-half of them are redundant.
-
-@example
-%
-% from file: library('clpqr/examples/elimination')
-%
-
-example(2, [X0,X1,X2,X3,X4]) :-
-  @{
-       +87*X0 +52*X1 +27*X2 -54*X3 +56*X4 =< -93,
-       +33*X0 -10*X1 +61*X2 -28*X3 -29*X4 =<  63,
-       -68*X0  +8*X1 +35*X2 +68*X3 +35*X4 =< -85,
-       +90*X0 +60*X1 -76*X2 -53*X3 +24*X4 =< -68,
-       -95*X0 -10*X1 +64*X2 +76*X3 -24*X4 =<  33,
-       +43*X0 -22*X1 +67*X2 -68*X3 -92*X4 =< -97,
-       +39*X0  +7*X1 +62*X2 +54*X3 -26*X4 =< -27,
-       +48*X0 -13*X1  +7*X2 -61*X3 -59*X4 =<  -2,
-       +49*X0 -23*X1 -31*X2 -76*X3 +27*X4 =<   3,
-       -50*X0 +58*X1  -1*X2 +57*X3 +20*X4 =<   6,
-       -13*X0 -63*X1 +81*X2  -3*X3 +70*X4 =<  64,
-       +20*X0 +67*X1 -23*X2 -41*X3 -66*X4 =<  52,
-       -81*X0 -44*X1 +19*X2 -22*X3 -73*X4 =< -17,
-       -43*X0  -9*X1 +14*X2 +27*X3 +40*X4 =<  39,
-       +16*X0 +83*X1 +89*X2 +25*X3 +55*X4 =<  36,
-       +2*X0  +40*X1 +65*X2 +59*X3 -32*X4 =<  13,
-       -65*X0 -11*X1 +10*X2 -13*X3 +91*X4 =<  49,
-       +93*X0 -73*X1 +91*X2  -1*X3 +23*X4 =< -87
-  @}.
-@end example
-
-Consequently, the answer consists of the system of nine non-redundant
-inequalities only:
-
-@example
-clp(q) ?- use_module(library('clpqr/examples/elimination')).
-clp(q) ?- example(2, [X0,X1,X2,X3,X4]).
-
-@{X0-2/17*X1-35/68*X2-X3-35/68*X4?=5/4@},
-@{X0-73/93*X1+91/93*X2-1/93*X3+23/93*X4=<-29/31@},
-@{X0-29/25*X1+1/50*X2-57/50*X3-2/5*X4>=-3/25@},
-@{X0+7/39*X1+62/39*X2+18/13*X3-2/3*X4=<-9/13@},
-@{X0+2/19*X1-64/95*X2-4/5*X3+24/95*X4>=-33/95@},
-@{X0+2/3*X1-38/45*X2-53/90*X3+4/15*X4=<-34/45@},
-@{X0-23/49*X1-31/49*X2-76/49*X3+27/49*X4=<3/49@},
-@{X0+44/81*X1-19/81*X2+22/81*X3+73/81*X4>=17/81@},
-@{X0+9/43*X1-14/43*X2-27/43*X3-40/43*X4>=-39/43@}
-@end example
-
-The projection (the shadow) of this polyhedral set into the
-@var{X0},@var{X1} space can be computed via the implicit elimination of
-non-query variables:
-
-@example
-clp(q) ?- example(2, [X0,X1--.]).
-
-@{X0+2619277/17854273*X1>=-851123/17854273@},
-@{X0+6429953/16575801*X1=<-12749681/16575801@},
-@{X0+19130/1213083*X1>=795400/404361@},
-@{X0-1251619/3956679*X1?=21101146/3956679@},
-@{X0+601502/4257189*X1>=220850/473021@}
-@end example
-
-Projection is quite a powerful concept that leads to surprisingly terse
-executable specifications of nontrivial problems like the computation of
-the convex hull from a set of points in an n-dimensional space: Given
-the program
-
-@example
-%
-% from file: library('clpqr/examples/elimination')
-%
-conv.hull(Points, Xs) :-
-  lin_comb(Points, Lambdas, Zero, Xs),
-  zero(Zero),
-  polytope(Lambdas).
-
-polytope(Xs) :-
-  positive_sum(Xs, 1).
-
-  positive_sum([], Z) :- @{Z=0@}.
-  positive_sum([X--Xs], SumX) :-
-    @{X >= 0, SumX = X+Sum @},
-    positive_sum(Xs, Sum).
-
-zero([]).
-zero([Z--Zs]) :- @{Z=0@}, zero(Zs).
-
-lin_comb([], [], S1, S1).
-lin_comb([Ps--Rest], [K--Ks], S1, S3) :-
-  lin_comb_r(Ps, K, S1, S2),
-  lin_comb(Rest, Ks, S2, S3).
-
-  lin_comb_r([], ., [], []).
-  lin_comb_r([P--Ps], K, [S--Ss], [Kps--Ss1]) :-
-    @{ Kps = K*P+S @},
-    lin_comb_r(Ps, K, Ss, Ss1).
-@end example
-
-we can post the following query:
-
-@example
-clp(q) ?- conv.hull([ [1,1], [2,0], [3,0], [1,2], [2,2] ], [X,Y]).
-
-@{Y=<2@},
-@{X+1/2*Y=<3@},
-@{X>=1@},
-@{Y>=0@},
-@{X+Y>=2@}
-@end example
-
-This answer is easily verified graphically:
-
-@example
- |
-2-   *   *
- |
- |
-1|   *
- |
- |
-0 ---|---*---*----
-     1   2   3
-@end example
-
-The convex hull program directly corresponds to the mathematical
-definition of the convex hull. What does the trick in operational terms
-is the implicit elimination of the Lambdas from the program
-formulation. Please note that this program does not limit the number of
-points or the dimension of the space they are from. Please note further
-that quantifier elimination is a computationally expensive operation and
-therefore this program is only useful as a benchmark for the projector
-and not so for the intended purpose.
-
-@node Why Disequations, Syntactic Sugar,Projecting Inequalities, CLPQR
-@section Why Disequations
-
-A beautiful example of disequations at work is due to [Colmerauer
-90]. It addresses the task of tiling a rectangle with squares of
-all-different, a priori unknown sizes. Here is a translation of the
-original Prolog-III program to clp(Q,R):
-
-@example 
-%
-% from file: library('clpqr/examples/squares')
-filled_rectangle( A, C) :-
-  @{ A >= 1 @},
-  distinct_squares( C),
-  filled_zone( [-1,A,1], _, C, []).
-
-distinct_squares( []).
-distinct_squares( [B|C]) :-
-  @{ B > 0 @},
-  outof( C, B),
-  distinct_squares( C).
-
-outof( [],     _).
-outof( [B1|C], B) :-
-  @{ B =\= B1 @},       % *** note disequation ***
-  outof( C, B).
-
-filled_zone( [V|L], [V|L], C0, C0) :-
-  @{ V >= 0 @}.
-filled_zone( [V|L], L3, [B|C], C2) :-
-  @{ V < 0 @},
-  placed_square( B, L, L1),
-  filled_zone( L1, L2, C, C1),
-  @{ Vb=V+B @},
-  filled_zone( [Vb,B|L2], L3, C1, C2).
-
-placed_square( B, [H,H0,H1|L], L1) :-
-  @{ B > H, H0=0, H2=H+H1 @},
-  placed_square( B, [H2|L], L1).
-placed_square( B, [B,V|L], [X|L]) :-
-  @{ X=V-B @}.
-placed_square( B, [H|L], [X,Y|L]) :-
-  @{ B < H, X= -B, Y=H-B @}.
-@end example
-
-There are no tilings with less than nine squares except the trivial one
-where the rectangle equals the only square. There are eight solutions
-for nine squares. Six further solutions are rotations of the first two.
-
-@example
-clp(q) ?- use_module(library('clpqr/examples/squares')).
-clp(q) ?- filled_rectangle(A, Squares).
-
-A = 1,f
-Squares = [1] ? ;
-
-A = 33/32,
-Squares = [15/32,9/16,1/4,7/32,1/8,7/16,1/32,5/16,9/32] ? ;
-
-A = 69/61,
-Squares = [33/61,36/61,28/61,5/61,2/61,9/61,25/61,7/61,16/61]
-@end example
-
-Depending on your hardware, the above query may take a few
-minutes. Supplying the knowledge about the minimal number of squares
-beforehand cuts the computation time by a factor of roughly four:
-
-@example
-clp(q) ?- length(Squares, 9), filled.rectangle(A, Squares).
-
-A = 33/32,
-Squares = [15/32,9/16,1/4,7/32,1/8,7/16,1/32,5/16,9/32] ? ;
-
-A = 69/61,
-Squares = [33/61,36/61,28/61,5/61,2/61,9/61,25/61,7/61,16/61]
-@end example
-
-@node Syntactic Sugar, Monash Examples,Why Disequations, CLPQR
-@section Syntactic Sugar
-
-There is a package that transforms programs and queries from a
-eval-quote variant of clp(Q,R) into corresponding programs and queries
-in a quote-eval variant. Before you use it, you need to know that in an
-eval-quote language, all symbols are interpreted unless explicitly
-quoted. This means that interpreted terms cannot be manipulated
-syntactically directly. Meta-programming in a CLP context by definition
-manipulates interpreted terms, therefore you need @code{quote/1} (just
-as in LISP) and some means to put syntactical terms back to their
-interpreted life: @code{@{@}/1}.
-
-In a quote-eval language, meta-programming is (pragmatically) simpler
-because everything is implicitly quoted until explicitly evaluated. On
-the other hand, now object programming suffers from the dual
-inconvenience.
-
-We chose to make our version of clp(Q,R) of the quote-eval type because
-this matches the intended use of the already existing boolean solver of
-SICStus. In order to keep the users of the eval-quote variant happy, we
-provide a source transformation package. It is activated via:
-
-@example
-| ?- use_module(library('clpqr/expand')). 
-@end example
-
-Loading the package puts you in a mode where the arithmetic functors
-like @code{+/2}, @code{*/2} and all numbers (functors of arity 0) are
-interpreted semantically.
-
-@example
-clp(r) ?- 2+2=X. X = 4.0
-@end example
-
-The package works by purifying programs and queries in the sense that
-all references to interpreted terms are made explicit. The above query
-is expanded prior to evaluation into:
-
-@example
-linear:@{2.0+2.0=X@}
-@end example
-
-The same mechanism applies when interpreted terms are nested deeper:
-
-@example
-some_predicate(10, f(A+B/2), 2*cos(A))
-@end example
-
-Expands into:
-
-@example
-linear:@{Xc=2.0*cos(A)@},
-linear:@{Xb=A+B/2@},
-linear:@{Xa=10.0@},
-some_predicate(Xa, f(Xb), Xc)
-@end example
-
-This process also applies when files are consulted or compiled. In fact,
-this is the only situation where expansion can be applied with relative
-safety. To see this, consider what happens when the toplevel evaluates
-the expansion, namely some calls to the clp(Q,R) solver, followed by the
-call of the purified query. As we learned in @pxref{Feedback and
-Bindings}, the solver may bind variables, which produces a goal with
-interpreted functors in it (numbers), which leads to another stage of
-expansion, and so on.
-
-We recommend that you only turn on expansion temporarily while
-consulting or compiling files needing expansion with @code{expand/0} and
-@code{noexpand/0}.
-
-@node Monash Examples,Compatibility Notes ,Syntactic Sugar, CLPQR
-@section Monash Examples
-
-This collection of examples has been distributed with the Monash
-University Version of clp(R) [Heintze et al. 87], and its inclusion into
-this distribution was kindly permitted by Roland Yap.
-
-In order to execute the examples, a small compatibility package has to
-be loaded first:
-
-@example
-clp(r) ?- use_module(library('clpqr/monash')).
-@end example
-
-Then, assuming you are using clp(R):
-
-@example
-clp(r) ?- expand, [library('clpqr/examples/monash/rkf45')],
-          noexpand.
-
-clp(r) ?- go.
-Point    0.00000 :    0.75000    0.00000 
-Point    0.50000 :    0.61969    0.47793 
-Point    1.00000 :    0.29417    0.81233 
-Point    1.50000 :   -0.10556    0.95809 
-Point    2.00000 :   -0.49076    0.93977 
-Point    2.50000 :   -0.81440    0.79929 
-Point    3.00000 :   -1.05440    0.57522
-
-Iteration finished
-------------------
- 439 derivative evaluations
-@end example
-
-@node Compatibility Notes, A Mixed Integer Linear Optimization Example,Monash Examples, CLPQR
-@section Compatibility Notes
-
-The Monash examples have been written for clp(R). Nevertheless, all but
-rkf45 complete nicely in clp(Q). With @code{rkf45}, clp(Q) runs out of
-memory. This is an instance of the problem discussed in @pxref{Numerical
-Precision and Rationals}.
-
-The Monash University clp(R) interpreter features a @code{dump/n}
-predicate. It is used to print the target variables according to the
-given ordering. Within this version of clp(Q,R), the corresponding
-functionality is provided via @code{ordering/1}. The difference is that
-@code{ordering/1} does only specify the ordering of the variables and no
-printing is performed. We think Prolog has enough predicates to perform
-output already. You can still run the examples referring to
-@code{dump/n} from the Prolog toplevel:
-
-@example
-clp(r) ?- expand, [library('clpqr/examples/monash/mortgage')], noexpand.
-
-% go2
-%
-clp(r) ?- mg(P,120,0.01,0,MP), dump([P,MP]).
-
-@{P=69.7005220313972*MP@}
-
-% go3
-% 
-clp(r) ?- mg(P,120,0.01,B,MP), dump([P,B,MP]).
-
-@{P=0.30299477968602706*B+69.7005220313972*MP@}
-
-% go4
-%
-clp(r) ?- mg(999, 3, Int, 0, 400), dump.
-
-nonlin:@{_B-_B*Int+.A+400.0=0.0@},
-nonlin:@{_A-_A*Int+400.0=0.0@},
-@{_B=599.0+999.0*Int@}
-@end example
-
-@node A Mixed Integer Linear Optimization Example, Implementation Architecture,Compatibility Notes, CLPQR
-@section A Mixed Integer Linear Optimization Example
-
-In this section we are going to exercise our solver a little by the
-computation of a small mixed integer optimization problem (MIP) from
-miplib, a collection of MIP models, housed at Rice University. Here are
-the original comments on the example:
-
-@example
-NAME:         flugpl
-ROWS:         18
-COLUMNS:      18
-INTEGER:      11
-NONZERO:      46
-BEST SOLN:    1201500 (opt)
-LP SOLN:      1167185.73
-SOURCE:       Harvey M. Wagner              
-              John W. Gregory (Cray Research)
-              E. Andrew Boyd (Rice University)
-APPLICATION:  airline model
-COMMENTS:     no integer variables are binary 
-@end example
-
-@example
-%
-% from file: library('clpqr/examples/mip')
-%
-example(flugpl, Obj, Vs, Ints, []) :-
-  Vs = [ Anm1,Anm2,Anm3,Anm4,Anm5,Anm6,
-         Stm1,Stm2,Stm3,Stm4,Stm5,Stm6,
-         UE1,UE2,UE3,UE4,UE5,UE6],
-  Ints = [Stm6, Stm5, Stm4, Stm3, Stm2,
-          Anm6, Anm5, Anm4, Anm3, Anm2, Anm1],
-
-  Obj =    2700*Stm1 + 1500*Anm1 + 30*UE1
-         + 2700*Stm2 + 1500*Anm2 + 30*UE2 
-         + 2700*Stm3 + 1500*Anm3 + 30*UE3
-         + 2700*Stm4 + 1500*Anm4 + 30*UE4 
-         + 2700*Stm5 + 1500*Anm5 + 30*UE5
-         + 2700*Stm6 + 1500*Anm6 + 30*UE6,
-
-  allpos(Vs),
-  @{  Stm1 = 60, 0.9*Stm1 +1*Anm1 -1*Stm2 = 0, 
-     0.9*Stm2 +1*Anm2 -1*Stm3 = 0, 0.9*Stm3 +1*Anm3 -1*Stm4 = 0, 
-     0.9*Stm4 +1*Anm4 -1*Stm5 = 0, 0.9*Stm5 +1*Anm5 -1*Stm6 = 0,
-     150*Stm1 -100*Anm1 +1*UE1 >= 8000,
-     150*Stm2 -100*Anm2 +1*UE2 >= 9000,
-     150*Stm3 -100*Anm3 +1*UE3 >= 8000,
-     150*Stm4 -100*Anm4 +1*UE4 >= 10000,
-     150*Stm5 -100*Anm5 +1*UE5 >= 9000,
-     150*Stm6 -100*Anm6 +1*UE6 >= 12000,
-     -20*Stm1 +1*UE1 =< 0, -20*Stm2 +1*UE2 =< 0, -20*Stm3 +1*UE3 =< 0, 
-     -20*Stm4 +1*UE4 =< 0, -20*Stm5 +1*UE5 =< 0, -20*Stm6 +1*UE6 =< 0,
-     Anm1 =< 18, 57 =< Stm2, Stm2 =< 75, Anm2 =< 18,
-     57 =< Stm3, Stm3 =< 75, Anm3 =< 18, 57 =< Stm4,
-     Stm4 =< 75, Anm4 =< 18, 57 =< Stm5, Stm5 =< 75,
-     Anm5 =< 18, 57 =< Stm6, Stm6 =< 75, Anm6 =< 18
-   @}.
-
-  allpos([]).
-  allpos([X|Xs]) :- @{X >= 0@}, allpos(Xs).
-@end example
-
-We can first check whether the relaxed problem has indeed the quoted
-infimum:
-
-@example
-clp(r) ?- example(flugpl, Obj, _, _, _), inf(Obj, Inf).
-
-Inf = 1167185.7255923203
-@end example
-
-Computing the infimum under the additional constraints that @var{Stm6},
-@var{Stm5}, @var{Stm4}, @var{Stm3}, @var{Stm2}, @var{Anm6}, @var{Anm5},
-@var{Anm4}, @var{Anm3}, @var{Anm2}, @var{Anm1} assume integer values at
-the infimum is computationally harder, but the query does not change
-much:
-
-@example
-clp(r) ?- example(flugpl, Obj, _, Ints, _), bb_inf(Ints, Obj, Inf).
-
-Inf = 1201500.0000000005
-@end example
-
-@node Implementation Architecture, Fragments and Bits,A Mixed Integer Linear Optimization Example, CLPQR
-@section Implementation Architecture
-
-The system consists roughly of the following components: 
-@itemize @bullet
-@item A polynomial normal form expression simplification mechanism.
-@item A solver for linear equations [Holzbaur 92].
-@item A simplex algorithm to decide linear inequalities [Holzbaur 94].
-@end itemize
-
-@node Fragments and Bits, CLPQR Bugs,Implementation Architecture, CLPQR
-@section Fragments and Bits
-
-The internal data structure for rational numbers is
-@code{rat(@var{Num},@var{Den})}. @var{Den} is always positive, i.e. the
-sign of the rational number is the sign of @var{Num}. Further, @var{Num}
-and @var{Den} are relative prime. Note that integer @var{N} looks like
-@code{rat(@var{N},1)} in this representation. You can control printing
-of terms with @code{portray/1}.
-
-Partial Evaluation
-
-Once one has a working solver, it is obvious and attractive to run the
-constraints in a clause definition at read time or compile time and
-proceed with the answer constraints in place of the original
-constraints. This gets you constant folding and in fact the full
-algebraic power of the solver applied to the avoidance of computations
-at runtime. The mechanism to realize this idea is to use
-@code{call_residue/2} for the expansion of @code{@{@}/1}.
-
-Asserting with Constraints
-
-If you use the dynamic data base, the clauses you assert might have
-constraints on the variables occurring in the clause. This should work
-as follows:
-
-@example
-clp(r) ?- @{A < 10@}, assert(p(A)).
-
-@{A < 10.0@}
-yes
-
-clp(r) ?- p(X).
-
-@{X<10.0@}
-@end example
-
-YAP currently does not implement this feature.
-
-@node CLPQR Bugs, CLPQR References, Fragments and Bits, CLPQR
-@section CLPQR bugs
-
-@itemize @bullet
-@item The fuzzy comparison of floats is the source for all sorts of
-weirdness. If a result in R surprises you, try to run the program in Q
-before you send me a bug report.
-
-@item The projector for floundered nonlinear relations keeps too many
-variables. Its output is rather unreadable.
-
-@item Disequations are not projected properly. 
-
-@item This list is probably incomplete.
-@end itemize
-
-Please send bug reports to @code{christian@@ai.univie.ac.at}.
-
-@node CLPQR References, ,CLPQR Bugs, CLPQR
-@section CLPQR References
-
-[Colmerauer 90] Colmerauer A.: An Introduction to Prolog III,
-Communications of the ACM, 33(7), 69-90, 1990.
-
-[Heintze et al. 87] Heintze N., Jaffar J., Michaylov S., Stuckey P., Yap
-R.: The CLP(R) Programmers Manual, Monash University, Clayton, Victoria,
-Australia, Department of Computer Science, 1987.
-
-[Holzbaur 92] Holzbaur C.: A High-Level Approach to the Realization of
-CLP Languages, in Proceedings of the JICSLP92 Post-Conference Workshop
-on Constraint Logic Programming Systems, Washington D.C., 1992.
-
-[Holzbaur 92] Holzbaur C.: Metastructures vs. Attributed Variables in
-the Context of Extensible Unification, in Bruynooghe M. & Wirsing
-M.(eds.), Programming Language Implementation and Logic Programming,
-Springer, LNCS 631, pp.260- 268, 1992.
-
-[Holzbaur 94] Holzbaur C.: A Specialized, Incremental Solved Form
-Algorithm for Systems of Linear Inequalities, Austrian Research
-Institute for Artificial Intelligence, Vienna, TR-94-07, 1994.
-
-[Jaffar & Michaylov 87] Jaffar J., Michaylov S.: Methodology and
-Implementation of a CLP System, in Lassez J.L.(ed.), Logic Programming -
-Proceedings of the 4th International Conference - Volume 1, MIT Press,
-Cambridge, MA, 1987.
-
-@node CHR, Logtalk, CLPQR, Top
-@chapter Constraint Handling Rules
+@node CHR, Logtalk, CLPR, Top
 
 @menu
-* CHR Copyright::               
 * CHR Introduction::            
-* CHR Introductory Examples::   
-* CHR Library::                 
+* CHR Syntax and Semantics::
+* CHR in YAP Programs::
 * CHR Debugging::               
-* CHR Programming Hints::       
-* CHR Constraint Handlers::     
-* CHR Backward Compatibility::  
+* CHR Examples::       
+* CHR Compatibility::     
+* CHR Guidelines::  
 @end menu
 
-@node CHR Copyright, CHR Introduction, CHR, CHR
-@unnumberedsec Copyright
-
-This chapter is Copyright @copyright{} 1996-98 LMU
-
-LMU (Ludwig-Maximilians-University)@*
-Munich, Germany
-
-Permission is granted to make and distribute verbatim copies of
-this chapter provided the copyright notice and this permission notice
-are preserved on all copies.
-
-Permission is granted to copy and distribute modified versions of this
-chapter under the conditions for verbatim copying, provided that the entire
-resulting derived work is distributed under the terms of a permission
-notice identical to this one.
-
-Permission is granted to copy and distribute translations of this chapter
-into another language, under the above conditions for modified versions,
-except that this permission notice may be stated in a translation approved
-by LMU.
-
-@node CHR Introduction, CHR Introductory Examples, CHR Copyright, CHR
-@comment  node-name,  next,  previous,  up
-@section Introduction
-
-Experience from real-life applications using constraint-based
-programming has shown that typically, one is confronted with a
-heterogeneous mix of different types of constraints. To be able to
-express constraints as they appear in the application and to write and
-combine constraint systems, a special purpose language for writing
-constraint systems called @dfn{constraint handling rules} (CHR) was
-developed.  CHR have been used to encode a wide range of constraint
-handlers (solvers), including new domains such as terminological and
-temporal reasoning.  Several CHR libraries exist in declarative
-languages such as Prolog and LISP, worldwide more than 20 projects use
-CHR. You can find more information about CHR at URL:
-@code{http://www.pst.informatik.uni-muenchen.de/personen/fruehwir/chr-intro.html}
-
-The high-level CHR are an excellent tool for rapid prototyping
-and implementation of constraint handlers. The usual abstract formalism
-to describe a constraint system, i.e.@: inference rules, rewrite rules,
-sequents, formulas expressing axioms and theorems, can be written as
-CHR in a straightforward way.  Starting from this executable
-specification, the rules can be refined and adapted to the specifics of
-the application.
-
-The CHR library includes a compiler, which translates
-CHR programs into Prolog programs on the fly, and a runtime system,
-which includes a stepper for debugging.  Many constraint
-handlers are provided in the example directory of the library.
-
-CHR are essentially a committed-choice language consisting of guarded
-rules that rewrite constraints into simpler ones until they are solved.
-CHR define both @dfn{simplification} of and @dfn{propagation} over
-constraints. Simplification replaces constraints by
-simpler constraints while preserving logical equivalence (e.g.@:  
-@code{X>Y,Y>X <=> fail}).  Propagation adds new constraints which are
-logically redundant but may cause further simplification (e.g.@: 
-@code{X>Y,Y>Z ==> X>Z}).  Repeatedly applying CHR incrementally simplifies
-and finally solves constraints (e.g.@: @code{A>B,B>C,C>A}
-leads to @code{fail}.
-
-With multiple heads and propagation rules, CHR provide two features
-which are essential for non-trivial constraint handling.  The
-declarative reading of CHR as formulas of first order logic allows
-one to reason about their correctness.  On the other hand, regarding
-CHR as a rewrite system on logical formulas allows one to reason
-about their termination and confluence.
-
-In case the implementation of CHR disagrees with your expectations
-based on this chapter, drop a line to the current maintainer:
-@code{christian@@ai.univie.ac.at} (Christian Holzbaur).
-
-@node CHR Introductory Examples, CHR Library, CHR Introduction, CHR
-@comment  node-name,  next,  previous,  up
-@section Introductory Examples
-
-We define a CHR constraint for less-than-or-equal, @code{leq}, that can
-handle variable arguments. This handler can be found in the library as
-the file @code{leq.pl}.  (The code works regardless of options switched
-on or off.)
-@example
-:- use_module(library(chr)).
-
-handler leq.
-constraints leq/2.
-:- op(500, xfx, leq).
-
-reflexivity  @@ X leq Y <=> X=Y | true.
-antisymmetry @@ X leq Y , Y leq X <=> X=Y.
-idempotence  @@ X leq Y \ X leq Y <=> true.
-transitivity @@ X leq Y , Y leq Z ==> X leq Z.
-@end example
-
-The CHR specify how @code{leq} simplifies and propagates as a
-constraint.  They implement reflexivity, idempotence, antisymmetry and
-transitivity in a straightforward way.  CHR @code{reflexivity} states
-that @code{X leq Y} simplifies to @code{true}, provided it is the case that
-@code{X=Y}. This test forms the (optional) guard of a rule, a
-precondition on the applicability of the rule.  Hence, whenever we see a
-constraint of the form @code{A leq A} we can simplify it to @code{true}.
-
-The rule @code{antisymmetry} means that if we find @code{X leq Y} as well as
-@code{Y leq X} in the constraint store, we can replace it by the
-logically equivalent @code{X=Y}. Note the different use of @code{X=Y} in
-the two rules: In the @code{reflexivity} rule the equality is a
-precondition (test) on the rule, while in the @code{antisymmetry} rule
-it is enforced when the rule fires. (The reflexivity rule could also have 
-been written as @code{reflexivity  @ X leq X <=> true}.)
-
-The rules @code{reflexivity} and @code{antisymmetry} are
-@dfn{simplification CHR}. In such rules, the constraints found are
-removed when the rule applies and fires.  The rule @code{idempotence} is
-a @dfn{simpagation CHR}, only the constraints right of @code{'\'} will
-be removed. The rule  says that if we find @code{X leq Y} and another @code{X
-leq Y} in the constraint store, we can remove one.
-
-Finally, the rule @code{transitivity} states that the conjunction
-@code{X leq Y, Y leq Z} implies @code{X leq Z}.  Operationally, we add
-@code{X leq Z} as (redundant) constraint, without removing the
-constraints @code{X leq Y, Y leq Z}. This kind of CHR is called
-@dfn{propagation CHR}.
-
-Propagation CHR are useful, as the query @code{A leq B,C leq A,B leq C}
-illustrates: The first two constraints cause CHR @code{transitivity} to
-fire and add @code{C leq B} to the query. This new constraint together
-with @code{B leq C} matches the head of CHR @code{antisymmetry}, @code{X
-leq Y, Y leq X}.  So the two constraints are replaced by
-@code{B=C}. Since @code{B=C} makes @code{B} and @code{C} equivalent, CHR
-@code{antisymmetry} applies to the constraints @code{A leq B, C leq A},
-resulting in @code{A=B}. The query contains no more CHR constraints, the
-simplification stops.  The constraint handler we built has solved
-@code{A leq B, C leq A, B leq C} and produced the answer @code{A=B,
-B=C}:
-
-@example
-A leq B,C leq A,B leq C. 
-% C leq A, A leq B propagates C leq B by transitivity.
-% C leq B, B leq C simplifies to B=C by antisymmetry.
-% A leq B, C leq A simplifies to A=B by antisymmetry since B=C.
-A=B,B=C.
-@end example
-
-Note that multiple heads of rules are essential in solving these
-constraints.  Also note that this handler implements a (partial) order
-constraint over any constraint domain, this generality is only possible
-with CHR.
-
-As another example, we can implement the sieve of Eratosthenes to
-compute primes simply as (for variations see the handler
-@file{primes.pl}):
-
-@example
-:- use_module(library(chr)).
-handler eratosthenes.
-constraints primes/1,prime/1.
-
-primes(1) <=> true.
-primes(N) <=> N>1 | M is N-1,prime(N),primes(M). % generate candidates
-
-absorb(J) @@ prime(I) \ prime(J) <=> J mod I =:= 0 | true. 
-@end example
-
-The constraint @code{primes(N)} generates candidates for prime numbers,
-@code{prime(M)}, where @code{M} is between @code{1} and @code{N}.
-The candidates react with each other such that each
-number absorbs multiples of itself. In the end, only prime numbers remain.
-
-Looking at the two rules defining @code{primes/1}, note that head
-matching is used in CHR, so the first rule will only apply to
-@code{primes(1)}. The test @code{N>1} is a guard (precondition) on the
-second rule.  A call with a free variable, like @code{primes(X)},
-will delay (suspend).  The third, multi-headed rule @code{absorb(J)} 
-reads as follows:
-If there is a constraint @code{prime(I)} and some other constraint
-@code{prime(J)} such that @code{J mod I =:= 0} holds, i.e.@: @code{J} is a
-multiple of @code{I}, then keep @code{prime(I)} but remove
-@code{prime(J)} and execute the body of the  rule,
-@code{true}.
-
-@node CHR Library, CHR Debugging, CHR Introductory Examples, CHR
-@section CHR Library
-
-CHR extend the Prolog syntax by a few constructs introduced in the next
-sections. Technically, the extension is achieved through the
-@code{user:term_expansion/2} mechanism. A file that contains a constraint
-handler may also contain arbitrary Prolog code.  Constraint handling
-rules can be scattered across a file. Declarations and options should
-precede rules. There can only be at most one constraint handler per module.
-
-@menu
-* CHR Loading the Library::     
-* CHR Declarations::            
-* CHR Syntax::                  
-* How CHR work::                
-* CHR Pragmas::                 
-* CHR Options::                 
-* CHR Built-In Predicates::     
-* CHR Consulting and Compiling::  
-* CHR Compiler-generated Predicates::  
-* CHR Operator Declarations::   
-* CHR Exceptions::              
-@end menu
-
-@node CHR Loading the Library, CHR Declarations, CHR Library, CHR Library
-@subsection Loading the Library
-
-Before you can load or compile any file containing a
-constraint handler (solver) written in CHR, the @code{chr} library
-module has to be imported:
-@example
-| ?- use_module(library(chr)).
-@end example
-It is recommended to include the corresponding directive at the 
-start of your files containing handlers:
-@example
-  :- use_module(library(chr)).
-@end example
-
-@node CHR Declarations, CHR Syntax, CHR Loading the Library, CHR Library
-@subsection Declarations
-
-Declarations in files containing CHR affect the compilation and thus
-the behavior of the rules at runtime.
-
-The mandatory handler declaration precedes any other CHR specific
-code.
-Example:
-@example
-handler minmax.
-@end example
-A handler name must be a valid Prolog @code{atom}.
-Per module, only one constraint handler can be defined.
-
-The constraints must be declared before they are used by rules.
-With this mandatory declaration one lists the constraints 
-the rules will later talk about. The declaration can be used more
-than once per handler.
-Example:
-@example
-constraints  leq/2, minimum/3, maximum/3.
-@end example
-
-
-The following
-optional declaration allows for conditional rule compilation.
-Only the rules mentioned get compiled. Rules are referred to by their 
-names (@pxref{CHR Syntax}). The latest occurrence takes precedence if used
-more than once per handler. Although it can be put anywhere in the handler
-file, it makes sense, as with other declarations, to use it early.
-Example:
-@example
-rules antisymmetry, transitivity.
-@end example
-
-To simplify the handling of operator declarations, in particular
-during @code{fcompile/1}, @code{operator/3} declarations with the
-same denotation as @code{op/3}, but 
-taking effect during compilation and loading, are helpful.
-Example:
-@example
-operator(700, xfx, ::).
-operator(600, xfx, :).
-@end example
-
-@node CHR Syntax, How CHR work, CHR Declarations, CHR Library
-@subsection Constraint Handling Rules, Syntax
-
-A constraint handling rule has one or more heads, an optional guard, a
-body and an optional name.  A @dfn{Head} is a @dfn{Constraint}. A
-constraint is a callable Prolog term,
-whose functor is a declared constraint.
-The @dfn{Guard} is a Prolog goal.  
-The @dfn{Body} of a rule is a Prolog
-goal (including constraints).  
-A rule can be named with
-a @dfn{Name} which can be any Prolog term (including variables
-from the rule). 
-
-There are three kinds of constraint handling rules:
-@example
-Rule           --> [Name @@] 
-                     (Simplification | Propagation | Simpagation) 
-                        [pragma Pragma].
-
-Simplification --> Heads         <=> [Guard '|'] Body
-Propagation    --> Heads         ==> [Guard '|'] Body
-Simpagation    --> Heads \ Heads <=> [Guard '|'] Body
-
-Heads          --> Head | Head, Heads
-Head           --> Constraint | Constraint # Id
-Constraint     --> a callable term declared as constraint
-Id             --> a unique variable
-
-Guard          --> Ask | Ask & Tell
-Ask            --> Goal
-Tell           --> Goal
-Goal           --> a callable term,
-                   including conjunction and disjunction etc.
-
-Body           --> Goal
-
-Pragma         --> a conjunction of terms usually referring to 
-                   one or more heads identified via #/2
-@end example
-
-The symbol @samp{|} separates the guard (if present) from the body of a
-rule.  Since @samp{|} is read as @samp{;} (disjunction) by the  
-reader, care has to be taken when using disjunction in the guard
-or body of the rule. The top level disjunction will always be
-interpreted as guard-body separator @samp{|}, so proper bracketing has
-to be used, e.g.@: @code{a <=> (b;c) | (d;e)} instead of @code{a <=> b;c |
-d;e} and @code{a <=> true | (d;e)} instead of @code{a <=> (d;e)}.
-
-In simpagation rules, @samp{\} separates the heads of the rule into two parts.
-
-Individual head constraints may be tagged with variables via
-@samp{#}, which may be used as identifiers in pragma declarations, for
-example. Constraint identifiers must be distinct variables, not
-occurring elsewhere in the heads.
-
-Guards test the applicability of a rule.  Guards come in two
-parts, tell and ask, separated by @samp{&}. 
-If the @samp{&} operator is not present, the whole guard is
-assumed to be of the ask type.
-
-Declaratively, a rule relates heads and body @dfn{provided the guard is
-true}.  A simplification rule means that the heads are true if and only
-if the body is true.  A propagation rule means that the body is true if
-the heads are true.  A simpagation rule combines a simplification and a
-propagation rule.  The rule @code{Heads1 \ Heads2 <=> Body} is
-equivalent to the simplification rule @code{Heads1, Heads2 <=> Heads1,
-Body}. However, the simpagation rule is more compact to write, more
-efficient to execute and has better termination behavior than the
-corresponding simplification rule, since the constraints comprising
-@code{Heads1} will not be removed and inserted again.
-
-@node How CHR work, CHR Pragmas, CHR Syntax, CHR Library
-@subsection How CHR work
-
-Each CHR constraint is associated with all rules in whose heads it
-occurs by the CHR compiler. Every time a CHR constraint is executed
-(called) or woken and reconsidered, it checks itself the applicability
-of its associated CHR by @dfn{trying} each CHR.  By default, the rules
-are tried in textual order, i.e.@: in the order they occur in the defining
-file.  To try a CHR, one of its heads is matched against the constraint.
-Matching succeeds if the constraint is an instance of the head.
-If a CHR has more than one head, the constraint store is searched for
-@dfn{partner} constraints that match the other heads.  Heads are tried
-from left to right, except that in simpagation rules, the heads to be
-removed are tried before the head constraints to be kept (this is done
-for efficiency reasons).  If the matching succeeds, the guard is
-executed. Otherwise the next rule is tried.
-
-The guard either succeeds or fails.  A guard succeeds if the execution
-of its Ask and Tell parts succeeds and in the ask part no variable that
-occurs also in the heads was touched or the cause of an instantiation
-error. The ask guard will fail otherwise.  A variable is @dfn{touched}
-if it is unified with a term (including other variables from other
-constraints) different from itself.  Tell guards, on the contrary, are
-trusted and not checked for that property.  If the guard succeeds, the
-rule applies.  Otherwise the next rule is tried.
-
-If the firing CHR is a simplification rule, the matched constraints are
-removed from the store and the body of the CHR is executed.  Similarly
-for a firing simpagation rule, except that the constraints that matched
-the heads preceding @samp{\} are kept.  If the firing CHR is a
-propagation rule the body of the CHR is executed without removing any
-constraints.  It is remembered that the propagation rule fired, so it
-will not fire again with the same constraints if the constraint is woken
-and reconsidered.  If the currently active constraint has not been
-removed, the next rule is tried.
-
-If the current constraint has not been removed and all rules have been
-tried, it delays until a variable occurring in the constraint is
-touched.  Delaying means that the constraint is inserted into the
-constraint store. When a constraint is woken, all its rules are tried
-again. (This process can be watched and inspected with the CHR debugger,
-see below.)
-
-
-@node CHR Pragmas, CHR Options, How CHR work, CHR Library
-@subsection Pragmas
-
-Pragmas are annotations to rules and constraints that enable the 
-compiler to generate more specific, more optimized code. A pragma
-can be a conjunction of the following terms:
-
-@table @code
-
-@item already_in_heads
-The intention of simplification and simpagation rules is often
-to combine the heads into a stronger version of one of them.
-Depending on the strength of the guard, the new constraint may
-be identical to one of the heads to removed by the rule.
-This removal followed by addition is inefficient and may even cause
-termination problems. If the pragma is used, this situation is
-detected and the corresponding problems are avoided.
-The pragma applies to all constraints removed by the rule.
-
-@item already_in_head(Id)
-Shares the intention of the previous pragma, but affects only 
-the constraint indicated via @var{Id}. Note that one can use more
-than one pragma per rule.
-
-@item passive(Id)
-No code will be generated for the specified constraint in the particular
-head position. This means that the constraint will not see the rule, it
-is passive in that rule. This changes the behavior of the CHR system,
-because normally, a rule can be entered starting from each head constraint.
-Usually this pragma will improve the efficiency of the
-constraint handler, but care has to be taken in order not to lose
-completeness.
-
-For example, in the handler @code{leq}, any pair of constraints, say
-@code{A leq B, B leq A}, that matches the head @code{X leq Y , Y leq X}
-of the @code{antisymmetry} rule, will also match it when the constraints
-are exchanged, @code{B leq A, A leq B}. Therefore it is enough if a
-currently active constraint enters this rule in the first head only,
-the second head can be declared to be passive. Similarly for the
-@code{idempotence} rule.  For this rule, it is more efficient to declare
-the first head passive, so that the currently active constraint will be
-removed when the rule fires (instead of removing the older constraint
-and redoing all the propagation with the currently active constraint).
-Note that the compiler itself detects the symmetry of the two head
-constraints in the simplification rule @code{antisymmetry}, thus it is
-automatically declared passive and the compiler outputs @code{CHR
-eliminated code for head 2 in antisymmetry}.
-@example
-antisymmetry @ X leq Y, Y leq X # Id <=> X=Y
-           pragma passive(Id).
-idempotence  @ X leq Y # Id \ X leq Y <=> true
-           pragma passive(Id).
-transitivity @ X leq Y # Id, Y leq Z ==> X leq Z
-           pragma passive(Id).
-@end example
-Declaring the first head of rule @code{transitivity} passive changes the
-behavior of the handler. It will propagate less depending on the order in
-which the constraints arrive:
-@example
-?- X leq Y, Y leq Z.
-X leq Y,
-Y leq Z,
-X leq Z ? 
-
-?- Y leq Z, X leq Y.
-Y leq Z,
-X leq Y ? 
-
-?- Y leq Z, X leq Y, Z leq X.
-Y = X,
-Z = X ?
-@end example
-The last query shows that the handler is still complete in the sense
-that all circular chains of leq-relations are collapsed into equalities.
-
-@end table
-
-@node CHR Options, CHR Built-In Predicates, CHR Pragmas, CHR Library
-@subsection Options
-
-Options parametrise the rule compilation process.
-Thus they should precede the rule definitions. Example:
-@example
-option(check_guard_bindings, off).
-@end example
-
-The format below lists the names of the recognized options together with
-the acceptable values. The first entry in the lists is the default
-value.
-
-@table @code
-
-@item option(debug_compile,         [off,on]).
-Instruments the generated code such that the execution
-of the rules may be traced (@pxref{CHR Debugging}).
-
-@item option(check_guard_bindings,  [on,off]).
-Per default, for guards of type ask the CHR runtime system makes sure
-that no variables are touched or the cause of an instantiation
-error. These checks may be turned off with this option, i.e.@: all guards
-are treated as if they were of the tell variety. The option was
-kept for backward compatibility. Tell and ask guards offer better
-granularity.
-
-@item option(already_in_store,      [off,on]).
-If this option is on, the CHR runtime system checks for the presence of
-an identical constraint upon the insertion into the store. If present,
-the attempted insertion has no effect. Since checking for duplicates for
-all constraints costs, duplicate removal specific to individual
-constraints, using a few simpagation rules of the following form instead,
-may be a better solution.
-@example
-Constraint \ Constraint <=> true.
-@end example
-
-@item option(already_in_heads,      [off,on]).
-The intention of simplification and simpagation rules is often
-to combine the heads into a stronger version of one of them.
-Depending on the strength of the guard, the new constraint may
-be identical to one of the heads removed by the rule.
-This removal followed by addition is inefficient and may even cause
-termination problems. If the option is enabled, this situation is
-detected and the corresponding problems are avoided.
-This option applies to all constraints and is provided mainly
-for backward compatibility. Better grained control can be achieved
-with corresponding pragmas. (@pxref{CHR Pragmas}).
-
-@end table
-
-The remaining options are meant for CHR implementors only:
-@table @code
-@item option(flatten,               [on,off]).
-@item option(rule_ordering,         [canonical,heuristic]).
-@item option(simpagation_scheme,    [single,multi]).
-@item option(revive_scheme,         [new,old]).
-@item option(dead_code_elimination, [on,off]).
-@end table
-
-@node CHR Built-In Predicates, CHR Consulting and Compiling, CHR Options, CHR Library
-@subsection Built-In Predicates
-
-This table lists the predicates made available by the CHR library.  They
-are meant for advanced users, who want to tailor the CHR system 
-towards their specific needs.
-@table @code
-@item current_handler(?Handler, ?Module)
-@findex current_handler/2
-Nondeterministically enumerates the defined handlers
-with the module they are defined in.
-
-@item current_constraint(?Handler, ?Constraint)
-@findex current_constraint/2
-Nondeterministically enumerates the defined constraints
-in the form @var{Functor/Arity} and the handlers they are
-defined in.
-
-@item insert_constraint(+Constraint, -Id)
-@findex insert_constraint/2
-Inserts @var{Constraint} into the constraint store
-without executing any rules. The constraint will be woken and reconsidered
-when one of the variables in @var{Constraint} is touched. @var{Id} is
-unified with an internal object representing the constraint.
-This predicate only gets defined when a handler and constraints are
-declared (@pxref{CHR Declarations}).
-
-@item insert_constraint(+Constraint, -Id, ?Term)
-@findex insert_constraint/3
-Inserts @var{Constraint} into the constraint store without executing
-any rules. The constraint will be woken and reconsidered when one of the
-variables in @var{Term} is touched. @var{Id} is
-unified with an internal object representing the constraint.
-This predicate only gets defined when a handler and constraints are
-declared (@pxref{CHR Declarations}).
-
-@item find_constraint(?Pattern, -Id)
-@findex find_constraint/2
-Nondeterministically enumerates constraints from the constraint
-store that match @var{Pattern}, i.e.@: which are instances of
-@var{Pattern}. @var{Id} is
-unified with an internal object representing the constraint.
-
-@item find_constraint(-Var, ?Pattern, -Id)
-@findex find_constraint/3
-Nondeterministically enumerates constraints from the constraint
-store that delay on @var{Var} and match @var{Pattern}, 
-i.e.@: which are instances of
-@var{Pattern}. The identifier @var{Id} can be used to
-refer to the constraint later, e.g.@: for removal.
-
-@item findall_constraints(?Pattern, ?List)
-@findex findall_constraints/2
-Unifies @var{List} with a list of @code{Constraint # Id} pairs
-from the constraint store that match @var{Pattern}.
-
-@item findall_constraints(-Var, ?Pattern, ?List)
-@findex findall_constraints/3
-Unifies @var{List} with a list of @code{Constraint # Id} pairs
-from the constraint store that delay on @var{Var} and
-match @var{Pattern}.
-
-@item remove_constraint(+Id)
-@findex remove_constraint/1
-Removes the constraint @var{Id}, obtained with one of the previous predicates,
-from the constraint store.
-
-@item unconstrained(?Var)
-@findex unconstrained/1
-Succeeds if no CHR constraint delays on @var{Var}. Defined as:
-@example
-unconstrained(X) :- 
-    find_constraint(X, _, _), !, fail.
-unconstrained(_).
-@end example
-
-@item notify_constrained(?Var)
-@findex notify_constrained/1
-Leads to the reconsideration of the constraints associated with @var{Var}.
-This mechanism allows solvers to communicate reductions on the set of
-possible values of variables prior to making bindings.
-@end table
-
-@node CHR Consulting and Compiling, CHR Compiler-generated Predicates, CHR Built-In Predicates, CHR Library
-@subsection Consulting and Compiling Constraint Handlers
-
-The CHR compilation process has been made as transparent as possible.
-The user deals with files containing CHR just as with files containing
-ordinary Prolog predicates. Thus CHR may be consulted, compiled with
-various compilation modes, and compiled to file.
-
-@node CHR Compiler-generated Predicates, CHR Operator Declarations, CHR Consulting and Compiling, CHR Library
-@subsection Compiler-generated Predicates
-
-Besides predicates for the defined constraints,
-the CHR compiler generates some support predicates in the
-module containing the handler. To avoid naming conflicts,
-the  following predicates must not be defined or referred to
-by user code in the same module:
-@table @code
-@item verify_attributes/3
-@item attribute_goal/2
-@item attach_increment/2
-@item 'attach_F/A'/2
-for every defined constraint F/A.
-@item 'F/A_N_M_...'/Arity
-for every defined constraint F/A. N,M is are integers, Arity > A.
-@end table
-
-For the prime number example that is:
-@example
-        attach_increment/2
-        attach_prime/1/2
-        attach_primes/1/2
-        attribute_goal/2
-        goal_expansion/3
-        prime/1
-        prime/1_1/2
-        prime/1_1_0/3
-        prime/1_2/2
-        primes/1
-        primes/1_1/2
-        verify_attributes/3
-@end example
-
-If an author of a handler wants to avoid naming conflicts with the
-code that uses the handler, it is easy to encapsulate the handler.
-The module declaration below puts the handler into module @code{primes},
-which exports only selected predicates - the constraints in our example.
-@example        
-        :- module(primes, [primes/1,prime/1]).
-
-        :- use_module(library(chr)).
-
-        handler eratosthenes.
-        constraints primes/1,prime/1.
-        ...
-@end example
-
-@node CHR Operator Declarations, CHR Exceptions, CHR Compiler-generated Predicates, CHR Library
-@subsection Operator Declarations
-
-This table lists the operators as used by the CHR library:
-@example
-@group
-:- op(1200, xfx, @@).
-:- op(1190, xfx, pragma).
-:- op(1180, xfx, [==>,<=>]).
-:- op(1180, fy,  chr_spy).
-:- op(1180, fy,  chr_nospy).
-:- op(1150, fx,  handler).
-:- op(1150, fx,  constraints).
-:- op(1150, fx,  rules).
-:- op(1100, xfx, '|').
-:- op(1100, xfx, \ ).
-:- op(1050, xfx, &).
-:- op( 500, yfx, #).
-@end group
-@end example
-
-@node CHR Exceptions,  , CHR Operator Declarations, CHR Library
-@subsection Exceptions
-
-The CHR runtime system reports instantiation and type errors for the predicates:
-@table @code
-@item find_constraint/2
-@item findall_constraints/3
-@item insert_constraint/2
-@item remove_constraint/1
-@item notify_constrained/1
-@end table
-
-The only other CHR specific runtime error is:
-@table @code
-@item @{CHR ERROR: registering <New>, module <Module> already hosts <Old>@}
-An attempt to load a second handler New into module <Module> already 
-hosting handler <Old> was made.
-@end table
-
-The following exceptional conditions are detected by the CHR
-compiler:
-
-@table @code
-@item @{CHR Compiler ERROR: syntax rule <N>: <Term>@}
-If the N-th <Term> in the file being loaded violates the CHR syntax (@pxref{CHR Syntax}).
-
-@item @{CHR Compiler ERROR: too many general heads in <Name>@}
-Unspecific heads in definitions like
-@code{C \ C <=> true}
-must not be combined with other heads in rule <Name>.
-
-@item @{CHR Compiler ERROR: bad pragma <Pragma> in <Name>@}
-The pragma <Pragma> used in rule <Name> does not qualify. Currently this only happens if
-<Pragma> is unbound.
-
-@item @{CHR Compiler ERROR: found head <F/A> in <Name>, expected one of: <F/A list>@}
-Rule <Name> has a head of given F/A which is not among the defined constraints.
-
-@item @{CHR Compiler ERROR: head identifiers in <Name> are not unique variables@}
-The identifiers to refer to individual constraints (heads) via @samp{#} in
-rule <Name> do not meet the indicated requirements.
-
-@item @{CHR Compiler ERROR: no handler defined@}
-CHR specific language elements, declarations or rules for example, are
-used before a handler was defined. This error is usually reported a couple
-of times, i.e.@: as often as there are CHR forms in the file expecting the missing
-definition.
-
-@item @{CHR Compiler ERROR: compilation failed@}
-Not your fault. Send us a bug report.
-@end table
-
-@node CHR Debugging, CHR Programming Hints, CHR Library, CHR
-@section Debugging CHR Programs
-
-Use @code{option(debug_compile,on)} preceding any rules
-in the file containing the handler to enable CHR debugging. 
-The CHR debugging mechanism works by instrumenting the code
-generated by the CHR compiler.
-Basically, the CHR debugger works like the Prolog debugger. 
-The main differences are: there are extra ports specific to CHR,
-and the CHR debugger provides no means for the user to change
-the flow of control, i.e.@: there are currently no @var{retry} and @var{fail}
-options available.
-
-@menu
-* CHR Control Flow Model::      
-* CHR Debugging Predicates::    
-* CHR Spy-points::              
-* CHR Debugging Messages::      
-* CHR Debugging Options::       
-@end menu
-
-@node CHR Control Flow Model, CHR Debugging Predicates, CHR Debugging, CHR Debugging
-@subsection Control Flow Model
-@cindex CHR control flow model
-
-The entities reflected by the CHR debugger are constraints
-and rules. Constraints are treated like ordinary Prolog goals
-with the usual ports: @code{[call,exit,redo,fail]}.
-In addition, constraints may get inserted into or removed from the 
-constraint store (ports: @code{insert,remove}), and stored
-constraints containing variables will be woken and reconsidered
-(port: @code{wake}) when variables are touched.
-
-The execution of a constraint consists of trying to apply the rules
-mentioning the constraint in their heads.  Two ports for rules reflect this
-process: At a @code{try} port the active constraint matches one of the
-heads of the rule, and matching constraints for the remaining heads of
-the rule, if any, have been found as well.  The transition from a
-@code{try} port to an @code{apply} port takes place when the guard has
-been successfully evaluated, i.e.@: when the rule commits. At the
-@code{apply} port, the body of the rule is just about to be executed. The
-body is a Prolog goal transparent to the CHR debugger. If the
-rule body contains CHR constraints, the CHR debugger will track
-them again.  If the rules were consulted, the Prolog debugger can be
-used to study the evaluations of the other predicates in the body.
-
-@node CHR Debugging Predicates, CHR Spy-points, CHR Control Flow Model, CHR Debugging
-@subsection CHR Debugging Predicates
-@cindex CHR debugging predicates
-
-The following predicates control the operation of the CHR debugger:
-
-@table @code
-@item chr_trace
-@findex chr_trace/0
-Switches the CHR debugger on and ensures that the
-next time control enters a CHR port, a message will be produced and
-you will be asked to interact. @refill
-
-@noindent
-At this point you have a number of options.  @xref{CHR Debugging Options}.  In
-particular, you can just type @key{cr} (Return) to @dfn{creep} (or single-step)
-into your program. You will
-notice that the CHR debugger stops at many ports.  If this is not
-what you want, the predicate @code{chr_leash} gives full control over
-the ports at which you are prompted. @refill
-
-@item chr_debug
-@findex chr_debug/0
-Switches the CHR debugger on and ensures that the next time
-control enters a CHR port with a spy-point set, a message will be produced
-and you will be asked to interact. @refill
-@refill
-
-@item chr_nodebug
-@findex chr_nodebug/0
-Switches the CHR debugger off.  If there are any spy-points set then they
-will be kept.  @refill
-
-@item chr_notrace
-@findex chr_notrace/0
-Equivalent to @code{chr_nodebug}.  @refill
-
-@item chr_debugging
-@findex chr_debugging/0
-Prints onto the standard error stream information about the current
-CHR debugging state.  This will show: @refill
-
-@enumerate
-@item
-Whether the CHR debugger is switched on.
-@item
-What spy-points have been set (see below).
-@item
-What mode of leashing is in force (see below).
-@end enumerate
-
-@item chr_leash(@var{+Mode})
-@findex chr_leash/1
-The leashing mode is set to @var{Mode}. It determines the CHR ports at
-which you are to be prompted when you @dfn{creep} through your program.
-At unleashed ports a tracing message is still output, but program
-execution does not stop to allow user interaction.  Note that the ports
-of spy-points are always leashed (and cannot be unleashed).  @var{Mode}
-is a list containing none, one or more of the following port names:
-@refill
-
-@table @code
-@item call
-Prompt when a constraint is executed for the first time.
-
-@item exit
-Prompt when the constraint is successfully processed, i.e.@: the applicable
-rules have applied.
-
-@item redo
-Prompt at subsequent exits generated by non-deterministic rule bodies.
-
-@item fail
-Prompt when a constraint fails.
-
-@item wake
-Prompt when a constraint from the constraint store is woken and
-reconsidered because one of its variables has been touched.
-
-@item try
-Prompt just before the guard evaluation of a rule, after constraints
-matching the heads have been found.
-
-@item  apply
-Prompt upon the application of a rule, after the successful guard evaluation,
-when the rule commits and fires, just before evaluating the body.
-
-@item insert
-Prompt when a constraint gets inserted into the constraint store,
-i.e.@: after all rules have been tried.
-
-@item remove
-Prompt when a constraint gets removed from the constraint store, e.g.
-when a simplification rule applies.
-
-@end table
-
-@noindent
-The initial value of the CHR leashing mode is
-@code{[call,exit,fail,wake,apply]}. Predefined shortcuts are:
-@table @code
-@item chr_leash(none), chr_leash(off)
-To turn leashing off.
-
-@item chr_leash(all)
-To prompt at every port.
-
-@item chr_leash(default)
-Same as @code{chr_leash([call,exit,fail,wake,apply])}.
-
-@item chr_leash(call)
-No need to use a list if only a singular port is to be leashed.
-@end table
-
-@end table
-
-@node CHR Spy-points, CHR Debugging Messages, CHR Debugging Predicates, CHR Debugging
-@subsection CHR Spy-points
-@cindex CHR spy-points
-
-For CHR programs of any size, it is clearly impractical to creep through the
-entire program.  @dfn{Spy-points} make it possible to stop the program
-upon an event of interest.  Once
-there, one can set further spy-points in order to catch the control flow
-a bit further on, or one can start creeping.
-
-Setting a spy-point on a constraint or a rule indicates that you wish to
-see all control flow through the various ports involved, except during
-skips.  When control passes through any port with a spy-point set on it,
-a message is output and the user is asked to interact.  Note that the
-current mode of leashing does not affect spy-points: user interaction is
-requested at @emph{every} port.
-
-Spy-points are set and removed by the following predicates,
-which are declared as prefix operators:
-
-@table @code
-@item chr_spy @var{Spec}
-@findex chr_spy/1
-Sets spy-points on constraints and rules given by @var{Spec}, which is
-is of the form:
-
-@table @asis
-@item @var{_} (variable)
-denoting all constraints and rules, or:
-
-@item @var{constraints Cs}
-where @var{Cs} is one of
-@table @asis
-
-@item @var{_} (variable)
-denoting all constraints
-
-@item @var{C},...,@var{C}
-denoting a list of constraints @var{C}
-
-@item @var{Name}
-denoting all constraints with this functor, regardless of arity
-
-@item @var{Name/Arity}
-denoting the constraint of that name and arity
-@end table
-
-@item @var{rules Rs}
-where @var{Rs} is one of:
-@table @asis
-
-@item @var{_} (variable)
-denoting all rules
-
-@item @var{R},...,@var{R}
-denoting a list of rules @var{R}
-
-@item @var{Name}
-where @var{Name} is the name of a rule in any handler.
-
-@item @var{already_in_store}
-The name of a rule implicitly defined by the system when
-the option @code{already_in_store} is in effect.
-
-@item @var{already_in_heads}
-The name of a rule implicitly defined by the system when
-the option @code{already_in_heads} or the corresponding 
-pragmas are in effect.
-
-@item @var{Handler:Name}
-where @var{Handler} is the name of a constraint handler
-and @var{Name} is the name of a rule in that handler
-
-@end table
-@end table
-
-@noindent
-Examples:
-
-@example
-| ?- chr_spy rules rule(3), transitivity, already_in_store.
-| ?- chr_spy constraints prime/1.
-@end example
-
-If you set spy-points, the CHR debugger will be switched on.
-
-@item chr_nospy @var{Spec}
-@findex chr_nospy/1
-Removes spy-points on constraints and rules given by @var{Spec}, where
-@var{Spec} is of the form as described for @code{chr_spy @var{Spec}}.
-There is no @code{chr_nospyall/0}.  To remove all CHR spy-points use
-@code{chr_nospy _}.
-@refill
-
-@end table
-
-@noindent
-The options available when you arrive at a spy-point are described later.
-@xref{CHR Debugging Options}.
-
-@node CHR Debugging Messages, CHR Debugging Options, CHR Spy-points, CHR Debugging
-@subsection CHR Debugging Messages
-@cindex CHR debugging messages
-
-All trace messages are output to the standard error
-stream.  This allows you to trace programs while they are performing
-file I/O.  The basic format is as follows:
-
-@example
-@var{S} 3 1 try eratosthenes:absorb(10) @@ prime(9)#<c4>, prime(10)#<c2> ?
-@end example
-
-@noindent
-@var{S} is a spy-point indicator. It is printed as @samp{@ } if there is 
-no spy-point, as @samp{r}, indicating that there is a spy-point on this
-rule, or as @samp{c} if one of the involved constraints has a spy-point.
-
-The first number indicates the current depth of the execution; i.e.@:
-the number of direct @dfn{ancestors} the currently active constraint
-has.
-@refill
-
-The second number indicates the head position of the currently active
-constraint at rule ports.
-
-The next item tells you which port is currently traced.
-
-A constraint or a matching rule are printed next.
-Constraints print as @code{Term#Id}, where @var{Id} is a unique
-identifier pointing into the constraint store.
-Rules are printed as @code{Handler:Name @@}, followed by the constraints
-matching the heads.
-
-The final @samp{?} is the prompt indicating that you should type in one of the
-debug options (@pxref{CHR Debugging Options}). @refill
-
-@node CHR Debugging Options,  , CHR Debugging Messages, CHR Debugging
-@subsection CHR Debugging Options
-@cindex CHR debugging options
-
-This section describes the options available when the system prompts you
-after printing out a debugging message.  Most of them you know from the
-standard Prolog debugger. All the options are one letter mnemonics, some
-of which can be optionally followed by a decimal integer.  They are read
-from the standard input stream up to the end of the line
-(Return, @key{<cr>}). Blanks will be ignored.
-
-The only option which you really have to remember is @samp{h}.  This
-provides help in the form of the following list of available options.
-
-@example
-@group
-CHR debugging options:
-   <cr>   creep            c      creep
-    l     leap                         
-    s     skip             s <i>  skip (ancestor i)
-    g     ancestors                   
-    &     constraints      & <i>  constraints (details)
-    n     nodebug          =      debugging
-    +     spy this                    
-    -     nospy this       .      show rule
-    <     reset printdepth < <n>  set printdepth
-    a     abort            b      break
-    ?     help             h      help
-@end group
-@end example
-
-@table @kbd
-@item c
-@itemx @key{<cr>}
-@dfn{creep} causes the debugger to single-step to the very next port
-and print a message.  Then if the port is leashed, the
-user is prompted for further interaction.  Otherwise, it continues creeping.
-If leashing is off, creep is the same as @dfn{leap} (see below) except that a
-complete trace is printed on the standard error stream.  @refill
-
-@item l
-@dfn{leap} causes the debugger to resume running your program, only
-stopping when a spy-point is reached (or when the program terminates).
-Leaping can thus be used to follow the execution at a higher level than
-exhaustive tracing. @refill
-
-@item s
-@itemx s i
-@dfn{skip} over the entire execution of the constraint.  That is, you
-will not see anything until control comes back to this constraint (at
-either the @code{exit} port or the @code{fail} port). This includes
-ports with spy-points set; they will be masked out during the skip.
-The command can be used with a numeric argument to skip the execution
-up to and including the ancestor indicated by the argument.
-Example:
-@example
-@group
-      ...
-      4   - exit    prime(8)#<c6> ? g
-Ancestors:
-      1   1 apply   eratosthenes:rule(2) @@ primes(10)#<c1>
-      2   1 apply   eratosthenes:rule(2) @@ primes(9)#<c3>
-      3   1 apply   eratosthenes:rule(2) @@ primes(8)#<c5>
-      4   - call    prime(8)#<c6>
-
-      4   - exit    prime(8)#<c6> ? s 2
-      2   - exit    primes(9)#<c3> ? 
-@end group
-@end example
-
-@item g
-@dfn{print ancestors} provides you with a list of ancestors to the
-currently active constraint, i.e.@: all constraints not yet exited that led 
-to the current constraint in the derivation sequence.
-The format is the same as with trace messages. 
-Constraints start with @code{call} entries in the stack.
-The subsequent application of a rule replaces the call entry
-in the stack with an @code{apply} entry. Later the constraint
-shows again as @code{redo} or @code{fail} entry.
-Example:
-@example
-@group
-      0   - call    primes(10)#<c1> ? 
-      1   1 try     eratosthenes:rule(2) @@ primes(10)#<c1> ? g
-
-Ancestors:
-      1   - call    primes(10)#<c1>
-
-      1   1 try     eratosthenes:rule(2) @@ primes(10)#<c1> ? 
-      1   1 apply   eratosthenes:rule(2) @@ primes(10)#<c1> ? 
-      1   - call    prime(10)#<c2> ? 
-      2   - insert  prime(10)#<c2>
-      2   - exit    prime(10)#<c2> ? g
-
-Ancestors:
-      1   1 apply   eratosthenes:rule(2) @@ primes(10)#<c1>
-      2   - call    prime(10)#<c2>
-@end group
-@end example
-
-@item &
-@dfn{print constraints} prints a list of the constraints in the
-constraint store. With a numeric argument, details relevant primarily to
-CHR implementors are shown. @refill
-
-@item n
-@dfn{nodebug} switches the CHR debugger off. @refill
-
-@item =
-@dfn{debugging} outputs information concerning the status of the CHR debugger
-as via @code{chr_debugging/0}
-
-@item +
-@dfn{spy this} sets a spy-point on the current constraint or rule.
-
-@item -
-@dfn{nospy this} removes the spy-point from the current constraint or
-rule, if it exists.
-
-@item .
-@dfn{show rule}
-prints the current rule instantiated by the matched constraints. Example:
-@example
- 8 1 apply  era:absorb(8) @@ prime(4)#<c14> \ prime(8)#<c6> ? .
-
- absorb(8) @@
-  prime(4)#<c14> \ 
-    prime(8)#<c6> <=>
-
-    8 mod 4=:=0
-    |
-    true.
-@end example
-
-@item <
-@itemx < n
-While in the debugger, a @dfn{printdepth} is in effect for limiting
-the subterm nesting level when printing rules and constraints.
-The limit is initially 10.  This command, without arguments, resets the
-limit to 10.  With an argument of @var{n}, the limit is set to
-@var{n}. An argument @var{n} of 0 disables depth limit in the debugger.
-@refill
-
-@item a
-@dfn{abort} calls the built-in predicate @code{abort/0}.
-@refill
-
-@item b
-@dfn{break} calls the built-in predicate @code{break/0}, thus putting
-you at a recursive top-level.  When you end the break (entering ^D)
-you will be re-prompted at the port at which you broke. The
-CHR debugger is temporarily switched off as you call the break and will
-be switched on again when you finish the break and go back to the old
-execution.  Any changes to the CHR leashing or to spy-points during the
-break will remain in effect.
-@refill
-
-@item ?
-@itemx h
-@dfn{help} displays the table of options given above.  @refill
-
-@end table
-
-
-
-
-@node CHR Programming Hints, CHR Constraint Handlers, CHR Debugging, CHR
-@section Programming Hints
-
-This section gives you some programming hints for CHR. For maximum
-efficiency of your constraint handler, see also the previous subsections
-on declarations and options.
-
-Constraint handling rules for a given constraint system can often be
-derived from its definition in formalisms such as inference rules,
-rewrite rules, sequents, formulas expressing axioms and theorems.
-CHR can also be found by first considering
-special cases of each constraint and then looking at interactions of
-pairs of constraints sharing a variable. Cases that do not occur in the
-application can be ignored.
-
-It is important to find the right @dfn{granularity} of the constraints.
-Assume one wants to express that @dfn{n} variables are different from
-each other.  It is more efficient to have a single constraint
-@code{all_different(List_of_n_Vars)} than @dfn{n*n} inequality
-constraints between each pair of different variables.  However, the
-extreme case of having a single constraint modeling the whole constraint
-store will usually be inefficient.
-
-Starting from an executable specification, the rules can then be refined
-and adapted to the specifics of the application.  Efficiency can be
-improved by weakening the guards to perform simplification as early as
-needed and by strengthening the guards to do the @dfn{just right} amount
-of propagation.  Propagation rules can be expensive, because no
-constraints are removed. 
-
-The more heads a rule has, the more expensive it is.  @dfn{Rules with
-several heads} are more efficient, if the heads of the rule share a
-variable (which is usually the case). Then the search for a partner
-constraint has to consider less candidates.  In the current
-implementation, constraints are indexed by their functors, so that the
-search is only performed among the constraints containing the shared
-variable. Moreover, two rules with identical
-(or sufficiently similar) heads can be merged into one rule so that the
-search for a partner constraint is only performed once instead of twice.
-
-As @dfn{guards} are tried frequently, they should be simple @dfn{tests}
-not involving side-effects.  Head matching is more efficient than
-explicitly checking equalities in the ask-part of the guard.  In the
-tell part of a guard, it should be made sure that variables from the
-head are never touched (e.g.@: by using @code{nonvar} or @code{ground} if
-necessary). For efficiency and clarity reasons, one should also avoid
-using constraints in guards.  Besides conjunctions, disjunctions are
-allowed in the guard, but they should be used with care.  The use of
-other control built-in predicates in the guard is
-discouraged.  Negation and if-then-else in the ask part of a guard can
-give wrong results, since e.g.@: failure of the negated goal may be due to
-touching its variables.
-
-@dfn{Several handlers can be used simultaneously if} they do not share
-constraints with the same name. The implementation will not work
-correctly if the same constraint is defined in rules of different
-handlers that have been compiled separately. In such a case, the
-handlers must be merged @dfn{by hand}. This means that the source code
-has to be edited so that the rules for the shared constraint are
-together (in one module). Changes may be necessary (like
-strengthening guards) to avoid divergence or loops in the computation.
-
-
-@node CHR Constraint Handlers, CHR Backward Compatibility, CHR Programming Hints, CHR
-@section Constraint Handlers
-
-The CHR library comes with plenty of constraint handlers written in CHR.
-The most recent versions of these are maintained at:
-
-@example
-http://www.pst.informatik.uni-muenchen.de/~fruehwir/chr-solver.html
-@end example
-
-@table @file
-
-@item arc.pl
-classical arc-consistency over finite domains
-
-@item bool.pl
-simple Boolean constraints
-
-@item cft.pl
-feature term constraints according to the CFT theory
-
-@item domain.pl
-finite domains over arbitrary ground terms and interval domains over integers and reals, but without arithmetic functions
-
-@item gcd.pl
-elegant two-liner for the greatest common divisor
-
-@item interval.pl
-straightforward interval domains over integers and reals, with arithmetic functions
-
-@item kl-one.pl
-terminological reasoning similar to KL-ONE or feature trees
-
-@item leq.pl
-standard introductory CHR example handler for less-than-or-equal
-
-@item list.pl
-equality constraints over concatenations of lists (or strings)
-
-@item listdom.pl
-a straightforward finite enumeration list domains over integers, similar to @file{interval.pl}
-
-@item math-elim.pl
-solves linear polynomial equations and inequations using variable elimination, several variations possible
-
-@item math-fougau.pl
-solves linear polynomial equations and inequations by combining variable elimination for equations with Fourier's algorithm for inequations, several variations possible
-
-@item math-fourier.pl 
-a straightforward Fouriers algorithm to solve polynomial inequations
-over the real or rational numbers
-
-@item math-gauss.pl
-a straightforward, elegant implementation of variable elimination for equations in one rule
-
-@item minmax.pl
-simple less-than and less-than-or-equal ordering constraints together with minimum and maximum constraints
-
-@item modelgenerator.pl
-example of how to use CHR for model generation in theorem proving
-
-@item monkey.pl
-classical monkey and banana problem, illustrates how CHR can be used as
-a fairly efficient production rule system
-
-@item osf.pl
-constraints over order sorted feature terms according to the OSF theory
-
-@item oztype.pl
-rational trees with disequality and OZ type constraint with intersection
-
-@item pathc.pl
-the most simple example of a handler for path consistency - two rules
-
-@item primes.pl
-elegant implementations of the sieve of Eratosthenes reminiscent of the
-chemical abstract machine model, also illustrates use of CHR as a
-general purpose concurrent constraint language
-
-@item scheduling.pl
-simple classical constraint logic programming scheduling example on building a house
-
-@item tarski.pl
-most of Tarski's axiomatization of geometry as constraint system
-
-@item term.pl
-Prolog term manipulation built-in predicates @code{functor/3, arg/3, =../2} as constraints
-
-@item time-pc.pl
-grand generic handler for path-consistency over arbitrary constraints,
-load via @file{time.pl} to get a powerful solver for temporal constraints based on Meiri's unifying framework. @file{time-rnd.pl} contains a generator for random test problems.
-
-@item time-point.pl
-quantitative temporal constraints over time points using path-consistency
-
-@item tree.pl
-equality and disequality over finite and infinite trees (terms)
-
-@item type.pl
-equalities and type constraints over finite and infinite trees (terms)
-
-@end table
-
-You can consult or compile a constraint handler from the CHR library using
-e.g.: 
-@example
-?- [library('chr/examples/gcd')].
-?- compile(library('chr/examples/gcd')).
-@end example
-If you want to learn more about the handlers, 
-look at their documented source code.
-
-In addition, there are files with example queries for some handlers,
-their file name starts with @file{examples-} and the file extension
-indicates the handler, e.g.@: @file{.bool}:
-
-@example
-examples-adder.bool
-examples-benchmark.math
-examples-deussen.bool
-examples-diaz.bool
-examples-fourier.math
-examples-holzbaur.math
-examples-lim1.math
-examples-lim2.math
-examples-lim3.math
-examples-puzzle.bool
-examples-queens.bool
-examples-queens.domain
-examples-stuckey.math
-examples-thom.math
-@end example
-
-
-@node CHR Backward Compatibility,  , CHR Constraint Handlers, CHR
-@section Backward Compatibility
-
-In this section, we discuss backward compatibility with the CHR library
-of Eclipse Prolog.
-
-@enumerate
-
-@item
-The restriction on at most two heads in a rule has been abandoned.  A
-rule can have as many heads as you like. Note however, that searching
-for partner constraints can be expensive.
-
-@item
-By default, rules are compiled in textual order. This gives the
-programmer more control over the constraint handling process. In the
-Eclipse library of CHR, the compiler was optimizing the order of
-rules. Therefore, when porting a handler, rules may have to
-be reordered. A good heuristic is to prefer simplification to
-simpagation and propagation and to prefer rules with single heads to
-rules with several heads. Instead of manually rearranging an old handler
-one may also use the following combination of options to get the
-corresponding effect:
-@example
-option(rule_ordering,heuristic).
-option(revive_scheme,old).
-@end example
-
-@item
-For backward compatibility, the @code{already_in_store},
-@code{already_in_head} and @code{guard_bindings} options
-are still around, but there are CHR syntax extensions: @ref{CHR Syntax} 
-and pragmas @ref{CHR Pragmas}
-offering better grained control.
-
-@item
-The Eclipse library of CHR provided automatic built-in labeling through
-the @code{label_with} declaration. Since it was not widely used and can
-be easily simulated, built-in labeling was dropped.  The same effect can
-be achieved by replacing the declaration @code{label_with Constraint if
-Guard} by the simplification rule @code{chr_labeling, Constraint <=>
-Guard | Constraint', chr_labeling} and by renaming the head in each
-clause @code{Constraint :- Body} into @code{Constraint' :- Body} where
-@code{Constraint'} is a new predicate.  Efficiency can be improved by
-declaring @code{Constraint} to be passive: @code{chr_labeling,
-Constraint#Id <=> Guard | Constraint', chr_labeling pragma passive(Id)}.
-This translation will not work if @code{option(already_in_heads,on)}.
-In that case use e.g.@: @code{chr_labeling(_), Constraint <=> Guard |
-Constraint', chr_labeling(_)} to make the new call to
-@code{chr_labeling} differ from the head occurrence.
-
-@item
-The set of built-in predicates for advanced CHR users is now larger
-and better designed. Also the debugger has been improved. The Opium
-debugging environment is not available in SICStus Prolog.
-@end enumerate
-
+@include chr.tex
 
 @node Logtalk, Threads, CHR, Extensions
 @chapter Logtalk