def _formulas(lexer, varname, fmt, nvars):
    """Return a tuple of DIMACS SAT formulas."""
    types = {IntegerToken, LPAREN} | _SAT_TOKS[fmt]
    tok = lexer.peek_token()
    if any(isinstance(tok, t) for t in types):
        first = _sat_formula(lexer, varname, fmt, nvars)
        rest = _formulas(lexer, varname, fmt, nvars)
        return (first, ) + rest
    # null
    else:
        return tuple()