Based on Cedar's Term language. (https://github.com/cedar-policy/cedar-spec/blob/main/cedar-lean/Cedar/SymCC/Term.lean) This file defines the Term language, a strongly and simply typed IR. The Term language has a straightforward translation to SMTLib. It is designed to reduce the semantic gap between Strata and SMTLib, and to faciliate proofs of soundness and completeness of the symbolic evaluator. Additionally, it allows us to generate different SMT encodings for different solvers (e.g., CVC5's theory of finite sets vs Z3's theory of Arrays).

Terms should not be created directly using Term constructors. Instead, they should be created using the factory functions defined in Factory.lean. The factory functions check the types of their arguments, perform optimizations, and ensure that applying them to well-formed terms results in well-formed terms.

See TermType.lean and Op.lean for definition of Term types and operators.

inductive Strata.SMT.TermPrim : Type

• bool : Bool → TermPrim
• int : Int → TermPrim
• real : StrataDDM.Decimal → TermPrim
• bitvec {n : Nat} : BitVec n → TermPrim
• string : String → TermPrim

def Strata.SMT.instReprTermPrim.repr : TermPrim → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Strata.SMT.instReprTermPrim : Repr TermPrim

Equations

• Strata.SMT.instReprTermPrim = { reprPrec := Strata.SMT.instReprTermPrim.repr }

@[instance_reducible]

instance Strata.SMT.instInhabitedTermPrim : Inhabited TermPrim

Equations

• Strata.SMT.instInhabitedTermPrim = { default := Strata.SMT.instInhabitedTermPrim.default }

@[instance_reducible]

instance Strata.SMT.instDecidableEqTermPrim : DecidableEq TermPrim

Equations

• Strata.SMT.instDecidableEqTermPrim = Strata.SMT.instDecidableEqTermPrim.decEq

def Strata.SMT.instDecidableEqTermPrim.decEq (x✝ x✝¹ : TermPrim) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.bool b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.int b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.real b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
• Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.string b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Strata.SMT.instHashableTermPrim.hash : TermPrim → UInt64

Equations

• Strata.SMT.instHashableTermPrim.hash (Strata.SMT.TermPrim.bool a) = mixHash 0 (hash a)
• Strata.SMT.instHashableTermPrim.hash (Strata.SMT.TermPrim.int a) = mixHash 1 (hash a)
• Strata.SMT.instHashableTermPrim.hash (Strata.SMT.TermPrim.real a) = mixHash 2 (hash a)
• Strata.SMT.instHashableTermPrim.hash (Strata.SMT.TermPrim.bitvec a_1) = mixHash (mixHash 3 (hash a)) (hash a_1)
• Strata.SMT.instHashableTermPrim.hash (Strata.SMT.TermPrim.string a) = mixHash 4 (hash a)

@[instance_reducible]

instance Strata.SMT.instHashableTermPrim : Hashable TermPrim

Equations

• Strata.SMT.instHashableTermPrim = { hash := Strata.SMT.instHashableTermPrim.hash }

def Strata.SMT.TermPrim.mkName : TermPrim → String

Equations

• (Strata.SMT.TermPrim.bool a).mkName = "bool"
• (Strata.SMT.TermPrim.int a).mkName = "int"
• (Strata.SMT.TermPrim.real a).mkName = "real"
• (Strata.SMT.TermPrim.bitvec a_1).mkName = "bitvec"
• (Strata.SMT.TermPrim.string a).mkName = "string"

def Strata.SMT.TermPrim.lt : TermPrim → TermPrim → Bool

Equations

• (Strata.SMT.TermPrim.bool b₁).lt (Strata.SMT.TermPrim.bool b₂) = decide (b₁ < b₂)
• (Strata.SMT.TermPrim.int i₁).lt (Strata.SMT.TermPrim.int i₂) = decide (i₁ < i₂)
• (Strata.SMT.TermPrim.real r₁).lt (Strata.SMT.TermPrim.real r₂) = decide (r₁.toRat < r₂.toRat)
• (Strata.SMT.TermPrim.bitvec bv₁).lt (Strata.SMT.TermPrim.bitvec bv₂) = (decide (n₁ < n₂) || decide (n₁ = n₂) && decide (bv₁.toNat < bv₂.toNat))
• (Strata.SMT.TermPrim.string s₁).lt (Strata.SMT.TermPrim.string s₂) = decide (s₁ < s₂)
• x✝¹.lt x✝ = decide (x✝¹.mkName < x✝.mkName)

@[instance_reducible]

instance Strata.SMT.instLTTermPrim : LT TermPrim

Equations

• Strata.SMT.instLTTermPrim = { lt := fun (x y : Strata.SMT.TermPrim) => x.lt y = true }

@[instance_reducible]

instance Strata.SMT.TermPrim.decLt (x y : TermPrim) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

inductive Strata.SMT.QuantifierKind : Type

• all : QuantifierKind
• exist : QuantifierKind

def Strata.SMT.instReprQuantifierKind.repr : QuantifierKind → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Strata.SMT.instReprQuantifierKind : Repr QuantifierKind

Equations

• Strata.SMT.instReprQuantifierKind = { reprPrec := Strata.SMT.instReprQuantifierKind.repr }

@[instance_reducible]

instance Strata.SMT.instDecidableEqQuantifierKind : DecidableEq QuantifierKind

Equations

• Strata.SMT.instDecidableEqQuantifierKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Strata.SMT.instHashableQuantifierKind.hash : QuantifierKind → UInt64

Equations

• Strata.SMT.instHashableQuantifierKind.hash Strata.SMT.QuantifierKind.all = 0
• Strata.SMT.instHashableQuantifierKind.hash Strata.SMT.QuantifierKind.exist = 1

@[instance_reducible]

instance Strata.SMT.instHashableQuantifierKind : Hashable QuantifierKind

Equations

• Strata.SMT.instHashableQuantifierKind = { hash := Strata.SMT.instHashableQuantifierKind.hash }

inductive Strata.SMT.Term : Type

• prim : TermPrim → Term
• var : TermVar → Term
• none : TermType → Term
• some : Term → Term
• app : Op → (args : List Term) → (retTy : TermType) → Term
• quant : QuantifierKind → (args : List TermVar) → (tr : List (List Term)) → (body : Term) → Term

partial def Strata.SMT.instReprTerm.repr : Term → Nat → Std.Format

@[instance_reducible]

instance Strata.SMT.instReprTerm : Repr Term

Equations

• Strata.SMT.instReprTerm = { reprPrec := Strata.SMT.instReprTerm.repr }

@[instance_reducible]

instance Strata.SMT.instInhabitedTerm : Inhabited Term

Equations

• Strata.SMT.instInhabitedTerm = { default := Strata.SMT.instInhabitedTerm.default }

def Strata.SMT.Term.isVar (t : Term) : Bool

Equations

• (Strata.SMT.Term.var a).isVar = true
• t.isVar = false

def Strata.SMT.Term.hasDecEq (t t' : Term) : Decidable (t = t')

Equations

• One or more equations did not get rendered due to their size.

def Strata.SMT.Term.hasListDec (ts₁ ts₂ : List Term) : Decidable (ts₁ = ts₂)

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.Term.hasListDec [] [] = isTrue Strata.SMT.Term.hasListDec._proof_1✝
• Strata.SMT.Term.hasListDec (head :: tail) [] = isFalse ⋯
• Strata.SMT.Term.hasListDec [] (head :: tail) = isFalse ⋯

def Strata.SMT.Term.hasListListDec (ts₁ ts₂ : List (List Term)) : Decidable (ts₁ = ts₂)

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.Term.hasListListDec [] [] = isTrue Strata.SMT.Term.hasListListDec._proof_1✝
• Strata.SMT.Term.hasListListDec (head :: tail) [] = isFalse ⋯
• Strata.SMT.Term.hasListListDec [] (head :: tail) = isFalse ⋯

@[instance_reducible]

instance Strata.SMT.instDecidableEqTerm : DecidableEq Term

Equations

• Strata.SMT.instDecidableEqTerm = Strata.SMT.Term.hasDecEq

def Strata.SMT.hashTerm (t : Term) : UInt64

Structural hash of a Term, recursing into app args and quant trigger/body.

Equations

• Strata.SMT.hashTerm (Strata.SMT.Term.prim a) = mixHash 2 (hash a)
• Strata.SMT.hashTerm (Strata.SMT.Term.var a) = mixHash 3 (hash a)
• Strata.SMT.hashTerm (Strata.SMT.Term.none a) = mixHash 5 (hash a)
• Strata.SMT.hashTerm a.some = mixHash 7 (Strata.SMT.hashTerm a)
• Strata.SMT.hashTerm (Strata.SMT.Term.app a a_1 a_2) = mixHash (mixHash 11 (mixHash (hash a) (hash a_2))) (Strata.SMT.hashTermList a_1)
• Strata.SMT.hashTerm (Strata.SMT.Term.quant a a_1 a_2 a_3) = mixHash (mixHash 13 (mixHash (hash a) (hash a_1))) (mixHash (Strata.SMT.hashTermListList a_2) (Strata.SMT.hashTerm a_3))

def Strata.SMT.hashTermList (ts : List Term) : UInt64

Equations

• Strata.SMT.hashTermList [] = 17
• Strata.SMT.hashTermList (t :: rest) = mixHash (Strata.SMT.hashTerm t) (Strata.SMT.hashTermList rest)

def Strata.SMT.hashTermListList (tss : List (List Term)) : UInt64

Equations

• Strata.SMT.hashTermListList [] = 19
• Strata.SMT.hashTermListList (ts :: rest) = mixHash (Strata.SMT.hashTermList ts) (Strata.SMT.hashTermListList rest)

@[instance_reducible]

instance Strata.SMT.instHashableTerm : Hashable Term

Equations

• Strata.SMT.instHashableTerm = { hash := Strata.SMT.hashTerm }

def Strata.SMT.Term.mkName : Term → String

Equations

• (Strata.SMT.Term.prim a).mkName = "prim"
• (Strata.SMT.Term.var a).mkName = "var"
• (Strata.SMT.Term.none a).mkName = "none"
• a.some.mkName = "some"
• (Strata.SMT.Term.app a args retTy).mkName = "app"
• (Strata.SMT.Term.quant Strata.SMT.QuantifierKind.all args tr body).mkName = "all"
• (Strata.SMT.Term.quant Strata.SMT.QuantifierKind.exist args tr body).mkName = "exists"

@[irreducible]

def Strata.SMT.Term.lt : Term → Term → Bool

Equations

• One or more equations did not get rendered due to their size.
• (Strata.SMT.Term.prim p₁).lt (Strata.SMT.Term.prim p₂) = decide (p₁ < p₂)
• (Strata.SMT.Term.var v₁).lt (Strata.SMT.Term.var v₂) = decide (v₁ < v₂)
• (Strata.SMT.Term.none ty₁).lt (Strata.SMT.Term.none ty₂) = decide (ty₁ < ty₂)
• t₁.some.lt t₂.some = t₁.lt t₂
• x✝¹.lt x✝ = decide (x✝¹.mkName < x✝.mkName)

@[irreducible]

def Strata.SMT.Term.ltList : List Term → List Term → Bool

Equations

• Strata.SMT.Term.ltList [] [] = false
• Strata.SMT.Term.ltList [] (head :: tail) = true
• Strata.SMT.Term.ltList (head :: tail) [] = false
• Strata.SMT.Term.ltList (t₁ :: ts₁) (t₂ :: ts₂) = (t₁.lt t₂ || decide (t₁ = t₂) && Strata.SMT.Term.ltList ts₁ ts₂)

@[instance_reducible]

instance Strata.SMT.instLTTerm : LT Term

Equations

• Strata.SMT.instLTTerm = { lt := fun (x y : Strata.SMT.Term) => x.lt y = true }

@[instance_reducible]

instance Strata.SMT.Term.decLt (x y : Term) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

@[reducible, inline]

abbrev Strata.SMT.Term.bool (b : Bool) : Term

Equations

• Strata.SMT.Term.bool b = Strata.SMT.Term.prim (Strata.SMT.TermPrim.bool b)

@[reducible, inline]

abbrev Strata.SMT.Term.int (i : Int) : Term

Equations

• Strata.SMT.Term.int i = Strata.SMT.Term.prim (Strata.SMT.TermPrim.int i)

@[reducible, inline]

abbrev Strata.SMT.Term.real (r : StrataDDM.Decimal) : Term

Equations

• Strata.SMT.Term.real r = Strata.SMT.Term.prim (Strata.SMT.TermPrim.real r)

@[reducible, inline]

abbrev Strata.SMT.Term.bitvec {n : Nat} (bv : BitVec n) : Term

Equations

• Strata.SMT.Term.bitvec bv = Strata.SMT.Term.prim (Strata.SMT.TermPrim.bitvec bv)

@[reducible, inline]

abbrev Strata.SMT.Term.string (s : String) : Term

Equations

• Strata.SMT.Term.string s = Strata.SMT.Term.prim (Strata.SMT.TermPrim.string s)

def Strata.SMT.TermPrim.typeOf : TermPrim → TermType

Equations

• (Strata.SMT.TermPrim.bool a).typeOf = Strata.SMT.TermType.bool
• (Strata.SMT.TermPrim.int a).typeOf = Strata.SMT.TermType.int
• (Strata.SMT.TermPrim.real a).typeOf = Strata.SMT.TermType.real
• (Strata.SMT.TermPrim.bitvec a).typeOf = Strata.SMT.TermType.bitvec n
• (Strata.SMT.TermPrim.string a).typeOf = Strata.SMT.TermType.string

def Strata.SMT.Term.typeOf : Term → TermType

Equations

• (Strata.SMT.Term.prim a).typeOf = a.typeOf
• (Strata.SMT.Term.var a).typeOf = a.ty
• (Strata.SMT.Term.none a).typeOf = a.option
• a.some.typeOf = a.typeOf.option
• (Strata.SMT.Term.app a a_1 a_2).typeOf = a_2
• (Strata.SMT.Term.quant a a_1 a_2 a_3).typeOf = Strata.SMT.TermType.bool

def Strata.SMT.Term.isLiteral : Term → Bool

Equations

• (Strata.SMT.Term.prim a).isLiteral = true
• (Strata.SMT.Term.none a).isLiteral = true
• t.some.isLiteral = t.isLiteral
• x✝.isLiteral = false

@[instance_reducible]

instance Strata.SMT.instCoeBoolTerm : Coe Bool Term

Equations

• Strata.SMT.instCoeBoolTerm = { coe := fun (b : Bool) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.bool b) }

@[instance_reducible]

instance Strata.SMT.instCoeIntTerm : Coe Int Term

Equations

• Strata.SMT.instCoeIntTerm = { coe := fun (i : Int) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.int i) }

@[instance_reducible]

instance Strata.SMT.instCoeInt64Term : Coe Int64 Term

Equations

• Strata.SMT.instCoeInt64Term = { coe := fun (i : Int64) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.bitvec i.toBitVec) }

@[instance_reducible]

instance Strata.SMT.instCoeOutBitVecTerm {n : Nat} : CoeOut (BitVec n) Term

Equations

• Strata.SMT.instCoeOutBitVecTerm = { coe := fun (b : BitVec n) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.bitvec b) }

@[instance_reducible]

instance Strata.SMT.instCoeStringTerm : Coe String Term

Equations

• Strata.SMT.instCoeStringTerm = { coe := fun (s : String) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.string s) }

@[instance_reducible]

instance Strata.SMT.instCoeTermVarTerm : Coe TermVar Term

Equations

• Strata.SMT.instCoeTermVarTerm = { coe := fun (v : Strata.SMT.TermVar) => Strata.SMT.Term.var v }

def Strata.SMT.TermVar.addSortNames (acc : Std.HashSet String) (v : TermVar) : Std.HashSet String

Add the names of the constructed sorts in the type of v.

Equations

• Strata.SMT.TermVar.addSortNames acc v = Strata.SMT.TermType.addSortNames acc v.ty

def Strata.SMT.Term.addSortNames (acc : Std.HashSet String) : Term → Std.HashSet String

Add the names of the constructed sorts of every subterm of a term.

Equations

• One or more equations did not get rendered due to their size.
• Strata.SMT.Term.addSortNames acc (Strata.SMT.Term.prim a) = acc
• Strata.SMT.Term.addSortNames acc (Strata.SMT.Term.var a) = Strata.SMT.TermVar.addSortNames acc a
• Strata.SMT.Term.addSortNames acc (Strata.SMT.Term.none a) = Strata.SMT.TermType.addSortNames acc a
• Strata.SMT.Term.addSortNames acc a.some = Strata.SMT.Term.addSortNames acc a
• Strata.SMT.Term.addSortNames acc (Strata.SMT.Term.app a a_1 a_2) = Strata.SMT.Term.addSortNamesList✝ (Strata.SMT.TermType.addSortNames acc a_2) a_1

structure Strata.SMT.IF : Type

• id : String
• args : List TermVar
• out : TermType
• body : Term
• isRec : Bool

  The body refers to the function itself: emit as define-fun-rec.

@[instance_reducible]

instance Strata.SMT.instReprIF : Repr IF

Equations

• Strata.SMT.instReprIF = { reprPrec := Strata.SMT.instReprIF.repr }

def Strata.SMT.instReprIF.repr : IF → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Strata.SMT.instDecidableEqIF : DecidableEq IF

Equations

• Strata.SMT.instDecidableEqIF = Strata.SMT.instDecidableEqIF.decEq

def Strata.SMT.instDecidableEqIF.decEq (x✝ x✝¹ : IF) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Strata.SMT.instInhabitedIF : Inhabited IF

Equations

• Strata.SMT.instInhabitedIF = { default := Strata.SMT.instInhabitedIF.default }

def Strata.SMT.instHashableIF.hash : IF → UInt64

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Strata.SMT.instHashableIF : Hashable IF

Equations

• Strata.SMT.instHashableIF = { hash := Strata.SMT.instHashableIF.hash }

def Strata.SMT.IF.toUF (f : IF) : UF

Equations

• f.toUF = { id := f.id, args := List.map (fun (x : Strata.SMT.TermVar) => x.ty) f.args, out := f.out }