summaryrefslogtreecommitdiff
path: root/test/unit/api
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/api')
-rw-r--r--test/unit/api/CMakeLists.txt25
-rw-r--r--test/unit/api/datatype_api_black.cpp29
-rw-r--r--test/unit/api/grammar_black.cpp29
-rw-r--r--test/unit/api/op_black.cpp27
-rw-r--r--test/unit/api/op_white.cpp27
-rw-r--r--test/unit/api/result_black.cpp27
-rw-r--r--test/unit/api/solver_black.cpp29
-rw-r--r--test/unit/api/solver_white.cpp29
-rw-r--r--test/unit/api/sort_black.cpp29
-rw-r--r--test/unit/api/term_black.cpp27
-rw-r--r--test/unit/api/term_white.cpp27
11 files changed, 154 insertions, 151 deletions
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 97564664a..899019b59 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -1,16 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-## Aina Niemetz, Andres Noetzli
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+# Aina Niemetz, Andres Noetzli
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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.
+# #############################################################################
+#
+# The build system configuration.
##
-#-----------------------------------------------------------------------------#
-# Add unit tests
+# Add unit tests.
cvc4_add_unit_test_black(datatype_api_black api)
cvc4_add_unit_test_black(grammar_black api)
cvc4_add_unit_test_black(op_black api)
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 190816921..7c85f84e0 100644
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -1,18 +1,17 @@
-/********************* */
-/*! \file datatype_api_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Aina Niemetz, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the datatype classes of the C++ API.
+ */
#include "test_api.h"
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index 9c1f750b8..ccab121db 100644
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -1,18 +1,17 @@
-/********************* */
-/*! \file grammar_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the guards of the C++ API functions.
+ */
#include "test_api.h"
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 0e6626ec5..0b67c0013 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -1,16 +1,17 @@
-/********************* */
-/*! \file op_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Makai Mann, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 Op class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Makai Mann, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Op class.
+ */
#include "test_api.h"
diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp
index 909aafcbb..4953cdd60 100644
--- a/test/unit/api/op_white.cpp
+++ b/test/unit/api/op_white.cpp
@@ -1,16 +1,17 @@
-/********************* */
-/*! \file op_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Makai Mann
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 White box testing of the Op class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Makai Mann
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * White box testing of the Op class.
+ */
#include "test_api.h"
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index ac4542c59..9bf6b8491 100644
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -1,16 +1,17 @@
-/********************* */
-/*! \file result_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Result class
+ */
#include "test_api.h"
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index fef06fa88..c5cdf4f8c 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1,18 +1,17 @@
-/********************* */
-/*! \file solver_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Mudathir Mohamed, Ying Sheng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 Solver class of the C++ API.
- **
- ** Black box testing of the Solver class of the C++ API.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Solver class of the C++ API.
+ */
#include "test_api.h"
diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/solver_white.cpp
index 25878f22d..5d7b9eacf 100644
--- a/test/unit/api/solver_white.cpp
+++ b/test/unit/api/solver_white.cpp
@@ -1,18 +1,17 @@
-/********************* */
-/*! \file solver_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Makai Mann, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 Solver class of the C++ API.
- **
- ** Black box testing of the Solver class of the C++ API.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Makai Mann, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Solver class of the C++ API.
+ */
#include "base/configuration.h"
#include "test_api.h"
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index fa4b1cc9d..8338ffa2c 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -1,18 +1,17 @@
-/********************* */
-/*! \file sort_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Andrew Reynolds, Yoni Zohar
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Andrew Reynolds, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the guards of the C++ API functions.
+ */
#include "test_api.h"
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 117b15394..d894f9720 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -1,16 +1,17 @@
-/********************* */
-/*! \file term_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Makai Mann, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 Term class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Makai Mann, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Term class.
+ */
#include "test_api.h"
diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp
index e7b7a9cd6..ace5645dc 100644
--- a/test/unit/api/term_white.cpp
+++ b/test/unit/api/term_white.cpp
@@ -1,16 +1,17 @@
-/********************* */
-/*! \file term_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Makai Mann, Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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 White box testing of the Term class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Makai Mann, Aina Niemetz, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * White box testing of the Term class.
+ */
#include "test_api.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback