kdrag.property

Generic properties like associativity, commutativity, idempotence, etc.

Functions

AbelSemiGroup(f)
Antisymm(rel)
Assoc(f[, T])
Comm(f[, T])
CommMonoid(f, e)
CommSemiRing(add, mul, zero, one)
Idem(f[, T])
LeftIdentity(f, e[, T])
Monoid(f, e)
PartialOrder(rel)
PreOrder(rel)
Refl(rel)
RightIdentity(f, e[, T])
SemiGroup(f)
SemiLattice(join)
SemiRing(add, mul, zero, one)
StarSemiring(add, mul, zero, one, star)
Trans(rel)

kdrag.property.AbelSemiGroup(f) → BoolRef

Return type:

BoolRef

kdrag.property.Antisymm(rel) → BoolRef

>>> Antisymm(smt.Function("rel", smt.IntSort(), smt.IntSort(), smt.BoolSort()))
ForAll([x, y], Implies(And(rel(x, y), rel(y, x)), x == y))

Return type:

BoolRef

kdrag.property.Assoc(f, T=None) → BoolRef

>>> Assoc(smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort()))
ForAll([x, y, z], f(f(x, y), z) == f(x, f(y, z)))

Return type:

BoolRef

kdrag.property.Comm(f, T=None) → BoolRef

>>> Comm(smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort()))
ForAll([x, y], f(x, y) == f(y, x))

Return type:

BoolRef

kdrag.property.CommMonoid(f, e: ExprRef) → BoolRef

Parameters:

e (ExprRef)

Return type:

BoolRef

kdrag.property.CommSemiRing(add, mul, zero, one) → BoolRef

Return type:

BoolRef

kdrag.property.Idem(f, T=None) → BoolRef

>>> Idem(smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort()))
ForAll(x, f(x, x) == x)

Return type:

BoolRef

kdrag.property.LeftIdentity(f, e: ExprRef, T=None) → BoolRef

>>> LeftIdentity(smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort()), smt.IntVal(0))
ForAll(x, f(0, x) == x)

Parameters:

e (ExprRef)

Return type:

BoolRef

kdrag.property.Monoid(f, e: ExprRef) → BoolRef

Parameters:

e (ExprRef)

Return type:

BoolRef

kdrag.property.PartialOrder(rel) → BoolRef

Return type:

BoolRef

kdrag.property.PreOrder(rel) → BoolRef

Return type:

BoolRef

kdrag.property.Refl(rel) → BoolRef

>>> Refl(smt.Function("rel", smt.IntSort(), smt.IntSort(), smt.BoolSort()))
ForAll(x, rel(x, x))

Return type:

BoolRef

kdrag.property.RightIdentity(f, e: ExprRef, T=None) → BoolRef

>>> RightIdentity(smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort()), smt.IntVal(0))
ForAll(x, f(x, 0) == x)

Parameters:

e (ExprRef)

Return type:

BoolRef

kdrag.property.SemiGroup(f) → BoolRef

Return type:

BoolRef

kdrag.property.SemiLattice(join) → BoolRef

>>> _ = SemiLattice(smt.Function("join", smt.IntSort(), smt.IntSort(), smt.IntSort()))

Return type:

BoolRef

kdrag.property.SemiRing(add, mul, zero, one) → BoolRef

Return type:

BoolRef

kdrag.property.StarSemiring(add, mul, zero, one, star)

kdrag.property.Trans(rel) → BoolRef

>>> Trans(smt.Function("rel", smt.IntSort(), smt.IntSort(), smt.BoolSort()))
ForAll([x, y, z], Implies(And(rel(x, y), rel(y, z)), rel(x, z)))

Return type:

BoolRef