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 adds a general way to initialize the finite field and the element
of the final field in the C++ API from a string of an arbitrary base.
---------
Signed-off-by: Sarkoxed <sarkoxed2013@yandex.ru>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
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).
