Feature: general CLP(Z) reification predicate

[librarianmage]

(aside: is it better to open CLP(Z) requests here or at triska/clpz? I see CLP(Z)-specific issues here, so I assume it’s okay to open them here)

library(clpz) currently offers #=/3 and #</3 to reify those constraints for use with library(reif). It would be nice to have a predicate that works with all of the reifiable predicates, say clpz_t/2 or #<==>/3.

[triska]

Yes, it's definitely OK to report and discuss CLP(Z) issues here, there were already several Scryer contributors who helped tremendously with issues and features of this library!

[triska]

@librarianmage: Regarding the different ways to provide this feature (i.e., one dedicated predicate for each arithmetic comparison, or one more general predicate, or another design variant), do you have any personal preference or recommendation? I would greatly appreciate your input on how to best make this logic available, and also if you could maybe share a few interesting applications and how the eventual code would look with each variant! Thank you a lot!

[librarianmage]

@triska In https://github.com/mthom/scryer-prolog/discussions/2193#discussioncomment-7740411, you mentioned how I could reuse (#=)/3 instead of my self-defined clpz_reif/2 predicate using #=(#X, 1, T), but that feels less nice because the false choice has clpz:(X in inf..0\/2..sup) instead of X = 0.

My personal preference is a clpz_t/2 where the first argument is a CLP(Z) expression and the second is the equivalent value for use in library(reif). Patterning off of what is already there, it could look something like

/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   Reified predicates for use with predicates from library(reif).
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */

clpz_t(X, T) :-
        X #<==> #B,
        zo_t(B, T).

#=(X, Y, T) :- clpz_t(X #= Y, T).

#<(X, Y, T) :- clpz_t(X #< Y, T).

zo_t(0, false).
zo_t(1, true).

This would allow one to write their own CLP(Z) reifiable predicates as needed pretty quickly.

[triska]

@librarianmage: Thank you a lot, that's also my favourite variant! Do you think it's possible to find a better name for it? I like the _t at the end, but what about clpz_ ?

[librarianmage]

@triska I'm struggling to come up with a suggestion that is sufficiently broad yet narrow enough to encompass "reifiable CLP(Z) expressions"

[dcnorris]

I see clpz_t/2 takes an Expr argument:

clpz_t(Expr, T) :-
        Expr #<==> #B,
        zo_t(B, T).

I find I cannot use a regular predicate in this first position, as one might like to do e.g. to avoid duplicated code:

:- use_module(library(clpz)).
:- initialization(assertz(clpz:monotonic)).

:- op(900, xfx, &=<).
&=<(T1/N1, T2/N2) :- #T1 #>= #T2 #/\ (#N1-T1) #=< (#N2-T2).

&=<(T1/N1, T2/N2, Truth) :-
%    clpz_t(#T1 #>= #T2 #/\ (#N1-T1) #=< (#N2-T2), Truth). % works fine, as below (*)
    clpz_t(&=<(T1/N1, T2/N2), Truth). % attempt to avoid duplicated code fails (**)

/*
?- &=<(3/4, 2/3).
%@    true.
?- 3/4 &=< 2/3.
%@    true.
?- &=<(3/4, 2/3, T).
%@    error(domain_error(clpz_reifiable_expression,3/4&=<2/3),unknown(3/4&=<2/3)-1). (**)
%@    T = true. % (*)
*/

Is this a necessary limitation, because library(clpz) cannot look into (&=<)/2 to see the expression inside?

---

It occurs to me on further thought that one might avoid duplicated code by defining the reified version as primary, then the 'regular' version as the special case where Truth = true.

[triska]

Yes, you cannot use a user-defined predicate as the first argument which must be a reifiable arithmetic expression. However, if you want to shorten code, you can easily define relations between abbreviations and such reifiable expressions.

For example, with:

expr(T1/N1, T2/N2, #T1 #>= #T2 #/\ (#N1-T1) #=< (#N2-T2)).

&=<(A, B) :- &=<(A, B, true).

&=<(T1/N1, T2/N2, Truth) :-
    expr(T1/N1, T2/N2, Expr),
    clpz_t(Expr, Truth).

We get:

?- &=<(3/4, 2/3).
   true.
?- 3/4 &=< 2/3.
   true.
?- &=<(3/4, 2/3, T).
   T = true.

expr/3 is not a good name for such a relation, I leave finding a better name as a challenge.