module SMT.Unsafe.Tests.RawFeatures where

open import Agda.Builtin.String using (String)

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

open import SMT.Unsafe.Z3

lia-model-output : String
lia-model-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (= (+ (* 2 x) 1) 7))\n" ++
      "(check-sat)\n" ++
      "(get-value (x))\n"
    )

lia-model-output-ok : lia-model-output ≡ "sat\n((x 3))\n"
lia-model-output-ok = refl

lia-unsat-bounds-output : String
lia-unsat-bounds-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (>= x 0))\n" ++
      "(assert (< x 0))\n" ++
      "(check-sat)\n"
    )

lia-unsat-bounds-output-ok : lia-unsat-bounds-output ≡ "unsat\n"
lia-unsat-bounds-output-ok = refl

incremental-push-pop-output : String
incremental-push-pop-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (= x 1))\n" ++
      "(push)\n" ++
      "(assert (= x 2))\n" ++
      "(check-sat)\n" ++
      "(pop)\n" ++
      "(check-sat)\n" ++
      "(get-value (x))\n"
    )

incremental-push-pop-output-ok :
  incremental-push-pop-output ≡ "unsat\nsat\n((x 1))\n"
incremental-push-pop-output-ok = refl

boolean-xor-output : String
boolean-xor-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const b Bool)\n" ++
      "(assert (= (xor b true) false))\n" ++
      "(check-sat)\n" ++
      "(get-value (b))\n"
    )

boolean-xor-output-ok : boolean-xor-output ≡ "sat\n((b true))\n"
boolean-xor-output-ok = refl

ite-output : String
ite-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const b Bool)\n" ++
      "(declare-const x Int)\n" ++
      "(assert b)\n" ++
      "(assert (= (ite b x 0) 5))\n" ++
      "(check-sat)\n" ++
      "(get-value (x b))\n"
    )

ite-output-ok : ite-output ≡ "sat\n((x 5)\n (b true))\n"
ite-output-ok = refl

distinct-unsat-output : String
distinct-unsat-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(declare-const y Int)\n" ++
      "(assert (distinct x y))\n" ++
      "(assert (= x 0))\n" ++
      "(assert (= y 0))\n" ++
      "(check-sat)\n"
    )

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

unsat-core-output : String
unsat-core-output =
  z3Run
    ( "(set-option :produce-unsat-cores true)\n" ++
      "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (! (>= x 0) :named nonneg))\n" ++
      "(assert (! (< x 0) :named neg))\n" ++
      "(check-sat)\n" ++
      "(get-unsat-core)\n"
    )

unsat-core-output-ok : unsat-core-output ≡ "unsat\n(nonneg neg)\n"
unsat-core-output-ok = refl

check-sat-assuming-output : String
check-sat-assuming-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const p Bool)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (= x 0))\n" ++
      "(assert (=> p (> x 1)))\n" ++
      "(check-sat-assuming (p))\n"
    )

check-sat-assuming-output-ok : check-sat-assuming-output ≡ "unsat\n"
check-sat-assuming-output-ok = refl

model-eval-output : String
model-eval-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (= x 3))\n" ++
      "(check-sat)\n" ++
      "(eval (+ x 1))\n"
    )

model-eval-output-ok : model-eval-output ≡ "sat\n4\n"
model-eval-output-ok = refl

bitvector-wrap-output : String
bitvector-wrap-output =
  z3Run
    ( "(set-logic QF_BV)\n" ++
      "(declare-const x (_ BitVec 8))\n" ++
      "(assert (= (bvadd x #x01) #x00))\n" ++
      "(check-sat)\n" ++
      "(get-value (x))\n"
    )

bitvector-wrap-output-ok : bitvector-wrap-output ≡ "sat\n((x #xff))\n"
bitvector-wrap-output-ok = refl

array-store-select-output : String
array-store-select-output =
  z3Run
    ( "(set-logic QF_AUFLIA)\n" ++
      "(declare-const a (Array Int Int))\n" ++
      "(assert (= (select (store a 0 42) 0) 42))\n" ++
      "(check-sat)\n"
    )

array-store-select-output-ok : array-store-select-output ≡ "sat\n"
array-store-select-output-ok = refl

uninterpreted-function-output : String
uninterpreted-function-output =
  z3Run
    ( "(set-logic QF_UF)\n" ++
      "(declare-sort A 0)\n" ++
      "(declare-fun f (A) A)\n" ++
      "(declare-const a A)\n" ++
      "(assert (distinct (f a) a))\n" ++
      "(check-sat)\n"
    )

uninterpreted-function-output-ok : uninterpreted-function-output ≡ "sat\n"
uninterpreted-function-output-ok = refl

real-arithmetic-output : String
real-arithmetic-output =
  z3Run
    ( "(set-logic QF_LRA)\n" ++
      "(declare-const x Real)\n" ++
      "(assert (= (+ x (/ 1.0 2.0)) 2.0))\n" ++
      "(check-sat)\n" ++
      "(get-value (x))\n"
    )

real-arithmetic-output-ok :
  real-arithmetic-output ≡ "sat\n((x (/ 3.0 2.0)))\n"
real-arithmetic-output-ok = refl

nonlinear-int-output : String
nonlinear-int-output =
  z3Run
    ( "(set-logic QF_NIA)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (= (* x x) 9))\n" ++
      "(assert (> x 0))\n" ++
      "(check-sat)\n" ++
      "(get-value (x))\n"
    )

nonlinear-int-output-ok : nonlinear-int-output ≡ "sat\n((x 3))\n"
nonlinear-int-output-ok = refl

quantifier-output : String
quantifier-output =
  z3Run
    ( "(set-logic ALL)\n" ++
      "(assert (forall ((x Int)) (> x 0)))\n" ++
      "(check-sat)\n"
    )

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

datatype-output : String
datatype-output =
  z3Run
    ( "(set-logic ALL)\n" ++
      "(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))\n" ++
      "(declare-const xs List)\n" ++
      "(assert (distinct xs nil))\n" ++
      "(check-sat)\n"
    )

datatype-output-ok : datatype-output ≡ "sat\n"
datatype-output-ok = refl

optimize-output : String
optimize-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(assert (and (<= 0 x) (<= x 10)))\n" ++
      "(maximize x)\n" ++
      "(check-sat)\n" ++
      "(get-objectives)\n"
    )

optimize-output-ok :
  optimize-output ≡ "sat\n(objectives\n (x 10)\n)\n"
optimize-output-ok = refl