diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-19 10:32:37 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-19 10:32:37 -0500 |
| commit | 06d91e9121ecdadfc96d6175792992395833329f (patch) | |
| tree | 15a969c7c044279c3677ded69465add67ea96fad /src/proof/sat_proof_implementation.h | |
| parent | f70674c2f0c6c1c55e3d7c5fed916fc1e7721ffe (diff) | |
Add infrastructure for tracking instantiation lemmas (for proofs, and minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
0 files changed, 0 insertions, 0 deletions