mthom
Implementation improvements to clpz_t/2
I am filing this issue so that the comment posted in https://github.com/mthom/scryer-prolog/pull/2319#issuecomment-1930515351 is properly remembered and addressed:
Is there a better implementation of clpz_t/2? Currently, reification is internally used in order to benefit from argument indexing and hence make the test deterministic if possible. Reification clearly has an overhead compared to "backtracking out" the cases, which also has an overhead in the form of redundant choice-points that may be left on the local stack.
Since the construct itself is sensible, it is a good candidate for implementation improvements. For example, could goal expansion be applied, similar to what (#=)/2 and other arithmetic comparisons already do? The pattern if_(.... clpz_t(....)), ..., ...) could be expanded to more efficient versions that take into account the concrete arithmetic term that occurs in the first argument of clpz_t/2, even if it occurs within a lambda expression as show in #2320.
I would greatly appreciate all insights and suggestions. Thank you a lot!
Both reif and clpz have a logical conjunction operator. Is there supposed to be a semantic difference between these two expressions?
if_(clpz_t(#A #/\ #B), write('t '), write('f ')).
# f clpz:(A in 0..1), clpz:(#A#/\ #B#<==>0), clpz:(B in 0..1)
# ; t A = 1, B = 1.
versus:
if_((clpz_t(#A),clpz_t(#B)), write('t '), write('f ')).
# f A = 0
# ; f A = 1, B = 0
# ; t A = 1, B = 1.
Which is more desirable - the residual goal or the additional choice-points?
