Migrate a majority of the functionality in parsers to the new API (#3838)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 5 Mar 2020 22:16:15 +0000 (16:16 -0600)
committerGitHub <noreply@github.com>
Thu, 5 Mar 2020 22:16:15 +0000 (16:16 -0600)
commit500f85f9c664001b84a90f4836bbb9577b871e29
treebe92a8a20267fe7d381ba1a6cf6c9477825776bf
parent50f82fac417bc5b27ecaeb34d4e8034339c5982f
Migrate a majority of the functionality in parsers to the new API (#3838)

This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout.

Remaining tasks:

Migrate the Datatypes to the new API in cvc/smt2.
Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL).
For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc.

Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version.

This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.
22 files changed:
examples/nra-translate/smt2toisat.cpp
examples/nra-translate/smt2tomathematica.cpp
examples/nra-translate/smt2toqepcad.cpp
examples/nra-translate/smt2toredlog.cpp
src/api/cvc4cpp.cpp
src/parser/CMakeLists.txt
src/parser/cvc/Cvc.g
src/parser/cvc/cvc_input.cpp
src/parser/parse_op.cpp [new file with mode: 0644]
src/parser/parse_op.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/smt2/smt2_input.cpp
src/parser/smt2/sygus_input.cpp
src/parser/tptp/Tptp.g
src/parser/tptp/tptp.cpp
src/parser/tptp/tptp.h
src/parser/tptp/tptp_input.cpp
test/unit/parser/parser_black.h