diff options
| author | makaimann <makaim@stanford.edu> | 2019-03-14 00:08:15 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-14 07:08:15 +0000 |
| commit | 1744dc5f3140f9dc2aeb71f99c530feb83264a04 (patch) | |
| tree | f1a651a00059640e03e80ad620afb7bc8b0bc4b6 | |
| parent | b574ccf82270f8887d2d697c537c591ff4ab68a2 (diff) | |
check for null assumption in query and replace with false (#2858)
The default assumption argument in query was a null `Expr`, but the implementation asserted that the assumption is not null:
declaration: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.h#L593
implementation: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3548
The change is to simply check if the assumption is null and replaces it with the `false` expression if it is.
It should be `false` not `true` because it is negated in checkSatisfiability (when it's a query) as seen here: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3607
Note: I couldn't find a clean way to make `false` the default argument of assumption, because the expression manager is non-static.
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bac2f2f50..9914992ef 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3559,8 +3559,10 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { - Assert(!assumption.isNull()); - return checkSatisfiability(assumption, inUnsatCore, true); + return checkSatisfiability( + assumption.isNull() ? d_exprManager->mkConst<bool>(false) : assumption, + inUnsatCore, + true); } Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore) |