Changeset 2700 for src/ASM/Policy.ma


Ignore:
Timestamp:
Feb 22, 2013, 2:12:24 PM (7 years ago)
Author:
sacerdot
Message:
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2653 r2700  
    322322      cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    323323      normalize nodelta
    324       [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     324      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le
     325        @monotonic_lt_times_r [/2/] %
    325326      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    326327        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
     
    333334    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    334335    normalize nodelta
    335     [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
     336    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le
     337      @monotonic_lt_times_r try % /2/
    336338    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    337339      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
Note: See TracChangeset for help on using the changeset viewer.