module SMT.Unsafe.Tests.RawAdvanced where

open import Agda.Builtin.String using (String)

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

open import SMT.Unsafe.Z3

multi-scope-linear-output : String
multi-scope-linear-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(declare-const y Int)\n" ++
      "(assert (= (+ x y) 7))\n" ++
      "(assert (<= 0 x))\n" ++
      "(assert (<= 0 y))\n" ++
      "(push)\n" ++
      "(assert (> x 10))\n" ++
      "(check-sat)\n" ++
      "(pop)\n" ++
      "(push)\n" ++
      "(assert (= x 3))\n" ++
      "(check-sat)\n" ++
      "(get-value (x y))\n" ++
      "(pop)\n" ++
      "(push)\n" ++
      "(assert (= y 8))\n" ++
      "(check-sat)\n" ++
      "(pop)\n" ++
      "(check-sat)\n"
    )

multi-scope-linear-output-ok :
  multi-scope-linear-output ≡ "unsat\nsat\n((x 3)\n (y 4))\nunsat\nsat\n"
multi-scope-linear-output-ok = refl

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

assumption-core-output-ok :
  assumption-core-output ≡ "unsat\n(a a-pos b b-neg)\nsat\n"
assumption-core-output-ok = refl

linear-expression-model-output : String
linear-expression-model-output =
  z3Run
    ( "(set-logic QF_LIA)\n" ++
      "(declare-const x Int)\n" ++
      "(declare-const y Int)\n" ++
      "(assert (>= x 0))\n" ++
      "(assert (>= y 0))\n" ++
      "(assert (= (+ (* 2 x) (* 3 y)) 17))\n" ++
      "(assert (> y 0))\n" ++
      "(check-sat)\n" ++
      "(get-value (x y (+ x y)))\n"
    )

linear-expression-model-output-ok :
  linear-expression-model-output ≡
  "sat\n((x 7)\n (y 1)\n ((+ x y) 8))\n"
linear-expression-model-output-ok = refl

nonlinear-pair-output : String
nonlinear-pair-output =
  z3Run
    ( "(set-logic QF_NIA)\n" ++
      "(declare-const x Int)\n" ++
      "(declare-const y Int)\n" ++
      "(assert (= (* x y) 12))\n" ++
      "(assert (= (+ x y) 7))\n" ++
      "(check-sat)\n" ++
      "(get-value (x y))\n"
    )

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

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

real-system-output-ok :
  real-system-output ≡ "sat\n((x (/ 4.0 3.0))\n (y 1.0))\n"
real-system-output-ok = refl

bitvector-extract-output : String
bitvector-extract-output =
  z3Run
    ( "(set-logic QF_BV)\n" ++
      "(declare-const x (_ BitVec 16))\n" ++
      "(assert (= ((_ extract 7 0) x) #xab))\n" ++
      "(assert (= ((_ extract 15 8) x) #xcd))\n" ++
      "(check-sat)\n" ++
      "(get-value (x))\n"
    )

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

bitvector-signed-unsigned-output : String
bitvector-signed-unsigned-output =
  z3Run
    ( "(set-logic QF_BV)\n" ++
      "(declare-const x (_ BitVec 8))\n" ++
      "(assert (bvslt x #x00))\n" ++
      "(assert (bvugt x #x7f))\n" ++
      "(check-sat)\n" ++
      "(get-value (x))\n"
    )

bitvector-signed-unsigned-output-ok :
  bitvector-signed-unsigned-output ≡ "sat\n((x #x80))\n"
bitvector-signed-unsigned-output-ok = refl

array-extensional-unsat-output : String
array-extensional-unsat-output =
  z3Run
    ( "(set-logic QF_AUFLIA)\n" ++
      "(declare-const a (Array Int Int))\n" ++
      "(declare-const b (Array Int Int))\n" ++
      "(assert (= a b))\n" ++
      "(assert (= (select a 0) 1))\n" ++
      "(assert (= (select b 0) 2))\n" ++
      "(check-sat)\n"
    )

array-extensional-unsat-output-ok :
  array-extensional-unsat-output ≡ "unsat\n"
array-extensional-unsat-output-ok = refl

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

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

uf-congruence-unsat-output : String
uf-congruence-unsat-output =
  z3Run
    ( "(set-logic QF_UFLIA)\n" ++
      "(declare-sort A 0)\n" ++
      "(declare-fun f (A) Int)\n" ++
      "(declare-const a A)\n" ++
      "(declare-const b A)\n" ++
      "(assert (= a b))\n" ++
      "(assert (distinct (f a) (f b)))\n" ++
      "(check-sat)\n"
    )

uf-congruence-unsat-output-ok :
  uf-congruence-unsat-output ≡ "unsat\n"
uf-congruence-unsat-output-ok = refl

uf-model-eval-output : String
uf-model-eval-output =
  z3Run
    ( "(set-logic QF_UFLIA)\n" ++
      "(declare-fun f (Int) Int)\n" ++
      "(assert (= (f 0) 1))\n" ++
      "(assert (= (f 1) 2))\n" ++
      "(check-sat)\n" ++
      "(eval (f 0))\n" ++
      "(eval (f 1))\n" ++
      "(eval (f 2))\n"
    )

uf-model-eval-output-ok : uf-model-eval-output ≡ "sat\n1\n2\n1\n"
uf-model-eval-output-ok = refl

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

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

quantifier-instantiation-output : String
quantifier-instantiation-output =
  z3Run
    ( "(set-logic LIA)\n" ++
      "(declare-const a Int)\n" ++
      "(assert (forall ((x Int)) (=> (> x 0) (> (+ x 1) 1))))\n" ++
      "(assert (> a 0))\n" ++
      "(assert (not (> (+ a 1) 1)))\n" ++
      "(check-sat)\n"
    )

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

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

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