diff options
Diffstat (limited to 'src/util')
88 files changed, 1442 insertions, 1464 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 015a484d1..c7f7e780c 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Mathias Preiner, Gereon Kremer, 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): +# Mathias Preiner, Gereon Kremer, 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. ## + configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h) configure_file(floatingpoint_literal_symfpu_traits.h.in floatingpoint_literal_symfpu_traits.h) diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index 1f8802d22..556ce6eb0 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file abstract_value.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Representation of abstract values - ** - ** Representation of abstract values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, 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. + * **************************************************************************** + * + * Representation of abstract values. + */ #include "util/abstract_value.h" diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index f933cafdf..ff7a05764 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file abstract_value.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Representation of abstract values - ** - ** Representation of abstract values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * Representation of abstract values. + */ #include "cvc4_public.h" diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index 7df5aa36d..162725a72 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -1,22 +1,22 @@ -/********************* */ -/*! \file bin_heap.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, 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 An implementation of a binary heap - ** - ** An implementation of a binary heap. - ** Attempts to roughly follow the contract of Boost's d_ary_heap. - ** (http://www.boost.org/doc/libs/1_49_0/doc/html/boost/heap/d_ary_heap.html) - ** Also attempts to generalize ext/pd_bs/priority_queue. - ** (http://gcc.gnu.org/onlinedocs/libstdc++/ext/pb_ds/priority_queue.html) - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, 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. + * **************************************************************************** + * + * An implementation of a binary heap + * + * Attempts to roughly follow the contract of Boost's d_ary_heap. + * (http://www.boost.org/doc/libs/1_49_0/doc/html/boost/heap/d_ary_heap.html) + * Also attempts to generalize ext/pd_bs/priority_queue. + * (http://gcc.gnu.org/onlinedocs/libstdc++/ext/pb_ds/priority_queue.html) + */ #include "cvc4_private.h" diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 210d03891..848fc44f9 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -1,20 +1,17 @@ -/********************* */ -/*! \file bitvector.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Liana Hadarean, 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 A fixed-size bit-vector. - ** - ** A fixed-size bit-vector, implemented as a wrapper around Integer. - ** - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Liana Hadarean, 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. + * **************************************************************************** + * + * A fixed-size bit-vector, implemented as a wrapper around Integer. + */ #include "util/bitvector.h" @@ -79,7 +76,7 @@ unsigned BitVector::isPow2() const } /* ----------------------------------------------------------------------- - ** Operators + * Operators * ----------------------------------------------------------------------- */ /* String Operations ----------------------------------------------------- */ @@ -340,7 +337,7 @@ BitVector BitVector::arithRightShift(const BitVector& y) const } /* ----------------------------------------------------------------------- - ** Static helpers. + * Static helpers. * ----------------------------------------------------------------------- */ BitVector BitVector::mkZero(unsigned size) diff --git a/src/util/bitvector.h b/src/util/bitvector.h index c069949ef..09d75ffe8 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file bitvector.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andres Noetzli, 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 A fixed-size bit-vector. - ** - ** A fixed-size bit-vector, implemented as a wrapper around Integer. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, 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. + * **************************************************************************** + * + * A fixed-size bit-vector, implemented as a wrapper around Integer. + */ #include "cvc4_public.h" @@ -276,7 +275,7 @@ class BitVector }; /* class BitVector */ /* ----------------------------------------------------------------------- - ** BitVector structs + * BitVector structs * ----------------------------------------------------------------------- */ /** @@ -376,7 +375,7 @@ struct IntToBitVector }; /* struct IntToBitVector */ /* ----------------------------------------------------------------------- - ** Hash Function structs + * Hash Function structs * ----------------------------------------------------------------------- */ /* @@ -415,7 +414,7 @@ struct UnsignedHashFunction }; /* struct UnsignedHashFunction */ /* ----------------------------------------------------------------------- - ** Output stream + * Output stream * ----------------------------------------------------------------------- */ inline std::ostream& operator<<(std::ostream& os, const BitVector& bv); diff --git a/src/util/bool.h b/src/util/bool.h index 46e5eda1a..d0fb3ec75 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file bool.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 A hash function for Boolean - ** - ** A hash function for Boolean. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * A hash function for Boolean. + */ #include "cvc4_public.h" diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index acbb26b19..1526cfa29 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file cardinality.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 Representation of cardinality - ** - ** Implementation of a simple class to represent a cardinality. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * Representation of cardinality. + * + * Implementation of a simple class to represent a cardinality. + */ #include "util/cardinality.h" diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 36b07c29d..3dd24131d 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file cardinality.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 Representation of cardinality - ** - ** Simple class to represent a cardinality; used by the CVC4 type system - ** give the cardinality of sorts. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * Representation of cardinality. + * + * Simple class to represent a cardinality; used by the CVC4 type system + * give the cardinality of sorts. + */ #include "cvc4_public.h" diff --git a/src/util/cardinality_class.cpp b/src/util/cardinality_class.cpp index 32390a97c..70b321963 100644 --- a/src/util/cardinality_class.cpp +++ b/src/util/cardinality_class.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file cardinality_class.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Utilities for cardinality classes - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Utilities for cardinality classes. + */ #include "util/cardinality_class.h" diff --git a/src/util/cardinality_class.h b/src/util/cardinality_class.h index 49f2b74c0..3c89b22bd 100644 --- a/src/util/cardinality_class.h +++ b/src/util/cardinality_class.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file cardinality_class.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Utilities for cardinality classes - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Utilities for cardinality classes. + */ #include "cvc4_private.h" diff --git a/src/util/dense_map.h b/src/util/dense_map.h index f3b0372b2..3d56243da 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -1,29 +1,30 @@ -/********************* */ -/*! \file dense_map.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Dejan Jovanovic, 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 This is an abstraction of a Map from unsigned integers to elements - ** of type T. - ** - ** This is an abstraction of a Map from an unsigned integer to elements of - ** type T. - ** This class is designed to provide constant time insertion, deletion, - ** element_of, and fast iteration. This is done by storing backing vectors of - ** size greater than the maximum key. - ** This datastructure is appropriate for heavy use datastructures where the - ** Keys are a dense set of integers. - ** - ** T must support T(), and operator=(). - ** - ** The derived utility classes DenseSet and DenseMultiset are also defined. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Dejan Jovanovic, 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. + * **************************************************************************** + * + * This is an abstraction of a Map from unsigned integers to elements + * of type T. + * + * This is an abstraction of a Map from an unsigned integer to elements of + * type T. + * This class is designed to provide constant time insertion, deletion, + * element_of, and fast iteration. This is done by storing backing vectors of + * size greater than the maximum key. + * This datastructure is appropriate for heavy use datastructures where the + * Keys are a dense set of integers. + * + * T must support T(), and operator=(). + * + * The derived utility classes DenseSet and DenseMultiset are also defined. + */ #include "cvc4_private.h" diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp index d8c099923..5b4fafc3d 100644 --- a/src/util/divisible.cpp +++ b/src/util/divisible.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file divisible.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "util/divisible.h" diff --git a/src/util/divisible.h b/src/util/divisible.h index 2cfe95ec7..1f960650f 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file divisible.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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): + * 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_public.h" diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index b6fa79e84..0df9488c5 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -1,20 +1,21 @@ -/********************* */ -/*! \file floatingpoint.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, Haniel Barbosa - ** Copyright (c) 2013 University of Oxford - ** 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 A floating-point value. - ** - ** This file contains the data structures used by the constant and parametric - ** types of the floating point theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain, Haniel Barbosa + * Copyright (c) 2013 University of Oxford + * + * 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. + * **************************************************************************** + * + * A floating-point value. + * + * This file contains the data structures used by the constant and parametric + * types of the floating point theory. + */ #include "util/floatingpoint.h" diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index e65c89b8a..ebd9ef9f9 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -1,20 +1,21 @@ -/********************* */ -/*! \file floatingpoint.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, Mathias Preiner - ** Copyright (c) 2013 University of Oxford - ** 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 A floating-point value. - ** - ** This file contains the data structures used by the constant and parametric - ** types of the floating point theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain, Mathias Preiner + * Copyright (c) 2013 University of Oxford + * + * 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. + * **************************************************************************** + * + * A floating-point value. + * + * This file contains the data structures used by the constant and parametric + * types of the floating point theory. + */ #include "cvc4_public.h" #ifndef CVC5__FLOATINGPOINT_H diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index f6bb9d541..c2c3fe77b 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file floatingpoint_literal_symfpu.cpp - ** \verbatim - ** Top contributors (to current version): - ** Martin Brain, Aina Niemetz, 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 SymFPU glue code for floating-point values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain, 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. + * **************************************************************************** + * + * SymFPU glue code for floating-point values. + */ #include "util/floatingpoint_literal_symfpu.h" #include "base/check.h" diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index e773c1f97..5e26ba685 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -1,18 +1,19 @@ -/********************* */ -/*! \file floatingpoint_literal_symfpu.h.in - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, 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 SymFPU glue code for floating-point values. - ** - ** !!! This header is not to be included in any other headers !!! - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * SymFPU glue code for floating-point values. + * + * !!! This header is not to be included in any other headers !!! + */ #include "cvc4_public.h" #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp index d1cd7621f..45fd4272f 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.cpp +++ b/src/util/floatingpoint_literal_symfpu_traits.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file floatingpoint_literal_symfpu_traits.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 SymFPU glue code for floating-point values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Martin Brain, 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. + * **************************************************************************** + * + * SymFPU glue code for floating-point values. + */ #if CVC5_USE_SYMFPU diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h.in index 2c2504ab7..eeff5bbfa 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.h.in +++ b/src/util/floatingpoint_literal_symfpu_traits.h.in @@ -1,20 +1,19 @@ -/********************* */ -/*! \file floatingpoint_literal_symfpu_traits.h.in - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, 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 SymFPU glue code for floating-point values. - ** - ** !!! This header is only to be included in floating-point literal headers !!! - **/ - -/** +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain, 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. + * **************************************************************************** + * + * SymFPU glue code for floating-point values. + * + * !!! This header is only to be included in floating-point literal headers !!! + * * This is a symfpu literal "back-end". It allows the library to be used as * an arbitrary precision floating-point implementation. This is effectively * the glue between symfpu's notion of "signed bit-vector" and CVC4's diff --git a/src/util/floatingpoint_size.cpp b/src/util/floatingpoint_size.cpp index cf7aea524..d0c1f95f3 100644 --- a/src/util/floatingpoint_size.cpp +++ b/src/util/floatingpoint_size.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file floatingpoint_size.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain - ** 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 The class representing a floating-point format. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain + * + * 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 class representing a floating-point format. + */ #include "util/floatingpoint_size.h" #include "base/check.h" diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h index 9322b9f72..e8ce27af8 100644 --- a/src/util/floatingpoint_size.h +++ b/src/util/floatingpoint_size.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file floatingpoint_size.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, 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 The class representing a floating-point format. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Martin Brain, 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. + * **************************************************************************** + * + * The class representing a floating-point format. + */ #include "cvc4_public.h" #ifndef CVC5__FLOATINGPOINT_SIZE_H diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 31c2eea84..fd25b6470 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file gmp_util.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Mathias Preiner, 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Mathias Preiner, 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_public.h" diff --git a/src/util/hash.h b/src/util/hash.h index a7cb214b0..7fcf6286e 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file hash.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, 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): + * Morgan Deters, Andres Noetzli, 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 "cvc4_public.h" diff --git a/src/util/iand.h b/src/util/iand.h index b05d23547..082a1b353 100644 --- a/src/util/iand.h +++ b/src/util/iand.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file iand.h - ** \verbatim - ** Top contributors (to current version): - ** 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 The integer AND operator. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, 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 integer AND operator. + */ #include "cvc4_public.h" @@ -32,7 +33,7 @@ struct IntAnd }; /* struct IntAnd */ /* ----------------------------------------------------------------------- - ** Output stream + * Output stream * ----------------------------------------------------------------------- */ inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia); diff --git a/src/util/index.cpp b/src/util/index.cpp index ffb49f943..d9fea498f 100644 --- a/src/util/index.cpp +++ b/src/util/index.cpp @@ -1,19 +1,17 @@ -/********************* */ -/*! \file index.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Standardized type for efficient array indexing. + */ #include "util/index.h" diff --git a/src/util/index.h b/src/util/index.h index 9ba608ef6..d8c47ae04 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file index.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, 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 Standardized type for efficient array indexing. - ** - ** Standardized type for efficient array indexing. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, 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. + * **************************************************************************** + * + * Standardized type for efficient array indexing. + */ #include "cvc4_private.h" diff --git a/src/util/indexed_root_predicate.h b/src/util/indexed_root_predicate.h index 9d03bc677..8b9caa037 100644 --- a/src/util/indexed_root_predicate.h +++ b/src/util/indexed_root_predicate.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file indexed_root_predicate.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Utils for indexed root predicates. - ** - ** Some utils for indexed root predicates. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Utils for indexed root predicates. + */ #include "cvc4_public.h" @@ -71,4 +70,4 @@ struct IndexedRootPredicateHashFunction } // namespace cvc5 -#endif
\ No newline at end of file +#endif diff --git a/src/util/integer.h.in b/src/util/integer.h.in index aabc8109d..cfcef4ae2 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -1,18 +1,17 @@ -/********************* */ -/*! \file integer.h.in - ** \verbatim - ** Top contributors (to current version): - ** 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 A multi-precision integer constant - ** - ** A multi-precision integer constant. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * A multi-precision integer constant. + */ // these gestures are used to avoid a public header dependence on cvc4autoconfig.h diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index c41b17fd6..f54630d23 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -1,19 +1,17 @@ -/********************* */ -/*! \file integer_cln_imp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A multiprecision integer constant; wraps a CLN multiprecision integer. + */ #include <sstream> #include <string> diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index fdc55871d..910e1a6a5 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -1,19 +1,17 @@ -/********************* */ -/*! \file integer_cln_imp.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, 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 A multiprecision integer constant; wraps a CLN multiprecision - ** integer. - ** - ** A multiprecision integer constant; wraps a CLN multiprecision integer. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A multiprecision integer constant; wraps a CLN multiprecision integer. + */ #include "cvc4_public.h" diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index a7ba33bb0..52e408a37 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file integer_gmp_imp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, 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 A multi-precision rational constant. - ** - ** A multi-precision rational constant. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A multi-precision rational constant. + */ #include "util/integer.h" diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index a5cc793ce..286eaf04b 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -1,19 +1,17 @@ -/********************* */ -/*! \file integer_gmp_imp.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, 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 A multiprecision integer constant; wraps a GMP multiprecision - ** integer. - ** - ** A multiprecision integer constant; wraps a GMP multiprecision integer. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A multiprecision integer constant; wraps a GMP multiprecision integer. + */ #include "cvc4_public.h" diff --git a/src/util/maybe.h b/src/util/maybe.h index 0d6489ad8..70d351c5f 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -1,27 +1,28 @@ -/********************* */ -/*! \file maybe.h - ** \verbatim - ** Top contributors (to current version): - ** 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 This provides a templated Maybe construct. - ** - ** This class provides a templated Maybe<T> construct. - ** This follows the rough pattern of the Maybe monad in haskell. - ** A Maybe is an algebraic type that is either Nothing | Just T - ** - ** T must support T() and operator=. - ** - ** This has a couple of uses: - ** - There is no reasonable value or particularly clean way to represent - ** Nothing using a value of T - ** - High level of assurance that a value is not used before it is set. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * This provides a templated Maybe construct. + * + * This class provides a templated Maybe<T> construct. + * This follows the rough pattern of the Maybe monad in haskell. + * A Maybe is an algebraic type that is either Nothing | Just T + * + * T must support T() and operator=. + * + * This has a couple of uses: + * - There is no reasonable value or particularly clean way to represent + * Nothing using a value of T + * - High level of assurance that a value is not used before it is set. + */ #include "cvc4_public.h" #ifndef CVC5__UTIL__MAYBE_H diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp index 8a3b2b47b..f7f4dfa86 100644 --- a/src/util/ostream_util.cpp +++ b/src/util/ostream_util.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file ostream_util.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Utilities for using ostreams. - ** - ** Utilities for using ostreams. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Utilities for using ostreams. + */ #include "util/ostream_util.h" #include <ostream> diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h index f1b343b21..f3df20cd5 100644 --- a/src/util/ostream_util.h +++ b/src/util/ostream_util.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file ostream_util.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Utilities for using ostreams. - ** - ** Utilities for using ostreams. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Utilities for using ostreams. + */ #include "cvc4_private.h" diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp index 50f42140b..133cd00a3 100644 --- a/src/util/poly_util.cpp +++ b/src/util/poly_util.cpp @@ -1,24 +1,17 @@ -/********************* */ -/*! \file poly_util.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 - ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for working with LibPoly. - ** - ** Utilities for working with LibPoly. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Utilities for working with LibPoly. + */ #include "poly_util.h" diff --git a/src/util/poly_util.h b/src/util/poly_util.h index 5ab96b5b1..5c67fc876 100644 --- a/src/util/poly_util.h +++ b/src/util/poly_util.h @@ -1,24 +1,17 @@ -/********************* */ -/*! \file poly_util.h - ** \verbatim - ** Top contributors (to current version): - ** 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 - ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for working with LibPoly. - ** - ** Utilities for working with LibPoly. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Utilities for working with LibPoly. + */ #include "cvc4_private.h" diff --git a/src/util/random.cpp b/src/util/random.cpp index feac8d5b6..a42d74a3c 100644 --- a/src/util/random.cpp +++ b/src/util/random.cpp @@ -1,20 +1,19 @@ -/********************* */ -/*! \file random.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 A Random Number Generator. - ** - ** A random number generator, implements the xorshift* generator - ** (see S. Vigna, An experimental exploration of Marsaglia's xorshift - ** generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016). - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A random number generator, implements the xorshift* generator + * (see S. Vigna, An experimental exploration of Marsaglia's xorshift + * generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016). + */ #include "util/random.h" diff --git a/src/util/random.h b/src/util/random.h index 32ec33a68..777ca7df1 100644 --- a/src/util/random.h +++ b/src/util/random.h @@ -1,20 +1,19 @@ -/********************* */ -/*! \file random.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andres Noetzli, 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 A Random Number Generator. - ** - ** A random number generator, implements the xorshift* generator - ** (see S. Vigna, An experimental exploration of Marsaglia's xorshift - ** generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, 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. + * **************************************************************************** + * + * A random number generator, implements the xorshift* generator + * (see S. Vigna, An experimental exploration of Marsaglia's xorshift + * generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016). + */ #include "cvc4_private.h" diff --git a/src/util/rational.h.in b/src/util/rational.h.in index b05aefbd3..c8b673d7e 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -1,18 +1,17 @@ -/********************* */ -/*! \file rational.h.in - ** \verbatim - ** Top contributors (to current version): - ** 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 A multi-precision rational constant - ** - ** A multi-precision rational constant. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * A multi-precision rational constant. + */ // these gestures are used to avoid a public header dependence on cvc4autoconfig.h diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 5d71e63f4..93816bd20 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file rational_cln_imp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, 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 A multi-precision rational constant. - ** - ** A multi-precision rational constant. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Christopher L. Conway, 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. + * **************************************************************************** + * + * A multi-precision rational constant. + */ #include "util/rational.h" #include <sstream> diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 4614620d5..c3808a5d9 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -1,19 +1,17 @@ -/********************* */ -/*! \file rational_cln_imp.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Gereon Kremer, 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 Multiprecision rational constants; wraps a CLN multiprecision - ** rational. - ** - ** Multiprecision rational constants; wraps a CLN multiprecision rational. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Gereon Kremer, 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. + * **************************************************************************** + * + * Multiprecision rational constants; wraps a CLN multiprecision rational. + */ #include "cvc4_public.h" @@ -40,19 +38,19 @@ namespace cvc5 { /** - ** A multi-precision rational constant. - ** This stores the rational as a pair of multi-precision integers, - ** one for the numerator and one for the denominator. - ** The number is always stored so that the gcd of the numerator and denominator - ** is 1. (This is referred to as referred to as canonical form in GMP's - ** literature.) A consequence is that that the numerator and denominator may be - ** different than the values used to construct the Rational. - ** - ** NOTE: The correct way to create a Rational from an int is to use one of the - ** int numerator/int denominator constructors with the denominator 1. Trying - ** to construct a Rational with a single int, e.g., Rational(0), will put you - ** in danger of invoking the char* constructor, from whence you will segfault. - **/ + * A multi-precision rational constant. + * This stores the rational as a pair of multi-precision integers, + * one for the numerator and one for the denominator. + * The number is always stored so that the gcd of the numerator and denominator + * is 1. (This is referred to as referred to as canonical form in GMP's + * literature.) A consequence is that that the numerator and denominator may be + * different than the values used to construct the Rational. + * + * NOTE: The correct way to create a Rational from an int is to use one of the + * int numerator/int denominator constructors with the denominator 1. Trying + * to construct a Rational with a single int, e.g., Rational(0), will put you + * in danger of invoking the char* constructor, from whence you will segfault. + */ class CVC4_EXPORT Rational { diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index f64bca32f..24e6e96d7 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file rational_gmp_imp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, 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 A multi-precision rational constant. - ** - ** A multi-precision rational constant. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, 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. + * **************************************************************************** + * + * A multi-precision rational constant. + */ #include "util/rational.h" #include <cmath> diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 1509e3e16..79dd8e83c 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -1,19 +1,17 @@ -/********************* */ -/*! \file rational_gmp_imp.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Gereon Kremer, 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 Multiprecision rational constants; wraps a GMP multiprecision - ** rational. - ** - ** Multiprecision rational constants; wraps a GMP multiprecision rational. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Gereon Kremer, 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. + * **************************************************************************** + * + * Multiprecision rational constants; wraps a GMP multiprecision rational. + */ #include "cvc4_public.h" @@ -32,19 +30,19 @@ namespace cvc5 { /** - ** A multi-precision rational constant. - ** This stores the rational as a pair of multi-precision integers, - ** one for the numerator and one for the denominator. - ** The number is always stored so that the gcd of the numerator and denominator - ** is 1. (This is referred to as referred to as canonical form in GMP's - ** literature.) A consequence is that that the numerator and denominator may be - ** different than the values used to construct the Rational. - ** - ** NOTE: The correct way to create a Rational from an int is to use one of the - ** int numerator/int denominator constructors with the denominator 1. Trying - ** to construct a Rational with a single int, e.g., Rational(0), will put you - ** in danger of invoking the char* constructor, from whence you will segfault. - **/ + * A multi-precision rational constant. + * This stores the rational as a pair of multi-precision integers, + * one for the numerator and one for the denominator. + * The number is always stored so that the gcd of the numerator and denominator + * is 1. (This is referred to as referred to as canonical form in GMP's + * literature.) A consequence is that that the numerator and denominator may be + * different than the values used to construct the Rational. + * + * NOTE: The correct way to create a Rational from an int is to use one of the + * int numerator/int denominator constructors with the denominator 1. Trying + * to construct a Rational with a single int, e.g., Rational(0), will put you + * in danger of invoking the char* constructor, from whence you will segfault. + */ class CVC4_EXPORT Rational { diff --git a/src/util/real_algebraic_number.h.in b/src/util/real_algebraic_number.h.in index 910b357d1..8eb8b35fb 100644 --- a/src/util/real_algebraic_number.h.in +++ b/src/util/real_algebraic_number.h.in @@ -1,18 +1,17 @@ -/********************* */ -/*! \file real_algebraic_number.h.in - ** \verbatim - ** Top contributors (to current version): - ** 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 A real algebraic number constant - ** - ** A real algebraic number constant. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * A real algebraic number constant. + */ // these gestures are used to avoid a public header dependence on cvc4autoconfig.h diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index 013fc2a4a..736970129 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file real_algebraic_number_poly_imp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Implementation of RealAlgebraicNumber based on libpoly. - ** - ** Implementation of RealAlgebraicNumber based on libpoly. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Implementation of RealAlgebraicNumber based on libpoly. + */ #include "cvc4autoconfig.h" #include "util/real_algebraic_number.h" diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h index 6b014830c..2c1b7072c 100644 --- a/src/util/real_algebraic_number_poly_imp.h +++ b/src/util/real_algebraic_number_poly_imp.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file real_algebraic_number_poly_imp.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Algebraic number constants; wraps a libpoly algebraic number. - ** - ** Algebraic number constants; wraps a libpoly algebraic number. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Algebraic number constants; wraps a libpoly algebraic number. + */ #include "cvc4_private.h" diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index ef08da6fa..43d73ae96 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file regexp.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Implementation of data structures for regular expression operators. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Implementation of data structures for regular expression operators. + */ #include "util/regexp.h" diff --git a/src/util/regexp.h b/src/util/regexp.h index b0862e15a..33ab89047 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file regexp.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Data structures for regular expression operators. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, 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. + * **************************************************************************** + * + * Data structures for regular expression operators. + */ #include "cvc4_public.h" @@ -42,7 +43,7 @@ struct RegExpLoop }; /* ----------------------------------------------------------------------- - ** Hash Function structs + * Hash Function structs * ----------------------------------------------------------------------- */ /* @@ -62,7 +63,7 @@ struct RegExpLoopHashFunction }; /* ----------------------------------------------------------------------- - ** Output stream + * Output stream * ----------------------------------------------------------------------- */ std::ostream& operator<<(std::ostream& os, const RegExpRepeat& bv); diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index a982c5e1d..56d760384 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -1,19 +1,19 @@ -/********************* */ -/*! \file resource_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, Mathias Preiner, Liana Hadarean - ** 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 - ** - ** [[ Add lengthier description here ]] - - ** \todo document this file - -**/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Mathias Preiner, Liana Hadarean + * + * 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. + * **************************************************************************** + * + * This file provides the ResourceManager class. It can be used to impose + * (cumulative and per-call) resource limits on the solver, as well as per-call + * time limits. + */ #include "util/resource_manager.h" #include <algorithm> diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 787dd9a0a..526e9f5f3 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -1,20 +1,19 @@ -/********************* */ -/*! \file resource_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, Mathias Preiner, Liana Hadarean - ** 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 Provides mechanisms to limit resources. - ** - ** This file provides the ResourceManager class. It can be used to impose - ** (cumulative and per-call) resource limits on the solver, as well as per-call - ** time limits. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Mathias Preiner, Liana Hadarean + * + * 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. + * **************************************************************************** + * + * This file provides the ResourceManager class. It can be used to impose + * (cumulative and per-call) resource limits on the solver, as well as per-call + * time limits. + */ #include "cvc4_public.h" diff --git a/src/util/result.cpp b/src/util/result.cpp index 32a7e5895..84e06cdb7 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file result.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 Encapsulation of the result of a query. - ** - ** Encapsulation of the result of a query. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, 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. + * **************************************************************************** + * + * Encapsulation of the result of a query. + */ #include "util/result.h" #include <algorithm> diff --git a/src/util/result.h b/src/util/result.h index b7cd1a6b6..8714b0d32 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file result.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, 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 Encapsulation of the result of a query. - ** - ** Encapsulation of the result of a query. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, 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. + * **************************************************************************** + * + * Encapsulation of the result of a query. + */ #include "cvc4_public.h" diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index 871bece21..3ea8758a5 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file roundingmode.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Martin Brain, 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 The definition of rounding mode values. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mathias Preiner, Martin Brain + * + * 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 definition of rounding mode values. + */ #include "cvc4_public.h" #ifndef CVC5__ROUNDINGMODE_H diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp index ce4f529a4..221809fec 100644 --- a/src/util/safe_print.cpp +++ b/src/util/safe_print.cpp @@ -1,22 +1,23 @@ -/********************* */ -/*! \file safe_print.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Definition of print functions that are safe to use in a signal - ** handler. - ** - ** Signal handlers only allow a very limited set of operations, e.g. dynamic - ** memory allocation is not possible. This set of functions can be used to - ** print information from a signal handler. All output is written to file - ** descriptors using the async-signal-safe write() function. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Definition of print functions that are safe to use in a signal + * handler. + * + * Signal handlers only allow a very limited set of operations, e.g. dynamic + * memory allocation is not possible. This set of functions can be used to + * print information from a signal handler. All output is written to file + * descriptors using the async-signal-safe write() function. + */ #include "safe_print.h" diff --git a/src/util/safe_print.h b/src/util/safe_print.h index 92eaaaeff..51e6745c7 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -1,36 +1,37 @@ -/********************* */ -/*! \file safe_print.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, 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 Print functions that are safe to use in a signal handler. - ** - ** Signal handlers only allow a very limited set of operations, e.g. dynamic - ** memory allocation is not possible. This set of functions can be used to - ** print information from a signal handler. - ** - ** The safe_print function takes a template parameter T and prints an argument - ** of type const T& to avoid copying, e.g. when printing std::strings. For - ** consistency, we also pass primitive types by reference (otherwise, functions - ** in statistics_registry.h would require specialization or we would have to - ** use function overloading). - ** - ** If there exists a function `toString(obj)` for a given object, it will be - ** used automatically. This is useful for printing enum values for example. - ** IMPORTANT: The `toString(obj)` function *must not* perform any allocations - ** or call other functions that are not async-signal-safe. - ** - ** This header is a "cvc4_private_library.h" header because it is private but - ** the safe_print functions are used in the driver. See also the description - ** of "statistics_registry.h" for more information on - ** "cvc4_private_library.h". - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, 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. + * **************************************************************************** + * + * Print functions that are safe to use in a signal handler. + * + * Signal handlers only allow a very limited set of operations, e.g. dynamic + * memory allocation is not possible. This set of functions can be used to + * print information from a signal handler. + * + * The safe_print function takes a template parameter T and prints an argument + * of type const T& to avoid copying, e.g. when printing std::strings. For + * consistency, we also pass primitive types by reference (otherwise, functions + * in statistics_registry.h would require specialization or we would have to + * use function overloading). + * + * If there exists a function `toString(obj)` for a given object, it will be + * used automatically. This is useful for printing enum values for example. + * IMPORTANT: The `toString(obj)` function *must not* perform any allocations + * or call other functions that are not async-signal-safe. + * + * This header is a "cvc4_private_library.h" header because it is private but + * the safe_print functions are used in the driver. See also the description + * of "statistics_registry.h" for more information on + * "cvc4_private_library.h". + */ #include "cvc4_private_library.h" diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp index a5ed5bbb4..9c50a39c4 100644 --- a/src/util/sampler.cpp +++ b/src/util/sampler.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file sampler.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Sampler class that generates random values of different sorts - ** - ** The Sampler class can be used to generate random values of different sorts - ** with biased and unbiased distributions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Sampler class that generates random values of different sorts + * + * The Sampler class can be used to generate random values of different sorts + * with biased and unbiased distributions. + */ #include "util/sampler.h" diff --git a/src/util/sampler.h b/src/util/sampler.h index 96dbf27e2..540e5d74e 100644 --- a/src/util/sampler.h +++ b/src/util/sampler.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file sampler.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, 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 Sampler class that generates random values of different sorts - ** - ** The Sampler class can be used to generate random values of different sorts - ** with biased and unbiased distributions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, 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. + * **************************************************************************** + * + * Sampler class that generates random values of different sorts + * + * The Sampler class can be used to generate random values of different sorts + * with biased and unbiased distributions. + */ #include "cvc4_private.h" diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 85dd038bb..045a17354 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -1,26 +1,25 @@ -/********************* */ -/*! \file sexpr.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, 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 Simple representation of S-expressions - ** - ** Simple representation of S-expressions. - ** - ** SExprs have their own language specific printing procedures. The reason for - ** this being implemented on SExpr and not on the Printer class is that the - ** Printer class lives in libcvc4. It has to currently as it prints fairly - ** complicated objects, like Model, which in turn uses SmtEngine pointers. - ** However, SExprs need to be printed by Statistics. To get the output - ** consistent with the previous version, the printing of SExprs in different - ** languages is handled in the SExpr class and the libexpr library. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Simple representation of S-expressions. + * + * SExprs have their own language specific printing procedures. The reason for + * this being implemented on SExpr and not on the Printer class is that the + * Printer class lives in libcvc4. It has to currently as it prints fairly + * complicated objects, like Model, which in turn uses SmtEngine pointers. + * However, SExprs need to be printed by Statistics. To get the output + * consistent with the previous version, the printing of SExprs in different + * languages is handled in the SExpr class and the libexpr library. + */ #include "util/sexpr.h" diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 7d76188bc..522dbea05 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -1,25 +1,25 @@ -/********************* */ -/*! \file sexpr.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, 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 Simple representation of S-expressions - ** - ** Simple representation of S-expressions. - ** These are used when a simple, and obvious interface for basic - ** expressions is appropriate. - ** - ** These are quite ineffecient. - ** These are totally disconnected from any ExprManager. - ** These keep unique copies of all of their children. - ** These are VERY overly verbose and keep much more data than is needed. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, 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. + * **************************************************************************** + * + * Simple representation of S-expressions + * + * These are used when a simple, and obvious interface for basic + * expressions is appropriate. + * + * These are quite ineffecient. + * These are totally disconnected from any ExprManager. + * These keep unique copies of all of their children. + * These are VERY overly verbose and keep much more data than is needed. + */ #include "cvc4_public.h" diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp index c4e01acc4..82750c48b 100644 --- a/src/util/smt2_quote_string.cpp +++ b/src/util/smt2_quote_string.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt2_quote_string.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Andres Noetzli, 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 Quotes a string if necessary for smt2. - ** - ** Quotes a string if necessary for smt2. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Andres Noetzli, 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. + * **************************************************************************** + * + * Quotes a string if necessary for smt2. + */ #include "util/smt2_quote_string.h" diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h index 487b10537..95e134056 100644 --- a/src/util/smt2_quote_string.h +++ b/src/util/smt2_quote_string.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file smt2_quote_string.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Quotes a string if necessary for smt2. - ** - ** Quotes a string if necessary for smt2. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Quotes a string if necessary for smt2. + */ #include "cvc4_private.h" diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 7053e9ea0..b2930a742 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file statistics.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Gereon Kremer, 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "util/statistics.h" diff --git a/src/util/statistics.h b/src/util/statistics.h index 0f6c7c7b9..5e3090ec7 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file statistics.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, 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): + * Morgan Deters, 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_public.h" diff --git a/src/util/statistics_public.cpp b/src/util/statistics_public.cpp index dd488c192..426bec37c 100644 --- a/src/util/statistics_public.cpp +++ b/src/util/statistics_public.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file statistics_public.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Registration of public statistics - ** - ** Registration and documentation for all public statistics. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Registration and documentation for all public statistics. + */ #include "util/statistics_public.h" diff --git a/src/util/statistics_public.h b/src/util/statistics_public.h index bc0882716..e68802acd 100644 --- a/src/util/statistics_public.h +++ b/src/util/statistics_public.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file statistics_public.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Registration of public statistics - ** - ** Registration and documentation for all public statistics. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Registration and documentation for all public statistics. + */ #include "cvc4_private_library.h" diff --git a/src/util/statistics_reg.cpp b/src/util/statistics_reg.cpp index efb564c74..cb245eb7a 100644 --- a/src/util/statistics_reg.cpp +++ b/src/util/statistics_reg.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file statistics_reg.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Central statistics registry. - ** - ** The StatisticsRegistry that issues statistic proxy objects. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Central statistics registry. + * + * The StatisticsRegistry that issues statistic proxy objects. + */ #include "util/statistics_reg.h" diff --git a/src/util/statistics_reg.h b/src/util/statistics_reg.h index 655d63a8c..385b6e168 100644 --- a/src/util/statistics_reg.h +++ b/src/util/statistics_reg.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file statistics_reg.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Central statistics registry. - ** - ** The StatisticsRegistry that issues statistic proxy objects. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Central statistics registry. + * + * The StatisticsRegistry that issues statistic proxy objects. + */ #include "cvc4_private_library.h" diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 094bf9709..ca7fb8b1c 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -1,19 +1,17 @@ -/********************* */ -/*! \file statistics_registry.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, 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. + * **************************************************************************** + * + * Statistics utility classes + */ #include "util/statistics_registry.h" diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index e0b0dc177..522a156e2 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -1,35 +1,36 @@ -/********************* */ -/*! \file statistics_registry.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, 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 Statistics utility classes - ** - ** Statistics utility classes, including classes for holding (and referring - ** to) statistics, the statistics registry, and some other associated - ** classes. - ** - ** This file is somewhat unique in that it is a "cvc4_private_library.h" - ** header. Because of this, most classes need to be marked as CVC4_EXPORT. - ** This is because CVC4_EXPORT is connected to the visibility of the linkage - ** in the object files for the class. It does not dictate what headers are - ** installed. - ** Because the StatisticsRegistry and associated classes are built into - ** libutil, which is used by libcvc4, and then later used by the libmain - ** without referring to libutil as well. Thus the without marking these as - ** CVC4_EXPORT the symbols would be external in libutil, internal in libcvc4, - ** and not be visible to libmain and linking would fail. - ** You can debug this using "nm" on the .so and .o files in the builds/ - ** directory. See - ** http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking - ** for a longer discussion on symbol visibility. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Gereon Kremer, 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. + * **************************************************************************** + * + * Statistics utility classes + * + * Statistics utility classes, including classes for holding (and referring + * to) statistics, the statistics registry, and some other associated + * classes. + * + * This file is somewhat unique in that it is a "cvc4_private_library.h" + * header. Because of this, most classes need to be marked as CVC4_EXPORT. + * This is because CVC4_EXPORT is connected to the visibility of the linkage + * in the object files for the class. It does not dictate what headers are + * installed. + * Because the StatisticsRegistry and associated classes are built into + * libutil, which is used by libcvc4, and then later used by the libmain + * without referring to libutil as well. Thus the without marking these as + * CVC4_EXPORT the symbols would be external in libutil, internal in libcvc4, + * and not be visible to libmain and linking would fail. + * You can debug this using "nm" on the .so and .o files in the builds/ + * directory. See + * http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking + * for a longer discussion on symbol visibility. + */ /** * On the design of the statistics: diff --git a/src/util/statistics_stats.cpp b/src/util/statistics_stats.cpp index 8aa686e5d..971c592ac 100644 --- a/src/util/statistics_stats.cpp +++ b/src/util/statistics_stats.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file statistics_stats.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Basic statistics representation - ** - ** The basic statistics classes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Basic statistics representation. + */ #include "util/statistics_stats.h" diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h index 97778bb5f..fe5ad9de7 100644 --- a/src/util/statistics_stats.h +++ b/src/util/statistics_stats.h @@ -1,21 +1,22 @@ -/********************* */ -/*! \file statistics_stats.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Statistic proxy objects - ** - ** Conceptually, every statistic consists of a data object and a proxy - ** object. The proxy objects are issued by the `StatisticsRegistry` and - ** maintained by the user. They only hold a pointer to a matching data - ** object. The purpose of proxy objects is to implement methods to easily - ** change the statistic data, but shield the regular user from the internals. +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Statistic proxy objects + * + * Conceptually, every statistic consists of a data object and a proxy + * object. The proxy objects are issued by the `StatisticsRegistry` and + * maintained by the user. They only hold a pointer to a matching data + * object. The purpose of proxy objects is to implement methods to easily + * change the statistic data, but shield the regular user from the internals. */ #include "cvc4_private_library.h" diff --git a/src/util/statistics_value.cpp b/src/util/statistics_value.cpp index 6db0b3cd3..e92507d72 100644 --- a/src/util/statistics_value.cpp +++ b/src/util/statistics_value.cpp @@ -1,26 +1,27 @@ -/********************* */ -/*! \file statistics_value.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Statistic data classes - ** - ** The statistic data classes that actually hold the data for the statistics. - ** - ** Conceptually, every statistic consists of a data object and a proxy object. - ** The data objects (statistic values) are derived from `StatisticBaseValue` - ** and live in the `StatisticsRegistry`. - ** They are solely exported to the proxy objects, which should be the sole - ** way to manipulate the data of a data object. - ** The data objects themselves need to implement printing (normal and safe) and - ** conversion to the API type `Stat`. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Statistic data classes + * + * The statistic data classes that actually hold the data for the statistics. + * + * Conceptually, every statistic consists of a data object and a proxy object. + * The data objects (statistic values) are derived from `StatisticBaseValue` + * and live in the `StatisticsRegistry`. + * They are solely exported to the proxy objects, which should be the sole + * way to manipulate the data of a data object. + * The data objects themselves need to implement printing (normal and safe) and + * conversion to the API type `Stat`. + */ #include "util/statistics_value.h" diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h index 67fd37118..b8d3f1fa3 100644 --- a/src/util/statistics_value.h +++ b/src/util/statistics_value.h @@ -1,26 +1,27 @@ -/********************* */ -/*! \file statistics_value.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Statistic data classes - ** - ** The statistic data classes that actually hold the data for the statistics. - ** - ** Conceptually, every statistic consists of a data object and a proxy object. - ** The data objects (statistic values) are derived from `StatisticBaseValue` - ** and live in the `StatisticsRegistry`. - ** They are solely exported to the proxy objects, which should be the sole - ** way to manipulate the data of a data object. - ** The data objects themselves need to implement printing (normal and safe) and - ** conversion to the API type `Stat`. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Statistic data classes. + * + * The statistic data classes that actually hold the data for the statistics. + * + * Conceptually, every statistic consists of a data object and a proxy object. + * The data objects (statistic values) are derived from `StatisticBaseValue` + * and live in the `StatisticsRegistry`. + * They are solely exported to the proxy objects, which should be the sole + * way to manipulate the data of a data object. + * The data objects themselves need to implement printing (normal and safe) and + * conversion to the API type `Stat`. + */ #include "cvc4_private_library.h" diff --git a/src/util/stats_base.cpp b/src/util/stats_base.cpp index 5d34b43f2..886effe5e 100644 --- a/src/util/stats_base.cpp +++ b/src/util/stats_base.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file stats_base.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Base statistic classes - ** - ** Base statistic classes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Tim King, 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. + * **************************************************************************** + * + * Base statistic classes. + */ #include "util/stats_base.h" diff --git a/src/util/stats_base.h b/src/util/stats_base.h index 9d168bad1..8be383224 100644 --- a/src/util/stats_base.h +++ b/src/util/stats_base.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file stats_base.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Base statistic classes - ** - ** Base statistic classes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Morgan Deters, 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. + * **************************************************************************** + * + * Base statistic classes. + */ #include "cvc4_private_library.h" diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h index e9968dd34..ef45471ee 100644 --- a/src/util/stats_histogram.h +++ b/src/util/stats_histogram.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file stats_histogram.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Histogram statistics - ** - ** Stat classes that represent histograms - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Mathias Preiner, 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. + * **************************************************************************** + * + * Histogram statistics. + * + * Stat classes that represent histograms. + */ #include "cvc4_private_library.h" diff --git a/src/util/stats_timer.cpp b/src/util/stats_timer.cpp index eedb30b4c..1ffbe28a8 100644 --- a/src/util/stats_timer.cpp +++ b/src/util/stats_timer.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file stats_timer.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Timer statistics - ** - ** Stat classes that hold timers - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Timer statistics. + * + * Stat classes that hold timers. + */ #include "util/stats_timer.h" diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h index 981c705f9..b11944152 100644 --- a/src/util/stats_timer.h +++ b/src/util/stats_timer.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file stats_timer.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Timer statistics - ** - ** Stat classes that hold timers - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Gereon Kremer, 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. + * **************************************************************************** + * + * Timer statistics. + * + * Stat classes that hold timers. + */ #include "cvc4_private_library.h" diff --git a/src/util/stats_utils.cpp b/src/util/stats_utils.cpp index 7908e0912..e30266cbb 100644 --- a/src/util/stats_utils.cpp +++ b/src/util/stats_utils.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file stats_utils.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Statistic utilities - ** - ** Statistic utilities - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Statistic utilities. + */ #include "util/stats_utils.h" diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h index 8488f66cf..ec910322d 100644 --- a/src/util/stats_utils.h +++ b/src/util/stats_utils.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file stats_utils.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Statistic utilities - ** - ** Statistic utilities - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Statistic utilities. + */ #include "cvc4_private_library.h" diff --git a/src/util/string.cpp b/src/util/string.cpp index b6f93aa0f..5f2bd5b83 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file string.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Tianyi Liang - ** 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 Implementation of the string data type. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Tianyi Liang + * + * 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. + * **************************************************************************** + * + * Implementation of the string data type. + */ #include "util/string.h" diff --git a/src/util/string.h b/src/util/string.h index 1df23b61a..84b67b043 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file string.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Tianyi Liang - ** 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 The string data type. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Tianyi Liang + * + * 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 string data type. + */ #include "cvc4_public.h" diff --git a/src/util/tuple.h b/src/util/tuple.h index 3e6c0d677..e343975fb 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file tuple.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 Tuple operators - ** - ** Tuple operators. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Mathias Preiner, 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. + * **************************************************************************** + * + * Tuple operators. + */ #include "cvc4_public.h" diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h index 876bec2c8..5164c6cd0 100644 --- a/src/util/unsafe_interrupt_exception.h +++ b/src/util/unsafe_interrupt_exception.h @@ -1,17 +1,18 @@ -/********************* */ -/*! \file unsafe_interrupt_exception.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, 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 An exception that is thrown when the solver is out of time/resources - ** and is interrupted in an unsafe state - **/ +/****************************************************************************** + * Top contributors (to current version): + * Liana Hadarean, Mathias Preiner, 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. + * **************************************************************************** + * + * An exception that is thrown when the solver is out of time/resources + * and is interrupted in an unsafe state. + */ #include "cvc4_public.h" diff --git a/src/util/utility.cpp b/src/util/utility.cpp index cde74c6eb..7e36a9c90 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file utility.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Some standard STL-related utility functions for CVC4 - ** - ** Some standard STL-related utility functions for CVC4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Some standard STL-related utility functions for CVC4. + */ #include "util/utility.h" diff --git a/src/util/utility.h b/src/util/utility.h index a11abe4e7..3d97cbd4e 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file utility.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, 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 Some standard STL-related utility functions for CVC4 - ** - ** Some standard STL-related utility functions for CVC4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, 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. + * **************************************************************************** + * + * Some standard STL-related utility functions for CVC4. + */ #include "cvc4_private.h" |