Nullable constructors, sort-erased

cvc5's Nullable is the Option sort: a value is either nullable.null or nullable.some v. Unlike a declared datatype, Srt.nullable gives the same sort every time for the same element sort.

It is a datatype underneath, so a nullable value is an APPLY_CONSTRUCTOR term.

Constructors

def Cvc.Untyped.Term.mkNull [Ω] (elm : Srt) : Env Term

The null value of the nullable sort over the element sort elm.

Equations

• Cvc.Untyped.Term.mkNull elm = do let srt ← elm.nullable Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableNull srt

def Cvc.Untyped.Term.nullableSome [Ω] (elem : Term) : Env Term

The nullable value holding elem, nullable.some elem.

Equations

• elem.nullableSome = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableSome elem

def Cvc.Untyped.Term.nullableVal [Ω] (nullable : Term) : Env Term

The element the nullable term nullable holds, nullable.val.

Equations

• nullable.nullableVal = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableVal nullable

def Cvc.Untyped.Term.nullableIsNull [Ω] (nullable : Term) : Env Term

Whether the nullable term nullable is null, nullable.is_null.

Equations

• nullable.nullableIsNull = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableIsNull nullable

def Cvc.Untyped.Term.nullableIsSome [Ω] (nullable : Term) : Env Term

Whether the nullable term nullable holds an element, nullable.is_some.

Equations

• nullable.nullableIsSome = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableIsSome nullable

Values

A nullable value is the constructor applied to nothing or to one element, so it is read off the term's kind and children. Unlike a set or a sequence, this works on a built term as well as on a model's answer.

def Cvc.Untyped.Term.getNullableElem? [Ω] (term : Term) : Env (Option Term)

The element a nullable term denotes, or none if it denotes the null value.

Fails unless the term is built by a nullable constructor (see isNullableValue): a declared constant of nullable sort, for instance, is not.

Equations

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

def Cvc.Untyped.Term.isNullableValue [Ω] (term : Term) : Env Bool

Whether a term is built by a nullable constructor, nullable.null or nullable.some.

That is what getNullableElem? needs. Being nullable-sorted is not enough: a declared constant of nullable sort is built by neither.

Equations

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

def Cvc.Untyped.Term.mkNullableValue {α : Type} [Ω] [ToTyp α] [ValueToTerm α] (value : Option α) : Env Term

The nullable term denoting an optional value.

Equations

• Cvc.Untyped.Term.mkNullableValue none = Cvc.Srt.of α >>= Cvc.Untyped.Term.mkNull
• Cvc.Untyped.Term.mkNullableValue (some elem) = Cvc.Untyped.Term.mkValue elem >>= Cvc.Untyped.Term.nullableSome

def Cvc.Untyped.Term.getNullableValue {α : Type} [Ω] [TermToValue α] (term : Term) : Env (Option α)

The optional value a nullable term denotes.

Equations

• term.getNullableValue = do let __do_lift ← term.getNullableElem? match __do_lift with | none => pure none | some elem => some <$> elem.extractValue

@[instance_reducible]

instance Cvc.Untyped.Term.instValueToTermOption {α : Type} [ToTyp α] [ValueToTerm α] : ValueToTerm (Option α)

Equations

• Cvc.Untyped.Term.instValueToTermOption = { valueToTerm := fun [Cvc.Ω] => Cvc.Untyped.Term.mkNullableValue }

@[instance_reducible]

instance Cvc.Untyped.Term.instTermToValueOption {α : Type} [TermToValue α] : TermToValue (Option α)

Equations

• Cvc.Untyped.Term.instTermToValueOption = { termToValue := fun [Cvc.Ω] => Cvc.Untyped.Term.getNullableValue }