def _expr2sat(ex, litmap): # pragma: no cover
    """Convert an expression to a DIMACS SAT string."""
    if isinstance(ex, Literal):
        return str(litmap[ex])
    elif isinstance(ex, NotOp):
        return "-(" + _expr2sat(ex.x, litmap) + ")"
    elif isinstance(ex, OrOp):
        return "+(" + " ".join(_expr2sat(x, litmap)
                               for x in ex.xs) + ")"
    elif isinstance(ex, AndOp):
        return "*(" + " ".join(_expr2sat(x, litmap)
                               for x in ex.xs) + ")"
    elif isinstance(ex, XorOp):
        return ("xor(" + " ".join(_expr2sat(x, litmap)
                                  for x in ex.xs) + ")")
    elif isinstance(ex, EqualOp):
        return "=(" + " ".join(_expr2sat(x, litmap)
                               for x in ex.xs) + ")"
    else:
        fstr = ("expected ex to be a Literal or Not/Or/And/Xor/Equal op, "
                "got {0.__name__}")
        raise ValueError(fstr.format(type(ex)))
Convert an expression to a DIMACS SAT string.