Commit 19f50a82 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'master' into 'master'

adding smt interval analysis

See merge request AVA/FloVer!15
parents cad900bc bac7151e
(*
Formalization of SMT Arithmetic for FloVer. Original author: Joachim Bard.
*)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.
Require Import Flover.Infra.ExpressionAbbrevs.
Open Scope R.
(* list of all expr that can occur in SMT queries *)
(* alternative for SMTArith
Inductive SMTExpr : expr Q -> Prop :=
| ConstQ r : SMTExpr (Const REAL r)
| VarQ x : SMTExpr (Var Q x)
| UMinusQ e : SMTExpr e -> SMTExpr (Unop Neg e)
| PlusQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Plus e1 e2)
| MinusQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Sub e1 e2)
| TimesQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Mult e1 e2)
| DivQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Div e1 e2).
*)
Inductive SMTArith :=
| ConstQ (r: Q) : SMTArith
| VarQ (x: nat) : SMTArith
| UMinusQ (e: SMTArith) : SMTArith
| PlusQ (e1 e2: SMTArith) : SMTArith
| MinusQ (e1 e2: SMTArith) : SMTArith
| TimesQ (e1 e2: SMTArith) : SMTArith
| DivQ (e1 e2: SMTArith) : SMTArith.
Inductive SMTLogic :=
| LessQ (e1 e2: SMTArith) : SMTLogic
| LessEqQ (e1 e2: SMTArith) : SMTLogic
| EqualsQ (e1 e2: SMTArith) : SMTLogic
| NotQ (q: SMTLogic) : SMTLogic
| AndQ (q1 q2: SMTLogic) : SMTLogic
| OrQ (q1 q2: SMTLogic) : SMTLogic.
(* TODO: broken (div by 0); remove it *)
Fixpoint evalArith (f: nat -> R) (e: SMTArith) : R :=
match e with
| ConstQ r => Q2R r
| VarQ x => f x
| UMinusQ e => - (evalArith f e)
| PlusQ e1 e2 => (evalArith f e1) + (evalArith f e2)
| MinusQ e1 e2 => (evalArith f e1) - (evalArith f e2)
| TimesQ e1 e2 => (evalArith f e1) * (evalArith f e2)
| DivQ e1 e2 => (evalArith f e1) / (evalArith f e2)
end.
Fixpoint evalLogic (f: nat -> R) (q: SMTLogic) : Prop :=
match q with
| LessQ q1 q2 => (evalArith f q1) < (evalArith f q2)
| LessEqQ q1 q2 => (evalArith f q1) <= (evalArith f q2)
| EqualsQ q1 q2 => (evalArith f q1) = (evalArith f q2)
| NotQ q => ~ (evalLogic f q)
| AndQ q1 q2 => (evalLogic f q1) /\ (evalLogic f q2)
| OrQ q1 q2 => (evalLogic f q1) \/ (evalLogic f q2)
end.
Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
| VarQ_load x v : E x = Some v -> eval_smt E (VarQ x) v
| ConstQ_eval r : eval_smt E (ConstQ r) (Q2R r)
| UMinusQ_eval e v : eval_smt E e v -> eval_smt E (UMinusQ e) (- v)
| PlusQ_eval e1 e2 v1 v2 :
eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (PlusQ e1 e2) (v1 + v2)
| MinusQ_eval e1 e2 v1 v2 :
eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (MinusQ e1 e2) (v1 - v2)
| TimesQ_eval e1 e2 v1 v2 :
eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (TimesQ e1 e2) (v1 * v2)
| DivQ_eval e1 e2 v1 v2 :
v2 <> 0 -> eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (DivQ e1 e2) (v1 / v2).
Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
match q with
| LessQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 < v2
| LessEqQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 <= v2
| EqualsQ e1 e2 => exists v, eval_smt E e1 v /\ eval_smt E e2 v
| NotQ q => ~ (eval_smt_logic E q)
| AndQ q1 q2 => eval_smt_logic E q1 /\ eval_smt_logic E q2
| OrQ q1 q2 => eval_smt_logic E q1 \/ eval_smt_logic E q2
end.
Fixpoint varsSMT (e: SMTArith) :=
match e with
| VarQ x => {{x}}
| ConstQ _ => NatSet.empty
| UMinusQ e => varsSMT e
| PlusQ e1 e2 => varsSMT e1 varsSMT e2
| MinusQ e1 e2 => varsSMT e1 varsSMT e2
| TimesQ e1 e2 => varsSMT e1 varsSMT e2
| DivQ e1 e2 => varsSMT e1 varsSMT e2
end.
Fixpoint varsLogic (q: SMTLogic) :=
match q with
| LessQ e1 e2 => varsSMT e1 varsSMT e2
| LessEqQ e1 e2 => varsSMT e1 varsSMT e2
| EqualsQ e1 e2 => varsSMT e1 varsSMT e2
| NotQ q => varsLogic q
| AndQ q1 q2 => varsLogic q1 varsLogic q2
| OrQ q1 q2 => varsLogic q1 varsLogic q2
end.
(*
(* Does not work for NotQ *)
Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
| LessQ_eval e1 e2 v1 v2 :
eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 < v2 -> eval_smt_logic E (LessQ e1 e2)
| LessEqQ_eval e1 e2 v1 v2 :
eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 <= v2 -> eval_smt_logic E (LessEqQ e1 e2)
| EqualsQ_eval e1 e2 v1 v2 :
eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 = v2 -> eval_smt_logic E (EqualsQ e1 e2)
(* | NotQ_eval q : ~ (eval_smt_logic E q) -> eval_smt_logic E (NotQ q) *)
| AndQ_eval q1 q2 :
eval_smt_logic E q1 -> eval_smt_logic E q2 -> eval_smt_logic E (AndQ q1 q2)
| OrQ_eval_l q1 q2 : eval_smt_logic E q1 -> eval_smt_logic E (OrQ q1 q2)
| OrQ_eval_r q1 q2 : eval_smt_logic E q2 -> eval_smt_logic E (OrQ q1 q2).
*)
Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
match e with
| ConstQ r => Expressions.Const REAL r
| VarQ x => Var Q x
| UMinusQ e0 => Unop Neg (SMTArith2Expr e0)
| PlusQ e1 e2 => Binop Plus (SMTArith2Expr e1) (SMTArith2Expr e2)
| MinusQ e1 e2 => Binop Sub (SMTArith2Expr e1) (SMTArith2Expr e2)
| TimesQ e1 e2 => Binop Mult (SMTArith2Expr e1) (SMTArith2Expr e2)
| DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
end.
Definition optionBind2 (X: Type) (F: X -> X -> X) (x x': option X) : option X :=
match x with
| Some v => match x' with
| Some v' => Some (F v v')
| None => x
end
| None => x'
end.
Definition merge_split (F: SMTLogic -> SMTLogic -> SMTLogic) l r :=
match l, r with
| (P1, q1), (P2, q2) => (optionBind2 AndQ P1 P2, optionBind2 F q1 q2)
end.
(*
(* TODO: splits by syntax *)
(* if q looks like part of the precondition it appears left, otherwise right *)
Fixpoint splitPre (q: SMTLogic) : option SMTLogic * option SMTLogic :=
match q with
| LessEqQ (ConstQ r) (VarQ x) => (Some q, None)
| LessEqQ (VarQ x) (ConstQ r) => (Some q, None)
| LessQ (ConstQ r) (VarQ x) => (Some q, None)
| LessQ (VarQ x) (ConstQ r) => (Some q, None)
| AndQ q1 q2 => merge_split AndQ (splitPre q1) (splitPre q2)
| _ => (None, Some q)
end.
Lemma splitPre_LessEqQ e1 e2 :
splitPre (LessEqQ e1 e2) = (Some (LessEqQ e1 e2), None)
\/ splitPre (LessEqQ e1 e2) = (None, Some (LessEqQ e1 e2)).
Proof.
destruct e1, e2; auto.
Qed.
Lemma splitPre_LessQ e1 e2 :
splitPre (LessQ e1 e2) = (Some (LessQ e1 e2), None)
\/ splitPre (LessQ e1 e2) = (None, Some (LessQ e1 e2)).
Proof.
destruct e1, e2; auto.
Qed.
Lemma splitPre_correct_SN q q' :
splitPre q = (Some q', None) -> q = q'.
Proof.
induction q in q' |- *; cbn; intros eq; try congruence.
- destruct e1, e2; congruence.
- destruct e1, e2; congruence.
- destruct (splitPre q1) as [[?|] [?|]]; destruct (splitPre q2) as [[?|] [?|]]; cbn in eq; try congruence.
+ rewrite (IHq1 s), (IHq2 s0); auto.
congruence.
+ rewrite (IHq1 s); auto. admit.
+
Lemma splitPre_corr E (q p' q': SMTLogic) :
(eval_smt_logic E q)
-> (splitPre q = (Some p', Some q') -> eval_smt_logic E p' /\ eval_smt_logic E q')
/\ (splitPre q = (None, Some q') -> eval_smt_logic E q')
/\ (splitPre q = (Some p', None) -> eval_smt_logic E p').
Proof.
induction q in p', q' |- *; intros H.
- destruct (splitPre_LessQ e1 e2) as [-> | ->]; repeat split; congruence.
- destruct (splitPre_LessEqQ e1 e2) as [-> | ->]; repeat split; congruence.
- cbn. repeat split; congruence.
- cbn. repeat split; try congruence. intros H'. assert (q' = NotQ q) by congruence.
now subst.
- destruct H as [H1 H2]. cbn.
destruct (splitPre q1) as [[?|] [?|]]; destruct (splitPre q2) as [[?|] [?|]]; cbn; repeat split; try congruence.
+ assert (p' = AndQ s s1) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s2 H2) as [? [? ?]]. tauto.
+ assert (q' = AndQ s0 s2) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s2 H2) as [? [? ?]]. tauto.
+ assert (p' = AndQ s s1) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s1 H2) as [? [? ?]]. tauto.
+ assert (q' = s0) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ assert (p' = s) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ assert (q' = AndQ s0 s1) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s1 H2) as [? [? ?]]. tauto.
+ assert (p' = s) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ assert (q' = s0) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ admit.
+ admit.
+ intros H. assert (p' = AndQ s s0) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s0 s0 H2) as [? [? ?]]. tauto.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
- cbn. repeat split; congruence.
Admitted.
Lemma splitPre_correct E (q p' q': SMTLogic) :
(splitPre q = (Some p', Some q') -> eval_smt_logic E p' /\ eval_smt_logic E q')
/\ (splitPre q = (None, Some q') -> eval_smt_logic E q')
/\ (splitPre q = (Some p', None) -> eval_smt_logic E p')
-> eval_smt_logic E q.
Proof.
induction q in p', q' |- *; intros [H1 [H2 H3]].
- destruct (splitPre_LessQ e1 e2) as [H|H]; rewrite H in *.
+ apply H3.
*)
(* TODO: Maybe introduce True as SMTLogic *)
Fixpoint findLow (q: SMTLogic) (x: nat) (lo: Q) : option SMTLogic * option SMTLogic :=
match q with
| LessEqQ (ConstQ c) (VarQ x) => if Qeq_bool c lo then (Some q, None) else (None, Some q)
| AndQ q1 q2 => match findLow q1 x lo with
| (Some q', None) => (Some q', Some q2)
| (Some q', Some q'') => (Some q', Some (AndQ q'' q2))
| (None, _) => match findLow q2 x lo with
| (Some q', None) => (Some q', Some q1)
| (Some q', Some q'') => (Some q', Some (AndQ q1 q''))
| (None , _) => (None, Some q)
end
end
| _ => (None, Some q)
end.
Lemma findLow_correct E v q q' x lo :
E x = Some v -> Q2R lo <= v -> fst (findLow q x lo) = Some q' -> eval_smt_logic E q'.
Proof.
intros H1 H2. induction q; try discriminate.
- cbn. destruct e1, e2; try discriminate.
(* cbn. intros H. assert (eq: q' = LessEqQ (ConstQ r) (VarQ x0)) by congruence.
rewrite eq. cbn. exists (Q2R r). exists v. repeat split; cbn; auto. *)
Abort.
Fixpoint findHi (q: SMTLogic) (x: nat) (hi: Q) : option SMTLogic * option SMTLogic :=
match q with
| LessEqQ (VarQ x) (ConstQ c) => if Qeq_bool c hi then (Some q, None) else (None, Some q)
| AndQ q1 q2 => match findHi q1 x hi with
| (Some q', None) => (Some q', Some q2)
| (Some q', Some q'') => (Some q', Some (AndQ q'' q2))
| (None, _) => match findHi q2 x hi with
| (Some q', None) => (Some q', Some q1)
| (Some q', Some q'') => (Some q', Some (AndQ q1 q''))
| (None , _) => (None, Some q)
end
end
| _ => (None, Some q)
end.
Lemma findHi_correct E v q q' x hi :
E x = Some v -> v <= Q2R hi -> fst (findHi q x hi) = Some q' -> eval_smt_logic E q'.
Admitted.
Definition findLowHi (q: SMTLogic) (x: nat) (iv: intv) :=
match findLow q x (fst iv) with
| (Some ql, Some q') => match findHi q' x (snd iv) with
| (Some qh, res) => (Some (AndQ ql qh), res)
| _ => (None, None) (* error occured *)
end
| _ => (None, None) (* error occured *)
end.
Definition foldFnc (el: expr Q * intv) (qs: option SMTLogic * option SMTLogic) :=
match el with
| (Var _ x, iv) =>
match qs with
| (None, Some q) => findLowHi q x iv
| (Some q', Some q) => match findLowHi q x iv with
| (Some q'', rest) => (Some (AndQ q'' q'), rest)
| _ => (None, None)
end
| _ => qs
end
| _ => qs
end.
Definition splitPre (P: FloverMap.t intv) q :=
List.fold_right foldFnc (None, Some q) (FloverMap.elements P).
Definition eval_precond E (P: FloverMap.t intv) :=
forall x lo hi, (List.In (Var Q x, (lo, hi)) (FloverMap.elements P)) -> exists vR: R,
E x = Some vR /\ FloverMap.find (Var Q x) P = Some (lo, hi)
/\ Q2R lo <= vR <= Q2R hi.
Lemma splitPre_correct E P q q' :
fst(splitPre P q) = Some q' -> eval_smt_logic E q' -> eval_precond E P.
Proof.
unfold splitPre, eval_precond.
induction (FloverMap.elements P) in q' |- *.
- cbn. tauto.
- cbn. intros H H' x lo hi [eq | tail].
+ admit.
+ destruct (List.fold_right foldFnc (None, Some q) l) as [[q''|] ?].
* apply (IHl q''); auto.
cbn in H. admit.
* destruct o, a, k; cbn in H; try discriminate.
Abort.
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith.
Definition x0 :expr Q := Var Q 0.
Definition y1 :expr Q := Var Q 1.
Definition e1 :expr Q := Binop Plus x0 y1.
Definition e2 :expr Q := Binop Div e1 y1.
Definition C34 :expr Q := Const M64 ((17)#(5)).
Definition e5 :expr Q := Binop Plus e2 C34.
Definition Rete5 := Ret e5.
Definition defVars_fnc1 :FloverMap.t mType :=
(FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType))).
Definition thePrecondition_fnc1:precond := fun (n:nat) =>
if n =? 0 then ( (-3)#(1), (6)#(1)) else if n =? 1 then ( (2)#(1), (8)#(1)) else (0#1,0#1).
Definition absenv_fnc1 :analysisResult := Eval compute in
FloverMap.add e5 (( (29)#(10), (75821)#(10240)), (31656575032439604176368417020690028172637826983022229834977068248762132258095105)#(4767828205180598627806767057994257910674911537412415567148097160036817151091933841114427031552)) (FloverMap.add C34 (( (17)#(5), (17)#(5)), (17)#(45035996273704960)) (FloverMap.add e2 (( (-1)#(2), (8201)#(2048)), (2879632975312110162723860570159105251222262341380356792653971457)#(529335265084873566077879553980951356026419978008369989458181366086188773933056)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add e1 (( (-1)#(1), (14)#(1)), (126100789566373895)#(40564819207303340847894502572032)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add x0 (( (-3)#(1), (6)#(1)), (3)#(4503599627370496)) (FloverMap.empty (intv * error)))))))).
Definition querymap_fnc1 := Eval compute in
FloverMap.add e5 (nil) (FloverMap.add C34 (nil) (FloverMap.add e2 ((cons (AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))) (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) (LessEqQ (VarQ 0) (ConstQ ((6)#(1)))))))) nil)) (FloverMap.add y1 (nil) (FloverMap.add e1 (nil) (FloverMap.add y1 (nil) (FloverMap.add x0 (nil) (FloverMap.empty (list SMTLogic)))))))).
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import RealRangeArith.
Require Import Flover.Expressions.
Definition query :=
match FloverMap.find e2 querymap_fnc1 with
| Some (List.cons q _) => q
| _ => EqualsQ (ConstQ (0#1)) (ConstQ (1#1)) (* 0 == 1 *)
end.
Lemma eval_smt_expr E e v :
eval_smt E e v -> eval_expr E (fun _ => Some REAL) (toRExp (SMTArith2Expr e)) v REAL.
Proof with try (right; apply Rabs_R0).
induction 1.
- now constructor.
- rewrite <- (delta_0_deterministic _ REAL 0)... constructor...
- rewrite <- (delta_0_deterministic _ REAL 0)... apply (Unop_neg (m:= REAL)); auto.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto...
Qed.
Lemma eval_expr_smt E Gamma e v :
eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> eval_smt E e v.
Proof.
induction e in v |- *; cbn; intros H.
- inversion H. cbn. constructor.
- inversion H. cbn. constructor; auto.
- inversion H. cbn. constructor. destruct m; try discriminate. auto.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor; auto.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
Qed.
Lemma e2_to_smt : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)).
Proof.
reflexivity.
Qed.
(*
Lemma refute_bound E :
fVars_P_sound (usedVars e2) E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> ~ eval_smt_logic E (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))).
Proof.
intros P unsatQ B.
apply unsatQ. cbn. repeat constructor.
- exact B.
- destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
- destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
- destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
- destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
Qed.
*)
Lemma refute_bound E :
fVars_P_sound (usedVars e2) E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> ~ eval_smt_logic E (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))).
Proof.
intros P unsatQ B.
apply unsatQ. cbn. repeat split.
- exact B.
- destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
exists v1. eexists. repeat split. 1-2: now constructor. apply H1.
- destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
eexists. exists v1. repeat split. 1-2: now constructor. apply H1.
- destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
eexists. exists v1. repeat split. 1-2: now constructor. apply H1.
- destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
exists v1. eexists. repeat split. 1-2: now constructor. apply H1.
Qed.
Theorem RangeBound_e2_sound E Gamma v :
fVars_P_sound (usedVars e2) E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL
-> v <= Q2R ((8201)#(2048)).
Proof.
intros Psound unsatQ e2v.
rewrite e2_to_smt in e2v.
apply eval_expr_smt in e2v.
apply Rnot_lt_le. intros B.
eapply refute_bound. 1-2: eassumption.
eexists. exists v. repeat split. constructor. exact e2v. exact B.
Qed.
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith.
Definition x0 :expr Q := Var Q 0.
Definition y1 :expr Q := Var Q 1.
Definition e1 :expr Q := Binop Plus x0 y1.
Definition e2 :expr Q := Binop Div e1 y1.
Definition C34 :expr Q := Const M64 ((17)#(5)).
Definition e5 :expr Q := Binop Plus e2 C34.
Definition Rete5 := Ret e5.
Definition defVars_fnc1 :FloverMap.t mType :=
(FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType))).
Definition thePrecondition_fnc1: FloverMap.t intv :=
FloverMap.add x0 ((-3)#(1), (6)#(1)) (FloverMap.add y1 (2#1, 8#1) (FloverMap.empty intv)).
Definition absenv_fnc1 :analysisResult := Eval compute in
FloverMap.add e5 (( (29)#(10), (75821)#(10240)), (31656575032439604176368417020690028172637826983022229834977068248762132258095105)#(4767828205180598627806767057994257910674911537412415567148097160036817151091933841114427031552)) (FloverMap.add C34 (( (17)#(5), (17)#(5)), (17)#(45035996273704960)) (FloverMap.add e2 (( (-1)#(2), (8201)#(2048)), (2879632975312110162723860570159105251222262341380356792653971457)#(529335265084873566077879553980951356026419978008369989458181366086188773933056)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add e1 (( (-1)#(1), (14)#(1)), (126100789566373895)#(40564819207303340847894502572032)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add x0 (( (-3)#(1), (6)#(1)), (3)#(4503599627370496)) (FloverMap.empty (intv * error)))))))).
Definition querymap_fnc1 := Eval compute in
FloverMap.add e5 (nil) (FloverMap.add C34 (nil) (FloverMap.add e2 ((cons (AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))) (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) (LessEqQ (VarQ 0) (ConstQ ((6)#(1)))))))) nil)) (FloverMap.add y1 (nil) (FloverMap.add e1 (nil) (FloverMap.add y1 (nil) (FloverMap.add x0 (nil) (FloverMap.empty (list SMTLogic)))))))).
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import RealRangeArith.
Require Import Flover.Expressions.
Definition query :=
match FloverMap.find e2 querymap_fnc1 with
| Some (List.cons q _) => q
| _ => TrueQ
end.
(*
Definition prec :=
match query with
| AndQ q1 q2 => q2
| _ => TrueQ
end.
*)
Definition prec :=
AndQ (LessEqQ (ConstQ (-3 # 1)) (VarQ 0))
(AndQ (LessEqQ (VarQ 0) (ConstQ (6 # 1)))
(AndQ (LessEqQ (ConstQ (2 # 1)) (VarQ 1))
(AndQ (LessEqQ (VarQ 1) (ConstQ (8 # 1))) TrueQ))).
Definition bound :=
match query with
| AndQ q1 q2 => q1
| _ => TrueQ
end.
Lemma prec_bound_correct E :
eval_smt_logic E query <-> eval_smt_logic E (AndQ prec bound).
Proof.
cbn. tauto.
Qed.
Definition bound_expr :=
match bound with
| LessQ e (ConstQ r) => e
| LessQ (ConstQ r) e => e
| _ => ConstQ (0#1)
end.
Lemma e2_to_smt : e2 = SMTArith2Expr bound_expr.
Proof.
reflexivity.
Qed.
(*
Lemma precond_bound_correct E :
eval_precond E thePrecondition_fnc1
-> eval_smt_logic E bound
-> eval_smt_logic E query.
Proof.
intros P B.