module SMT.Tests.ProgressiveRendering where

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

open import SMT.Core
open import SMT.Examples.Progressive

valid-demorgan-renders :
  counterexampleCheckSMT valid-demorgan ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const p Bool)\n" ++s
  "(declare-const q Bool)\n" ++s
  "(assert (not (= (not (and p q)) (or (not p) (not q)))))\n" ++s
  "(check-sat)\n"
valid-demorgan-renders = refl

valid-linear-chain-equality-renders :
  counterexampleCheckSMT valid-linear-chain-equality ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const z Int)\n" ++s
  "(assert (= x (+ y 2)))\n" ++s
  "(assert (= y (+ z 3)))\n" ++s
  "(assert (not (= x (+ z 5))))\n" ++s
  "(check-sat)\n"
valid-linear-chain-equality-renders = refl

valid-guarded-ite-nonnegative-renders :
  counterexampleCheckSMT valid-guarded-ite-nonnegative ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (=> b (>= x 0)))\n" ++s
  "(assert (=> (not b) (>= y 0)))\n" ++s
  "(assert (not (>= (ite b x y) 0)))\n" ++s
  "(check-sat)\n"
valid-guarded-ite-nonnegative-renders = refl

invalid-negative-scale-monotone-renders :
  counterexampleCheckSMT invalid-negative-scale-monotone ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (<= x y))\n" ++s
  "(assert (not (<= (* (- 1) x) (* (- 1) y))))\n" ++s
  "(check-sat)\n"
invalid-negative-scale-monotone-renders = refl

invalid-linear-offset-cancel-renders :
  counterexampleCheckSMT invalid-linear-offset-cancel ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(declare-const z Int)\n" ++s
  "(assert (= (+ x y) z))\n" ++s
  "(assert (not (= x z)))\n" ++s
  "(check-sat)\n"
invalid-linear-offset-cancel-renders = refl

valid-nested-boolean-guard-renders :
  counterexampleCheckSMT valid-nested-boolean-guard ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(declare-const y Int)\n" ++s
  "(assert (or b (not b)))\n" ++s
  "(assert (=> b (> x 0)))\n" ++s
  "(assert (=> (not b) (> y 0)))\n" ++s
  "(assert (not (> (ite b x y) 0)))\n" ++s
  "(check-sat)\n"
valid-nested-boolean-guard-renders = refl