diff options
Diffstat (limited to 'src/theory/arith/nl')
73 files changed, 1028 insertions, 983 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 4cd9077ca..80a9ada2d 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -1,19 +1,18 @@ -/********************* */ -/*! \file cdcac.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements the CDCAC approach. - ** - ** Implements the CDCAC approach as described in - ** https://arxiv.org/pdf/2003.05633.pdf. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements the CDCAC approach as described in + * https://arxiv.org/pdf/2003.05633.pdf. + */ #include "theory/arith/nl/cad/cdcac.h" diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 58aa41bd1..eafe979a1 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -1,19 +1,18 @@ -/********************* */ -/*! \file cdcac.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements the CDCAC approach. - ** - ** Implements the CDCAC approach as described in - ** https://arxiv.org/pdf/2003.05633.pdf. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements the CDCAC approach as described in + * https://arxiv.org/pdf/2003.05633.pdf. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp index 3ceb36bd3..b975a0850 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.cpp +++ b/src/theory/arith/nl/cad/cdcac_utils.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdcac_utils.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements utilities for cdcac. - ** - ** Implements utilities for cdcac. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements utilities for cdcac. + */ #include "theory/arith/nl/cad/cdcac_utils.h" diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h index 50f2f8bc9..f0f3c357b 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.h +++ b/src/theory/arith/nl/cad/cdcac_utils.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file cdcac_utils.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements utilities for cdcac. - ** - ** Implements utilities for cdcac. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements utilities for cdcac. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp index b244bd358..628859a8f 100644 --- a/src/theory/arith/nl/cad/constraints.cpp +++ b/src/theory/arith/nl/cad/constraints.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file constraints.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements a container for CAD constraints. - ** - ** Implements a container for CAD constraints. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements a container for CAD constraints. + */ #include "theory/arith/nl/cad/constraints.h" diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index 1ddbfc821..3655ef5c0 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file constraints.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements a container for CAD constraints. - ** - ** Implements a container for CAD constraints. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements a container for CAD constraints. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp index 8aea538f1..6d86b8104 100644 --- a/src/theory/arith/nl/cad/projections.cpp +++ b/src/theory/arith/nl/cad/projections.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file projections.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements utilities for CAD projection operators. - ** - ** Implements utilities for CAD projection operators. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements utilities for CAD projection operators. + */ #include "theory/arith/nl/cad/projections.h" diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index f3c8aa0f1..25deb0d0d 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file projections.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements utilities for CAD projection operators. - ** - ** Implements utilities for CAD projection operators. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements utilities for CAD projection operators. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp index 3cd8fe98e..562b57722 100644 --- a/src/theory/arith/nl/cad/proof_checker.cpp +++ b/src/theory/arith/nl/cad/proof_checker.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of CAD proof checker - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of CAD proof checker. + */ #include "theory/arith/nl/cad/proof_checker.h" diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index d2013e14b..36d18c854 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief CAD proof checker utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * CAD proof checker utility. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index 291447647..5c4391d68 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_generator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of CAD proof generator - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of CAD proof generator. + */ #include "theory/arith/nl/cad/proof_generator.h" diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index 993524504..440f25e49 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_generator.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements the proof generator for CAD - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements the proof generator for CAD. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp index e7c8b214a..daf3f48a8 100644 --- a/src/theory/arith/nl/cad/variable_ordering.cpp +++ b/src/theory/arith/nl/cad/variable_ordering.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file variable_ordering.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements variable orderings tailored to CAD. - ** - ** Implements variable orderings tailored to CAD. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements variable orderings tailored to CAD. + */ #include "theory/arith/nl/cad/variable_ordering.h" diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index fb40a7b7d..00fbc8f49 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/cad/variable_ordering.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file variable_ordering.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements variable orderings tailored to CAD. - ** - ** Implements variable orderings tailored to CAD. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements variable orderings tailored to CAD. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 202788ba1..5d30d5db4 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file cad_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of new non-linear solver - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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 new non-linear solver. + */ #include "theory/arith/nl/cad_solver.h" diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 1d51cf9c5..b9becec44 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file cad_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief CAD-based solver based on https://arxiv.org/pdf/2003.05633.pdf. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * CAD-based solver based on https://arxiv.org/pdf/2003.05633.pdf. + */ #ifndef CVC5__THEORY__ARITH__CAD_SOLVER_H #define CVC5__THEORY__ARITH__CAD_SOLVER_H diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp index 688bab86d..2f479f8f0 100644 --- a/src/theory/arith/nl/ext/constraint.cpp +++ b/src/theory/arith/nl/ext/constraint.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file constraint.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 Implementation of utilities for non-linear constraints - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of utilities for non-linear constraints. + */ #include "theory/arith/nl/ext/constraint.h" diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h index ef9f8fef3..d3ee1df42 100644 --- a/src/theory/arith/nl/ext/constraint.h +++ b/src/theory/arith/nl/ext/constraint.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file constraint.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 Utilities for non-linear constraints - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for non-linear constraints. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__CONSTRAINT_H #define CVC5__THEORY__ARITH__NL__EXT__CONSTRAINT_H diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index e20224207..9ebd42d55 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file ext_state.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Common data shared by multiple checks - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Common data shared by multiple checks. + */ #include "theory/arith/nl/ext/ext_state.h" diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 1571f3173..b2279344d 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file ext_state.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Common data shared by multiple checks - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Common data shared by multiple checks. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H #define CVC5__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 09e1d4f10..c4bba6ec8 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file factoring_check.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Implementation of factoring check - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of factoring check. + */ #include "theory/arith/nl/ext/factoring_check.h" diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index feff91112..9ae94f22d 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file factoring_check.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 Check for factoring lemma - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Check for factoring lemma. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H #define CVC5__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index 784c07691..c969fe0e7 100644 --- a/src/theory/arith/nl/ext/monomial.cpp +++ b/src/theory/arith/nl/ext/monomial.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file monomial.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Implementation of utilities for monomials - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Implementation of utilities for monomials. + */ #include "theory/arith/nl/ext/monomial.h" diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h index bbae33eda..130cf37bb 100644 --- a/src/theory/arith/nl/ext/monomial.h +++ b/src/theory/arith/nl/ext/monomial.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file monomial.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for monomials - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for monomials. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_H #define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_H diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 344218148..44f59c521 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file monomial_bounds_check.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Check for monomial bound inference lemmas - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Check for monomial bound inference lemmas. + */ #include "theory/arith/nl/ext/monomial_bounds_check.h" diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h index e95cda778..3a21e7f58 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.h +++ b/src/theory/arith/nl/ext/monomial_bounds_check.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file monomial_bounds_check.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Check for monomial bound inference lemmas - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Check for monomial bound inference lemmas. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H #define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index a30d4aff9..6df35c71d 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file monomial_check.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Check for some monomial lemmas - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Check for some monomial lemmas. + */ #include "theory/arith/nl/ext/monomial_check.h" diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index f84d69b6b..3cf239bf5 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file monomial_check.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Check for some monomial lemmas - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Check for some monomial lemmas. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H #define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index b6c4572f5..67679d7a6 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Implementation of NlExt proof checker - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of NlExt proof checker. + */ #include "theory/arith/nl/ext/proof_checker.h" diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index 5e901ddf5..21807a79d 100644 --- a/src/theory/arith/nl/ext/proof_checker.h +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief NlExt proof checker utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * NlExt proof checker utility. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 7392d45f4..ace7e0868 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file split_zero_check.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of split zero check - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of split zero check. + */ #include "theory/arith/nl/ext/split_zero_check.h" diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index bd07a79f6..b42c7932d 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file split_zero_check.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Check for split zero lemma - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Check for split zero lemma. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H #define CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 711bc9816..a66f1396c 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file tangent_plane_check.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Implementation of tangent_plane check - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Implementation of tangent_plane check. + */ #include "theory/arith/nl/ext/tangent_plane_check.h" diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h index b5fd797aa..c9b7a3c7f 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.h +++ b/src/theory/arith/nl/ext/tangent_plane_check.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file tangent_plane_check.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 Check for tangent_plane lemma - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Check for tangent_plane lemma. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H #define CVC5__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 8fa1a56c9..c778a89cc 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file ext_theory_callback.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Tianyi Liang - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The extended theory callback for non-linear arithmetic - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Tianyi Liang + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The extended theory callback for non-linear arithmetic + */ #include "theory/arith/nl/ext_theory_callback.h" diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index 56faacddd..a810d9d53 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file ext_theory_callback.h - ** \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 The extended theory callback for non-linear arithmetic - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The extended theory callback for non-linear arithmetic. + */ #ifndef CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H #define CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 0e339857b..cb2fdab6f 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file iand_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Makai Mann, 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 integer and (IAND) solver - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Makai Mann, 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 integer and (IAND) solver. + */ #include "theory/arith/nl/iand_solver.h" diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 52f97bf0e..676390478 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file iand_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Makai Mann, 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 Solver for integer and (IAND) constraints - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Makai Mann, 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 integer and (IAND) constraints. + */ #ifndef CVC5__THEORY__ARITH__NL__IAND_SOLVER_H #define CVC5__THEORY__ARITH__NL__IAND_SOLVER_H diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index e08068b7e..af0f5e169 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -1,17 +1,17 @@ -/********************* */ -/*! \file iand_utils.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Makai Mann, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities to maintain finite tables that represent - ** the value of iand. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Makai Mann, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities to maintain finite tables that represent the value of iand. + */ #include "theory/arith/nl/iand_utils.h" diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index cad5c80d5..d4239f606 100644 --- a/src/theory/arith/nl/iand_utils.h +++ b/src/theory/arith/nl/iand_utils.h @@ -1,17 +1,17 @@ -/********************* */ -/*! \file iand_utils.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Makai Mann, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities to maintain finite tables that represent - ** the value of iand. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Makai Mann, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities to maintain finite tables that represent the value of iand. + */ #ifndef CVC5__THEORY__ARITH__IAND_TABLE_H #define CVC5__THEORY__ARITH__IAND_TABLE_H diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp index 4a6d0748a..4d024c155 100644 --- a/src/theory/arith/nl/icp/candidate.cpp +++ b/src/theory/arith/nl/icp/candidate.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file candidate.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Represents a contraction candidate for ICP-style propagation. + */ #include "theory/arith/nl/icp/candidate.h" diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index d65db52b5..932698d71 100644 --- a/src/theory/arith/nl/icp/candidate.h +++ b/src/theory/arith/nl/icp/candidate.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file candidate.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Represents a contraction candidate for ICP-style propagation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Represents a contraction candidate for ICP-style propagation. + */ #ifndef CVC5__THEORY__ARITH__ICP__CANDIDATE_H #define CVC5__THEORY__ARITH__ICP__CANDIDATE_H diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp index acf499a21..213736ac3 100644 --- a/src/theory/arith/nl/icp/contraction_origins.cpp +++ b/src/theory/arith/nl/icp/contraction_origins.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file contraction_origins.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements a way to track the origins of ICP-style contractions. + */ #include "theory/arith/nl/icp/contraction_origins.h" diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h index fd899cfd2..e31e99908 100644 --- a/src/theory/arith/nl/icp/contraction_origins.h +++ b/src/theory/arith/nl/icp/contraction_origins.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file contraction_origins.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implements a way to track the origins of ICP-style contractions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements a way to track the origins of ICP-style contractions. + */ #ifndef CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H #define CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 39504c3aa..ed50b85cf 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file icp_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 ICP-based solver for nonlinear arithmetic. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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 ICP-based solver for nonlinear arithmetic. + */ #include "theory/arith/nl/icp/icp_solver.h" diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 0efb2021f..e7eb83bd4 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file icp_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 ICP-based solver for nonlinear arithmetic. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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 ICP-based solver for nonlinear arithmetic. + */ #ifndef CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H #define CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index 6a914bc03..4814fb300 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file intersection.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implement intersection of intervals for propagation. + */ #include "theory/arith/nl/icp/intersection.h" diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index a82ad6b8e..1911a397f 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file intersection.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implement intersection of intervals for propagation. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implement intersection of intervals for propagation. + */ #ifndef CVC5__THEORY__ARITH__ICP__INTERSECTION_H #define CVC5__THEORY__ARITH__ICP__INTERSECTION_H diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index 42f2084e0..4b47ae954 100644 --- a/src/theory/arith/nl/icp/interval.h +++ b/src/theory/arith/nl/icp/interval.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file interval.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An interval with poly::Value bounds and origins for these bounds. + */ #ifndef CVC5__THEORY__ARITH__ICP__INTERVAL_H #define CVC5__THEORY__ARITH__ICP__INTERVAL_H diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index 9740e1b46..3e2ebe87e 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file nl_lemma_utils.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 utilities for the non-linear solver - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Implementation of utilities for the non-linear solver. + */ #include "theory/arith/nl/nl_lemma_utils.h" diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 474212821..dba5e6ad2 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file nl_lemma_utils.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for processing lemmas from the non-linear solver - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for processing lemmas from the non-linear solver. + */ #ifndef CVC5__THEORY__ARITH__NL__NL_LEMMA_UTILS_H #define CVC5__THEORY__ARITH__NL__NL_LEMMA_UTILS_H diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 882cd12a4..9b1246f67 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file nl_model.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Model object for the non-linear extension class - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Model object for the non-linear extension class. + */ #include "theory/arith/nl/nl_model.h" diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 4a50cd54f..600dbd02c 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file nl_model.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Model object for the non-linear extension 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. + * **************************************************************************** + * + * Model object for the non-linear extension class. + */ #ifndef CVC5__THEORY__ARITH__NL__NL_MODEL_H #define CVC5__THEORY__ARITH__NL__NL_MODEL_H diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 20d64b0d5..a3b32c6e9 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file nonlinear_extension.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "theory/arith/nl/nonlinear_extension.h" diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 5dd1374cd..e39f97402 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -1,19 +1,18 @@ -/********************* */ -/*! \file nonlinear_extension.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Extensions for incomplete handling of nonlinear multiplication. - ** - ** Extensions to the theory of arithmetic incomplete handling of nonlinear - ** multiplication via axiom instantiations. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Extensions to the theory of arithmetic incomplete handling of nonlinear + * multiplication via axiom instantiations. + */ #ifndef CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H #define CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index f708896a6..d80dacd78 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file poly_conversion.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for converting to and from LibPoly objects. - ** - ** Utilities for converting to and from LibPoly objects. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Utilities for converting to and from LibPoly objects. + */ #include "poly_conversion.h" diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index c97923f23..9e2b71ffe 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file poly_conversion.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Utilities for converting to and from LibPoly objects. - ** - ** Utilities for converting to and from LibPoly objects. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Utilities for converting to and from LibPoly objects. + */ #ifndef CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H #define CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp index 33a73ddd7..fa06fa73e 100644 --- a/src/theory/arith/nl/stats.cpp +++ b/src/theory/arith/nl/stats.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file stats.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 Statistics for non-linear arithmetic - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Statistics for non-linear arithmetic. + */ #include "theory/arith/nl/stats.h" diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index 3e947160e..e80a66aca 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file stats.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 Statistics for non-linear arithmetic - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Statistics for non-linear arithmetic. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index 4df53b103..01e319d37 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file strategy.cpp - ** \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 Implementation of non-linear solver - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Implementation of non-linear solver. + */ #include "theory/arith/nl/strategy.h" diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index 4fc115476..ba0d3370e 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file strategy.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Strategies for the nonlinear extension - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Strategies for the nonlinear extension. + */ #ifndef CVC5__THEORY__ARITH__NL__STRATEGY_H #define CVC5__THEORY__ARITH__NL__STRATEGY_H diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 5e2358b68..11e2b9cc8 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file exponential_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Implementation of solver for handling transcendental functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Implementation of solver for handling transcendental functions. + */ #include "theory/arith/nl/transcendental/exponential_solver.h" diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index a7ae92498..db540c40e 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file exponential_solver.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 Solving for handling exponential function. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Solving for handling exponential function. + */ #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index 4fc85666a..ca62fe394 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Implementation of proof checker for transcendentals - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of proof checker for transcendentals. + */ #include "theory/arith/nl/transcendental/proof_checker.h" diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index 83788b60e..1c0a00ca8 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.h +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Proof checker utility for transcendental solver - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Proof checker utility for transcendental solver. + */ #include "cvc4_private.h" diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 2a1f2ad91..26d959878 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sine_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, 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 Implementation of solver for handling transcendental functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, 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. + * **************************************************************************** + * + * Implementation of solver for handling transcendental functions. + */ #include "theory/arith/nl/transcendental/sine_solver.h" diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index 80b4fb10b..83de35f52 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sine_solver.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 Solving for handling exponential function. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Solving for handling exponential function. + */ #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index 5a9e87b7f..d64eb8f19 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file taylor_generator.cpp - ** \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 Generate taylor approximations transcendental lemmas. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Generate taylor approximations transcendental lemmas. + */ #include "theory/arith/nl/transcendental/taylor_generator.h" diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index 4ecf5aa9a..df4cb128c 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file taylor_generator.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 Generate taylor approximations transcendental lemmas. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Generate taylor approximations transcendental lemmas. + */ #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index b3fd40ce7..62d101686 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file transcendental_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Gereon Kremer, 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 Implementation of solver for handling transcendental functions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of solver for handling transcendental functions. + */ #include "theory/arith/nl/transcendental/transcendental_solver.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 1a2f59282..54bad2c1d 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file transcendental_solver.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 Solving for handling transcendental functions. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Solving for handling transcendental functions. + */ #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index e662c017e..c0f5d23b2 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file transcendental_state.cpp - ** \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 Implementation of solver for handling transcendental functions. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Implementation of solver for handling transcendental functions. + */ #include "theory/arith/nl/transcendental/transcendental_state.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 3d1c4a037..f98986fad 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file transcendental_state.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 Utilities for transcendental lemmas. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for transcendental lemmas. + */ #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H |