Fix Context::forall and Context::exists quantifiers

[octalsrc]

The Context::forall and Context::exists functions were not structuring the S-expressions for variables correctly. This PR fixes that, and adds an example that uses quantifiers as a means of testing.

To demonstrate the problem, run the new example without the changes to src/context.rs. The example uses the following forall quantifier:

ctx.assert(
    // For any pair of sets,
    ctx.forall(
        [("s1", ctx.atom("MySet")), ("s2", ctx.atom("MySet"))],
        // One of the following is true:
        ctx.or(
            ...
        )
    )
)

which produces the following trace:

$ RUST_LOG="easy_smt=trace" cargo run --example quantifiers
...
[_] -> (declare-fun subset (MySet MySet) Bool)
[_] <- success
[_] -> (assert (forall (s1 MySet) (s2 MySet) (or (subset s1 s2) (exists (x MyElement) (and (member x s1) (not (member x s2)))))))
[_] <- (error "line 8 column 17: invalid sorted variable, '(' expected got s1")

The problem is that the variable declarations (s1 MySet) and (s2 MySet) are not grouped together as a sub-list. The forall expression is supposed to have the shape:

(forall ((var1 Sort1) ... (varN SortN)) (body))

The same problem occurs for the exists function: the variable declaration (x MyElement) in the above trace should be a singleton list ((x MyElement)).

With the changes to src/context.rs, the example is fixed:

$ RUST_LOG="easy_smt=trace" cargo run --example quantifiers
...
[_] -> (declare-fun subset (MySet MySet) Bool)
[_] <- success
[_] -> (assert (forall ((s1 MySet) (s2 MySet)) (or (subset s1 s2) (exists ((x MyElement)) (and (member x s1) (not (member x s2)))))))
[_] <- success
...

Thanks for writing this library! Aside from this bug, I've found it easy to get up and running with it.

[elliottt]

This looks great, thanks for fixing this!