• Johannes Kanig's avatar
    N127-001 improve performance on fastWP · 2afdad2c
    Johannes Kanig authored
    On N121-024 we fixed a bug where a state was incorrectly reused during
    merge. The fix was to never reuse state when merging. This resulted in a
    performance drop.
    
    The new fix now marks states which should not be reused - basically
    states that come from raise - and when such a state is present during
    merging, we don't reuse. Otherwise, we reuse.  This seems to get us the
    performance and passes all tests.
    
    Marking is implemented simply by a flag in states
    
    * mlw_wp.ml:
    (mark) allows to set the marked flag of a state
    (empty) empty state is not marked
    (havoc) havoc doesn't change marked state
    (merge_vars, merge_regs) new argument "marked", only create a new
      variable when marked is true, otherwise reuse
    (fast_wp) in the case of Eraise, mark the used state
    
    M415-042 pass labels down to conjunctions
    
    Why3 parser groups the loop invariants into a single formula. This patch
    allows to have the VC labels on every conjunct
    
    mlw_wp.ml
    (fastwp) call wp_expl instead of t_label
    2afdad2c
Name
Last commit
Last update
..
coq-tactic Loading commit data...
core Loading commit data...
driver Loading commit data...
ide Loading commit data...
jessie Loading commit data...
mlw Loading commit data...
parser Loading commit data...
printer Loading commit data...
session Loading commit data...
tools Loading commit data...
transform Loading commit data...
trywhy3 Loading commit data...
util Loading commit data...
why3doc Loading commit data...
why3session Loading commit data...
whyml Loading commit data...
config.sh.in Loading commit data...