SMT-LIB logics

A Logic names the fragment a solver should expect, as Solver.setLogic takes it: QF_LIA, UFBV, ALL… Start from a named logic and extend it, or build one from nothing with Logic.mk:

s.setLogic Logic.qf_lia.uf                        -- QF_UFLIA
s.setLogic (Logic.mk.uf.arith .lia).toLogic.qf    -- QF_UFLIA

Logic.ofSmtLib parses a logic's name, and Logic.toSmtLib prints one.

Specification for the arithmetic (Int/Real) part of the logic

inductive Cvc.Logic.Arith.Kind : Type

Difference logic / linearity / transcendental numbers.

• diff : Kind

  Only permits difference logic (implies linear).

• nonDiff (linear transcendental : Bool) : Kind

  Arithmetic.

  • linear: only allows linear terms if true, allows non-linear terms if false.
  • transcendental: (dis)allows non-algebraic numbers (wikipedia).

def Cvc.Logic.Arith.Kind.simplest : Kind

Equations

• Cvc.Logic.Arith.Kind.simplest = Cvc.Logic.Arith.Kind.diff

def Cvc.Logic.Arith.Kind.setNonDiff : Kind → Kind

Equations

• Cvc.Logic.Arith.Kind.diff.setNonDiff = Cvc.Logic.Arith.Kind.nonDiff true false
• (Cvc.Logic.Arith.Kind.nonDiff linear transcendental).setNonDiff = Cvc.Logic.Arith.Kind.nonDiff linear transcendental

def Cvc.Logic.Arith.Kind.setNonLinear : Kind → Kind

Equations

• Cvc.Logic.Arith.Kind.diff.setNonLinear = Cvc.Logic.Arith.Kind.nonDiff false false
• (Cvc.Logic.Arith.Kind.nonDiff linear t).setNonLinear = Cvc.Logic.Arith.Kind.nonDiff false t

def Cvc.Logic.Arith.Kind.setTranscendental : Kind → Kind

Equations

• Cvc.Logic.Arith.Kind.diff.setTranscendental = Cvc.Logic.Arith.Kind.nonDiff true true
• (Cvc.Logic.Arith.Kind.nonDiff linear t).setTranscendental = Cvc.Logic.Arith.Kind.nonDiff linear true

inductive Cvc.Logic.Arith.IntReal : Type

Int, Real, or both.

• int : IntReal

  Only Ints.

• real : IntReal

  Only Reals.

• both : IntReal

  Ints and Reals.

def Cvc.Logic.Arith.IntReal.simplest : IntReal

Equations

• Cvc.Logic.Arith.IntReal.simplest = Cvc.Logic.Arith.IntReal.int

def Cvc.Logic.Arith.IntReal.toSmtLib : IntReal → String

Gives the I, R, or IR part of the logic, e.g. IR in LIRA.

Equations

• Cvc.Logic.Arith.IntReal.int.toSmtLib = "I"
• Cvc.Logic.Arith.IntReal.real.toSmtLib = "R"
• Cvc.Logic.Arith.IntReal.both.toSmtLib = "IR"

def Cvc.Logic.Arith.IntReal.ofSmtLib : String → Res IntReal

Equations

• Cvc.Logic.Arith.IntReal.ofSmtLib "I" = pure Cvc.Logic.Arith.IntReal.int
• Cvc.Logic.Arith.IntReal.ofSmtLib "R" = pure Cvc.Logic.Arith.IntReal.real
• Cvc.Logic.Arith.IntReal.ofSmtLib "IR" = pure Cvc.Logic.Arith.IntReal.both
• Cvc.Logic.Arith.IntReal.ofSmtLib x✝ = Cvc.throwUser (toString "illegal int/real bit `" ++ toString x✝ ++ toString "`, expected `I`, `R`, or `IR`")

def Cvc.Logic.Arith.IntReal.setInt : IntReal → IntReal

Equations

• Cvc.Logic.Arith.IntReal.real.setInt = Cvc.Logic.Arith.IntReal.both
• Cvc.Logic.Arith.IntReal.int.setInt = Cvc.Logic.Arith.IntReal.int
• Cvc.Logic.Arith.IntReal.both.setInt = Cvc.Logic.Arith.IntReal.both

def Cvc.Logic.Arith.IntReal.setReal : IntReal → IntReal

Equations

• Cvc.Logic.Arith.IntReal.int.setReal = Cvc.Logic.Arith.IntReal.both
• Cvc.Logic.Arith.IntReal.real.setReal = Cvc.Logic.Arith.IntReal.real
• Cvc.Logic.Arith.IntReal.both.setReal = Cvc.Logic.Arith.IntReal.both

structure Cvc.Logic.Arith : Type

Full arithmetic (Int/Real) specification.

• kind : Kind

  Difference logic / linearity / transcendental numbers.

• intReal : IntReal

  Int, Real, or both.

def Cvc.Logic.Arith.simplest : Arith

Equations

• Cvc.Logic.Arith.simplest = { kind := Cvc.Logic.Arith.Kind.simplest, intReal := Cvc.Logic.Arith.IntReal.simplest }

def Cvc.Logic.Arith.setNonDiff (self : Arith) : Arith

Equations

• self.setNonDiff = { kind := self.kind.setNonDiff, intReal := self.intReal }

def Cvc.Logic.Arith.setNonLinear (self : Arith) : Arith

Equations

• self.setNonLinear = { kind := self.kind.setNonLinear, intReal := self.intReal }

def Cvc.Logic.Arith.setTranscendental (self : Arith) : Arith

Equations

• self.setTranscendental = { kind := self.kind.setTranscendental, intReal := self.intReal }

def Cvc.Logic.Arith.setInt (self : Arith) : Arith

Equations

• self.setInt = { kind := self.kind, intReal := self.intReal.setInt }

def Cvc.Logic.Arith.setReal (self : Arith) : Arith

Equations

• self.setReal = { kind := self.kind, intReal := self.intReal.setReal }

def Cvc.Logic.Arith.toSmtLib (self : Arith) : String

Generates the arithmetic part of an SMT-LIB logic, e.g. NIRA.

Equations

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

def Cvc.Logic.Arith.lia : Arith

LIA.

Equations

• Cvc.Logic.Arith.lia = { kind := Cvc.Logic.Arith.Kind.nonDiff true false, intReal := Cvc.Logic.Arith.IntReal.int }

def Cvc.Logic.Arith.lra : Arith

LRA.

Equations

• Cvc.Logic.Arith.lra = { kind := Cvc.Logic.Arith.Kind.nonDiff true false, intReal := Cvc.Logic.Arith.IntReal.real }

def Cvc.Logic.Arith.lira : Arith

LIRA.

Equations

• Cvc.Logic.Arith.lira = { kind := Cvc.Logic.Arith.Kind.nonDiff true false, intReal := Cvc.Logic.Arith.IntReal.both }

def Cvc.Logic.Arith.nia : Arith

NIA.

Equations

• Cvc.Logic.Arith.nia = { kind := Cvc.Logic.Arith.Kind.nonDiff false false, intReal := Cvc.Logic.Arith.IntReal.int }

def Cvc.Logic.Arith.nra : Arith

NRA.

Equations

• Cvc.Logic.Arith.nra = { kind := Cvc.Logic.Arith.Kind.nonDiff false false, intReal := Cvc.Logic.Arith.IntReal.real }

def Cvc.Logic.Arith.nira : Arith

NIRA.

Equations

• Cvc.Logic.Arith.nira = { kind := Cvc.Logic.Arith.Kind.nonDiff false false, intReal := Cvc.Logic.Arith.IntReal.both }

def Cvc.Logic.Arith.liat : Arith

LIAT.

Equations

• Cvc.Logic.Arith.liat = { kind := Cvc.Logic.Arith.Kind.nonDiff true true, intReal := Cvc.Logic.Arith.IntReal.int }

def Cvc.Logic.Arith.lrat : Arith

LRAT.

Equations

• Cvc.Logic.Arith.lrat = { kind := Cvc.Logic.Arith.Kind.nonDiff true true, intReal := Cvc.Logic.Arith.IntReal.real }

def Cvc.Logic.Arith.lirat : Arith

LIRAT.

Equations

• Cvc.Logic.Arith.lirat = { kind := Cvc.Logic.Arith.Kind.nonDiff true true, intReal := Cvc.Logic.Arith.IntReal.both }

def Cvc.Logic.Arith.niat : Arith

NIAT.

Equations

• Cvc.Logic.Arith.niat = { kind := Cvc.Logic.Arith.Kind.nonDiff false true, intReal := Cvc.Logic.Arith.IntReal.int }

def Cvc.Logic.Arith.nrat : Arith

NRAT.

Equations

• Cvc.Logic.Arith.nrat = { kind := Cvc.Logic.Arith.Kind.nonDiff false true, intReal := Cvc.Logic.Arith.IntReal.real }

def Cvc.Logic.Arith.nirat : Arith

NIRAT.

Equations

• Cvc.Logic.Arith.nirat = { kind := Cvc.Logic.Arith.Kind.nonDiff false true, intReal := Cvc.Logic.Arith.IntReal.both }

def Cvc.Logic.Arith.idl : Arith

IDL.

Equations

• Cvc.Logic.Arith.idl = { kind := Cvc.Logic.Arith.Kind.diff, intReal := Cvc.Logic.Arith.IntReal.int }

def Cvc.Logic.Arith.rdl : Arith

RDL.

Equations

• Cvc.Logic.Arith.rdl = { kind := Cvc.Logic.Arith.Kind.diff, intReal := Cvc.Logic.Arith.IntReal.real }

def Cvc.Logic.Arith.irdl : Arith

IRDL.

Equations

• Cvc.Logic.Arith.irdl = { kind := Cvc.Logic.Arith.Kind.diff, intReal := Cvc.Logic.Arith.IntReal.both }

structure Cvc.Logic : Type

An SMT-LIB logic, such as QF_LIA.

• mkRaw :: (
• all? : Bool
• ho? : Bool
• qf? : Bool
• sep? : Bool
• array? : Bool
• uf? : Bool
• card? : Bool
• bitVec? : Bool
• ff? : Bool
• float? : Bool
• datatype? : Bool
• string? : Bool
• arith? : Option Cvc.Logic.Arith
• )

def Cvc.Logic.isValid (self : Logic) : Bool

Whether the logic is ALL or enables at least one theory.

Equations

• self.isValid = decide (Cvc.Logic.all?✝ self = true ∨ Cvc.Logic.oneTrailing?✝ false self = true)

def Cvc.Logic.valid (self : Logic) : Prop

Whether the logic is ALL or enables at least one theory.

Equations

• self.valid = (self.isValid = true)

@[instance_reducible]

instance Cvc.Logic.instDecidableValid (self : Logic) : Decidable self.valid

Equations

• self.instDecidableValid = Cvc.Logic.instDecidableValid._aux_1 self

structure Cvc.Logic.Builderextends Cvc.Logic : Type

A logic built from nothing, started by Logic.mk and finished by toLogic.

• mk' :: (
• all? : Bool
• ho? : Bool
• qf? : Bool
• sep? : Bool
• array? : Bool
• uf? : Bool
• card? : Bool
• bitVec? : Bool
• ff? : Bool
• float? : Bool
• datatype? : Bool
• string? : Bool
• arith? : Option Cvc.Logic.Arith
• )

def Cvc.Logic.Builder.mk : Builder

The empty logic, to add theories to.

Equations

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

def Cvc.Logic.Builder.ho (self : Builder) : Builder

Adds higher-order reasoning, HO_.

Equations

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

def Cvc.Logic.Builder.qf (self : Builder) : Builder

Makes the logic quantifier-free, QF_.

Equations

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

def Cvc.Logic.Builder.sep (self : Builder) : Builder

Adds separation logic, SEP_.

Equations

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

def Cvc.Logic.Builder.array (self : Builder) : Builder

Adds arrays, A or AX.

Equations

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

def Cvc.Logic.Builder.uf (self : Builder) : Builder

Adds uninterpreted functions, UF.

Equations

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

def Cvc.Logic.Builder.card (self : Builder) : Builder

Adds cardinality constraints, C.

Equations

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

theorem Cvc.Logic.Builder.card_valid {b : Builder} : b.card.valid

def Cvc.Logic.Builder.bitVec (self : Builder) : Builder

Adds bit-vectors, BV.

Equations

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

theorem Cvc.Logic.Builder.bitVec_valid {b : Builder} : b.bitVec.valid

def Cvc.Logic.Builder.ff (self : Builder) : Builder

Adds finite fields, FF.

Equations

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

theorem Cvc.Logic.Builder.ff_valid {b : Builder} : b.ff.valid

def Cvc.Logic.Builder.float (self : Builder) : Builder

Adds floating-point arithmetic, FP.

Equations

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

theorem Cvc.Logic.Builder.float_valid {b : Builder} : b.float.valid

def Cvc.Logic.Builder.datatype (self : Builder) : Builder

Adds datatypes, DT.

Equations

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

theorem Cvc.Logic.Builder.datatype_valid {b : Builder} : b.datatype.valid

def Cvc.Logic.Builder.string (self : Builder) : Builder

Adds strings, S.

Equations

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

theorem Cvc.Logic.Builder.string_valid {b : Builder} : b.string.valid

def Cvc.Logic.Builder.arith (self : Builder) (arith : Arith) : Builder

Sets the arithmetic part, such as Arith.lia.

Equations

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

theorem Cvc.Logic.Builder.arith_valid {b : Builder} {a : Arith} : (b.arith a).valid

def Cvc.Logic.Builder.nonDiff (self : Builder) : Builder

Makes the arithmetic linear rather than difference logic.

Equations

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

def Cvc.Logic.Builder.nonLinear (self : Builder) : Builder

Makes the arithmetic non-linear.

Equations

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

def Cvc.Logic.Builder.transcendental (self : Builder) : Builder

Adds transcendental functions to the arithmetic.

Equations

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

def Cvc.Logic.Builder.int (self : Builder) : Builder

Adds integers to the arithmetic.

Equations

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

def Cvc.Logic.Builder.real (self : Builder) : Builder

Adds reals to the arithmetic.

Equations

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

def Cvc.Logic.all : Logic

ALL: every theory cvc5 supports.

Equations

• Cvc.Logic.all = { all? := true }

theorem Cvc.Logic.all_valid : all.valid

def Cvc.Logic.mk : Builder

Starts building a logic from nothing.

Equations

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

def Cvc.Logic.ho (self : Logic) : Logic

Adds higher-order reasoning, HO_.

Equations

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

theorem Cvc.Logic.ho_valid {l : Logic} : l.valid → l.ho.valid

def Cvc.Logic.qf (self : Logic) : Logic

Makes the logic quantifier-free, QF_.

Equations

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

theorem Cvc.Logic.qf_valid {l : Logic} : l.valid → l.qf.valid

def Cvc.Logic.sep (self : Logic) : Logic

Adds separation logic, SEP_.

Equations

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

theorem Cvc.Logic.sep_valid {l : Logic} : l.valid → l.sep.valid

def Cvc.Logic.array (self : Logic) : Logic

Adds arrays, A or AX.

Equations

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

theorem Cvc.Logic.array_valid {l : Logic} : l.valid → l.array.valid

def Cvc.Logic.uf (self : Logic) : Logic

Adds uninterpreted functions, UF.

Equations

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

theorem Cvc.Logic.uf_valid {l : Logic} : l.valid → l.uf.valid

def Cvc.Logic.card (self : Logic) : Logic

Adds cardinality constraints, C.

Equations

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

theorem Cvc.Logic.card_valid {l : Logic} : l.card.valid

def Cvc.Logic.bitVec (self : Logic) : Logic

Adds bit-vectors, BV.

Equations

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

theorem Cvc.Logic.bitVec_valid {l : Logic} : l.bitVec.valid

def Cvc.Logic.ff (self : Logic) : Logic

Adds finite fields, FF.

Equations

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

theorem Cvc.Logic.ff_valid {l : Logic} : l.ff.valid

def Cvc.Logic.float (self : Logic) : Logic

Adds floating-point arithmetic, FP.

Equations

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

theorem Cvc.Logic.float_valid {l : Logic} : l.float.valid

def Cvc.Logic.datatype (self : Logic) : Logic

Adds datatypes, DT.

Equations

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

theorem Cvc.Logic.datatype_valid {l : Logic} : l.datatype.valid

def Cvc.Logic.string (self : Logic) : Logic

Adds strings, S.

Equations

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

theorem Cvc.Logic.string_valid {l : Logic} : l.string.valid

def Cvc.Logic.arith (self : Logic) (arith : Arith) : Logic

Sets the arithmetic part, such as Arith.lia.

Equations

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

theorem Cvc.Logic.arith_valid {l : Logic} {a : Arith} : (l.arith a).valid

Pure arithmetic logics

Each is the logic of its name: Logic.lira is LIRA, Logic.qf_nia is QF_NIA.

def Cvc.Logic.lia : Logic

Equations

• Cvc.Logic.lia = (Cvc.Logic.mk.arith Cvc.Logic.Arith.lia).toLogic

def Cvc.Logic.lra : Logic

Equations

• Cvc.Logic.lra = (Cvc.Logic.mk.arith Cvc.Logic.Arith.lra).toLogic

def Cvc.Logic.lira : Logic

Equations

• Cvc.Logic.lira = (Cvc.Logic.mk.arith Cvc.Logic.Arith.lira).toLogic

def Cvc.Logic.nia : Logic

Equations

• Cvc.Logic.nia = (Cvc.Logic.mk.arith Cvc.Logic.Arith.nia).toLogic

def Cvc.Logic.nra : Logic

Equations

• Cvc.Logic.nra = (Cvc.Logic.mk.arith Cvc.Logic.Arith.nra).toLogic

def Cvc.Logic.nira : Logic

Equations

• Cvc.Logic.nira = (Cvc.Logic.mk.arith Cvc.Logic.Arith.nira).toLogic

def Cvc.Logic.liat : Logic

Equations

• Cvc.Logic.liat = (Cvc.Logic.mk.arith Cvc.Logic.Arith.liat).toLogic

def Cvc.Logic.lrat : Logic

Equations

• Cvc.Logic.lrat = (Cvc.Logic.mk.arith Cvc.Logic.Arith.lrat).toLogic

def Cvc.Logic.lirat : Logic

Equations

• Cvc.Logic.lirat = (Cvc.Logic.mk.arith Cvc.Logic.Arith.lirat).toLogic

def Cvc.Logic.niat : Logic

Equations

• Cvc.Logic.niat = (Cvc.Logic.mk.arith Cvc.Logic.Arith.niat).toLogic

def Cvc.Logic.nrat : Logic

Equations

• Cvc.Logic.nrat = (Cvc.Logic.mk.arith Cvc.Logic.Arith.nrat).toLogic

def Cvc.Logic.nirat : Logic

Equations

• Cvc.Logic.nirat = (Cvc.Logic.mk.arith Cvc.Logic.Arith.nirat).toLogic

def Cvc.Logic.idl : Logic

Equations

• Cvc.Logic.idl = (Cvc.Logic.mk.arith Cvc.Logic.Arith.idl).toLogic

def Cvc.Logic.rdl : Logic

Equations

• Cvc.Logic.rdl = (Cvc.Logic.mk.arith Cvc.Logic.Arith.rdl).toLogic

def Cvc.Logic.irdl : Logic

Equations

• Cvc.Logic.irdl = (Cvc.Logic.mk.arith Cvc.Logic.Arith.irdl).toLogic

def Cvc.Logic.qf_lia : Logic

Equations

• Cvc.Logic.qf_lia = Cvc.Logic.lia.qf

def Cvc.Logic.qf_lra : Logic

Equations

• Cvc.Logic.qf_lra = Cvc.Logic.lra.qf

def Cvc.Logic.qf_lira : Logic

Equations

• Cvc.Logic.qf_lira = Cvc.Logic.lira.qf

def Cvc.Logic.qf_nia : Logic

Equations

• Cvc.Logic.qf_nia = Cvc.Logic.nia.qf

def Cvc.Logic.qf_nra : Logic

Equations

• Cvc.Logic.qf_nra = Cvc.Logic.nra.qf

def Cvc.Logic.qf_nira : Logic

Equations

• Cvc.Logic.qf_nira = Cvc.Logic.nira.qf

Conversion from/to strings

def Cvc.Logic.toSmtLib : Logic → String

SMT-LIB string representation.

Equations

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

@[reducible, inline]

abbrev Cvc.Logic.toString : Logic → String

SMT-LIB string representation.

Equations

• Cvc.Logic.toString = Cvc.Logic.toSmtLib

@[instance_reducible]

instance Cvc.Logic.instToString : ToString Logic

Equations

• Cvc.Logic.instToString = { toString := Cvc.Logic.toString }

def Cvc.Logic.ofSmtLib (s : String) : Res Logic

Parses an SMT-LIB logic name, such as QF_UFLIA.

Equations

• Cvc.Logic.ofSmtLib s = Except.mapError Cvc.Error.user ((Cvc.Logic.parseSmtLib✝ true).run s)