module SMT.Unsafe.Tests.Advanced where

open import Agda.Builtin.String using (String)

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

open import SMT.Examples.Advanced
open import SMT.Unsafe.Z3

valid-subtract-back-check : String
valid-subtract-back-check = z3CounterexampleCheck valid-subtract-back

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

valid-negated-subtraction-check : String
valid-negated-subtraction-check = z3CounterexampleCheck valid-negated-subtraction

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

valid-strict-chain-check : String
valid-strict-chain-check = z3CounterexampleCheck valid-strict-chain

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

valid-diseq-from-strict-check : String
valid-diseq-from-strict-check = z3CounterexampleCheck valid-diseq-from-strict

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

valid-absolute-value-nonnegative-check : String
valid-absolute-value-nonnegative-check =
  z3CounterexampleCheck valid-absolute-value-nonnegative

valid-absolute-value-nonnegative-check-ok :
  valid-absolute-value-nonnegative-check ≡ "unsat\n"
valid-absolute-value-nonnegative-check-ok = refl

valid-conditional-upper-bound-check : String
valid-conditional-upper-bound-check =
  z3CounterexampleCheck valid-conditional-upper-bound

valid-conditional-upper-bound-check-ok :
  valid-conditional-upper-bound-check ≡ "unsat\n"
valid-conditional-upper-bound-check-ok = refl

valid-branch-refinement-check : String
valid-branch-refinement-check = z3CounterexampleCheck valid-branch-refinement

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

valid-additive-upper-bound-check : String
valid-additive-upper-bound-check = z3CounterexampleCheck valid-additive-upper-bound

valid-additive-upper-bound-check-ok :
  valid-additive-upper-bound-check ≡ "unsat\n"
valid-additive-upper-bound-check-ok = refl

valid-unsat-numeric-assumptions-check : String
valid-unsat-numeric-assumptions-check =
  z3CounterexampleCheck valid-unsat-numeric-assumptions

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

valid-boolean-resolution-check : String
valid-boolean-resolution-check = z3CounterexampleCheck valid-boolean-resolution

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

valid-xor-left-elim-check : String
valid-xor-left-elim-check = z3CounterexampleCheck valid-xor-left-elim

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

valid-implication-chain-check : String
valid-implication-chain-check = z3CounterexampleCheck valid-implication-chain

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

invalid-strict-from-nonstrict-check : String
invalid-strict-from-nonstrict-check =
  z3CounterexampleCheck invalid-strict-from-nonstrict

invalid-strict-from-nonstrict-check-ok :
  invalid-strict-from-nonstrict-check ≡ "sat\n"
invalid-strict-from-nonstrict-check-ok = refl

invalid-diseq-from-nonstrict-check : String
invalid-diseq-from-nonstrict-check =
  z3CounterexampleCheck invalid-diseq-from-nonstrict

invalid-diseq-from-nonstrict-check-ok :
  invalid-diseq-from-nonstrict-check ≡ "sat\n"
invalid-diseq-from-nonstrict-check-ok = refl

invalid-drop-branch-guard-check : String
invalid-drop-branch-guard-check =
  z3CounterexampleCheck invalid-drop-branch-guard

invalid-drop-branch-guard-check-ok :
  invalid-drop-branch-guard-check ≡ "sat\n"
invalid-drop-branch-guard-check-ok = refl

invalid-boolean-resolution-check : String
invalid-boolean-resolution-check =
  z3CounterexampleCheck invalid-boolean-resolution

invalid-boolean-resolution-check-ok :
  invalid-boolean-resolution-check ≡ "sat\n"
invalid-boolean-resolution-check-ok = refl

invalid-xor-to-left-check : String
invalid-xor-to-left-check = z3CounterexampleCheck invalid-xor-to-left

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

invalid-additive-cancel-check : String
invalid-additive-cancel-check = z3CounterexampleCheck invalid-additive-cancel

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

invalid-absolute-value-positive-check : String
invalid-absolute-value-positive-check =
  z3CounterexampleCheck invalid-absolute-value-positive

invalid-absolute-value-positive-check-ok :
  invalid-absolute-value-positive-check ≡ "sat\n"
invalid-absolute-value-positive-check-ok = refl

invalid-subtraction-bound-check : String
invalid-subtraction-bound-check = z3CounterexampleCheck invalid-subtraction-bound

invalid-subtraction-bound-check-ok :
  invalid-subtraction-bound-check ≡ "sat\n"
invalid-subtraction-bound-check-ok = refl

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

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

invalid-branch-equality-check : String
invalid-branch-equality-check = z3CounterexampleCheck invalid-branch-equality

invalid-branch-equality-check-ok : invalid-branch-equality-check ≡ "sat\n"
invalid-branch-equality-check-ok = refl