Integer Values

The finite domain solver allows denoting integer value expressions. These expressions can contain native Prolog variables. Integer expressions are posted to the finite domain solver via the predicate #=/2. Internally integer equations are broken down into elementary integer equations with the help of new native Prolog variables. The resulting elementary integer equations are automatically shown by the top-level.

?- X*Y*Z #= T.
_C*Z #= T,
X*Y #= _C

Forward chaining rules and attribute variable hooks guard the interaction between the elementary integer equations. A minimal logic reading of forward chaining rules with delete has been presented in [1]. It has also been shown there how forward chaining rules with delete can do simplifications if the constraint store is held in the forward store. Currently the following inference rule sets have been implemented for integer value expressions:

The forward checking consists of the two inference rules constant elimination and constant back propagation, depending on whether the constants equations have first arrived in the for-ward store or the elementary integer equations. The forward checking also provides the inference rules of union find and variable renaming. Where permitted the #=/2 integer equations are replaced by native Prolog unification. It is also allowed mixing native Prolog unification =/2 with integer equations:

?- X = Y, 4 #= X+Y.
X = 2,
Y = 2
?- 4 #= X+Y, X = Y.
X = 2,
Y = 2

The duplicate detection has only been implemented for elementary integer equations that are the scalar product of a constant vector and a variable vector. The duplicate detection does not yet work for arbitrary products. It is handy in that it reduces the number of elementary equations and might also detect inconsistencies early on:

?- 2*X #= 4*Y, 3*X #= 6*Y.
X #= 2*Y
?- X #= Y+1, Y #= X+1.

The following integer value expressions are provided:

V (finite):
A native Prolog variable V represents an integer variable.
I (finite):
An integer I represents an integer constant.
A + B (finite):
If A and B are expressions then the sum A+B is also an expression.
A – B (finite):
If A and B are expressions then the subtraction A-B is also an expression.
- A (finite):
If A is an expression then the change sign -A is also an expression.
A * B (finite):
If A and B are expressions then the multiplication A*B is also an expression.
abs(A) (finite):
If A is an expression then absolute value abs(A) is also an expression.
T [E1, .., En] (finite):
If T is a term and E1, .., En are expressions for 1 ≤ n ≤ 7 then the array subscript T [E1, .., En] is also an expression.
C (finite):
A callable C is also an expression.

The following integer value predicates are provided:

A #= B:
If A and B are expressions then their equality is posted.