This file defines an ADT that represents unary functions over terms. These functions can be uninterpreted symbols or interpretations of these symbols that are generated by an SMT solver. We assume that SMT function interpretations take a fixed format---effectively, a lookup table with a fixed number of entries, along with a default value that is returned for all elements of the domain that are not found in the table. The SMT solver represents these tables as nested ite expressions, where each condition checks if the input is equal to a value in the domain, and if so returns the corresponding output. Our target SMT solver (CVC5) always returns interpretations of this form.

structure Cedar.SymCC.UDF : Type

• arg : TermType
• out : TermType
• table : Data.Map Term Term
• default : Term

instance Cedar.SymCC.instReprUDF : Repr UDF

Equations

• Cedar.SymCC.instReprUDF = { reprPrec := Cedar.SymCC.instReprUDF.repr }

def Cedar.SymCC.instReprUDF.repr : UDF → Nat → Std.Format

Equations

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

def Cedar.SymCC.instDecidableEqUDF.decEq (x✝ x✝¹ : UDF) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.SymCC.instDecidableEqUDF : DecidableEq UDF

Equations

• Cedar.SymCC.instDecidableEqUDF = Cedar.SymCC.instDecidableEqUDF.decEq

def Cedar.SymCC.instInhabitedUDF.default : UDF

Equations

• Cedar.SymCC.instInhabitedUDF.default = { arg := default, out := default, table := default, default := default }

instance Cedar.SymCC.instInhabitedUDF : Inhabited UDF

Equations

• Cedar.SymCC.instInhabitedUDF = { default := Cedar.SymCC.instInhabitedUDF.default }

inductive Cedar.SymCC.UnaryFunction : Type

• uuf : UUF → UnaryFunction
• udf : UDF → UnaryFunction

def Cedar.SymCC.UnaryFunction.argType : UnaryFunction → TermType

Equations

• (Cedar.SymCC.UnaryFunction.uuf f).argType = f.arg
• (Cedar.SymCC.UnaryFunction.udf f).argType = f.arg

def Cedar.SymCC.UnaryFunction.outType : UnaryFunction → TermType

Equations

• (Cedar.SymCC.UnaryFunction.uuf f).outType = f.out
• (Cedar.SymCC.UnaryFunction.udf f).outType = f.out

@[inline]

def Cedar.SymCC.UnaryFunction.isUUF : UnaryFunction → Bool

Equations

• (Cedar.SymCC.UnaryFunction.uuf f).isUUF = true
• (Cedar.SymCC.UnaryFunction.udf f).isUUF = false

@[inline]

def Cedar.SymCC.UnaryFunction.isUDF : UnaryFunction → Bool

Equations

• (Cedar.SymCC.UnaryFunction.udf a).isUDF = true
• (Cedar.SymCC.UnaryFunction.uuf a).isUDF = false

def Cedar.SymCC.UDF.isLiteral (f : UDF) : Bool

Equations

• f.isLiteral = (f.default.isLiteral && f.table.toList.all fun (x : Cedar.SymCC.Term × Cedar.SymCC.Term) => match x with | (tᵢ, tₒ) => tᵢ.isLiteral && tₒ.isLiteral)

@[inline]

def Cedar.SymCC.UnaryFunction.isLiteral : UnaryFunction → Bool

Equations

• (Cedar.SymCC.UnaryFunction.udf a).isLiteral = a.isLiteral
• (Cedar.SymCC.UnaryFunction.uuf a).isLiteral = false

instance Cedar.SymCC.instReprUnaryFunction : Repr UnaryFunction

Equations

• Cedar.SymCC.instReprUnaryFunction = { reprPrec := Cedar.SymCC.instReprUnaryFunction.repr }

def Cedar.SymCC.instReprUnaryFunction.repr : UnaryFunction → Nat → Std.Format

Equations

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

def Cedar.SymCC.instDecidableEqUnaryFunction.decEq (x✝ x✝¹ : UnaryFunction) : Decidable (x✝ = x✝¹)

Equations

• Cedar.SymCC.instDecidableEqUnaryFunction.decEq (Cedar.SymCC.UnaryFunction.uuf a) (Cedar.SymCC.UnaryFunction.uuf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.SymCC.instDecidableEqUnaryFunction.decEq (Cedar.SymCC.UnaryFunction.uuf a) (Cedar.SymCC.UnaryFunction.udf a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqUnaryFunction.decEq (Cedar.SymCC.UnaryFunction.udf a) (Cedar.SymCC.UnaryFunction.uuf a_1) = isFalse ⋯
• Cedar.SymCC.instDecidableEqUnaryFunction.decEq (Cedar.SymCC.UnaryFunction.udf a) (Cedar.SymCC.UnaryFunction.udf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.SymCC.instDecidableEqUnaryFunction : DecidableEq UnaryFunction

Equations

• Cedar.SymCC.instDecidableEqUnaryFunction = Cedar.SymCC.instDecidableEqUnaryFunction.decEq

def Cedar.SymCC.instInhabitedUnaryFunction.default : UnaryFunction

Equations

• Cedar.SymCC.instInhabitedUnaryFunction.default = Cedar.SymCC.UnaryFunction.uuf default

instance Cedar.SymCC.instInhabitedUnaryFunction : Inhabited UnaryFunction

Equations

• Cedar.SymCC.instInhabitedUnaryFunction = { default := Cedar.SymCC.instInhabitedUnaryFunction.default }