Replace SExpr class by simpler conversion routines (#6363)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 16 Apr 2021 10:45:10 +0000 (12:45 +0200)
committerGitHub <noreply@github.com>
Fri, 16 Apr 2021 10:45:10 +0000 (10:45 +0000)
commit7cae3947227391313d93fa1e2ef7bfb4e9e3986d
tree81860022a8288282678ebcfcf4976e8f20388ffc
parent03c2724cef26fa20862634e25e3adc476d049db4
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
src/api/cpp/cvc5.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/util/sexpr.cpp
src/util/sexpr.h