; GraphAtlas proof WL-01
; Statement: For every vehicle inside the family, the interpolated CO2 lies between the CO2 of the low vehicle and the CO2 of the high vehicle.
; About: interpolateCo2 in src/kernel/wltp.ts, as a statement about real numbers. The weight is defined by weight times (energy_high minus energy_low) equals (energy_individual minus energy_low), the quotient the code computes. The function counts a vehicle within a trillionth of the span of an end as inside and clamps to the interval, so rounding cannot leave it.
; Source: Regulation (EU) 2017/1151, Annex XXI, Sub-Annex 7, paragraph 3.2.3.2.4
; Expected: unsat for each of the 3 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun energy_high () Real)
(declare-fun energy_low () Real)
(declare-fun energy_individual () Real)
(declare-fun weight () Real)
(declare-fun co2_high () Real)
(declare-fun co2_low () Real)
(assert (< energy_low energy_high))
(assert (>= energy_individual energy_low))
(assert (<= energy_individual (+ energy_high 0.0)))
(assert (= (* weight (- energy_high energy_low)) (- energy_individual energy_low)))

; Lemma 1, negated
(push 1)
(assert (not (and (>= weight 0.0) (<= weight 1.0))))
(check-sat)
(pop 1)
; Lemma 1 holds, so later checks may use it
(assert (and (>= weight 0.0) (<= weight 1.0)))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (>= (+ co2_low (* weight 1.0 (- co2_high co2_low))) co2_low)) (a!2 (<= (+ co2_low (* weight 1.0 (- co2_high co2_low))) co2_high))) (=> (<= co2_low co2_high) (and a!1 a!2)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (>= (+ co2_low (* weight 1.0 (- co2_high co2_low))) co2_high)) (a!2 (<= (+ co2_low (* weight 1.0 (- co2_high co2_low))) co2_low))) (=> (> co2_low co2_high) (and a!1 a!2)))))
(check-sat)
(pop 1)