fact: Fixpoint decomposeToCProp {Tl T} (t : ArithExpr Tl T) vars md := match t with | Int _ n => (CInt n, true, Void, CTrue) | BinFl _ x => let f := Prim2B x in match f with | B754_zero _ => (CBinFl 0 0, true, Void, CTrue) | B754_finite s m e _ => (CBinFl (if s then Z.neg m else Z.pos m) e, true, Void, CTrue) | _ => (CInt 0%Z, false, Void, CTrue) end | Var _ n => let (u, b) := nth n vars (CInt 0%Z, false) in (u, b, Void, CTrue) | Op _ T'' OP t1 t2 => let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in let b := andb b1 b2 in let bt := Node (if b2 then match OP with | DIV => Leaf (NonZero u2) | _ => Void end else Void) (Node bt1 bt2) in let p := CAnd (if b2 then CTrue else match OP with | DIV => CAtom (NonZero u2) | _ => CTrue end) (CAnd p1 p2) in match T'' with | Integer => let t := COp (ArithOpToCArithOp T'' OP) u1 u2 in let bt' := Node (if b then Leaf (InInt32 t) else Void) bt in let p' := CAnd (if b then CTrue else CAtom (InInt32 t)) p in (t, b, bt', p') | BinFloat => let t := CRnd md (COp (ArithOpToCArithOp T'' OP) u1 u2) in let bt' := Node (if b then Leaf (InFloat64 t) else Void) bt in let p' := CAnd (if b then CTrue else CAtom (InFloat64 t)) p in (t, b, bt', p') end | OpExact _ OP t1 t2 => let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in let t := COp (ArithOpToCArithOp BinFloat OP) u1 u2 in let b := andb b1 b2 in let bt := Node (if b then match OP with | DIV => Node (Leaf (NonZero u2)) (Leaf (InFloat64 t)) | _ => Leaf (InFloat64 t) end else Void) (Node bt1 bt2) in let p := CAnd (CAnd (if b then CTrue else match OP with | DIV => CAnd (CAtom (NonZero u2)) (CAtom (InFloat64 t)) | _ => CAtom (InFloat64 t) end) (CAtom (RndExact md t))) (CAnd p1 p2) in (t, b, bt, p) | Fma _ t1 t2 t3 => let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in let '(u3, b3, bt3, p3) := decomposeToCProp t3 vars md in let t := CRnd md (COp CADD (COp CMUL u1 u2) u3) in let b := andb (andb b1 b2) b3 in let bt := Node (if b then Leaf (InFloat64 t) else Void) (Node (Node bt1 bt2) bt3) in let p := CAnd (if b then CTrue else CAtom (InFloat64 t)) (CAnd (CAnd p1 p2) p3) in (t, b, bt, p) | FmaExact _ t1 t2 t3 => let '(u1, b1, bt1, p1) := decomposeToCProp t1 vars md in let '(u2, b2, bt2, p2) := decomposeToCProp t2 vars md in let '(u3, b3, bt3, p3) := decomposeToCProp t3 vars md in let t := COp CADD (COp CMUL u1 u2) u3 in let b := andb (andb b1 b2) b3 in let bt := Node (if b then Leaf (InFloat64 t) else Void) (Node (Node bt1 bt2) bt3) in let p := CAnd (if b then CTrue else CAtom (InFloat64 t)) (CAnd (CAnd p1 p2) p3) in (t, b, bt, CAnd p (CAtom (RndExact md t))) | Nearbyint _ t => let '(u, b, bt, p) := decomposeToCProp t vars md in (CNearbyint u, b, bt, p) | FastNearbyint _ t => let '(u, b, bt, p) := decomposeToCProp t vars md in let t := CNearbyint u in let bt' := Node (if b then Leaf (InInt51 u) else Void) bt in let p' := CAnd (if b then CTrue else CAtom (InInt51 u)) p in (t, b, bt', p') | FastNearbyintToInt _ t => let '(u, b, bt, p) := decomposeToCProp t vars md in let t := CNearbyint u in let bt' := Node (if b then Leaf (InInt32 u) else Void) bt in let p' := CAnd (if b then CTrue else CAtom (InInt32 u)) p in (t, b, bt', p') | TruncToInt _ t => let '(u, b, bt, p) := decomposeToCProp t vars md in let t := CTrunc u in let bt' := Node (if b then Leaf (InInt32 t) else Void) bt in let p' := CAnd (if b then CTrue else CAtom (InInt32 t)) p in (t, b, bt', p') | FloatInj _ t => let '(u, b, bt, p) := decomposeToCProp t vars md in let bt' := Node (if b then Leaf (InFloat64Int u) else Void) bt in let p' := CAnd (if b then CTrue else CAtom (InFloat64Int u)) p in (u, b, bt', p') | Sqrt _ T'' t => let '(u, b, bt, p) := decomposeToCProp t vars md in let t := CSqrt u in let bt' := Node (if b then Leaf (NonNeg u) else Void) bt in let p' := CAnd (if b then CTrue else CAtom (NonNeg u)) p in match T'' with | Integer => (CTrunc t, b, bt', p') | BinFloat => (CRnd md t, b, bt', p') end | ArrayAcc _ _ _ => (CInt 0%Z, false, Void, CTrue) | Let _ _ _ t1 t2 => let '(u, b1, bt1, p1) := decomposeToCProp t1 vars md in let '(t, b2, bt2, p2) := decomposeToCProp t2 ((u, b1) :: vars) md in let b := b2 in let bt := Node bt2 bt1 in let p := CAnd p1 p2 in (t, b, bt, p) | Assert _ _ _ t | Postcond _ _ _ t => decomposeToCProp t vars md end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr