module SMT.Unsafe.Tests.Integration where

open import Agda.Builtin.String using (String)

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

open import SMT.Examples
  using (problem₁; problem₂; problem₄; problem₅; problem₆; problem₇; problem₈; problem₉)
open import SMT.Unsafe.Z3

raw-unsat-output : String
raw-unsat-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(assert false)\n" ++
      "(check-sat)\n"
    )

raw-unsat-output-ok : raw-unsat-output ≡ "unsat\n"
raw-unsat-output-ok = refl

raw-empty-model-output : String
raw-empty-model-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(assert true)\n" ++
      "(check-sat)\n" ++
      "(get-model)\n"
    )

raw-empty-model-output-ok : raw-empty-model-output ≡ "sat\n(\n)\n"
raw-empty-model-output-ok = refl

problem₁-z3-check-output : String
problem₁-z3-check-output = z3CounterexampleCheck problem₁

problem₁-z3-check-output-ok : problem₁-z3-check-output ≡ "sat\n"
problem₁-z3-check-output-ok = refl

problem₂-z3-check-output : String
problem₂-z3-check-output = z3CounterexampleCheck problem₂

problem₂-z3-check-output-ok : problem₂-z3-check-output ≡ "sat\n"
problem₂-z3-check-output-ok = refl

problem₄-z3-check-output : String
problem₄-z3-check-output = z3CounterexampleCheck problem₄

problem₄-z3-check-output-ok : problem₄-z3-check-output ≡ "sat\n"
problem₄-z3-check-output-ok = refl

problem₅-z3-check-output : String
problem₅-z3-check-output = z3CounterexampleCheck problem₅

problem₅-z3-check-output-ok : problem₅-z3-check-output ≡ "sat\n"
problem₅-z3-check-output-ok = refl

problem₆-z3-check-output : String
problem₆-z3-check-output = z3CounterexampleCheck problem₆

problem₆-z3-check-output-ok : problem₆-z3-check-output ≡ "unsat\n"
problem₆-z3-check-output-ok = refl

problem₇-z3-check-output : String
problem₇-z3-check-output = z3CounterexampleCheck problem₇

problem₇-z3-check-output-ok : problem₇-z3-check-output ≡ "sat\n"
problem₇-z3-check-output-ok = refl

problem₈-z3-check-output : String
problem₈-z3-check-output = z3CounterexampleCheck problem₈

problem₈-z3-check-output-ok : problem₈-z3-check-output ≡ "sat\n"
problem₈-z3-check-output-ok = refl

problem₉-z3-check-output : String
problem₉-z3-check-output = z3CounterexampleCheck problem₉

problem₉-z3-check-output-ok : problem₉-z3-check-output ≡ "unsat\n"
problem₉-z3-check-output-ok = refl