We now track difficulty on lemmas themselves, which can potentially used as a heuristic for measuring the usefulness of lemmas.
This also makes it so that all literals in lemmas are used for incrementing difficulty.
Adds necessary API methods for supporting abstract sorts in the cpp, java, python APIs.
An abstract sort represents a class of sorts. It is parameterized by a kind. For example, the abstract sort parameterized by the kind BITVECTOR_SORT denotes bitvectors of unspecified bit-width.
To support the above functionality, the kinds of Sort must be exported in the API, which is done in this PR.
This is the first step towards supporting the rewrite DSL for parameterized sorts, and planned SyGuS extensions that use gradual typing.
Fixes#9140. Instead of crashing with an assertion error during the
creation of the operator, the commit introduces error checks at the API
level to ensure that the indices are `> 1` as required by the SMT-LIB
standard.
It also fixes our error check for `mkFloatingPointSort` to ensure that
the exponent and the significand length are both greater than one as
required by the SMT-LIB standard.
The method DatatypeDecl::isResolved() was not accurate, nor was it being checked in cvc5_checks.h when constructing multiple datatypes.
Fixescvc5/cvc5-projects#522.
This refactors Sort, Term, Op and datatype objects to not maintain a
reference (and depend) on Solver, but an associated NodeManager. This
allows to share node managers between solver instances.
Also changes the name of the enum for now to have a prefix, since we are not using enum classes.
Furthermore this excludes true from being a preprocessed learned literal.
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.
