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 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 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 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.
The CommandSequence command was not widely used and was essentially
just replicating the functionality of a vector of commands. This is work
towards a streamlined 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
When using --editline, our interactive_shell_black unit test was not
working because the unit test was redirecting std::cin and std::cout
to std::stringstreams, which does not work with Editline. This commit
refactors our InteractiveShell class to explicitly take the input and
output streams as arguments, which fixes the issue because we do not use
Editline for input streams that are not std::cin. Additionally, the
commit updates the unit test to use SMT-LIB syntax instead of the
deprecated CVC language.
This PR introduces a new ManagedStream class that replaces the previous ManagedOstream. It allows to directly store the (wrapped) stream objects in the options. Handling the stream options is moved from the options manager to option predicates and the different options for input and output streams are combined into a single one.
Some associated utilities (open_ostream.h and update_ostream.h) are now obsolete and thus removed.
This PR improves the check when we use libedit: only when the input is an interactive terminal.
This is motivated by a change to the unit test for the interactive mode that now properly redirects standard input (and output).
This PR gets rid of the Options::set() method, replacing it by direct access to the options data.
This method was only used internally and did nothing except for resolving the options data from the option tag type via template specializations (via ref()), which is no longer necessary.
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
