Generated FiniteField constructors, sort-erased

def Cvc.Untyped.Term.ffNeg [Ω] (ff : Term) : Env Term

Negation.

Equations

• ff.ffNeg = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FINITE_FIELD_NEG #[ff]

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

ffBitsum over two or more terms.

Equations

• Cvc.Untyped.Term.ffBitsumN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FINITE_FIELD_BITSUM terms

def Cvc.Untyped.Term.ffBitsum [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.ffBitsum rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FINITE_FIELD_BITSUM #[lft, rgt]

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

ffMul over two or more terms.

Equations

• Cvc.Untyped.Term.ffMulN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FINITE_FIELD_MULT terms

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

ffAdd over two or more terms.

Equations

• Cvc.Untyped.Term.ffAddN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FINITE_FIELD_ADD terms

def Cvc.Untyped.Term.ffMul [Ω] (lft rgt : Term) : Env Term

Multiplication.

Equations

• lft.ffMul rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FINITE_FIELD_MULT #[lft, rgt]

def Cvc.Untyped.Term.ffAdd [Ω] (lft rgt : Term) : Env Term

Addition.

Equations

• lft.ffAdd rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.FINITE_FIELD_ADD #[lft, rgt]

inductive Cvc.Untyped.View.FiniteField [Ω] : Type

FiniteField's operators, taken apart one level, sort-erased.

• ffAdd [Ω] (kids : Kids) : View.FiniteField

  Addition.

  kids holds every operand, two or more.

• ffMul [Ω] (kids : Kids) : View.FiniteField

  Multiplication.

  kids holds every operand, two or more.

• ffNeg [Ω] (ff : Term) : View.FiniteField

  Negation.

• ffBitsum [Ω] (kids : Kids) : View.FiniteField

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

  kids holds every operand, two or more.

def Cvc.Untyped.View.FiniteField.of? [Ω] (viewed : Term) : Option View.FiniteField

Takes a term apart one level, if FiniteField owns its operator.

Equations

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

def Cvc.Untyped.Term.mkFiniteFieldElem [Ω] (value : Int) (srt : Srt) : Env Term

An element of the finite field a sort describes.

Equations

• Cvc.Untyped.Term.mkFiniteFieldElem value srt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFiniteFieldElem value (Cvc.Srt.toUnsafe✝ srt)

Values

The size lives in the sort, so reading a value back recovers it from there and checks it against the one asked for.

def Cvc.Untyped.Term.isFiniteFieldValue [Ω] (term : Term) : Bool

Determine if this term is a finite field value.

Equations

• term.isFiniteFieldValue = (Cvc.Untyped.Term.toUnsafe✝ term).isFiniteFieldValue

def Cvc.Untyped.Term.getFiniteFieldRepr [Ω] (term : Term) : Res Int

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

Equations

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

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

The term denoting an element of a finite field of known size.

Equations

• Cvc.Untyped.Term.FiniteField.toTerm elem = do let __do_lift ← Cvc.Srt.of (Cvc.FiniteField size) Cvc.Untyped.Term.mkFiniteFieldElem elem.repr __do_lift

def Cvc.Untyped.Term.FiniteField.ofTermErased [Ω] (term : Term) : Env FiniteField.Erased

The finite-field element a constant term denotes, at whatever size it turns out to have.

Equations

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

def Cvc.Untyped.Term.FiniteField.ofTerm [Ω] {size : Nat} (term : Term) : Env (FiniteField size)

The finite-field element a constant term denotes, failing unless the size is the expected.

Equations

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

@[instance_reducible]

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

Equations

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