kdrag.theories.option

Algebraic data type for optional values

Functions

`None_`(T)	Helper to create Option None_ values >>> None_(smt.IntSort()) None_
`OptionSort`(T)	Define an Option type for a given type T >>> OInt = OptionSort(smt.IntSort()) >>> OInt.Some(1) Some(1) >>> OInt.None_ None_ >>> OInt.Some(1).val val(Some(1))
`Some`(x)	Helper to create Option values >>> Some(42) Some(42) >>> Some(42).sort() Option_Int
`get`(x, default)	Get the value of an Option, or a default value if it is None_ >>> get(Some(42), 0) If(is(Some, Some(42)), val(Some(42)), 0)
`is_option`(x)	Check if a value is an Option >>> is_option(Some(42)) True >>> is_option(42) False

kdrag.theories.option.None_(T: SortRef) → DatatypeRef

Helper to create Option None_ values >>> None_(smt.IntSort()) None_

Parameters:: T (SortRef)
Return type:: DatatypeRef

kdrag.theories.option.OptionSort(T: SortRef) → DatatypeSortRef

Define an Option type for a given type T >>> OInt = OptionSort(smt.IntSort()) >>> OInt.Some(1) Some(1) >>> OInt.None_ None_ >>> OInt.Some(1).val val(Some(1))

Parameters:: T (SortRef)
Return type:: DatatypeSortRef

kdrag.theories.option.Some(x: ExprRef) → DatatypeRef

Helper to create Option values >>> Some(42) Some(42) >>> Some(42).sort() Option_Int

Parameters:: x (ExprRef)
Return type:: DatatypeRef

kdrag.theories.option.get(x: DatatypeRef, default: ExprRef) → ExprRef

Get the value of an Option, or a default value if it is None_ >>> get(Some(42), 0) If(is(Some, Some(42)), val(Some(42)), 0)

Parameters:

x (DatatypeRef)
default (ExprRef)

Return type:

ExprRef

kdrag.theories.option.is_option(x: DatatypeRef) → bool

Check if a value is an Option >>> is_option(Some(42)) True >>> is_option(42) False

Parameters:: x (DatatypeRef)
Return type:: bool