cvc5's enumerations

The cvc5 enumerations the API takes or answers, mirrored as Lean inductives, plus the constant combinators 𝕂 and 𝕂².

def Cvc.term𝕂_ : Lean.ParserDescr

The constant combinator.

Equations

• Cvc.term𝕂_ = Lean.ParserDescr.node `Cvc.term𝕂_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝕂 ") (Lean.ParserDescr.cat `term 0))

def Cvc.«term𝕂²_» : Lean.ParserDescr

The constant combinator ignoring its first two arguments.

Equations

• Cvc.«term𝕂²_» = Lean.ParserDescr.node `Cvc.«term𝕂²_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝕂² ") (Lean.ParserDescr.cat `term 0))

def Cvc.enumDefStx : Lean.ParserDescr

Equations

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

def Cvc.enumDefStxElab : Lean.Elab.Command.CommandElab

Equations

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

@[instance_reducible]

instance Cvc.Unknown.instReprExplanation : Repr Explanation

Equations

• Cvc.Unknown.instReprExplanation = { reprPrec := Cvc.Unknown.instReprExplanation.repr }

@[instance_reducible]

instance Cvc.Unknown.Explanation.instToString : ToString Explanation

Equations

• Cvc.Unknown.Explanation.instToString = { toString := fun (x : Cvc.Unknown.Explanation) => toString (repr x) }

@[instance_reducible]

instance Cvc.Unknown.Explanation.instLE : LE Explanation

Equations

• Cvc.Unknown.Explanation.instLE = { le := fun (x1 x2 : Cvc.Unknown.Explanation) => x1.ble x2 = true }

@[instance_reducible]

instance Cvc.Unknown.Explanation.instInhabited : Inhabited Explanation

Equations

• Cvc.Unknown.Explanation.instInhabited = { default := Cvc.Unknown.Explanation.unknownReason }

@[instance_reducible]

instance Cvc.Unknown.instHashableExplanation : Hashable Explanation

Equations

• Cvc.Unknown.instHashableExplanation = { hash := Cvc.Unknown.instHashableExplanation.hash }

@[instance_reducible]

instance Cvc.Unknown.Explanation.instLT : LT Explanation

Equations

• Cvc.Unknown.Explanation.instLT = { lt := fun (x1 x2 : Cvc.Unknown.Explanation) => x1.blt x2 = true }

@[instance_reducible]

instance Cvc.Unknown.Explanation.instDecidableLE : DecidableLE Explanation

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Unknown.instOrdExplanation : Ord Explanation

Equations

• Cvc.Unknown.instOrdExplanation = { compare := Cvc.Unknown.instOrdExplanation.ord }

inductive Cvc.Unknown.Explanation : Type

Why a check answered "unknown".

• requiresFullCheck : Explanation

  A full check is required, for instance after preprocessing only.

• incomplete : Explanation

  A theory solver is incomplete.

• timeOut : Explanation

  The time limit was reached.

• resourceOut : Explanation

  The resource limit was reached.

• memOut : Explanation

  The memory limit was reached.

• interrupted : Explanation

  The solver was interrupted.

• unsupported : Explanation

  An unsupported feature was encountered.

• other : Explanation

  Another reason.

• requiresCheckAgain : Explanation

  Another check is required.

• unknownReason : Explanation

  No specific reason was given.

def Cvc.Unknown.instHashableExplanation.hash : Explanation → UInt64

Equations

• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.requiresFullCheck = 0
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.incomplete = 1
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.timeOut = 2
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.resourceOut = 3
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.memOut = 4
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.interrupted = 5
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.unsupported = 6
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.other = 7
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.requiresCheckAgain = 8
• Cvc.Unknown.instHashableExplanation.hash Cvc.Unknown.Explanation.unknownReason = 9

def Cvc.Unknown.instReprExplanation.repr : Explanation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cvc.Unknown.instBEqExplanation : BEq Explanation

Equations

• Cvc.Unknown.instBEqExplanation = { beq := Cvc.Unknown.instBEqExplanation.beq }

@[instance_reducible]

instance Cvc.Unknown.Explanation.instDecidableLT : DecidableLT Explanation

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

def Cvc.Unknown.instBEqExplanation.beq : Explanation → Explanation → Bool

Equations

• Cvc.Unknown.instBEqExplanation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Cvc.Unknown.instOrdExplanation.ord : Explanation → Explanation → Ordering

Equations

• Cvc.Unknown.instOrdExplanation.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Cvc.Unknown.instDecidableEqExplanation : DecidableEq Explanation

Equations

• Cvc.Unknown.instDecidableEqExplanation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Cvc.Unknown.Explanation.ble : Explanation → Explanation → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

@[reducible, inline]

abbrev Cvc.Unknown.Explanation.blt : Explanation → Explanation → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

@[reducible, inline]

abbrev Cvc.Float.RoundingMode.ble : RoundingMode → RoundingMode → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

@[instance_reducible]

instance Cvc.Float.RoundingMode.instLT : LT RoundingMode

Equations

• Cvc.Float.RoundingMode.instLT = { lt := fun (x1 x2 : Cvc.Float.RoundingMode) => x1.blt x2 = true }

def Cvc.Float.instReprRoundingMode.repr : RoundingMode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cvc.Float.instOrdRoundingMode : Ord RoundingMode

Equations

• Cvc.Float.instOrdRoundingMode = { compare := Cvc.Float.instOrdRoundingMode.ord }

@[instance_reducible]

instance Cvc.Float.instHashableRoundingMode : Hashable RoundingMode

Equations

• Cvc.Float.instHashableRoundingMode = { hash := Cvc.Float.instHashableRoundingMode.hash }

@[instance_reducible]

instance Cvc.Float.instBEqRoundingMode : BEq RoundingMode

Equations

• Cvc.Float.instBEqRoundingMode = { beq := Cvc.Float.instBEqRoundingMode.beq }

def Cvc.Float.instHashableRoundingMode.hash : RoundingMode → UInt64

Equations

• Cvc.Float.instHashableRoundingMode.hash Cvc.Float.RoundingMode.nearestTiesToEven = 0
• Cvc.Float.instHashableRoundingMode.hash Cvc.Float.RoundingMode.towardPositive = 1
• Cvc.Float.instHashableRoundingMode.hash Cvc.Float.RoundingMode.towardNegative = 2
• Cvc.Float.instHashableRoundingMode.hash Cvc.Float.RoundingMode.towardZero = 3
• Cvc.Float.instHashableRoundingMode.hash Cvc.Float.RoundingMode.nearestTiesToAway = 4

@[instance_reducible]

instance Cvc.Float.instReprRoundingMode : Repr RoundingMode

Equations

• Cvc.Float.instReprRoundingMode = { reprPrec := Cvc.Float.instReprRoundingMode.repr }

@[reducible, inline]

abbrev Cvc.Float.RoundingMode.blt : RoundingMode → RoundingMode → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

@[instance_reducible]

instance Cvc.Float.RoundingMode.instLE : LE RoundingMode

Equations

• Cvc.Float.RoundingMode.instLE = { le := fun (x1 x2 : Cvc.Float.RoundingMode) => x1.ble x2 = true }

@[instance_reducible]

instance Cvc.Float.RoundingMode.instInhabited : Inhabited RoundingMode

Equations

• Cvc.Float.RoundingMode.instInhabited = { default := Cvc.Float.RoundingMode.ofNat 0 }

@[instance_reducible]

instance Cvc.Float.RoundingMode.instDecidableLT : DecidableLT RoundingMode

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Float.instDecidableEqRoundingMode : DecidableEq RoundingMode

Equations

• Cvc.Float.instDecidableEqRoundingMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Float.instOrdRoundingMode.ord : RoundingMode → RoundingMode → Ordering

Equations

• Cvc.Float.instOrdRoundingMode.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

def Cvc.Float.instBEqRoundingMode.beq : RoundingMode → RoundingMode → Bool

Equations

• Cvc.Float.instBEqRoundingMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Cvc.Float.RoundingMode.instToString : ToString RoundingMode

Equations

• Cvc.Float.RoundingMode.instToString = { toString := fun (x : Cvc.Float.RoundingMode) => toString (repr x) }

@[instance_reducible]

instance Cvc.Float.RoundingMode.instDecidableLE : DecidableLE RoundingMode

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

inductive Cvc.Float.RoundingMode : Type

The SMT-LIB rounding modes of floating-point arithmetic.

• nearestTiesToEven : RoundingMode

  To the nearest representable number, ties to the one with an even last digit.

• towardPositive : RoundingMode

  Towards positive infinity.

• towardNegative : RoundingMode

  Towards negative infinity.

• towardZero : RoundingMode

  Towards zero.

• nearestTiesToAway : RoundingMode

  To the nearest representable number, ties away from zero.

inductive Cvc.Model.BlockMode : Type

How a solver's blockModel blocks a model.

• literals : BlockMode

  Block models based on the SAT skeleton.

• values : BlockMode

  Block models based on the concrete model values for the free variables.

@[instance_reducible]

instance Cvc.Model.instReprBlockMode : Repr BlockMode

Equations

• Cvc.Model.instReprBlockMode = { reprPrec := Cvc.Model.instReprBlockMode.repr }

@[instance_reducible]

instance Cvc.Model.instBEqBlockMode : BEq BlockMode

Equations

• Cvc.Model.instBEqBlockMode = { beq := Cvc.Model.instBEqBlockMode.beq }

@[instance_reducible]

instance Cvc.Model.instHashableBlockMode : Hashable BlockMode

Equations

• Cvc.Model.instHashableBlockMode = { hash := Cvc.Model.instHashableBlockMode.hash }

@[reducible, inline]

abbrev Cvc.Model.BlockMode.blt : BlockMode → BlockMode → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

@[instance_reducible]

instance Cvc.Model.BlockMode.instLE : LE BlockMode

Equations

• Cvc.Model.BlockMode.instLE = { le := fun (x1 x2 : Cvc.Model.BlockMode) => x1.ble x2 = true }

@[instance_reducible]

instance Cvc.Model.instOrdBlockMode : Ord BlockMode

Equations

• Cvc.Model.instOrdBlockMode = { compare := Cvc.Model.instOrdBlockMode.ord }

def Cvc.Model.instBEqBlockMode.beq : BlockMode → BlockMode → Bool

Equations

• Cvc.Model.instBEqBlockMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Cvc.Model.BlockMode.instInhabited : Inhabited BlockMode

Equations

• Cvc.Model.BlockMode.instInhabited = { default := Cvc.Model.BlockMode.ofNat 0 }

@[instance_reducible]

instance Cvc.Model.BlockMode.instLT : LT BlockMode

Equations

• Cvc.Model.BlockMode.instLT = { lt := fun (x1 x2 : Cvc.Model.BlockMode) => x1.blt x2 = true }

def Cvc.Model.instHashableBlockMode.hash : BlockMode → UInt64

Equations

• Cvc.Model.instHashableBlockMode.hash Cvc.Model.BlockMode.literals = 0
• Cvc.Model.instHashableBlockMode.hash Cvc.Model.BlockMode.values = 1

@[instance_reducible]

instance Cvc.Model.instDecidableEqBlockMode : DecidableEq BlockMode

Equations

• Cvc.Model.instDecidableEqBlockMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Model.BlockMode.instDecidableLT : DecidableLT BlockMode

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Model.BlockMode.instDecidableLE : DecidableLE BlockMode

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Model.BlockMode.instToString : ToString BlockMode

Equations

• Cvc.Model.BlockMode.instToString = { toString := fun (x : Cvc.Model.BlockMode) => toString (repr x) }

@[reducible, inline]

abbrev Cvc.Model.BlockMode.ble : BlockMode → BlockMode → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

def Cvc.Model.instOrdBlockMode.ord : BlockMode → BlockMode → Ordering

Equations

• Cvc.Model.instOrdBlockMode.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

def Cvc.Model.instReprBlockMode.repr : BlockMode → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Model.instReprBlockMode.repr Cvc.Model.BlockMode.values prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Model.BlockMode.values")).group prec✝

@[instance_reducible]

instance Cvc.LearnedLitType.instDecidableLE : DecidableLE LearnedLitType

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.LearnedLitType.instLE : LE LearnedLitType

Equations

• Cvc.LearnedLitType.instLE = { le := fun (x1 x2 : Cvc.LearnedLitType) => x1.ble x2 = true }

@[instance_reducible]

instance Cvc.instReprLearnedLitType : Repr LearnedLitType

Equations

• Cvc.instReprLearnedLitType = { reprPrec := Cvc.instReprLearnedLitType.repr }

def Cvc.instBEqLearnedLitType.beq : LearnedLitType → LearnedLitType → Bool

Equations

• Cvc.instBEqLearnedLitType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Cvc.instHashableLearnedLitType.hash : LearnedLitType → UInt64

Equations

• Cvc.instHashableLearnedLitType.hash Cvc.LearnedLitType.preprocessSolved = 0
• Cvc.instHashableLearnedLitType.hash Cvc.LearnedLitType.preprocess = 1
• Cvc.instHashableLearnedLitType.hash Cvc.LearnedLitType.input = 2
• Cvc.instHashableLearnedLitType.hash Cvc.LearnedLitType.solvable = 3
• Cvc.instHashableLearnedLitType.hash Cvc.LearnedLitType.constantProp = 4
• Cvc.instHashableLearnedLitType.hash Cvc.LearnedLitType.internal = 5
• Cvc.instHashableLearnedLitType.hash Cvc.LearnedLitType.unknown = 6

def Cvc.instOrdLearnedLitType.ord : LearnedLitType → LearnedLitType → Ordering

Equations

• Cvc.instOrdLearnedLitType.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[reducible, inline]

abbrev Cvc.LearnedLitType.blt : LearnedLitType → LearnedLitType → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

inductive Cvc.LearnedLitType : Type

Kinds of learned literals.

A literal may belong to several kinds; it is classified by the first one in this list it fits.

• preprocessSolved : LearnedLitType

  An equality (= x t), x not occurring in t, turned into a substitution.

• preprocess : LearnedLitType

  A top-level literal (unit clause) from the preprocessed input formulas.

• input : LearnedLitType

  A literal of the preprocessed input formulas that is not top-level after preprocessing.

  Typically the most interesting kind of literal to learn.

• solvable : LearnedLitType

  An internal literal (= x t) solvable for an input variable x not occurring in t.

• constantProp : LearnedLitType

  An internal literal (= t c), c a constant, propagating a constant for an input term.

• internal : LearnedLitType

  Any other internal literal.

• unknown : LearnedLitType

  Answered when the produce-learned-literals option is not set.

def Cvc.instReprLearnedLitType.repr : LearnedLitType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.instReprLearnedLitType.repr Cvc.LearnedLitType.input prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.LearnedLitType.input")).group prec✝
• Cvc.instReprLearnedLitType.repr Cvc.LearnedLitType.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.LearnedLitType.unknown")).group prec✝

@[instance_reducible]

instance Cvc.instDecidableEqLearnedLitType : DecidableEq LearnedLitType

Equations

• Cvc.instDecidableEqLearnedLitType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.instOrdLearnedLitType : Ord LearnedLitType

Equations

• Cvc.instOrdLearnedLitType = { compare := Cvc.instOrdLearnedLitType.ord }

@[instance_reducible]

instance Cvc.instBEqLearnedLitType : BEq LearnedLitType

Equations

• Cvc.instBEqLearnedLitType = { beq := Cvc.instBEqLearnedLitType.beq }

@[instance_reducible]

instance Cvc.LearnedLitType.instDecidableLT : DecidableLT LearnedLitType

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.LearnedLitType.instToString : ToString LearnedLitType

Equations

• Cvc.LearnedLitType.instToString = { toString := fun (x : Cvc.LearnedLitType) => toString (repr x) }

@[reducible, inline]

abbrev Cvc.LearnedLitType.ble : LearnedLitType → LearnedLitType → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

@[instance_reducible]

instance Cvc.LearnedLitType.instLT : LT LearnedLitType

Equations

• Cvc.LearnedLitType.instLT = { lt := fun (x1 x2 : Cvc.LearnedLitType) => x1.blt x2 = true }

@[instance_reducible]

instance Cvc.LearnedLitType.instInhabited : Inhabited LearnedLitType

Equations

• Cvc.LearnedLitType.instInhabited = { default := Cvc.LearnedLitType.ofNat 0 }

@[instance_reducible]

instance Cvc.instHashableLearnedLitType : Hashable LearnedLitType

Equations

• Cvc.instHashableLearnedLitType = { hash := Cvc.instHashableLearnedLitType.hash }

def Cvc.Proof.instOrdComponent.ord : Component → Component → Ordering

Equations

• Cvc.Proof.instOrdComponent.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Cvc.Proof.Component.instDecidableLE : DecidableLE Component

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

def Cvc.Proof.instBEqComponent.beq : Component → Component → Bool

Equations

• Cvc.Proof.instBEqComponent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[reducible, inline]

abbrev Cvc.Proof.Component.blt : Component → Component → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

inductive Cvc.Proof.Component : Type

The part of a refutation a proof is asked for.

• rawPreprocess : Component

  Proofs of the preprocessed input formulas, from the input formulas.

• preprocess : Component

  Proofs of the clauses the SAT proof uses, from the input formulas it uses.

• sat : Component

  A proof of false from the preprocessed input clauses and the theory lemmas.

• theoryLemmas : Component

  Proofs of the theory lemmas the SAT proof uses.

• full : Component

  A proof of false from the input formulas.

def Cvc.Proof.instReprComponent.repr : Component → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Proof.instReprComponent.repr Cvc.Proof.Component.sat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Component.sat")).group prec✝
• Cvc.Proof.instReprComponent.repr Cvc.Proof.Component.full prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Component.full")).group prec✝

@[instance_reducible]

instance Cvc.Proof.instOrdComponent : Ord Component

Equations

• Cvc.Proof.instOrdComponent = { compare := Cvc.Proof.instOrdComponent.ord }

@[reducible, inline]

abbrev Cvc.Proof.Component.ble : Component → Component → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

@[instance_reducible]

instance Cvc.Proof.instBEqComponent : BEq Component

Equations

• Cvc.Proof.instBEqComponent = { beq := Cvc.Proof.instBEqComponent.beq }

@[instance_reducible]

instance Cvc.Proof.Component.instInhabited : Inhabited Component

Equations

• Cvc.Proof.Component.instInhabited = { default := Cvc.Proof.Component.full }

@[instance_reducible]

instance Cvc.Proof.Component.instDecidableLT : DecidableLT Component

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Proof.Component.instLE : LE Component

Equations

• Cvc.Proof.Component.instLE = { le := fun (x1 x2 : Cvc.Proof.Component) => x1.ble x2 = true }

@[instance_reducible]

instance Cvc.Proof.Component.instToString : ToString Component

Equations

• Cvc.Proof.Component.instToString = { toString := fun (x : Cvc.Proof.Component) => toString (repr x) }

def Cvc.Proof.instHashableComponent.hash : Component → UInt64

Equations

• Cvc.Proof.instHashableComponent.hash Cvc.Proof.Component.rawPreprocess = 0
• Cvc.Proof.instHashableComponent.hash Cvc.Proof.Component.preprocess = 1
• Cvc.Proof.instHashableComponent.hash Cvc.Proof.Component.sat = 2
• Cvc.Proof.instHashableComponent.hash Cvc.Proof.Component.theoryLemmas = 3
• Cvc.Proof.instHashableComponent.hash Cvc.Proof.Component.full = 4

@[instance_reducible]

instance Cvc.Proof.Component.instLT : LT Component

Equations

• Cvc.Proof.Component.instLT = { lt := fun (x1 x2 : Cvc.Proof.Component) => x1.blt x2 = true }

@[instance_reducible]

instance Cvc.Proof.instHashableComponent : Hashable Component

Equations

• Cvc.Proof.instHashableComponent = { hash := Cvc.Proof.instHashableComponent.hash }

@[instance_reducible]

instance Cvc.Proof.instReprComponent : Repr Component

Equations

• Cvc.Proof.instReprComponent = { reprPrec := Cvc.Proof.instReprComponent.repr }

@[instance_reducible]

instance Cvc.Proof.instDecidableEqComponent : DecidableEq Component

Equations

• Cvc.Proof.instDecidableEqComponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Proof.Format.instInhabited : Inhabited Format

Equations

• Cvc.Proof.Format.instInhabited = { default := Cvc.Proof.Format.fromSolver }

@[instance_reducible]

instance Cvc.Proof.Format.instDecidableLE : DecidableLE Format

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Proof.instReprFormat : Repr Format

Equations

• Cvc.Proof.instReprFormat = { reprPrec := Cvc.Proof.instReprFormat.repr }

@[instance_reducible]

instance Cvc.Proof.instBEqFormat : BEq Format

Equations

• Cvc.Proof.instBEqFormat = { beq := Cvc.Proof.instBEqFormat.beq }

@[reducible, inline]

abbrev Cvc.Proof.Format.ble : Format → Format → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

@[instance_reducible]

instance Cvc.Proof.instDecidableEqFormat : DecidableEq Format

Equations

• Cvc.Proof.instDecidableEqFormat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Proof.instHashableFormat.hash : Format → UInt64

Equations

• Cvc.Proof.instHashableFormat.hash Cvc.Proof.Format.no = 0
• Cvc.Proof.instHashableFormat.hash Cvc.Proof.Format.dot = 1
• Cvc.Proof.instHashableFormat.hash Cvc.Proof.Format.lfsc = 2
• Cvc.Proof.instHashableFormat.hash Cvc.Proof.Format.alethe = 3
• Cvc.Proof.instHashableFormat.hash Cvc.Proof.Format.cpc = 4
• Cvc.Proof.instHashableFormat.hash Cvc.Proof.Format.fromSolver = 5

def Cvc.Proof.instBEqFormat.beq : Format → Format → Bool

Equations

• Cvc.Proof.instBEqFormat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Cvc.Proof.instOrdFormat : Ord Format

Equations

• Cvc.Proof.instOrdFormat = { compare := Cvc.Proof.instOrdFormat.ord }

@[instance_reducible]

instance Cvc.Proof.Format.instLE : LE Format

Equations

• Cvc.Proof.Format.instLE = { le := fun (x1 x2 : Cvc.Proof.Format) => x1.ble x2 = true }

def Cvc.Proof.instOrdFormat.ord : Format → Format → Ordering

Equations

• Cvc.Proof.instOrdFormat.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Cvc.Proof.Format.instToString : ToString Format

Equations

• Cvc.Proof.Format.instToString = { toString := fun (x : Cvc.Proof.Format) => toString (repr x) }

def Cvc.Proof.instReprFormat.repr : Format → Nat → Std.Format

Equations

• Cvc.Proof.instReprFormat.repr Cvc.Proof.Format.no prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Format.no")).group prec✝
• Cvc.Proof.instReprFormat.repr Cvc.Proof.Format.dot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Format.dot")).group prec✝
• Cvc.Proof.instReprFormat.repr Cvc.Proof.Format.lfsc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Format.lfsc")).group prec✝
• Cvc.Proof.instReprFormat.repr Cvc.Proof.Format.alethe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Format.alethe")).group prec✝
• Cvc.Proof.instReprFormat.repr Cvc.Proof.Format.cpc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Format.cpc")).group prec✝
• Cvc.Proof.instReprFormat.repr Cvc.Proof.Format.fromSolver prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Proof.Format.fromSolver")).group prec✝

inductive Cvc.Proof.Format : Type

The format a proof is printed in.

• no : Format

  cvc5's own output, untranslated; the only format a non-full proof can be printed in.

• dot : Format

  DOT, for Graphviz.

• lfsc : Format

  LFSC.

• alethe : Format

  Alethe.

• cpc : Format

  The Cooperating Proof Calculus, over Eunoia signatures.

• fromSolver : Format

  The format the solver's options select.

@[instance_reducible]

instance Cvc.Proof.Format.instLT : LT Format

Equations

• Cvc.Proof.Format.instLT = { lt := fun (x1 x2 : Cvc.Proof.Format) => x1.blt x2 = true }

@[instance_reducible]

instance Cvc.Proof.Format.instDecidableLT : DecidableLT Format

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Proof.instHashableFormat : Hashable Format

Equations

• Cvc.Proof.instHashableFormat = { hash := Cvc.Proof.instHashableFormat.hash }

@[reducible, inline]

abbrev Cvc.Proof.Format.blt : Format → Format → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

@[reducible, inline]

abbrev Cvc.Synth.FindTarget.ble : FindTarget → FindTarget → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

@[instance_reducible]

instance Cvc.Synth.instHashableFindTarget : Hashable FindTarget

Equations

• Cvc.Synth.instHashableFindTarget = { hash := Cvc.Synth.instHashableFindTarget.hash }

inductive Cvc.Synth.FindTarget : Type

What Solver.findSynth looks for.

• enum : FindTarget

  The next term in the enumeration of the grammar.

• rewrite : FindTarget

  A pair of equivalent terms t, s of the grammar that do not rewrite to the same term.

  Answers the equality (= t s); useful to synthesize rewrite rules. The rewriter is the one the sygus-rewrite option selects.

• rewriteUnsound : FindTarget

  A term t of the grammar rewriting to a term s not equivalent to it.

  Answers the equality (= t s); any answer is an unsoundness of the rewriter.

• rewriteInput : FindTarget

  Like rewrite, for terms matching terms of the input assertions.

• query : FindTarget

  A query over the grammar, as equalities if its terms are not Boolean.

@[instance_reducible]

instance Cvc.Synth.FindTarget.instLT : LT FindTarget

Equations

• Cvc.Synth.FindTarget.instLT = { lt := fun (x1 x2 : Cvc.Synth.FindTarget) => x1.blt x2 = true }

@[instance_reducible]

instance Cvc.Synth.FindTarget.instDecidableLE : DecidableLE FindTarget

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

def Cvc.Synth.instBEqFindTarget.beq : FindTarget → FindTarget → Bool

Equations

• Cvc.Synth.instBEqFindTarget.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Cvc.Synth.FindTarget.instToString : ToString FindTarget

Equations

• Cvc.Synth.FindTarget.instToString = { toString := fun (x : Cvc.Synth.FindTarget) => toString (repr x) }

@[instance_reducible]

instance Cvc.Synth.FindTarget.instDecidableLT : DecidableLT FindTarget

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Synth.FindTarget.instInhabited : Inhabited FindTarget

Equations

• Cvc.Synth.FindTarget.instInhabited = { default := Cvc.Synth.FindTarget.ofNat 0 }

def Cvc.Synth.instHashableFindTarget.hash : FindTarget → UInt64

Equations

• Cvc.Synth.instHashableFindTarget.hash Cvc.Synth.FindTarget.enum = 0
• Cvc.Synth.instHashableFindTarget.hash Cvc.Synth.FindTarget.rewrite = 1
• Cvc.Synth.instHashableFindTarget.hash Cvc.Synth.FindTarget.rewriteUnsound = 2
• Cvc.Synth.instHashableFindTarget.hash Cvc.Synth.FindTarget.rewriteInput = 3
• Cvc.Synth.instHashableFindTarget.hash Cvc.Synth.FindTarget.query = 4

@[reducible, inline]

abbrev Cvc.Synth.FindTarget.blt : FindTarget → FindTarget → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

def Cvc.Synth.instReprFindTarget.repr : FindTarget → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Synth.instReprFindTarget.repr Cvc.Synth.FindTarget.enum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Synth.FindTarget.enum")).group prec✝

@[instance_reducible]

instance Cvc.Synth.instBEqFindTarget : BEq FindTarget

Equations

• Cvc.Synth.instBEqFindTarget = { beq := Cvc.Synth.instBEqFindTarget.beq }

@[instance_reducible]

instance Cvc.Synth.instReprFindTarget : Repr FindTarget

Equations

• Cvc.Synth.instReprFindTarget = { reprPrec := Cvc.Synth.instReprFindTarget.repr }

@[instance_reducible]

instance Cvc.Synth.instOrdFindTarget : Ord FindTarget

Equations

• Cvc.Synth.instOrdFindTarget = { compare := Cvc.Synth.instOrdFindTarget.ord }

@[instance_reducible]

instance Cvc.Synth.FindTarget.instLE : LE FindTarget

Equations

• Cvc.Synth.FindTarget.instLE = { le := fun (x1 x2 : Cvc.Synth.FindTarget) => x1.ble x2 = true }

def Cvc.Synth.instOrdFindTarget.ord : FindTarget → FindTarget → Ordering

Equations

• Cvc.Synth.instOrdFindTarget.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Cvc.Synth.instDecidableEqFindTarget : DecidableEq FindTarget

Equations

• Cvc.Synth.instDecidableEqFindTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Option.instHashableCategory : Hashable Category

Equations

• Cvc.Option.instHashableCategory = { hash := Cvc.Option.instHashableCategory.hash }

@[instance_reducible]

instance Cvc.Option.instOrdCategory : Ord Category

Equations

• Cvc.Option.instOrdCategory = { compare := Cvc.Option.instOrdCategory.ord }

inductive Cvc.Option.Category : Type

Option category enumeration.

Specifies the category of an option for user interface purposes.

• regular : Category

  Option available to regular users.

• expert : Category

  Option available to expert users.

• common : Category

  Common options.

• undocumented : Category

  Undocumented options.

@[instance_reducible]

instance Cvc.Option.Category.instToString : ToString Category

Equations

• Cvc.Option.Category.instToString = { toString := fun (x : Cvc.Option.Category) => toString (repr x) }

@[reducible, inline]

abbrev Cvc.Option.Category.blt : Category → Category → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

def Cvc.Option.instBEqCategory.beq : Category → Category → Bool

Equations

• Cvc.Option.instBEqCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Cvc.Option.Category.instDecidableLE : DecidableLE Category

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Option.Category.instDecidableLT : DecidableLT Category

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Option.Category.instLE : LE Category

Equations

• Cvc.Option.Category.instLE = { le := fun (x1 x2 : Cvc.Option.Category) => x1.ble x2 = true }

def Cvc.Option.instOrdCategory.ord : Category → Category → Ordering

Equations

• Cvc.Option.instOrdCategory.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Cvc.Option.instDecidableEqCategory : DecidableEq Category

Equations

• Cvc.Option.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Option.instReprCategory : Repr Category

Equations

• Cvc.Option.instReprCategory = { reprPrec := Cvc.Option.instReprCategory.repr }

def Cvc.Option.instReprCategory.repr : Category → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Option.instReprCategory.repr Cvc.Option.Category.expert prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Option.Category.expert")).group prec✝
• Cvc.Option.instReprCategory.repr Cvc.Option.Category.common prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Option.Category.common")).group prec✝

def Cvc.Option.instHashableCategory.hash : Category → UInt64

Equations

• Cvc.Option.instHashableCategory.hash Cvc.Option.Category.regular = 0
• Cvc.Option.instHashableCategory.hash Cvc.Option.Category.expert = 1
• Cvc.Option.instHashableCategory.hash Cvc.Option.Category.common = 2
• Cvc.Option.instHashableCategory.hash Cvc.Option.Category.undocumented = 3

@[instance_reducible]

instance Cvc.Option.Category.instInhabited : Inhabited Category

Equations

• Cvc.Option.Category.instInhabited = { default := Cvc.Option.Category.ofNat 0 }

@[instance_reducible]

instance Cvc.Option.instBEqCategory : BEq Category

Equations

• Cvc.Option.instBEqCategory = { beq := Cvc.Option.instBEqCategory.beq }

@[instance_reducible]

instance Cvc.Option.Category.instLT : LT Category

Equations

• Cvc.Option.Category.instLT = { lt := fun (x1 x2 : Cvc.Option.Category) => x1.blt x2 = true }

@[reducible, inline]

abbrev Cvc.Option.Category.ble : Category → Category → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

inductive Cvc.InputLanguage : Type

An input language cvc5 can parse.

• smtLib_2_6 : InputLanguage

  The SMT-LIB version 2.6 language.

• sygus_2_1 : InputLanguage

  The SyGuS version 2.1 language.

• unknown : InputLanguage

  No language given.

@[instance_reducible]

instance Cvc.instHashableInputLanguage : Hashable InputLanguage

Equations

• Cvc.instHashableInputLanguage = { hash := Cvc.instHashableInputLanguage.hash }

@[instance_reducible]

instance Cvc.instBEqInputLanguage : BEq InputLanguage

Equations

• Cvc.instBEqInputLanguage = { beq := Cvc.instBEqInputLanguage.beq }

def Cvc.instOrdInputLanguage.ord : InputLanguage → InputLanguage → Ordering

Equations

• Cvc.instOrdInputLanguage.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Cvc.InputLanguage.instLE : LE InputLanguage

Equations

• Cvc.InputLanguage.instLE = { le := fun (x1 x2 : Cvc.InputLanguage) => x1.ble x2 = true }

@[instance_reducible]

instance Cvc.InputLanguage.instDecidableLE : DecidableLE InputLanguage

Equations

• val1✝.instDecidableLE val2✝ = if h : val1✝.ble val2✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.InputLanguage.instToString : ToString InputLanguage

Equations

• Cvc.InputLanguage.instToString = { toString := fun (x : Cvc.InputLanguage) => toString (repr x) }

@[instance_reducible]

instance Cvc.instOrdInputLanguage : Ord InputLanguage

Equations

• Cvc.instOrdInputLanguage = { compare := Cvc.instOrdInputLanguage.ord }

@[instance_reducible]

instance Cvc.InputLanguage.instInhabited : Inhabited InputLanguage

Equations

• Cvc.InputLanguage.instInhabited = { default := Cvc.InputLanguage.ofNat 0 }

def Cvc.instBEqInputLanguage.beq : InputLanguage → InputLanguage → Bool

Equations

• Cvc.instBEqInputLanguage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[reducible, inline]

abbrev Cvc.InputLanguage.ble : InputLanguage → InputLanguage → Bool

Equations

• val1✝.ble val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => true | Ordering.gt => false

@[instance_reducible]

instance Cvc.instReprInputLanguage : Repr InputLanguage

Equations

• Cvc.instReprInputLanguage = { reprPrec := Cvc.instReprInputLanguage.repr }

def Cvc.instHashableInputLanguage.hash : InputLanguage → UInt64

Equations

• Cvc.instHashableInputLanguage.hash Cvc.InputLanguage.smtLib_2_6 = 0
• Cvc.instHashableInputLanguage.hash Cvc.InputLanguage.sygus_2_1 = 1
• Cvc.instHashableInputLanguage.hash Cvc.InputLanguage.unknown = 2

@[reducible, inline]

abbrev Cvc.InputLanguage.blt : InputLanguage → InputLanguage → Bool

Equations

• val1✝.blt val2✝ = match compare val1✝ val2✝ with | Ordering.lt => true | Ordering.eq => false | Ordering.gt => false

@[instance_reducible]

instance Cvc.instDecidableEqInputLanguage : DecidableEq InputLanguage

Equations

• Cvc.instDecidableEqInputLanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.InputLanguage.instLT : LT InputLanguage

Equations

• Cvc.InputLanguage.instLT = { lt := fun (x1 x2 : Cvc.InputLanguage) => x1.blt x2 = true }

@[instance_reducible]

instance Cvc.InputLanguage.instDecidableLT : DecidableLT InputLanguage

Equations

• val1✝.instDecidableLT val2✝ = if h : val1✝.blt val2✝ = true then isTrue h else isFalse h

def Cvc.instReprInputLanguage.repr : InputLanguage → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.instReprInputLanguage.repr Cvc.InputLanguage.sygus_2_1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.InputLanguage.sygus_2_1")).group prec✝
• Cvc.instReprInputLanguage.repr Cvc.InputLanguage.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.InputLanguage.unknown")).group prec✝