| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #5163. When `:global-declarations` is disabled (the default), then
`(reset-assertions)` should remove all declared and defined symbols. Before
this commit, we would remove the defined function from `SmtEngine` but the
parser would not remove it from its symbol table because the symbol was defined
at (what it considered) level 0. Level 0, however, is reserved for global
symbols that we never want to remove.
This commit adds an additional global `pushScope()`/`popScope()`, similar to
what we have in `SmtEngine`. As a result, user-defined symbols are now defined
at level 1 and get removed from the `SymbolTable` when `(reset-assertions)` is
called. The commit also makes sure that symbols defined by the logic are
asserted at level 0, so that they are not removed by `(reset-assertions)`. It
adds a flag to `defineType` to ignore duplicate definitions because some
symbols are defined by multiple logics, which leads to a failing assertion when
inserting them both at level 0 in the hashmap of the `SymbolTable`. E.g.
strings and integer arithmetic both define `Int`. The commit also fixes
existing unit tests that fail with these stricter semantics of
`(reset-assertions)`.
Signed-off-by: Andres Noetzli <noetzli@amazon.com>
|
|
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.
|
|
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.
|
|
Calling (reset) multiple times produced parsing problems (#4866) and could probably lead to all kinds of interesting issues.
In a nutshell, reset() failed to properly reset d_initialOptions (which is used to properly reset d_options) so that all options defaulted after the second call to reset().
This PR properly sets d_initialOptions after a reset (and the filename as well).
Fixes #4866.
|
|
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).
|
|
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.
|
|
This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.
|
|
Fixes #4151. Commit e9f4cec2cad02e270747759223090c16b9d2d44c fixed how
`(reset-assertions)` is handled by destroying and recreating the
`PropEngine` owned by `SmtEngine`. When unsat cores are enabled,
creating a `PropEngine` triggers the creation of a SAT proof and a CNF
proof. In the `ProofManager`, we had assertions that checked that those
kinds of proofs were only created once, which is not true anymore. This
commit removes the assertions, cleans up the memory management in
`ProofManager` to use `std::unique_ptr` and makes all the
`ProofManager::init*` methods non-static for consistency.
The commit also fixes an additional issue that I encountered while
testing the fix: When creating the new `PropEngine`, we were not
asserting `true` and `(not false)`, which lead to an error if we tried
to get the unsat core after a `(reset-assertion)` command and we had
asserted `(assert false)`. The commit fixes this by asserting `true` and
`(not false)` in the constructor of `PropEngine`.
The regression test is an extension of the example in #4151 and covers
both issues.
|
|
Fixes #4077. The master equality engine in `TheoryEngine` was being
created at SAT context level 1. If the context was popped to level zero
by `(reset-assertions)`, `true` and `false` were removed from the master
equality engine, which lead for example to `(= ((_ extract 3 3) x) (_
bv1 1))` and `(_ bv1 4)` being merged (this can be gathered from looking
at `-t equality`). This commit fixes the issue by postponing the global
context pushes until after the theory engine has been initialized.
|
|
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
|
|
Fixes #4028. TheoryEngine's pointer was not updated to the new
PropEngine when resetting assertions. This commit fixes that. As far
as I can tell, this was the only class storing a PropEngine* that
isn't owned by PropEngine, so we should hopefully not have other
similar issues.
|
|
Calling (reset-assertions) in start mode was not handled correctly.
Additionally, when calling (check-sat) after (reset-assertions) after a
(check-sat) call that answered unsat, we answered unsat instead of sat.
This cleans up and fixes reset-assertions) handling.
|
|
This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers.
This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue.
This is work towards parser migration.
|
|
Fixes #3353. #3062 introduced a flag that tracks whether we have seen a
`(set-logic ...)` command to improve the handling of `--force-logic`.
However, the flag was not set to `false` when `(reset)` was called. This
commit fixes the issue.
|
|
|
|
This commit adds a check to make sure that the result of a `(check-sat)`
call matches the expected result set via `(set-info :status ...)`. In
doing so, it also fixes an issue where CVC4 would crash if asked for the
unsat core after setting the status to `unsat` but before calling
`(check-sat)` (see regression for concrete example). This happened
because CVC4 was storing the expected result and the computed result
both in the same variable (the expected result wasn't really being used
though). This commit keeps track of the expected result and the computed
result in separate variables to fix that issue.
|
|
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.
|
|
Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.
|
