diff options
Diffstat (limited to 'src/theory/bags')
28 files changed, 394 insertions, 368 deletions
diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 478ce58cd..47eb90f45 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file bag_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 solver for the theory of bags. - ** - ** solver for the theory of bags. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Solver for the theory of bags. + */ #include "theory/bags/bag_solver.h" diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index 191fd481c..4c15b0243 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file bag_solver.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 solver for the theory of bags. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Solver for the theory of bags. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index f4670f8be..6e3b38d8d 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file bags_rewriter.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 Bags theory rewriter. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Gereon Kremer, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Bags theory rewriter. + */ #include "theory/bags/bags_rewriter.h" diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 26686bcc0..2cdcffec1 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file bags_rewriter.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 Bags theory rewriter. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Bags theory rewriter. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/bags_statistics.cpp b/src/theory/bags/bags_statistics.cpp index 6c88ffb43..018dbb231 100644 --- a/src/theory/bags/bags_statistics.cpp +++ b/src/theory/bags/bags_statistics.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file bags_statistics.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 Statistics for the theory of 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. + * **************************************************************************** + * + * Statistics for the theory of bags. + */ #include "theory/bags/bags_statistics.h" diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h index 58765a996..be95cf7ca 100644 --- a/src/theory/bags/bags_statistics.h +++ b/src/theory/bags/bags_statistics.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file bags_statistics.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 Statistics for the theory of bags - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Statistics for the theory of bags. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp index c0fac0753..9080f29e9 100644 --- a/src/theory/bags/infer_info.cpp +++ b/src/theory/bags/infer_info.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file infer_info.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 inference information utility. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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 inference information utility. + */ #include "theory/bags/infer_info.h" diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h index 633c3a828..a55755e68 100644 --- a/src/theory/bags/infer_info.h +++ b/src/theory/bags/infer_info.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file infer_info.h - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 Inference information utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Inference information utility. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 57a306820..6286f20b7 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file inference_generator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 Inference generator utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Inference generator utility. + */ #include "inference_generator.h" diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 639fd3215..32a49e611 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file inference_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 Inference generator utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Inference generator utility. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp index 422fb53d0..797ec0f4d 100644 --- a/src/theory/bags/inference_manager.cpp +++ b/src/theory/bags/inference_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file inference_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, Morgan Deters, 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 the inference manager for the theory of bags - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Gereon Kremer, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of the inference manager for the theory of bags. + */ #include "theory/bags/inference_manager.h" diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h index f17a6828b..fff6c7690 100644 --- a/src/theory/bags/inference_manager.h +++ b/src/theory/bags/inference_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file inference_manager.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 The inference manager for the theory of bags. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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 inference manager for the theory of bags. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp index 168379390..ed3d4cf26 100644 --- a/src/theory/bags/make_bag_op.cpp +++ b/src/theory/bags/make_bag_op.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file make_bag_op.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 MK_BAG operator - **/ +/****************************************************************************** + * 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 MK_BAG operator. + */ #include "make_bag_op.h" diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h index 33de51ed7..aa602d364 100644 --- a/src/theory/bags/make_bag_op.h +++ b/src/theory/bags/make_bag_op.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file make_bag_op.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 MK_BAG operator - **/ +/****************************************************************************** + * 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 MK_BAG operator. + */ #include "cvc4_public.h" diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp index 1773346f0..08142e6f9 100644 --- a/src/theory/bags/normal_form.cpp +++ b/src/theory/bags/normal_form.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file normal_form.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 Normal form for bag constants. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Normal form for bag constants. + */ #include "normal_form.h" #include "theory/sets/normal_form.h" diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h index 9eb2d8137..362dedb34 100644 --- a/src/theory/bags/normal_form.h +++ b/src/theory/bags/normal_form.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file normal_form.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 Normal form for bag constants. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Normal form for bag constants. + */ #include <expr/node.h> diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp index 4d6929346..ff77c4187 100644 --- a/src/theory/bags/rewrites.cpp +++ b/src/theory/bags/rewrites.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file rewrites.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 Implementation of inference information utility. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Implementation of inference information utility. + */ #include "theory/bags/rewrites.h" diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h index 54bf72c2f..cde671f1c 100644 --- a/src/theory/bags/rewrites.h +++ b/src/theory/bags/rewrites.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file rewrites.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 Type for rewrites for 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. + * **************************************************************************** + * + * Type for rewrites for bags. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index aa714a61b..6c80e00bd 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file solver_state.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 Implementation of bags state object - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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 bags state object. + */ #include "theory/bags/solver_state.h" diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h index 9309a704f..8560388d0 100644 --- a/src/theory/bags/solver_state.h +++ b/src/theory/bags/solver_state.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file solver_state.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 Bags state object - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Bags state object. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index dd3820c82..2db38e62b 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_registry.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 Implementation of bags term registry object - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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 bags term registry object. + */ #include "theory/bags/term_registry.h" diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index a9a03abe6..6e3a5fadb 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_registry.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 Bags state object - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Bags state object. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 933f1b1a1..89312f99a 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 Bags theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Haniel Barbosa, 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. + * **************************************************************************** + * + * Bags theory. + */ #include "theory/bags/theory_bags.h" diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index f1122ed6b..482181ad2 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags.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 Bags theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Bags theory. + */ #include "cvc4_private.h" diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp index f34d304fb..4695c1db7 100644 --- a/src/theory/bags/theory_bags_type_enumerator.cpp +++ b/src/theory/bags/theory_bags_type_enumerator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags_type_enumerator.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 bag enumerator implementation - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Bag enumerator implementation + */ #include "theory/bags/theory_bags_type_enumerator.h" @@ -83,4 +84,4 @@ bool BagEnumerator::isFinished() } // namespace bags } // namespace theory -} // namespace cvc5
\ No newline at end of file +} // namespace cvc5 diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h index 74325e2c5..f4efb7ce2 100644 --- a/src/theory/bags/theory_bags_type_enumerator.h +++ b/src/theory/bags/theory_bags_type_enumerator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags_type_enumerator.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 type enumerator for 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. + * **************************************************************************** + * + * Type enumerator for bags + */ #include "cvc4_private.h" @@ -88,4 +89,4 @@ class BagEnumerator : public TypeEnumeratorBase<BagEnumerator> } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H */
\ No newline at end of file +#endif /* CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index f198d68e9..66117d64a 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags_type_rules.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 Bags theory type rules. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Bags theory type rules. + */ #include "theory/bags/theory_bags_type_rules.h" diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index 599b3879a..06cc74e2a 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_bags_type_rules.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 Bags theory type rules. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Bags theory type rules. + */ #include "cvc4_private.h" |