Consider adding SMT framing

Using `is_sat` in the body of a rule doesn't use any framing, so even if the solver has discharged the sat determination, it remains in memory within the solver and can't be discarded even if it will no longer be used. When the rule is being used to process a large number of intensional facts, this can cause significant memory consumption overhead in the solver.

For example:

```
@external
input values(i32)

output solve(i32, i32, i32, i32)
solve(X, Y, Z, A) :-
values(X), values(Y), values(Z),
X != Y, X != Z, Y != Z,
2020 = X + Y + Z,
A = X * Y * Z.
```

This trivial program generates results for all triples that sum to 2020. For a values.tsv file with 1000 entries, this executes in Formulog on the order of 9 seconds on my system.

Changing the line
```
2020 = X + Y + Z,
```
to
```
is_sat(`2020 #= bv_add(bv_add(X, Y), Z)`),
```

can generate millions of SMT terms. While each of these is trivially sat/unsat by Z3, I would expect this to run for some lengthy period of time and produce the same answer as the Datalog-only version. Instead, this runs for tens of minutes with the Z3 process slowly accumulating more memory consumption before dying from memory exhaustion on my 32GB machine. Using SMT framing should allow previous results to be garbage collected and avoid this memory exhaustion.