Module Clpfd

Jan Burse, created Oct 25. 2018
/**
* As a convenience the finite domain solver provides a couple of
* comparisons between integers. The following features are provided
* in connection with integer comparison:
*
* * Constraint Factoring
* * Global Constraints
*
* Our finite domain solver is probably unique in that it allows posting
* element hood for arbitrary expressions. This feature is used to
* internally implement integer comparison. We find the usual comparisons
* such as #\=/2, #/2, #==/2. Comparisons are
* reconstructed from element hood when displaying constraints.
*
* Example:
* ?- Y - X in 0..sup.
* X #=< Y
*
* The constraint solver also attempts to combine element hood constraints.
* Element hood constraints over the same expression are intersected
* similarly to domain constraints. Consequently comparisons can be
* contracted, subsumed or conflict. Also interaction with equations is
* possible, which are then treated as singleton element hood constraints.
*
* Example:
* ?- X #> Y, X #= Y.
* No
*
* The integer comparisons can be used to define more complex conditions.
* A recurring problem is stating the inequality of a couple of value
* expressions. The predicate all_different/2 has been defined as a
* corresponding convenience.
*
* Warranty & Liability
* To the extent permitted by applicable law and unless explicitly
* otherwise agreed upon, XLOG Technologies GmbH makes no warranties
* regarding the provided information. XLOG Technologies GmbH assumes
* no liability that any problems might be solved with the information
* provided by XLOG Technologies GmbH.
*
* Rights & License
* All industrial property rights regarding the information - copyright
* and patent rights in particular - are the sole property of XLOG
* Technologies GmbH. If the company was not the originator of some
* excerpts, XLOG Technologies GmbH has at least obtained the right to
* reproduce, change and translate the information.
*
* Reproduction is restricted to the whole unaltered document. Reproduction
* of the information is only allowed for non-commercial uses. Selling,
* giving away or letting of the execution of the library is prohibited.
* The library can be distributed as part of your applications and libraries
* for execution provided this comment remains unchanged.
*
* Restrictions
* Only to be distributed with programs that add significant and primary
* functionality to the library. Not to be distributed with additional
* software intended to replace any components of the library.
*
* Trademarks
* Jekejeke is a registered trademark of XLOG Technologies GmbH.
*/
% :- package(library(ordered)).
:- package(library(jekmin/reference/finite)).
:- use_package(library(jekmin/reference/minimal)).
:- use_package(library(jekpro/frequent/misc)).
:- module(clpfd, []).
:- use_module(library(basic/lists)).
:- use_module(library(minimal/assume)).
:- use_module(library(minimal/delta)).
:- use_module(library(misc/struc)).
:- use_module(library(misc/elem)).
:- use_module(library(experiment/surrogate)).
:- use_module(library(experiment/trail)).
:- use_module(library(experiment/attr)).
:- use_module(helper).
:- reexport(linform).
:- reexport(intset).
:- reexport(reify).
:- reexport(enum).
% sys_in(+Wrap, +Set, +Bound)
% sys_in(X,S,_) = X in S
:- multifile intset:sys_in/3.
:- thread_local intset:sys_in/3.
:- multifile intset:sys_in/4.
/**********************************************************/
/* Multiplication Constraints */
/**********************************************************/
% sys_hook_mul(+Var, +Term)
:- private sys_hook_mul/2.
var(W), !,
throw(error(type_error(integer,T),_)).
% sys_var_mul(+Wrap, +Wrap)
% sys_var_mul(X, Y) = X = Y
:- private sys_var_mul/2.
:- thread_local sys_var_mul/2.
:- private sys_var_mul/3.
/* Union Find */
% sys_const_mul(+Wrap, +Integer)
% sys_const_mul(X, C) = X = C
:- private sys_const_mul/2.
:- thread_local sys_const_mul/2.
:- private sys_const_mul/3.
/* Constant Elimination */
% sys_mulv(+Wrap, +Wrap, +Warp)
% sys_mulv(X, Y, Z), X*Y = Z
% sys_mulv_ord(+Wrap, +Wrap, +Wrap)
% sys_mulv_ord(X, Y, Z), X*Y = Z, X @< Y
:- multifile sys_mulv_ord/3.
:- thread_local sys_mulv_ord/3.
:- private sys_mulv_ord/4.
/* Special Case */
post(sys_sqrv(X, Y))
<= phaseout_posted(sys_mulv(X, X, Y)), !.
post(sys_impv(X, Y))
<= phaseout_posted(sys_mulv(X, Y, X)), !.
post(sys_impv(X, Y))
<= phaseout_posted(sys_mulv(Y, X, X)), !.
/* Order Arguments */
post(sys_mulv_ord(X, Y, Z))
<= phaseout_posted(sys_mulv(X, Y, Z)),
X @< Y, !.
post(sys_mulv_ord(X, Y, Z))
<= phaseout_posted(sys_mulv(Y, X, Z)).
/* Mul & Mul Intersection */
sys_mulv_ord(X, Y, T), !.
sys_mulc_ord(X, Y, C), !.
/* Union Find */
post(sys_mulv(T, Y, Z))
var(H), !,
post(sys_mulv(X, T, Z))
var(H), !,
post(sys_mulv(X, Y, T))
var(H), !,
/* Constant Elimination */
post(sys_lin(L, 0))
sys_make_prod(C, Y, [], H),
sys_add_prod(H, [-1*Z], L).
post(sys_lin(L, 0))
sys_make_prod(C, X, [], H),
sys_add_prod(H, [-1*Z], L).
post(sys_mulc_ord(X, Y, C))
integer(C), !.
/* Hook Adding */
sys_melt_hook(X, sys_hook_mul),
sys_melt_hook(Y, sys_hook_mul),
sys_melt_hook(Z, sys_hook_mul)
/* Set Diffusion, Directed, Bounds */
post(intset:sys_in(Z, [S], S))
Z @> Y, !,
S \== ... .
post(intset:sys_in(Y, L, S))
( sys_slash_range(R, T, S)
-> S \== ...,
L = [S]
; L = [],
S = ...).
/* Variable Rename */
post(sys_mulv(T, Y, Z))
post(sys_mulv(X, T, Z))
Y \== X.
post(sys_mulv(X, Y, T))
Z \== X,
Z \== Y.
/* Constant Backpropagation */
post(sys_lin(L, 0))
sys_make_prod(C, Y, [], H),
sys_add_prod(H, [-1*Z], L).
post(sys_lin(L, 0))
Y \== X,
sys_make_prod(C, X, [], H),
sys_add_prod(H, [-1*Z], L).
post(sys_mulc_ord(X, Y, C))
Z \== X,
Z \== Y.
/* Set Update, Directed, Bounds */
post(intset:sys_in(Z, [S], S))
<= posted(intset:sys_in(X, _, R)),
R \== ...,
sys_mulv_ord(X, Y, Z),
Z @> Y,
S \== ... .
post(intset:sys_in(Z, [S], S))
<= posted(intset:sys_in(Y, _, R)),
R \== ...,
sys_mulv_ord(X, Y, Z),
Z @> Y,
S \== ... .
post(intset:sys_in(Y, L, S))
<= posted(intset:sys_in(Z, _, R)),
R \== ...,
sys_mulv_ord(X, Y, Z),
Z @=< Y,
( sys_slash_range(R, T, S)
-> S \== ...,
L = [S]
; L = [],
S = ...).
post(intset:sys_in(Y, L, S))
<= posted(intset:sys_in(X, _, R)),
sys_mulv_ord(X, Y, Z),
Z @=< Y,
( sys_slash_range(T, R, S)
-> S \== ...,
L = [S]
; L = [],
S = ...).
% sys_mulc(+Wrap, +Wrap, +Integer)
% sys_mulc(X,Y,C), X*Y = C
% sys_mulc_ord(+Wrap, +Wrap, +Integer)
% sys_mulc_ord(X,Y,C), X*Y = C, X @< Y
:- private sys_mulc_ord/3.
:- thread_local sys_mulc_ord/3.
:- private sys_mulc_ord/4.
/* Special Case */
post(sys_sqrc(X, C))
<= phaseout_posted(sys_mulc(X, X, C)), !.
/* Order Arguments */
post(sys_mulc_ord(X, Y, C))
<= phaseout_posted(sys_mulc(X, Y, C)),
X @< Y, !.
post(sys_mulc_ord(X, Y, C))
<= phaseout_posted(sys_mulc(Y, X, C)).
/* Mul & Mul Intersection */
sys_mulv_ord(X, Y, T), !.
sys_mulc_ord(X, Y, D),
C \== D, !.
sys_mulc_ord(X, Y, C), !.
/* Union Find */
post(sys_mulc(Z, Y, C))
var(H), !,
post(sys_mulc(X, Z, C))
var(H), !,
/* Constant Elimination */
post(sys_lin(L, C))
sys_make_prod(D, Y, [], L).
post(sys_lin(L, C))
sys_make_prod(D, X, [], L).
/* Hook Adding */
sys_melt_hook(X, sys_hook_mul),
sys_melt_hook(Y, sys_hook_mul)
/* Set Diffusion, Directed, Bounds */
post(intset:sys_in(Y, L, S))
( sys_slash_range(C, R, S)
-> S \== ...,
L = [S]
; L = [],
S = ...).
/* Variable Rename */
post(sys_mulc(Z, Y, C))
post(sys_mulc(X, Z, C))
Y \== X.
/* Constant Backpropagation */
post(sys_lin(L, C))
sys_make_prod(S, Y, [], L).
post(sys_lin(L, C))
Y \== X,
sys_make_prod(S, X, [], L).
/* Set Update, Directed, Bounds */
post(intset:sys_in(Y, L, S))
<= posted(intset:sys_in(X, _, R)),
sys_mulc_ord(X, Y, C),
( sys_slash_range(C, R, S)
-> S \== ...,
L = [S]
; L = [],
S = ...).
% residue:sys_current_eq(+Var, -Handle)
:- public residue:sys_current_eq/2.
:- multifile residue:sys_current_eq/2.
:- discontiguous residue:sys_current_eq/2.
residue:sys_current_eq(V, mulv(X,Y,Z)) :-
sys_mulv_ord(X, Y, Z).
residue:sys_current_eq(V, mulv(X,Y,Z)) :-
sys_mulv_ord(X, Y, Z).
residue:sys_current_eq(V, mulv(X,Y,Z)) :-
sys_mulv_ord(X, Y, Z).
residue:sys_current_eq(V, mulc(X,Y,C)) :-
sys_mulc_ord(X, Y, C).
residue:sys_current_eq(V, mulc(X,Y,C)) :-
sys_mulc_ord(X, Y, C).
% residue:sys_unwrap_eq(+Handle, -Goals, +Goals)
:- public residue:sys_unwrap_eq/3.
:- multifile residue:sys_unwrap_eq/3.
:- discontiguous residue:sys_unwrap_eq/3.
residue:sys_unwrap_eq(mulv(X,Y,Z), [C#=A*B|L], L) :-
Z @> Y, !,
sys_melt_var(Z, C).
residue:sys_unwrap_eq(mulv(X,Y,Z), [A*B#=C|L], L) :-
sys_melt_var(Z, C).
residue:sys_unwrap_eq(mulc(X,Y,C), [C#=A*B|L], L) :-
sys_melt_var(Y, B).
/**********************************************************/
/* Special Cases Constraints */
/**********************************************************/
% sys_hook_spez(+Var, +Term)
:- private sys_hook_spez/2.
var(W), !,
throw(error(type_error(integer,T),_)).
% sys_var_spez(+Wrap, +Wrap)
% sys_var_spez(X, Y) = X = Y
:- private sys_var_spez/2.
:- thread_local sys_var_spez/2.
:- private sys_var_spez/3.
/* Union Find */
% sys_const_spez(+Wrap, +Integer)
% sys_const_spez(X, C) = X = C
:- private sys_const_spez/2.
:- thread_local sys_const_spez/2.
:- private sys_const_spez/3.
/* Constant Elimination */
% sys_sqrv(+Wrap, +Wrap)
% sys_sqrv(X,Y), X*X = Y
:- private sys_sqrv/2.
:- thread_local sys_sqrv/2.
:- private sys_sqrv/3.
/* Special Case */
post(intset:sys_in(X, [0..1], 0..1))
/* Sqr & Sqr Intersection */
sys_sqrv(X, T), !.
/* Union Find */
post(sys_sqrv(T, Y))
var(H), !,
post(sys_sqrv(X, T))
var(H), !,
/* Constant Elimination */
D is C*C.
post(sys_sqrc(X, C))
integer(C), !.
/* Hook Adding */
sys_melt_hook(X, sys_hook_spez),
sys_melt_hook(Y, sys_hook_spez)
/* Set Diffusion, Directed, Bounds */
post(intset:sys_in(X, L, S))
X @>= Y, !,
-> S \== ...,
L = [S]
; L = [],
S = ...).
post(intset:sys_in(Y, [S], S))
/* Variable Rename */
post(sys_sqrv(T, Y))
post(sys_sqrv(X, T))
Y \== X.
/* Constant Backpropagation */
D is C*C.
post(sys_sqrc(X, C))
Y \== X.
/* Set Update, Directed, Bounds */
post(intset:sys_in(X, L, S))
<= posted(intset:sys_in(Y, _, R)),
R \== ...,
sys_sqrv(X, Y),
X @>= Y,
-> S \== ...,
L = [S]
; L = [],
S = ...).
post(intset:sys_in(Y, [S], S))
<= posted(intset:sys_in(X, _, R)),
sys_sqrv(X, Y),
X @< Y,
% sys_sqrc(+Wrap, +Integer)
% sys_sqrc(X,C), X*X = C
:- private sys_sqrc/2.
:- thread_local sys_sqrc/2.
:- private sys_sqrc/3.
% Special Case
C < 0, !.
post(intset:sys_in(X, [H,D], H..D))
sqrtrem(C, D, R),
R =:= 0,
H is -D, !.
% sys_impv(+Wrap, +Wrap)
% sys_impv(X,Y), X*Y = X
:- private sys_impv/2.
:- thread_local sys_impv/2.
:- private sys_impv/3.
/* Special Case */
post(intset:sys_in(X, [0..1], 0..1))
/* Union Find */
post(sys_impv(T, Y))
var(H), !,
post(sys_impv(X, T))
var(H), !,
/* Constant Elimination */
post(sys_lin(L, C))
sys_make_prod(C, Y, [], L).
post(sys_lin(L, 0))
D is C-1,
sys_make_prod(D, X, [], L).
/* Hook Adding */
sys_melt_hook(X, sys_hook_spez),
sys_melt_hook(Y, sys_hook_spez)
/* Set Diffusion, Directed, Bounds */
post(intset:sys_in(X, [S], S))
X @>= Y, !,
S \== ... .
post(intset:sys_in(Y, [S], S))
S \== ... .
/* Variable Rename */
post(sys_impv(T, Y))
post(sys_impv(X, T))
Y \== X.
/* Constant Backpropagation */
post(sys_lin(L, C))
sys_make_prod(C, Y, [], L).
post(sys_lin(L, 0))
Y \== X,
D is C-1,
sys_make_prod(D, X, [], L).
/* Set Update, Directed, Bounds */
post(intset:sys_in(X, [S], S))
<= posted(intset:sys_in(Y, _, R)),
R \== ...,
sys_impv(X, Y),
X @>= Y,
S \== ... .
post(intset:sys_in(Y, [S], S))
<= posted(intset:sys_in(X, _, R)),
R \== ...,
sys_impv(X, Y),
X @< Y,
S \== ... .
% residue:sys_current_eq(+Var, -Goal)
residue:sys_current_eq(V, sqrv(X,Y)) :-
sys_sqrv(X, Y).
residue:sys_current_eq(V, sqrv(X,Y)) :-
sys_sqrv(X, Y).
residue:sys_current_eq(V, impv(X,Y)) :-
sys_impv(X, Y).
residue:sys_current_eq(V, impv(X,Y)) :-
sys_impv(X, Y).
% residue:sys_unwrap_eq(+Goal, -Goal)
residue:sys_unwrap_eq(sqrv(X,Y), [A*A#=B|L], L) :-
X @>= Y, !,
sys_melt_var(Y, B).
residue:sys_unwrap_eq(sqrv(X,Y), [B#=A*A|L], L) :-
sys_melt_var(Y, B).
residue:sys_unwrap_eq(impv(X,Y), [A#=B*A|L], L) :-
X @>= Y, !,
sys_melt_var(Y, B).
residue:sys_unwrap_eq(impv(X,Y), [A#=A*B|L], L) :-
sys_melt_var(Y, B).
/**********************************************************/
/* Absolute Constraints */
/**********************************************************/
% sys_hook_abs(+Var, +Term)
:- private sys_hook_abs/2.
var(W), !,
throw(error(type_error(integer,T),_)).
% sys_var_abs(+Wrap, +Wrap)
% sys_var_abs(X, Y) = X = Y
:- private sys_var_abs/2.
:- thread_local sys_var_abs/2.
:- private sys_var_abs/3.
/* Union Find */
% sys_const_abs(+Wrap, +Integer)
% sys_const_abs(X, C) = X = C
:- private sys_const_abs/2.
:- thread_local sys_const_abs/2.
:- private sys_const_abs/3.
/* Constant Elimination */
% sys_absv(+Wrap, +Wrap)
% sys_absv(X,Y), abs(X) = Y
:- multifile sys_absv/2.
:- thread_local sys_absv/2.
/* Special Case */
post(intset:sys_in(X, [0...], 0...))
/* Abs & Abs Intersection */
sys_absv(X, T), !.
/* Union Find */
post(sys_absv(T, Y))
var(H), !,
post(sys_absv(X, T))
var(H), !,
/* Constant Elimination */
D is abs(C).
post(sys_absc(X, C))
integer(C), !.
/* Hook Adding */
sys_melt_hook(X, sys_hook_abs),
sys_melt_hook(Y, sys_hook_abs)
/* Set Diffusion, Directed, Bounds */
post(intset:sys_in(X, L, S))
X @>= Y, !,
-> S \== ...,
L = [S]
; L = [],
S = ...).
post(intset:sys_in(Y, [S], S))
/* Variable Rename */
post(sys_absv(T, Y))
post(sys_absv(X, T))
Y \== X.
/* Constant Backpropagation */
D is abs(C).
post(sys_absc(X, C))
Y \== X.
/* Set Update, Directed, Bounds */
post(intset:sys_in(X, L, S))
<= posted(intset:sys_in(Y, _, R)),
R \== ...,
sys_absv(X, Y),
X @>= Y,
-> S \== ...,
L = [S]
; L = [],
S = ...).
post(intset:sys_in(Y, [S], S))
<= posted(intset:sys_in(X, _, R)),
sys_absv(X, Y),
X @< Y,
% sys_absc(+Wrap, +Integer)
% sys_absc(X,C), abs(X) = C
:- private sys_absc/2.
:- thread_local sys_absc/2.
:- private sys_absc/3.
% Special Case
C < 0, !.
post(intset:sys_in(X, [H,C], H..C))
H is -C.
% residue:sys_current_eq(+Var, -Goal)
residue:sys_current_eq(V, absv(X,Y)) :-
sys_absv(X, Y).
residue:sys_current_eq(V, absv(X,Y)) :-
sys_absv(X, Y).
% residue:sys_unwrap_eq(+Goal, -Goal)
residue:sys_unwrap_eq(absv(X,Y), [abs(A)#=B|L], L) :-
X @>= Y, !,
sys_melt_var(Y, B).
residue:sys_unwrap_eq(absv(X,Y), [B#=abs(A)|L], L) :-
sys_melt_var(Y, B).

Comments