changed predicate format

The way CVC4 does quantifiers, is 

    Expr expr = em.mkExpr(QuantifierType, bound_var_vector, formula);

For example

    em.mkExpr(EXISTS, [x], x=3);

Hence `x=3`, the "formula*", is a `Constraint`.

or a more complicated example:

    em.mkExpr(EXISTS, [x,y], [(x=3) /\ (x>y) => (y<3)] );

So `(x=3) /\ (x>y) => (y<3)`, the `Formula*` in this case is a `Connective`.

Can we leave it? I can't think out any way to ensure I can parse it correctly, other than making it as close to CVC's format as I can.