The solver contains predicates for checking the consistency and entailment of finite domain constraints, as well as solving for solution values for your problem variables.
In the context of this constraint solver, a finite domain is a subset of small integers, and a finite domain constraint denotes a relation over a tuple of small integers (see Glossary). Hence, only small integers and unbound variables are allowed in finite domain constraints.
All domain variables, i.e. variables that occur as arguments to
finite domain constraints get associated with a finite domain, either
explicitly declared by the program, or implicitly imposed by the
constraint solver. Temporarily, the domain of a variable may actually
be infinite, if it does not have a finite lower or upper bound. If
during the computation a variable receives a new lower or upper bound
that cannot be represented as a small integer, an overflow condition is
issued. This is expressed as silent failure or as a representation
error, subject to the
overflow option of
The set of current domains of all domain variables is called the domain store. Domain store S is an extension of domain store T if each domain in S is a subset of the corresponding domain in T. If some domain is empty, the store is contradictory and execution backtracks; otherwise, it is consistent. At the end of a successful computation, all domains have usually become singletons, i.e. the domain variables have become assigned. The domains don't become singletons automatically. Usually, it takes some amount of search to find an assignment that satisfies all constraints. It is the programmer's responsibility to do so. If some domain variables are left unassigned in a computation, the garbage collector will preserve all constraint data that is attached to them.
Please note: if a term containing domain variables is written,
copied, asserted, gathered as a solution to
friends, or raised as an exception, those domain variables will be
replaced by brand new variables in the copy. To retain the domains and
any attached constraints, you can use
clpfd:full_answer asserted (see ref-lte-cpt and Answer Constraints). API change wrt. release 3.
Every finite domain constraint is implemented by a propagator, or a set of such. Some constraints have alternative propagators with differing properties. All propagators act as coroutines performing incremental constraint solving, removing values from domains, and/or entailment checking. They wake up by changes in the domains of its arguments. A propagator P can be seen as a function on constraint store S: P(S) denotes the extension of S resulting from applying P on S.
Propagators come in two kinds: indexicals, stateless reactive functional rules implemented by a stack machine and running, and global propagators, usually stateful, implemented in C or Prolog, and using algorithms from many fields of computer science. At the heart of the constraint solver is a scheduler for propagators, where indexicals have priority over global propagators.
Certain properties of propagators are desirable: