kdrag.modal

Treating T -> Bool as a kind of truth value

Functions

`Box`(p[, prefix])
`In`(x, S[, prefix])
`MImplies`(p, q)	https://en.wikipedia.org/wiki/Modal_companion
`Next`(p[, prefix])
`PAnd`(*args[, prefix])	Pointwise And
`PDistinct`(*args[, prefix])	Pointwise Distinct
`PEq`(x, y)	Pointwise equality rather than on the nose equality.
`PIf`(c, t, e)	Pointwise if-then-else rather than on the nose if-then-else.
`PImplies`(p, q[, prefix])	Pointwise Implies
`POr`(*args[, prefix])	Pointwise Or
`PointEq`(x, y)	Pointwise equality rather than on the nose equality.
`PointIf`(c, t, e)	Pointwise if-then-else rather than on the nose if-then-else.
`Valid`(p[, prefix])	Convert from modal truth to regular Bool
`coerce`(s, e)

kdrag.modal.Box(p: PBoolRef, prefix='t') → PBoolRef

Parameters:: p (PBoolRef)
Return type:: PBoolRef

kdrag.modal.In(x: PExprRef, S: ArrayRef | QuantifierRef, prefix='t') → PBoolRef

>>> x = smt.Array("x", smt.IntSort(), smt.IntSort())
>>> S = smt.Array("S", smt.IntSort(), smt.SetSort(smt.IntSort()))
>>> In(x, S)
Lambda(t!..., S[t!...][x[t!...]])

Parameters:

x (PExprRef)
S (ArrayRef | QuantifierRef)

Return type:

PBoolRef

kdrag.modal.MImplies(p: PBoolRef, q: PBoolRef) → PBoolRef

https://en.wikipedia.org/wiki/Modal_companion

Parameters:

p (PBoolRef)
q (PBoolRef)

Return type:

PBoolRef

kdrag.modal.Next(p: PBoolRef, prefix='t') → PBoolRef

>>> t = smt.Const("t", smt.IntSort())
>>> Next(smt.Lambda([t], t))
Lambda(t!..., t!... + 1)

Parameters:: p (PBoolRef)
Return type:: PBoolRef

kdrag.modal.PAnd(*args, prefix='t') → PBoolRef

Pointwise And

>>> t = smt.Const("t", smt.IntSort())
>>> PAnd(smt.Lambda([t], t > 0), smt.Lambda([t], t < 10))
Lambda(t!..., And(t!... > 0, t!... < 10))

Return type:: PBoolRef

type kdrag.modal.PBoolRef = ArrayRef | QuantifierRef

kdrag.modal.PDistinct(*args, prefix='t') → PBoolRef

Pointwise Distinct

>>> t = smt.Const("t", smt.IntSort())
>>> PDistinct(smt.Lambda([t], t), smt.Lambda([t], t + 1))
Lambda(t!..., t!...  != t!... + 1)

Return type:: PBoolRef

kdrag.modal.PEq(x: PExprRef, y: PExprRef) → PBoolRef

Pointwise equality rather than on the nose equality.

>>> x = smt.Int("x")
>>> PointEq(smt.Lambda([x], x), 1)
Lambda(x0!..., x0!... == 1)

Parameters:

x (PExprRef)
y (PExprRef)

Return type:

PBoolRef

type kdrag.modal.PExprRef = ArrayRef | QuantifierRef

kdrag.modal.PIf(c, t: ExprRef, e: ExprRef) → ExprRef

Pointwise if-then-else rather than on the nose if-then-else.

>>> x = smt.Int("x")
>>> PointIf(smt.Lambda([x], x > 0), 1, -1)
Lambda(x0!..., If(x0!... > 0, 1, -1))
>>> PointIf(smt.Lambda([x], x > 0), smt.Lambda([x], x+1), -1)
Lambda(x0!..., If(x0!... > 0, x0!... + 1, -1))

Parameters:

t (ExprRef)
e (ExprRef)

Return type:

ExprRef

kdrag.modal.PImplies(p: PBoolRef, q: PBoolRef, prefix='t') → PBoolRef

Pointwise Implies

>>> t = smt.Const("t", smt.IntSort())
>>> PImplies(smt.Lambda([t], t > 0), smt.Lambda([t], t > 1))
Lambda(t!..., Implies(t!... > 0, t!... > 1))

Parameters:

p (PBoolRef)
q (PBoolRef)

Return type:

PBoolRef

kdrag.modal.POr(*args, prefix='t') → PBoolRef

Pointwise Or

>>> t = smt.Const("t", smt.IntSort())
>>> POr(smt.Lambda([t], t > 0), smt.Lambda([t], t < 10))
Lambda(t!..., Or(t!... > 0, t!... < 10))

Return type:: PBoolRef

kdrag.modal.PointEq(x: PExprRef, y: PExprRef) → PBoolRef

Pointwise equality rather than on the nose equality.

>>> x = smt.Int("x")
>>> PointEq(smt.Lambda([x], x), 1)
Lambda(x0!..., x0!... == 1)

Parameters:

x (PExprRef)
y (PExprRef)

Return type:

PBoolRef

kdrag.modal.PointIf(c, t: ExprRef, e: ExprRef) → ExprRef

Pointwise if-then-else rather than on the nose if-then-else.

>>> x = smt.Int("x")
>>> PointIf(smt.Lambda([x], x > 0), 1, -1)
Lambda(x0!..., If(x0!... > 0, 1, -1))
>>> PointIf(smt.Lambda([x], x > 0), smt.Lambda([x], x+1), -1)
Lambda(x0!..., If(x0!... > 0, x0!... + 1, -1))

Parameters:

t (ExprRef)
e (ExprRef)

Return type:

ExprRef

kdrag.modal.Valid(p: PBoolRef, prefix='t') → BoolRef

Convert from modal truth to regular Bool

https://en.wikipedia.org/wiki/Validity_(logic)#Valid_formula

>>> t = smt.Const("t", smt.IntSort())
>>> Valid(Box(smt.Lambda([t], t > 0)))
ForAll(t!..., ForAll(t1!..., Implies(t!... <= t1!..., t1!... > 0)))

Parameters:: p (PBoolRef)
Return type:: BoolRef

kdrag.modal.coerce(s: SortRef, e) → ExprRef

Parameters:: s (SortRef)
Return type:: ExprRef