kdrag.datatype
Convenience features for datatypes.
You should use these instead of raw smt.Datatype. This also maintains a record of existing datatypes so that you don’t clobber old ones, a possible source of unsoundness.
Datatypes support accessor notation l.is_cons, l.hd, l.tl etc.
x._replace() syntax on single constructor datatypes
>>> import kdrag.theories.nat as nat
>>> n = smt.Const("n", nat.Nat)
>>> n.is_Z
is(Z, n)
>>> n.pred
pred(n)
>>> kd.prove(nat.one.pred == nat.Z)
|= pred(S(Z)) == Z
Module Attributes
A registry for overloadable call on datatypes |
|
SortDispatch for the relation associated with a Datatype of evidence |
Functions
|
Shorthand for simple enumeration datatypes. |
|
Define an inductive type of evidence and a relation the recurses on that evidence |
|
Minimal wrapper around a sort for sort based overloading |
|
Define a record datatype. |
|
Accessor lemmas for a datatype. |
|
|
|
|
|
Enable "call" syntax for constructors of smt datatypes |
|
Enable iteration over constructors of a datatype sort |
|
Enable len() on datatype sorts. |
|
Pattern matching for datatypes. |
|
Like NamedTuple, you can replace fields of a record datatype. |
|
Define a function by pattern matching equations. |
|
Constructors are distinct lemmas. |
|
Injectivity lemmas for a datatype. |
|
|
|
A Symbolic execution of sorts of pattern matching. |
- kdrag.datatype.Enum(name: str, args: str | list[str]) DatatypeSortRef
Shorthand for simple enumeration datatypes. Similar to python’s Enum. >>> Color = Enum(“Color”, “Red Green Blue”) >>> smt.And(Color.Red != Color.Green, Color.Red != Color.Blue) And(Red != Green, Red != Blue)
- Parameters:
name (str)
args (str | list[str])
- Return type:
DatatypeSortRef
- kdrag.datatype.InductiveRel(name: str, *params: ExprRef) Datatype
Define an inductive type of evidence and a relation the recurses on that evidence
>>> x = smt.Int("x") >>> Even = InductiveRel("Even", x) >>> Even.declare("Ev_Z", pred = x == 0) >>> Even.declare("Ev_SS", ("sub2_evidence", Even), pred = lambda evid: evid.rel(x-2)) >>> Even = Even.create() >>> smt.Const("ev", Even).rel(4) even(ev, 4)
- Parameters:
name (str)
params (ExprRef)
- Return type:
Datatype
- kdrag.datatype.NewType(name: str, sort: SortRef, pred=None) DatatypeSortRef
Minimal wrapper around a sort for sort based overloading
>>> NatI = NewType("NatI", smt.IntSort(), pred = lambda x: x.val >= 0) >>> x = smt.Const("x", NatI) >>> kd.QForAll([x], x.val >= -7) ForAll(x, Implies(val(x) >= 0, val(x) >= -7))
- Parameters:
name (str)
sort (SortRef)
- Return type:
DatatypeSortRef
- kdrag.datatype.Struct(name: str, *fields: tuple[str, SortRef], pred=None) DatatypeSortRef
Define a record datatype. This is the analog in many respects of python’s NamedTuple. The optional argument pred will add a well-formedness condition to the record giving something akin to a refinement type.
>>> Point = Struct("Point", ("x", smt.RealSort()), ("y", smt.RealSort())) >>> Point(1,2) Point(ToReal(1), ToReal(2)) >>> Point(1,2).x x(Point(ToReal(1), ToReal(2))) >>> PosPoint = Struct("PosPoint", ("x", smt.RealSort()), ("y", smt.RealSort()), pred = lambda p: smt.And(p.x > 0, p.y > 0)) >>> p = smt.Const("p", PosPoint) >>> kd.QForAll([p], p.x > -42) ForAll(p, Implies(And(x(p) > 0, y(p) > 0), x(p) > -42))
- Parameters:
name (str)
fields (tuple[str, SortRef])
- Return type:
DatatypeSortRef
- kdrag.datatype.accessor_lemmas(dt: DatatypeSortRef) list[Proof]
Accessor lemmas for a datatype.
>>> import kdrag.theories.nat as nat >>> accessor_lemmas(nat.Nat)[0] |= ForAll(x!..., pred(S(x!...)) == x!...)
- Parameters:
dt (DatatypeSortRef)
- Return type:
list[Proof]
- kdrag.datatype.accessor_num(s: DatatypeSortRef, constr_num: int, k: str) int
- Parameters:
s (DatatypeSortRef)
constr_num (int)
k (str)
- Return type:
int
- kdrag.datatype.call_dict: dict[SortRef, Callable] = {}
A registry for overloadable call on datatypes
- kdrag.datatype.constructor_num(s: DatatypeSortRef, k: str) int
- Parameters:
s (DatatypeSortRef)
k (str)
- Return type:
int
- kdrag.datatype.datatype_call(self: DatatypeSortRef, *args: ExprRef, **kwargs) DatatypeRef
Enable “call” syntax for constructors of smt datatypes
>>> Point = kd.Struct("Point", ("x", smt.IntSort()), ("y", smt.IntSort())) >>> Point(1,2) Point(1, 2) >>> Point(y=2, x=1) Point(1, 2)
- Parameters:
self (DatatypeSortRef)
args (ExprRef)
- Return type:
DatatypeRef
- kdrag.datatype.datatype_iter(self: DatatypeSortRef) Iterator[DatatypeRef]
Enable iteration over constructors of a datatype sort
- Parameters:
self (DatatypeSortRef)
- Return type:
Iterator[DatatypeRef]
- kdrag.datatype.datatype_len(self: DatatypeSortRef) int
Enable len() on datatype sorts. Returns the number of constructors
- Parameters:
self (DatatypeSortRef)
- Return type:
int
- kdrag.datatype.datatype_match_(x, *cases, default=None)
Pattern matching for datatypes.
>>> import kdrag.theories.nat as nat >>> x = smt.Const("x", nat.Nat) >>> x.match_((nat.S(x), nat.S(x)), (nat.one, nat.one), default=x) If(is(S, x), S(pred(x)), If(And(is(S, x), is(Z, pred(x))), S(Z), x))
>>> import kdrag.theories.list as list_ >>> IntList = list_.List(smt.IntSort()) >>> l = smt.Const("l", IntList) >>> x,y,z = smt.Ints("x y z") >>> l.match_((IntList.Nil, 0), (IntList.Cons(x, l), 1 + x)) If(is(Nil, l), 0, If(is(Cons, l), 1 + head(l), unreachable!...))
- kdrag.datatype.datatype_replace(self: DatatypeRef, **kwargs: ExprRef) DatatypeRef
Like NamedTuple, you can replace fields of a record datatype.
>>> Point = kd.Struct("Point", ("x", smt.RealSort()), ("y", smt.RealSort())) >>> Point(0,1)._replace(x=3, y=10) Point(3, 10) >>> p = smt.Const("p", Point) >>> q = p._replace(y=10) >>> q Point(x(p), 10) >>> q._replace(x=1) Point(1, 10)
- Parameters:
self (DatatypeRef)
kwargs (ExprRef)
- Return type:
DatatypeRef
- kdrag.datatype.define_fun(eqs)
Define a function by pattern matching equations.
>>> import kdrag.theories.nat as nat >>> n, m = smt.Consts("n m", nat.Nat) >>> myadd = smt.Function("myadd", nat.Nat, nat.Nat, nat.Nat) >>> myadd = define_fun([myadd(nat.Z, m) == m, myadd(nat.S(n), m) == nat.S(myadd(n, m))]) >>> myadd.case0 |= ForAll(m, myadd(Z, m) == m) >>> myadd.case1 |= ForAll([n, m], myadd(S(n), m) == S(myadd(n, m)))
- kdrag.datatype.distinct_lemmas(dt: DatatypeSortRef) list[Proof]
Constructors are distinct lemmas.
>>> import kdrag.theories.nat as nat >>> distinct_lemmas(nat.Nat)[0] |= ForAll(x!..., S(x!...) != Z)
- Parameters:
dt (DatatypeSortRef)
- Return type:
list[Proof]
- kdrag.datatype.inj_lemmas(dt: DatatypeSortRef) list[Proof]
Injectivity lemmas for a datatype. Z3 internally understands these, but can be useful to be explicit about them in some situations
>>> import kdrag.theories.nat as nat >>> inj_lemmas(nat.Nat)[0] |= ForAll([x!..., y!...], (S(x!...) == S(y!...)) == And(x!... == y!...))
- Parameters:
dt (DatatypeSortRef)
- Return type:
list[Proof]
- kdrag.datatype.multipattern_match(*cases: tuple[DatatypeRef, DatatypeRef]) tuple[list[BoolRef], dict[DatatypeRef, DatatypeRef]]
- Parameters:
cases (tuple[DatatypeRef, DatatypeRef])
- Return type:
tuple[list[BoolRef], dict[DatatypeRef, DatatypeRef]]
- kdrag.datatype.pattern_match(x: DatatypeRef, pat: DatatypeRef) tuple[list[BoolRef], dict[DatatypeRef, DatatypeRef]]
A Symbolic execution of sorts of pattern matching. Returns the constraints and substitutions for variables
>>> import kdrag.theories.nat as nat >>> n,m = smt.Consts("n m", nat.Nat) >>> pattern_match(n, nat.S(nat.S(m))) ([is(S, n), is(S, pred(n))], {m: pred(pred(n))})
- Parameters:
x (DatatypeRef)
pat (DatatypeRef)
- Return type:
tuple[list[BoolRef], dict[DatatypeRef, DatatypeRef]]
- kdrag.datatype.recognizer_lemmas(dt: DatatypeSortRef) list[Proof]
>>> import kdrag.theories.nat as nat >>> recognizer_lemmas(nat.Nat)[0] |= is(Z, Z) == True
- Parameters:
dt (DatatypeSortRef)
- Return type:
list[Proof]
- kdrag.datatype.rel = <kdrag.notation.SortDispatch object>
SortDispatch for the relation associated with a Datatype of evidence