IntervalValidation.v 2.56 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
Require Import Coq.QArith.QArith.
Require Import Daisy.Expressions Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.IntervalArithQ Daisy.Infra.RationalConstruction.

Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
  let (intv, _) := absenv e in
    match e with
    | Var v =>
      let bounds_v := P v in
      andb (Qeqb (fst intv) (fst (bounds_v))) (Qeqb (snd intv) (snd (bounds_v)))
    | Param v =>
      let bounds_v := P v in
      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd intv) (snd (bounds_v)))
    | Const n =>
      andb (Qleb (fst intv) n) (Qleb (snd intv) n)
    | Binop b e1 e2 =>
      let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
      let (iv1,_) := absenv e1 in
      let (iv2,_) := absenv e2 in
      let opres :=
          match b with
          | Plus =>
            let new_iv := addIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Sub =>
            let new_iv := subtractIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Mult =>
            let new_iv := multIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Div => false
          end
      in
      andb rec opres
    end.

Definition u:nat := 1.
(** 1655/5 = 331; 0,4 = 2/5 **)
Definition cst1:Q := 1657 # 5.

(** Define abbreviations **)
Definition varU:exp Q := Param Q u.
Definition valCst:exp Q := Const cst1.
Definition valCstAddVarU:exp Q := Binop Plus valCst varU.

(** Error values **)
Definition errCst1 :Q := rationalFromNum (36792791036077685#1) 16 14.
Definition errVaru := rationalFromNum (11102230246251565#1) 16 14.
Definition lowerBoundAddUCst:Q := 1157 # 5.
Definition upperBoundAddUCst:Q := 2157 # 5.
Definition errAddUCst := rationalFromNum (9579004256465851#1) 15 14.

(** The added assertion becomes the precondition for us **)
Definition precondition := fun n:nat => (- (100#1),100#1).
Definition absenv := fun e:exp Q => match e with
                                 |Const n => (cst1,cst1,0)
                                 |Binop b e1 e2 => (lowerBoundAddUCst,upperBoundAddUCst,0)
                                 | Param v => (-(100#1),100#1,0)
                                 | _ => (0,0,0)
                                 end.

Eval compute in isSupersetIntv (lowerBoundAddUCst,upperBoundAddUCst) (lowerBoundAddUCst,upperBoundAddUCst).
Eval compute in addIntv (cst1,cst1) (-(100#1),100#1).

Eval compute in validIntervalbounds valCst (fun _ => (cst1,cst1,0)) (fun _ => (cst1,cst1)).
Eval compute in validIntervalbounds varU (fun _ => (- (100#1),100#1,0)) precondition.