Commit 08889677 authored by Joachim Bard's avatar Joachim Bard
Browse files

adding support for empty subdivs

parent 2f33f960
......@@ -654,12 +654,33 @@ Proof.
apply in_map_iff; eauto.
Qed.
Definition isNonEmptySubdiv e (S: precond * analysisResult * usedQueries) :=
match S with
| (P, A, Q) => match FloverMap.find e Q with
| Some (q, _) => negb (checkPre P q)
| None => true
end
end.
Lemma isNonEmptySubdiv_sound E e P A Q :
eval_precond E P ->
unsat_queries Q ->
isNonEmptySubdiv e (P, A, Q) = true.
Proof.
intros HP HQ. cbn.
destruct (FloverMap.find e Q) as [[q1 q2] |] eqn: Hfind; auto.
destruct (checkPre P q1) eqn: H; auto.
exfalso. destruct (HQ E e q1 q2) as [HnP _]; auto.
apply HnP.
eapply checkPre_pre_smt; eauto.
Qed.
(** Interval subdivisions checking function **)
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) subdivs (defVars: FloverMap.t mType) Gamma :=
validSSA e (preVars P) &&
checkPreconds (map (fun S => match S with (P, _, _) => P end) subdivs) P &&
checkSubdivs e absenv subdivs defVars Gamma.
checkSubdivs e absenv (filter (isNonEmptySubdiv e) subdivs) defVars Gamma.
Definition queriesInSubdivs (subdivs: list (precond * analysisResult * usedQueries)) :=
map (fun S => match S with (_, _, Q) => Q end) subdivs.
......@@ -700,7 +721,11 @@ Proof.
{ eapply validSSA_eq_set; eauto. eapply checkPreconds_preVars; eauto. }
apply in_map_iff in in_subdivs as [[[P2 A] Qmap] [Heq in_subdivs]].
cbn in Heq; subst.
pose proof (checkSubdivs_sound e _ _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (In (P1, A, Qmap) (filter (isNonEmptySubdiv e) subdivs)) as in_nonempty_subdivs.
{ apply filter_In. split; auto.
eapply isNonEmptySubdiv_sound; eauto.
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
pose proof (checkSubdivs_sound e _ _ _ _ _ _ _ valid_subdivs in_nonempty_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P1 Qmap defVars Gamma = true) as res_check
by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
eapply approxEnv_empty_dVars in approxEnv; eauto.
......
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