summaryrefslogtreecommitdiff
path: root/src/smt/command.cpp
AgeCommit message (Collapse)Author
2018-10-22Recover from wrong use of get-info :reason-unknown (#2667)Andres Noetzli
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.
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-08-21Removing unused bool members in command.cpp. Also initializes a bool member. ↵Tim King
(#2321)
2018-08-13Fix get-unsat-assumptions output (#2301)Andres Noetzli
Fixes #2298. The `get-unsat-assumptions` command was printing the result with square brackets and commas instead of parentheses and spaces between the assumptions.
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
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).
2018-04-09Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)Aina Niemetz
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
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)).
2018-02-28SmtEngine::getAssignment now returns a vector of assignments. (#1628)Aina Niemetz
2018-01-08Removes throw specifiers from command.{h,cpp}. (#1485)Tim King
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-14Cleaning up exporting vectors within commands. Resolves CID 1172285 and ↵Tim King
1172284. (#1362)
2017-11-03Sygus clean main (#1297)Andrew Reynolds
* Remove front end hack for sygus. * Remove other hack, add sygus solution output mode. * Clang format * Minor * Fix * Minor * Remove unused field.
2017-10-17Making the values argument const in the SetUserAttributeCommand const… (#1249)Tim King
* Making the values argument const in the SetUserAttributeCommand constructor. Misc. cleanup of SetUserAttributeCommand. * Removing override keyword that was making SWIG unhappy.
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
* 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
2017-09-26Fixing CIDs 1172014 and 1172013: Initializing members of GetProofCommand and ↵Tim King
GetModelCommand to nullptr. (#1142)
2017-09-26CID 1362904: Initializing GetInstantiationsCommand::d_smtEngine to nullptr. ↵Tim King
(#1135)
2017-09-24CID 1362907: Initializing d_smtEngine to nullptr. (#1134)Tim King
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
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.
2017-07-07Update copyright headers.Mathias Preiner
2017-03-30[Coverity] Remove throw qualifiers in src/smtremove_throwAndres Notzli
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
2016-04-20update from the masterPaulMeng
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ↵Tim King
Breaking an edge between the sat solver and command.h.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback