fact: Definition generateCProp {Tl T} (t : ArithExpr Tl T) md vars hyps := let (tointerval, unsolvable) := extractCProp t md in let tointerval := BTreeToList tointerval in let lexpr := map (fun p => CArithExprToTree (getCArithExpr p)) tointerval in match extract_list lexpr vars with | Eabort => merge tointerval unsolvable | Eprog prog consts => let goals := map (fun p => AtomToGoal p) tointerval in let ieval := fun xi => IH.A.BndValuator.eval prec prog xi in let bounds := IH.compute_inputs prec hyps consts in let results := ieval bounds in let compared := compareResults goals results in par_mergerest tointerval compared unsolvable 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