Commit 68a14034 authored by Joachim Bard's avatar Joachim Bard

checker function returns false for testcases

precondition part of the queries is mixed up
parent ff0f8d41
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
Require Import Flover.SMTValidation.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition C34 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
Definition e5 :expr Q := Binop Mult C34 T2.
Definition e6 :expr Q := Binop Plus C12 e5.
Definition UMine6 :expr Q := Unop Neg e6.
Definition v1 :expr Q := Var Q 1.
Definition e7 :expr Q := Binop Mult UMine6 v1.
Definition u0 :expr Q := Var Q 0.
Definition e8 :expr Q := Binop Plus e6 u0.
Definition e9 :expr Q := Binop Mult e8 e8.
Definition e10 :expr Q := Binop Div e7 e9.
Definition Rete10 := Ret e10.
Definition defVars_doppler :FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 2) (M64) (FloverMap.empty mType)))).
Definition thePrecondition_doppler :=
FloverMap.add u0 (-100#1, 100#1) (FloverMap.add v1 (20#1, 20000#1) (FloverMap.add T2 (-30#1, 50#1) (FloverMap.empty intv))).
Definition absenv_doppler :analysisResult := Eval compute in
FloverMap.add e10 (( (-26688776647036775)#(193898302136352), (-156700)#(5322249)), (4539010972026683303050120095327512216096422204478916695616374703820945778271922835308820707992089065905809072803102359543119833046473491986173951465620708023920966108209278836911630406540351629664583258832952458474781714583641201336156211255871250258363339134573360321968683520123662731962148793248799126762059670142230384240259443958280927316219469399605577522382054092479955357491038836701067526006061330750371234271363459989977730726293112263204327432621633884375)#(6946881575336902398274073006442580695940363163353906376754739965735202698392559846418891988118801115081550268650112893004414138824905360424712176030962427176970330198413894472430113124972848478861036028596232644451943248527831305533814306762870254280021814184312793167557111190875651884658457951357503922164630579910655264970400579248413892869201129019278339105434841776095040929995238102957547326071498788437802549670716277097027061404357118143901490561892403102252934918832128)) (FloverMap.add e9 (( (1138489)#(25), (5322249)#(25)), (31925542667783538931925887764808218521724458943918984144150813990256848378453146446353514550378395469015865480921312990060616935650290296361584748492021295664945174009)#(197864321178483627248402016815717752028105079280969471931250444874317780085225493736253120848994435991678137140812911471481092027445400967974036924081514534333285417718959308800)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (22118872259511654165679074210367094250583915178799247531173589549131)#(148213874223764730142170860811120522052185580372019921970505707530128805939118080)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add e6 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e5 (( (-18)#(1), (30)#(1)), (3650833728657301081634471694827535)#(365375409332725729550921208179070754913983135744)) (FloverMap.add T2 (( (-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C34 (( (3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (22118872259511654165679074210367094250583915178799247531173589549131)#(148213874223764730142170860811120522052185580372019921970505707530128805939118080)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add e6 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e5 (( (-18)#(1), (30)#(1)), (3650833728657301081634471694827535)#(365375409332725729550921208179070754913983135744)) (FloverMap.add T2 (( (-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C34 (( (3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.add e7 (( (-7228000)#(1), (-6268)#(1)), (27893851128912527228254446719689338467872526596253813879482502889568449178778992649375)#(8343699359066055009355553539724812947666814540455674882605631280555545803830627148527195652096)) (FloverMap.add v1 (( (20)#(1), (20000)#(1)), (625)#(281474976710656)) (FloverMap.add UMine6 (( (-1807)#(5), (-1567)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e6 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e5 (( (-18)#(1), (30)#(1)), (3650833728657301081634471694827535)#(365375409332725729550921208179070754913983135744)) (FloverMap.add T2 (( (-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C34 (( (3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error))))))))))))))))))))))))).
Definition querymap_doppler :=
FloverMap.add e10 ((AndQ (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) TrueQ)))))) (AndQ (LessQ (DivQ (TimesQ (UMinusQ (PlusQ (ConstQ ((1657)#(5))) (TimesQ (ConstQ ((3)#(5))) (VarQ 2)))) (VarQ 1)) (TimesQ (PlusQ (PlusQ (ConstQ ((1657)#(5))) (TimesQ (ConstQ ((3)#(5))) (VarQ 2))) (VarQ 0)) (PlusQ (PlusQ (ConstQ ((1657)#(5))) (TimesQ (ConstQ ((3)#(5))) (VarQ 2))) (VarQ 0)))) (ConstQ ((-26688776647036775)#(193898302136352)))) TrueQ)), FalseQ) (FloverMap.empty (SMTLogic * SMTLogic)).
Theorem test_validation :
validSMTIntervalbounds e10 absenv_doppler thePrecondition_doppler querymap_doppler NatSet.empty = true.
Proof.
cbv.
Abort.
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
Require Import Flover.SMTValidation.
Definition x0 :expr Q := Var Q 0.
Definition y1 :expr Q := Var Q 1.
Definition e1 :expr Q := Binop Plus x0 y1.
......@@ -21,6 +22,11 @@ FloverMap.add e5 (( (29)#(10), (75821)#(10240)), (316565750324396041763684170206
Definition querymap_fnc1 :=
FloverMap.add e2 (FalseQ, (AndQ (AndQ (LessEqQ (VarQ 0) (ConstQ ((6)#(1)))) (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) TrueQ)))) (AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))) TrueQ))) (FloverMap.empty (SMTLogic * SMTLogic)).
Theorem test_validation :
validSMTIntervalbounds e5 absenv_fnc1 thePrecondition_fnc1 querymap_fnc1 NatSet.empty = true.
Proof.
cbv.
Abort.
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import RealRangeArith.
......@@ -40,28 +46,22 @@ Definition hiQ :=
Definition query := hiQ.
Definition prec :=
match query with
| AndQ q _ => q
| _ => TrueQ
end.
Definition prec := optionBind (getPrecond query) (fun q => q) TrueQ.
Definition prec_reorder :=
Definition prec_reorder := precond2SMT thePrecondition_fnc1.
(*
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 _ (AndQ q _) => q
| _ => TrueQ
end.
Definition bound := optionBind (getBound query) (fun q => q) TrueQ.
Lemma prec_bound_correct E :
eval_smt_logic E query <-> eval_smt_logic E (AndQ prec_reorder bound).
Proof.
cbn; tauto.
cbv. tauto.
Qed.
Definition bound_expr :=
......
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