the structure function
Generates DIMACS and OPB files encoding the prime implicant enumeration problem to solve them using external solvers.
Parses a sharpCDCL model file, possibly containing several models of a same formula.
Parses a sharpCDCL model file, possibly containing several models of a same formula. TODO implement real parsing, string splitting + scanning does not scale
Translates the structure function of a system represented by a z3 expression to a SAT-solver friendly formula in DIMACS or OPB format for prime implicant enumeration using external solvers.