module SMT.Derived where

open import Cubical.Data.Bool.Base using (true; false)
open import Cubical.Data.Int.Base using (ℤ; pos)
open import Cubical.Data.List.Base using (List; []; _∷_)

open import SMT.Core

z0 z1 z2 z3 : ℤ
z0 = pos 
z1 = pos 
z2 = pos 
z3 = pos 

int0 int1 int2 int3 : ∀ {Γ} → Expr Γ sInt
int0 = int z0
int1 = int z1
int2 = int z2
int3 = int z3

allBool : ∀ {Γ} → List (Expr Γ sBool) → Expr Γ sBool
allBool [] = bool true
allBool (p ∷ ps) = bAnd p (allBool ps)

anyBool : ∀ {Γ} → List (Expr Γ sBool) → Expr Γ sBool
anyBool [] = bool false
anyBool (p ∷ ps) = bOr p (anyBool ps)

between : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
between lo x hi = bAnd (iLe lo x) (iLe x hi)

iMin : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt
iMin x y = ite (iLe x y) x y

iMax : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt
iMax x y = ite (iLe x y) y x

iAbs : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt
iAbs x = ite (iGe x int0) x (iNeg x)

iClamp : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt
iClamp lo hi x = iMin hi (iMax lo x)

indicator : ∀ {Γ} → Expr Γ sBool → Expr Γ sInt
indicator p = ite p int1 int0

countTrue : ∀ {Γ} → List (Expr Γ sBool) → Expr Γ sInt
countTrue [] = int0
countTrue (p ∷ ps) = iAdd (indicator p) (countTrue ps)

atLeast : ∀ {Γ} → Expr Γ sInt → List (Expr Γ sBool) → Expr Γ sBool
atLeast n ps = iGe (countTrue ps) n

atMost : ∀ {Γ} → Expr Γ sInt → List (Expr Γ sBool) → Expr Γ sBool
atMost n ps = iLe (countTrue ps) n