summaryrefslogtreecommitdiff
path: root/src/smt/command.h
AgeCommit message (Collapse)Author
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-09-01Removes old proof code (#4964)Haniel Barbosa
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure. It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
This PR makes two simultaneous changes: The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API. Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType. This PR removes : ExprManger::mkDatatypeType. The Expr-level datatype itself. This PR removes all references to its include file. It also updates one remaining unit test from Expr -> Node. This PR will enable further removal of other datatype-specific things in the Expr layer.
2020-08-18Refactor functions that print commands (Part 2) (#4905)Abdalrhman Mohamed
This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code.
2020-08-12Refactor functions that print commands (Part 1) (#4869)Abdalrhman Mohamed
This PR is a step towards migrating commands to the Term/Sort level. The functions for printing synth-fun command and its grammar were modified to remove their dependency on command objects and use nodes instead of exprs and types. Similar changes to other functions that print commands will follow.
2020-08-04Modify the smt2 parser to use the Sygus grammar. (#4829)Abdalrhman Mohamed
2020-07-10Add support for printing 'get-abduct' in verbose mode (#4710)Andrew V. Jones
Issue For any of the following files: test/regress/regress1/abduct-dt.smt2 test/regress/regress1/sygus-abduct-test-ccore.smt2 test/regress/regress1/sygus-abduct-test.smt2 test/regress/regress1/sygus-abduct-ex1-grammar.smt2 test/regress/regress1/sygus-abduct-test-user.smt2 test/regress/regress1/sygus/abduction_1255.corecstrs.readable.smt2 test/regress/regress1/sygus/abduction_streq.readable.smt2 test/regress/regress1/sygus/abd-simple-conj-4.smt2 test/regress/regress1/sygus/uf-abduct.smt2 test/regress/regress1/sygus/yoni-true-sol.smt2 running the following: ./bin/cvc4 -vvv <file> would print: Invoking: ERROR: don't know how to print a Command of class: N4CVC416GetAbductCommandE Resolution This PR adds support in src/printer/smt2/smt2_printer.cpp to be able to print a Command of type GetAbductCommand. Given the similarities between get-abduct and synth-fun, I have refactored the printing logic in toStream(std::ostream& out, const SynthFunCommand* c) for a printing a SyGuS grammar to be shared between both SynthFunCommand and GetAbductCommand. As a result, you now see something like this: [avj@tempvm build]$ ./bin/cvc4 -vvv ../test/regress/regress1/abduct-dt.smt2 Invoking: (set-option :incremental false) Invoking: (set-logic ALL) Invoking: (declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List))))) Invoking: (declare-fun x () List) Invoking: (assert (distinct x nil)) minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy. Invoking: (get-abduct A (= x (cons (head x) (tail x)))) (error "Cannot get abduct when produce-abducts options is off.") Signed-off-by: Andrew V. Jones andrew.jones@vector.com
2020-06-30Interpolation step 1 (#4638)Ying Sheng
This is the first step of adding Interpolation. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack. The first step creates the API framework, while omits the implementation for getting interpolation.
2020-06-25Remove sygus1 parser (#4651)Andrew Reynolds
We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard). As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script. This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR. FYI @abdoo8080 .
2020-06-18Add logic check for define-fun(s)-rec (#4577)Andres Noetzli
This commit adds a logic check for `define-fun-rec`/`define-funs-rec` at the level of the new API that checks whether the logic is quantified and includes UF. To make sure that the parser actually executes that check, this commit converts the `DefineFunctionRecCommand` command to use the new API instead of the old one. This temporarily breaks the `exportTo` functionality for `DefineFunctionRecCommand` but this is not currently used within the CVC4 code base (and it seems unlikely that users use commands).
2020-06-16Update copyright headers.Aina Niemetz
2020-06-06Keep definitions when global-declarations enabled (#4572)Andres Noetzli
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions are kept when `:global-declarations` are enabled. Until now, CVC4 was keeping track of the symbols of a definition correctly but lost the body of the definition when the user context was popped. This commit fixes the issue by adding a `global` parameter to `SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If that parameter is set, the definitions of functions are added at level 0 to `d_definedFunctions` and the lemmas for recursive function definitions are kept in an additional list and asserted during each `checkSat` call. The commit also updates new API, the commands, and the parsers to reflect this change.
2020-03-06Simplify DatatypeDeclarationCommand command (#3928)Andrew Reynolds
The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here. It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort. This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
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-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-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-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-26Adds a macro to SWIG to ignore the override and final C++11 keywords in ↵Tim King
older versions of SWIG. (#1281)
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