diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-31 19:05:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-01 00:05:29 +0000 |
| commit | 5e969241cd3bdec90138edb5d1c88d3e1797cb43 (patch) | |
| tree | 1c4a28fd98492f46bd03c4254b7f46031551ba50 /examples/simple_vc_quant_cxx.cpp | |
| parent | e461f722ff0888165e63916ee4be8502bd0b657c (diff) | |
Lazy proof reconstruction for strings theory solver (#7096)
This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule.
This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs).
Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).
Diffstat (limited to 'examples/simple_vc_quant_cxx.cpp')
0 files changed, 0 insertions, 0 deletions