From 0bca5b8291cd34b4a77b04e5ced7dba76ae3219a Mon Sep 17 00:00:00 2001 From: Hennie de Villiers Date: Mon, 25 Feb 2013 13:13:27 +0200 Subject: [PATCH] Fix for +-rule-down 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. --- screamer.lisp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/screamer.lisp b/screamer.lisp index 3e86f65..35a209b 100644 --- a/screamer.lisp +++ b/screamer.lisp @@ -4205,13 +4205,17 @@ Otherwise returns the value of X." (fail)))) (defun +-rule-down (z x y) + ;; ORIGINAL COMMENT ;; 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. - (if (and (variable-integer? z) (or (variable-real? x) (variable-real? y))) + ;; FIX: 2013/02/25 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 either X or Y + ;; is an integer + (if (and (variable-integer? z) (or (variable-integer? x) (variable-integer? y))) ; Original: (or (variable-real? x) (variable-real? y))) (restrict-integer! x)) ;; note: Ditto. (if (and (variable-real? z) (or (variable-real? x) (variable-real? y)))