Skip to content
Snippets Groups Projects
Commit d6245ae1 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Fixes the evaluation engine when a domain oracle returns Bottom.

When the evaluation of any subexpression leads to Bottom, the evaluation of the
complete expression returns only Bottom with no valuation: thus the valuation
cache is no longer updated.

However, when the evaluation of another expression requested by a domain through
the oracle leads to Bottom, the evaluation of the primary expression may
continue without leading to Bottom (domains are allowed to request the evaluation
of 1/0 at any time, after all).

In this case, we should properly update the cached valuation by binding Bottom
to the expression requested by the domain, in case it should be used again in
the evaluation (for instance if the requested evaluation was a subexpression of
the primary target of the evaluation).

And especially, if subdivided evaluations are enabled, the reference to the
cached valuation must _always_ be reset after the oracle (even when it returns
Bottom), as the cache has been used for successive evaluations with various
hypotheses, and the last one is probably not sound in the general case.
parent 0b8c66d1
No related branches found
No related tags found
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment