diff options
Diffstat (limited to 'src/theory/sets')
25 files changed, 354 insertions, 353 deletions
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index bbe100e98..8ba3cd9ea 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -1,17 +1,18 @@ -/********************* */ -/*! \file cardinality_extension.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed, 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 an extension of the theory sets for handling - ** cardinality constraints. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of an extension of the theory sets for handling + * cardinality constraints. + */ #include "theory/sets/cardinality_extension.h" diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index 7f426d003..24981d4be 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file cardinality_extension.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An extension of the theory sets for handling cardinality constraints - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An extension of the theory sets for handling cardinality constraints. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 2523512cc..a2d7b33a5 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file inference_manager.cpp - ** \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 Implementation of the inference manager for the theory of sets - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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 sets. + */ #include "theory/sets/inference_manager.h" diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index 0d7d437be..68cbfa4a7 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file inference_manager.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 inference manager for the theory of sets. - **/ +/****************************************************************************** + * 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 inference manager for the theory of sets. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index ae967cc39..7cbad751f 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file normal_form.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Kshitij Bansal, 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 set constants. - ** - ** Normal form for set constants. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Kshitij Bansal, 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 set constants. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 545e3c08c..46eeecd58 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file rels_utils.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 Sets theory implementation. - ** - ** Extension to Sets theory. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Extension to Sets theory. + */ #ifndef SRC_THEORY_SETS_RELS_UTILS_H_ #define SRC_THEORY_SETS_RELS_UTILS_H_ diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp index 0fc411788..993457fe8 100644 --- a/src/theory/sets/singleton_op.cpp +++ b/src/theory/sets/singleton_op.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file singleton_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 singleton operator for sets - **/ +/****************************************************************************** + * 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 singleton operator for sets. + */ #include "singleton_op.h" diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h index 591b9f0ee..02d646290 100644 --- a/src/theory/sets/singleton_op.h +++ b/src/theory/sets/singleton_op.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file singleton_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 singleton operator for sets - **/ +/****************************************************************************** + * 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 singleton operator for sets. + */ #include "cvc4_public.h" diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp index 8c0d125d5..285d53c4a 100644 --- a/src/theory/sets/skolem_cache.cpp +++ b/src/theory/sets/skolem_cache.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file skolem_cache.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 a cache of skolems for theory of sets. - **/ +/****************************************************************************** + * 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 a cache of skolems for theory of sets. + */ #include "theory/sets/skolem_cache.h" diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h index f3e86cc96..3d1ce3628 100644 --- a/src/theory/sets/skolem_cache.h +++ b/src/theory/sets/skolem_cache.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file skolem_cache.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 cache of skolems for theory of sets. - **/ +/****************************************************************************** + * 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 cache of skolems for theory of sets. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 31f0d4aa3..2aaa82706 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file solver_state.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level 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 sets state object - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed, Paul Meng + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the 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 sets state object. + */ #include "theory/sets/solver_state.h" diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index e6c742c86..db63596cc 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file solver_state.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sets state object - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sets state object. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index 43eed46a6..af9d9e42d 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_registry.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed, 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 sets term registry object - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed, 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 sets term registry object. + */ #include "theory/sets/term_registry.h" diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 2cff01b86..6b5a3d640 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file term_registry.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sets state object - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sets state object. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index eb2363eb7..fdb744d67 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Sets theory. - ** - ** Sets theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Sets theory. + */ #include "theory/sets/theory_sets.h" diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 5aa145a15..acb6b1910 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Sets theory. - ** - ** Sets theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Sets theory. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 5001b51dd..eea90da41 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_private.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mudathir Mohamed, 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 Sets theory implementation. - ** - ** Sets theory implementation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mudathir Mohamed, 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. + * **************************************************************************** + * + * Sets theory implementation. + */ #include "theory/sets/theory_sets_private.h" diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 94baa3c0e..7f492bc88 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_private.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Kshitij Bansal, 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 Sets theory implementation. - ** - ** Sets theory implementation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Kshitij Bansal, 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. + * **************************************************************************** + * + * Sets theory implementation. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index aa79f903b..0e14a6c34 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_rels.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, 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 Sets theory implementation. - ** - ** Extension to Sets theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Paul Meng, 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. + * **************************************************************************** + * + * Extension to Sets theory. + */ #include "theory/sets/theory_sets_rels.h" diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index badf14bd0..76edde5ae 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_rels.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, 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 Sets theory implementation. - ** - ** Extension to Sets theory. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Paul Meng, 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. + * **************************************************************************** + * + * Extension to Sets theory. + */ #ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_ #define SRC_THEORY_SETS_THEORY_SETS_RELS_H_ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 9007cc250..d05318cc8 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_rewriter.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Kshitij Bansal, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sets theory rewriter. - ** - ** Sets theory rewriter. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Kshitij Bansal, Paul Meng + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sets theory rewriter. + */ #include "theory/sets/theory_sets_rewriter.h" diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index 9c81c1e67..e54b65d92 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_rewriter.h - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, 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 Sets theory rewriter. - ** - ** Sets theory rewriter. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Kshitij Bansal, 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. + * **************************************************************************** + * + * Sets theory rewriter. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp index 87fcd2d8f..503a33ebd 100644 --- a/src/theory/sets/theory_sets_type_enumerator.cpp +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_type_enumerator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, 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 set enumerator implementation - ** - ** set enumerator implementation - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, 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. + * **************************************************************************** + * + * Set enumerator implementation. + */ #include "theory/sets/theory_sets_type_enumerator.h" diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 457aede12..15ea9a59f 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file theory_sets_type_enumerator.h - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief type enumerator for sets - ** - ** A set enumerator that iterates over the power set of the element type - ** starting with the empty set as the initial value - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Mathias Preiner, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Type enumerator for sets. + * + * A set enumerator that iterates over the power set of the element type + * starting with the empty set as the initial value. + */ #include "cvc4_private.h" diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 7b8aa9778..1cac17d02 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_sets_type_rules.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Kshitij Bansal, 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 Sets theory type rules. - ** - ** Sets theory type rules. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Kshitij Bansal, 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. + * **************************************************************************** + * + * Sets theory type rules. + */ #include "cvc4_private.h" |