Arithmetic, typed

def Cvc.Typed.Term.toInt [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term α) : Env (Term Int)

Conversion to an integer, rounding towards negative infinity.

Equations

• arithTerm.toInt = Cvc.Untyped.Term.toInt arithTerm

def Cvc.Typed.Term.arccotangent [Ω] (arg : Term Rat) : Env (Term Rat)

Arc cotangent.

Equations

• arg.arccotangent = Cvc.Untyped.Term.arccotangent arg

def Cvc.Typed.Term.arctangent [Ω] (arg : Term Rat) : Env (Term Rat)

Arc tangent.

Equations

• arg.arctangent = Cvc.Untyped.Term.arctangent arg

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

add over two or more terms.

Equations

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

def Cvc.Typed.Term.le [Ω] {α : Type} [ToTyp α] [IsArith α] (lft rgt : Term α) : Env (Term Bool)

Binary less-than-or-equal-to; leN chains, as ltN does.

Equations

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

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

ge over two or more terms.

Equations

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

def Cvc.Typed.Term.cosine [Ω] (arg : Term Rat) : Env (Term Rat)

Cosine.

Equations

• arg.cosine = Cvc.Untyped.Term.cosine arg

def Cvc.Typed.Term.mulN' [Ω] {α : Type} [ToTyp α] [IsArith α] (terms : Terms α) : Env (Term α)

mul over any number of terms: none gives 1, one gives that term.

Equations

• Cvc.Typed.Term.mulN' terms = Cvc.Untyped.Term.mulN' terms (match Cvc.Typ.of α with | Cvc.Typ.real => Cvc.Untyped.Term.mkReal 1 | x => Cvc.Untyped.Term.mkInt 1)

def Cvc.Typed.Term.cosecant [Ω] (arg : Term Rat) : Env (Term Rat)

Cosecant.

Equations

• arg.cosecant = Cvc.Untyped.Term.cosecant arg

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

sub over two or more terms.

Equations

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

def Cvc.Typed.Term.ge [Ω] {α : Type} [ToTyp α] [IsArith α] (lft rgt : Term α) : Env (Term Bool)

Binary greater-than-or-equal-to; geN chains, as ltN does.

Equations

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

def Cvc.Typed.Term.mkRealOfString [Ω] (repr : String) : Env (Term Rat)

A real literal, read from a decimal ("1.5") or a fraction ("3/4").

Equations

• Cvc.Typed.Term.mkRealOfString repr = Cvc.Untyped.Term.mkRealOfString repr

def Cvc.Typed.Term.mkInt [Ω] (i : Int) : Env (Term Int)

An integer literal.

Equations

• Cvc.Typed.Term.mkInt i = Cvc.Untyped.Term.mkInt i

def Cvc.Typed.Term.arccosine [Ω] (arg : Term Rat) : Env (Term Rat)

Arc cosine.

Equations

• arg.arccosine = Cvc.Untyped.Term.arccosine arg

def Cvc.Typed.Term.sine [Ω] (arg : Term Rat) : Env (Term Rat)

Sine.

Equations

• arg.sine = Cvc.Untyped.Term.sine arg

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

lt over two or more terms.

Equations

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

def Cvc.Typed.Term.realDiv [Ω] (lft rgt : Term Rat) : Env (Term Rat)

Real division, left-associative; unspecified on a zero divisor.

Equations

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

def Cvc.Typed.Term.pow [Ω] {α : Type} [ToTyp α] [IsArith α] (base exponent : Term α) : Env (Term α)

Exponentiation.

Equations

• base.pow exponent = Cvc.Untyped.Term.pow base exponent

def Cvc.Typed.Term.add [Ω] {α : Type} [ToTyp α] [IsArith α] (lft rgt : Term α) : Env (Term α)

Binary addition.

Equations

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

def Cvc.Typed.Term.pow2 [Ω] (exponent : Term Int) : Env (Term Int)

Two raised to a non-negative exponent.

Equations

• exponent.pow2 = Cvc.Untyped.Term.pow2 exponent

def Cvc.Typed.Term.piand [Ω] (size lft rgt : Term Int) : Env (Term Int)

Bit-wise and of the low size bits of lft and rgt; zero when size ≤ 0.

Equations

• size.piand lft rgt = Cvc.Untyped.Term.piand size lft rgt

def Cvc.Typed.Term.mul [Ω] {α : Type} [ToTyp α] [IsArith α] (lft rgt : Term α) : Env (Term α)

Binary multiplication.

Equations

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

def Cvc.Typed.Term.intDivTotal [Ω] (lft rgt : Term Int) : Env (Term Int)

Euclidean integer division, left-associative; zero on a zero divisor.

Equations

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

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

intDivTotal over two or more terms.

Equations

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

def Cvc.Typed.Term.mkReal [Ω] (r : Rat) : Env (Term Rat)

A real literal.

Equations

• Cvc.Typed.Term.mkReal r = Cvc.Untyped.Term.mkReal r

def Cvc.Typed.Term.arccosecant [Ω] (arg : Term Rat) : Env (Term Rat)

Arc cosecant.

Equations

• arg.arccosecant = Cvc.Untyped.Term.arccosecant arg

def Cvc.Typed.Term.gt [Ω] {α : Type} [ToTyp α] [IsArith α] (lft rgt : Term α) : Env (Term Bool)

Binary greater-than; gtN chains, as ltN does.

Equations

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

def Cvc.Typed.Term.mkIntOfString [Ω] (repr : String) : Env (Term Int)

An integer literal, read from its decimal representation.

Equations

• Cvc.Typed.Term.mkIntOfString repr = Cvc.Untyped.Term.mkIntOfString repr

def Cvc.Typed.Term.secant [Ω] (arg : Term Rat) : Env (Term Rat)

Secant.

Equations

• arg.secant = Cvc.Untyped.Term.secant arg

def Cvc.Typed.Term.arcsine [Ω] (arg : Term Rat) : Env (Term Rat)

Arc sine.

Equations

• arg.arcsine = Cvc.Untyped.Term.arcsine arg

def Cvc.Typed.Term.arcsecant [Ω] (arg : Term Rat) : Env (Term Rat)

Arc secant.

Equations

• arg.arcsecant = Cvc.Untyped.Term.arcsecant arg

def Cvc.Typed.Term.sub [Ω] {α : Type} [ToTyp α] [IsArith α] (lft rgt : Term α) : Env (Term α)

Binary subtraction; subN is left-associative.

Equations

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

def Cvc.Typed.Term.intMod [Ω] (lft rgt : Term Int) : Env (Term Int)

Euclidean integer modulus, never negative; unspecified on a zero divisor.

Equations

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

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

le over two or more terms.

Equations

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

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

realDivTotal over two or more terms.

Equations

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

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

realDiv over two or more terms.

Equations

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

def Cvc.Typed.Term.addN' [Ω] {α : Type} [ToTyp α] [IsArith α] (terms : Terms α) : Env (Term α)

add over any number of terms: none gives 0, one gives that term.

Equations

• Cvc.Typed.Term.addN' terms = Cvc.Untyped.Term.addN' terms (match Cvc.Typ.of α with | Cvc.Typ.real => Cvc.Untyped.Term.mkReal 0 | x => Cvc.Untyped.Term.mkInt 0)

def Cvc.Typed.Term.divisible [Ω] (divisor : Nat) (arg : Term Int) : Env (Term Bool)

Whether arg is divisible by divisor.

Equations

• Cvc.Typed.Term.divisible divisor arg = Cvc.Untyped.Term.divisible divisor arg

def Cvc.Typed.Term.toReal [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term α) : Env (Term Rat)

Conversion to a real.

Equations

• arithTerm.toReal = Cvc.Untyped.Term.toReal arithTerm

def Cvc.Typed.Term.exp [Ω] (arg : Term Rat) : Env (Term Rat)

The exponential function.

Equations

• arg.exp = Cvc.Untyped.Term.exp arg

def Cvc.Typed.Term.intModTotal [Ω] (lft rgt : Term Int) : Env (Term Int)

Euclidean integer modulus; the dividend on a zero divisor.

Equations

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

def Cvc.Typed.Term.neg [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term α) : Env (Term α)

Arithmetic negation.

Equations

• arithTerm.neg = Cvc.Untyped.Term.neg arithTerm

def Cvc.Typed.Term.sqrt [Ω] (arg : Term Rat) : Env (Term Rat)

Square root.

Equations

• arg.sqrt = Cvc.Untyped.Term.sqrt arg

def Cvc.Typed.Term.pi [Ω] : Env (Term Rat)

The constant π.

Equations

• Cvc.Typed.Term.pi = Cvc.Untyped.Term.pi

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

intDiv over two or more terms.

Equations

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

def Cvc.Typed.Term.iand [Ω] (size : Nat) (lft rgt : Term Int) : Env (Term Int)

Bit-wise and of the low size bits of lft and rgt.

Equations

• Cvc.Typed.Term.iand size lft rgt = Cvc.Untyped.Term.iand size lft rgt

def Cvc.Typed.Term.log2 [Ω] (arg : Term Int) : Env (Term Int)

Base-two logarithm.

Equations

• arg.log2 = Cvc.Untyped.Term.log2 arg

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

mul over two or more terms.

Equations

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

def Cvc.Typed.Term.isInt [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term α) : Env (Term Bool)

Whether an arithmetic term denotes an integer.

Equations

• arithTerm.isInt = Cvc.Untyped.Term.isInt arithTerm

def Cvc.Typed.Term.cotangent [Ω] (arg : Term Rat) : Env (Term Rat)

Cotangent.

Equations

• arg.cotangent = Cvc.Untyped.Term.cotangent arg

def Cvc.Typed.Term.abs [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term α) : Env (Term α)

Absolute value.

Equations

• arithTerm.abs = Cvc.Untyped.Term.abs arithTerm

def Cvc.Typed.Term.intDiv [Ω] (lft rgt : Term Int) : Env (Term Int)

Euclidean integer division, left-associative; unspecified on a zero divisor.

Equations

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

def Cvc.Typed.Term.lt [Ω] {α : Type} [ToTyp α] [IsArith α] (lft rgt : Term α) : Env (Term Bool)

Binary less-than; ltN chains: ltN #[a, b, c] is a < b ∧ b < c.

Equations

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

def Cvc.Typed.Term.realDivTotal [Ω] (lft rgt : Term Rat) : Env (Term Rat)

Real division, left-associative; zero on a zero divisor.

Equations

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

def Cvc.Typed.Term.tangent [Ω] (arg : Term Rat) : Env (Term Rat)

Tangent.

Equations

• arg.tangent = Cvc.Untyped.Term.tangent arg

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

gt over two or more terms.

Equations

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

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

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

• int [Ω] : OnInt → View.Arith Typ.int

  An operator with a result of sort Int.

• real [Ω] : OnRat → View.Arith Typ.real

  An operator with a result of sort Rat.

• any [Ω] {τ : Typ} : OnAny τ.Denote → View.Arith τ

  An operator whose result's sort is a type variable.

• bool [Ω] : OnBool → View.Arith Typ.bool

  An operator with a result of sort Bool.

inductive Cvc.Typed.View.Arith.OnRat [Ω] : Type

Arith's operators with a result of sort Rat.

• realDiv [Ω] (kids : Kids Rat) : OnRat

  Real division, left-associative; unspecified on a zero divisor.

  kids holds every operand, two or more.

• realDivTotal [Ω] (kids : Kids Rat) : OnRat

  Real division, left-associative; zero on a zero divisor.

  kids holds every operand, two or more.

• sqrt [Ω] (arg : Term Rat) : OnRat

  Square root.

• exp [Ω] (arg : Term Rat) : OnRat

  The exponential function.

• toReal [Ω] (α : Typ) {h0 : α.isArith = true} (arithTerm : Term α.Denote) : OnRat

  Conversion to a real.

• sine [Ω] (arg : Term Rat) : OnRat

  Sine.

• cosine [Ω] (arg : Term Rat) : OnRat

  Cosine.

• tangent [Ω] (arg : Term Rat) : OnRat

  Tangent.

• cosecant [Ω] (arg : Term Rat) : OnRat

  Cosecant.

• secant [Ω] (arg : Term Rat) : OnRat

  Secant.

• cotangent [Ω] (arg : Term Rat) : OnRat

  Cotangent.

• arcsine [Ω] (arg : Term Rat) : OnRat

  Arc sine.

• arccosine [Ω] (arg : Term Rat) : OnRat

  Arc cosine.

• arctangent [Ω] (arg : Term Rat) : OnRat

  Arc tangent.

• arccosecant [Ω] (arg : Term Rat) : OnRat

  Arc cosecant.

• arcsecant [Ω] (arg : Term Rat) : OnRat

  Arc secant.

• arccotangent [Ω] (arg : Term Rat) : OnRat

  Arc cotangent.

• pi [Ω] : OnRat

  The constant π.

inductive Cvc.Typed.View.Arith.OnAny [Ω] (β : Type) [ToTyp β] : Type

Arith's operators whose result's sort is a type variable.

• neg [Ω] {β : Type} [ToTyp β] {h0 : (Typ.of β).isArith = true} (arithTerm : Term β) : OnAny β

  Arithmetic negation.

• add [Ω] {β : Type} [ToTyp β] {h0 : (Typ.of β).isArith = true} (kids : Kids β) : OnAny β

  Binary addition.

  kids holds every operand, two or more.

• sub [Ω] {β : Type} [ToTyp β] {h0 : (Typ.of β).isArith = true} (kids : Kids β) : OnAny β

  Binary subtraction; subN is left-associative.

  kids holds every operand, two or more.

• mul [Ω] {β : Type} [ToTyp β] {h0 : (Typ.of β).isArith = true} (kids : Kids β) : OnAny β

  Binary multiplication.

  kids holds every operand, two or more.

• abs [Ω] {β : Type} [ToTyp β] {h0 : (Typ.of β).isArith = true} (arithTerm : Term β) : OnAny β

  Absolute value.

• pow [Ω] {β : Type} [ToTyp β] {h0 : (Typ.of β).isArith = true} (base exponent : Term β) : OnAny β

  Exponentiation.

inductive Cvc.Typed.View.Arith.OnInt [Ω] : Type

Arith's operators with a result of sort Int.

• intDiv [Ω] (kids : Kids Int) : OnInt

  Euclidean integer division, left-associative; unspecified on a zero divisor.

  kids holds every operand, two or more.

• intDivTotal [Ω] (kids : Kids Int) : OnInt

  Euclidean integer division, left-associative; zero on a zero divisor.

  kids holds every operand, two or more.

• intMod [Ω] (lft rgt : Term Int) : OnInt

  Euclidean integer modulus, never negative; unspecified on a zero divisor.

• intModTotal [Ω] (lft rgt : Term Int) : OnInt

  Euclidean integer modulus; the dividend on a zero divisor.

• pow2 [Ω] (exponent : Term Int) : OnInt

  Two raised to a non-negative exponent.

• log2 [Ω] (arg : Term Int) : OnInt

  Base-two logarithm.

• toInt [Ω] (α : Typ) {h0 : α.isArith = true} (arithTerm : Term α.Denote) : OnInt

  Conversion to an integer, rounding towards negative infinity.

• piand [Ω] (size lft rgt : Term Int) : OnInt

  Bit-wise and of the low size bits of lft and rgt; zero when size ≤ 0.

• iand [Ω] (size : Nat) (lft rgt : Term Int) : OnInt

  Bit-wise and of the low size bits of lft and rgt.

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

Takes a term apart one level, at its sort, if Arith 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.Arith.OnBool [Ω] : Type

Arith's operators with a result of sort Bool.

• lt [Ω] (α : Typ) {h0 : α.isArith = true} (kids : Kids α.Denote) : OnBool

  Binary less-than; ltN chains: ltN #[a, b, c] is a < b ∧ b < c.

  kids holds every operand, two or more.

• le [Ω] (α : Typ) {h0 : α.isArith = true} (kids : Kids α.Denote) : OnBool

  Binary less-than-or-equal-to; leN chains, as ltN does.

  kids holds every operand, two or more.

• gt [Ω] (α : Typ) {h0 : α.isArith = true} (kids : Kids α.Denote) : OnBool

  Binary greater-than; gtN chains, as ltN does.

  kids holds every operand, two or more.

• ge [Ω] (α : Typ) {h0 : α.isArith = true} (kids : Kids α.Denote) : OnBool

  Binary greater-than-or-equal-to; geN chains, as ltN does.

  kids holds every operand, two or more.

• isInt [Ω] (α : Typ) {h0 : α.isArith = true} (arithTerm : Term α.Denote) : OnBool

  Whether an arithmetic term denotes an integer.

• divisible [Ω] (divisor : Nat) (arg : Term Int) : OnBool

  Whether arg is divisible by divisor.

Values

def Cvc.Typed.Term.getSign [Ω] {α : Type} [ToTyp α] [IsArith α] (term : Term α) : Res Int

The sign of an arithmetic value: negative, zero or positive as -1, 0, 1.

Equations

• term.getSign = Cvc.Untyped.Term.getSign term

Machine-width views

An SMT integer is unbounded, so these say whether a value happens to fit a machine word and hand it over if it does. They are views of getIntValue, not a different value.

def Cvc.Typed.Term.isInt32Value [Ω] (term : Term Int) : Bool

Determine if this term is an Int32 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isInt32Value = Cvc.Untyped.Term.isInt32Value term

def Cvc.Typed.Term.getInt32Value [Ω] (term : Term Int) : Res Int32

Get the Int32 representation of this integral value.

NB: requires that this term is an Int32 value (see isInt32Value).

Equations

• term.getInt32Value = Cvc.Untyped.Term.getInt32Value term

def Cvc.Typed.Term.isInt64Value [Ω] (term : Term Int) : Bool

Determine if this term is an Int64 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isInt64Value = Cvc.Untyped.Term.isInt64Value term

def Cvc.Typed.Term.getInt64Value [Ω] (term : Term Int) : Res Int64

Get the Int64 representation of this integral value.

NB: requires that this term is an Int64 value (see isInt64Value).

Equations

• term.getInt64Value = Cvc.Untyped.Term.getInt64Value term

def Cvc.Typed.Term.isUInt32Value [Ω] (term : Term Int) : Bool

Determine if this term is an UInt32 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isUInt32Value = Cvc.Untyped.Term.isUInt32Value term

def Cvc.Typed.Term.getUInt32Value [Ω] (term : Term Int) : Res UInt32

Get the UInt32 representation of this integral value.

NB: requires that this term is an UInt32 value (see isUInt32Value).

Equations

• term.getUInt32Value = Cvc.Untyped.Term.getUInt32Value term

def Cvc.Typed.Term.isUInt64Value [Ω] (term : Term Int) : Bool

Determine if this term is an UInt64 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isUInt64Value = Cvc.Untyped.Term.isUInt64Value term

def Cvc.Typed.Term.getUInt64Value [Ω] (term : Term Int) : Res UInt64

Get the UInt64 representation of this integral value.

NB: requires that this term is an UInt64 value (see isUInt64Value).

Equations

• term.getUInt64Value = Cvc.Untyped.Term.getUInt64Value term

def Cvc.Typed.Term.isReal32Value [Ω] (term : Term Rat) : Bool

Whether a term denotes a real that fits a 32-bit numerator and denominator.

Equations

• term.isReal32Value = Cvc.Untyped.Term.isReal32Value term

def Cvc.Typed.Term.getReal32Value [Ω] (term : Term Rat) : Res (Int32 × UInt32)

The numerator and denominator of a real value, at 32 bits.

Equations

• term.getReal32Value = Cvc.Untyped.Term.getReal32Value term

def Cvc.Typed.Term.isReal64Value [Ω] (term : Term Rat) : Bool

Whether a term denotes a real that fits a 64-bit numerator and denominator.

Equations

• term.isReal64Value = Cvc.Untyped.Term.isReal64Value term

def Cvc.Typed.Term.getReal64Value [Ω] (term : Term Rat) : Res (Int64 × UInt64)

The numerator and denominator of a real value, at 64 bits.

Equations

• term.getReal64Value = Cvc.Untyped.Term.getReal64Value term

Real algebraic numbers

A real algebraic number is not a rational, so it has no getRatValue. It is described instead by a polynomial it is a root of, together with an interval isolating that root.

def Cvc.Typed.Term.isRealAlgebraicNumber [Ω] (term : Term Rat) : Bool

Determine if this term is a real algebraic number.

Equations

• term.isRealAlgebraicNumber = Cvc.Untyped.Term.isRealAlgebraicNumber term

def Cvc.Typed.Term.getRealAlgebraicNumberPolynomial [Ω] (term : Term Rat) (v : BVar Rat) : Env (Term Rat)

The polynomial a real algebraic number is a root of, written in the bound variable v.

Equations

• term.getRealAlgebraicNumberPolynomial v = Cvc.Untyped.Term.getRealAlgebraicNumberPolynomial term v.toUntyped

def Cvc.Typed.Term.getRealAlgebraicNumberLowerBound [Ω] (term : Term Rat) : Env (Term Rat)

Get the lower bound for a real algebraic number value.

NB: asserts isRealAlgebraicNumber.

Equations

• term.getRealAlgebraicNumberLowerBound = Cvc.Untyped.Term.getRealAlgebraicNumberLowerBound term

def Cvc.Typed.Term.getRealAlgebraicNumberUpperBound [Ω] (term : Term Rat) : Env (Term Rat)

Get the upper bound for a real algebraic number value.

NB: asserts isRealAlgebraicNumber.

Equations

• term.getRealAlgebraicNumberUpperBound = Cvc.Untyped.Term.getRealAlgebraicNumberUpperBound term

def Cvc.Typed.Term.isIntValue [Ω] (term : Term Int) : Bool

Determine if this real/integer constant term is an integral value.

Equations

• term.isIntValue = Cvc.Untyped.Term.isIntValue term

def Cvc.Typed.Term.getIntValue [Ω] (term : Term Int) : Res Int

The integer a term denotes, failing if it denotes none.

Equations

• term.getIntValue = Cvc.Untyped.Term.getIntValue term

def Cvc.Typed.Term.getIntValue? [Ω] (term : Term Int) : Option Int

The integer a term denotes, failing if it denotes none.

Equations

• term.getIntValue? = Cvc.Untyped.Term.getIntValue? term

def Cvc.Typed.Term.isRealValue [Ω] (term : Term Rat) : Bool

Determine if this term is a rational value.

NB: A term of kind Kind.PI is not considered to be a real value.

Equations

• term.isRealValue = Cvc.Untyped.Term.isRealValue term

def Cvc.Typed.Term.getRealValue [Ω] (term : Term Rat) : Res String

The real a term denotes as a string, failing if it denotes none.

Equations

• term.getRealValue = Cvc.Untyped.Term.getRealValue term

def Cvc.Typed.Term.getRealValue? [Ω] (term : Term Rat) : Option String

The real a term denotes as a string, failing if it denotes none.

Equations

• term.getRealValue? = Cvc.Untyped.Term.getRealValue? term

def Cvc.Typed.Term.getRatValue [Ω] (term : Term Rat) : Res Rat

The real a term denotes as a Rat, failing if it denotes none.

An irrational model value, which nonlinear real arithmetic can produce, is no Rat: read it as a term instead, and take it apart with the getRealAlgebraicNumber… functions.

Equations

• term.getRatValue = Cvc.Untyped.Term.getRatValue term

def Cvc.Typed.Term.getRatValue? [Ω] (term : Term Rat) : Option Rat

The real a term denotes as a Rat, failing if it denotes none.

An irrational model value, which nonlinear real arithmetic can produce, is no Rat: read it as a term instead, and take it apart with the getRealAlgebraicNumber… functions.

Equations

• term.getRatValue? = Cvc.Untyped.Term.getRatValue? term

@[instance_reducible]

instance Cvc.Typed.Term.instSrtLikeInt : SrtLike Int

Equations

• Cvc.Typed.Term.instSrtLikeInt = { toToTyp := Cvc.ToTyp.instInt, termToValue := fun [Cvc.Ω] (t : Cvc.Typed.Term Int) => liftM t.getIntValue, valueToTerm := fun [Cvc.Ω] => Cvc.Typed.Term.mkInt }

@[instance_reducible]

instance Cvc.Typed.Term.instSrtLikeRat : SrtLike Rat

Equations

• Cvc.Typed.Term.instSrtLikeRat = { toToTyp := Cvc.ToTyp.instRat, termToValue := fun [Cvc.Ω] (t : Cvc.Typed.Term Rat) => liftM t.getRatValue, valueToTerm := fun [Cvc.Ω] => Cvc.Typed.Term.mkReal }

smt! literals of this theory

An integer literal is a Term Int and a decimal one a Term Rat (1.5, 1.5e-3): with r : Term Rat, write smt! r + 1.0, since smt! r + 1 does not typecheck.