kdrag.termination

Do not use. Work in progress

Functions

default_measure(e)	Some default measures for built in types and algebraic datatypes.
lex_gt(es, es1[, measure])	Lexicographic greater than on lists of expressions.
opaque_abs_size(e)	A kludge to get around the fact that Z3's size function can return negative values, which breaks some of my proofs.
search_wf(head, calls, list[~z3.z3.ExprRef]]])	Find a permutation that makes every head greater than every call.

kdrag.termination.default_measure(e: ExprRef) → ExprRef

Some default measures for built in types and algebraic datatypes.

>>> x = smt.Int("x")
>>> kd.prove(default_measure(smt.IntVal(5)) == 5)
|= If(5 > 0, 5, -5) == 5
>>> assert default_measure(kd.Nat.S(kd.Nat.Z)) == 2
>>> kd.prove(default_measure(kd.seq(1,2,3)) == 3)
|= Length(Concat(Unit(1), Concat(Unit(2), Unit(3)))) == 3
>>> _ = kd.prove(default_measure(kd.Nat.S(kd.Nat.Z).pred) == 1)
>>> x = smt.Const("x", kd.Nat)
>>> _ = kd.prove(smt.Implies(x.is_S, default_measure(x) > default_measure(x.pred)))
>>> _ = kd.prove(smt.Implies(smt.And(x.is_S, x.pred.is_S), default_measure(x) > default_measure(x.pred.pred)))
>>> y = smt.BitVec("y",32)
>>> kd.prove(default_measure(smt.BitVecVal(-1, 32)) > default_measure(smt.BitVecVal(0, 32)))
|= BV2Int(4294967295) > BV2Int(0)

Parameters:

e (ExprRef)

Return type:

ExprRef

kdrag.termination.lex_gt(es: list[~z3.z3.ExprRef], es1: list[~z3.z3.ExprRef], measure=<function default_measure>) → BoolRef

Lexicographic greater than on lists of expressions.

>>> x, y = smt.Consts("x y", kd.Nat)
>>> _ = kd.prove(smt.Implies(x.is_S, lex_gt([x], [x.pred])))
>>> _ = kd.prove(smt.Implies(y.is_S, lex_gt([x, y], [x, y.pred])))
>>> _ = kd.prove(smt.Implies(y.is_S, smt.Not(lex_gt([x, y.pred], [x, y]))))
>>> _ = kd.prove(smt.Not(lex_gt([x, y], [x, y])))
>>> _ = kd.prove(smt.Implies(x.is_S, lex_gt([x, y], [x.pred, y])))

Parameters:

• es (list[ExprRef])

• es1 (list[ExprRef])

Return type:

BoolRef

kdrag.termination.opaque_abs_size(e: ExprRef) → ExprRef

A kludge to get around the fact that Z3’s size function can return negative values, which breaks some of my proofs.

Parameters:

e (ExprRef)

Return type:

ExprRef

kdrag.termination.search_wf(head: list[~z3.z3.ExprRef], calls: list[tuple[~z3.z3.BoolRef, list[~z3.z3.ExprRef]]], measure=<function default_measure>) → tuple[int, ...]

Find a permutation that makes every head greater than every call.

>>> x, y = smt.Consts("x y", kd.Nat)
>>> search_wf([x, y], [(x.is_S, [x.pred, y])])
(0, 1)
>>> search_wf([x, y], [(y.is_S, [x, y.pred])])
(0, 1)
>>> search_wf([x, y], [(y.is_S, [kd.Nat.S(x), y.pred])])
(1, 0)

Parameters:

• head (list[ExprRef])

• calls (list[tuple[BoolRef, list[ExprRef]]])

Return type:

tuple[int, …]