diff options
Diffstat (limited to 'src/expr')
117 files changed, 1806 insertions, 1746 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 1161d1b70..17bd49ea7 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Mathias Preiner, Andrew Reynolds, 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, Andrew Reynolds, 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. ## + libcvc4_add_sources( array_store_all.cpp array_store_all.h diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index b92ba8607..848d86edd 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -1,20 +1,18 @@ -/********************* */ -/*! \file array_store_all.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 Representation of a constant array (an array in which the - ** element is the same for all indices) - ** - ** Representation of a constant array (an array in which the element is - ** the same for all indices). - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Representation of a constant array (an array in which the element is the + * same for all indices). + */ #include "expr/array_store_all.h" diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 49031e28a..75b1a6d06 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -1,20 +1,18 @@ -/********************* */ -/*! \file array_store_all.h - ** \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 Representation of a constant array (an array in which the - ** element is the same for all indices) - ** - ** Representation of a constant array (an array in which the element is - ** the same for all indices). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, 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. + * **************************************************************************** + * + * Representation of a constant array (an array in which the element is the + * same for all indices). + */ #include "cvc4_public.h" diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp index 83254f5a5..e0f1c3ec8 100644 --- a/src/expr/ascription_type.cpp +++ b/src/expr/ascription_type.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file ascription_type.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 A class representing a type ascription - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A class representing a type ascription. + */ #include "expr/ascription_type.h" diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index fe6f2c23f..bb8967abd 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file ascription_type.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, 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 class representing a type ascription - ** - ** A class representing a parameter for the type ascription operator. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A class representing a parameter for the type ascription operator. + */ #include "cvc4_public.h" diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 062f0a2d2..1cb8adad6 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file attribute.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Dejan Jovanovic, 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 AttributeManager implementation. - ** - ** AttributeManager implementation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Dejan Jovanovic, 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. + * **************************************************************************** + * + * AttributeManager implementation. + */ #include "expr/attribute.h" #include <utility> diff --git a/src/expr/attribute.h b/src/expr/attribute.h index df621d860..7ddc01427 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file attribute.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Node attributes. - ** - ** Node attributes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, 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. + * **************************************************************************** + * + * Node attributes. + */ #include "cvc4_private.h" diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index a0ef6ea02..e1c6f759f 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file attribute_internals.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, 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 Node attributes' internals. - ** - ** Node attributes' internals. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, 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. + * **************************************************************************** + * + * Node attributes' internals. + */ #include "cvc4_private.h" diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index b475a700d..df7194f5a 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file attribute_unique_id.h - ** \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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_private.h" diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp index e97e559a8..fa7e4305d 100644 --- a/src/expr/bound_var_manager.cpp +++ b/src/expr/bound_var_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file bound_var_manager.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 Bound variable manager - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Bound variable manager. + */ #include "expr/bound_var_manager.h" diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index d1d1c1a38..fdfbc8460 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file bound_var_manager.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 Bound variable manager utility - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Bound variable manager. + */ #include "cvc4_private.h" diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp index 40820ea20..b37295c52 100644 --- a/src/expr/buffered_proof_generator.cpp +++ b/src/expr/buffered_proof_generator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file buffered_proof_generator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa - ** 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 a proof generator for buffered proof steps - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of a proof generator for buffered proof steps. + */ #include "expr/buffered_proof_generator.h" diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index 228af460c..81e2667bf 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file buffered_proof_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds, 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 proof generator for buffered proof steps - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, 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 proof generator for buffered proof steps. + */ #include "cvc4_private.h" diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp index 6f530529a..01f975523 100644 --- a/src/expr/datatype_index.cpp +++ b/src/expr/datatype_index.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file datatype_index.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 class representing an index to a datatype living in NodeManager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 class representing an index to a datatype living in NodeManager. + */ #include "expr/datatype_index.h" #include <sstream> diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h index ca4d6d743..c46bcda85 100644 --- a/src/expr/datatype_index.h +++ b/src/expr/datatype_index.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file datatype_index.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Ken Matsui - ** 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 class representing an index to a datatype living in NodeManager. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * A class representing an index to a datatype living in NodeManager. + */ #include "cvc4_public.h" diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 48c0e9f00..73f760170 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dtype.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 class representing a datatype definition - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 class representing a datatype definition. + */ #include "expr/dtype.h" #include <sstream> diff --git a/src/expr/dtype.h b/src/expr/dtype.h index e0f37d811..cee95cdc6 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dtype.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 class representing a datatype definition - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 class representing a datatype definition. + */ #include "cvc4_private.h" diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index c358aa2e8..debb66ef4 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dtype_cons.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 class representing a datatype definition - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 class representing a datatype definition. + */ #include "expr/dtype_cons.h" #include "expr/dtype.h" diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index 52b0a4d69..368d4cbde 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dtype_cons.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 class representing a datatype definition - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 class representing a datatype definition. + */ #include "cvc4_private.h" diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index d6a3b4469..d6a3923df 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dtype_selector.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 A class representing a datatype selector. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * A class representing a datatype selector. + */ #include "expr/dtype_selector.h" diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h index 66a4f4f4f..391d233ca 100644 --- a/src/expr/dtype_selector.h +++ b/src/expr/dtype_selector.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file dtype_selector.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 class representing a datatype selector. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 class representing a datatype selector. + */ #include "cvc4_private.h" diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp index d45612a9c..d85aca30c 100644 --- a/src/expr/emptybag.cpp +++ b/src/expr/emptybag.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file emptybag.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A class for empty bags - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A class for empty bags. + */ #include "expr/emptybag.h" diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h index 19efe3a94..78c573674 100644 --- a/src/expr/emptybag.h +++ b/src/expr/emptybag.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file emptybag.h - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A class for empty bags - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A class for empty bags. + */ #include "cvc4_public.h" diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp index 4d6604a63..d0d1d4e78 100644 --- a/src/expr/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file emptyset.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Kshitij Bansal, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Kshitij Bansal, 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 "expr/emptyset.h" diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index b1c00a5ad..a545e48b0 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file emptyset.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Andres Noetzli, Kshitij Bansal - ** 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, Andres Noetzli, Kshitij Bansal + * + * 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/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp index 4417ccb5c..06fcaee66 100644 --- a/src/expr/expr_iomanip.cpp +++ b/src/expr/expr_iomanip.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file expr_iomanip.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Kshitij Bansal - ** 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 Expr IO manipulation classes. - ** - ** Expr IO manipulation classes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Kshitij Bansal + * + * 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. + * **************************************************************************** + * + * Expr IO manipulation classes. + */ #include "expr/expr_iomanip.h" diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 91b0fcc2e..35ee6c324 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file expr_iomanip.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 Expr IO manipulation classes. - ** - ** Expr IO manipulation classes. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Expr IO manipulation classes. + */ #include "cvc4_public.h" diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index 28cbf5c37..1add4eb31 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file kind_map.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, Mathias Preiner, 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 bitmap of Kinds - ** - ** This is a class representation for a bitmap of Kinds that is - ** iterable, manipulable, and packed. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Mathias Preiner, 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 bitmap of Kinds. + * + * This is a class representation for a bitmap of Kinds that is iterable, + * manipulable, and packed. + */ #include "cvc4_private.h" diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index d9f913ddf..0674a61b0 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file kind_template.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Christopher L. Conway, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Aina Niemetz, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <sstream> diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index d24f46551..c4fc6fc73 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file kind_template.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Morgan Deters, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Template for the Node kind header - ** - ** Template for the Node kind header. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Template for the Node kind header. + */ #include "cvc4_public.h" diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 95ce1406c..8a54637fa 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file lazy_proof.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 lazy proof utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of lazy proof utility. + */ #include "expr/lazy_proof.h" diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index b60bfd409..21a862691 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file lazy_proof.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Lazy proof utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Lazy proof utility. + */ #include "cvc4_private.h" diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 5e638b55f..f5cf56983 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file lazy_proof_chain.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds, 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 Implementation of lazy proof utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of lazy proof utility. + */ #include "expr/lazy_proof_chain.h" diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 87881fae1..5a91e3e29 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file lazy_proof_chain.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds, 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 Lazy proof chain utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, 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. + * **************************************************************************** + * + * Lazy proof chain utility. + */ #include "cvc4_private.h" diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp index b014339ad..43665cc3c 100644 --- a/src/expr/match_trie.cpp +++ b/src/expr/match_trie.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file match_trie.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 Implements a match trie, also known as a discrimination tree. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implements a match trie, also known as a discrimination tree. + */ #include "expr/match_trie.h" diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h index 6f85d20c9..e17b711fc 100644 --- a/src/expr/match_trie.h +++ b/src/expr/match_trie.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file match_trie.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements a match trie, also known as a discrimination tree. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implements a match trie, also known as a discrimination tree. + */ #include "cvc4_private.h" diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp index 451464d17..01b0c01a8 100644 --- a/src/expr/metakind_template.cpp +++ b/src/expr/metakind_template.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file metakind_template.cpp - ** \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, 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "expr/metakind.h" diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 7f232b4e2..2af169577 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file metakind_template.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 Template for the metakind header. - ** - ** Template for the metakind header. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Aina Niemetz, 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. + * **************************************************************************** + * + * Template for the metakind header. + */ #include "cvc4_private.h" diff --git a/src/expr/mkexpr b/src/expr/mkexpr index c5ff67a43..0be51c71c 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -15,23 +15,26 @@ # Output is to standard out. # -copyright=2010-2014 +copyright=2010-2021 filename=`basename "$1" | sed 's,_template,,'` cat <<EOF -/********************* */ -/** $filename - ** - ** Copyright $copyright New York University and The University of Iowa, - ** and as below. - ** - ** This file automatically generated by: - ** - ** $0 $@ - ** - ** for the CVC4 project. - **/ +/****************************************************************************** + * This file is part of the cvc5 project. + * + * Copyright (c) $copyright by the authors listed in the file AUTHORS + * in the 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 was automatically generated by: + * + * $0 $@ + * + * for the cvc5 project. + */ /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ diff --git a/src/expr/mkkind b/src/expr/mkkind index 289789a9e..bf0da1073 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -14,23 +14,26 @@ # Output is to standard out. # -copyright=2010-2014 +copyright=2010-2021 filename=`basename "$1" | sed 's,_template,,'` cat <<EOF -/********************* */ -/** $filename - ** - ** Copyright $copyright New York University and The University of Iowa, - ** and as below. - ** - ** This header file automatically generated by: - ** - ** $0 $@ - ** - ** for the CVC4 project. - **/ +/****************************************************************************** + * This file is part of the cvc5 project. + * + * Copyright (c) $copyright by the authors listed in the file AUTHORS + * in the 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 header file was automatically generated by: + * + * $0 $@ + * + * for the cvc5 project. + */ /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 7c0d110fb..52fe070e6 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -17,21 +17,24 @@ # Output is to standard out. # -copyright=2010-2014 +copyright=2010-2021 cat <<EOF -/********************* */ -/** metakind.h - ** - ** Copyright $copyright New York University and The University of Iowa, - ** and as below. - ** - ** This header file automatically generated by: - ** - ** $0 $@ - ** - ** for the CVC4 project. - **/ +/****************************************************************************** + * This file is part of the cvc5 project. + * + * Copyright (c) $copyright by the authors listed in the file AUTHORS + * in the 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 header file was automatically generated by: + * + * $0 $@ + * + * for the cvc5 project. + */ EOF diff --git a/src/expr/node.cpp b/src/expr/node.cpp index ec6b7c6fb..e4acfb476 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Yoni Zohar - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Reference-counted encapsulation of a pointer to node information. - ** - ** Reference-counted encapsulation of a pointer to node information. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Reference-counted encapsulation of a pointer to node information. + */ #include "expr/node.h" #include <cstring> diff --git a/src/expr/node.h b/src/expr/node.h index 4554c1ee8..bd2120695 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, 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 Reference-counted encapsulation of a pointer to node information - ** - ** Reference-counted encapsulation of a pointer to node information. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Dejan Jovanovic, 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. + * **************************************************************************** + * + * Reference-counted encapsulation of a pointer to node information. + */ #include "cvc4_private.h" diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 1fb1a5220..0dc8858a2 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -1,19 +1,19 @@ -/********************* */ -/*! \file node_algorithm.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Common algorithms on nodes - ** - ** This file implements common algorithms applied to nodes, such as checking if - ** a node contains a free or a bound variable. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * Common algorithms on nodes. + * + * This file implements common algorithms applied to nodes, such as checking if + * a node contains a free or a bound variable. + */ #include "expr/node_algorithm.h" diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 09630cb28..b55802fd4 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -1,20 +1,20 @@ -/********************* */ -/*! \file node_algorithm.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Yoni Zohar - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Common algorithms on nodes - ** - ** This file implements common algorithms applied to nodes, such as checking if - ** a node contains a free or a bound variable. This file should generally only - ** be included in source files. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * Common algorithms on nodes. + * + * This file implements common algorithms applied to nodes, such as checking if + * a node contains a free or a bound variable. This file should generally only + * be included in source files. + */ #include "cvc4_private.h" diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 307c3aaf8..042e4442d 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file node_builder.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 A builder interface for Nodes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, 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 builder interface for Nodes. + */ #include "expr/node_builder.h" diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 95e91bb52..dd9a41146 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,136 +1,135 @@ -/********************* */ -/*! \file node_builder.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, 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 builder interface for Nodes. - ** - ** A builder interface for Nodes. - ** - ** The idea is to permit a flexible and efficient (in the common - ** case) interface for building Nodes. The general pattern of use is - ** to create a NodeBuilder, set its kind, append children to it, then - ** "extract" the resulting Node. This resulting Node may be one that - ** already exists (the NodeManager keeps a table of all Nodes in the - ** system), or may be entirely new. - ** - ** This implementation gets a bit hairy for a handful of reasons. We - ** want a user-supplied "in-line" buffer (probably on the stack, see - ** below) to hold the children, but then the number of children must - ** be known ahead of time. Therefore, if this buffer is overrun, we - ** need to heap-allocate a new buffer to hold the children. - ** - ** Note that as children are added to a NodeBuilder, they are stored - ** as raw pointers-to-NodeValue. However, their reference counts are - ** carefully maintained. - ** - ** When the "in-line" buffer "d_inlineNv" is superceded by a - ** heap-allocated buffer, we allocate the new buffer (a NodeValue - ** large enough to hold more children), copy the elements to it, and - ** mark d_inlineNv as having zero children. We do this last bit so - ** that we don't have to modify any child reference counts. The new - ** heap-allocated buffer "takes over" the reference counts of the old - ** "in-line" buffer. (If we didn't mark it as having zero children, - ** the destructor may improperly decrement the children's reference - ** counts.) - ** - ** There are then four normal cases at the end of a NodeBuilder's - ** life cycle: - ** - ** 0. We have a VARIABLE-kinded Node. These are special (they have - ** no children and are all distinct by definition). They are - ** really a subcase of 1(b), below. - ** 1. d_nv points to d_inlineNv: it is the backing store supplied - ** by the user (or derived class). - ** (a) The Node under construction already exists in the - ** NodeManager's pool. - ** (b) The Node under construction is NOT already in the - ** NodeManager's pool. - ** 2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer - ** that was heap-allocated by this NodeBuilder. - ** (a) The Node under construction already exists in the - ** NodeManager's pool. - ** (b) The Node under construction is NOT already in the - ** NodeManager's pool. - ** - ** When a Node is extracted, we convert the NodeBuilder to a Node and - ** make sure the reference counts are properly maintained. That - ** means we must ensure there are no reference-counting errors among - ** the node's children, that the children aren't re-decremented on - ** clear() or NodeBuilder destruction, and that the returned Node - ** wraps a NodeValue with a reference count of 1. - ** - ** 0. If a VARIABLE, treat similarly to 1(b), except that we - ** know there are no children (no reference counts to reason - ** about) and we don't keep VARIABLE-kinded Nodes in the - ** NodeManager pool. - ** - ** 1(a). Reference-counts for all children in d_inlineNv must be - ** decremented, and the NodeBuilder must be marked as "used" - ** and the number of children set to zero so that we don't - ** decrement them again on destruction. The existing - ** NodeManager pool entry is returned. - ** - ** 1(b). A new heap-allocated NodeValue must be constructed and all - ** settings and children from d_inlineNv copied into it. - ** This new NodeValue is put into the NodeManager's pool. - ** The NodeBuilder is marked as "used" and the number of - ** children in d_inlineNv set to zero so that we don't - ** decrement child reference counts on destruction (the child - ** reference counts have been "taken over" by the new - ** NodeValue). We return a Node wrapper for this new - ** NodeValue, which increments its reference count. - ** - ** 2(a). Reference counts for all children in d_nv must be - ** decremented. The NodeBuilder is marked as "used" and the - ** heap-allocated d_nv deleted. d_nv is repointed to - ** d_inlineNv so that destruction of the NodeBuilder doesn't - ** cause any problems. The existing NodeManager pool entry - ** is returned. - ** - ** 2(b). The heap-allocated d_nv is "cropped" to the correct size - ** (based on the number of children it _actually_ has). d_nv - ** is repointed to d_inlineNv so that destruction of the - ** NodeBuilder doesn't cause any problems, and the (old) - ** value it had is placed into the NodeManager's pool and - ** returned in a Node wrapper. - ** - ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper - ** temporary for the NodeValue in the NodeBuilder::operator Node() - ** member function. If we create a temporary (for example by writing - ** Debug("builder") << Node(nv) << endl), the NodeValue will have its - ** reference count incremented from zero to one, then decremented, - ** which makes it eligible for collection before the builder has even - ** returned it! So this is a no-no. - ** - ** There are also two cases when the NodeBuilder is clear()'ed: - ** - ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied - ** backing store): all d_inlineNv children have their reference - ** counts decremented, d_inlineNv.d_nchildren is set to zero, - ** and its kind is set to UNDEFINED_KIND. - ** - ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all - ** d_nv children have their reference counts decremented, d_nv - ** is deallocated, and d_nv is set to &d_inlineNv. d_inlineNv's - ** kind is set to UNDEFINED_KIND. - ** - ** ... destruction is similar: - ** - ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied - ** backing store): all d_inlineNv children have their reference - ** counts decremented. - ** - ** 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all - ** d_nv children have their reference counts decremented, and - ** d_nv is deallocated. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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 builder interface for Nodes. + * + * The idea is to permit a flexible and efficient (in the common + * case) interface for building Nodes. The general pattern of use is + * to create a NodeBuilder, set its kind, append children to it, then + * "extract" the resulting Node. This resulting Node may be one that + * already exists (the NodeManager keeps a table of all Nodes in the + * system), or may be entirely new. + * + * This implementation gets a bit hairy for a handful of reasons. We + * want a user-supplied "in-line" buffer (probably on the stack, see + * below) to hold the children, but then the number of children must + * be known ahead of time. Therefore, if this buffer is overrun, we + * need to heap-allocate a new buffer to hold the children. + * + * Note that as children are added to a NodeBuilder, they are stored + * as raw pointers-to-NodeValue. However, their reference counts are + * carefully maintained. + * + * When the "in-line" buffer "d_inlineNv" is superceded by a + * heap-allocated buffer, we allocate the new buffer (a NodeValue + * large enough to hold more children), copy the elements to it, and + * mark d_inlineNv as having zero children. We do this last bit so + * that we don't have to modify any child reference counts. The new + * heap-allocated buffer "takes over" the reference counts of the old + * "in-line" buffer. (If we didn't mark it as having zero children, + * the destructor may improperly decrement the children's reference + * counts.) + * + * There are then four normal cases at the end of a NodeBuilder's + * life cycle: + * + * 0. We have a VARIABLE-kinded Node. These are special (they have + * no children and are all distinct by definition). They are + * really a subcase of 1(b), below. + * 1. d_nv points to d_inlineNv: it is the backing store supplied + * by the user (or derived class). + * (a) The Node under construction already exists in the + * NodeManager's pool. + * (b) The Node under construction is NOT already in the + * NodeManager's pool. + * 2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer + * that was heap-allocated by this NodeBuilder. + * (a) The Node under construction already exists in the + * NodeManager's pool. + * (b) The Node under construction is NOT already in the + * NodeManager's pool. + * + * When a Node is extracted, we convert the NodeBuilder to a Node and + * make sure the reference counts are properly maintained. That + * means we must ensure there are no reference-counting errors among + * the node's children, that the children aren't re-decremented on + * clear() or NodeBuilder destruction, and that the returned Node + * wraps a NodeValue with a reference count of 1. + * + * 0. If a VARIABLE, treat similarly to 1(b), except that we + * know there are no children (no reference counts to reason + * about) and we don't keep VARIABLE-kinded Nodes in the + * NodeManager pool. + * + * 1(a). Reference-counts for all children in d_inlineNv must be + * decremented, and the NodeBuilder must be marked as "used" + * and the number of children set to zero so that we don't + * decrement them again on destruction. The existing + * NodeManager pool entry is returned. + * + * 1(b). A new heap-allocated NodeValue must be constructed and all + * settings and children from d_inlineNv copied into it. + * This new NodeValue is put into the NodeManager's pool. + * The NodeBuilder is marked as "used" and the number of + * children in d_inlineNv set to zero so that we don't + * decrement child reference counts on destruction (the child + * reference counts have been "taken over" by the new + * NodeValue). We return a Node wrapper for this new + * NodeValue, which increments its reference count. + * + * 2(a). Reference counts for all children in d_nv must be + * decremented. The NodeBuilder is marked as "used" and the + * heap-allocated d_nv deleted. d_nv is repointed to + * d_inlineNv so that destruction of the NodeBuilder doesn't + * cause any problems. The existing NodeManager pool entry + * is returned. + * + * 2(b). The heap-allocated d_nv is "cropped" to the correct size + * (based on the number of children it _actually_ has). d_nv + * is repointed to d_inlineNv so that destruction of the + * NodeBuilder doesn't cause any problems, and the (old) + * value it had is placed into the NodeManager's pool and + * returned in a Node wrapper. + * + * NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper + * temporary for the NodeValue in the NodeBuilder::operator Node() + * member function. If we create a temporary (for example by writing + * Debug("builder") << Node(nv) << endl), the NodeValue will have its + * reference count incremented from zero to one, then decremented, + * which makes it eligible for collection before the builder has even + * returned it! So this is a no-no. + * + * There are also two cases when the NodeBuilder is clear()'ed: + * + * 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied + * backing store): all d_inlineNv children have their reference + * counts decremented, d_inlineNv.d_nchildren is set to zero, + * and its kind is set to UNDEFINED_KIND. + * + * 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all + * d_nv children have their reference counts decremented, d_nv + * is deallocated, and d_nv is set to &d_inlineNv. d_inlineNv's + * kind is set to UNDEFINED_KIND. + * + * ... destruction is similar: + * + * 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied + * backing store): all d_inlineNv children have their reference + * counts decremented. + * + * 2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all + * d_nv children have their reference counts decremented, and + * d_nv is deallocated. + */ #include "cvc4_private.h" diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 072685e09..42be16742 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,20 +1,17 @@ -/********************* */ -/*! \file node_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Expression manager implementation. - ** - ** Expression manager implementation. - ** - ** Reviewed by Chris Conway, Apr 5 2010 (bug #65). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 manager for Nodes. + */ #include "expr/node_manager.h" #include <algorithm> diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 98eb111bc..39d0510a6 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1,20 +1,17 @@ -/********************* */ -/*! \file node_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, 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 A manager for Nodes - ** - ** A manager for Nodes. - ** - ** Reviewed by Chris Conway, Apr 5 2010 (bug #65). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A manager for Nodes. + */ #include "cvc4_private.h" diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index c88df3cee..1a82e3316 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file node_manager_attributes.h - ** \verbatim - ** Top contributors (to current version): - ** 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): + * 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 + */ #pragma once diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 73fecf4ef..d4ebed9a3 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_self_iterator.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Iterator supporting Node "self-iteration" - ** - ** Iterator supporting Node "self-iteration." - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Iterator supporting Node "self-iteration." + */ #include "cvc4_private.h" diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp index 01140a806..4e2439668 100644 --- a/src/expr/node_traversal.cpp +++ b/src/expr/node_traversal.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file node_traversal.cpp - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Iterators for traversing nodes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Alex Ozdemir, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Iterators for traversing nodes. + */ #include "node_traversal.h" diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index 4b695d2ba..095494edb 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file node_traversal.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Iterators for traversing nodes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Alex Ozdemir, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Iterators for traversing nodes. + */ #include "cvc4_private.h" diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp index 5af1cef01..ae33ae92f 100644 --- a/src/expr/node_trie.cpp +++ b/src/expr/node_trie.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file node_trie.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 a trie class for Nodes and TNodes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of a trie class for Nodes and TNodes. + */ #include "expr/node_trie.h" diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h index c2c686295..5519f4666 100644 --- a/src/expr/node_trie.h +++ b/src/expr/node_trie.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file node_trie.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 trie class for Nodes and TNodes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A trie class for Nodes and TNodes. + */ #include "cvc4_private.h" diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 7b3e413f7..10e32ac71 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -1,22 +1,22 @@ -/********************* */ -/*! \file node_value.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An expression node. - ** - ** An expression node. - ** - ** Instances of this class are generally referenced through - ** cvc4::Node rather than by pointer; cvc4::Node maintains the - ** reference count on NodeValue instances and - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Aina Niemetz, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A node value. + * + * The actual node implementation. + * Instances of this class are generally referenced through cvc5::Node rather + * than by pointer. Note that cvc5::Node maintains the reference count on + * NodeValue instances. + */ #include "expr/node_value.h" #include <sstream> diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 57eef062b..268fadeef 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -1,22 +1,22 @@ -/********************* */ -/*! \file node_value.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz, 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 An expression node. - ** - ** An expression node. - ** - ** Instances of this class are generally referenced through - ** cvc4::Node rather than by pointer; cvc4::Node maintains the - ** reference count on NodeValue instances and - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Aina Niemetz, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A node value. + * + * The actual node implementation. + * Instances of this class are generally referenced through cvc5::Node rather + * than by pointer. Note that cvc5::Node maintains the reference count on + * NodeValue instances. + */ #include "cvc4_private.h" diff --git a/src/expr/node_visitor.h b/src/expr/node_visitor.h index 9816e37e8..52755e9fa 100644 --- a/src/expr/node_visitor.h +++ b/src/expr/node_visitor.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file node_visitor.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple visitor for nodes - ** - ** A simple visitor for nodes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Andrew Reynolds, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple visitor for nodes. + */ #pragma once diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index c0ba27a64..289a5be5b 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof.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 proof - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of proof. + */ #include "expr/proof.h" diff --git a/src/expr/proof.h b/src/expr/proof.h index 5cea5354e..de599a252 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Proof utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Proof utility. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index ca1b96f1e..5cd7d225d 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.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 proof checker - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of proof checker. + */ #include "expr/proof_checker.h" diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index 06e813e2d..a6aa1e557 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Proof checker utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Proof checker utility. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp index 6947cfd44..e89bd6692 100644 --- a/src/expr/proof_ensure_closed.cpp +++ b/src/expr/proof_ensure_closed.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_ensure_closed.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 debug checks for ensuring proofs are closed - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of debug checks for ensuring proofs are closed. + */ #include "expr/proof_ensure_closed.h" diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h index 8a7461287..71bfa86fd 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/expr/proof_ensure_closed.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_ensure_closed.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Debug checks for ensuring proofs are closed - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Debug checks for ensuring proofs are closed. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index a315ba2cd..7c034c10d 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_generator.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 proof generator utility - **/ +/****************************************************************************** + * 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 proof generator utility. + */ #include "expr/proof_generator.h" diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 2cc64e083..e95cf3a3c 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 The abstract proof generator class - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The abstract proof generator class. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp index 9450ddc99..92daad8ed 100644 --- a/src/expr/proof_node.cpp +++ b/src/expr/proof_node.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node.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 proof node utility - **/ +/****************************************************************************** + * 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 proof node utility. + */ #include "expr/proof_node.h" diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index b849e2391..abac0431c 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Alex Ozdemir - ** 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 Proof node utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Alex Ozdemir + * + * 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. + * **************************************************************************** + * + * Proof node utility. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp index f307b78b9..957893cb3 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/expr/proof_node_algorithm.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_algorithm.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa - ** 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 proof node algorithm utilities - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of proof node algorithm utilities. + */ #include "expr/proof_node_algorithm.h" diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index 6aa045481..58d0098d1 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_algorithm.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, 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 Proof node algorithm utilities. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Proof node algorithm utilities. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 7ac228f80..d4a8b604f 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa - ** 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 proof node manager - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Implementation of proof node manager. + */ #include "expr/proof_node_manager.h" diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 251d43ed3..d83143e82 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, 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 Proof node manager utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Proof node manager utility. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp index b53ce368d..033232959 100644 --- a/src/expr/proof_node_to_sexpr.cpp +++ b/src/expr/proof_node_to_sexpr.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_to_sexpr.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa - ** 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 proof node to s-expression - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Implementation of proof node to s-expression. + */ #include "expr/proof_node_to_sexpr.h" diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h index 31b04466e..46fb32308 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/expr/proof_node_to_sexpr.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_to_sexpr.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, 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 Conversion from ProofNode to s-expressions - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Conversion from ProofNode to s-expressions. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index cbd457cd7..e2fd0c566 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_updater.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa - ** 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 a utility for updating proof nodes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of a utility for updating proof nodes. + */ #include "expr/proof_node_updater.h" diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 6f3e5b420..be54de207 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_node_updater.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, 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 utility for updating proof nodes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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 utility for updating proof nodes. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 8141a017c..92944a7f4 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_rule.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, 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 Implementation of proof rule - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Implementation of proof rule. + */ #include "expr/proof_rule.h" diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 8aaf697d4..11b4c1bb0 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_rule.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, 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 Proof rule enumeration - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Proof rule enumeration. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h index f684045c6..7193f5572 100644 --- a/src/expr/proof_set.h +++ b/src/expr/proof_set.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_set.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Proof set utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Proof set utility. + */ #include "cvc4_private.h" diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp index 4ecee9130..84cfc040c 100644 --- a/src/expr/proof_step_buffer.cpp +++ b/src/expr/proof_step_buffer.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_step_buffer.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 proof step and proof step buffer utilities. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of proof step and proof step buffer utilities. + */ #include "expr/proof_step_buffer.h" diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h index ef57540c7..b74ced0f1 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/expr/proof_step_buffer.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_step_buffer.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Proof step and proof step buffer utilities. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Proof step and proof step buffer utilities. + */ #include "cvc4_private.h" diff --git a/src/expr/record.cpp b/src/expr/record.cpp index 367315d84..0792de20c 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file record.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 A class representing a record definition - ** - ** A class representing a record definition. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A class representing a record definition. + */ #include "expr/record.h" diff --git a/src/expr/record.h b/src/expr/record.h index fa6a34395..555d0ae08 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file record.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 A class representing a Record definition - ** - ** A class representing a Record definition. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A class representing a Record definition. + */ #include "cvc4_public.h" diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index df40c8534..9e68f6cd7 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sequence.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Implementation of the sequence data type. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of the sequence data type. + */ #include "expr/sequence.h" diff --git a/src/expr/sequence.h b/src/expr/sequence.h index e75c38956..b2018d0eb 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sequence.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 The sequence data type. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, 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 sequence data type. + */ #include "cvc4_public.h" diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 8ca8810b1..1d66cbee2 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file skolem_manager.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 skolem manager class - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of skolem manager class. + */ #include "expr/skolem_manager.h" diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index b69853a85..426202b7e 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file skolem_manager.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 Skolem manager utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Skolem manager utility. + */ #include "cvc4_private.h" diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index 8c1d67c47..7e9c83d06 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file subs.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 Simple substitution utility - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Simple substitution utility. + */ #include "expr/subs.h" diff --git a/src/expr/subs.h b/src/expr/subs.h index d351eeaa7..56158d36c 100644 --- a/src/expr/subs.h +++ b/src/expr/subs.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file subs.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 Simple substitution utility - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Simple substitution utility. + */ #ifndef CVC5__EXPR__SUBS_H #define CVC5__EXPR__SUBS_H diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index 82585eabe..c5c603cad 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sygus_datatype.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa - ** 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 class for constructing SyGuS datatypes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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. + * **************************************************************************** + * + * Implementation of class for constructing SyGuS datatypes. + */ #include "expr/sygus_datatype.h" diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h index b3130a028..ef0fa4de7 100644 --- a/src/expr/sygus_datatype.h +++ b/src/expr/sygus_datatype.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sygus_datatype.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa - ** 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 class for constructing SyGuS datatypes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A class for constructing SyGuS datatypes. + */ #include "cvc4_private.h" #ifndef CVC5__EXPR__SYGUS_DATATYPE_H diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index 9610e443d..4e9b7822b 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file symbol_manager.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 The symbol manager - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 symbol manager. + */ #include "expr/symbol_manager.h" diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 96bc3954d..9f951ebfb 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file symbol_manager.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 symbol manager - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The symbol manager. + */ #include "cvc4_public.h" diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 9e60680c7..9e1fe9582 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -1,20 +1,18 @@ -/********************* */ -/*! \file symbol_table.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Convenience class for scoping variable and type - ** declarations (implementation) - ** - ** Convenience class for scoping variable and type declarations - ** (implementation). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Convenience class for scoping variable and type declarations + * (implementation). + */ #include "expr/symbol_table.h" diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 98cba9ff8..5539adefb 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file symbol_table.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Convenience class for scoping variable and type declarations. - ** - ** Convenience class for scoping variable and type declarations. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Convenience class for scoping variable and type declarations. + */ #include "cvc4_public.h" diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp index d51e07e83..00e961628 100644 --- a/src/expr/tconv_seq_proof_generator.cpp +++ b/src/expr/tconv_seq_proof_generator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file tconv_seq_proof_generator.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 Term conversion sequence proof generator utility - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Term conversion sequence proof generator utility. + */ #include "expr/tconv_seq_proof_generator.h" diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h index 2e14acb98..960a2f081 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/expr/tconv_seq_proof_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file tconv_seq_proof_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Term conversion sequence proof generator utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Term conversion sequence proof generator utility. + */ #include "cvc4_private.h" diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp index 11a992d16..0480a046a 100644 --- a/src/expr/term_canonize.cpp +++ b/src/expr/term_canonize.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_canonize.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 term canonize. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of term canonize. + */ #include "expr/term_canonize.h" diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h index a032f3a84..188359e58 100644 --- a/src/expr/term_canonize.h +++ b/src/expr/term_canonize.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_canonize.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 constructing canonical terms. - **/ +/****************************************************************************** + * 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 constructing canonical terms. + */ #include "cvc4_private.h" diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp index 883fa3e08..d339a3d28 100644 --- a/src/expr/term_context.cpp +++ b/src/expr/term_context.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_context.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 term context utilities. - **/ +/****************************************************************************** + * 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 term context utilities. + */ #include "expr/term_context.h" diff --git a/src/expr/term_context.h b/src/expr/term_context.h index 5bdab4fca..320c8e65b 100644 --- a/src/expr/term_context.h +++ b/src/expr/term_context.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_context.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 Term context utilities. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Term context utilities. + */ #include "cvc4_private.h" diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp index 564459d37..09f1de7f1 100644 --- a/src/expr/term_context_node.cpp +++ b/src/expr/term_context_node.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_context_node.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 Term context node utility. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Term context node utility. + */ #include "expr/term_context_node.h" diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h index 1c3542b57..cc60f01b5 100644 --- a/src/expr/term_context_node.h +++ b/src/expr/term_context_node.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_context_node.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Term context node utility. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Term context node utility. + */ #include "cvc4_private.h" diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp index 8a0fd91c9..a8839564b 100644 --- a/src/expr/term_context_stack.cpp +++ b/src/expr/term_context_stack.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_context_stack.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 Term context stack - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Term context stack. + */ #include "expr/term_context_stack.h" diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h index 48892e654..51cf922aa 100644 --- a/src/expr/term_context_stack.h +++ b/src/expr/term_context_stack.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_context_stack.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 Term context - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Term context. + */ #include "cvc4_private.h" diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index df4708f74..22e1309d2 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_conversion_proof_generator.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 term conversion proof generator utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of term conversion proof generator utility. + */ #include "expr/term_conversion_proof_generator.h" diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index 961ac61cc..946c31acb 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_conversion_proof_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Term conversion proof generator utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Term conversion proof generator utility. + */ #include "cvc4_private.h" diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index 5b806e671..077158749 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_checker.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 A type checker - ** - ** A type checker. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A type checker. + */ #include "cvc4_private.h" diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index d99d5e82d..3944fac11 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_checker_template.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, 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 TypeChecker implementation - ** - ** TypeChecker implementation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * TypeChecker implementation. + */ #include <sstream> diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h index 207c242b8..5bdfbb02f 100644 --- a/src/expr/type_checker_util.h +++ b/src/expr/type_checker_util.h @@ -1,21 +1,22 @@ -/********************* */ -/*! \file type_checker_util.h - ** \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 Templates for simple type rules - ** - ** This file defines templates for simple type rules. If a kind has the a - ** type rule where each argument matches exactly a specific sort, these - ** templates can be used to define typechecks without writing dedicated classes - ** for them. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Templates for simple type rules + * + * This file defines templates for simple type rules. If a kind has the a + * type rule where each argument matches exactly a specific sort, these + * templates can be used to define typechecks without writing dedicated classes + * for them. + */ #include "cvc4_private.h" diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp index 9389ce4b8..df6639b78 100644 --- a/src/expr/type_matcher.cpp +++ b/src/expr/type_matcher.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file type_matcher.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Implementation of a class representing a type matcher - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of a class representing a type matcher. + */ #include "type_matcher.h" diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h index 6df955c06..0d5cc9265 100644 --- a/src/expr/type_matcher.h +++ b/src/expr/type_matcher.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file type_matcher.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 A class representing a type matcher - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * A class representing a type matcher. + */ #include "cvc4_private.h" diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 2dafe40da..2da1b7ad2 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_node.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Reference-counted encapsulation of a pointer to node information. - ** - ** Reference-counted encapsulation of a pointer to node information. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Reference-counted encapsulation of a pointer to node information. + */ #include "expr/type_node.h" #include <vector> diff --git a/src/expr/type_node.h b/src/expr/type_node.h index a1c4fa92b..9b2f4b4d0 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_node.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, 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 Reference-counted encapsulation of a pointer to node information. - ** - ** Reference-counted encapsulation of a pointer to node information. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Dejan Jovanovic, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Reference-counted encapsulation of a pointer to node information. + */ #include "cvc4_private.h" diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index c6fb29b71..799233378 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_properties_template.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 Template for the Type properties header - ** - ** Template for the Type properties header. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Template for the Type properties header. + */ #include "cvc4_private.h" diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index bd934e391..039a77eb3 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file uninterpreted_constant.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds, 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 constants of uninterpreted sorts - ** - ** Representation of constants of uninterpreted sorts. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Andrew Reynolds, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Representation of constants of uninterpreted sorts. + */ #include "expr/uninterpreted_constant.h" diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 841b32626..edf2cf154 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file uninterpreted_constant.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, 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 constants of uninterpreted sorts - ** - ** Representation of constants of uninterpreted sorts. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, 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. + * **************************************************************************** + * + * Representation of constants of uninterpreted sorts. + */ #include "cvc4_public.h" |