kdrag.theories.logic.temporal

Functions

`Always`(x[, vs])	Returns the TBool signal that x is always true after time t (inclusive).
`And`(*args)
`Bool`(name)	Create a Boolean signal
`Bools`(names)	Create a list of Boolean signals
`Eq`(x, y)
`Eventually`(x)
`F`(x)
`G`(x[, vs])
`If`(c, x, y)
`Implies`(x, y)
`Int`(name)	Create an integer signal
`Ints`(names)	Create a list of Integer signals
`NEq`(x, y)
`Next`(x)
`Not`(x)
`Or`(*args)
`TLift`(n)	Lift a value into a constant signal
`TSort`(sort)	Lift a sort to a sort that depends on time
`UNCHANGED`(p)	Returns the TBool representing that signal at time t equals signal at time t + 1
`Valid`(p)	The statement that the formula is true at t = 0.
`X`(p)
`is_T`(x)
`lift_binop`(S, op)
`lift_unop`(S, op)

kdrag.theories.logic.temporal.Always(x: DatatypeRef, vs=None) → DatatypeRef

Returns the TBool signal that x is always true after time t (inclusive).

>>> t = smt.Int("t")
>>> s = TBool(smt.Lambda([t], t >= 1))
>>> _ = kd.prove(smt.Not(Valid(Always(s))))
>>> _ = kd.prove(Valid(Always(Next(s))))

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

kdrag.theories.logic.temporal.And(*args)

>>> _ = And(TLift(True), TLift(False))

kdrag.theories.logic.temporal.Bool(name: str) → DatatypeRef

Create a Boolean signal

>>> x = Bool("x")
>>> _ = x & True

Parameters:: name (str)
Return type:: DatatypeRef

kdrag.theories.logic.temporal.Bools(names: str) → list[DatatypeRef]

Create a list of Boolean signals

>>> x, y = Bools("x y")
>>> _ = x & y

Parameters:: names (str)
Return type:: list[DatatypeRef]

kdrag.theories.logic.temporal.Eq(x, y)

>>> x,y = smt.Consts("x y", TSort(smt.IntSort()))
>>> smt.simplify(Valid(Eq(x,y)))
val(x)[0] == val(y)[0]

kdrag.theories.logic.temporal.Eventually(x)

kdrag.theories.logic.temporal.F(x)

kdrag.theories.logic.temporal.G(x, vs=None)

kdrag.theories.logic.temporal.If(c: DatatypeRef, x: DatatypeRef, y: DatatypeRef) → DatatypeRef

>>> _ = If(TLift(True), TLift(1), TLift(2))

Parameters:

c (DatatypeRef)
x (DatatypeRef)
y (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.logic.temporal.Implies(x: DatatypeRef, y: DatatypeRef) → DatatypeRef

>>> x,y = smt.Consts("x y", TSort(smt.BoolSort()))
>>> smt.simplify(Valid(Implies(x, y)))
Or(Not(val(x)[0]), val(y)[0])

Parameters:

x (DatatypeRef)
y (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.logic.temporal.Int(name: str) → DatatypeRef

Create an integer signal

>>> x = Int("x")
>>> _ = x + TLift(1)

Parameters:: name (str)
Return type:: DatatypeRef

kdrag.theories.logic.temporal.Ints(names: str) → list[DatatypeRef]

Create a list of Integer signals

>>> x, y = Ints("x y")
>>> _ = x + y

Parameters:: names (str)
Return type:: list[DatatypeRef]

kdrag.theories.logic.temporal.NEq(x, y)

>>> x,y = smt.Consts("x y", TSort(smt.IntSort()))
>>> smt.simplify(Valid(NEq(x,y)))
Not(val(x)[0] == val(y)[0])

kdrag.theories.logic.temporal.Next(x)

>>> x = smt.Const("x", TSort(smt.BoolSort()))
>>> Next(x)
T_Bool(Lambda(t!..., val(x)[t!... + 1]))

kdrag.theories.logic.temporal.Not(x: DatatypeRef) → DatatypeRef

>>> x = smt.Const("x", TSort(smt.BoolSort()))
>>> smt.simplify(Valid(Not(x)))
Not(val(x)[0])

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

kdrag.theories.logic.temporal.Or(*args)

>>> _ = Or(TLift(True), TLift(False))

kdrag.theories.logic.temporal.TLift(n: ExprRef | int | str) → DatatypeRef

Lift a value into a constant signal

>>> TLift(1)
T_Int(K(Int, 1))
>>> TLift(True)
T_Bool(K(Int, True))

Parameters:: n (ExprRef | int | str)
Return type:: DatatypeRef

kdrag.theories.logic.temporal.TSort(sort)

Lift a sort to a sort that depends on time

>>> TR = TSort(smt.RealSort())
>>> x,y = smt.Consts("x y", TR)
>>> _ = x + y
>>> _ = x + TLift(2.1)

kdrag.theories.logic.temporal.UNCHANGED(p: DatatypeRef) → DatatypeRef

Returns the TBool representing that signal at time t equals signal at time t + 1

>>> smt.simplify(Valid(UNCHANGED(TLift(1))))
True

Parameters:: p (DatatypeRef)
Return type:: DatatypeRef

kdrag.theories.logic.temporal.Valid(p: DatatypeRef) → BoolRef

The statement that the formula is true at t = 0. Convert a temporal formula into a Boolean. https://en.wikipedia.org/wiki/Kripke_semantics#Semantics_of_modal_logic

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

kdrag.theories.logic.temporal.X(p)

kdrag.theories.logic.temporal.is_T(x: ExprRef) → bool

>>> x = Int("x")
>>> is_T(x)
True
>>> is_T(TLift(1))
True
>>> is_T(smt.BoolVal(True))
False

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

kdrag.theories.logic.temporal.lift_binop(S, op)

kdrag.theories.logic.temporal.lift_unop(S, op)