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).
This is the key step for eliminating the use of subtyping.
This makes several changes:
(1) CONST_INTEGER is now used for integer constants, which is now exported in the API. The type rule for CONST_RATIONAL is changed to always return Real, even if its value is integral. This means we can distinguish real and integer versions of the integers. Note this also implies that the rewriter now fully preserves types, as rewriting TO_REAL applied to a constant integer will return a constant integral rational.
(2) The type rules for EQUAL, DISTINCT, ITE and APPLY_UF are made strict, in other words, we given a type exception for equalities between an Int and a Real. This restriction impacts the API.
(3) The arithmetic rewrite for (Real) equality casts integers to reals as needed to ensure Reals are only made equal to Reals. The net effect is that TO_REAL may appear on either side of equalities.
(4) The core arithmetic theory solver is modified in several places to be made robust to TO_REAL occurring as the top symbol of sides of equality.
Several assertions are strengthened or added to ensure that equalities and substitutions are between terms of the same type, when it is necessary to do so.
Two quantifiers regressions are modified since the solving techniques are not robust to TO_REAL. A few unit tests are fixed to use proper types.
Solver::printStatisticsSafe() is private right now. There is no real reason for that, and as we claim that the driver is only using the regular API we should just make it public.
This makes it so that Tuple types are properly represented in the AST. It also removes a spurious restriction that disallowed higher-order tuples (this was leftover from a very old sanity check in the old API).
For example, a tuple type over (Int, Int) is now (TUPLE_TYPE INT INT) instead of a DATATYPE_TYPE constant.
Tuple types behave exactly like datatypes; we can still retrieve their DType as before.
This is in preparation for gradual types and symbolic tuple projections.
This PR moves two tests that dealt with particular issues out of unit/api/cpp (which should only have generic unit tests). They are now in unit/theory and api/cpp/.
When translating nodes with no children, the default case does not change the original node, and so we do not need to assume anything about the node. fixescvc5/cvc5-projects#416 . The example from the issue is added as a unit test.
This is in line with the change for non-parametric constructors (getConstructorTerm -> getTerm).
Also adds documentation to make the use of constructors, selectors, testers, updaters more clear.
This PR makes it so that common users of the datatypes API do not need to use "unresolved" datatypes sorts. Instead, these are automatically inferred by the NodeManager when calling mkMutualDatatypeTypes.
API Changes:
(1) adds addSelectorUnresolved to DatatypeConstructorDecl, which is the sole method needed to specify ordinary recursive selectors.
(2) adds to unit test examples that use this variant instead of using unresolved sorts.
(3) the API method mkUnresolvedSort is renamed to mkUnresolvedDatatypeSort and is marked experimental.
Note that unresolved datatype sorts are still needed to support mixed parametric datatypes and nested recursive datatypes in the smt2 parser, so they cannot be deleted yet.
Followup PR will add to documentation on elaborate further on how to use the datatypes API.
mkFunctionSort that takes two sorts as arguments is redundant, because
the first argument is equivalent to a vector of size one passed to the
other overload of mkFunctionSort. This commit removes the method from
the C++ API but keeps the existing semantics for the Java and Python
bindings for convenience and consistency with, e.g. mkTerm.
This kind is hardcoded only to work for sygus. I am not sure we want to support general constraints over it, or even if the token dt.size is the appropriate one.
Also adds a missing experimental warning that I had missed.
Fixescvc5/cvc5-projects#504.
