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
Right now, the printers expect some options to be passed explicitly and read other options statically from the options object.
This refactors this, using the `ioutils` utility which we already use to store option values in the private storage associated with output streams. In detail, does a couple of things:
- the `mkoptions.py` script now generates the `options/io_utils.*` files to handle all options defined in the `printer` options module
- reading the necessary options from the ostreams is pushed into the printers themselves
- explicit options are removed from (almost) all `toStream()` functions
- a few options are moved to the `printer` options module (making the `printSuccess` utility obsolete)
One of the loose ends of the options refactor is that internal code can write to options at will, even when the accessing it via Env::getOptions() which returns a const reference. There are technical reasons for this, C++ does not propagate the constness into reference members.
This PR changes this behaviour by making the references members we use all over the place (options().smt.foo) const references and adding new functions writeSmt() which allow write access -- if you have a non-const handle to the options object.
In order to do that, this PR also changes all places that legitimately change the options (options handlers, set defaults, solver engine and places where we spawn subsolvers) to use the new syntax. After that, only a single place remains: the solver engine attempts to write the filename (from Solver::setInfo("filename", "...");) into the original options (that are restored to the new solver object after a reset. As only the API solver has write access to this, it is moved to the Solver::setInfo() method.
With this PR, all internal code is properly guarded against erroneous (and reckless) changing of options.
Fixescvc5/cvc5-projects#12.
With this PR, CI passes when using CONST_INTEGER instead of (all) integral CONST_RATIONAL.
This does not make this change yet, so CONST_RATIONAL is still used throughout.
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 renames the arithmetic internal and API kind PLUS to ADD for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_ADD, FLOATINGPOINT_ADD).
This renames the internal arithmetic kinds MINUS and UMINUS for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_SUB, FLOATINGPOINT_SUB).
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.
This is in preparation of having two different kinds (CONST_RATIONAL
and CONST_INT) share the same payload. To do so, we cannot rely on
ConstantMap<Rational> anymore to map the payload type to a kind. This
commit extends support in the mkmetakind script to deal with such
payloads by adding a + suffix to the type. The commit also does some
minor refactoring of NodeManager::mkConst() and
NodeManager::mkConstInternal() to support setting the kind explicitly.
Finally, the commit addresses all instances where mkConst<Rational>()
is used, including the API.
This makes all methods for constructing skolems local to SkolemManager.
It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.
This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
This PR moves the code responsible for parsing the command line to the main folder. Note that the options themselves, and converting strings to the options proper types, calling predicates etc, stays in libcvc5. The PR also slightly refactors the options code to get rid of the assign_* functions.
This PR moves the remaining special purpose functions out of the Options class. This set of functions is only used to implement API functions in the smt engine (getting and setting options by string), and by the main driver for parsing and printing usage information.
This feature is useful for example for succinctly inserting children of
a node in the reverse order. To make this work, the commit fixes the
declaration of `reference` in the `NodeValue::iterator`. The
`std::reverse_iterator` adapter expects the `reference` type to match
the return type of `operator*` in the corresponding iterator (as
mandated by the standard). Despite its name, `reference` does not have
to be a C++ reference. Note that we cannot actually make it a C++
reference because `NodeValue::iterator` wraps the `NodeValue*` in a
`Node`/`TNode` in `operator*`.
The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.
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.
