Also fixes a debug failure for the nightlies.
This also changes mkTuple to not rely on subtyping (this method should regardless be deleted from our API, as it is not the recommended way of constructing tuples).
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 commit unifies abstract values and "uninterpreted constants" into a
single kind. Note that "uninterpreted constants" is a bit of a misnomer
in the context of the new API, since they do not correspond to the
equivalent of a declare-const command, but instead are values for
symbols of an uninterpreted sort (and thus special cases of abstract
values). Instead of treating "uninterpreted constants" as a separate
kind, this commit extends abstract values to hold a type (instead of
marking their type via attribute in NodeManager::mkAbstractValue())
and uses the type of the abstract values to determine whether they are a
value for a constant of uninterpreted sort or not. Unifying these
representations simplifies code and brings the terminology more in line
with the SMT-LIB standard.
This commit also updates the APIs to remove support for creating
abstract values and "uninterpreted constants". Users should never create
those. They can only be returned as a value for a term after a
satisfiability check.
Finally, the commit removes code in the parser for parsing abstract
values and updates the code for getting values involving abstract
values. Since the parser does not allow the declaration/definition of
abstract values, and determining whether a symbol is an abstract value
was broken (not all symbols starting with an @ are abstract values),
the code was effectively dead. Getting values involving "uninterpreted
constants" now no longer requires parsing the string of the values, but
instead, we can use existing API functionality.
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.
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.
