Also makes another method statically available in NodeManager
(mkDummySkolem).
---------
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
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.
