Commit fa8496dd authored by Joachim Bard's avatar Joachim Bard

updating CI testcases

parent b860d761
......@@ -2,21 +2,25 @@ Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition Rete3 := Ret e3.
Definition defVars_additionSimple :FloverMap.t mType :=
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition thePrecondition_additionSimple:precond := fun (n:nat) =>
if n =? 0 then ( (-100)#(1), (100)#(1)) else (0#1,0#1).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
].
Definition absenv_additionSimple :analysisResult := Eval compute in
FloverMap.add e3 (( (1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Theorem ErrorBound_additionSimple_Sound :
CertificateCheckerCmd Rete3 absenv_additionSimple thePrecondition_additionSimple defVars_additionSimple = true.
Proof.
vm_compute; auto.
Qed.
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition thePrecondition_additionSimple_sub0 :=
(FloverMap.add u0 ((-100)#(1), (-100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub1 :=
(FloverMap.add u0 ((-100)#(3), (100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub2 :=
(FloverMap.add u0 ((100)#(3), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition querymap_additionSimple_sub0 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub1 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub2 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition absenv_additionSimple_sub0: analysisResult :=
FloverMap.add e3 (((1157)#(5), (4471)#(15)), (19711354849075188187)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(1), (-100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub1: analysisResult :=
FloverMap.add e3 (((4471)#(15), (5471)#(15)), (21512794700023386587)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(3), (100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub2: analysisResult :=
FloverMap.add e3 (((5471)#(15), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((100)#(3), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
(thePrecondition_additionSimple_sub0, absenv_additionSimple_sub0, querymap_additionSimple_sub0);(thePrecondition_additionSimple_sub1, absenv_additionSimple_sub1, querymap_additionSimple_sub1);(thePrecondition_additionSimple_sub2, absenv_additionSimple_sub2, querymap_additionSimple_sub2)].
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition thePrecondition_additionSimple_sub0 :=
(FloverMap.add u0 ((-100)#(1), (-100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub1 :=
(FloverMap.add u0 ((-100)#(3), (100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub2 :=
(FloverMap.add u0 ((100)#(3), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition querymap_additionSimple_sub0 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub1 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub2 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition absenv_additionSimple_sub0: analysisResult :=
FloverMap.add e3 (((1157)#(5), (4471)#(15)), (19711354849075188187)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(1), (-100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub1: analysisResult :=
FloverMap.add e3 (((4471)#(15), (5471)#(15)), (21512794700023386587)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(3), (100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub2: analysisResult :=
FloverMap.add e3 (((5471)#(15), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((100)#(3), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
(thePrecondition_additionSimple_sub0, absenv_additionSimple_sub0, querymap_additionSimple_sub0);(thePrecondition_additionSimple_sub1, absenv_additionSimple_sub1, querymap_additionSimple_sub1);(thePrecondition_additionSimple_sub2, absenv_additionSimple_sub2, querymap_additionSimple_sub2)].
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
Definition C34 :expr Q := Const M64 ((1657)#(5)).
Definition FMA5mult :expr Q := Binop Mult C12 T2.
Definition FMA5 :expr Q := Fma C12 T2 C34.
Definition t15 :expr Q := Var Q 5.
Definition UMint15 :expr Q := Unop Neg t15.
Definition v1 :expr Q := Var Q 1.
Definition e6 :expr Q := Binop Mult UMint15 v1.
Definition u0 :expr Q := Var Q 0.
Definition e7 :expr Q := Binop Plus t15 u0.
Definition e8 :expr Q := Binop Mult e7 e7.
Definition e9 :expr Q := Binop Div e6 e8.
Definition Let10 := Let M64 5 FMA5 e9.
Definition defVars_doppler: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 5) (M64) (FloverMap.add (Var Q 2) (M64) (FloverMap.empty mType))))).
Definition subdivs_doppler: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_doppler :=
(FloverMap.add T2 ((-30)#(1), (50)#(1)) (FloverMap.add v1 ((20)#(1), (20000)#(1)) (FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv))),
(AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ)).
Definition absenv_doppler: analysisResult :=
FloverMap.add Let10 (((-180700000)#(1138489), (-156700)#(5322249)), (6830474556051150717276799761411546903312647039023687172223811352204070680260786237572370408687560441727006035326226907571046644765565610826295450225945821689766113946084926436173485860032840000964523515885271737730095253157325021312893152796246718141576145498964466082789239458535219584103497743580035241118781706960333496399469040697857641019083062655105934801391066722947827783153125)#(10652421913510213733898407083420012913520344863420275587860254841070206042654275053211239601233990813544801557039628247004768110951082434032072365979905419580587655195775106519963774511263809230729529345878113187715691336518180342419923881592311850124427434616938294137618896157525426696073050860327859392612474295413649439400913925656013708636956880301351141496628302550147680567001131206431473664)) (FloverMap.add e9 (((-180700000)#(1138489), (-156700)#(5322249)), (6830474556051150717276799761411546903312647039023687172223811352204070680260786237572370408687560441727006035326226907571046644765565610826295450225945821689766113946084926436173485860032840000964523515885271737730095253157325021312893152796246718141576145498964466082789239458535219584103497743580035241118781706960333496399469040697857641019083062655105934801391066722947827783153125)#(10652421913510213733898407083420012913520344863420275587860254841070206042654275053211239601233990813544801557039628247004768110951082434032072365979905419580587655195775106519963774511263809230729529345878113187715691336518180342419923881592311850124427434616938294137618896157525426696073050860327859392612474295413649439400913925656013708636956880301351141496628302550147680567001131206431473664)) (FloverMap.add e8 (((1138489)#(25), (5322249)#(25)), (386016739293039129357381964239803461348537618308829254644034741686921309846763562236550650398450203284331927422628136288220741271295481)#(2438866054934368930766872835775911176366092298957008711608716374707321670952941890718989143018353102468614789938598924137068730999443972895539200)) (FloverMap.add e7 (((1067)#(5), (2307)#(5)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e7 (((1067)#(5), (2307)#(5)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e6 (((-7228000)#(1), (-6268)#(1)), (3035133155978965067333019855358048910502028922472741755023387525129375)#(926336713898529563388567880069503262826159877325124512315660672063305037119488)) (FloverMap.add v1 (((20)#(1), (20000)#(1)), (625)#(281474976710656)) (FloverMap.add UMint15 (((-1807)#(5), (-1567)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add FMA5 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add C34 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.add T2 (((-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C12 (((3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.empty (intv * error))))))))))))))))))).
Definition querymap_doppler :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_doppler_sound :
CertificateChecker Let10 absenv_doppler thePrecondition_doppler querymap_doppler subdivs_doppler defVars_doppler= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
Definition C34 :expr Q := Const M64 ((1657)#(5)).
Definition FMA5mult :expr Q := Binop Mult C12 T2.
Definition FMA5 :expr Q := Fma C12 T2 C34.
Definition t15 :expr Q := Var Q 5.
Definition UMint15 :expr Q := Unop Neg t15.
Definition v1 :expr Q := Var Q 1.
Definition e6 :expr Q := Binop Mult UMint15 v1.
Definition u0 :expr Q := Var Q 0.
Definition e7 :expr Q := Binop Plus t15 u0.
Definition e8 :expr Q := Binop Mult e7 e7.
Definition e9 :expr Q := Binop Div e6 e8.
Definition Let10 := Let M64 5 FMA5 e9.
Definition defVars_doppler: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 5) (M64) (FloverMap.add (Var Q 2) (M64) (FloverMap.empty mType))))).
Definition subdivs_doppler: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_doppler :=
(FloverMap.add T2 ((-30)#(1), (50)#(1)) (FloverMap.add v1 ((20)#(1), (20000)#(1)) (FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv))),
(AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ)).
Definition absenv_doppler: analysisResult :=
FloverMap.add Let10 (((-9223372036854775323)#(67009023665787196), (-5384171002265600)#(159863851257405257)), (6395146761044357765503690801371276441765368447015101151813296635119433028390557896565475544956496553833459191531639848229164847988961573864464670748776813353525138213843738842546201283089853904954629246749165169810621322980144875026220656880567564902052374804615727126723160410736986845127244991996621049078998530821579057621625396893839494221224899982880254084100240465023731783153125)#(10652421913510219219409264963744548661917487941121320395994513318430551904512362747199924221778332168092965488723607243456011259465287188475318845213631543374252546820055908805724854791821012630200619036164098945114325414650541776464238357256998182652973892059080760766652998114554695566408635758783296967862860271493631237713524640412280353981040909615148658257257365203796839224604304840970993664)) (FloverMap.add e9 (((-9223372036854775323)#(67009023665787196), (-5384171002265600)#(159863851257405257)), (6395146761044357765503690801371276441765368447015101151813296635119433028390557896565475544956496553833459191531639848229164847988961573864464670748776813353525138213843738842546201283089853904954629246749165169810621322980144875026220656880567564902052374804615727126723160410736986845127244991996621049078998530821579057621625396893839494221224899982880254084100240465023731783153125)#(10652421913510219219409264963744548661917487941121320395994513318430551904512362747199924221778332168092965488723607243456011259465287188475318845213631543374252546820055908805724854791821012630200619036164098945114325414650541776464238357256998182652973892059080760766652998114554695566408635758783296967862860271493631237713524640412280353981040909615148658257257365203796839224604304840970993664)) (FloverMap.add e8 (((1138489)#(25), (159863851257405257)#(858993459200)), (357420066689505453360604417031945985271053151583235238178647155606033671479078134881359541739295517978633657744644427266878325030655481)#(2438866054934368930766872835775911176366092298957008711608716374707321670952941890718989143018353102468614789938598924137068730999443972895539200)) (FloverMap.add e7 (((1067)#(5), (8835207)#(20480)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e7 (((1067)#(5), (8835207)#(20480)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e6 (((-7228000)#(1), (-6268)#(1)), (3035133155978965067333019855358048910502028922472741755023387525129375)#(926336713898529563388567880069503262826159877325124512315660672063305037119488)) (FloverMap.add v1 (((20)#(1), (20000)#(1)), (625)#(281474976710656)) (FloverMap.add UMint15 (((-1807)#(5), (-1567)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add FMA5 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add C34 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.add T2 (((-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C12 (((3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.empty (intv * error))))))))))))))))))).
Definition querymap_doppler :=
FloverMap.add Let10 ((AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (DivQ (TimesQ (UMinusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5))))) (VarQ 1)) (TimesQ (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)))) (ConstQ ((-9223372036854775323)#(67009023665787196)))) TrueQ)), FalseQ) (FloverMap.add e9 ((AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (DivQ (TimesQ (UMinusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5))))) (VarQ 1)) (TimesQ (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)))) (ConstQ ((-9223372036854775323)#(67009023665787196)))) TrueQ)), FalseQ) (FloverMap.add e8 (FalseQ, (AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (ConstQ ((159863851257405257)#(858993459200))) (TimesQ (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)))) TrueQ))) (FloverMap.add e7 (FalseQ, (AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (ConstQ ((8835207)#(20480))) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0))) TrueQ))) (FloverMap.add e7 (FalseQ, (AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (ConstQ ((8835207)#(20480))) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0))) TrueQ))) (FloverMap.empty (SMTLogic * SMTLogic)))))).
Theorem ErrorBound_doppler_sound :
CertificateChecker Let10 absenv_doppler thePrecondition_doppler querymap_doppler subdivs_doppler defVars_doppler= true.
Proof. vm_compute; auto. Qed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
Require Import Flover.CertificateChecker.
Definition x10 :expr Q := Var Q 0.
Definition e1 :expr Q := Binop Mult x10 x10.
Definition x21 :expr Q := Var Q 1.
Definition e2 :expr Q := Binop Plus e1 x21.
Definition t14 :expr Q := Var Q 4.
Definition e3 :expr Q := Binop Mult x21 x21.
Definition e4 :expr Q := Binop Plus x10 e3.
Definition t25 :expr Q := Var Q 5.
Definition C56 :expr Q := Const M64 ((11)#(1)).
Definition e7 :expr Q := Binop Sub t14 C56.
Definition e8 :expr Q := Binop Mult e7 e7.
Definition C910 :expr Q := Const M64 ((7)#(1)).
Definition e11 :expr Q := Binop Sub t25 C910.
Definition e12 :expr Q := Binop Mult e11 e11.
Definition e13 :expr Q := Binop Plus e8 e12.
Definition Let14 := Let M64 5 e4 e13.
Definition Let15 := Let M64 4 e2 Let14.
Definition defVars_himmilbeau: FloverMap.t mType :=
(FloverMap.add (Var Q 5) (M64) (FloverMap.add (Var Q 4) (M64) (FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType))))).
Definition subdivs_himmilbeau: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_himmilbeau :=
(FloverMap.add x21 ((-5)#(1), (5)#(1)) (FloverMap.add x10 ((-5)#(1), (5)#(1)) (FloverMap.empty intv)),
TrueQ).
Definition absenv_himmilbeau: analysisResult :=
FloverMap.add Let15 (((-2539445)#(1073741824), (890)#(1)), (214326632700533617242861152656345650019577498247133528214421121374194110240108056161295111503685251789492904723213079331326398813638014683212103657629022558066392458762474278093425)#(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMap.add Let14 (((-2539445)#(1073741824), (890)#(1)), (214326632700533617242861152656345650019577498247133528214421121374194110240108056161295111503685251789492904723213079331326398813638014683212103657629022558066392458762474278093425)#(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMap.add e13 (((-2539445)#(1073741824), (890)#(1)), (214326632700533617242861152656345650019577498247133528214421121374194110240108056161295111503685251789492904723213079331326398813638014683212103657629022558066392458762474278093425)#(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMap.add e12 (((-391)#(65536), (529)#(1)), (24494476745446527224805203707196455287788610482184994605367511523865495355084763447144119690867611178754214656532304097974615641183339850168336901755850382009959025)#(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMap.add e11 (((-12)#(1), (23)#(1)), (921482552099875582371005419234933846549265058874253722785201258521)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C910 (((7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e11 (((-12)#(1), (23)#(1)), (921482552099875582371005419234933846549265058874253722785201258521)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C910 (((7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e8 (((-209)#(65536), (361)#(1)), (19967444739687434637754919059652361566527336890697100496795325241802486801511301449055543161938200539717368949324161383771403052570803743760393603174179185581097585)#(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMap.add e7 (((-16)#(1), (19)#(1)), (921482552099875585294008693896739682956634724306819762097066344473)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (((11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e7 (((-16)#(1), (19)#(1)), (921482552099875585294008693896739682956634724306819762097066344473)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (((11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add t25 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e4 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e3 (((0)#(1), (25)#(1)), (6084722881095501802724119491379225)#(730750818665451459101842416358141509827966271488)) (FloverMap.add x21 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add x21 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add x10 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add t14 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e2 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add x21 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add e1 (((0)#(1), (25)#(1)), (6084722881095501802724119491379225)#(730750818665451459101842416358141509827966271488)) (FloverMap.add x10 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add x10 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.empty (intv * error)))))))))))))))))))))))))))))).
Definition querymap_himmilbeau :=
FloverMap.add Let15 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (PlusQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))))) (ConstQ ((-2539445)#(1073741824)))) TrueQ)), FalseQ) (FloverMap.add Let14 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (PlusQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))))) (ConstQ ((-2539445)#(1073741824)))) TrueQ)), FalseQ) (FloverMap.add e13 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (PlusQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))))) (ConstQ ((-2539445)#(1073741824)))) TrueQ)), FalseQ) (FloverMap.add e12 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1))))) (ConstQ ((-391)#(65536)))) TrueQ)), FalseQ) (FloverMap.add e8 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (ConstQ ((-209)#(65536)))) TrueQ)), FalseQ) (FloverMap.add e3 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (VarQ 1) (VarQ 1)) (ConstQ ((0)#(1)))) TrueQ)), FalseQ) (FloverMap.add e1 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (VarQ 0) (VarQ 0)) (ConstQ ((0)#(1)))) TrueQ)), FalseQ) (FloverMap.empty (SMTLogic * SMTLogic)))))))).
Theorem ErrorBound_himmilbeau_sound :
CertificateChecker Let15 absenv_himmilbeau thePrecondition_himmilbeau querymap_himmilbeau subdivs_himmilbeau defVars_himmilbeau= true.
Proof. vm_compute; auto. Qed.
This diff is collapsed.
This diff is collapsed.
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