module SMT.Unsafe.Tests.Progressive where

open import Agda.Builtin.String using (String)

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

open import SMT.Examples.Progressive
open import SMT.Unsafe.Z3

valid-bool-id-check : String
valid-bool-id-check = z3CounterexampleCheck valid-bool-id

valid-bool-id-check-ok : valid-bool-id-check ≡ "unsat\n"
valid-bool-id-check-ok = refl

valid-xor-comm-check : String
valid-xor-comm-check = z3CounterexampleCheck valid-xor-comm

valid-xor-comm-check-ok : valid-xor-comm-check ≡ "unsat\n"
valid-xor-comm-check-ok = refl

valid-demorgan-check : String
valid-demorgan-check = z3CounterexampleCheck valid-demorgan

valid-demorgan-check-ok : valid-demorgan-check ≡ "unsat\n"
valid-demorgan-check-ok = refl

invalid-or-left-check : String
invalid-or-left-check = z3CounterexampleCheck invalid-or-left

invalid-or-left-check-ok : invalid-or-left-check ≡ "sat\n"
invalid-or-left-check-ok = refl

valid-linear-transitivity-check : String
valid-linear-transitivity-check = z3CounterexampleCheck valid-linear-transitivity

valid-linear-transitivity-check-ok :
  valid-linear-transitivity-check ≡ "unsat\n"
valid-linear-transitivity-check-ok = refl

valid-linear-chain-equality-check : String
valid-linear-chain-equality-check =
  z3CounterexampleCheck valid-linear-chain-equality

valid-linear-chain-equality-check-ok :
  valid-linear-chain-equality-check ≡ "unsat\n"
valid-linear-chain-equality-check-ok = refl

valid-affine-monotone-check : String
valid-affine-monotone-check = z3CounterexampleCheck valid-affine-monotone

valid-affine-monotone-check-ok :
  valid-affine-monotone-check ≡ "unsat\n"
valid-affine-monotone-check-ok = refl

valid-diseq-symmetry-check : String
valid-diseq-symmetry-check = z3CounterexampleCheck valid-diseq-symmetry

valid-diseq-symmetry-check-ok :
  valid-diseq-symmetry-check ≡ "unsat\n"
valid-diseq-symmetry-check-ok = refl

valid-guarded-ite-nonnegative-check : String
valid-guarded-ite-nonnegative-check =
  z3CounterexampleCheck valid-guarded-ite-nonnegative

valid-guarded-ite-nonnegative-check-ok :
  valid-guarded-ite-nonnegative-check ≡ "unsat\n"
valid-guarded-ite-nonnegative-check-ok = refl

valid-inconsistent-assumptions-check : String
valid-inconsistent-assumptions-check =
  z3CounterexampleCheck valid-inconsistent-assumptions

valid-inconsistent-assumptions-check-ok :
  valid-inconsistent-assumptions-check ≡ "unsat\n"
valid-inconsistent-assumptions-check-ok = refl

invalid-nonnegative-sum-positive-check : String
invalid-nonnegative-sum-positive-check =
  z3CounterexampleCheck invalid-nonnegative-sum-positive

invalid-nonnegative-sum-positive-check-ok :
  invalid-nonnegative-sum-positive-check ≡ "sat\n"
invalid-nonnegative-sum-positive-check-ok = refl

invalid-negative-scale-monotone-check : String
invalid-negative-scale-monotone-check =
  z3CounterexampleCheck invalid-negative-scale-monotone

invalid-negative-scale-monotone-check-ok :
  invalid-negative-scale-monotone-check ≡ "sat\n"
invalid-negative-scale-monotone-check-ok = refl

invalid-unguarded-ite-lower-bound-check : String
invalid-unguarded-ite-lower-bound-check =
  z3CounterexampleCheck invalid-unguarded-ite-lower-bound

invalid-unguarded-ite-lower-bound-check-ok :
  invalid-unguarded-ite-lower-bound-check ≡ "sat\n"
invalid-unguarded-ite-lower-bound-check-ok = refl

invalid-linear-offset-cancel-check : String
invalid-linear-offset-cancel-check =
  z3CounterexampleCheck invalid-linear-offset-cancel

invalid-linear-offset-cancel-check-ok :
  invalid-linear-offset-cancel-check ≡ "sat\n"
invalid-linear-offset-cancel-check-ok = refl

valid-ite-with-arithmetic-branches-check : String
valid-ite-with-arithmetic-branches-check =
  z3CounterexampleCheck valid-ite-with-arithmetic-branches

valid-ite-with-arithmetic-branches-check-ok :
  valid-ite-with-arithmetic-branches-check ≡ "unsat\n"
valid-ite-with-arithmetic-branches-check-ok = refl

valid-nested-boolean-guard-check : String
valid-nested-boolean-guard-check =
  z3CounterexampleCheck valid-nested-boolean-guard

valid-nested-boolean-guard-check-ok :
  valid-nested-boolean-guard-check ≡ "unsat\n"
valid-nested-boolean-guard-check-ok = refl