module SMT.Unsafe.ProgressiveAssume where

open import Cubical.Foundations.Prelude

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

linear-transitivity-type : Type₀
linear-transitivity-type = z3CheckedStatement valid-linear-transitivity

linear-transitivity-type-ok :
  linear-transitivity-type ≡ Statement valid-linear-transitivity
linear-transitivity-type-ok = refl

linear-chain-type : Type₀
linear-chain-type = z3CheckedStatement valid-linear-chain-equality

linear-chain-type-ok :
  linear-chain-type ≡ Statement valid-linear-chain-equality
linear-chain-type-ok = refl

affine-monotone-type : Type₀
affine-monotone-type = z3CheckedStatement valid-affine-monotone

affine-monotone-type-ok :
  affine-monotone-type ≡ Statement valid-affine-monotone
affine-monotone-type-ok = refl

guarded-ite-type : Type₀
guarded-ite-type = z3CheckedStatement valid-guarded-ite-nonnegative

guarded-ite-type-ok :
  guarded-ite-type ≡ Statement valid-guarded-ite-nonnegative
guarded-ite-type-ok = refl

nested-boolean-guard-type : Type₀
nested-boolean-guard-type = z3CheckedStatement valid-nested-boolean-guard

nested-boolean-guard-type-ok :
  nested-boolean-guard-type ≡ Statement valid-nested-boolean-guard
nested-boolean-guard-type-ok = refl

postulate
  assume-linear-transitivity :
    z3CheckedStatement valid-linear-transitivity
  assume-linear-chain :
    z3CheckedStatement valid-linear-chain-equality
  assume-affine-monotone :
    z3CheckedStatement valid-affine-monotone
  assume-diseq-symmetry :
    z3CheckedStatement valid-diseq-symmetry
  assume-guarded-ite :
    z3CheckedStatement valid-guarded-ite-nonnegative
  assume-inconsistent-assumptions :
    z3CheckedStatement valid-inconsistent-assumptions
  assume-ite-with-arithmetic-branches :
    z3CheckedStatement valid-ite-with-arithmetic-branches
  assume-nested-boolean-guard :
    z3CheckedStatement valid-nested-boolean-guard