kdrag.notation

SortDispatch system for z3 sort based dispatch akin to functools.singledispatch.

The SortDispatch system enables z3 sort based dispatch akin to ` functools.singledispatch`. This is the mechanism for operator overloading in knuckledragger.

A special overloadable operation is the “well-formed” predicate wf. Using the QForAll and QExists quantifiers will automatically insert wf calls for the appropriate sorts. In this way, we can achieve an effect similar to refinement types.

Importing this module will add some syntactic sugar to smt.

Expr overload by single dispatch
Bool supports &, |, ~
Sorts supports >> for ArraySort

Module Attributes

`add`	Sort based dispatch for + syntax
`radd`	Sort based dispatch for + syntax
`sub`	Sort based dispatch for - syntax
`mul`	Sort based dispatch for * syntax
`rmul`	Sort based dispatch for * syntax
`matmul`	Sort based dispatch for @ syntax
`neg`	Sort based dispatch for - syntax
`div`	Sort based dispatch for / syntax
`and_`	Sort based dispatch for & syntax
`or_`	Sort based dispatch for \| syntax
`invert`	Sort based dispatch for ~ syntax
`lt`	Sort based dispatch for < syntax
`le`	Sort based dispatch for <= syntax
`ge`	Sort based dispatch for >= syntax
`gt`	Sort based dispatch for > syntax
`eq`	Sort based dispatch for == syntax
`ne`	Sort based dispatch for != syntax
`wf`	wf is a special predicate for well-formedness.
`induct`	Sort based dispatch for induction principles.
`getitem`	Sort based dispatch for [] getitem syntax
`to_int`	Sort based dispatch for to_int
`to_real`	Sort based dispatch for to_real

Functions

`ExistsUnique`(v, *concs)	Unique Existence
`QExists`(vs, *concs)	Quantified Exists
`QForAll`(vs, *hyp_conc)	Quantified ForAll
`QLambda`(xs, *args)	Conditional Lambda.
`cond`(*cases[, default])	Helper for chained ifs defined by cases.
`conde`(*cases)	Minikanren style helper to create an Or of `And`s
`quantifier_call`(self, *args)	Instantiate a quantifier.

Classes

`Cond`()	Imperative class based API to build a chain of if-else statements
`SortDispatch`([name, default])	Sort dispatch is modeled after functools.singledispatch It allows for dispatching on the sort of the first argument

class kdrag.notation.Cond

Bases: object

Imperative class based API to build a chain of if-else statements

expr() → ExprRef

Return type:: ExprRef

otherwise(els: ExprRef)

Parameters:: els (ExprRef)

then(thn: ExprRef)

Parameters:: thn (ExprRef)

when(cond: BoolRef)

Parameters:: cond (BoolRef)

kdrag.notation.ExistsUnique(v: ExprRef, *concs) → BoolRef

Unique Existence

Parameters:: v (ExprRef)
Return type:: BoolRef

kdrag.notation.QExists(vs: list[ExprRef], *concs) → BoolRef

Quantified Exists

Shorthand for ForAll(vars, And(conc[0], conc[1], …))

If variables have a property wf attached, this is anded into the properties.

Parameters:: vs (list[ExprRef])
Return type:: BoolRef

kdrag.notation.QForAll(vs: list[ExprRef], *hyp_conc) → BoolRef

Quantified ForAll

Shorthand for ForAll(vars, Implies(And(hyp[0], hyp[1], …), conc))

If variables have a property wf attached, this is added as a hypothesis.

There is no downside to always using this compared to smt.ForAll and it can avoid some errors.

>>> x,y = smt.Ints("x y")
>>> QForAll([x,y], x > 0, y > 0, x + y > 0)
ForAll([x, y], Implies(And(x > 0, y > 0), x + y > 0))

Parameters:: vs (list[ExprRef])
Return type:: BoolRef

kdrag.notation.QLambda(xs: list[ExprRef], *args)

Conditional Lambda. If conjunction of conditions are not met, returns unconstrained value.

>>> x = smt.Int("x")
>>> QLambda([x], x > 0, x + 1)
Lambda(x, If(x > 0, x + 1, f!...(x)))
>>> QLambda([x], x > 0, x < 10, x + 1)
Lambda(x, If(And(x > 0, x < 10), x + 1, f!...(x)))

Parameters:: xs (list[ExprRef])

class kdrag.notation.SortDispatch(name=None, default=None)

Bases: object

Sort dispatch is modeled after functools.singledispatch It allows for dispatching on the sort of the first argument

>>> my_func = SortDispatch(name="my_func")
>>> my_func.register(smt.IntSort(), lambda x: x + 1)
>>> my_func.register(smt.BoolSort(), lambda x: smt.Not(x))
>>> my_func(smt.IntVal(3))
3 + 1
>>> my_func(smt.BoolVal(True))
Not(True)

define(args, body): Shorthand to define a new function for this dispatch. Calls kdrag.define.

register(sort, func)

kdrag.notation.add = <kdrag.notation.SortDispatch object>: Sort based dispatch for + syntax

kdrag.notation.and_ = <kdrag.notation.SortDispatch object>: Sort based dispatch for & syntax

kdrag.notation.cond(*cases, default=None) → ExprRef

Helper for chained ifs defined by cases. Each case is a tuple of a bool condition and a term. If default is not given, a check is performed for totality.

>>> x = smt.Int("x")
>>> kd.cond((x < 0, 2 * x), (x == 0, 3 * x), (x > 0, 5 * x))
If(x < 0,
   2*x,
   If(x == 0, 3*x, If(x > 0, 5*x, unreachable...)))
>>> kd.cond((x < 0, 2 * x), (x == 0, 3 * x), default = 5 * x)
If(x < 0, 2*x, If(x == 0, 3*x, 5*x))

Return type:: ExprRef

kdrag.notation.conde(*cases)

Minikanren style helper to create an Or of `And`s

>>> x,y = smt.Ints("x y")
>>> conde((x > 0, y == x + 1), (x < 0, y == x - 1))
Or(And(x > 0, y == x + 1), And(x < 0, y == x - 1))

kdrag.notation.div = <kdrag.notation.SortDispatch object>: Sort based dispatch for / syntax

kdrag.notation.eq = <kdrag.notation.SortDispatch object>: Sort based dispatch for == syntax

kdrag.notation.ge = <kdrag.notation.SortDispatch object>: Sort based dispatch for >= syntax

kdrag.notation.getitem = <kdrag.notation.SortDispatch object>: Sort based dispatch for [] getitem syntax

kdrag.notation.gt = <kdrag.notation.SortDispatch object>: Sort based dispatch for > syntax

kdrag.notation.induct = <kdrag.notation.SortDispatch object>: Sort based dispatch for induction principles. Should instantiate an induction scheme for variable x and predicate P

kdrag.notation.invert = <kdrag.notation.SortDispatch object>: Sort based dispatch for ~ syntax

kdrag.notation.le = <kdrag.notation.SortDispatch object>: Sort based dispatch for <= syntax

kdrag.notation.lt = <kdrag.notation.SortDispatch object>: Sort based dispatch for < syntax

kdrag.notation.matmul = <kdrag.notation.SortDispatch object>: Sort based dispatch for @ syntax

kdrag.notation.mul = <kdrag.notation.SortDispatch object>: Sort based dispatch for * syntax

kdrag.notation.ne = <kdrag.notation.SortDispatch object>: Sort based dispatch for != syntax

kdrag.notation.neg = <kdrag.notation.SortDispatch object>: Sort based dispatch for - syntax

kdrag.notation.or_ = <kdrag.notation.SortDispatch object>: Sort based dispatch for | syntax

kdrag.notation.quantifier_call(self, *args)

Instantiate a quantifier. This does substitution >>> x,y = smt.Ints(“x y”) >>> smt.Lambda([x,y], x + 1)(2,3) 2 + 1

To apply a Lambda without substituting, use square brackets >>> smt.Lambda([x,y], x + 1)[2,3] Select(Lambda([x, y], x + 1), 2, 3)

kdrag.notation.radd = <kdrag.notation.SortDispatch object>: Sort based dispatch for + syntax

kdrag.notation.rmul = <kdrag.notation.SortDispatch object>: Sort based dispatch for * syntax

kdrag.notation.sub = <kdrag.notation.SortDispatch object>: Sort based dispatch for - syntax

kdrag.notation.to_int = <kdrag.notation.SortDispatch object>: Sort based dispatch for to_int

kdrag.notation.to_real = <kdrag.notation.SortDispatch object>: Sort based dispatch for to_real

kdrag.notation.wf = <kdrag.notation.SortDispatch object>: wf is a special predicate for well-formedness. It is auto inserted by QForAll and QExists.