diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-03 08:08:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-03 08:08:04 -0500 |
| commit | 0a960638857ae4682162cf19b47801bc19dd94c3 (patch) | |
| tree | ab8415d9235f518661c2af3147c747ef3d216af9 /proofs/signatures | |
| parent | bbfb310eba34ae078ee2601c7e5ea2b56dbe1252 (diff) | |
Update CEGQI to use lemma status instead of forcing preprocess (#4551)
This PR removes a hack in counterexample-guided quantifier instantiation.
The issue is the CEGQI needs to know the form of certain lemmas, after theory preprocessing. CEGQI needs to know this since it must construct solutions (e.g. solved form of equalities) for free variables in these lemmas, which includes fresh variables in the lemma after postprocess like ITE skolems.
Previously, CEGQI was hacked so that it applied the preprocessing eagerly so that it had full knowledge of the postprocessed lemma. This PR updates CEGQI so that it uses the returned LemmaStatus as the way of getting the lemma after postprocess. It also fixes the lemma status returned by TheoryEngine so that all lemmas not just the "main lemma" are returned as a conjunction.
This PR is in preparation for major refactoring to theory preprocessing for the sake of proofs.
Diffstat (limited to 'proofs/signatures')
0 files changed, 0 insertions, 0 deletions