Finite fields, typed

def Cvc.Typed.Term.ffBitsum [Ω] {k : Nat} (lft rgt : Term (FiniteField k)) : Env (Term (FiniteField k))

Weighted sum lft + 2 * rgt; ffBitsumN weighs further terms by 4, 8, …

Equations

• lft.ffBitsum rgt = Cvc.Untyped.Term.ffBitsum lft rgt

def Cvc.Typed.Term.ffMulN [Ω] {k : Nat} (terms : Terms (FiniteField k)) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (FiniteField k))

ffMul over two or more terms.

Equations

• Cvc.Typed.Term.ffMulN terms atLeastTwoElements = Cvc.Untyped.Term.ffMulN terms atLeastTwoElements

def Cvc.Typed.Term.ffAdd [Ω] {k : Nat} (lft rgt : Term (FiniteField k)) : Env (Term (FiniteField k))

Addition.

Equations

• lft.ffAdd rgt = Cvc.Untyped.Term.ffAdd lft rgt

def Cvc.Typed.Term.ffNeg [Ω] {k : Nat} (ff : Term (FiniteField k)) : Env (Term (FiniteField k))

Negation.

Equations

• ff.ffNeg = Cvc.Untyped.Term.ffNeg ff

def Cvc.Typed.Term.ffMul [Ω] {k : Nat} (lft rgt : Term (FiniteField k)) : Env (Term (FiniteField k))

Multiplication.

Equations

• lft.ffMul rgt = Cvc.Untyped.Term.ffMul lft rgt

def Cvc.Typed.Term.ffAddN [Ω] {k : Nat} (terms : Terms (FiniteField k)) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (FiniteField k))

ffAdd over two or more terms.

Equations

• Cvc.Typed.Term.ffAddN terms atLeastTwoElements = Cvc.Untyped.Term.ffAddN terms atLeastTwoElements

def Cvc.Typed.Term.ffBitsumN [Ω] {k : Nat} (terms : Terms (FiniteField k)) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (FiniteField k))

ffBitsum over two or more terms.

Equations

• Cvc.Typed.Term.ffBitsumN terms atLeastTwoElements = Cvc.Untyped.Term.ffBitsumN terms atLeastTwoElements

def Cvc.Typed.View.FiniteField.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.FiniteField τ))

Takes a term apart one level, at its sort, if FiniteField owns its operator and the term's sort fits it.

Equations

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

inductive Cvc.Typed.View.FiniteField [Ω] : Typ → Type

FiniteField's operators, taken apart one level, indexed by the sort each produces.

• finiteField [Ω] (q : Nat) : OnFiniteField q → View.FiniteField (Typ.finiteField q)

  An operator with a result of sort FiniteField.

inductive Cvc.Typed.View.FiniteField.OnFiniteField [Ω] (q : Nat) : Type

FiniteField's operators with a result of sort FiniteField.

• ffAdd [Ω] {q : Nat} (kids : Kids (FiniteField q)) : OnFiniteField q

  Addition.

  kids holds every operand, two or more.

• ffMul [Ω] {q : Nat} (kids : Kids (FiniteField q)) : OnFiniteField q

  Multiplication.

  kids holds every operand, two or more.

• ffNeg [Ω] {q : Nat} (ff : Term (FiniteField q)) : OnFiniteField q

  Negation.

• ffBitsum [Ω] {q : Nat} (kids : Kids (FiniteField q)) : OnFiniteField q

  Weighted sum lft + 2 * rgt; ffBitsumN weighs further terms by 4, 8, …

  kids holds every operand, two or more.

Values

def Cvc.Typed.Term.isFiniteFieldValue [Ω] {size : Nat} (term : Term (FiniteField size)) : Bool

Determine if this term is a finite field value.

Equations

• term.isFiniteFieldValue = Cvc.Untyped.Term.isFiniteFieldValue term

def Cvc.Typed.Term.getFiniteFieldRepr [Ω] {size : Nat} (term : Term (FiniteField size)) : Res Int

The integer representing a constant finite-field element, in cvc5's symmetric representation.

Equations

• term.getFiniteFieldRepr = Cvc.Untyped.Term.getFiniteFieldRepr term

def Cvc.Typed.Term.mkFiniteFieldValue [Ω] {size : Nat} (elem : FiniteField size) : Env (Term (FiniteField size))

The term denoting an element of a finite field.

Equations

• Cvc.Typed.Term.mkFiniteFieldValue = Cvc.Untyped.Term.FiniteField.toTerm

def Cvc.Typed.Term.getFiniteFieldValue [Ω] {size : Nat} : Term (FiniteField size) → Env (FiniteField size)

The finite-field element a constant term denotes.

Equations

• Cvc.Typed.Term.getFiniteFieldValue = Cvc.Untyped.Term.FiniteField.ofTerm

@[instance_reducible]

instance Cvc.Typed.Term.instSrtLikeFiniteField {size : Nat} : SrtLike (FiniteField size)

Equations

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