kdrag.termination.default_measure

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