diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 19:47:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-02 19:47:52 -0500 |
| commit | 5f3d21a7402538af837eaf943b5252b1db90080b (patch) | |
| tree | 0f8a791a8b9fcd03545f720df1110516ada7689e /src/theory/bv/theory_bv.cpp | |
| parent | 4e6eb0a191ec78cbebd842f9c732ef9bd76bd724 (diff) | |
(proof-new) Support proofs of quantifier instantiation (#5001)
This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
0 files changed, 0 insertions, 0 deletions