Logic

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 true
• (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.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.

Based on [cvc5's logic_info.cpp][cpp].

[cpp] https://github.com/cvc5/cvc5/blob/7ee7051df025e6db566fc67086a7aa4e1023c8f2/src/theory/logic_info.cpp#L270-L367

• mkRaw :: (
• all? : Bool

  Trumps the rest of the specification and turns everything on.

  You should probably not use this, tailoring the logic to the terms you actually use allows the solver to use the best approach available and is crucial for performance.

• ho? : Bool

  Higher-order, for reasoning about functions that take functions as arguments.

• qf? : Bool

  Quantifier-free, terms cannot use quantifiers.

• sep? : Bool

  [Separation logic], typically to reason about program memory.

  Separation logic

• array? : Bool

  For reasoning about arrays.

• uf? : Bool

  Uninterpreted functions, terms can use symbols of a function-sort.

• card? : Bool

  Cardinality constraints, a.k.a pseudo-boolean constraints.

  A cardinality constraint, as a term, is an Int-arithmetic relation with Bool-sorted symbols. These symbols are coerced into Int as false ↦ 0, true ↦ 1. So, assuming a b : Bool we can write a + b ≥ 1 for a ∨ b, or a * b = 1 for a ∧ b.

• bitvec? : Bool

  Bit-vectors.

• ff? : Bool

  Finite fields theory.

• float? : Bool

  Floating point numbers.

• datatype? : Bool

  User-defined potentially-recursive datatypes.

• string? : Bool

  Theory of strings.

• arith? : Option Cvc.Logic.Arith

  Specification of the Int/Real arithmetic theory.

• )

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

SMT-LIB string representation.

Equations

• One or more equations did not get rendered due to their size.
• self.toSmtLib = "ALL"

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

Either Logic.all? or at least one actual fragment is active.

Equations

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

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

Either Logic.all? or at least one actual fragment is active.

Equations

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

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

Equations

• self.instDecidableValid = inferInstanceAs (Decidable (self.isValid = true))

structure Cvc.Logic.Builderextends Cvc.Logic : Type

• 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

Equations

• Cvc.Logic.Builder.mk = { }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Cvc.Logic.all : Logic

Equations

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

theorem Cvc.Logic.all_valid : all.valid

def Cvc.Logic.mk : Builder

Equations

• Cvc.Logic.mk = { }

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

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

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

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

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

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

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

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

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

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

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

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

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

Convenient Logic constructors for Arith

def Cvc.Logic.lia : Builder

Equations

• Cvc.Logic.lia = Cvc.Logic.mk.arith Cvc.Logic.Arith.lia

def Cvc.Logic.lra : Builder

Equations

• Cvc.Logic.lra = Cvc.Logic.mk.arith Cvc.Logic.Arith.lra

def Cvc.Logic.lira : Builder

Equations

• Cvc.Logic.lira = Cvc.Logic.mk.arith Cvc.Logic.Arith.lira

def Cvc.Logic.nia : Builder

Equations

• Cvc.Logic.nia = Cvc.Logic.mk.arith Cvc.Logic.Arith.nia

def Cvc.Logic.nra : Builder

Equations

• Cvc.Logic.nra = Cvc.Logic.mk.arith Cvc.Logic.Arith.nra

def Cvc.Logic.nira : Builder

Equations

• Cvc.Logic.nira = Cvc.Logic.mk.arith Cvc.Logic.Arith.nira

def Cvc.Logic.liat : Builder

Equations

• Cvc.Logic.liat = Cvc.Logic.mk.arith Cvc.Logic.Arith.liat

def Cvc.Logic.lrat : Builder

Equations

• Cvc.Logic.lrat = Cvc.Logic.mk.arith Cvc.Logic.Arith.lrat

def Cvc.Logic.lirat : Builder

Equations

• Cvc.Logic.lirat = Cvc.Logic.mk.arith Cvc.Logic.Arith.lirat

def Cvc.Logic.niat : Builder

Equations

• Cvc.Logic.niat = Cvc.Logic.mk.arith Cvc.Logic.Arith.niat

def Cvc.Logic.nrat : Builder

Equations

• Cvc.Logic.nrat = Cvc.Logic.mk.arith Cvc.Logic.Arith.nrat

def Cvc.Logic.nirat : Builder

Equations

• Cvc.Logic.nirat = Cvc.Logic.mk.arith Cvc.Logic.Arith.nirat

def Cvc.Logic.idl : Builder

Equations

• Cvc.Logic.idl = Cvc.Logic.mk.arith Cvc.Logic.Arith.idl

def Cvc.Logic.rdl : Builder

Equations

• Cvc.Logic.rdl = Cvc.Logic.mk.arith Cvc.Logic.Arith.rdl

def Cvc.Logic.irdl : Builder

Equations

• Cvc.Logic.irdl = Cvc.Logic.mk.arith Cvc.Logic.Arith.irdl

Ubiquitous logics

def Cvc.Logic.qf_lia : Builder

Equations

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

def Cvc.Logic.qf_lra : Builder

Equations

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

def Cvc.Logic.qf_lira : Builder

Equations

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

def Cvc.Logic.qf_nia : Builder

Equations

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

def Cvc.Logic.qf_nra : Builder

Equations

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

def Cvc.Logic.qf_nira : Builder

Equations

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