This introduces a TermManager object, which will, in the future, be the
sole object responsible for handling/managing terms and sorts. For now,
all corresponding functions in `cvc5::Solver` are marked as deprecated,
as is constructor `cvc5::Solver::Solver()`, since in the future a solver
instance must be constructed from a term manager instance. Currently, we
maintain a static thread_local term manager instance to not break the
API and continue providing constructor `cvc5::Solver::Solver()`.
Note that this already converts all C++ unit tests to use the
TermManager except for a single test `getStatistics()` in
`test/unit/api/cpp/solver_black.cpp`. Statistics handling is currently
still maintained on the solver level. The statistics we maintain,
however, concern terms only and will eventually be refactored to be
tracked in the NodeManager.
Further note that the Java and Python APIs will be refactored in
separate PRs.
This PR adds the proper checks for the parser API. It furthermore adds examples and unit tests for the parser API.
Note that InputParser::nextCommand and InputParser::nextTerm don't catch exceptions, since we want to throw ParserExceptions containing the parsing information, not API exceptions.
Also, at the moment, the InputParser can throw an exception during initialization, which is not caught either.
This is another step towards the parser API.
It hides the symbol manager's interface entirely. The old implementation is now contained via a new class SymManager.
The last step will be to move this (+ command.h, input_parser.h) from parser/api/cpp/ to include/cvc5/.
This is in preparation for new uses of the input parser, e.g. for parsing terms.
This adds the functionality to initialize the logic of the parser without reading commands.
It simplifies the handling of how logics were initialized previously.
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.
This moves `SymbolManager` and `SymbolTable` to the parser. To do so, it
modifies headers in the `context` package to be public to the parser
(changes `cvc5_private.h` to `cvc5parser_public.h`), because they are
shared between the parser and the main library.
mkFunctionSort that takes two sorts as arguments is redundant, because
the first argument is equivalent to a vector of size one passed to the
other overload of mkFunctionSort. This commit removes the method from
the C++ API but keeps the existing semantics for the Java and Python
bindings for convenience and consistency with, e.g. mkTerm.
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 replaces all usages of Debug() by Trace(), the same for similar methods like Debug.isOn().
Given that Debug is no longer used then, it is removed.
Fixes#2705. This commit removes the broken and unused --mmap option.
Given that we are planning to change to a different parser at some
point, it is not worth attempting to fix the option.
