Commit 4f514011 authored by Joachim Bard's avatar Joachim Bard

SMT validation without not needed sets

parent e2264f8c
......@@ -248,12 +248,23 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
| OrQ_eval_r q1 q2 : eval_smt_logic E q2 -> eval_smt_logic E (OrQ q1 q2).
*)
Definition unsat_queries E qMap :=
forall e ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh.
(*
Definition eval_precond E (P: FloverMap.t intv) :=
forall x iv, FloverMap.find (Var Q x) P = Some iv
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)
(* TODO: move eval_precond and eqb_var somewhere else *)
Lemma eqb_var x e : FloverMapFacts.P.F.eqb (Var Q x) e = true -> e = Var Q x.
Proof.
rewrite eqb_cmp_eq. destruct e; cbn; try discriminate.
case_eq (x ?= n)%nat; intros H; try discriminate.
apply Nat.compare_eq in H. now subst.
Qed.
Definition eval_precond E (P: FloverMap.t intv) :=
forall e x iv, List.In (e, iv) (FloverMap.elements P)
-> (FloverMapFacts.P.F.eqb (Var Q x) e = true)
......
......@@ -14,7 +14,7 @@ From Flover
Infra.Ltacs Infra.RealSimps TypeValidator.
From Flover
Require Export IntervalArithQ IntervalArith SMTArith2 ssaPrgs RealRangeArith.
Require Export IntervalArithQ IntervalArith SMTArith ssaPrgs RealRangeArith.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
match q with
......@@ -202,17 +202,16 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t
end.
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv)
(Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma :
(forall e loQ hiQ, FloverMap.find e Q = Some (loQ, hiQ) -> ~ eval_smt_logic E loQ /\ ~ eval_smt_logic E hiQ) ->
(Q: FloverMap.t (SMTLogic * SMTLogic)) dVars (E: env) Gamma :
unsat_queries E Q ->
validSMTIntervalbounds f A P Q dVars = true ->
dVars_range_valid dVars E A ->
NatSet.Subset (usedVars f -- dVars) fVars ->
eval_precond E P ->
validTypes f Gamma ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
induction f;
intros unsat_queries valid_bounds valid_definedVars usedVars_subset valid_precond types_defined;
intros unsat_qs valid_bounds valid_definedVars valid_precond types_defined;
cbn in *.
- destruct (NatSet.mem n dVars) eqn:?; cbn in *; split; auto.
+ destruct (valid_definedVars n)
......@@ -230,7 +229,6 @@ Proof.
apply findA_find in Heqo0 as [e' [? ?]].
apply find_some in H as [? ?].
destruct (valid_precond e' n i0) as [vR [env_valid bounds_valid]]; auto.
assert (NatSet.In n fVars) by set_tac.
canonize_hyps.
kill_trivial_exists.
eexists; split; [auto | split].
......@@ -295,9 +293,9 @@ Proof.
- destruct types_defined
as [? [? [[? [? ?]]?]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf1; try auto).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf2; try auto).
repeat split;
[ intros; subst; Flover_compute; congruence |
auto | auto |].
......@@ -376,11 +374,11 @@ Proof.
- destruct types_defined
as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf1; try auto).
assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf2; try auto).
assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
by (Flover_compute; try congruence; apply IHf3; try auto).
repeat split; try auto.
apply validRanges_single in valid_f1;
apply validRanges_single in valid_f2;
......
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