Consider adding SMT framing

[kquick]

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.

[aaronbembenek]

Thanks for the suggestion! Just to make sure I understand it correctly: are you referring to assertion levels in the SMT solver that are created with the SMT-LIB push and pop commands? If so, we do have modes that use assertion levels, and some of them reset the solver state entirely after each query (they're currently undocumented; I added this shortcoming as issue #7). However, on your example, these modes are not working the way I would expect them to, so I am going to need to spend some time looking into what is happening.

[kquick]

Yes, the push and pop commands. The is_sat rule should be discharged atomically and not need to accumulate across backtracking of the intensional parameters.