summaryrefslogtreecommitdiff
path: root/src/smt/command.h
AgeCommit message (Collapse)Author
2021-01-08[proof-new] Implementing getProof in the API and SMT engine (#5751)Haniel Barbosa
A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).
2020-12-02Update copyright headers.Aina Niemetz
2020-11-30Eliminate uses of SExpr from the parser. (#5496)Abdalrhman Mohamed
This is a step towards migrating Commands to the API. SExpr is an internal module that's not used by the API but is used by the parser and some commands. This PR replaces SExpr with terms of kind SEXPR in the parser and strings in commands (which brings them more inline with the API).
2020-11-30Remove includes for old API from internal code (#5536)Andrew Reynolds
The only code including the old API now are in parser/ and main/ which will require further untangling.
2020-11-26Removing infrastructure related to SMT model (#5527)Andrew Reynolds
Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine. The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.
2020-11-19Use symbol manager for unsat cores (#5468)Andrew Reynolds
This PR uses the symbol manager for handling names for unsat cores. This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.
2020-11-18Use symbol manager for get assignment (#5451)Andrew Reynolds
This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine. Note: we now limit :named terms to those not beneath quantifiers and let-bindings.
2020-11-11Move symbol manager to src/expr/ (#5420)Andrew Reynolds
This is required since symbol manager will use context dependent data structures (in its cpp). This is required since classes in src/parser/ are not allowed to include private headers.
2020-11-11Pass symbol manager to commands (#5410)Andrew Reynolds
This PR passes the symbol manager to Command::invoke. There are no behavior changes in this PR. This is in preparation for reimplementing several features in the parser related to symbols.
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic. This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred. Fixes #5343, fixes #4926. Work towards CVC4/cvc4-wishues#22.
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
This removes infrastructure for stream property related to printing type annotations on all variables. This is towards refactoring the printers.
2020-10-28Remove more uses of Expr (#5357)Andrew Reynolds
This PR removes more uses of Expr, mostly related to UnsatCore. It makes UnsatCore a cvc4_private object storing Node instead of Expr.
2020-10-20Remove some Commands from the API. (#5268)Abdalrhman Mohamed
This PR removes Solver::getAssignment command from the API as there is no way to assign names to terms in the API. It also removes ExpandDefinitionsCommand, an internal functionality in CVC4.
2020-10-16Refactor SMT-level model object (#5277)Andrew Reynolds
This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary. Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only. This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.
2020-10-10Provide API version of some SMT Commands. (#5222)Abdalrhman Mohamed
This PR provides an SMT version of the following SMT commands: get-instantiations block-model block-model-values get-qe get-qe-disjunct command.cpp now calls those functions instead of their SmtEngine counterparts. In addition, SEXPR is now an API kind.
2020-10-05Recover from some exceptions. (#5203)Abdalrhman Mohamed
This PR replaces more calls to SmtEngine functions with calls to corresponding Solver functions in command.cpp. The PR also adds CVC4_API_RECOVERABLE_CHECK macro to use for recoverable exceptions.
2020-09-22Refactor Commands to use the Public API. (#5105)Abdalrhman Mohamed
This is work towards eliminating the Expr layer. This PR does the following: Replace Expr/Type with Term/Sort in the API for commands. Remove the command export functionality which is not supported. Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors.
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback