Strange results from assume (maybe a bug?) ad asksign
Subject: Strange results from assume (maybe a bug?) ad asksign
From: Alexey Beshenov
Date: Sun, 28 Dec 2008 00:22:19 +0300
On Saturday 27 December 2008 23:24:26 Stavros Macrakis wrote:
> > "assume(x>a and x<b)" will just make "is(x>y)" return "true" for
> > y<=a, return "false" for y>=b, and return "unknown" otherwise
> > (I'm not sure it was intended). I guess now there is no way to
> > declare bounds for a variable correctly through the "assume"
> > mechanism.
>
> I'm not sure I understand what the problem is here. What would you
> expect is(x>y) to return if y is not <= a or >= b?
I think that "unknown" is okay, and it seems that it's the intended
return value, but the original question assumes that it should be
"true".
--
Sweetmorn, Aftermath 69 YOLD 3174
Alexey Beshenov http://beshenov.ru/