diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-04-16 12:45:10 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-16 10:45:10 +0000 |
| commit | 7cae3947227391313d93fa1e2ef7bfb4e9e3986d (patch) | |
| tree | 81860022a8288282678ebcfcf4976e8f20388ffc /cmake/FindGTest.cmake | |
| parent | 03c2724cef26fa20862634e25e3adc476d049db4 (diff) | |
Replace SExpr class by simpler conversion routines (#6363)
This PR finally removes the SExpr class. SMT-LIB compatible output is retained by using new on-the-fly conversion to s-expression strings. This finally allows us to remove includes to integer and rational from smt_engine.h.
In detail:
- a new set of toSExpr() methods is implemented that converts certain types to s-expression strings (without an intermediate class representing s-expressions)
- SmtEngine::getInfo() returns a string instead of SExpr and uses the new toSExpr methods
- SmtEngine::getStatistic() is removed
- SExpr class is removed
- d_commandVerbosity uses int instead of Integer
Diffstat (limited to 'cmake/FindGTest.cmake')
0 files changed, 0 insertions, 0 deletions