module SMT.Examples.Systems where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool.Base using (true; false)
open import Cubical.Data.Int.Base using (ℤ; negsuc; pos)
open import Cubical.Data.List.Base using (List; []; _∷_)
open import Cubical.Data.Unit.Base using (tt)
open import Cubical.Relation.Nullary.Base using (¬_)

open import SMT.Core
open import SMT.Derived
open import SMT.Syntax

z4 z10 : ℤ
z4 = pos 
z10 = pos 

minusOne : ℤ
minusOne = negsuc 

Gqueue : Ctx
Gqueue =
  decl "enq" sBool ∷
  decl "deq" sBool ∷
  decl "q" sInt ∷
  decl "cap" sInt ∷
  decl "qNext" sInt ∷
  []

enqQ : Expr Gqueue sBool
enqQ = var vz

deqQ : Expr Gqueue sBool
deqQ = var (vs vz)

qQ : Expr Gqueue sInt
qQ = var (vs (vs vz))

capQ : Expr Gqueue sInt
capQ = var (vs (vs (vs vz)))

qNextQ : Expr Gqueue sInt
qNextQ = var (vs (vs (vs (vs vz))))

queue-next-computed : Expr Gqueue sInt
queue-next-computed =
  qQ +ᵢ indicator enqQ -ᵢ indicator deqQ

queue-common-assumptions : List (Expr Gqueue sBool)
queue-common-assumptions =
  int0 ≤ᵢ qQ
  ∷ qQ ≤ᵢ capQ
  ∷ int0 ≤ᵢ capQ
  ∷ qNextQ ≡ᵢ queue-next-computed
  ∷ []

valid-queue-step-preserves-bounds : Problem Gqueue
valid-queue-step-preserves-bounds =
  ( int0 ≤ᵢ qQ
    ∷ qQ ≤ᵢ capQ
    ∷ int0 ≤ᵢ capQ
    ∷ enqQ ⇒ᵇ qQ <ᵢ capQ
    ∷ deqQ ⇒ᵇ qQ >ᵢ int0
    ∷ qNextQ ≡ᵢ queue-next-computed
    ∷ []
  )
  ⊢ [ int0 ≤ᵢ qNextQ ≤ᵢ capQ ]

invalid-queue-step-missing-dequeue-guard : Problem Gqueue
invalid-queue-step-missing-dequeue-guard =
  ( int0 ≤ᵢ qQ
    ∷ qQ ≤ᵢ capQ
    ∷ int0 ≤ᵢ capQ
    ∷ enqQ ⇒ᵇ qQ <ᵢ capQ
    ∷ qNextQ ≡ᵢ queue-next-computed
    ∷ []
  )
  ⊢ [ int0 ≤ᵢ qNextQ ≤ᵢ capQ ]

invalid-queue-step-missing-dequeue-guard-counterexample :
  Counterexample invalid-queue-step-missing-dequeue-guard
invalid-queue-step-missing-dequeue-guard-counterexample =
  counterexample
    (false , (true , (z0 , (z0 , (minusOne , tt)))))
    ( refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷ all[]))))
    )
    refl

not-invalid-queue-step-missing-dequeue-guard :
  ¬ Statement invalid-queue-step-missing-dequeue-guard
not-invalid-queue-step-missing-dequeue-guard =
  refute invalid-queue-step-missing-dequeue-guard-counterexample

invalid-queue-step-missing-enqueue-guard : Problem Gqueue
invalid-queue-step-missing-enqueue-guard =
  ( int0 ≤ᵢ qQ
    ∷ qQ ≤ᵢ capQ
    ∷ int0 ≤ᵢ capQ
    ∷ deqQ ⇒ᵇ qQ >ᵢ int0
    ∷ qNextQ ≡ᵢ queue-next-computed
    ∷ []
  )
  ⊢ [ int0 ≤ᵢ qNextQ ≤ᵢ capQ ]

invalid-queue-step-missing-enqueue-guard-counterexample :
  Counterexample invalid-queue-step-missing-enqueue-guard
invalid-queue-step-missing-enqueue-guard-counterexample =
  counterexample
    (true , (false , (z0 , (z0 , (z1 , tt)))))
    ( refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷ all[]))))
    )
    refl

not-invalid-queue-step-missing-enqueue-guard :
  ¬ Statement invalid-queue-step-missing-enqueue-guard
not-invalid-queue-step-missing-enqueue-guard =
  refute invalid-queue-step-missing-enqueue-guard-counterexample

Gschedule : Ctx
Gschedule =
  decl "orderAB" sBool ∷
  decl "startA" sInt ∷
  decl "durA" sInt ∷
  decl "startB" sInt ∷
  decl "durB" sInt ∷
  decl "deadline" sInt ∷
  []

orderAB : Expr Gschedule sBool
orderAB = var vz

startA : Expr Gschedule sInt
startA = var (vs vz)

durA : Expr Gschedule sInt
durA = var (vs (vs vz))

startB : Expr Gschedule sInt
startB = var (vs (vs (vs vz)))

durB : Expr Gschedule sInt
durB = var (vs (vs (vs (vs vz))))

deadline : Expr Gschedule sInt
deadline = var (vs (vs (vs (vs (vs vz)))))

endA : Expr Gschedule sInt
endA = startA +ᵢ durA

endB : Expr Gschedule sInt
endB = startB +ᵢ durB

tasks-do-not-overlap : Expr Gschedule sBool
tasks-do-not-overlap = endA ≤ᵢ startB ∨ᵇ endB ≤ᵢ startA

tasks-finish-by-deadline : Expr Gschedule sBool
tasks-finish-by-deadline = endA ≤ᵢ deadline ∧ᵇ endB ≤ᵢ deadline

valid-scheduled-tasks-are-nonoverlapping-and-finish : Problem Gschedule
valid-scheduled-tasks-are-nonoverlapping-and-finish =
  ( int0 ≤ᵢ startA
    ∷ int0 ≤ᵢ startB
    ∷ int0 ≤ᵢ durA
    ∷ int0 ≤ᵢ durB
    ∷ orderAB ⇒ᵇ endA ≤ᵢ startB
    ∷ ¬ᵇ orderAB ⇒ᵇ endB ≤ᵢ startA
    ∷ endA ≤ᵢ deadline
    ∷ endB ≤ᵢ deadline
    ∷ []
  )
  ⊢ tasks-do-not-overlap ∧ᵇ tasks-finish-by-deadline

invalid-schedule-missing-second-order-case : Problem Gschedule
invalid-schedule-missing-second-order-case =
  ( int0 ≤ᵢ startA
    ∷ int0 ≤ᵢ startB
    ∷ int0 ≤ᵢ durA
    ∷ int0 ≤ᵢ durB
    ∷ orderAB ⇒ᵇ endA ≤ᵢ startB
    ∷ endA ≤ᵢ deadline
    ∷ endB ≤ᵢ deadline
    ∷ []
  )
  ⊢ tasks-do-not-overlap

invalid-schedule-missing-second-order-case-counterexample :
  Counterexample invalid-schedule-missing-second-order-case
invalid-schedule-missing-second-order-case-counterexample =
  counterexample
    (false , (z0 , (z2 , (z1 , (z2 , (z10 , tt))))))
    ( refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷ all[]))))))
    )
    refl

not-invalid-schedule-missing-second-order-case :
  ¬ Statement invalid-schedule-missing-second-order-case
not-invalid-schedule-missing-second-order-case =
  refute invalid-schedule-missing-second-order-case-counterexample

Gvotes : Ctx
Gvotes =
  decl "a" sBool ∷
  decl "b" sBool ∷
  decl "c" sBool ∷
  decl "d" sBool ∷
  []

voteA : Expr Gvotes sBool
voteA = var vz

voteB : Expr Gvotes sBool
voteB = var (vs vz)

voteC : Expr Gvotes sBool
voteC = var (vs (vs vz))

voteD : Expr Gvotes sBool
voteD = var (vs (vs (vs vz)))

votes : List (Expr Gvotes sBool)
votes = voteA ∷ voteB ∷ voteC ∷ voteD ∷ []

pairwise-covered : Expr Gvotes sBool
pairwise-covered =
  allBool
    ( voteA ∨ᵇ voteB
    ∷ voteA ∨ᵇ voteC
    ∷ voteA ∨ᵇ voteD
    ∷ voteB ∨ᵇ voteC
    ∷ voteB ∨ᵇ voteD
    ∷ voteC ∨ᵇ voteD
    ∷ []
    )

valid-quorum-three-gives-pairwise-coverage : Problem Gvotes
valid-quorum-three-gives-pairwise-coverage =
  (atLeast int3 votes ∷ []) ⊢ pairwise-covered

invalid-quorum-two-gives-pairwise-coverage : Problem Gvotes
invalid-quorum-two-gives-pairwise-coverage =
  (atLeast int2 votes ∷ []) ⊢ pairwise-covered

invalid-quorum-two-gives-pairwise-coverage-counterexample :
  Counterexample invalid-quorum-two-gives-pairwise-coverage
invalid-quorum-two-gives-pairwise-coverage-counterexample =
  counterexample
    (true , (true , (false , (false , tt))))
    (refl all∷ all[])
    refl

not-invalid-quorum-two-gives-pairwise-coverage :
  ¬ Statement invalid-quorum-two-gives-pairwise-coverage
not-invalid-quorum-two-gives-pairwise-coverage =
  refute invalid-quorum-two-gives-pairwise-coverage-counterexample