1.1. Terms🔗

Cvc.Term α represents a cvc5 term of some type α. In practice, most cvc.lean features expect α to have a IsSrt α instance, which guarantees that α corresponds to some SMT sort (Srt).

structure

Cvc.Term (α : Type) : Type
Cvc.Term (α : Type) : Type

Type-safe cvc5 terms, input type expected to be IsSrt for most uses.

No direct constructor exposed publicly, users must go through the Term.Build monadic constructors.

Fields

hasSymbols : Bool

True if the term mentions symbols.

toUnsafe : cvc5.Term

Underlying unsafe term.

For this introduction, we will mostly use Term Int and Term Bool for the sake of simplicity. Note that these term variants are often mentioned through aliases:

def

Cvc.Formula : Type
Cvc.Formula : Type

Abbreviation for a Term Bool.

def

Cvc.Term.Int : Type
Cvc.Term.Int : Type

Integer terms: Term Int.

def

Cvc.Term.Bool : Type
Cvc.Term.Bool : Type

Boolean terms: Term Bool.

Since cvc.lean are actually C++-level cvc5 terms, almost all term management relies on FFI with the C++ cvc5 API. Term management relies on the Term.Build error/state monad, For the monad transformer version, see Term.BuildT. for instance for term creation.

Here are a few term-creation functions, note that they are all in the Term namespace but produce results in the Term.Build monad.

def

Cvc.Term.int (i : Int) : Term.Build Term.Int
Cvc.Term.int (i : Int) :
  Term.Build Term.Int

Builds a constant integer term.

def

Cvc.Term.bool (b : Bool) : Term.Build Term.Bool
Cvc.Term.bool (b : Bool) :
  Term.Build Term.Bool

Builds a constant Boolean term.

def

Cvc.Term.equal {α : Type} (lft rgt : Term α) : Term.Build Formula
Cvc.Term.equal {α : Type}
  (lft rgt : Term α) : Term.Build Formula

Builds an equality term.

def

Cvc.Term.and (lft rgt : Term Bool) : Term.Build Formula
Cvc.Term.and (lft rgt : Term Bool) :
  Term.Build Formula

Builds a conjunction term.

def

Cvc.Term.ite {α : Type} [IsSrt α] (cnd : Term.Bool) (thn els : Term α) :
  Term.Build (Term α)
Cvc.Term.ite {α : Type} [IsSrt α]
  (cnd : Term.Bool) (thn els : Term α) :
  Term.Build (Term α)

Builds an if-then-else term.

Let's see this in action.

ite: (ite (and true (= 7 5)) 21 12)
#eval Cvc.Term.Build.runIO do
  let seven ← Term.int 7
  let five ← Term.int 5
  let cnd ← (← Term.bool true).and (← seven.equal five)
  let ite ← cnd.ite (← Term.int 21) (← Term.int 12)
  println! "ite: {ite}"

ite: (ite (and true (= 7 5)) 21 12)

That's not great, we can see that for complex terms the syntax will become painful very fast. Cvc.lean provides an smt! syntax extension so that we can write Terms like we would lean propositions.

open Cvc.Term.Dsl in
ite: (ite (and true (= 7 5)) 21 12)
#eval Cvc.Term.Build.runIO do
  let seven ← smt! 7
  let five ← smt! 5
  let cnd ← smt! true ∧ seven = five
  let ite ← smt! if cnd then 21 else 12
  println! "ite: {ite}"

ite: (ite (and true (= 7 5)) 21 12)

Writing the final term as just one line is way more readable:

open Cvc.Term.Dsl in
ite: (ite (and true (= 7 5)) 21 12)
#eval Cvc.Term.Build.runIO do
  let ite ← smt! if true ∧ 7 = 5 then 21 else 12
  println! "ite: {ite}"

ite: (ite (and true (= 7 5)) 21 12)