module SMT.Unsafe.Tests.Showcase where

open import Agda.Builtin.String using (String)

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

open import SMT.Examples.Showcase
open import SMT.Unsafe.Z3

valid-clamp-between-check : String
valid-clamp-between-check = z3CounterexampleCheck valid-clamp-between

valid-clamp-between-check-ok : valid-clamp-between-check ≡ "unsat\n"
valid-clamp-between-check-ok = refl

invalid-clamp-between-unordered-check : String
invalid-clamp-between-unordered-check =
  z3CounterexampleCheck invalid-clamp-between-unordered

invalid-clamp-between-unordered-check-ok :
  invalid-clamp-between-unordered-check ≡ "sat\n"
invalid-clamp-between-unordered-check-ok = refl

valid-overlapping-interval-meet-check : String
valid-overlapping-interval-meet-check =
  z3CounterexampleCheck valid-overlapping-interval-meet

valid-overlapping-interval-meet-check-ok :
  valid-overlapping-interval-meet-check ≡ "unsat\n"
valid-overlapping-interval-meet-check-ok = refl

invalid-disjoint-interval-meet-check : String
invalid-disjoint-interval-meet-check =
  z3CounterexampleCheck invalid-disjoint-interval-meet

invalid-disjoint-interval-meet-check-ok :
  invalid-disjoint-interval-meet-check ≡ "sat\n"
invalid-disjoint-interval-meet-check-ok = refl

valid-absolute-difference-window-check : String
valid-absolute-difference-window-check =
  z3CounterexampleCheck valid-absolute-difference-window

valid-absolute-difference-window-check-ok :
  valid-absolute-difference-window-check ≡ "unsat\n"
valid-absolute-difference-window-check-ok = refl

valid-mode-selected-load-bounded-check : String
valid-mode-selected-load-bounded-check =
  z3CounterexampleCheck valid-mode-selected-load-bounded

valid-mode-selected-load-bounded-check-ok :
  valid-mode-selected-load-bounded-check ≡ "unsat\n"
valid-mode-selected-load-bounded-check-ok = refl

invalid-mode-selected-load-missing-both-case-check : String
invalid-mode-selected-load-missing-both-case-check =
  z3CounterexampleCheck invalid-mode-selected-load-missing-both-case

invalid-mode-selected-load-missing-both-case-check-ok :
  invalid-mode-selected-load-missing-both-case-check ≡ "sat\n"
invalid-mode-selected-load-missing-both-case-check-ok = refl

invalid-mode-selected-load-missing-y-nonnegative-check : String
invalid-mode-selected-load-missing-y-nonnegative-check =
  z3CounterexampleCheck invalid-mode-selected-load-missing-y-nonnegative

invalid-mode-selected-load-missing-y-nonnegative-check-ok :
  invalid-mode-selected-load-missing-y-nonnegative-check ≡ "sat\n"
invalid-mode-selected-load-missing-y-nonnegative-check-ok = refl