<SYSTEM_TASK:>
Solve the following problem using Python, implementing the functions described below, one line at a time
<END_TASK>
<USER_TASK:>
Description:
 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)))