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.
This PR moves the public API headers into a top-level include directory. This makes it easier to find the public API of cvc5 and makes the install headers script obsolete.
Fixes#9553Fixes#9556
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.
Organizing the PR a bit:
we hook up the subtheories to TheoryFf
we expose FF-related things via the C++/Pytohn API and SMT-LIB2 interface.
we add a bunch of tests against these interfaces.
This experimental option causes cvc5 to synthesize rewrite rules based on the input. The code for this is a preprocessing pass which used to rewrite the input to a sygus conjecture. This is confusing since it changes the semantics of the input. We now call a separate subsolver.
This also cleans up set defaults. The options required for synthesizing rewrite rules are now applied locally to the subsolver spawned by the preprocessing pass.
We now terminate with an exception in the rare case when rewrite rule synthesis terminates.
This is required for further enhancements to the sygus solver for answering infeasible.
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.
Fixescvc5/cvc5-projects#435. To compute the cardinality class of constructors, we compute the maximum of the cardinality of the arguments. However, we considered the result of max(INTERPRETED_ONE, FINITE) to be FINITE. This is not accurate when finite model finding is turned off. This led to issues in the sequences solver, because we considered a constructor with an argument of an uninterpreted sort as finite and tried to retrieve that cardinality. This commit fixes the issue by making the result of max(INTERPRETED_ONE, FINITE) be FINITE_INTERPRETED.
Note in the original issue, the following assertion failure:
Fatal failure within void cvc5::Minisat::Solver::pop() at src/prop/minisat/core/Solver.cc:1971
Check failure
decisionLevel() == 0
occurred because of an IllegalArgumentException was being thrown (calling Cardinality::getFiniteCardinality() on a sort with an non-finite cardinality). This exception then lead to an unexpected decision level (similar to the issue with uncaught TypeCheckingExceptionPrivate exceptions fixed in c4be9f5). There is an on-going effort to get rid of IllegalArgumentException, so it is not worth adding a fix for this. For example, commit
f8306b2 changed the code in cardinality.cpp that was throwing the exception in this case.
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.
This PR fixes the issue of replacing bars with underscores in already quoted symbols.
For example previously this line would print |_a _|
std::cout << d_solver.declareFun("|a |", {}, d_solver.getRealSort());
Now it prints |a |.
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).
