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.
I increased cmake's minimum version in order to use the FindPython module, which allows the build system to specify python versions that are supported. Currently the support is extended to 3.6 through 3.10. I also removed some backward compatible conditions that do not apply anymore provided that cmake's minimum version is guaranteed to be 3.12.
MacOS builds are reenabled in ci.yml.
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.
Due to previous refactoring, the SMT solver called by the SyGuS solver no longer answers unsat when the synthesis problem has a valid solution.
This PR makes it so that unsat from the underlying SMT solver is now interpreted as "infeasible" and is officially returned as such by the SyGuS solver. Note that we return unsat when e.g. a CEGIS refinement lemma is equivalent to false. On the other hand, we do not yet answer unsat when we run out of terms (e.g. for finite grammars), as this is still guarded. A followup PR will address this.
To make the SMT solver answer unsat for infeasible conjectures, we do not guard CEGIS lemmas with the "feasible guard", instead we use the conjecture itself, similar to quantifier instantiation lemmas.
This further removes the "feasible guard" from the internal sygus solver, which was used as a way to prevent unsat due to the infeasibility of CEGIS refinement lemmas.
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.
This makes Solver::getNullarySort() obsolete and refactors everything
related to this function on the C++ and Python level. We still have to
keep it (temporarily) in the C++ API until the Java API is also
refactored accordingly.
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.
This PR addresses a few issues in the Python API:
the implementation of defineFunsRec() lacked the call to the C++ function
a bunch of tests for defineFunsRec() were missing
the test for getInstantiations() was incorrectly named and thus not valled.
add missing test for hashing of Sort
