Frontend to library(clpr) and library(clpfd) to allow shorthand functional notations in clpr and clpfd constraints on arrays and lists

author

- Francois Fages

version

- 1.1.5

This library

defines a few extra clpfd constraints int_sum/3, int_product/3, int_minimum/2, int_maximum/2, lex_leq/2, lex_lt/2, and clpr constraints float_sum/3, float_product/3;
adds reification constraint truth_value/2 for both clpfd and clpr constraints

?- array(A, [3]), truth_value({A[1] < 3.14}, Boolean).
A = array(_A, _, _),
when((nonvar(_A);nonvar(B)), clp:clpr_reify(_A<3.14, _A>=3.14, [_A], Boolean)),
clpfd:(Boolean in 0..1).

?- array(A, [3]), truth_value({A[1] < 3.14}, Boolean), array_list(A, [1, 2.7, 42]).
A = array(1, 2.7, 42),
Boolean = 1.

allows shorthand/3 functional notations in domains and constraints, e.g. for subscripted variables with Array[Indices] functional notation:

?- array(A, [3]), for_all(I in 1..2, A[I] #< A[I+1]).
A = array(_A, _B, _C),
clpfd:(_A#=<_B+ -1),
clpfd:(_B#=<_C+ -1).

adds shorthand/3 clauses for allowing constraint predicates to appear as constraint functions in expressions, with last predicate argument as result, e.g. the magic series puzzle can be writen using shorthand truth_value functional notation for truth_value/2 constraint:

?- array(X, [N]), for_all(I in 1..N, X[I] #= int_sum(J in 1..N, truth_value(X[J] #= I-1))), label(X).
X = array(1, 2, 1, 0),
N = 4 ;
X = array(2, 0, 2, 0),
N = 4 ;
X = array(2, 1, 2, 0, 0),
N = 5 ;
X = array(3, 2, 1, 1, 0, 0, 0),
N = 7 ;
X = array(4, 2, 1, 0, 1, 0, 0, 0),
N = 8 ;
X = array(5, 2, 1, 0, 0, 1, 0, 0, 0),
N = 9 ;
X = array(6, 2, 1, 0, 0, 0, 1, 0, 0, 0),
N = 10 .

defines hybrid clpr-clpfd constraints on lists and arrays, including op_rel/5, sum/3, e.g.

?- A=array([1,2],[3,4]), op_rel(A, +, A, #=, C).
A = array([1, 2], [3, 4]),
C = array(array(2, 4), array(6, 8)).

?- A=[[1,2],[3,4]], op_rel(A, +, A, #=, C).
A = [[1, 2], [3, 4]],
C = [[2, 4], [6, 8]].

?- L=[X, Y, Z], L ins 1..3, for_all(V in L, V#>1).
L = [X, Y, Z],
clpfd:(X in 2..3),
clpfd:(Y in 2..3),
clpfd:(Z in 2..3).

adds option trace to labeling/2 predicate for building the search tree and visualizing it using search_tree_text/0, search_tree_term/1, search_tree_latex/1, search_tree_tikz/1 of library(tracesearch).
adds a patch to library(clpfd) unify_attributes_hook/2 to avoid the duplication of constraint propagators when unifying two clpfd variables. The duplication of library(clpfd) constraints was due to the use of append/3 in unify_attributes_hook/2 now replaced by union_propagators/3

?- use_module(library(clpfd)).
true.

?- X#>Z, Y#>Z, X#=Y.
X = Y,
Z#=<Y+ -1,
Z#=<Y+ -1.

?- L=[A, B], L ins 1..2, A #=< B, bagof(W, member(W, L), L2).
L = L2, L2 = [A, B],
A in 1..2,
B#>=A,
B#>=A,
B#>=A,
B in 1..2.

You can set nb_setval(fdvar_unification_warning, true) to get warnings when two fd variables are unified (default is false).

TODO: the constraint propagators should rather be simplified when 2 variable unify (as done in SMT solvers). This is a winning strategy on global constraints compared to mere domain consistency checking;

e.g. simplification of sum scalar_product lex_chain serialized global_cardinality cumulative element automaton? transpose? chain?

e.g. in all_distinct/1 all_different/1 unify_attribute_hook should rather fail when propagators get duplicated variables

?- L=[X, Y, Z], L ins 1..3, all_distinct(L), X #= Y.
Warning: unifying fdvar _252 clpfd_attr(no,no,no,from_to(n(1),n(3)),fd_props([propagator(pexclude([_252,_308],[],_252),_396)],[],[propagator(pdistinct([_252,_252,_308]),_554)]))
 with fdvar domain from_to(n(1),n(3)) fd_props([propagator(pexclude([_308],[_252],_252),_466)],[],[propagator(pdistinct([_252,_252,_308]),_554)])
L = [Y, Y, Z],
X = Y,
clpfd:(Y in 1..3),
clpfd:all_distinct([Y, Y, Z]),
clpfd:(Z in 1..3).