def add_ast(t, bdd):
    """Add abstract syntax tree `t` to `self`.

    Any AST nodes are acceptable,
    provided they have attributes:
      - `"operator"` and `"operands"` for operator nodes
      - `"value"` equal to:
        - `"True"` or `"False"` for Boolean constants
        - a key (var name) passed to `bdd.var()` for variables

    @type t: `Terminal` or `Operator` of `astutils`
    @type bdd: object with:
      - `bdd.false`
      - `bdd.true`
      - `bdd.var()`
      - `bdd.apply()`
      - `bdd.quantify()`
    """
    # operator ?
    if t.type == 'operator':
        if t.operator in ('\A', '\E') and len(t.operands) == 2:
            qvars, expr = t.operands
            u = add_ast(expr, bdd)
            qvars = {x.value for x in qvars}
            assert t.operator in ('\A', '\E'), t.operator
            forall = (t.operator == '\A')
            return bdd.quantify(u, qvars, forall=forall)
        elif t.operator == '\S':
            expr, rename = t.operands
            u = add_ast(expr, bdd)
            rename = {k.value: v.value for k, v in rename}
            return bdd.rename(u, rename)
        else:
            operands = [add_ast(x, bdd) for x in t.operands]
            return bdd.apply(t.operator, *operands)
    elif t.type == 'bool':
        u = bdd.false if t.value.lower() == 'false' else bdd.true
        return u
    elif t.type == 'var':
        return bdd.var(t.value)
    elif t.type == 'num':
        i = int(t.value)
        u = bdd._add_int(i)
        return u
    else:
        raise Exception(
            'unknown node type "{t}"'.format(t=t.type))