module SMT.Unsafe.AdvancedAssume where

open import Cubical.Foundations.Prelude

open import SMT.Core using (Statement)
open import SMT.Examples.Advanced
open import SMT.Unsafe.Z3

subtract-back-type : Type₀
subtract-back-type = z3CheckedStatement valid-subtract-back

subtract-back-type-ok :
  subtract-back-type ≡ Statement valid-subtract-back
subtract-back-type-ok = refl

negated-subtraction-type : Type₀
negated-subtraction-type = z3CheckedStatement valid-negated-subtraction

negated-subtraction-type-ok :
  negated-subtraction-type ≡ Statement valid-negated-subtraction
negated-subtraction-type-ok = refl

strict-chain-type : Type₀
strict-chain-type = z3CheckedStatement valid-strict-chain

strict-chain-type-ok :
  strict-chain-type ≡ Statement valid-strict-chain
strict-chain-type-ok = refl

absolute-value-nonnegative-type : Type₀
absolute-value-nonnegative-type =
  z3CheckedStatement valid-absolute-value-nonnegative

absolute-value-nonnegative-type-ok :
  absolute-value-nonnegative-type ≡ Statement valid-absolute-value-nonnegative
absolute-value-nonnegative-type-ok = refl

conditional-upper-bound-type : Type₀
conditional-upper-bound-type =
  z3CheckedStatement valid-conditional-upper-bound

conditional-upper-bound-type-ok :
  conditional-upper-bound-type ≡ Statement valid-conditional-upper-bound
conditional-upper-bound-type-ok = refl

branch-refinement-type : Type₀
branch-refinement-type = z3CheckedStatement valid-branch-refinement

branch-refinement-type-ok :
  branch-refinement-type ≡ Statement valid-branch-refinement
branch-refinement-type-ok = refl

additive-upper-bound-type : Type₀
additive-upper-bound-type = z3CheckedStatement valid-additive-upper-bound

additive-upper-bound-type-ok :
  additive-upper-bound-type ≡ Statement valid-additive-upper-bound
additive-upper-bound-type-ok = refl

unsat-numeric-assumptions-type : Type₀
unsat-numeric-assumptions-type =
  z3CheckedStatement valid-unsat-numeric-assumptions

unsat-numeric-assumptions-type-ok :
  unsat-numeric-assumptions-type ≡ Statement valid-unsat-numeric-assumptions
unsat-numeric-assumptions-type-ok = refl

boolean-resolution-type : Type₀
boolean-resolution-type = z3CheckedStatement valid-boolean-resolution

boolean-resolution-type-ok :
  boolean-resolution-type ≡ Statement valid-boolean-resolution
boolean-resolution-type-ok = refl

xor-left-elim-type : Type₀
xor-left-elim-type = z3CheckedStatement valid-xor-left-elim

xor-left-elim-type-ok :
  xor-left-elim-type ≡ Statement valid-xor-left-elim
xor-left-elim-type-ok = refl

implication-chain-type : Type₀
implication-chain-type = z3CheckedStatement valid-implication-chain

implication-chain-type-ok :
  implication-chain-type ≡ Statement valid-implication-chain
implication-chain-type-ok = refl