Improvements to qAlpha algorithm

[edenfrenkel]

Add several improvements and modifications to qAlpha, including:

• Refine invariant language for pDNF, to avoid cubes with literals that only mention variables that appear before the first existential quantifier in the prefix. Such formulas can be equivalently decomposed into formulas that use disjunctive literals instead of the cube, or that use cubes whose literals mention variables from after the first existential quantifier.
• By default, advance the "frontier" frame as much as possible, as opposed to gradually. The gradual option can now be enabled using the flag --gradual-advance. (The gradual SMT option, previously --gradual, is now --gradual-smt.) When using the gradual option, only weaken lemmas which appear in some UNSAT-core, or which have no weakenings.
• Add logging of parallel SMT queries during inference, which show how much time elapsed before the first SAT result was encountered, as well as the total time spent, and the number of SAT and UNSAT results encountered.
• As preprocessing, ignore atoms in the language which are either universally true or universally false.

[edenfrenkel]

I don't think the snapshot tests of qalpha make sense, because they require the invariants in the output to be printed in a specific way, which isn't necessarily the case. The only algorithmic guarantee is that the same invariants will be found, but ordering and variable names may change. Previously, I tried using --gradual-advance to make it more deterministic, but it seems there's still some indeterminism that makes this work only most of the time. @tchajed what do you think?

[tchajed]

I agree that snapshotting the invariant isn't worth the trouble. One thing we can (and probably should) do is to omit the entire invariant in the output that we snapshot.

[edenfrenkel]

@tchajed I agree with your snapshotting suggestion. Would you like to implement this as a part of the snapshotting, or to add some command-line argument to avoid printing the invariant? If you want to change the snapshotting, can you implement that? I tried to take a look and I'm not completely sure how you'd want to go about this.

[tchajed]

I'll work on changing the snapshotting, I'd prefer to redact there if possible.

[tchajed]

I changed my mind and made it a flag, it was a little easier to implement. Is this branch ready for a review now?

[edenfrenkel]

I changed my mind and made it a flag, it was a little easier to implement. Is this branch ready for a review now?

Yes, looks ready.