This is a variant of get-timeout-core that asks to find a timeout core over a given set of assumptions, while all current assertions are implicitly included in the core.
Also adds news + an entry missed from #9585.
This pull requests adds support to get Proofs as proper objects from the API.
To do so it adds an object Proof that encapsulates a ProofNode. Furthermore, it adds a function proofsToString to the Solver object that prints (a vector of) proofs. Finally, it modifies the getProof function of the Solver object to return proofs.
Proof rules are returned as strings.
One thing I don't quite like is that the proof component configuration must be given to both the getProof and proofsToString method and must be the same.
Feature is based on the SAT proof. The lemmas that are accumulated by the ProofCnfStream during a check-sat call are filtered according to being used or not in the SAT proof and then printed as a list.
The motivation of this PR is to make the InputParser more foolproof in regards to initializing the logic.
The main change is that if the user provides a solver or symbol manager with a logic that has been set, then that logic is used. This means we throw an error if the 2 are using different logics.
It also removes the InputParser::setLogic method.
This requires adding isLogicSet and getLogic to the Solver and SymbolManager API.
This change is analogous to the one for declareFun and is required for making it easier to communicate formulas with uninterpreted sorts in a distributed setting.
Also fixes two minor parser issues:
We should revert to "assert" mode if a declaration is received, e.g. in between a check-sat and get-model.
We should catch errors for overloaded symbols even when fresh declarations are disabled.
This allows the user to have a consistent way of constructing constants (when fresh=false), without manually tracking a symbol table.
It also adds an option fresh-declarations to control whether the parser uses fresh constants. This is true by default to preserve backwards compatibility.
It also fixes an issue with using global-declarations from CLI.
This introduces a general way to use public enums both in the C++ and
the (upcoming) C API. For the C++ case, we now use enum classes rather
than enums for public enums. This also includes definitions for
C API to_string conversions for public enums. C API definitions in
cvc5_types.h are only included from the C API, guarded via a macro
(thus, for now, not included yet when the header is included).
This reenables the regressions for find-synth algorithms using the new smt2 commands.
Note that I simplified the FindSynthSolver (as you had suggested earlier).
This changes (get-timeout-core) to operate on preprocessed assertions, and to do dependency tracking to input assertions analogous to unsat cores.
This is to address scalability issues for timeout cores on problems with many definitions, as requested by Certora.
As a result, (get-timeout-core) now requires unsat cores to be enabled.
This further required improving our tracking of preprocessed assertions to take incremental mode into account, which was previously wrong.
Parser did not recognize `(fp #bX #bY #bZ)` as FP value. This further
introduces a new API function `Solver::mkFloatingPoint(const Term&,
const Term& const Term&)` to create a floating-point value from its
IEEE-754 bit-vector components.
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.
