kdrag.solvers.bdd

Classes

BDD()

class kdrag.solvers.bdd.BDD

Bases: object

>>> x,y,z = smt.Bools('x y z')
>>> bdd = BDD()
>>> bdd.declare(x,y,z)
>>> bdd.declare(z)
>>> bdd.translate(smt.And(x, smt.Or(z, y))).count()
3
>>> bdd.translate(smt.Exists([y], smt.And(x, smt.Or(z, y)))).count()
1
>>> list(bdd.pick_iter(smt.Exists([y], smt.And(x, smt.Or(z, y)))))
[[(x, True)]]

declare(*vs: ExprRef)

Parameters:

vs (ExprRef)

pick(expr: BoolRef, care_vars: list[ExprRef]) → list[tuple[BoolRef, bool]] | None

Parameters:

• expr (BoolRef)

• care_vars (list[ExprRef])

Return type:

list[tuple[BoolRef, bool]] | None

pick_iter(expr: BoolRef)

Parameters:

expr (BoolRef)

substitute(e: BoolRef, *substs) → Function

Parameters:

e (BoolRef)

Return type:

Function

translate(expr: BoolRef) → Function

Parameters:

expr (BoolRef)

Return type:

Function