Commit 83c1c774 authored by Joachim Bard's avatar Joachim Bard

adjusting testcases to renaming of files

parent 2ae8fcbd
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
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.
......
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
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.
......
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)))))))).
Section Test.
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.
Require Import RealRangeArith.
Require Import IntervalArithQ.
Open Scope R.
Definition query := Eval compute in
match FloverMap.find e2 querymap_fnc1 with
| Some (List.cons q _) => q
| _ => EqualsQ (ConstQ (0#1)) (ConstQ (1#1)) (* 0 == 1 *)
end.
Definition preC :=
(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))))))).
Definition bound := (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))).
Definition q := AndQ bound preC.
Arguments bound : simpl never.
Arguments preC : simpl never.
Lemma test0 : forall f, evalLogic f preC -> ~ evalLogic f q -> ~ evalLogic f bound.
Proof.
intros f P nq B.
apply nq. cbn. auto.
Qed.
(* this (or similar) might be already defined somewhere *)
Definition evalPrecond f (P: precond) n :=
match P n with
|(lo, hi) => (Q2R lo <= f n) /\ (f n <= Q2R hi)
end.
Lemma test1 : forall f, (forall n, evalPrecond f thePrecondition_fnc1 n) -> evalLogic f preC.
Proof.
intros f H. unfold preC. cbn. repeat split.
- apply (H 1%nat).
- apply (H 0%nat).
- apply (H 1%nat).
- apply (H 0%nat).
Qed.
Lemma test2 : forall f, (forall n, evalPrecond f thePrecondition_fnc1 n) -> ~ evalLogic f q -> ~ evalLogic f bound.
Proof.
intros f H. apply test0. apply test1. apply H.
Qed.
Definition get_bound q :=
match q with
| AndQ b _ => b (* only works if the bound is at the left *)
| _ => q (* FAIL: q has not the right format *)
end.
Lemma test3 : forall f, (forall n, evalPrecond f thePrecondition_fnc1 n) -> ~ evalLogic f query -> ~ evalLogic f (get_bound query).
Proof.
unfold query, bound. cbn. intros f validP unsatQ validB.
apply unsatQ.
split; [exact validB | clear unsatQ validB ].
repeat split; first [now apply (validP 0%nat) | now apply (validP 1%nat)].
Qed.
Lemma test4 :
forall f, ~ evalLogic f (get_bound query) -> evalLogic f (LessEqQ (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)) (ConstQ (8201 # 2048))).
Proof.
cbn. intros f unsatB. now apply Rnot_lt_le.
Qed.
Lemma test5 : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)).
Proof.
reflexivity.
Qed.
(*
Print eval_expr.
Print env.
Print toREval.
Print option.
Print mTypeToR.
Print toRExp.
Print fVars_P_sound.
Print toRTMap.
Print toRExpMap.
*)
(* Lemma bound_e2 : eval_expr _ _ (toRExp e2). *)
End Test.
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
Require Import Flover.SMTArith.
(* Require Import Flover.SMTValidation. *)
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition C34 :expr Q := Const M64 ((3)#(5)).
......
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
Require Import Flover.SMTArith.
(* Require Import Flover.SMTValidation. *)
Definition x0 :expr Q := Var Q 0.
Definition y1 :expr Q := Var Q 1.
......
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