def _sat(lexer, varname):
    """Return a DIMACS SAT."""
    _expect_token(lexer, {KW_p})
    fmt = _expect_token(lexer, {KW_sat, KW_satx, KW_sate, KW_satex}).value
    nvars = _expect_token(lexer, {IntegerToken}).value
    return _sat_formula(lexer, varname, fmt, nvars)
Return a DIMACS SAT.