kdrag.refine

Classes

OpenDefn(name, *sorts)	An Open Definition.
RefinedDefn(name, *sorts)	EXPERIMENTAL IDEA.

class kdrag.refine.OpenDefn(name, *sorts)

Bases: object

An Open Definition. This is sound to because it is implemented as an if-then-else chain where we are adding definitions to previously undefined cases. There is a floppy tail kept at the end of the chain.

This is debatably a new axiom schema. It only uses kd.define, but unusual uses of kd.define have the force of a new axiom.

>>> d = OpenDefn("f9023", smt.IntSort(), smt.IntSort())
>>> f = d.decl()
>>> x = smt.Int("x")
>>> d.define([x], x < 0, -x)
>>> kd.full_simp(f(-5))
5
>>> kd.full_simp(f(5)) # undefined. Reaches end of current chain so can't be simplified further
f90231(5)
>>> d.define([x], x >= 0, x + 1)
>>> kd.full_simp(f(5))
6
>>> d.define([x], x == 0, 42) # covered by previous case, so is irrelevant
>>> kd.full_simp(f(0))
1

Parameters:

• name (str)

• sorts (tuple[SortRef, ...])

decl()

define(args, precond, body)

fs: list[FuncDeclRef]

name: str

sorts: tuple[SortRef, ...]

class kdrag.refine.RefinedDefn(name: str, *sorts: tuple[SortRef, ...])

Bases: object

EXPERIMENTAL IDEA. DO NOT USE

This is using an is_sat judgement rather than an is_valid judgement. It only somewhat protects you from inconsistency.

It is very possible for multiple undefined values to be refined such that their axioms are not consistent

>>> r = RefinedDefn("g123", smt.IntSort())
>>> g123 = r.decl()
>>> r.refine(g123 > 0)
>>> r.refine(g123 > 1)
>>> r.property
|= And(And(True, g123 > 0), g123 > 1)
>>> r.refine(g123 < 0)
Traceback (most recent call last):
...
ValueError: Refinement is inconsistent

Parameters:

• name (str)

• sorts (tuple[SortRef, ...])

decl: FuncDeclRef

property property

refine(newprop: BoolRef, example: BoolRef | None = None)

Parameters:

• newprop (BoolRef)

• example (BoolRef | None)