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

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f7ffe850a781503610cd163bcc3c54d67df83fbe..ddc1a61a0be9c7a198e2bff5ab51c943a03bba33 100644 (file)
--- 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 e05c228bcdc8e1cb3eaab5714b186421662200d6..396c4eedb02c882fa94d876ed2deb84ed6b35103 100644 (file)
--- 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 3343abc29d78b412147b4c5c78d928c1b6f9f246..910855505374e75b0bc3f286daae2142bb6537a1 100644 (file)
--- 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)

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 7566c432d1e71b6e863b8af0374f02b7b097de70..fc146186205c5f1b9f9cb5077214fd9655e0373c 100644 (file)
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -3,6 +3,7 @@
 
 cvc4_add_unit_test_black(datatype_api_black api)
 cvc4_add_unit_test_black(op_black api)
+cvc4_add_unit_test_black(result_black api)
 cvc4_add_unit_test_black(solver_black api)
 cvc4_add_unit_test_black(sort_black api)
 cvc4_add_unit_test_black(term_black api)

diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
new file mode 100644 (file)
index 0000000..ab5d65e
--- /dev/null
+++ b/test/unit/api/result_black.h
@@ -0,0 +1,136 @@
+/*********************                                                        */
+/*! \file result_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the Result class
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class ResultBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() { d_solver.reset(new Solver()); }
+  void tearDown() override {}
+
+  void testIsNull();
+  void testEq();
+  void testIsSat();
+  void testIsUnsat();
+  void testIsSatUnknown();
+  void testIsValid();
+  void testIsInvalid();
+  void testIsValidUnknown();
+
+ private:
+  std::unique_ptr<Solver> d_solver;
+};
+
+void ResultBlack::testIsNull()
+{
+  Result res_null;
+  TS_ASSERT(res_null.isNull());
+  TS_ASSERT(!res_null.isSat());
+  TS_ASSERT(!res_null.isUnsat());
+  TS_ASSERT(!res_null.isSatUnknown());
+  TS_ASSERT(!res_null.isValid());
+  TS_ASSERT(!res_null.isInvalid());
+  TS_ASSERT(!res_null.isValidUnknown());
+  Sort u_sort = d_solver->mkUninterpretedSort("u");
+  Term x = d_solver->mkVar(u_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x));
+  Result res = d_solver->checkSat();
+  TS_ASSERT(!res.isNull());
+}
+
+void ResultBlack::testEq()
+{
+  Sort u_sort = d_solver->mkUninterpretedSort("u");
+  Term x = d_solver->mkVar(u_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x));
+  Result res;
+  Result res2 = d_solver->checkSat();
+  Result res3 = d_solver->checkSat();
+  res = res2;
+  TS_ASSERT_EQUALS(res, res2);
+  TS_ASSERT_EQUALS(res3, res2);
+}
+
+void ResultBlack::testIsSat()
+{
+  Sort u_sort = d_solver->mkUninterpretedSort("u");
+  Term x = d_solver->mkVar(u_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x));
+  Result res = d_solver->checkSat();
+  TS_ASSERT(res.isSat());
+  TS_ASSERT(!res.isSatUnknown());
+}
+
+void ResultBlack::testIsUnsat()
+{
+  Sort u_sort = d_solver->mkUninterpretedSort("u");
+  Term x = d_solver->mkVar(u_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver->checkSat();
+  TS_ASSERT(res.isUnsat());
+  TS_ASSERT(!res.isSatUnknown());
+}
+
+void ResultBlack::testIsSatUnknown()
+{
+  d_solver->setLogic("QF_NIA");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("solve-int-as-bv", "32");
+  Sort int_sort = d_solver->getIntegerSort();
+  Term x = d_solver->mkVar(int_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver->checkSat();
+  TS_ASSERT(!res.isSat());
+  TS_ASSERT(res.isSatUnknown());
+}
+
+void ResultBlack::testIsValid()
+{
+  Sort u_sort = d_solver->mkUninterpretedSort("u");
+  Term x = d_solver->mkVar(u_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver->checkValid();
+  TS_ASSERT(res.isValid());
+  TS_ASSERT(!res.isValidUnknown());
+}
+
+void ResultBlack::testIsInvalid()
+{
+  Sort u_sort = d_solver->mkUninterpretedSort("u");
+  Term x = d_solver->mkVar(u_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x));
+  Result res = d_solver->checkValid();
+  TS_ASSERT(res.isInvalid());
+  TS_ASSERT(!res.isValidUnknown());
+}
+
+void ResultBlack::testIsValidUnknown()
+{
+  d_solver->setLogic("QF_NIA");
+  d_solver->setOption("incremental", "false");
+  d_solver->setOption("solve-int-as-bv", "32");
+  Sort int_sort = d_solver->getIntegerSort();
+  Term x = d_solver->mkVar(int_sort, "x");
+  d_solver->assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver->checkValid();
+  TS_ASSERT(!res.isValid());
+  TS_ASSERT(res.isValidUnknown());
+  TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON");
+}
+