module SMT.Tests.Rendering where

open import Agda.Builtin.String using (String)

open import Cubical.Foundations.Prelude using (_≡_; refl)
open import Cubical.Data.Bool.Base using (false)
open import Cubical.Data.Int.Base using (negsuc)
open import Cubical.Data.List.Base using ([])

open import SMT.Core
open import SMT.Examples using (b₂; problem₁; problem₅; problem₆; problem₇; problem₉; x)

negative-int-renders-smtlib : exprSMT (int {Γ = []} (negsuc )) ≡ "(- 2)"
negative-int-renders-smtlib = refl

distinct-renders-smtlib : exprSMT (iNe x (int (negsuc ))) ≡ "(distinct x (- 1))"
distinct-renders-smtlib = refl

xor-renders-smtlib : exprSMT (bXor b₂ (bool false)) ≡ "(xor b false)"
xor-renders-smtlib = refl

problem₁-check-renders-smtlib :
  counterexampleCheckSMT problem₁ ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(assert (not (<= 0 (+ x 1))))\n" ++s
  "(check-sat)\n"
problem₁-check-renders-smtlib = refl

problem₁-query-renders-smtlib :
  counterexampleQuerySMT problem₁ ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(assert (not (<= 0 (+ x 1))))\n" ++s
  "(check-sat)\n" ++s
  "(get-model)\n"
problem₁-query-renders-smtlib = refl

problem₅-check-renders-smtlib :
  counterexampleCheckSMT problem₅ ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(declare-const x Int)\n" ++s
  "(assert (not (<= (ite b x 0) x)))\n" ++s
  "(check-sat)\n"
problem₅-check-renders-smtlib = refl

problem₆-check-renders-smtlib :
  counterexampleCheckSMT problem₆ ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(assert (and b true))\n" ++s
  "(assert (not b))\n" ++s
  "(check-sat)\n"
problem₆-check-renders-smtlib = refl

problem₇-check-renders-smtlib :
  counterexampleCheckSMT problem₇ ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const x Int)\n" ++s
  "(assert (>= x 0))\n" ++s
  "(assert (not (> x 0)))\n" ++s
  "(check-sat)\n"
problem₇-check-renders-smtlib = refl

problem₉-check-renders-smtlib :
  counterexampleCheckSMT problem₉ ≡
  "(set-logic QF_LIA)\n" ++s
  "(declare-const b Bool)\n" ++s
  "(assert (not (not (xor b b))))\n" ++s
  "(check-sat)\n"
problem₉-check-renders-smtlib = refl