summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2020-12-02 09:13:34 -0800
committerGitHub <noreply@github.com>2020-12-02 09:13:34 -0800
commit95409c284cf683aaf12b68242b503c95241ac01e (patch)
tree64068e82448c637fc61469661199e19e8a11d490
parent57b54a2eba7904652dfaf7e32b4eac8abd22c79b (diff)
google test: api: Migrate grammar_black. (#5566)
-rw-r--r--test/unit/api/CMakeLists.txt2
-rw-r--r--test/unit/api/grammar_black.cpp117
-rw-r--r--test/unit/api/grammar_black.h137
3 files changed, 118 insertions, 138 deletions
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index a8c696c00..b437146d9 100644
--- 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
index 000000000..2cfe67825
--- /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
index afbd09d0f..000000000
--- 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&);
-}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback