First, the current propagator is now logged and not re-triggered
during filtering. Second, and more significantly, all neq_num/2
constraints are scheduled and processed before more global constraints
are invoked. In this way, all the distilled information can be taken
into account by subsequently invoked global constraints.
These changes yield a 3-fold improvement in several Sudoku instances,
and a significant runtime reduction in social golfer instance 8-4-9.
This terminology is a bit harder to understand than that of the other
type checks.
Scryer Prolog comprises two individually consistent but incompatible
notions of terms, namely terms and rational trees (which are also
called "cyclic terms"). This leads to a confusion in terminology,
because cyclic terms are not terms in the former sense even though
they also contain the word "term" in their name.
This terminological confusion is not restricted to terms: We also find
it for example in the notion of lists. Lists are defined inductively:
- The empty list (written as "" or [], called 'nil') is a list.
- A term with principal functor '.'/2 is a list if its second argument
is a list.
Note that a list may contain cyclic terms as elements, and still be
called a list. However, if we post:
?- Ls = [_|Ls].
then Ls is not a list, because it does not fit the inductive
definition. Still, it is sometimes referred to as a "cyclic list" or
"circular list", even though it is not a list. Even Prolog
implementors that aim for strict conformance to the Prolog ISO
standard and are deeply familiar with the standard use this
terminology when talking about such terms, see for example:
https://github.com/ichiban/prolog/pull/198
Consequently, must_be(list, Ls) raises a *type error* in this case.
Terms are distinguished from cyclic terms completely analogously. This
leads to the counterintuitive consequence that *cyclic lists are not
terms*. The reason for this apparent contradiction in terminology is
the mutual incompatibility of different notions of terms. The notion
of "term" precludes rational trees, similar to the notion of "list"
which precludes cyclic lists.
We therefore introduce:
* must_be(term, Term)
- raises an instantiation error if Term contains variables (since
it could still become a rational tree)
- raises a type error if Term is a rational tree
* can_be(term, Term)
- raises a type error if Term is a rational tree
Note that using the notion of "cyclic term" and "acyclic term" in this
terminology would not be a good idea, because this confusion is
precisely what we want to eliminate: must_be(term, Term) should be
usable as a test that reliably determines whether Term can be treated
as a term with the logical properties we expect from terms.
This addresses #1428.
Markus Triska