author

- Francois Fages

version

- 1.1.4

This module provides a constraint-based mathematical modeling language in the spirit of MiniZinc in Prolog (A MiniZinc parser is planned to be added to this library in a next release).

The pack includes 5 modules with the following dependencies quantifiers.pl --> arrays.pl --> clp.pl --> modeling.pl --> examplesFLOPS2024.pl

library(examplesFLOPS2024) contains the examples and benchmark presented in the article:

• F. Fages. A Constraint-based Mathematical Modeling Library in Prolog with Answer Constraint Semantics. 17th International Symposium on Functional and Logic Programming, FLOPS 2024. May 15, 2024 - May 17, 2024, Kumamoto, Japan. LNCS, Springer-Verlag.

library(quantifiers) defines bounded quantifiers with "in" domain and "where" conditions, let bindings, and a multifile user-defined predicate for defining shorthand/3 functional notations in expressions, e.g. conditional expressions with if/3 term.

library(arrays) defines multidimensional arrays for constraints on subscripted variables and the Array[Indices] shorthand/3 notation.

library(clp) is a frontend to library(clpr) and library(clpfd) to define hybrid constraints and allow shorthand notations such as Array[Indices] in constraints and domains.

Below is the example of a goal that can be written in this library to solve the 4-queens placement problem and pretty-print the chessboard, using subscripted variables (arrays) instead of lists, bounded quantifiers instead of recursion and functional notations in let bindings and constraints.

?- N=4, int_array(Queens, [N], 1..N),
  
  for_all([I in 1..N-1, D in 1..N-I],
    (Queens[I] #\= Queens[I+D],
     Queens[I] #\= Queens[I+D]+D,
     Queens[I] #\= Queens[I+D]-D)),
  
  satisfy(Queens),
  
  for_all([I, J] in 1..N,
    let([QJ = Queens[J],
         Q = if(QJ = I, 'Q', '.'),
         B = if(J = N, '\n', ' ')],
        format("~w~w",[Q,B]))).
. . Q .
Q . . .
. . . Q
. Q . .
N = 4,
Queens = array(2, 4, 1, 3) ;
. Q . .
. . . Q
Q . . .
. . Q .
N = 4,
Queens = array(3, 1, 4, 2) ;
false.

Below is an example of hybrid reified clpr clpfd constraint defined in library(clp).

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

?- array(A, [3]), truth_value({A[1] < 3.14}, B), {A[1]=2.7}.
A = array(2.7, _, _),
B = 1.

 bool_array(?Array, ?Dimensions)

Array is a array of Boolean values (0 or 1) or Boolean variables of dimensions Dimensions.

 int_array(?Array, ?Dimensions)

Array is an array of integer numbers or variables of dimensions Dimensions.

 int_array(?Array, ?Dimensions, +Domain)

Array is an array of integer numbers or variables in Domain of dimensions Dimensions.

 float_array(?Array, ?Dimensions)

Array is an array of real numbers or variables of dimensions Dimensions.

 float_array(?Array, ?Dimensions, +Range)

Array is an array of real numbers or variables in Range Min..Max of dimensions Dimensions. If not given the Range variables are returned with constraints, or fails if they are unbounded.

 satisfy(+Term)

enumerate all solutions of the variables contained or related to Term, with smallest-domain first-fail and-choice heuristics ff.

 satisfy(+Term, +Options)

same as satisfy/1 with the Options from library(clpfd) predicate labeling/2.

 satisfy_attvars(+Term)

same as satisfy/1 but enumerating the values of the variables in term and in their attributes.

 satisfy_attvars(+Term, +Options)

same as satisfy/2 but enumerating also the values of the variables contained in the attributes of the variables in Term.

 minimize(+Expr, +Term)

enumerate all solutions of the variables contained in Term in increasing order of Expr.

 minimize(+Expr, +Term, +Options)

same as minimize/2 using extra library(clpfd) labeling/2 options

 maximize(+Expr, +Term)

enumerate all solutions of the variables contained in Term in decreasing order of Expr.

 maximize(+Expr, +Term, +Options)

same as maximize/2 using extra library(clpfd) labeling/2 options

Undocumented predicates

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

 sum(Arg1, Arg2, Arg3)

 scalar_product(Arg1, Arg2, Arg3, Arg4)

 op_rel(Arg1, Arg2, Arg3, Arg4, Arg5)

 rel(Arg1, Arg2, Arg3)

 truth_value(Arg1, Arg2)

 clpr_entailed(Arg1)

 float_sum(Arg1, Arg2, Arg3)

 float_product(Arg1, Arg2, Arg3)

 int_sum(Arg1, Arg2, Arg3)

 int_product(Arg1, Arg2, Arg3)

 int_minimum(Arg1, Arg2, Arg3)

 int_minimum(Arg1, Arg2)

 int_maximum(Arg1, Arg2, Arg3)

 int_maximum(Arg1, Arg2)

 lex_leq(Arg1, Arg2)

 lex_lt(Arg1, Arg2)

 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)

 all_different(Arg1)

 all_distinct(Arg1)

 tuples_in(Arg1, Arg2)

 labeling(Arg1, Arg2)

 label(Arg1)

 lex_chain(Arg1)

 serialized(Arg1, Arg2)

 global_cardinality(Arg1, Arg2)

 global_cardinality(Arg1, Arg2, Arg3)

 circuit(Arg1)

 cumulative(Arg1)

 cumulative(Arg1, Arg2)

 disjoint2(Arg1)

 element(Arg1, Arg2, Arg3)

 automaton(Arg1, Arg2, Arg3)

 transpose(Arg1, Arg2)

 chain(Arg1, Arg2)

 float_sum(Arg1, Arg2, Arg3)

 float_product(Arg1, Arg2, Arg3)

 {=}(Arg1, Arg2)

 {>=}(Arg1, Arg2)

 {>}(Arg1, Arg2)

 {<}(Arg1, Arg2)

 {=<}(Arg1, Arg2)

 {=\=}(Arg1, Arg2)

 {Arg1}

 entailed(Arg1)

 maximize(Arg1)

 minimize(Arg1)

 inf(Arg1, Arg2)

 sup(Arg1, Arg2)

 bb_inf(Arg1, Arg2, Arg3)

 bb_inf(Arg1, Arg2, Arg3, Arg4, Arg5)

 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)