`an-integer-abovev` and `funcallv` do not work well together under `:gfc`

[kisp]

Note: screamer:*strategy* is set to its default value of :gfc here.

The following solution is incorrect:

SCREAMER-USER> (let ((x (an-integer-abovev 1)))
                 (assert! (funcallv #'evenp x))
                 (one-value (solution x (static-ordering #'linear-force))))
1

This returns 1, which is unexpected.

However, using an-integer-betweenv, we get the expected result:

SCREAMER-USER> (let ((x (an-integer-betweenv 1 10)))
                 (assert! (funcallv #'evenp x))
                 (one-value (solution x (static-ordering #'linear-force))))
2

To investigate further, I traced evenp:

SCREAMER-USER> (trace evenp)
(EVENP)
SCREAMER-USER> (let ((x (an-integer-betweenv 1 10)))
                 (assert! (funcallv #'evenp x))
                 (one-value (solution x (static-ordering #'linear-force))))
  0: (EVENP 1)
  0: EVENP returned NIL
  0: (EVENP 2)
  0: EVENP returned T
  0: (EVENP 3)
  0: EVENP returned NIL
  0: (EVENP 4)
  0: EVENP returned T
  0: (EVENP 5)
  0: EVENP returned NIL
  0: (EVENP 6)
  0: EVENP returned T
  0: (EVENP 7)
  0: EVENP returned NIL
  0: (EVENP 8)
  0: EVENP returned T
  0: (EVENP 9)
  0: EVENP returned NIL
  0: (EVENP 10)
  0: EVENP returned T
2

With an-integer-betweenv, evenp is correctly called multiple times.

However, when using an-integer-abovev, evenp is never called:

SCREAMER-USER> (let ((x (an-integer-abovev 1)))
                 (assert! (funcallv #'evenp x))
                 (one-value (solution x (static-ordering #'linear-force))))
1
SCREAMER-USER> 

It seems that funcallv does not properly constrain x when using an-integer-abovev.

The funcallv docstring states:

Additionally, if all but one of V and the argument variables become known, and
the remaining variable has a finite domain, then that domain is further
restricted to be consistent with other arguments.

This explains why, in the case of an-integer-betweenv, the domain is fully pruned by funcallv. Since an-integer-abovev has an infinite domain, this kind of pruning is not possible.

It seems that the funcallv constraint needs to be delayed - but this is not happening.

[kisp]

SCREAMER-USER> (setq *strategy* :ac)
:AC
SCREAMER-USER> (let ((x (an-integer-abovev 1)))
                 (assert! (funcallv #'evenp x))
                 (one-value (solution x (static-ordering #'linear-force))))
  0: (EVENP 1)
  0: EVENP returned NIL
  0: (EVENP 2)
  0: EVENP returned T
2

[PHRaposo]

I believe the issue lies is in Screamer's propagation mechanism, since both :gfc and :ac propagate values when the variable has a finite domain, as you noted.

To work around this limitation, it is possible to use screamer::assert!-true or screamer::assert!-false directly, which works with both :ac and :gfc:

(let ((*strategy* :ac) 
       (x (an-integer-abovev 1)))
     (screamer::assert!-true (funcallv #'evenp x))
     (one-value (solution x (static-ordering #'linear-force))))
;2

(let ((x (an-integer-abovev 1)))
     (screamer::assert!-true (funcallv #'evenp x))
     (one-value (solution x (static-ordering #'linear-force))))
;2 

It is also possible to create the functions evenpv or oddpv:

(defun evenpv (x)
    (assert! (realpv x))
    (let ((z (funcallv #'evenp x)))
        z))

(defun oddpv (x)
    (assert! (realpv x))
    (let ((z (funcallv #'oddp x)))
        z))

(let ((x (an-integer-abovev 1)))
    (assert! (evenpv x))
    (one-value (solution x (static-ordering #'linear-force))))
;2

(let ((x (an-integer-abovev 1)))
    (assert! (oddpv x))
    (one-value (solution x (static-ordering #'linear-force))))
;1

Since the variable Z will always be created using funcallv or applyv outside the context of assert!, this ensures that noticers are correctly attached to the variables.