From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 2 Dec 2020 02:24:21 +0000 (-0800)
Subject: google test: api: Migrate result_black. (#5569)
X-Git-Tag: cvc5-1.0.0~2527
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=558efa2593fda09235c5f2163836771680d3442a;p=cvc5.git

google test: api: Migrate result_black. (#5569)

google test: api: Migrate result_black.
---

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 9fcf881a8..a8c696c00 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -13,7 +13,7 @@
 
 cvc4_add_unit_test_black(datatype_api_black api)
 cvc4_add_cxx_unit_test_black(op_black api)
-cvc4_add_cxx_unit_test_black(result_black api)
+cvc4_add_unit_test_black(result_black api)
 cvc4_add_cxx_unit_test_black(solver_black api)
 cvc4_add_cxx_unit_test_black(sort_black api)
 cvc4_add_cxx_unit_test_black(term_black api)
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
new file mode 100644
index 000000000..260845495
--- /dev/null
+++ b/test/unit/api/result_black.cpp
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file result_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds
+ ** 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 "test_api.h"
+
+using namespace CVC4::api;
+
+class TestApiResultBlack : public TestApi
+{
+};
+
+TEST_F(TestApiResultBlack, isNull)
+{
+  Result res_null;
+  ASSERT_TRUE(res_null.isNull());
+  ASSERT_FALSE(res_null.isSat());
+  ASSERT_FALSE(res_null.isUnsat());
+  ASSERT_FALSE(res_null.isSatUnknown());
+  ASSERT_FALSE(res_null.isEntailed());
+  ASSERT_FALSE(res_null.isNotEntailed());
+  ASSERT_FALSE(res_null.isEntailmentUnknown());
+  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();
+  ASSERT_FALSE(res.isNull());
+}
+
+TEST_F(TestApiResultBlack, eq)
+{
+  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;
+  EXPECT_EQ(res, res2);
+  EXPECT_EQ(res3, res2);
+}
+
+TEST_F(TestApiResultBlack, isSat)
+{
+  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();
+  ASSERT_TRUE(res.isSat());
+  ASSERT_FALSE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isUnsat)
+{
+  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();
+  ASSERT_TRUE(res.isUnsat());
+  ASSERT_FALSE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isSatUnknown)
+{
+  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();
+  ASSERT_FALSE(res.isSat());
+  ASSERT_TRUE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isEntailed)
+{
+  d_solver.setOption("incremental", "true");
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkConst(u_sort, "x");
+  Term y = d_solver.mkConst(u_sort, "y");
+  Term a = x.eqTerm(y).notTerm();
+  Term b = x.eqTerm(y);
+  d_solver.assertFormula(a);
+  Result entailed = d_solver.checkEntailed(a);
+  ASSERT_TRUE(entailed.isEntailed());
+  ASSERT_FALSE(entailed.isEntailmentUnknown());
+  Result not_entailed = d_solver.checkEntailed(b);
+  ASSERT_TRUE(not_entailed.isNotEntailed());
+  ASSERT_FALSE(not_entailed.isEntailmentUnknown());
+}
+
+TEST_F(TestApiResultBlack, isEntailmentUnknown)
+{
+  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.checkEntailed(x.eqTerm(x));
+  ASSERT_FALSE(res.isEntailed());
+  ASSERT_TRUE(res.isEntailmentUnknown());
+  EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON");
+}
diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
deleted file mode 100644
index aaa59e506..000000000
--- a/test/unit/api/result_black.h
+++ /dev/null
@@ -1,132 +0,0 @@
-/*********************                                                        */
-/*! \file result_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
- ** 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 { d_solver.reset(nullptr); }
-
-  void testIsNull();
-  void testEq();
-  void testIsSat();
-  void testIsUnsat();
-  void testIsSatUnknown();
-  void testIsEntailed();
-  void testIsEntailmentUnknown();
-
- 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.isEntailed());
-  TS_ASSERT(!res_null.isNotEntailed());
-  TS_ASSERT(!res_null.isEntailmentUnknown());
-  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::testIsEntailed()
-{
-  d_solver->setOption("incremental", "true");
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkConst(u_sort, "x");
-  Term y = d_solver->mkConst(u_sort, "y");
-  Term a = x.eqTerm(y).notTerm();
-  Term b = x.eqTerm(y);
-  d_solver->assertFormula(a);
-  Result entailed = d_solver->checkEntailed(a);
-  TS_ASSERT(entailed.isEntailed());
-  TS_ASSERT(!entailed.isEntailmentUnknown());
-  Result not_entailed = d_solver->checkEntailed(b);
-  TS_ASSERT(not_entailed.isNotEntailed());
-  TS_ASSERT(!not_entailed.isEntailmentUnknown());
-}
-
-void ResultBlack::testIsEntailmentUnknown()
-{
-  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->checkEntailed(x.eqTerm(x));
-  TS_ASSERT(!res.isEntailed());
-  TS_ASSERT(res.isEntailmentUnknown());
-  TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON");
-}
-