module SMT.Unsafe.Tests.Systems where

open import Agda.Builtin.String using (String)

open import Cubical.Foundations.Prelude using (_≡_; refl)

open import SMT.Examples.Systems
open import SMT.Unsafe.Z3

valid-queue-step-preserves-bounds-check : String
valid-queue-step-preserves-bounds-check =
  z3CounterexampleCheck valid-queue-step-preserves-bounds

valid-queue-step-preserves-bounds-check-ok :
  valid-queue-step-preserves-bounds-check ≡ "unsat\n"
valid-queue-step-preserves-bounds-check-ok = refl

invalid-queue-step-missing-dequeue-guard-check : String
invalid-queue-step-missing-dequeue-guard-check =
  z3CounterexampleCheck invalid-queue-step-missing-dequeue-guard

invalid-queue-step-missing-dequeue-guard-check-ok :
  invalid-queue-step-missing-dequeue-guard-check ≡ "sat\n"
invalid-queue-step-missing-dequeue-guard-check-ok = refl

invalid-queue-step-missing-enqueue-guard-check : String
invalid-queue-step-missing-enqueue-guard-check =
  z3CounterexampleCheck invalid-queue-step-missing-enqueue-guard

invalid-queue-step-missing-enqueue-guard-check-ok :
  invalid-queue-step-missing-enqueue-guard-check ≡ "sat\n"
invalid-queue-step-missing-enqueue-guard-check-ok = refl

valid-scheduled-tasks-are-nonoverlapping-and-finish-check : String
valid-scheduled-tasks-are-nonoverlapping-and-finish-check =
  z3CounterexampleCheck valid-scheduled-tasks-are-nonoverlapping-and-finish

valid-scheduled-tasks-are-nonoverlapping-and-finish-check-ok :
  valid-scheduled-tasks-are-nonoverlapping-and-finish-check ≡ "unsat\n"
valid-scheduled-tasks-are-nonoverlapping-and-finish-check-ok = refl

invalid-schedule-missing-second-order-case-check : String
invalid-schedule-missing-second-order-case-check =
  z3CounterexampleCheck invalid-schedule-missing-second-order-case

invalid-schedule-missing-second-order-case-check-ok :
  invalid-schedule-missing-second-order-case-check ≡ "sat\n"
invalid-schedule-missing-second-order-case-check-ok = refl

valid-quorum-three-gives-pairwise-coverage-check : String
valid-quorum-three-gives-pairwise-coverage-check =
  z3CounterexampleCheck valid-quorum-three-gives-pairwise-coverage

valid-quorum-three-gives-pairwise-coverage-check-ok :
  valid-quorum-three-gives-pairwise-coverage-check ≡ "unsat\n"
valid-quorum-three-gives-pairwise-coverage-check-ok = refl

invalid-quorum-two-gives-pairwise-coverage-check : String
invalid-quorum-two-gives-pairwise-coverage-check =
  z3CounterexampleCheck invalid-quorum-two-gives-pairwise-coverage

invalid-quorum-two-gives-pairwise-coverage-check-ok :
  invalid-quorum-two-gives-pairwise-coverage-check ≡ "sat\n"
invalid-quorum-two-gives-pairwise-coverage-check-ok = refl