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
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
Created by kdelmas on 04/11/16.