google test: api: Migrate grammar_black. (#5566)

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index a8c696c0018f5bfdc5545b2382455d3017acd439..b437146d9501d48afce438d4793df3e297de5b83 100644 (file)
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -12,10 +12,10 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(datatype_api_black api)
+cvc4_add_unit_test_black(grammar_black api)
 cvc4_add_cxx_unit_test_black(op_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)
-cvc4_add_cxx_unit_test_black(grammar_black api)
 

diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
new file mode 100644 (file)
index 0000000..2cfe678
--- /dev/null
+++ b/test/unit/api/grammar_black.cpp
@@ -0,0 +1,117 @@
+/*********************                                                        */
+/*! \file grammar_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Abdalrhman Mohamed, 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 guards of the C++ API functions.
+ **
+ ** Black box testing of the guards of the C++ API functions.
+ **/
+
+#include "test_api.h"
+
+using namespace CVC4::api;
+
+class TestApiGrammarBlack : public TestApi
+{
+};
+
+TEST_F(TestApiGrammarBlack, addRule)
+{
+  Sort boolean = d_solver.getBooleanSort();
+  Sort integer = d_solver.getIntegerSort();
+
+  Term nullTerm;
+  Term start = d_solver.mkVar(boolean);
+  Term nts = d_solver.mkVar(boolean);
+
+  Grammar g = d_solver.mkSygusGrammar({}, {start});
+
+  ASSERT_NO_THROW(g.addRule(start, d_solver.mkBoolean(false)));
+
+  ASSERT_THROW(g.addRule(nullTerm, d_solver.mkBoolean(false)),
+               CVC4ApiException);
+  ASSERT_THROW(g.addRule(start, nullTerm), CVC4ApiException);
+  ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC4ApiException);
+  ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC4ApiException);
+
+  d_solver.synthFun("f", {}, boolean, g);
+
+  ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC4ApiException);
+}
+
+TEST_F(TestApiGrammarBlack, addRules)
+{
+  Sort boolean = d_solver.getBooleanSort();
+  Sort integer = d_solver.getIntegerSort();
+
+  Term nullTerm;
+  Term start = d_solver.mkVar(boolean);
+  Term nts = d_solver.mkVar(boolean);
+
+  Grammar g = d_solver.mkSygusGrammar({}, {start});
+
+  ASSERT_NO_THROW(g.addRules(start, {d_solver.mkBoolean(false)}));
+
+  ASSERT_THROW(g.addRules(nullTerm, {d_solver.mkBoolean(false)}),
+               CVC4ApiException);
+  ASSERT_THROW(g.addRules(start, {nullTerm}), CVC4ApiException);
+  ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC4ApiException);
+  ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC4ApiException);
+
+  d_solver.synthFun("f", {}, boolean, g);
+
+  ASSERT_THROW(g.addRules(start, {d_solver.mkBoolean(false)}),
+               CVC4ApiException);
+}
+
+TEST_F(TestApiGrammarBlack, addAnyConstant)
+{
+  Sort boolean = d_solver.getBooleanSort();
+
+  Term nullTerm;
+  Term start = d_solver.mkVar(boolean);
+  Term nts = d_solver.mkVar(boolean);
+
+  Grammar g = d_solver.mkSygusGrammar({}, {start});
+
+  ASSERT_NO_THROW(g.addAnyConstant(start));
+  ASSERT_NO_THROW(g.addAnyConstant(start));
+
+  ASSERT_THROW(g.addAnyConstant(nullTerm), CVC4ApiException);
+  ASSERT_THROW(g.addAnyConstant(nts), CVC4ApiException);
+
+  d_solver.synthFun("f", {}, boolean, g);
+
+  ASSERT_THROW(g.addAnyConstant(start), CVC4ApiException);
+}
+
+TEST_F(TestApiGrammarBlack, addAnyVariable)
+{
+  Sort boolean = d_solver.getBooleanSort();
+
+  Term nullTerm;
+  Term x = d_solver.mkVar(boolean);
+  Term start = d_solver.mkVar(boolean);
+  Term nts = d_solver.mkVar(boolean);
+
+  Grammar g1 = d_solver.mkSygusGrammar({x}, {start});
+  Grammar g2 = d_solver.mkSygusGrammar({}, {start});
+
+  ASSERT_NO_THROW(g1.addAnyVariable(start));
+  ASSERT_NO_THROW(g1.addAnyVariable(start));
+  ASSERT_NO_THROW(g2.addAnyVariable(start));
+
+  ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC4ApiException);
+  ASSERT_THROW(g1.addAnyVariable(nts), CVC4ApiException);
+
+  d_solver.synthFun("f", {}, boolean, g1);
+
+  ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException);
+}

diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
deleted file mode 100644 (file)
index afbd09d..0000000
--- a/test/unit/api/grammar_black.h
+++ /dev/null
@@ -1,137 +0,0 @@
-/*********************                                                        */
-/*! \file grammar_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Abdalrhman Mohamed, 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 guards of the C++ API functions.
- **
- ** Black box testing of the guards of the C++ API functions.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-
-using namespace CVC4::api;
-
-class GrammarBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override;
-  void tearDown() override;
-
-  void testAddRule();
-  void testAddRules();
-  void testAddAnyConstant();
-  void testAddAnyVariable();
-
- private:
-  std::unique_ptr<Solver> d_solver;
-};
-
-void GrammarBlack::setUp() { d_solver.reset(new Solver()); }
-
-void GrammarBlack::tearDown() { d_solver.reset(nullptr); }
-
-void GrammarBlack::testAddRule()
-{
-  Sort boolean = d_solver->getBooleanSort();
-  Sort integer = d_solver->getIntegerSort();
-
-  Term nullTerm;
-  Term start = d_solver->mkVar(boolean);
-  Term nts = d_solver->mkVar(boolean);
-
-  Grammar g = d_solver->mkSygusGrammar({}, {start});
-
-  TS_ASSERT_THROWS_NOTHING(g.addRule(start, d_solver->mkBoolean(false)));
-
-  TS_ASSERT_THROWS(g.addRule(nullTerm, d_solver->mkBoolean(false)),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRule(start, nullTerm), CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRule(nts, d_solver->mkBoolean(false)),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkInteger(0)), CVC4ApiException&);
-
-  d_solver->synthFun("f", {}, boolean, g);
-
-  TS_ASSERT_THROWS(g.addRule(start, d_solver->mkBoolean(false)),
-                   CVC4ApiException&);
-}
-
-void GrammarBlack::testAddRules()
-{
-  Sort boolean = d_solver->getBooleanSort();
-  Sort integer = d_solver->getIntegerSort();
-
-  Term nullTerm;
-  Term start = d_solver->mkVar(boolean);
-  Term nts = d_solver->mkVar(boolean);
-
-  Grammar g = d_solver->mkSygusGrammar({}, {start});
-
-  TS_ASSERT_THROWS_NOTHING(g.addRules(start, {d_solver->mkBoolean(false)}));
-
-  TS_ASSERT_THROWS(g.addRules(nullTerm, {d_solver->mkBoolean(false)}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRules(start, {nullTerm}), CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRules(nts, {d_solver->mkBoolean(false)}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkInteger(0)}), CVC4ApiException&);
-
-  d_solver->synthFun("f", {}, boolean, g);
-
-  TS_ASSERT_THROWS(g.addRules(start, {d_solver->mkBoolean(false)}),
-                   CVC4ApiException&);
-}
-
-void GrammarBlack::testAddAnyConstant()
-{
-  Sort boolean = d_solver->getBooleanSort();
-
-  Term nullTerm;
-  Term start = d_solver->mkVar(boolean);
-  Term nts = d_solver->mkVar(boolean);
-
-  Grammar g = d_solver->mkSygusGrammar({}, {start});
-
-  TS_ASSERT_THROWS_NOTHING(g.addAnyConstant(start));
-  TS_ASSERT_THROWS_NOTHING(g.addAnyConstant(start));
-
-  TS_ASSERT_THROWS(g.addAnyConstant(nullTerm), CVC4ApiException&);
-  TS_ASSERT_THROWS(g.addAnyConstant(nts), CVC4ApiException&);
-
-  d_solver->synthFun("f", {}, boolean, g);
-
-  TS_ASSERT_THROWS(g.addAnyConstant(start), CVC4ApiException&);
-}
-
-void GrammarBlack::testAddAnyVariable()
-{
-  Sort boolean = d_solver->getBooleanSort();
-
-  Term nullTerm;
-  Term x = d_solver->mkVar(boolean);
-  Term start = d_solver->mkVar(boolean);
-  Term nts = d_solver->mkVar(boolean);
-
-  Grammar g1 = d_solver->mkSygusGrammar({x}, {start});
-  Grammar g2 = d_solver->mkSygusGrammar({}, {start});
-
-  TS_ASSERT_THROWS_NOTHING(g1.addAnyVariable(start));
-  TS_ASSERT_THROWS_NOTHING(g1.addAnyVariable(start));
-  TS_ASSERT_THROWS_NOTHING(g2.addAnyVariable(start));
-
-  TS_ASSERT_THROWS(g1.addAnyVariable(nullTerm), CVC4ApiException&);
-  TS_ASSERT_THROWS(g1.addAnyVariable(nts), CVC4ApiException&);
-
-  d_solver->synthFun("f", {}, boolean, g1);
-
-  TS_ASSERT_THROWS(g1.addAnyVariable(start), CVC4ApiException&);
-}