From d96815ffdd4ee0bf9422b7f0194a23a0a42462c3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 3 Jan 2019 14:48:18 -0800 Subject: API/Smt2 parser: refactor termAtomic (#2674) --- test/unit/api/CMakeLists.txt | 3 +- test/unit/api/datatype_api_black.h | 57 ++++++++++++++++++++++++++++++++ test/unit/api/solver_black.h | 67 ++++++++++++++++++++++++++++++++++---- 3 files changed, 119 insertions(+), 8 deletions(-) create mode 100644 test/unit/api/datatype_api_black.h (limited to 'test') diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 8a6be70b9..ca3c59750 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -1,7 +1,8 @@ #-----------------------------------------------------------------------------# # Add unit tests +cvc4_add_unit_test_black(datatype_api_black api) +cvc4_add_unit_test_black(opterm_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) -cvc4_add_unit_test_black(opterm_black api) diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h new file mode 100644 index 000000000..bca6a35ce --- /dev/null +++ b/test/unit/api/datatype_api_black.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file datatype_api_black.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 datatype classes of the C++ API. + ** + ** Black box testing of the datatype classes of the C++ API. + **/ + +#include + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class DatatypeBlack : public CxxTest::TestSuite +{ + public: + void setUp() override; + void tearDown() override; + + void testMkDatatypeSort(); + + private: + Solver d_solver; +}; + +void DatatypeBlack::setUp() {} + +void DatatypeBlack::tearDown() {} + +void DatatypeBlack::testMkDatatypeSort() +{ + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype d = listSort.getDatatype(); + DatatypeConstructor consConstr = d[0]; + DatatypeConstructor nilConstr = d[1]; + TS_ASSERT_THROWS(d[2], CVC4ApiException&); + TS_ASSERT(consConstr.isResolved()); + TS_ASSERT(nilConstr.isResolved()); + TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm()); + TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); +} diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index d4082163a..76388d48f 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file api_guards_black.h +/*! \file solver_black.h ** \verbatim ** Top contributors (to current version): ** Aina Niemetz @@ -9,9 +9,9 @@ ** 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. + ** \brief Black box testing of the Solver class of the C++ API. ** - ** Black box testing of the guards of the C++ API functions. + ** Black box testing of the Solver class of the C++ API. **/ #include @@ -29,10 +29,11 @@ class SolverBlack : public CxxTest::TestSuite void testGetBooleanSort(); void testGetIntegerSort(); + void testGetNullSort(); void testGetRealSort(); void testGetRegExpSort(); - void testGetStringSort(); void testGetRoundingmodeSort(); + void testGetStringSort(); void testMkArraySort(); void testMkBitVectorSort(); @@ -49,20 +50,22 @@ class SolverBlack : public CxxTest::TestSuite void testMkUninterpretedSort(); void testMkBitVector(); - void testMkBoundVar(); void testMkBoolean(); + void testMkBoundVar(); void testMkConst(); void testMkEmptySet(); void testMkFalse(); + void testMkFloatingPoint(); void testMkPi(); void testMkReal(); void testMkRegexpEmpty(); void testMkRegexpSigma(); void testMkSepNil(); void testMkString(); - void testMkUniverseSet(); void testMkTerm(); void testMkTrue(); + void testMkTuple(); + void testMkUniverseSet(); void testMkVar(); void testDeclareFun(); @@ -88,6 +91,11 @@ void SolverBlack::testGetIntegerSort() TS_ASSERT_THROWS_NOTHING(d_solver.getIntegerSort()); } +void SolverBlack::testGetNullSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getNullSort()); +} + void SolverBlack::testGetRealSort() { TS_ASSERT_THROWS_NOTHING(d_solver.getRealSort()); @@ -248,6 +256,10 @@ void SolverBlack::testMkBitVector() TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector(size2, val2)); TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector("1010", 2)); TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVector("1010", 16)); + TS_ASSERT_THROWS(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException&); + TS_ASSERT_EQUALS(d_solver.mkBitVector(8, "01010101", 2).toString(), + "0bin01010101"); + TS_ASSERT_EQUALS(d_solver.mkBitVector(8, "F", 16).toString(), "0bin00001111"); } void SolverBlack::testMkBoundVar() @@ -411,6 +423,26 @@ void SolverBlack::testMkFalse() TS_ASSERT_THROWS_NOTHING(d_solver.mkFalse()); } +void SolverBlack::testMkFloatingPoint() +{ + if (CVC4::Configuration::isBuiltWithSymFPU()) + { + TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkNegInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkNaN(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkPosInf(3, 5)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkNegZero(3, 5)); + } + else + { + TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkNegInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkNaN(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkPosInf(3, 5), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkNegZero(3, 5), CVC4ApiException&); + } +} + void SolverBlack::testMkOpTerm() { // mkOpTerm(Kind kind, Kind k) @@ -507,6 +539,10 @@ void SolverBlack::testMkString() { TS_ASSERT_THROWS_NOTHING(d_solver.mkString("")); TS_ASSERT_THROWS_NOTHING(d_solver.mkString("asdfasdf")); + TS_ASSERT_EQUALS(d_solver.mkString("asdf\\nasdf").toString(), + "\"asdf\\\\nasdf\""); + TS_ASSERT_EQUALS(d_solver.mkString("asdf\\nasdf", true).toString(), + "\"asdf\\nasdf\""); } void SolverBlack::testMkTerm() @@ -599,10 +635,27 @@ void SolverBlack::testMkTrue() TS_ASSERT_THROWS_NOTHING(d_solver.mkTrue()); } +void SolverBlack::testMkTuple() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkTuple({d_solver.mkBitVectorSort(3)}, + {d_solver.mkBitVector("101", 2)})); + TS_ASSERT_THROWS_NOTHING( + d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkReal("5")})); + + TS_ASSERT_THROWS(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkTuple({d_solver.mkBitVectorSort(4)}, + {d_solver.mkBitVector("101", 2)}), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}), + CVC4ApiException&); +} + void SolverBlack::testMkUniverseSet() { TS_ASSERT_THROWS(d_solver.mkUniverseSet(Sort()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver.mkUniverseSet(d_solver.getBooleanSort())); } void SolverBlack::testMkVar() -- cgit v1.2.3