From: makaimann <makaim@stanford.edu>
Date: Thu, 14 Mar 2019 07:08:15 +0000 (-0700)
Subject: check for null assumption in query and replace with false (#2858)
X-Git-Tag: cvc5-1.0.0~4250
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1744dc5f3140f9dc2aeb71f99c530feb83264a04;p=cvc5.git

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.
---

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)