Did you know ... Search Documentation:
Pack modeling -- prolog/clp.pl
PublicShow source
author
- Francois Fages
version
- 1.1.5

This library

?- 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).
?- 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).
 int_sum(+VarDomains, +Expr, ?Sum)
Sum of int Expr defined in comprehension by "in" domain and "where" condition
 int_product(+VarDomains, +Expr, ?Product)
Product of int Expr defined in comprehension by "in" domain and "where" condition
 int_minimum(+A, ?Min)
constrains variable Min to be the minimum value of non-empty array or list A of integers.
 int_minimum(+VarDomains, +Expr, ?Minimum)
Minimum value of int Expr in non-empty set defined in comprehension by "in" domain and "where" conditions.
 int_maximum(+VarDomains, +Expr, ?Maximum)
Maximum value of int Expr in non-empty set defined in comprehension by "in" domain and "where" conditions.
 int_maximum(+A, ?Max)
constrains variable Max to be the maximum value in non-empty array or list A of integers.
 lex_leq(+A, +B)
lexicographic ordering between arrays or lists
 lex_lt(+A, +B)
strict lexicographic ordering between arrays or lists
 truth_value(+Constraint, ?Boolean)
Reification constraint for clpr and clpfd constraints. Equivalent to Boolean #<==> Constraint for a clpfd constraint. For a clpr constraint, its entailment is checked only once when posting the constraint. See clpr_entailed/1 for checking later entailment of a clpr constraint reified by truth_value/2.
?- array(A, [3]), truth_value({A[1] < 3.14}, B).
A = array(_A, _, _),
freeze(B, clp:clpr_reify(_A<3.14, _A>=3.14, B)).
 clpr_entailed(?Boolean)
checks entailment of any clpr constraint reified by truth_value/2 on Boolean variable.
 rel(?Arg1, +Relation, ?Arg2)
applies binary Relation to Arg1 and Arg2, element-wise. The arguments can be arrays, lists, clpfd or clpr variables or constants interpreted as constant array or list of appropriate size.
 op_rel(?Arg1, +Operation, ?Arg2, +Relation, ?Arg3)
applies binary Operation to Arg1 and Arg2, element-wise, and compares the results with Relation to Arg3. The arguments can be arrays, lists, clpfd or clpr variables or constants interpreted as constant array or list of appropriate size.

E.g. the Hadamart product of two integer matrices of same dimension can be defined by op_rel(A, *, B, #=, C) over integers, op_rel(A, *, B, '{=}', C) over real numbers.

 sum(+A, +Relation, ?Sum)
hybrid constraint to constrain Sum to be in clpfd or clpr Relation to the sum of elements in array or list A.
 scalar_product(+A, +B, +Rel, ?C)
constraint on arrays or lists similar to library(clpfd) constraint scalar_product on list of integers or reals.
 transpose(+A, ?B)
constraint on arrays or lists A and B similar to library(clpfd) constraint transpose on lists.
 all_different(+A)
constraint on arrays similar to library(clpfd) constraint all_different on lists.
 all_distinct(A)
constraint on arrays or lists using library(clpfd) constraint all_distinct on list.
 lex_chain(+A)
constraint on array or list A similar to library(clpfd) constraint lex_chain on lists.
 tuples_in(+A, +B)
constraint on arrays or lists A and B similar to library(clpfd) constraint tuples_in on lists.
 serialized(+A, +B)
constraint on arrays or lists A and B similar to library(clpfd) constraint serialized on lists.
 global_cardinality(+A, +B)
constraint on array or list A similar to library(clpfd) constraint global_cardinality on lists.
 global_cardinality(+A, +B, +C)
constraint on array or list A similar to library(clpfd) constraint global_cardinality on lists.
 circuit(+A)
constraint on array or list A similar to library(clpfd) constraint circuit on lists.
 cumulative(+A)
constraint on array or list A similar to library(clpfd) constraint cumulative on lists.
 cumulative(+A, +O)
constraint on array or list A with options O similar to library(clpfd) constraint cumulative on lists.
 disjoint2(+A)
constraint on array or list A similar to library(clpfd) constraint disjoint2 on lists.
 element(+I, +A, +V)
constraint on array or list B similar to library(clpfd) constraint element on list.
 automaton(+A, +B, +C)
constraint on arrays or lists A, B, C similar to library(clpfd) constraint automaton on lists.
 chain(+A, +B)
constraint on array or list A similar to library(clpfd) constraint chain on lists.
 label(Var)
value enumeration predicate on integer arrays or lists similar to library(clpfd) label/1 predicate on lists.
 labeling(Options, Vars)
enumeration predicate on integer array or list Vars, similar to library(clpfd) labeling/2 predicate on lists, but with a new option trace or trace(VarNames) to create the search tree of variable instantiations perfomed by labeling, to visualize it with search_tree_text/0, search_tree_term/1, search_tree_latex/1, search_tree_tikz/1 of library(tracesearch).

VarNames can be a list of same length as Vars, or an atom like 'Q' in which case the variables will be named Q1,...,QN.

?- queens(4, Queens), search_tree_text.
labeling([Q1,Q2,Q3,Q4])
 Q1=1
  Q2=3
  Q2$\neq$3
 Q1$\neq$1
  Q1=2
   [2,4,1,3]
Queens = array(2, 4, 1, 3) ;
labeling([Q1,Q2,Q3,Q4])
 Q1=1
  Q2=3
  Q2$\neq$3
 Q1$\neq$1
  Q1=2
   [2,4,1,3]
  Q1$\neq$2
   Q1=3
    [3,1,4,2]
Queens = array(3, 1, 4, 2) ;
false.
 float_sum(+VarDomains, +Expr, ?Sum)
Sum of float Expr defined in comprehension by "in" domain and "where" condition
 float_product(+VarDomains, +Expr, ?Product)
Product of float Expr defined in comprehension by "in" domain and "where" condition
 {=}(+Expr1, +Expr2)
predicate name for constraint {Expr1 = Expr2}
 {>=}(+Expr1, +Expr2)
predicate name for constraint {Expr1 >= Expr2}
 {=<}(+Expr1, +Expr2)
predicate name for constraint {Expr1 =< Expr2}
 {>}(+Expr1, +Expr2)
predicate name for constraint {Expr1 > Expr2}
 {<}(+Expr1, +Expr2)
predicate name for constraint {Expr1 < Expr2}
 {=\=}(+Expr1, +Expr2)
predicate name for constraint {Expr1 =\= Expr2}
 {+Constraint}
front-end to library(clpr) {}/1 predicate for allowing shorthand functional notations in Constraint.
 entailed(+Constraint)
front-end to library(clpr) entailed/1 predicate for allowing shorthand functional notations in Constraint.
 maximize(+Expression)
front-end to library(clpr) maximize/1 predicate for allowing shorthand functional notations in Expression.
 minimize(+Expression)
front-end to library(clpr) minimize/1 predicate for allowing shorthand functional notations in Expression.
 inf(+Expression, -Inf)
front-end to library(clpr) inf/2 predicate for allowing shorthand functional notations in Expression.
 sup(+Expression, -Sup)
front-end to library(clpr) sup/2 predicate for allowing shorthand functional notations in Expression.
 bb_inf(+Ints, +Expression, -Inf, -Vertex, +Eps)
front-end to library(clpr) bb_inf/5 predicate for allowing shorthand functional notations in Expression.
 bb_inf(+Ints, +Expression, -Inf)
front-end to library(clpr) bb_inf/3 predicate for allowing shorthand functional notations in Expression.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 in(Arg1, Arg2)
 ins(Arg1, Arg2)
 #>(Arg1, Arg2)
 #<(Arg1, Arg2)
 #>=(Arg1, Arg2)
 #=<(Arg1, Arg2)
 #=(Arg1, Arg2)
 #\=(Arg1, Arg2)
 #\(Arg1)
 #<==>(Arg1, Arg2)
 #==>(Arg1, Arg2)
 #<==(Arg1, Arg2)
 #\/(Arg1, Arg2)
 #\(Arg1, Arg2)
 #/\(Arg1, Arg2)
 array(Arg1)
 array(Arg1, Arg2)
 cell(Arg1, Arg2, Arg3)
 cell(Arg1, Arg2)
 array_lists(Arg1, Arg2)
 array_list(Arg1, Arg2)
 set_cell(Arg1, Arg2, Arg3)
 set_cell(Arg1, Arg2)
 nb_set_cell(Arg1, Arg2, Arg3)
 nb_set_cell(Arg1, Arg2)
 for_all(Arg1, Arg2)
 list_of(Arg1, Arg2, Arg3)
 aggregate_for(Arg1, Arg2, Arg3, Arg4, Arg5, Arg6)
 exists(Arg1, Arg2)
 let(Arg1, Arg2)
 start_tracing
 currently_tracing
 stop_tracing
 clear_tracing
 add_node(Arg1)
 current_search_tree_depth(Arg1)
 search_tree_term(Arg1)
 search_tree_latex(Arg1)
 search_tree_latex
 search_tree_tikz(Arg1)
 search_tree_tikz
 search_tree_text
 search_tree_text(Arg1)
 term_to_text(Arg1)
 term_to_text(Arg1, Arg2)
 term_to_tikz(Arg1)
 term_to_tikz(Arg1, Arg2)
 term_to_latex(Arg1)
 term_to_latex(Arg1, Arg2)