; GraphAtlas proof PQ-03
; Statement: A use that others wait for finishes no later than it would alone and no later than any of them can start, and no later finish does both. It starts strictly earlier than each of them, so a use that is late makes every use it waits for late too.
; About: The backward pass in plan in src/kernel/pqc.ts, for one use and two uses that wait for it. The pass takes the earliest of the use's own finish and the latest start of each dependent, and the latest start of a dependent is its finish less the years its migration takes, which is at least one. The dependents are taken as already settled, which the pass guarantees by walking the order backwards and which the check of every plan confirms by a second method (PQ-04). A third dependent adds nothing, because the earliest of three is the earliest of the earliest of two and the third.
; Source: The planning rule of this product, Latest finish, the backward pass of critical path scheduling
; Expected: unsat for each of the 8 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun own_finish () Int)
(declare-fun finish_first_dependent () Int)
(declare-fun finish_second_dependent () Int)
(declare-fun other_finish () Int)
(declare-fun years_to_migrate () Int)
(declare-fun years_to_migrate_first_dependent () Int)
(declare-fun years_to_migrate_second_dependent () Int)
(assert (>= own_finish (- 200)))
(assert (<= own_finish 200))
(assert (>= finish_first_dependent (- 200)))
(assert (<= finish_first_dependent 200))
(assert (>= finish_second_dependent (- 200)))
(assert (<= finish_second_dependent 200))
(assert (>= other_finish (- 200)))
(assert (<= other_finish 200))
(assert (>= years_to_migrate 1))
(assert (<= years_to_migrate 30))
(assert (>= years_to_migrate_first_dependent 1))
(assert (<= years_to_migrate_first_dependent 30))
(assert (>= years_to_migrate_second_dependent 1))
(assert (<= years_to_migrate_second_dependent 30))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (<= (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent)) own_finish))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (<= (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent)) (- finish_first_dependent years_to_migrate_first_dependent)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (<= (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent)) (- finish_second_dependent years_to_migrate_second_dependent)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (let ((a!2 (<= other_finish (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent))))) (=> (and (<= other_finish own_finish) (<= other_finish (- finish_first_dependent years_to_migrate_first_dependent)) (<= other_finish (- finish_second_dependent years_to_migrate_second_dependent))) a!2)))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (let ((a!2 (- (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent)) years_to_migrate))) (< a!2 (- finish_first_dependent years_to_migrate_first_dependent))))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (let ((a!2 (- (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent)) years_to_migrate))) (< a!2 (- finish_second_dependent years_to_migrate_second_dependent))))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (let ((a!2 (- (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent)) years_to_migrate))) (=> (< (- finish_first_dependent years_to_migrate_first_dependent) 0) (< a!2 0))))))
(check-sat)
(pop 1)

; Goal 8, negated
(push 1)
(assert (not (let ((a!1 (ite (<= own_finish (- finish_first_dependent years_to_migrate_first_dependent)) own_finish (- finish_first_dependent years_to_migrate_first_dependent)))) (let ((a!2 (- (ite (<= a!1 (- finish_second_dependent years_to_migrate_second_dependent)) a!1 (- finish_second_dependent years_to_migrate_second_dependent)) years_to_migrate))) (=> (< (- finish_second_dependent years_to_migrate_second_dependent) 0) (< a!2 0))))))
(check-sat)
(pop 1)