module SMT.Tests.SystemsRendering where

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

open import SMT.Core
open import SMT.Examples.Systems

valid-queue-step-preserves-bounds-renders :
  counterexampleCheckSMT valid-queue-step-preserves-bounds ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const enq Bool)\n" ++s
  "(declare-const deq Bool)\n" ++s
  "(declare-const q Int)\n" ++s
  "(declare-const cap Int)\n" ++s
  "(declare-const qNext Int)\n" ++s
  "(assert (<= 0 q))\n" ++s
  "(assert (<= q cap))\n" ++s
  "(assert (<= 0 cap))\n" ++s
  "(assert (=> enq (< q cap)))\n" ++s
  "(assert (=> deq (> q 0)))\n" ++s
  "(assert (= qNext (- (+ q (ite enq 1 0)) (ite deq 1 0))))\n" ++s
  "(assert (not (and (<= 0 qNext) (<= qNext cap))))\n" ++s
  "(check-sat)\n"
valid-queue-step-preserves-bounds-renders = refl

valid-scheduled-tasks-are-nonoverlapping-and-finish-renders :
  counterexampleCheckSMT valid-scheduled-tasks-are-nonoverlapping-and-finish ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const orderAB Bool)\n" ++s
  "(declare-const startA Int)\n" ++s
  "(declare-const durA Int)\n" ++s
  "(declare-const startB Int)\n" ++s
  "(declare-const durB Int)\n" ++s
  "(declare-const deadline Int)\n" ++s
  "(assert (<= 0 startA))\n" ++s
  "(assert (<= 0 startB))\n" ++s
  "(assert (<= 0 durA))\n" ++s
  "(assert (<= 0 durB))\n" ++s
  "(assert (=> orderAB (<= (+ startA durA) startB)))\n" ++s
  "(assert (=> (not orderAB) (<= (+ startB durB) startA)))\n" ++s
  "(assert (<= (+ startA durA) deadline))\n" ++s
  "(assert (<= (+ startB durB) deadline))\n" ++s
  "(assert (not (and (or (<= (+ startA durA) startB) (<= (+ startB durB) startA)) (and (<= (+ startA durA) deadline) (<= (+ startB durB) deadline)))))\n" ++s
  "(check-sat)\n"
valid-scheduled-tasks-are-nonoverlapping-and-finish-renders = refl