Age | Commit message (Collapse) | Author |
|
Fixes #2584. Currently, we are immediately terminating CVC4 if the user
issues a `(get-info :reason-unknown)` command if it didn't succeed a
`(check-sat)` call returning `unknown`. This commit changes the behavior
to return an `(error ...)` but continue executing afterwards. It turns
the `ModalException` thrown in this case into a
`RecoverableModalException` and adds a check in
`GetInfoCommand::invoke()` to turn it into a
`CommandRecoverableFailure`, which solves the issue.
|
|
|
|
(#2321)
|
|
Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.
|
|
|
|
This eliminates some hacks for dealing with Int/Real.
- Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA.
- Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant.
- Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852.
- Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).
|
|
|
|
|
|
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).
|
|
|
|
|
|
|
|
|
|
1172284. (#1362)
|
|
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
|
|
* Making the values argument const in the SetUserAttributeCommand constructor. Misc. cleanup of SetUserAttributeCommand.
* Removing override keyword that was making SWIG unhappy.
|
|
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand.
* Comment
* Pass expression names by reference.
* Update throw specifiers.
* Minor
* Switch expression names to CDMap, simplify interface for printing unsat core names.
* Revert throw specifier change.
* Minor simplifcations
|
|
GetModelCommand to nullptr. (#1142)
|
|
(#1135)
|
|
|
|
Commit 54d24c786d6a843cc72dfb5e377603349ea5e420 was
changing CVC4 to handle certain non-fatal errors
(such as calling get-unsat-core without a proceding
unsat check-sat command) without terminating the
solver. In the case of get-unsat-cores, the changes
lead to the solver crashing because it was trying to
print an unsat core initialized with the default
constructor, so the member variable d_smt was NULL,
which lead to a dereference of a null pointer.
One of the issues of the way non-fatal errors were
handled was that the error reporting was done in the
invoke() method of the command instead of the
printResult() method, which lead to the error
described above and other issues such as a call to
get-value printing a value after reporting an error.
This commit aims to improve the design by adding a
RecoverableModalException for errors that the solver
can recover from and CommandRecoverableFailure to
communicate that a command failed in a way that does
not prohibit the solver from continuing to execute.
The exception RecoverableModalException is thrown by
the SMTEngine and the commands catch it and turn it
into a CommandRecoverableFailure. The commit changes
all error conditions from the commit above and adds a
regression test for them.
|
|
|
|
Addresses coverity issues:
1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413
|
|
|
|
Breaking an edge between the sat solver and command.h.
|