New C++ API: Add nullary constructor for Result. (#3603)

3 files changed, 24 insertions, 6 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f7ffe850a..ddc1a61a0 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -706,6 +706,13 @@ class CVC4ApiExceptionStream
 
 Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {}
 
+Result::Result() : d_result(new CVC4::Result()) {}
+
+bool Result::isNull() const
+{
+  return d_result->getType() == CVC4::Result::TYPE_NONE;
+}
+
 bool Result::isSat(void) const
 {
   return d_result->getType() == CVC4::Result::TYPE_SAT
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index e05c228bc..396c4eedb 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -82,6 +82,15 @@ class CVC4_PUBLIC Result
    */
   Result(const CVC4::Result& r);
 
+  /** Constructor. */
+  Result();
+
+  /**
+   * Return true if Result is empty, i.e., a nullary Result, and not an actual
+   * result returned from a checkSat() (and friends) query.
+   */
+  bool isNull() const;
+
   /**
    * Return true if query was a satisfiable checkSat() or checkSatAssuming()
    * query.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3343abc29..910855505 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3678,15 +3678,17 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
 
 Result SmtEngine::query(const Expr& assumption, bool inUnsatCore)
 {
-  return checkSatisfiability(
-      assumption.isNull() ? std::vector<Expr>() : std::vector<Expr>{assumption},
-      inUnsatCore,
-      true);
+  return checkSatisfiability(assumption.isNull()
+                                 ? std::vector<Expr>()
+                                 : std::vector<Expr>{assumption},
+                             inUnsatCore,
+                             true)
+      .asValidityResult();
 }
 
 Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore)
 {
-  return checkSatisfiability(assumptions, inUnsatCore, true);
+  return checkSatisfiability(assumptions, inUnsatCore, true).asValidityResult();
 }
 
 Result SmtEngine::checkSatisfiability(const Expr& expr,
@@ -3771,7 +3773,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       d_private->addFormula(e.getNode(), inUnsatCore, true, true);
     }
 
-    r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult();
+    r = check();
 
     if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
         && r.asSatisfiabilityResult().isSat() == Result::UNSAT)