On Thursday, 7 August 2014 at 03:51:02 UTC, Ola Fosheim Grøstad
wrote:
On Wednesday, 6 August 2014 at 21:33:35 UTC, Timon Gehr wrote:
On 08/06/2014 11:18 PM, Matthias Bentrup wrote:
Ah, I had a different understanding of assume, i.e. placing an
assume(A) at some point in code adds not the axiom A, but
rather
the axiom "control flow reaches this spot => A".
(Your understanding is the conventional one.)
Not right.
You need to take into account that assume() provides a
mathematical definition, it isn't an imperative. That would
make no sense. So there is no control flow, only mathematical
dependencies.
But control flow can introduce mathematical dependencies. E.g.
for assert the code
if(a) {
assert(b);
...
}
is not equivalent to
assert(b);
if(a) {
...
}
but not because the assertion depends on a different incarnation
of "b", but because it also depends on "a", so it is like
assert(!a || b);
if(a) {
...
}
If assume is independent of control flow, then clearly this
cannot be related to assert. But I think the proposal was not to
replace assert with the textbook definition of assume, rather to
use the information in asserts to optimize the code. So if assume
doesn't work, what about assume_here() ?
