kdrag.solvers.symunion

Symbolic union a la Rosette

Module Attributes

expr2py

class SymPartial[T] A single entry of symunion.

Functions

`expr2py_default`(e)
`py2expr`(...)

Classes

`PartialExpr`(expr[, cond])
`PartialFuncDecl`(decl[, contract])
`SymUnion`(values)	Symbolic Union.

class kdrag.solvers.symunion.PartialExpr(expr: z3.z3.ExprRef, cond: z3.z3.BoolRef | None = None)

Bases: object

Parameters:

expr (ExprRef)
cond (BoolRef | None)

cond: BoolRef | None = None

expr: ExprRef

map(f: Callable[[ExprRef], ExprRef]) → PartialExpr

Parameters:: f (Callable[[ExprRef], ExprRef])
Return type:: PartialExpr

map2(other: PartialExpr, f: Callable[[ExprRef, ExprRef], ExprRef]) → PartialExpr

Parameters:

other (PartialExpr)
f (Callable[[ExprRef, ExprRef], ExprRef])

Return type:

PartialExpr

class kdrag.solvers.symunion.PartialFuncDecl(decl: z3.z3.FuncDeclRef, contract: Callable[[z3.z3.ExprRef], z3.z3.BoolRef] | None = None)

Bases: object

Parameters:

decl (FuncDeclRef)
contract (Callable[[ExprRef], BoolRef] | None)

contract: Callable[[ExprRef], BoolRef] | None = None

decl: FuncDeclRef

class kdrag.solvers.symunion.SymUnion(values: tuple[tuple[BoolRef, T], ...])

Bases: Generic

Symbolic Union. A SymUnion[T] represents a value of type T that can be one of several possibilities, each with an associated symbolic boolean condition.

https://docs.racket-lang.org/rosette-guide/sec_value-reflection.html https://hackage.haskell.org/package/grisette

>>> su1 = SymUnion.wrap(42)

Parameters:: values (tuple[tuple[BoolRef, T], ...])

assume(cond: BoolRef) → SymUnion[T]

Add a guard to the SymUnion. The could also be called guard or project or perhaps filter.

Parameters:

self (SymUnion[T])
cond (BoolRef)

Return type:

SymUnion[T]

collect() → SymUnion[ExprRef]

Collect via if-then-else chain all the branches into a single guarded expression. This is a merge of symbolic states into a single symbolic state. It internalizes the branching back into the solver

>>> b = smt.Bool("b")
>>> su = SymUnion.of_list([(b, 42), (smt.Not(b), 43)]).map(py2expr)
>>> su.collect()
SymUnion(values=((Or(b, Not(b)), If(b, 42, If(Not(b), 43, undef!...))),))

Parameters:: self (SymUnion[ExprRef])
Return type:: SymUnion[ExprRef]

concretize() → SymUnion[object]

Turn a symbolic expression into all combinations of

Parameters:: self (SymUnion[ExprRef])
Return type:: SymUnion[object]

classmethod empty() → SymUnion[T]

The empty SymUnion. This is the identity for union and the annihilator for intersection. >>> SymUnion.empty() SymUnion(values=())

Return type:: SymUnion[T]

flatmap(f: Callable[[T], SymUnion[U]], strict=False) → SymUnion[U]

Parameters:

self (SymUnion[T])
f (Callable[[T], SymUnion[U]])

Return type:

SymUnion[U]

static flip() → SymUnion[bool]

Flip a coin.

>>> SymUnion.flip()
SymUnion(values=((b!..., True), (Not(b!...), False)))

Return type:: SymUnion[bool]

join() → SymUnion[T]

Flatten a SymUnion of SymUnions. This is monadic join

Parameters:: self (SymUnion[SymUnion[T]])
Return type:: SymUnion[T]

map(f: Callable[[T], U]) → SymUnion[U]

Parameters:

self (SymUnion[T])
f (Callable[[T], U])

Return type:

SymUnion[U]

map2(other: SymUnion[U], f: Callable[[T, U], V]) → SymUnion[V]

Map a binary function over two SymUnions

Parameters:

self (SymUnion[T])
other (SymUnion[U])
f (Callable[[T, U], V])

Return type:

SymUnion[V]

classmethod of_list(values: list[tuple[BoolRef, T]]) → SymUnion[T]

Create a SymUnion from a list of (condition, value) pairs.

>>> su2 = SymUnion.of_list([(smt.BoolVal(True), 42), (smt.BoolVal(False), 43)])
>>> su2
SymUnion(values=((True, 42), (False, 43)))

Parameters:: values (list[tuple[BoolRef, T]])
Return type:: SymUnion[T]

prune() → SymUnion[T]

Remove impossible conditions via smt query.

>>> su = SymUnion.of_list([(smt.BoolVal(True), 42), (smt.BoolVal(False), 43)])
>>> su.prune()
SymUnion(values=((True, 42),))

Parameters:: self (SymUnion[T])
Return type:: SymUnion[T]

store(index: int, value: SymUnion) → SymUnion

Parameters:

self (SymUnion[tuple])
index (int)
value (SymUnion)

Return type:

SymUnion

valueize() → SymUnion[ExprRef]

Use smt solver to enumrate all possible models of the expression.

Parameters:: self (SymUnion[ExprRef])
Return type:: SymUnion[ExprRef]

values: tuple[tuple[BoolRef, T], ...]

classmethod wrap(v: T, ctx=True) → SymUnion[T]

Wrap a value in a SymUnion. This is monadic pure/return >>> SymUnion.wrap(42) SymUnion(values=((True, 42),))

Parameters:: v (T)
Return type:: SymUnion[T]

kdrag.solvers.symunion.expr2py = <kdrag.notation.SortDispatch object>: class SymPartial[T] A single entry of symunion. The Maybe monand to it’s List. But why bother?

kdrag.solvers.symunion.expr2py_default(e: ExprRef) → object

Parameters:: e (ExprRef)
Return type:: object

kdrag.solvers.symunion.py2expr(x: object) → ExprRef

kdrag.solvers.symunion.py2expr(x: ExprRef) → ExprRef

kdrag.solvers.symunion.py2expr(x: int) → ExprRef

kdrag.solvers.symunion.py2expr(x: float) → ExprRef

kdrag.solvers.symunion.py2expr(x: bool) → ExprRef

kdrag.solvers.symunion.py2expr(x: str) → ExprRef

kdrag.solvers.symunion.py2expr(x: tuple) → ExprRef

kdrag.solvers.symunion.py2expr(x: list) → ExprRef

kdrag.solvers.symunion.py2expr(x: complex) → ExprRef

kdrag.solvers.symunion.py2expr(x: set) → ExprRef

kdrag.solvers.symunion.py2expr(x: frozenset) → ExprRef

>>> py2expr(1)
1
>>> py2expr(1.5)
3/2
>>> py2expr(True)
True
>>> py2expr("hello")
"hello"
>>> py2expr((1, 2))
Tuple_Int_Int(1, 2)
>>> py2expr({1, 2})
Store(Store(K(Int, False), 1, True), 2, True)
>>> py2expr([1,2,4,6])
Concat(Unit(1), Concat(Unit(2), Concat(Unit(4), Unit(6))))
>>> py2expr(1+2j)
C(1, 2)

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