This PR:
Updates the functionality of setIncrementalStringInput / appendIncrementalStringInput to a more intuitive behavior where append does not replace the current contents of the input.
Adds setStringInput to the API and updates the interactive shell to use this interface.
Updates the examples
Adds new unit tests
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 allows us to terminate quickly during preprocessing if a false assertion is encountered.
The other flags allow more generic handling of how to post-process results of check-sat.
Add a test for '<<' for the proof format mode
Add this test to the uncovered functions for Python and Java
Return placeholder value if Proof object is empty
Add tests for this (and add them to uncovered functions)
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.
This pull requests makes the enum that lists all proof rules a part of the API.
It also renames the enum from PfRule to ProofRule. It also renames some unrelated types and function names that share the PfRule name (such as DslPfRule).
This rename unfortunately touches many files since PfRule is not an uncommon type. (second to last commit)
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.
Work towards supporting (find-synth :X).
This adds a unified utility SynthFinder for implementing the functionality removed in #9796.
It introduces "find synth targets" as different things that can be found using find-synth.
Further PRs will connect this utility to the API.
