Commit 80518221 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Progress with dVars condition

parent 8bc8c028
This diff is collapsed.
......@@ -16,6 +16,26 @@ Module FloverMapFacts := OrdProperties (FloverMap).
Definition analysisResult :Type := FloverMap.t (intv * error).
Definition expressionsAffine: Type := FloverMap.t (affine_form Q).
Definition contained_flover_map V expmap1 expmap2 :=
forall (e: exp Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v.
Instance contained_flover_map_preorder (V: Type) : PreOrder (@contained_flover_map V).
Proof.
constructor; unfold Reflexive, Transitive, contained_flover_map; eauto.
Qed.
Lemma contained_flover_map_extension V (expmap: FloverMap.t V) e v:
FloverMap.find e expmap = None ->
contained_flover_map expmap (FloverMap.add e v expmap).
Proof.
intros Hnone e' v' Hcont.
rewrite <- Hcont.
destruct (Q_orderedExps.expCompare e e') eqn: Hcomp.
- assert (FloverMap.find e expmap = FloverMap.find e' expmap) by (apply FloverMapFacts.P.F.find_o; auto); congruence.
- apply FloverMapFacts.P.F.add_neq_o; congruence.
- apply FloverMapFacts.P.F.add_neq_o; congruence.
Qed.
(**
We treat a function mapping an expression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
......
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