Schedule preregistration lemmas to be satisfied after user assertions (#6134)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 12 Mar 2021 20:26:55 +0000 (12:26 -0800)
committerGitHub <noreply@github.com>
Fri, 12 Mar 2021 20:26:55 +0000 (20:26 +0000)
commit210734994076904f4770dfe7a1877bf3d2687f39
tree872fdbf73ef7694d400f2647f3f84b0e432567e5
parent092d7d16cd7be4337d4408d35ce8b200fca3c768
Schedule preregistration lemmas to be satisfied after user assertions (#6134)

Commit d47a8708171f1cf488fe9ce05f56f2566db53093 refactored the interface of
prop engine. In doing so, it changed the order in which preregistration lemmas
were asserted. Before the commit, they were asserted after all the user
assertions. After the commit, they were asserted after each user assertion that
generated them. This, however, seems to have a negative performance impact,
especially for string benchmarks because the justification heuristic tries to
justify the assertions in the order in which they appear. Intuitively, it makes
sense to first try to satisfy the user assertions before trying to satisfy the
preregistration lemmas.

Signed-off-by: Andres Noetzli <noetzli@amazon.com>
src/prop/prop_engine.cpp