This exports SkolemFunId to the API, and adds it to the Java, Python APIs, and adds unit tests.
It does some minor refactoring to remove unnecessary ids and to move abstract value to an internal skolem id.
Followup PRs will add methods for constructing/parsing skolems. I will also rename SkolemFunId -> SkolemId throughout the code base after this PR is merged.
This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.
This PR complements #8422 by adding a tester and a getter for cardinality constraints to the python API. The corresponding test from solver_black is translated and included.
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.
