This PR moves the public API headers into a top-level include directory. This makes it easier to find the public API of cvc5 and makes the install headers script obsolete.
Fixes#9553Fixes#9556
This corrects issues in our parser related to when symbols should be added to our symbol table.
In particular, symbols should be bound only when commands are executed and not as they are parsed. Binding during parsing leads to errors in interactive mode where those symbols are bound more than once, say if a command is partially parsed and then re-parsed based on our line buffering. This required further modifications to the interactive shell to execute commands immediately as they are parsed, since executing them may impact parsing (say if a declare-fun was on the same line as the subsequent command).
This adds new methods for accessing the binding methods of the underlying symbol table of symbol manager.
There are further issues of this form to correct, e.g. for define-fun-rec, which will be addressed in a separate PR.
This renames Smt2 and Tptp to Smt2State and TptpState, and decouples their implementation from ANTLR specific parsing. The Smt2State will be reused in the new flex parser.
It introduces ANTLR-specific wrappers of these classes (called by their previous names Smt2 and Tptp to avoid propagating further name changes), having the same functionality for parsing.
Followup PRs will clean Smt2State / TptpState and move them to smt2_state.h / tptp_state.h.
This commit moves the `Command` infrastructure to the parser (to
`src/parser/api/cpp`) and moves it to the `cvc5::parser` namespace. The
`Command`-related files are compiled with `-D__BUILDING_CVC5LIB`,
because they need access to the internal printers. The commit refactors
the internal code to not depend on `Command` anymore. To do this, the
commit refactors printing derived classes of `CommandStatus` to follow a
similar structure to printing commands (so that we can also print
command statuses internally without creating instances of
`Commandstatus`). This is a step towards a parser API.
The public cvc5 API now lives in the cvc5 namespace. All internal parts were moved into the (new) internal namespace.
The final hierarchy will be as follows:
cvc5
~~ public API
::context
::internal
::parser
::main
After this PR it will be:
cvc5
~~ public API
::internal
::context
::main
::parser
This PR consolidates SetLanguage, ExprSetDepth and ExprDag into a single consistent utility. Also, it makes it play more nicely with users setting these options and removes some obsolete code.
