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

`call`	Sort based dispatch for () call syntax
`getitem`	Sort based dispatch for [] getitem syntax
`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.
`measure`	`measure is an Int value associated with an ExprRef for use in defining well-founded recursion.
`choose`	Sort based dispatch for Hilbert choice operator.
`forall`	Sort based dispatch for ForAll quantifier.
`exists`	Sort based dispatch for Exists quantifier.
`induct`	Sort based dispatch for induction principles.
`to_int`	Sort based dispatch for to_int
`to_real`	Sort based dispatch for to_real

Functions

`ExistsUnique`(v, *concs)	Unique Existence
`GenericDispatch`(default_factory)	A decorator version of SortDispatch with a default factory.
`QExists`(vs, *concs0)	Quantified Exists
`QForAll`(vs, *hyp_conc)	Quantified ForAll
`QImplies`(*hyp_conc)	Quantified Implies
`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
`induct_default`(x, P)
`induct_int`(x, P)
`induct_seq`(a, P)
`quantifier_call`(self, *args)	Instantiate a quantifier.

Classes

`Cond`()	Imperative class based API to build a chain of if-else statements
`SortDispatch`([name, default, pointwise, ...])	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.GenericDispatch(default_factory) → SortDispatch

A decorator version of SortDispatch with a default factory. This is useful for definition Sort generic definitions.

>>> @GenericDispatch
... def id(sort):
...    x = smt.Const("x", sort)
...    return kd.define("id", [x], x)
>>> id(smt.IntVal(3))
id(3)

Return type:: SortDispatch

kdrag.notation.QExists(vs: list[ExprRef], *concs0) → 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.QImplies(*hyp_conc) → BoolRef

Quantified Implies

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

>>> x,y = smt.Ints("x y")
>>> QImplies(x > 0, y > 0, x + y > 0)
Implies(And(x > 0, y > 0), x + y > 0)

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, pointwise=False, default_factory=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)

__call__(*args, **kwargs)

TODO: Overloading in theories.set is interfering. Which to keep? # >>> _ = smt.Lambda([x], x > 0) & smt.BoolVal(False)

>>> x = smt.Int("x")
>>> _ = smt.Lambda([x], x > 0) & smt.Lambda([x], x > 1)
>>> foo = SortDispatch("foo", pointwise=True)
>>> foo.register(smt.IntSort(), lambda x: x + 1)
>>> foo(x)
x + 1
>>> z = smt.Array("z", smt.RealSort(), smt.IntSort())
>>> foo(z)
Lambda(x0!..., z[x0!...] + 1)
>>> smt.Lambda([x], x) + smt.Lambda([x], x)
Lambda(x0!..., x0!... + x0!...)
>>> smt.Lambda([x], x) + 1
Lambda(x0!..., x0!... + 1)

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.call = <kdrag.notation.SortDispatch object>: Sort based dispatch for () call syntax

kdrag.notation.choose = <kdrag.notation.SortDispatch object>: Sort based dispatch for Hilbert choice operator.

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.exists = <kdrag.notation.SortDispatch object>: Sort based dispatch for Exists quantifier.

kdrag.notation.forall = <kdrag.notation.SortDispatch object>: Sort based dispatch for ForAll quantifier.

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.induct_default(x, P)

kdrag.notation.induct_int(x, P)

kdrag.notation.induct_seq(a: SeqRef, P) → Proof

>>> x = smt.Const("x", smt.SeqSort(smt.IntSort()))
>>> induct(x, lambda s: smt.Length(s) >= 0)
|= Implies(And(Length(Empty(Seq(Int))) >= 0,
            ForAll(z!..., Length(Unit(z!...)) >= 0),
            ForAll([x!..., y!...],
                   Implies(And(Length(x!...) >= 0,
                               Length(y!...) >= 0),
                           Length(Concat(x!..., y!...)) >= 0))),
        Length(x) >= 0)

Parameters:: a (SeqRef)
Return type:: Proof

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.measure = <kdrag.notation.SortDispatch object>: `measure is an Int value associated with an ExprRef for use in defining well-founded recursion.

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.