diff options
Diffstat (limited to 'test/unit')
100 files changed, 1431 insertions, 1434 deletions
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 93ca679f3..e99d92303 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Aina Niemetz, Mathias Preiner, Gereon Kremer -## 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, Mathias Preiner, Gereon Kremer +# +# 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. ## + find_package(GTest REQUIRED) include(GoogleTest) 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" diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt index 4530c0711..65d352c0b 100644 --- a/test/unit/base/CMakeLists.txt +++ b/test/unit/base/CMakeLists.txt @@ -1,14 +1,17 @@ -##################### -## CMakeLists.txt -## 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_black(map_util_black base) diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp index 3ba866f30..1b5565c1b 100644 --- a/test/unit/base/map_util_black.cpp +++ b/test/unit/base/map_util_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file map_util_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King - ** 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 map utility functions. - ** - ** Black box testing of map utility functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King + * + * 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 map utility functions. + */ #include <map> #include <set> diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index 9bf07e13c..e5a8caf0f 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -1,16 +1,19 @@ -##################### -## CMakeLists.txt -## 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_black(cdlist_black context) cvc4_add_unit_test_black(cdhashmap_black context) cvc4_add_unit_test_white(cdhashmap_white context) diff --git a/test/unit/context/cdhashmap_black.cpp b/test/unit/context/cdhashmap_black.cpp index fbeae85b5..c4d744914 100644 --- a/test/unit/context/cdhashmap_black.cpp +++ b/test/unit/context/cdhashmap_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdmap_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters - ** 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 cvc5::context::CDMap<>. - ** - ** Black box testing of cvc5::context::CDMap<>. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters + * + * 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 cvc5::context::CDMap<>. + */ #include <map> diff --git a/test/unit/context/cdhashmap_white.cpp b/test/unit/context/cdhashmap_white.cpp index 72e437250..d45c58731 100644 --- a/test/unit/context/cdhashmap_white.cpp +++ b/test/unit/context/cdhashmap_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdmap_white.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 White box testing of cvc5::context::CDMap<>. - ** - ** White box testing of cvc5::context::CDMap<>. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * White box testing of cvc5::context::CDMap<>. + */ #include "base/check.h" #include "context/cdhashmap.h" diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp index c944b0722..57c25a2b3 100644 --- a/test/unit/context/cdlist_black.cpp +++ b/test/unit/context/cdlist_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdlist_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters - ** 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 cvc5::context::CDList<>. - ** - ** Black box testing of cvc5::context::CDList<>. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters + * + * 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 cvc5::context::CDList<>. + */ #include <limits.h> diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp index c4e9b8dd5..64b6c0700 100644 --- a/test/unit/context/cdo_black.cpp +++ b/test/unit/context/cdo_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdo_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Dejan Jovanovic, 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 cvc5::context::CDO<>. - ** - ** Black box testing of cvc5::context::CDO<>. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Dejan Jovanovic, 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 cvc5::context::CDO<>. + */ #include <iostream> #include <vector> diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp index ee5140da3..316aa7d46 100644 --- a/test/unit/context/context_black.cpp +++ b/test/unit/context/context_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file context_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, Dejan Jovanovic - ** 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 cvc5::context::Context. - ** - ** Black box testing of cvc5::context::Context. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, Dejan Jovanovic + * + * 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 cvc5::context::Context. + */ #include <iostream> #include <vector> diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp index 22b15d70d..d35166193 100644 --- a/test/unit/context/context_mm_black.cpp +++ b/test/unit/context/context_mm_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file context_mm_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Dejan Jovanovic, 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 cvc5::context::ContextMemoryManager. - ** - ** Black box testing of cvc5::context::ContextMemoryManager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Dejan Jovanovic, 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 cvc5::context::ContextMemoryManager. + */ #include <cstring> #include <iostream> diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp index 7bda5d2da..b82fae5dd 100644 --- a/test/unit/context/context_white.cpp +++ b/test/unit/context/context_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file context_white.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 White box testing of cvc5::context::Context. - ** - ** White box testing of cvc5::context::Context. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * White box testing of cvc5::context::Context. + */ #include "base/check.h" #include "context/cdo.h" diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt index 6cdf48cb4..36c4cfb48 100644 --- a/test/unit/main/CMakeLists.txt +++ b/test/unit/main/CMakeLists.txt @@ -1,14 +1,17 @@ -##################### -## CMakeLists.txt -## 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_black(interactive_shell_black main) diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index 52f07a2f2..71ad2b1f4 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file interactive_shell_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Christopher L. Conway, 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 cvc5::InteractiveShell. - ** - ** Black box testing of cvc5::InteractiveShell. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Christopher L. Conway, 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 cvc5::InteractiveShell. + */ #include <sstream> #include <vector> diff --git a/test/unit/memory.h b/test/unit/memory.h index 45c65c202..68982077c 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -1,31 +1,27 @@ -/********************* */ -/*! \file memory.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, 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 Utility class to help testing out-of-memory conditions. - ** - ** Utility class to help testing out-of-memory conditions. - ** - ** Use it like this (for example): - ** - ** cvc5::test::WithLimitedMemory wlm(amount); - ** TS_ASSERT_THROWS( foo(), bad_alloc ); - ** - ** The WithLimitedMemory destructor will re-establish the previous limit. - ** - ** This class does not exist in CVC5_MEMORY_LIMITING_DISABLED is defined. - ** This can be disabled for a variety of reasons. - ** If this is disabled, there will be a function: - ** void WarnWithLimitedMemoryDisabledReason() - ** uses TS_WARN to alert users that these tests are disabled. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Morgan Deters, 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. + * **************************************************************************** + * + * Utility class to help testing out-of-memory conditions. + * + * Use it like this (for example): + * + * cvc5::test::WithLimitedMemory wlm(amount); + * ASSERT_THROW( foo(), bad_alloc ); + * + * The WithLimitedMemory destructor will re-establish the previous limit. + * + * This class does not exist in CVC4_MEMORY_LIMITING_DISABLED is defined. + * This can be disabled for a variety of reasons. + */ #include "test.h" diff --git a/test/unit/node/CMakeLists.txt b/test/unit/node/CMakeLists.txt index 52e591aeb..5f4c3458c 100644 --- a/test/unit/node/CMakeLists.txt +++ b/test/unit/node/CMakeLists.txt @@ -1,16 +1,19 @@ -##################### -## CMakeLists.txt -## 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_black(attribute_black expr) cvc4_add_unit_test_white(attribute_white expr) cvc4_add_unit_test_black(kind_black expr) diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp index 0ec1c5e56..ff3aa04d9 100644 --- a/test/unit/node/attribute_black.cpp +++ b/test/unit/node/attribute_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file attribute_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Morgan Deters - ** 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 cvc5::Attribute. - ** - ** Black box testing of cvc5::Attribute. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, 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 cvc5::Attribute. + */ #include <sstream> #include <vector> diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp index 59d9500c7..fe74130d1 100644 --- a/test/unit/node/attribute_white.cpp +++ b/test/unit/node/attribute_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file attribute_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters - ** 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 Node attributes. - ** - ** White box testing of Node attributes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters + * + * 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 Node attributes. + */ #include <string> diff --git a/test/unit/node/kind_black.cpp b/test/unit/node/kind_black.cpp index defc3aa6f..a0253b728 100644 --- a/test/unit/node/kind_black.cpp +++ b/test/unit/node/kind_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file kind_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 cvc5::Kind. - ** - ** Black box testing of cvc5::Kind. - **/ +/****************************************************************************** + * 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 cvc5::Kind. + */ #include <iostream> #include <sstream> diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp index 428da7206..6cc3197d2 100644 --- a/test/unit/node/kind_map_black.cpp +++ b/test/unit/node/kind_map_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file kind_map_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Gereon Kremer - ** 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 cvc5::KindMap - ** - ** Black box testing of cvc5::KindMap. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Gereon Kremer + * + * 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 cvc5::KindMap. + */ #include <iostream> #include <sstream> diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index 1a739cf1b..6b8c27c17 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_algorithm_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed - ** 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 utility functions in node_algorithm.{h,cpp} - ** - ** Black box testing of node_algorithm.{h,cpp} - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Yoni Zohar, 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 node_algorithm.{h,cpp} + */ #include <string> #include <vector> diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index b63541d6c..94eb3ae83 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, 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 cvc5::Node. - ** - ** Black box testing of cvc5::Node. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Morgan Deters + * + * 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 cvc5::Node. + */ #include <algorithm> #include <sstream> diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index fbf2b9108..fc8b6fb7b 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_builder_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Morgan Deters - ** 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 cvc5::NodeBuilder. - ** - ** Black box testing of cvc5::NodeBuilder. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, 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 cvc5::NodeBuilder. + */ #include <limits.h> diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index a2d25c8d8..7d9d3b556 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_manager_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Christopher L. Conway, Dejan Jovanovic - ** 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 cvc5::NodeManager. - ** - ** Black box testing of cvc5::NodeManager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Dejan Jovanovic, 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 cvc5::NodeManager. + */ #include <string> #include <vector> diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index 986eac870..fe06f85d3 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_manager_white.cpp - ** \verbatim - ** 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.\endverbatim - ** - ** \brief White box testing of cvc5::NodeManager. - ** - ** White box testing of cvc5::NodeManager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, 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 cvc5::NodeManager. + */ #include <string> diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp index fa4889540..66696b71e 100644 --- a/test/unit/node/node_self_iterator_black.cpp +++ b/test/unit/node/node_self_iterator_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_self_iterator_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Morgan Deters - ** 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 cvc5::expr::NodeSelfIterator - ** - ** Black box testing of cvc5::expr::NodeSelfIterator - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Tim King + * + * 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 cvc5::expr::NodeSelfIterator. + */ #include "expr/node.h" #include "expr/node_builder.h" diff --git a/test/unit/node/node_traversal_black.cpp b/test/unit/node/node_traversal_black.cpp index 8366b1a63..b8e68c91b 100644 --- a/test/unit/node/node_traversal_black.cpp +++ b/test/unit/node/node_traversal_black.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file node_traversal_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Alex Ozdemir, 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 node traversal iterators. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Alex Ozdemir, 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 node traversal iterators. + */ #include <algorithm> #include <cstddef> diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index 9e3c4bb7d..bf0b8db57 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_white.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 White box testing of cvc5::Node. - ** - ** White box testing of cvc5::Node. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * White box testing of cvc5::Node. + */ #include <string> diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp index 7b01b520d..baae33694 100644 --- a/test/unit/node/symbol_table_black.cpp +++ b/test/unit/node/symbol_table_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file symbol_table_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, Christopher L. Conway - ** 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 cvc5::SymbolTable - ** - ** Black box testing of cvc5::SymbolTable. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, Christopher L. Conway + * + * 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 cvc5::SymbolTable. + */ #include <sstream> #include <string> diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp index f0ee99a7d..21e87c5c2 100644 --- a/test/unit/node/type_cardinality_black.cpp +++ b/test/unit/node/type_cardinality_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_cardinality_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters - ** 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 Public box testing of Type::getCardinality() for various Types - ** - ** Public box testing of Type::getCardinality() for various Types. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters + * + * 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. + * **************************************************************************** + * + * Public box testing of Type::getCardinality() for various Types. + */ #include <string> diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index c6f862e03..4fb057fa9 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_node_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 TypeNode - ** - ** White box testing of TypeNode. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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 TypeNode. + */ #include <iostream> #include <sstream> diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt index 216dcdd0f..0044a1d97 100644 --- a/test/unit/parser/CMakeLists.txt +++ b/test/unit/parser/CMakeLists.txt @@ -1,15 +1,18 @@ -##################### -## CMakeLists.txt -## 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_black(parser_black parser) -cvc4_add_unit_test_black(parser_builder_black parser)
\ No newline at end of file +cvc4_add_unit_test_black(parser_builder_black parser) diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 27d008228..1e8e210ca 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -1,19 +1,17 @@ -/********************* */ -/*! \file parser_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Christopher L. Conway, Morgan Deters - ** 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 cvc5::parser::Parser for CVC and SMT-LIBv2 - ** inputs. - ** - ** Black box testing of cvc5::parser::Parser for CVC and SMT-LIbv2 inputs. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Christopher L. Conway, Morgan Deters + * + * 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 cvc5::parser::Parser for CVC and SMT-LIbv2 inputs. + */ #include <sstream> diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index 113a5abd5..b8c12eee2 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file parser_builder_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Christopher L. Conway, Tim King - ** 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 cvc5::parser::ParserBuilder. - ** - ** Black box testing of cvc5::parser::ParserBuilder. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Christopher L. Conway, Tim King + * + * 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 cvc5::parser::ParserBuilder. + */ #include <stdio.h> #include <string.h> diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt index 023b8623d..c16cb07fc 100644 --- a/test/unit/preprocessing/CMakeLists.txt +++ b/test/unit/preprocessing/CMakeLists.txt @@ -1,15 +1,18 @@ -##################### -## CMakeLists.txt -## 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing) -cvc4_add_unit_test_white(pass_foreign_theory_rewrite_white preprocessing)
\ No newline at end of file +cvc4_add_unit_test_white(pass_foreign_theory_rewrite_white preprocessing) diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 6f0398439..5905f8404 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file pass_bv_gauss_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, 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 Unit tests for Gaussian Elimination preprocessing pass. - ** - ** Unit tests for Gaussian Elimination preprocessing pass. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mathias Preiner, 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. + * **************************************************************************** + * + * Unit tests for Gaussian Elimination preprocessing pass. + */ #include <iostream> #include <vector> diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index 662a53777..64b93b3db 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -1,17 +1,17 @@ -/********************* */ -/*! \file pass_foreign_theory_rewrite_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, 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 Unit tests for Foreign Theory Rerwrite prepricessing pass - ** Unit tests for Foreign Theory Rerwrite prepricessing pass - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Yoni Zohar + * + * 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. + * **************************************************************************** + * + * Unit tests for Foreign Theory Rerwrite prepricessing pass. + */ #include "expr/node_manager.h" #include "preprocessing/passes/foreign_theory_rewrite.h" diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt index b142d6fab..7cec81221 100644 --- a/test/unit/printer/CMakeLists.txt +++ b/test/unit/printer/CMakeLists.txt @@ -1,14 +1,17 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Andres Noetzli, 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_black(smt2_printer_black printer) diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index d89930033..a80b27ace 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt2_printer_black.cpp - ** \verbatim - ** 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.\endverbatim - ** - ** \brief Black box testing of the SMT2 printer - ** - ** Black box testing of the SMT2 printer. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Black box testing of the SMT2 printer. + */ #include <iostream> diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt index 650bbeef0..8e93c14f9 100644 --- a/test/unit/prop/CMakeLists.txt +++ b/test/unit/prop/CMakeLists.txt @@ -1,14 +1,17 @@ -##################### -## CMakeLists.txt -## 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. +############################################################################### +# 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. +# ############################################################################# +# +# The build system configuration. ## -#-----------------------------------------------------------------------------# -# Add unit tests +# Add unit tests. cvc4_add_unit_test_white(cnf_stream_white prop) diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp index 0529f209c..4dfd7a1bb 100644 --- a/test/unit/prop/cnf_stream_white.cpp +++ b/test/unit/prop/cnf_stream_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cnf_stream_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Christopher L. Conway, 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 White box testing of cvc5::prop::CnfStream. - ** - ** White box testing of cvc5::prop::CnfStream. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Christopher L. Conway, 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. + * **************************************************************************** + * + * White box testing of cvc5::prop::CnfStream. + */ #include "base/check.h" #include "context/context.h" diff --git a/test/unit/test.h b/test/unit/test.h index 383360302..d7035efcd 100644 --- a/test/unit/test.h +++ b/test/unit/test.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file test.h - ** \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 Common header for API unit test. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Common header for API unit test. + */ #ifndef CVC5__TEST__UNIT__TEST_H #define CVC5__TEST__UNIT__TEST_H diff --git a/test/unit/test_api.h b/test/unit/test_api.h index be0ef46d0..533bdaaa2 100644 --- a/test/unit/test_api.h +++ b/test/unit/test_api.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file test_api.h - ** \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 Common header for API unit test. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Common header for API unit test. + */ #ifndef CVC5__TEST__UNIT__TEST_API_H #define CVC5__TEST__UNIT__TEST_API_H diff --git a/test/unit/test_context.h b/test/unit/test_context.h index 3ab333806..b034aaa2e 100644 --- a/test/unit/test_context.h +++ b/test/unit/test_context.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file test_context.h - ** \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 Header for context unit tests. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Header for context unit tests. + */ #ifndef CVC5__TEST__UNIT__TEST_CONTEXT_H #define CVC5__TEST__UNIT__TEST_CONTEXT_H diff --git a/test/unit/test_node.h b/test/unit/test_node.h index ff6ef9b09..4250bb7da 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file test_node.h - ** \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 Common header for Node unit tests. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Common header for Node unit tests. + */ #ifndef CVC5__TEST__UNIT__TEST_NODE_H #define CVC5__TEST__UNIT__TEST_NODE_H diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 4307fd1ba..3c19a8c03 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file test_smt.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Morgan Deters - ** 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 Common header for unit tests that need an SmtEngine. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Haniel Barbosa + * + * 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. + * **************************************************************************** + * + * Common header for unit tests that need an SmtEngine. + */ #ifndef CVC5__TEST__UNIT__TEST_SMT_H #define CVC5__TEST__UNIT__TEST_SMT_H diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index fef2bdd38..75dd8c32c 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -1,13 +1,19 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Aina Niemetz, Michael Chang -## 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, Yoni Zohar, Yancheng Ou +# +# 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. cvc4_add_unit_test_black(regexp_operation_black theory) cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index 2afaf3a48..25ffa0572 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file evaluator_white.cpp - ** \verbatim - ** 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.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <vector> diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index 5c18b7c98..e51929cad 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file logic_info_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, 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 Unit testing for cvc5::LogicInfo class - ** - ** Unit testing for cvc5::LogicInfo class. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, 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. + * **************************************************************************** + * + * Unit testing for cvc5::LogicInfo class. + */ #include "base/configuration.h" #include "expr/kind.h" diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index 608eeb649..6ba942b6b 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file regexp_operation_black.cpp - ** \verbatim - ** 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.\endverbatim - ** - ** \brief Unit tests for symbolic regular expression operations - ** - ** Unit tests for symbolic regular expression operations. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Unit tests for symbolic regular expression operations. + */ #include <iostream> #include <memory> diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index f66a87a83..02472e71e 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file sequences_rewriter_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andres Noetzli, 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 Unit tests for the strings/sequences rewriter - ** - ** Unit tests for the strings/sequences rewriter. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, 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. + * **************************************************************************** + * + * Unit tests for the strings/sequences rewriter. + */ #include <iostream> #include <memory> diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index 13ee14306..bc6f400c0 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file strings_rewriter_white.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 Unit tests for the strings rewriter - ** - ** Unit tests for the strings rewriter. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Unit tests for the strings rewriter. + */ #include <iostream> #include <memory> diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 27ce7158a..4132be8df 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_arith_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Dejan Jovanovic - ** 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 Whitebox tests for theory Arithmetic. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Whitebox tests for theory Arithmetic. + */ #include <list> #include <vector> diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 88a1412a7..88808c018 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags_normal_form_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mudathir Mohamed - ** 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 bags normal form - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mudathir 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. + * **************************************************************************** + * + * White box testing of bags normal form + */ #include "expr/dtype.h" #include "test_smt.h" diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 10a606d11..6828e8cdf 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags_rewriter_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mudathir Mohamed - ** 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 bags rewriter - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * White box testing of bags rewriter + */ #include "expr/dtype.h" #include "test_smt.h" diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 2948c2e9e..4d8270ec6 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags_type_rules_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mudathir Mohamed - ** 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 bags typing rules - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mudathir 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 bags typing rules + */ #include "expr/dtype.h" #include "test_smt.h" diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index de3cdaf4d..db4a1e046 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_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 cvc5::theory - ** - ** Black box testing of cvc5::theory - **/ +/****************************************************************************** + * 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 cvc5::theory. + */ #include <sstream> #include <vector> diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index df1c3755b..ff08a2024 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_bv_rewriter_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Unit tests for bit-vector solving via integers - ** - ** Unit tests for bit-vector solving via integers. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * 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. + * **************************************************************************** + * + * Unit tests for bit-vector solving via integers. + */ #include <iostream> #include <memory> diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index fde7a5e2e..386f5b8f8 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bv_opt_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yancheng Ou - ** 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 for optimization module for BitVectors. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yancheng Ou, Michael Chang + * + * 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 for optimization module for BitVectors. + */ #include <iostream> #include "smt/optimization_solver.h" diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp index e0c2dad04..5ea8fa4dd 100644 --- a/test/unit/theory/theory_bv_rewriter_white.cpp +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_bv_rewriter_white.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 Unit tests for the bit-vector rewriter - ** - ** Unit tests for the bit-vector rewriter. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Unit tests for the bit-vector rewriter. + */ #include <iostream> #include <memory> diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index bcd91f9b8..bfdcfb604 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file theory_bv_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Abdalrhman Mohamed, Mathias Preiner - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Abdalrhman Mohamed, 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <vector> diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index 57741b98d..dd3426973 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -1,22 +1,22 @@ -/********************* */ -/*! \file theory_engine_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, 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 White box testing of cvc5::theory::Theory. - ** - ** White box testing of cvc5::theory::Theory. This test creates - ** "fake" theory interfaces and injects them into TheoryEngine, so we - ** can test TheoryEngine's behavior without relying on independent - ** theory behavior. This is done in TheoryEngineWhite::setUp() by - ** means of the TheoryEngineWhite::registerTheory() interface. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, 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. + * **************************************************************************** + * + * White box testing of cvc5::theory::Theory. + * + * This test creates "fake" theory interfaces and injects them into + * TheoryEngine, so we can test TheoryEngine's behavior without relying on + * independent theory behavior. This is done in TheoryEngineWhite::setUp() by + * means of the TheoryEngineWhite::registerTheory() interface. + */ #include <memory> #include <string> diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index feab15b2b..e8daef819 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_int_opt_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Michael Chang, Yancheng Ou - ** 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 for optimization module for Integers. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Michael Chang, Yancheng Ou + * + * 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 for optimization module for Integers. + */ #include <iostream> #include "smt/optimization_solver.h" diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp index 19968cbdd..211552590 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_quantifiers_bv_instantiator_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, 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 Unit tests for BvInstantiator. - ** - ** Unit tests for BvInstantiator. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mathias Preiner, 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. + * **************************************************************************** + * + * Unit tests for BvInstantiator. + */ #include <iostream> #include <vector> diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 92e76d5f5..83d982d8e 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_quantifiers_bv_inverter_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Abdalrhman Mohamed - ** 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 Unit tests for BV inverter. - ** - ** Unit tests for BV inverter. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mathias Preiner, 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. + * **************************************************************************** + * + * Unit tests for BV inverter. + */ #include "expr/node.h" #include "test_smt.h" diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp index f20cf50d2..ecef0773b 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.cpp +++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp @@ -1,21 +1,20 @@ -/********************* */ -/*! \file theory_sets_type_enumerator_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Mudathir Mohamed - ** 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 cvc5::theory::sets::SetsTypeEnumerator - ** - ** White box testing of cvc5::theory::sets::SetsTypeEnumerator. (These tests - ** depends on the ordering that the SetsTypeEnumerator use, so it's a - *white-box - ** test.) - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Mudathir 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. + * **************************************************************************** + * + * White box testing of cvc5::theory::sets::SetsTypeEnumerator + * + * These tests depend on the ordering that the SetsTypeEnumerator use, so + * it's a white-box test. + */ #include "expr/dtype.h" #include "test_smt.h" diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index 899a75ae9..d75e5881d 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_sets_type_rules_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mudathir Mohamed - ** 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 sets typing rules - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mudathir 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. + * **************************************************************************** + * + * White box testing of sets typing rules + */ #include "expr/dtype.h" #include "test_api.h" diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index 920075674..24cbd166e 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_strings_skolem_cache_black.cpp - ** \verbatim - ** 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.\endverbatim - ** - ** \brief Black box testing of the skolem cache of the theory of strings. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, 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 skolem cache of the theory of strings. + */ #include <memory> diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp index 1ea73c0cc..9119cf1af 100644 --- a/test/unit/theory/theory_strings_word_white.cpp +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_strings_word_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Unit tests for the strings word utilities - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Unit tests for the strings word utilities + */ #include <iostream> #include <memory> diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index cb6e5ebfe..5a469ed97 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Dejan Jovanovic - ** 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 cvc5::theory::Theory. - ** - ** Black box testing of cvc5::theory::Theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Dejan Jovanovic + * + * 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 cvc5::theory::Theory. + */ #include <memory> #include <vector> diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index 6cab15b27..ab77a74ce 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file type_enumerator_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Morgan Deters - ** 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 cvc5::theory::TypeEnumerator - ** - ** White box testing of cvc5::theory::TypeEnumerator. (These tests depends - ** on the ordering that the TypeEnumerators use, so it's a white-box test.) - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Morgan Deters + * + * 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 cvc5::theory::TypeEnumerator. + * + * These tests depend on the ordering that the TypeEnumerators use, so it's a + * white-box test. + */ #include <unordered_set> diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index fc5484a1f..85cc04c94 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -1,16 +1,19 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Aina Niemetz, Yoni Zohar, Gereon Kremer -## 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, Yoni Zohar, Gereon Kremer +# +# 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_white(array_store_all_white util) cvc4_add_unit_test_white(assert_white util) cvc4_add_unit_test_black(binary_heap_black util) diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index b82807835..a33848610 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file array_store_all_white.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 cvc5::ArrayStoreAll - ** - ** Black box testing of cvc5::ArrayStoreAll. - **/ +/****************************************************************************** + * 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 cvc5::ArrayStoreAll. + */ #include "expr/array_store_all.h" #include "test_smt.h" diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp index 245ef8aaa..41a5621c4 100644 --- a/test/unit/util/assert_white.cpp +++ b/test/unit/util/assert_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file assert_white.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 White box testing of cvc5::Configuration. - ** - ** White box testing of cvc5::Configuration. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * White box testing of cvc5::Configuration. + */ #include <cstring> #include <string> diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp index 76462b687..acbf0871b 100644 --- a/test/unit/util/binary_heap_black.cpp +++ b/test/unit/util/binary_heap_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file binary_heap_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters - ** 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 cvc5::BinaryHeap - ** - ** Black box testing of cvc5::BinaryHeap. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters + * + * 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 cvc5::BinaryHeap. + */ #include <iostream> #include <sstream> diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp index 61dfa8101..2450747cd 100644 --- a/test/unit/util/bitvector_black.cpp +++ b/test/unit/util/bitvector_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file bitvector_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 cvc5::BitVector - ** - ** Black box testing of cvc5::BitVector. - **/ +/****************************************************************************** + * 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 cvc5::BitVector. + */ #include <sstream> diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index 1ec9c923c..4a3afb281 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file boolean_simplification_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, Tim King - ** 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 cvc5::BooleanSimplification - ** - ** Black box testing of cvc5::BooleanSimplification. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, 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 cvc5::BooleanSimplification. + */ #include <algorithm> #include <set> diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp index f4b2f3ac4..b19f88ae4 100644 --- a/test/unit/util/cardinality_black.cpp +++ b/test/unit/util/cardinality_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cardinality_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters - ** 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 Public-box testing of cvc5::Cardinality - ** - ** Public-box testing of cvc5::Cardinality. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters + * + * 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. + * **************************************************************************** + * + * Public-box testing of cvc5::Cardinality. + */ #include <sstream> #include <string> diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp index d517e4364..335c8c3b2 100644 --- a/test/unit/util/check_white.cpp +++ b/test/unit/util/check_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file check_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Mathias Preiner - ** 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 check utilities. - ** - ** White box testing of check utilities. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, 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. + * **************************************************************************** + * + * White box testing of check utilities. + */ #include <cstring> #include <string> diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp index 508aa179b..a651085c6 100644 --- a/test/unit/util/configuration_black.cpp +++ b/test/unit/util/configuration_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file configuration_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 cvc5::Configuration. - ** - ** Black box testing of cvc5::Configuration. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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 cvc5::Configuration. + */ #include "base/configuration.h" #include "test.h" diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 37cfe0cfa..3fd817e9d 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file datatype_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Morgan Deters - ** 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 cvc5::DType - ** - ** Black box testing of cvc5::DType. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Morgan Deters + * + * 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 cvc5::DType. + */ #include <sstream> diff --git a/test/unit/util/exception_black.cpp b/test/unit/util/exception_black.cpp index 2884dbfb8..1ebc94b75 100644 --- a/test/unit/util/exception_black.cpp +++ b/test/unit/util/exception_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file exception_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters - ** 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 cvc5::Exception. - ** - ** Black box testing of cvc5::Exception. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters + * + * 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 cvc5::Exception. + */ #include <iostream> #include <sstream> diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp index 0fe48928f..4bf01151a 100644 --- a/test/unit/util/floatingpoint_black.cpp +++ b/test/unit/util/floatingpoint_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file floatingpoint_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 cvc5::FloatingPoint. - ** - ** Black box testing of cvc5::FloatingPoint. - **/ +/****************************************************************************** + * 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 cvc5::FloatingPoint. + */ #include "test.h" #include "util/floatingpoint.h" diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp index 1a3e75256..368f12222 100644 --- a/test/unit/util/integer_black.cpp +++ b/test/unit/util/integer_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file integer_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King - ** 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 cvc5::Integer. - ** - ** Black box testing of cvc5::Integer. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King + * + * 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 cvc5::Integer. + */ #include <limits> #include <sstream> diff --git a/test/unit/util/integer_white.cpp b/test/unit/util/integer_white.cpp index 117f82195..a7582ba17 100644 --- a/test/unit/util/integer_white.cpp +++ b/test/unit/util/integer_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file integer_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King - ** 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 cvc5::Integer. - ** - ** White box testing of cvc5::Integer. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King + * + * 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 cvc5::Integer. + */ #include <sstream> diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp index 09991a6d0..8e9595009 100644 --- a/test/unit/util/output_black.cpp +++ b/test/unit/util/output_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file output_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, Tim King - ** 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 CVC4 output classes. - ** - ** Black box testing of CVC4 output classes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, 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 CVC4 output classes. + */ #include <iostream> #include <sstream> diff --git a/test/unit/util/rational_black.cpp b/test/unit/util/rational_black.cpp index d3b116d26..d117025a5 100644 --- a/test/unit/util/rational_black.cpp +++ b/test/unit/util/rational_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file rational_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 cvc5::Rational. - ** - ** Black box testing of cvc5::Rational. - **/ +/****************************************************************************** + * 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 cvc5::Rational. + */ #include <sstream> diff --git a/test/unit/util/rational_white.cpp b/test/unit/util/rational_white.cpp index c5b52e3c8..20740652e 100644 --- a/test/unit/util/rational_white.cpp +++ b/test/unit/util/rational_white.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file rational_white.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King - ** 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 cvc5::Rational. - ** - ** White box testing of cvc5::Rational. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King + * + * 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 cvc5::Rational. + */ #include <sstream> @@ -93,7 +92,7 @@ TEST_F(TestUtilWhiteRational, constructors) ASSERT_EQ(dz, qz.getDenominator()); // Not sure how to catch this... - // TS_ASSERT_THROWS(Rational div_0(0,0),__gmp_exception ); + // ASSERT_THROW(Rational div_0(0,0),__gmp_exception ); } TEST_F(TestUtilWhiteRational, destructor) diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp index c130023ca..8969091bd 100644 --- a/test/unit/util/real_algebraic_number_black.cpp +++ b/test/unit/util/real_algebraic_number_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file real_algebraic_number_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Gereon Kremer - ** 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 cvc5::RealAlgebraicNumber. - ** - ** Black box testing of cvc5::RealAlgebraicNumber. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Gereon Kremer + * + * 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 cvc5::RealAlgebraicNumber. + */ #include "test.h" #include "util/real_algebraic_number.h" diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp index c15b0cd47..d2df271d3 100644 --- a/test/unit/util/stats_black.cpp +++ b/test/unit/util/stats_black.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file stats_black.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Aina Niemetz, Gereon Kremer - ** 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 cvc5::Stat and associated classes - ** - ** Black box testing of cvc5::Stat and associated classes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, Gereon Kremer + * + * 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 cvc5::Stat and associated classes. + */ #include <fcntl.h> |