Built InsMore Advanced Topics

In order to simplify problem representations, and for reasons of efficiency, a number of sorts and functions have been provided as built in features of the language. Note that built in function symbols are all in UPPER CASE.

Built in sorts

Two sorts are pre-defined. The first you have already met: natural numbers (non-negative integers) are available using the sort natnum. Their canonical names are what you learned they were in primary school, namely “36”, “0”, “5”, etc. and they come in the expected order. The sort name “natnum” may be abbreviated to “nat”.

The second built-in sort is bool (i.e. boolean) which is an enumerated sort with just two elements “FALSE” and “TRUE” in that order. Note that if you do not write these in UPPER CASE they will be parsed as arbitrary names, and errors may then occur. Functions whose value sort is bool are just relations (also known as predicates). You will see examples on the “Constraints revisited” page and in the various sample problems.

Temporary note: the current version of the solver does not yet have the ability to treat numbers fully in accordance with arithmetic. Instead, it thinks natnum is just another finite domain consisting of the numbers 0 to MAX, where MAX is a smallish constant (by default set to 30, for no especially good reason, and redefinable by means of a sort “cardinality” statement). The sort name “int” is allowed, for reasons of backward compatibility with old versions of the solver, but integers as a sort are not implemented. Instead, “int” is treated as another synonym for “natnum”, so negative numbers and numbers greater than MAX will not be handled properly. For logic puzzles, anyway, you don’t need them.

Built in functions

There are some pre-defined boolean operations or connectives:

NOT (bool): bool	The negation operator reverses the sense of propositions. The logical symbol ¬ means NOT.
AND (bool,bool): bool	The conjunction “X AND Y” holds if and only if both X and Y hold. The logical symbol ∧ means AND.
OR (bool,bool): bool	The disjunction “X OR Y” holds if and only if either X holds or Y holds (or both). The logical symbol ∨ means OR.
XOR (bool,bool): bool	“X XOR Y” holds if and only if either X holds or Y holds, but not both. If X and Y are boolean, the non-identity symbol != means XOR.
IMP (bool,bool): bool	The implication “X IMP Y” holds if and only if either X fails or Y holds (or both). The logical symbol → means IMP.
IFF (bool,bool): bool	The equivalence “X IFF Y” holds if and only if X and Y either both hold or both fail. If X and Y are boolean, the identity symbol = means IFF.

There are also “quantifiers” which can be used to bind variables of any sort S.

ALL (var:S) (bool): bool	The universal quantifier binds a variable and is used to say that the formula in its scope is true for all values of that variable. The logical symbol ∀ means ALL.
SOME (var:S) (bool): bool	The existential quantifier binds a variable and is used to say that the formula in its scope is true for at least one value of that variable. The logical symbol ∃ means SOME.

Moreover, every sort S comes with the following pre-defined predicates:

= (S,S)	The identity relation is true if the two “S” objects are in fact one and the same, and false if they are different.
< (S,S)	The “less than” relation is true if the thing on the left comes before the thing on the right in the enumeration of “S” objects, or if it has a lower number in the case of a non-enumerated sort.
<= (S,S)	The “less than or equal to” relation holds if either of the previous two does.
> (S,S)	The “greater than” relation is true if the thing on the left comes after the thing on the right in the enumeration of “S” objects, or if it has a higher number in the case of a non-enumerated sort.
>= (S,S)	The “greater than or equal to” relation holds if either the two objects are identical or else the first one is greater than the second.
<> (S,S)	The “different” relation is true if the first of the two “S” objects is either less than or greater than the second, and false if they are identical.
EST (S)	“EST” (“there Exists Such a Thing as”) is true if the thing it applies to exists, and false if it does not. For example, if “Fin” is the last thing in the enumeration of “S” objects, then EST (Fin) is true but EST (Fin+1) is false.

Each of the pre-defined binary relations may be negated by placing ‘!’ before it, so we may use “!=” for non-identity, or “!<=” in place of “>”, for example. The negative relations obtained in this way are subtly different from the “corresponding” positive ones, in cases where things do not exist. For details, see the guide page on existence.

pre-defined functions:

+ (S,natnum): S	The addition function, applied to any object and any natural number N, gives the N-th next “S” object.
- (S,natnum): S	The subtraction function, applied to any object and any natural number N, gives the N-th previous “S” object.
PRED (S): S	The predecessor function, applied to any object other than MIN, gives the previous object in the ordering of sort S. Thus PRED (x) means exactly the same as x-1. PRED (MIN) does not exist.
SUCC (S): S	The successor function, applied to any object other than MAX, gives the next object in the ordering of sort S. Thus SUCC (x) means exactly the same as x+1. SUCC (MAX) does not exist.
DIF (S,S): natnum	The difference function, applied to any two objects of the same sort, gives the (absolute) distance between them in the enumeration of “S” objects. So DIF (a,a) is always 0, and DIF (A,MIN) is the position of a (starting from 0) in the standard ordering of its sort.

and pre-defined names:

MIN : S.	The constant MIN is the first thing in the ordering of S, written as zero if S is not defined by “enum”. If the type if MIN is not deducible from its position in a constraint, it must be supplied by appending an underscore and the name of S. So MIN_nat is the number 0, for instance.
MAX : S.	The constant MAX is the last thing in the ordering of S. If the type of MAX is not deducible from its position in a constraint, it must be supplied by appending an underscore and the name of S. So MAX_bool is the truth value TRUE, for instance.