Fix for +-rule-down

[hacdevilliers]

Argument presented in the source code was
;; note: We can't assert that X and Y are integers when Z is an integer since
;; Z may be an integer when X and Y are Gaussian integers. But we can
;; make such an assertion if either X or Y is real. If the Screamer
;; type system could distinguish Gaussian integers from other complex
;; numbers we could make such an assertion whenever either X or Y was
;; not a Gaussian integer.
The argument above must surely be incorrect. If Z is an integer, and Y is a real
say 2.5 then X will surely not be an integer. The argument does work if eithe
r X or Y are integers. So changed things so that Z being an integer and X OR Y being an INTEGER means that X AND Y are both integers. (Note the assertion is only for X, but this is correct given that the assertion for Y happens in another call to this rule.

[hacdevilliers]

This is just the text of the original issue that I opened (sorry about the duplication, haven't used github for this sort of thing before)

function -v erroneously restricts arguments to integers in certain cases

I'm a bit too busy to delve into this issue more deeply at the moment (maybe I'll poke at the screamer sources later, haven't really had a look at them before), but

(-v (a-real-betweenv 1.1 1.2))

emits an error. (This form distils the issue I had in much more complicated code) Mysteriously, the real variable created by a-real-between-v has been restricted to be an integer, causing the exception later on. Further investigation reveals

(-v 0 (a-real-betweenv 1.1 1.2))

has the same issue, but the following works correctly

(-v 0.0 (a-real-betweenv 1.1 1.2))

This can be used as a workaround for anyone similarly affected.

In the case of +v, there is seemingly no such problem.

(+v (a-real-betweenv 1.1 1.2))
(+v 0 (a-real-betweenv 1.1 1.2))
(+v 0.0 (a-real-betweenv 1.1 1.2))

all work correctly. Perhaps this means a fix may be relatively simple?

(Note: I'm using the quicklisp screamer-20111105-git distro in case this matters)

[nikodemus]

A test case that demonstrates the problem would appreciated. (In tests.lisp)

[PHRaposo]

I'm experiencing some problems with restrictions to integers/non-integers with functions /v and *v.

Here are some examples:

;; This erroneusly restricts Z to be an integer.

(let* ((x (an-integer-betweenv 1 10))
       (y (an-integer-betweenv 1 10))
       (z (/v x y)))
 (all-values (solution (list x y z) (static-ordering #'linear-force))))
;;((1 1 1) (2 1 2) (2 2 1) (3 1 3) (3 3 1) (4 1 4) (4 2 2) (4 4 1) (5 1 5) (5 5 1) (6 1 6) (6 2 3) (6 3 2) (6 6 1) (7 1 7) (7 7 1) (8 1 8) (8 2 4) (8 4 2) (8 8 1) (9 1 9) (9 3 3) (9 9 1) (10 1 10) (10 2 5) (10 5 2) (10 10 1))

Another problem is when integer variables have the lower bound 0:

(let* ((x (an-integer-betweenv 0 10))
        (y (an-integer-betweenv 0 10))
	(z (/v x y)))
 (all-values (solution (list x y z) (static-ordering #'linear-force))))
;; This runs forever...

I believe there is a problem with /-rule, which does not include a condition when the lower bound or the upper bound is equal zero.

There is a similar problem with ratios (the multiplication of the non-integer variables X and Y restricts Z to be a non-integer):

(let* ((x (a-member-ofv '(2/3 3/2)))
         (y (a-member-ofv '(2/3 3/2)))
         (z (*v x y)))
 (assert! (integerpv z)) 
 ;fails
 (all-values (solution (list x y z) (static-ordering #'linear-force))))

;; This works: 

(let* ((x (a-member-ofv '(2/3 3/2)))
        (y (a-member-ofv '(2/3 3/2)))
        (z (*v x y)))
  (assert! (=v (an-integerv) z))
 (all-values (solution (list x y z) (reorder #'domain-size #'(lambda (x) (< x 1e-6)) #'> #'linear-force))))
;;((3/2 2/3 [34 noninteger-real 1:2]) (2/3 3/2 [34 noninteger-real 1:2]))

The lower-bound and upper-bound of Z are the same:

 (let* ((x (a-member-ofv '(2/3 3/2)))
        (y (a-member-ofv '(2/3 3/2)))
        (z (*v x y)))
  (assert! (=v (an-integerv) z))
 (all-values
 (mapcar #'(lambda (el)
                   (if (bound? el)
                        el
                        (list (variable-lower-bound el) (variable-upper-bound el))))
 (solution (list x y z) (reorder #'domain-size #'(lambda (x) (< x 1e-6)) #'> #'linear-force)))))
;;((3/2 2/3 (1 1)) (2/3 3/2 (1 1)))

Maybe it would be necessary to revise all the rules (+-rule-up, +-rule-down, /-rule, *-rule-up, *-rule-down) and also the functions +v2, -v2, *v2 and /v2, but it seems to be not an easy task.

I'm also wondering if would be possible to include a distinction between integers and ratios (rational) and floats variables.

Any ideas?

[swapneils]

Any ideas?

Addressed here

Separately, for posterity, the above logic is wrong in general, even in the modified case this PR proposes. Even when Z and Y are both integers, multiplication of ratios can reduce to integers, so X might be some fraction whose denominator is a factor of Y (e.g. 1 = 2 * 1/2, as in the above-quoted comment).

The "right answer" here is to track Gaussian integers, as the original comment states; ratios naturally convert to such, so the primary blocker seems to be converting integer floats into integers. Would have to investigate to find all the fiddly bits that need to be fixed to allow this.

Alternatively, swapneils#9 would fix this automatically, along with some other issues in Screamer's current variable-type system.