Transform a at most n using the sequential encoding
Transform a at most n using the sequential encoding
the Boolean expressions addressed by the at most
the maximum number of kids which must be true
the Z3 context to create Z3 terms
Z3 Boolean expression
Transfrom a Boolean expression to a BDD
Transfrom a Boolean expression to a BDD
the Z3 Boolean expression
the BDD for Boolean variable (leaves of the Z3 AST)
context in which the expression has been built
the BDD
Transform a Boolean expression to a truncated BDD
Transform a Boolean expression to a truncated BDD
the Z3 Boolean expression
the BDD for Boolean variable (leaves of the Z3 AST)
context in which the expression has been built
the maximum number of positive arc in paths of BDD
the BDD
Transform an expression to its dnfFrom
Transform an expression to its dnfFrom
Boolean expression
the list of leaves terms
the context use to build the expression
the DNF form
Transform the expression in NNF form
Transform the expression in NNF form
the expression to transform
the list of leaves
the context use to build the expression
break ite into i.t + \neg i.e
the NNF form
Base trait for translating Z3 SMT Boolean expression to BDD