This PR merges together SMTLib2 commands whose output can be ignored (typically when the output is either (success) or an error). In practice, these commands are effectively added to a queue given by a ByteString Builder and this queue is only sent to the solver as one big batched command when the output of the next command cannot be ignored. This also means that in non-debug mode the commands are not checked to be valid and may thus lead to an error that isn't caught immediately.
The expected speed-up is described in the qa/z3_binding_faster_eval branch of pirouette-benchmarks: Pirouette is now 1.16 times faster on the largest example, isUnity. Note that these measurements were made with a version of Z3 that improves the speed of the binding used in Pirouette's code but isn't part of a release yet, so until the next release the actual speed-up may differ.
While that wasn't measured to improve the speed of Pirouette, the serialization of s-expressions to bytestring is now done using the untrimmed strategy which is theoretically faster for building a bytestring which will be consumed immediately afterwards. Similarly, we manually set the size of the chunks depending on whether a single command or a whole batch is being serialized.
This PR merges together SMTLib2 commands whose output can be ignored (typically when the output is either
(success)or an error). In practice, these commands are effectively added to a queue given by a ByteString Builder and this queue is only sent to the solver as one big batched command when the output of the next command cannot be ignored. This also means that in non-debug mode the commands are not checked to be valid and may thus lead to an error that isn't caught immediately.The expected speed-up is described in the
qa/z3_binding_faster_evalbranch ofpirouette-benchmarks: Pirouette is now 1.16 times faster on the largest example,isUnity. Note that these measurements were made with a version of Z3 that improves the speed of the binding used in Pirouette's code but isn't part of a release yet, so until the next release the actual speed-up may differ.While that wasn't measured to improve the speed of Pirouette, the serialization of s-expressions to bytestring is now done using the untrimmed strategy which is theoretically faster for building a bytestring which will be consumed immediately afterwards. Similarly, we manually set the size of the chunks depending on whether a single command or a whole batch is being serialized.