From: Aina Niemetz Date: Wed, 2 Dec 2020 17:13:34 +0000 (-0800) Subject: google test: api: Migrate grammar_black. (#5566) X-Git-Tag: cvc5-1.0.0~2523 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=95409c284cf683aaf12b68242b503c95241ac01e;p=cvc5.git google test: api: Migrate grammar_black. (#5566) --- 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 - -#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 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&); -}