module SMT.Tests.ShowcaseRendering where

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

open import SMT.Core
open import SMT.Examples.Showcase

valid-clamp-between-renders :
  counterexampleCheckSMT valid-clamp-between ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const lo Int)\n" ++s
  "(declare-const hi Int)\n" ++s
  "(declare-const x Int)\n" ++s
  "(assert (<= lo hi))\n" ++s
  "(assert (not (and (<= lo (ite (<= hi (ite (<= lo x) x lo)) hi (ite (<= lo x) x lo))) (<= (ite (<= hi (ite (<= lo x) x lo)) hi (ite (<= lo x) x lo)) hi))))\n" ++s
  "(check-sat)\n"
valid-clamp-between-renders = refl

valid-overlapping-interval-meet-renders :
  counterexampleCheckSMT valid-overlapping-interval-meet ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const a Int)\n" ++s
  "(declare-const b Int)\n" ++s
  "(declare-const c Int)\n" ++s
  "(declare-const d Int)\n" ++s
  "(assert (<= a b))\n" ++s
  "(assert (<= c d))\n" ++s
  "(assert (not (or (< b c) (< d a))))\n" ++s
  "(assert (not (<= (ite (<= a c) c a) (ite (<= b d) b d))))\n" ++s
  "(check-sat)\n"
valid-overlapping-interval-meet-renders = refl

valid-absolute-difference-window-renders :
  counterexampleCheckSMT valid-absolute-difference-window ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const delta Int)\n" ++s
  "(assert (<= 0 delta))\n" ++s
  "(assert (<= (ite (>= (- x y) 0) (- x y) (- (- x y))) delta))\n" ++s
  "(assert (not (and (<= (- y delta) x) (<= x (+ y delta)))))\n" ++s
  "(check-sat)\n"
valid-absolute-difference-window-renders = refl

valid-mode-selected-load-bounded-renders :
  counterexampleCheckSMT valid-mode-selected-load-bounded ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const p Bool)\n" ++s
  "(declare-const q Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const z Int)\n" ++s
  "(declare-const cap Int)\n" ++s
  "(assert (<= 0 z))\n" ++s
  "(assert (=> p (<= 0 x)))\n" ++s
  "(assert (=> q (<= 0 y)))\n" ++s
  "(assert (=> (and p q) (<= (+ (+ x y) z) cap)))\n" ++s
  "(assert (=> (and p (not q)) (<= (+ x z) cap)))\n" ++s
  "(assert (=> (and (not p) q) (<= (+ y z) cap)))\n" ++s
  "(assert (=> (and (not p) (not q)) (<= z cap)))\n" ++s
  "(assert (not (and (<= 0 (+ (+ (ite p x 0) (ite q y 0)) z)) (<= (+ (+ (ite p x 0) (ite q y 0)) z) cap))))\n" ++s
  "(check-sat)\n"
valid-mode-selected-load-bounded-renders = refl

invalid-mode-selected-load-missing-both-case-renders :
  counterexampleCheckSMT invalid-mode-selected-load-missing-both-case ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const p Bool)\n" ++s
  "(declare-const q Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const z Int)\n" ++s
  "(declare-const cap Int)\n" ++s
  "(assert (<= 0 z))\n" ++s
  "(assert (=> p (<= 0 x)))\n" ++s
  "(assert (=> q (<= 0 y)))\n" ++s
  "(assert (=> (and p (not q)) (<= (+ x z) cap)))\n" ++s
  "(assert (=> (and (not p) q) (<= (+ y z) cap)))\n" ++s
  "(assert (=> (and (not p) (not q)) (<= z cap)))\n" ++s
  "(assert (not (and (<= 0 (+ (+ (ite p x 0) (ite q y 0)) z)) (<= (+ (+ (ite p x 0) (ite q y 0)) z) cap))))\n" ++s
  "(check-sat)\n"
invalid-mode-selected-load-missing-both-case-renders = refl