Commit af40a32d authored by Nikita Zyuzin's avatar Nikita Zyuzin

Make visited expression check the first branch in validAffineBounds

parent f39146e5
......@@ -22,8 +22,6 @@ Definition nozeroiv iv :=
Fixpoint validAffineBounds (e: exp Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
(exprsAf: expressionsAffine) (currentMaxNoise: nat): option (expressionsAffine * nat) :=
olet ares := FloverMap.find e A in
let (intv, _) := ares in
match FloverMap.find e exprsAf with
| Some _ =>
(* expression has already been checked; we do not want to introduce *)
......@@ -31,6 +29,8 @@ Fixpoint validAffineBounds (e: exp Q) (A: analysisResult) (P: precond) (validVar
Some (exprsAf, currentMaxNoise)
| None =>
(* We see it for the first time; update the expressions map *)
olet ares := FloverMap.find e A in
let (intv, _) := ares in
match e with
| Var _ v =>
if NatSet.mem v validVars then
......@@ -529,9 +529,9 @@ Proof.
specialize (fVarsSound n map1 inoise).
specialize (varsTyped n).
specialize (visitedExpr (Var Q n) map1 exprAfs noise iexpmap inoise).
destruct (FloverMap.find (elt:=affine_form Q) (Var Q n) iexpmap) eqn: Hvisited; eauto using visitedExpr.
destruct (FloverMap.find (elt:=intv * error) (Var Q n) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
destruct (FloverMap.find (elt:=affine_form Q) (Var Q n) iexpmap) eqn: Hvisited; eauto using visitedExpr.
destruct (n mem dVars) eqn: Hmem.
+ rewrite NatSet.mem_spec in Hmem.
specialize (dVarsValid Hmem).
......@@ -564,11 +564,11 @@ Proof.
reflexivity.
- clear varsTyped varsDisjoint dVarsValid fVarsSound fVars.
specialize (visitedExpr (Const m v)).
destruct (FloverMap.find (elt:=affine_form Q) (Const m v) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
destruct (FloverMap.find (elt:=intv * error) (Const m v) A) eqn: Hares;
simpl in validBounds; try congruence.
destruct p as [i e].
destruct (FloverMap.find (elt:=affine_form Q) (Const m v) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
destruct (isSupersetIntv (v, v) i) eqn: Hsup; try congruence.
assert (isSupersetIntv (v, v) i = true) as Hsup' by assumption.
apply andb_prop in Hsup' as [L R].
......@@ -611,11 +611,11 @@ Proof.
lra.
- pose proof visitedExpr as visitedExpr'.
specialize (visitedExpr (Unop u e)).
destruct (FloverMap.find (elt:=affine_form Q) (Unop u e) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Unop u e) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
destruct (FloverMap.find (elt:=affine_form Q) (Unop u e) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
destruct (validAffineBounds e A P dVars iexpmap inoise) eqn: Hsubvalid; simpl in validBounds; try congruence.
destruct p as [subexprAff subnoise].
destruct (FloverMap.find (elt:=affine_form Q) e subexprAff) as [af | af] eqn: He; simpl in validBounds; try congruence.
......@@ -673,11 +673,11 @@ Proof.
now rewrite afQ2R_inverse_aff.
- pose proof visitedExpr as visitedExpr'.
specialize (visitedExpr (Binop b e1 e2)).
destruct (FloverMap.find (elt:=affine_form Q) (Binop b e1 e2) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Binop b e1 e2) A) as [p | _] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
destruct (FloverMap.find (elt:=affine_form Q) (Binop b e1 e2) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
destruct (validAffineBounds e1 A P dVars iexpmap inoise) eqn: Hsubvalid1; simpl in validBounds; try congruence.
destruct p as [subexprAff1 subnoise1].
destruct (FloverMap.find (elt:=affine_form Q) e1 subexprAff1) as [af1 | _] eqn: He1; simpl in validBounds; try congruence.
......@@ -860,11 +860,11 @@ Proof.
rewrite afQ2R_divide_aff; auto.
- pose proof visitedExpr as visitedExpr'.
specialize (visitedExpr (Fma e1 e2 e3)).
destruct (FloverMap.find (elt:=affine_form Q) (Fma e1 e2 e3) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Fma e1 e2 e3) A) as [p | _] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
destruct (FloverMap.find (elt:=affine_form Q) (Fma e1 e2 e3) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
destruct (validAffineBounds e1 A P dVars iexpmap inoise) eqn: Hsubvalid1; simpl in validBounds; try congruence.
destruct p as [subexprAff1 subnoise1].
destruct (FloverMap.find (elt:=affine_form Q) e1 subexprAff1) as [af1 | _] eqn: He1; simpl in validBounds; try congruence.
......@@ -949,11 +949,11 @@ Proof.
eapply af_evals_map_extension; try apply contained_map_extension; auto.
- pose proof visitedExpr as visitedExpr'.
specialize (visitedExpr (Downcast m e)).
destruct (FloverMap.find (elt:=affine_form Q) (Downcast m e) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Downcast m e) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
destruct (FloverMap.find (elt:=affine_form Q) (Downcast m e) iexpmap) eqn: Hvisited;
eauto using visitedExpr.
destruct (validAffineBounds e A P dVars iexpmap inoise) eqn: Hsubvalid; simpl in validBounds; try congruence.
destruct p as [subexprAff subnoise].
destruct (FloverMap.find e A) as [p | p] eqn: Hasub; simpl in validBounds; try congruence.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment