This changes the default behavior of `simplify` not to apply top-level
substitutions.
This behavior is can be unintuitive and may e.g. introduce internal
skolems into the term the user simplifies.
The previous behavior can be enabled by passing `applySubs` to true.
This moves term statistics collection from Solver to TermManager.
TermManager and Solver now both provide `getStatistics()`, the former
captures API level term statistics, the latter internal solver
statistics.
This also adds iterator capabilities to the Python Statistics class.
This introduces a TermManager object, which will, in the future, be the
sole object responsible for handling/managing terms and sorts. For now,
all corresponding functions in `cvc5::Solver` are marked as deprecated,
as is constructor `cvc5::Solver::Solver()`, since in the future a solver
instance must be constructed from a term manager instance. Currently, we
maintain a static thread_local term manager instance to not break the
API and continue providing constructor `cvc5::Solver::Solver()`.
Note that this already converts all C++ unit tests to use the
TermManager except for a single test `getStatistics()` in
`test/unit/api/cpp/solver_black.cpp`. Statistics handling is currently
still maintained on the solver level. The statistics we maintain,
however, concern terms only and will eventually be refactored to be
tracked in the NodeManager.
Further note that the Java and Python APIs will be refactored in
separate PRs.
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.
