diff options
Diffstat (limited to 'src/preprocessing')
78 files changed, 1327 insertions, 1274 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 92027a303..7d21066d8 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -1,17 +1,18 @@ -/********************* */ -/*! \file assertion_pipeline.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief AssertionPipeline stores a list of assertions modified by - ** preprocessing passes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * AssertionPipeline stores a list of assertions modified by + * preprocessing passes. + */ #include "preprocessing/assertion_pipeline.h" diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index a04c03c22..e555da299 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -1,17 +1,18 @@ -/********************* */ -/*! \file assertion_pipeline.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief AssertionPipeline stores a list of assertions modified by - ** preprocessing passes - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Andrew Reynolds, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * AssertionPipeline stores a list of assertions modified by + * preprocessing passes. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 525d0b243..6b2f142fc 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -1,25 +1,26 @@ -/********************* */ -/*! \file ackermann.cpp - ** \verbatim - ** Top contributors (to current version): - ** Ying Sheng, Yoni Zohar, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Ackermannization preprocessing pass. - ** - ** This implements the Ackermannization preprocessing pass, which enables - ** very limited theory combination support for eager bit-blasting via - ** Ackermannization. It reduces constraints over the combination of the - ** theories of fixed-size bit-vectors and uninterpreted functions as - ** described in - ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for - ** Bit-vectors in Satisfiability Modulo Theories. - ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf - **/ +/****************************************************************************** + * Top contributors (to current version): + * Ying Sheng, Yoni Zohar, 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. + * **************************************************************************** + * + * Ackermannization preprocessing pass. + * + * This implements the Ackermannization preprocessing pass, which enables + * very limited theory combination support for eager bit-blasting via + * Ackermannization. It reduces constraints over the combination of the + * theories of fixed-size bit-vectors and uninterpreted functions as + * described in + * Liana Hadarean, An Efficient and Trustworthy Theory Solver for + * Bit-vectors in Satisfiability Modulo Theories. + * https://cs.nyu.edu/media/publications/hadarean_liana.pdf + */ #include "preprocessing/passes/ackermann.h" diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index 05709b227..c7d65d5cc 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -1,25 +1,26 @@ -/********************* */ -/*! \file ackermann.h - ** \verbatim - ** Top contributors (to current version): - ** Ying Sheng, Aina Niemetz, Yoni Zohar - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Ackermannization preprocessing pass. - ** - ** This implements the Ackermannization preprocessing pass, which enables - ** very limited theory combination support for eager bit-blasting via - ** Ackermannization. It reduces constraints over the combination of the - ** theories of fixed-size bit-vectors and uninterpreted functions as - ** described in - ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for - ** Bit-vectors in Satisfiability Modulo Theories. - ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf - **/ +/****************************************************************************** + * Top contributors (to current version): + * Ying Sheng, Aina Niemetz, Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Ackermannization preprocessing pass. + * + * This implements the Ackermannization preprocessing pass, which enables + * very limited theory combination support for eager bit-blasting via + * Ackermannization. It reduces constraints over the combination of the + * theories of fixed-size bit-vectors and uninterpreted functions as + * described in + * Liana Hadarean, An Efficient and Trustworthy Theory Solver for + * Bit-vectors in Satisfiability Modulo Theories. + * https://cs.nyu.edu/media/publications/hadarean_liana.pdf + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 12f3375b0..324cd89b9 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file apply_substs.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Apply substitutions preprocessing pass. - ** - ** Apply top level substitutions to assertions, rewrite, and store back into - ** assertions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, 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. + * **************************************************************************** + * + * Apply substitutions preprocessing pass. + * + * Apply top level substitutions to assertions, rewrite, and store back into + * assertions. + */ #include "preprocessing/passes/apply_substs.h" diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index 0dead915e..6b6155114 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file apply_substs.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, 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 Apply substitutions preprocessing pass. - ** - ** Apply top level substitutions to assertions, rewrite, and store back into - ** assertions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mathias Preiner, 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. + * **************************************************************************** + * + * Apply substitutions preprocessing pass. + * + * Apply top level substitutions to assertions, rewrite, and store back into + * assertions. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index ac7707d16..dfa0c378d 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -1,17 +1,18 @@ -/********************* */ -/*! \file bool_to_bv.cpp - ** \verbatim - ** Top contributors (to current version): - ** Makai Mann, Yoni Zohar, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level 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 BoolToBV preprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Makai Mann, Yoni Zohar, Clark Barrett + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the 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 BoolToBV preprocessing pass. + * + */ #include "preprocessing/passes/bool_to_bv.h" diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index c55ce2168..de6a82a13 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -1,17 +1,18 @@ -/********************* */ -/*! \file bool_to_bv.h - ** \verbatim - ** Top contributors (to current version): - ** Makai Mann, Yoni Zohar, 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 The BoolToBV preprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Makai Mann, Yoni Zohar, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The BoolToBV preprocessing pass. + * + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index b7a9e9c69..597481678 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -1,25 +1,26 @@ -/********************* */ -/*! \file bv_abstraction.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 The BvAbstraction preprocessing pass - ** - ** Abstract common structures over small domains to UF. This preprocessing - ** is particularly useful on QF_BV/mcm benchmarks and can be enabled via - ** option `--bv-abstraction`. - ** For more information see 3.4 Refactoring Isomorphic Circuits in [1]. - ** - ** [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for - ** Bit-vectors in Satisfiability Modulo Theories - ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Andrew Reynolds, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The BvAbstraction preprocessing pass. + * + * Abstract common structures over small domains to UF. This preprocessing + * is particularly useful on QF_BV/mcm benchmarks and can be enabled via + * option `--bv-abstraction`. + * For more information see 3.4 Refactoring Isomorphic Circuits in [1]. + * + * [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for + * Bit-vectors in Satisfiability Modulo Theories + * https://cs.nyu.edu/media/publications/hadarean_liana.pdf + */ #include "preprocessing/passes/bv_abstraction.h" diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index c5d30124c..7e07653da 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -1,25 +1,26 @@ -/********************* */ -/*! \file bv_abstraction.h - ** \verbatim - ** Top contributors (to current version): - ** 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 The BvAbstraction preprocessing pass - ** - ** Abstract common structures over small domains to UF. This preprocessing - ** is particularly useful on QF_BV/mcm benchmarks and can be enabled via - ** option `--bv-abstraction`. - ** For more information see 3.4 Refactoring Isomorphic Circuits in [1]. - ** - ** [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for - ** Bit-vectors in Satisfiability Modulo Theories - ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The BvAbstraction preprocessing pass. + * + * Abstract common structures over small domains to UF. This preprocessing + * is particularly useful on QF_BV/mcm benchmarks and can be enabled via + * option `--bv-abstraction`. + * For more information see 3.4 Refactoring Isomorphic Circuits in [1]. + * + * [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for + * Bit-vectors in Satisfiability Modulo Theories + * https://cs.nyu.edu/media/publications/hadarean_liana.pdf + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp index 54f967bfc..3ba2f8870 100644 --- a/src/preprocessing/passes/bv_eager_atoms.cpp +++ b/src/preprocessing/passes/bv_eager_atoms.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file bv_eager_atoms.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 Wrap assertions in BITVECTOR_EAGER_ATOM nodes. - ** - ** This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes - ** and allows to use eager bit-blasting in the BV solver. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Wrap assertions in BITVECTOR_EAGER_ATOM nodes. + * + * This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes + * and allows to use eager bit-blasting in the BV solver. + */ #include "preprocessing/passes/bv_eager_atoms.h" diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index 85d86e3f7..87fd87c91 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file bv_eager_atoms.h - ** \verbatim - ** Top contributors (to current version): - ** 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 Wrap assertions in BITVECTOR_EAGER_ATOM nodes. - ** - ** This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes - ** and allows to use eager bit-blasting in the BV solver. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * Wrap assertions in BITVECTOR_EAGER_ATOM nodes. + * + * This preprocessing pass wraps all assertions in BITVECTOR_EAGER_ATOM nodes + * and allows to use eager bit-blasting in the BV solver. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index ebdc9aba2..557584490 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file bv_gauss.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, 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 Gaussian Elimination preprocessing pass. - ** - ** Simplify a given equation system modulo a (prime) number via Gaussian - ** Elimination if possible. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mathias Preiner, 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. + * **************************************************************************** + * + * Gaussian Elimination preprocessing pass. + * + * Simplify a given equation system modulo a (prime) number via Gaussian + * Elimination if possible. + */ #include "preprocessing/passes/bv_gauss.h" diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index f680fa652..ceda3a885 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file bv_gauss.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Gaussian Elimination preprocessing pass. - ** - ** Simplify a given equation system modulo a (prime) number via Gaussian - ** Elimination if possible. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Mathias Preiner, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Gaussian Elimination preprocessing pass. + * + * Simplify a given equation system modulo a (prime) number via Gaussian + * Elimination if possible. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index fb6a123dd..829655121 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -1,20 +1,21 @@ -/********************* */ -/*! \file bv_intro_pow2.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The BvIntroPow2 preprocessing pass - ** - ** Traverses the formula and applies the IsPowerOfTwo rewrite rule. This - ** preprocessing pass is particularly useful on QF_BV/pspace benchmarks and - ** can be enabled via option `--bv-intro-pow2`. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Liana Hadarean, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The BvIntroPow2 preprocessing pass. + * + * Traverses the formula and applies the IsPowerOfTwo rewrite rule. This + * preprocessing pass is particularly useful on QF_BV/pspace benchmarks and + * can be enabled via option `--bv-intro-pow2`. + */ #include "preprocessing/passes/bv_intro_pow2.h" diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index 63c8e5345..fe4b7dceb 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -1,20 +1,21 @@ -/********************* */ -/*! \file bv_intro_pow2.h - ** \verbatim - ** Top contributors (to current version): - ** 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 The BvIntroPow2 preprocessing pass - ** - ** Traverses the formula and applies the IsPowerOfTwo rewrite rule. This - ** preprocessing pass is particularly useful on QF_BV/pspace benchmarks and - ** can be enabled via option `--bv-intro-pow2`. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The BvIntroPow2 preprocessing pass. + * + * Traverses the formula and applies the IsPowerOfTwo rewrite rule. This + * preprocessing pass is particularly useful on QF_BV/pspace benchmarks and + * can be enabled via option `--bv-intro-pow2`. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index a8382974c..c30017f31 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -1,19 +1,19 @@ -/********************* */ -/*! \file bv_to_bool.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Liana Hadarean, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. - ** - ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. - ** Implemented recursively. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Liana Hadarean, 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. + * **************************************************************************** + * + * Preprocessing pass that lifts bit-vectors of size 1 to booleans. + * + * Implemented recursively. + */ #include "preprocessing/passes/bv_to_bool.h" diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index 270d4b243..442812a20 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file bv_to_bool.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Yoni Zohar, 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 Preprocessing pass that lifts bit-vectors of size 1 to booleans. - ** - ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Liana Hadarean, Yoni Zohar, 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. + * **************************************************************************** + * + * Preprocessing pass that lifts bit-vectors of size 1 to booleans. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 9809adf63..6fe676e30 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file bv_to_int.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Mathias Preiner, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The BVToInt preprocessing pass - ** - ** Converts bit-vector operations into integer operations. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, 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. + * **************************************************************************** + * + * The BVToInt preprocessing pass. + * + * Converts bit-vector operations into integer operations. + * + */ #include "preprocessing/passes/bv_to_int.h" diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index 6ac2a956b..d8d9e1262 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -1,67 +1,68 @@ -/********************* */ -/*! \file bv_to_int.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Gereon Kremer, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level 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 BVToInt preprocessing pass - ** - ** Converts bit-vector formulas to integer formulas. - ** The conversion is implemented using a translation function Tr, - ** roughly described as follows: - ** - ** Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh - ** integer variable. - ** Tr(c) = the integer value of c, for any bit-vector constant c. - ** Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of - ** s and t. - ** Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg, - ** bvnot, bvconcat, bvextract - ** Tr((_ zero_extend m) x) = Tr(x) - ** Tr((_ sign_extend m) x) = ite(msb(x)=0, x, 2^k*(2^m-1) + x)) - ** explanation: if the msb is 0, this is the same as zero_extend, - ** which does not change the integer value. - ** If the msb is 1, then the result should correspond to - ** concat(1...1, x), with m 1's. - ** m 1's is 2^m-1, and multiplying it by x's width (k) moves it - ** to the front. - ** - ** Tr((bvand s t)) depends on the granularity, which is provided by the user - ** when enabling this preprocessing pass. - ** We divide s and t to blocks. - ** The size of each block is the granularity, and so the number of - ** blocks is: - ** bit width/granularity (rounded down). - ** We create an ITE that represents an arbitrary block, - ** and then create a sum by mutiplying each block by the - ** appropriate power of two. - ** More formally: - ** Let g denote the granularity. - ** Let k denote the bit width of s and t. - ** Let b denote floor(k/g) if k >= g, or just k otherwise. - ** Tr((bvand s t)) = - ** Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g) - ** - ** Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor. - ** - ** Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of - ** a and b, and ITE represents exponentiation up to k, that is: - ** ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...)) - ** Similar transformations are done for bvlshr. - ** - ** Tr(a=b) = Tr(a)=Tr(b) - ** Tr((bvult a b)) = Tr(a) < Tr(b) - ** Similar transformations are done for bvule, bvugt, and bvuge. - ** - ** Bit-vector operators that are not listed above are either eliminated using - ** the function eliminationPass, or are not supported. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Gereon Kremer, Makai Mann + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the 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 BVToInt preprocessing pass + * + * Converts bit-vector formulas to integer formulas. + * The conversion is implemented using a translation function Tr, + * roughly described as follows: + * + * Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh + * integer variable. + * Tr(c) = the integer value of c, for any bit-vector constant c. + * Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of + * s and t. + * Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg, + * bvnot, bvconcat, bvextract + * Tr((_ zero_extend m) x) = Tr(x) + * Tr((_ sign_extend m) x) = ite(msb(x)=0, x, 2^k*(2^m-1) + x)) + * explanation: if the msb is 0, this is the same as zero_extend, + * which does not change the integer value. + * If the msb is 1, then the result should correspond to + * concat(1...1, x), with m 1's. + * m 1's is 2^m-1, and multiplying it by x's width (k) moves it + * to the front. + * + * Tr((bvand s t)) depends on the granularity, which is provided by the user + * when enabling this preprocessing pass. + * We divide s and t to blocks. + * The size of each block is the granularity, and so the number of + * blocks is: + * bit width/granularity (rounded down). + * We create an ITE that represents an arbitrary block, + * and then create a sum by mutiplying each block by the + * appropriate power of two. + * More formally: + * Let g denote the granularity. + * Let k denote the bit width of s and t. + * Let b denote floor(k/g) if k >= g, or just k otherwise. + * Tr((bvand s t)) = + * Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g) + * + * Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor. + * + * Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of + * a and b, and ITE represents exponentiation up to k, that is: + * ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...)) + * Similar transformations are done for bvlshr. + * + * Tr(a=b) = Tr(a)=Tr(b) + * Tr((bvult a b)) = Tr(a) < Tr(b) + * Similar transformations are done for bvule, bvugt, and bvuge. + * + * Bit-vector operators that are not listed above are either eliminated using + * the function eliminationPass, or are not supported. + * + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index 38519e96b..a36388c26 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file extended_rewriter_pass.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The ExtRewPre preprocessing pass - ** - ** Applies the extended rewriter to assertions - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The ExtRewPre preprocessing pass. + * + * Applies the extended rewriter to assertions. + */ #include "preprocessing/passes/extended_rewriter_pass.h" diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index f4688582a..69c456720 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file extended_rewriter_pass.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, 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 The ExtRewPre preprocessing pass - ** - ** Applies the extended rewriter to assertions - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The ExtRewPre preprocessing pass. + * + * Applies the extended rewriter to assertions. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp index 60345992f..888d5e43a 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.cpp +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file foreign_theory_rewrite.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The foreign_theory_rewrite preprocessing pass - ** - ** Simplifies nodes of one theory using rewrites from another. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Andres Noetzli, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The foreign_theory_rewrite preprocessing pass. + * + * Simplifies nodes of one theory using rewrites from another. + */ #include "preprocessing/passes/foreign_theory_rewrite.h" diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h index 0af4f487a..2fc90e4c6 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.h +++ b/src/preprocessing/passes/foreign_theory_rewrite.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file foreign_theory_rewrite.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The foreign_theory_rewrite preprocessing pass - ** - ** Simplifies nodes of one theory using rewrites from another. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, 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 foreign_theory_rewrite preprocessing pass. + * + * Simplifies nodes of one theory using rewrites from another. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index 8d1fed4a3..8c97aabc7 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file fun_def_fmf.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, 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 Function definition processor for finite model finding - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Function definition processor for finite model finding. + */ #include "preprocessing/passes/fun_def_fmf.h" diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h index 908f15654..9b51cd73e 100644 --- a/src/preprocessing/passes/fun_def_fmf.h +++ b/src/preprocessing/passes/fun_def_fmf.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file fun_def_fmf.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 Function definition processor for finite model finding - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Function definition processor for finite model finding. + */ #ifndef CVC5__PREPROCESSING__PASSES__FUN_DEF_FMF_H #define CVC5__PREPROCESSING__PASSES__FUN_DEF_FMF_H diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 5cb5663c3..b09870c11 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file global_negate.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Yoni Zohar - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of global_negate - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Yoni Zohar, 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 global_negate. + */ #include "preprocessing/passes/global_negate.h" diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 2d0357490..5b5f7db4d 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -1,25 +1,26 @@ -/********************* */ -/*! \file global_negate.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Mathias Preiner, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief the global_negate preprocessing pass - ** - ** Updates a set of assertions to the negation of these assertions. - ** In detail, if assertions is: - ** F1, ..., Fn - ** then we update this vector to: - ** forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true - ** where x1...xm are the free variables of F1...Fn. - ** When this is done, d_globalNegation flag is marked, so that the solver - ** checks for unsat instead of sat. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Mathias Preiner, 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. + * **************************************************************************** + * + * The global_negate preprocessing pass. + * + * Updates a set of assertions to the negation of these assertions. + * In detail, if assertions is: + * F1, ..., Fn + * then we update this vector to: + * forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true + * where x1...xm are the free variables of F1...Fn. + * When this is done, d_globalNegation flag is marked, so that the solver + * checks for unsat instead of sat. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 619f3cfe2..48ec7860d 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file ho_elim.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The HoElim preprocessing pass - ** - ** Eliminates higher-order constraints. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The HoElim preprocessing pass. + * + * Eliminates higher-order constraints. + */ #include "preprocessing/passes/ho_elim.h" diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index fe22ada98..998e4f353 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file ho_elim.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The HoElim preprocessing pass - ** - ** Eliminates higher-order constraints. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The HoElim preprocessing pass. + * + * Eliminates higher-order constraints. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 1f223ad4f..21ec77d0c 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -1,20 +1,21 @@ -/********************* */ -/*! \file int_to_bv.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Yoni Zohar, Alex Ozdemir - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The IntToBV preprocessing pass - ** - ** Converts integer operations into bitvector operations. The width of the - ** bitvectors is controlled through the `--solve-int-as-bv` command line - ** option. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Yoni Zohar, Alex Ozdemir + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The IntToBV preprocessing pass. + * + * Converts integer operations into bitvector operations. The width of the + * bitvectors is controlled through the `--solve-int-as-bv` command line + * option. + */ #include "preprocessing/passes/int_to_bv.h" diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index 01b5c8ee0..e25154199 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -1,20 +1,21 @@ -/********************* */ -/*! \file int_to_bv.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The IntToBV preprocessing pass - ** - ** Converts integer operations into bitvector operations. The width of the - ** bitvectors is controlled through the `--solve-int-as-bv` command line - ** option. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The IntToBV preprocessing pass. + * + * Converts integer operations into bitvector operations. The width of the + * bitvectors is controlled through the `--solve-int-as-bv` command line + * option. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index cae898a7a..278192c97 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file ite_removal.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Remove ITEs from the assertions - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Remove ITEs from the assertions. + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "preprocessing/passes/ite_removal.h" diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index 8f771fbcc..5b9ac4beb 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -1,19 +1,17 @@ -/********************* */ -/*! \file ite_removal.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Remove ITEs from the assertions - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Remove ITEs from the assertions. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 0ad4f1abc..efa50e0a0 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file ite_simp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, 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 ITE simplification preprocessing pass. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, 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. + * **************************************************************************** + * + * ITE simplification preprocessing pass. + */ #include "preprocessing/passes/ite_simp.h" diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index dc5d99175..1cbe6d904 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file ite_simp.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief ITE simplification preprocessing pass. - **/ +/****************************************************************************** + * Top contributors (to current version): + * 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. + * **************************************************************************** + * + * ITE simplification preprocessing pass. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 687cb3a96..574566661 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -1,17 +1,18 @@ -/********************* */ -/*! \file miplib_trick.cpp - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Andrew Reynolds, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The MIPLIB trick preprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Andrew Reynolds, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The MIPLIB trick preprocessing pass. + * + */ #include "preprocessing/passes/miplib_trick.h" diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index 3619d5882..5f5af1661 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -1,17 +1,17 @@ -/********************* */ -/*! \file miplib_trick.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The MIPLIB trick preprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Morgan Deters, 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. + * **************************************************************************** + * + * The MIPLIB trick preprocessing pass. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index f07c5419f..bb32e7ba2 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file nl_ext_purify.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The NlExtPurify preprocessing pass - ** - ** Purifies non-linear terms - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The NlExtPurify preprocessing pass. + * + * Purifies non-linear terms. + */ #include "preprocessing/passes/nl_ext_purify.h" diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index 4f306e326..7b6c24ced 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file nl_ext_purify.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, 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 The NlExtPurify preprocessing pass - ** - ** Purifies non-linear terms by replacing sums under multiplications by fresh - ** variables - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The NlExtPurify preprocessing pass. + * + * Purifies non-linear terms by replacing sums under multiplications by fresh + * variables. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 8992dad5e..e2b8c0276 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file non_clausal_simp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, 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 Non-clausal simplification preprocessing pass. - ** - ** Run the nonclausal solver and try to solve all assigned theory literals. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, 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. + * **************************************************************************** + * + * Non-clausal simplification preprocessing pass. + * + * Run the nonclausal solver and try to solve all assigned theory literals. + */ #include "preprocessing/passes/non_clausal_simp.h" diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index 2e5d17dbd..80dae3972 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file non_clausal_simp.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, 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 Non-clausal simplification preprocessing pass. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Aina Niemetz, 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. + * **************************************************************************** + * + * Non-clausal simplification preprocessing pass. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index 510281bee..dc48bc2a6 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file pseudo_boolean_processor.cpp - ** \verbatim - ** Top contributors (to current version): - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Andres Noetzli, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "preprocessing/passes/pseudo_boolean_processor.h" diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index 49061dcb8..5b259dd55 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file pseudo_boolean_processor.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Andres Noetzli, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Andres Noetzli, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 6c97936b0..b3a80de2c 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file quantifier_macros.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Yoni Zohar, Haniel Barbosa - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sort inference module - ** - ** This class implements quantifiers macro definitions. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Yoni Zohar, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sort inference module. + * + * This class implements quantifiers macro definitions. + */ #include "preprocessing/passes/quantifier_macros.h" diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 64cdc39b7..8ee878c29 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file quantifier_macros.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Pre-process step for detecting quantifier macro definitions - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Pre-process step for detecting quantifier macro definitions. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index 92b2c8aae..a9363c549 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -1,21 +1,20 @@ -/********************* */ -/*! \file quantifiers_preprocess.cpp - ** \verbatim - ** Top contributors (to current version): - ** Caleb Donovick, 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 Remove rewrite rules, apply pre-skolemization to existential - *quantifiers - ** - ** - ** Calls the quantifier rewriter, removing rewrite rules and applying - ** pre-skolemization to existential quantifiers - **/ +/****************************************************************************** + * Top contributors (to current version): + * Caleb Donovick, 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. + * **************************************************************************** + * + * Remove rewrite rules, apply pre-skolemization to existential quantifiers. + * + * Calls the quantifier rewriter, removing rewrite rules and applying + * pre-skolemization to existential quantifiers + */ #include "preprocessing/passes/quantifiers_preprocess.h" diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index c0835c90e..50781a8ef 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -1,21 +1,20 @@ -/********************* */ -/*! \file quantifiers_preprocess.h - ** \verbatim - ** Top contributors (to current version): - ** Caleb Donovick, 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 Remove rewrite rules, apply pre-skolemization to existential - *quantifiers - ** - ** - ** Calls the quantifier rewriter, removing rewrite rules and applying - ** pre-skolemization to existential quantifiers - **/ +/****************************************************************************** + * Top contributors (to current version): + * Caleb Donovick, 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. + * **************************************************************************** + * + * Remove rewrite rules, apply pre-skolemization to existential quantifiers. + * + * Calls the quantifier rewriter, removing rewrite rules and applying + * pre-skolemization to existential quantifiers + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index d8993ff1b..7c4097564 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file real_to_int.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, 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 RealToInt preprocessing pass - ** - ** Converts real operations into integer operations - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The RealToInt preprocessing pass. + * + * Converts real operations into integer operations. + */ #include "preprocessing/passes/real_to_int.h" diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index 3ee0e45d0..d33a49dfb 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file real_to_int.h - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, 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 The RealToInt preprocessing pass - ** - ** Converts real operations into integer operations - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The RealToInt preprocessing pass. + * + * Converts real operations into integer operations. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index e5ff22d4f..4704f1cb5 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file rewrite.cpp - ** \verbatim - ** Top contributors (to current version): - ** Caleb Donovick - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level 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 rewrite preprocessing pass - ** - ** Calls the rewriter on every assertion - **/ +/****************************************************************************** + * Top contributors (to current version): + * Caleb Donovick, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The rewrite preprocessing pass. + * + * Calls the rewriter on every assertion. + */ #include "preprocessing/passes/rewrite.h" diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index ae083c7ac..3ecc4cd22 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file rewrite.h - ** \verbatim - ** Top contributors (to current version): - ** Caleb Donovick, 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 The rewrite preprocessing pass - ** - ** Calls the rewriter on every assertion - **/ +/****************************************************************************** + * Top contributors (to current version): + * Caleb Donovick, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The rewrite preprocessing pass. + * + * Calls the rewriter on every assertion. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 0c5ca9af9..4322e60d5 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -1,17 +1,17 @@ -/********************* */ -/*! \file sep_skolem_emp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, Andrew Reynolds, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The sep-pre-skolem-emp preprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Andrew Reynolds, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The sep-pre-skolem-emp preprocessing pass. + */ #include "preprocessing/passes/sep_skolem_emp.h" diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index 628b05975..70f25ffb4 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -1,17 +1,17 @@ -/********************* */ -/*! \file sep_skolem_emp.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, 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 The sep-pre-skolem-emp eprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The sep-pre-skolem-emp eprocessing pass. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index cb8818f96..53f3feffc 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sort_infer.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sort inference preprocessing pass - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sort inference preprocessing pass. + */ #include "preprocessing/passes/sort_infer.h" diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index d83e679d2..3f9b2c1ab 100644 --- a/src/preprocessing/passes/sort_infer.h +++ b/src/preprocessing/passes/sort_infer.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sort_infer.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sort inference preprocessing pass - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sort inference preprocessing pass. + */ #ifndef CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ #define CVC5__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 5e572d1d8..278252da9 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -1,17 +1,17 @@ -/********************* */ -/*! \file static_learning.cpp - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, 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 The static learning preprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, 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. + * **************************************************************************** + * + * The static learning preprocessing pass. + */ #include "preprocessing/passes/static_learning.h" diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index d9f1f2b60..8163ba638 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -1,17 +1,17 @@ -/********************* */ -/*! \file static_learning.h - ** \verbatim - ** Top contributors (to current version): - ** Yoni Zohar, 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 The static learning preprocessing pass - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The static learning preprocessing pass. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp index ea12010b0..6ab3a9bd2 100644 --- a/src/preprocessing/passes/strings_eager_pp.cpp +++ b/src/preprocessing/passes/strings_eager_pp.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file strings_eager_pp.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The strings eager preprocess utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The strings eager preprocess utility. + */ #include "preprocessing/passes/strings_eager_pp.h" diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h index 74d12d731..5f2977938 100644 --- a/src/preprocessing/passes/strings_eager_pp.h +++ b/src/preprocessing/passes/strings_eager_pp.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file strings_eager_pp.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The strings eager preprocess utility - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The strings eager preprocess utility. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index a0d4ed91e..870ad6625 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sygus_inference.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sygus inference module - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Sygus inference module. + */ #include "preprocessing/passes/sygus_inference.h" diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index 1ffc73c3b..e657ca99e 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file sygus_inference.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief SygusInference - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * SygusInference. + */ #ifndef CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ #define CVC5__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index b2333b30e..e521ceffa 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -1,17 +1,18 @@ -/********************* */ -/*! \file synth_rew_rules.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A technique for synthesizing candidate rewrites of the form t1 = t2, - ** where t1 and t2 are subterms of the input. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A technique for synthesizing candidate rewrites of the form t1 = t2, + * where t1 and t2 are subterms of the input. + */ #include "preprocessing/passes/synth_rew_rules.h" diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index d23cf6145..daaed88d5 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -1,17 +1,18 @@ -/********************* */ -/*! \file synth_rew_rules.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A technique for synthesizing candidate rewrites of the form t1 = t2, - ** where t1 and t2 are subterms of the input. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A technique for synthesizing candidate rewrites of the form t1 = t2, + * where t1 and t2 are subterms of the input. + */ #ifndef CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H #define CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 8e79a7b09..88cc8112d 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file theory_preprocess.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The TheoryPreprocess preprocessing pass - ** - ** Calls Theory::preprocess(...) on every assertion of the formula. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The TheoryPreprocess preprocessing pass. + * + * Calls Theory::preprocess(...) on every assertion of the formula. + */ #include "preprocessing/passes/theory_preprocess.h" diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index b74b6b5dd..f8264e622 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file theory_preprocess.h - ** \verbatim - ** Top contributors (to current version): - ** 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 The TheoryPreprocess preprocessing pass - ** - ** Calls Theory::preprocess(...) on every assertion of the formula. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The TheoryPreprocess preprocessing pass. + * + * Calls Theory::preprocess(...) on every assertion of the formula. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp index c5a73f89b..862585790 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.cpp +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_rewrite_eq.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The TheoryRewriteEq preprocessing pass - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The TheoryRewriteEq preprocessing pass. + */ #include "preprocessing/passes/theory_rewrite_eq.h" diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index 8f620f580..e88678eb5 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file theory_rewrite_eq.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The TheoryRewriteEq preprocessing pass - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * The TheoryRewriteEq preprocessing pass. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 69ca1fa84..922c3bdd5 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -1,20 +1,21 @@ -/********************* */ -/*! \file unconstrained_simplifier.cpp - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Andres Noetzli, 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 Simplifications based on unconstrained variables - ** - ** This module implements a preprocessing phase which replaces certain - ** "unconstrained" expressions by variables. Based on Roberto - ** Bruttomesso's PhD thesis. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Clark Barrett, Andres Noetzli, 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. + * **************************************************************************** + * + * Simplifications based on unconstrained variables. + * + * This module implements a preprocessing phase which replaces certain + * "unconstrained" expressions by variables. Based on Roberto + * Bruttomesso's PhD thesis. + */ #include "preprocessing/passes/unconstrained_simplifier.h" diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index 23d7545a6..914d450b0 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -1,20 +1,21 @@ -/********************* */ -/*! \file unconstrained_simplifier.h - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Andres Noetzli, 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 Simplifications based on unconstrained variables - ** - ** This module implements a preprocessing phase which replaces certain - ** "unconstrained" expressions by variables. Based on Roberto - ** Bruttomesso's PhD thesis. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Clark Barrett, Andres Noetzli, 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. + * **************************************************************************** + * + * Simplifications based on unconstrained variables + * + * This module implements a preprocessing phase which replaces certain + * "unconstrained" expressions by variables. Based on Roberto + * Bruttomesso's PhD thesis. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index f9effecba..959afe5d7 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file preprocessing_pass.cpp - ** \verbatim - ** Top contributors (to current version): - ** Justin Xu, Abdalrhman Mohamed, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The preprocessing pass super class - ** - ** Preprocessing pass super class. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Justin Xu, Abdalrhman Mohamed, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The preprocessing pass super class. + */ #include "preprocessing/preprocessing_pass.h" diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index c1fcf7715..8cfec5ed6 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -1,30 +1,31 @@ -/********************* */ -/*! \file preprocessing_pass.h - ** \verbatim - ** Top contributors (to current version): - ** Justin Xu, Mathias Preiner, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The preprocessing pass super class - ** - ** Implementation of the preprocessing pass super class. Preprocessing passes - ** that inherit from this class, need to pass their name to the constructor to - ** register the pass appropriately. The core of a preprocessing pass lives - ** in applyInternal(), which operates on a list of assertions and is called - ** from apply() in the super class. The apply() method automatically takes - ** care of the following: - ** - ** - Dumping assertions before and after the pass - ** - Initializing the timer - ** - Tracing and chatting - ** - ** Optionally, preprocessing passes can overwrite the initInteral() method to - ** do work that only needs to be done once. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Justin Xu, Mathias Preiner, 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 preprocessing pass super class + * + * Implementation of the preprocessing pass super class. Preprocessing passes + * that inherit from this class, need to pass their name to the constructor to + * register the pass appropriately. The core of a preprocessing pass lives + * in applyInternal(), which operates on a list of assertions and is called + * from apply() in the super class. The apply() method automatically takes + * care of the following: + * + * - Dumping assertions before and after the pass + * - Initializing the timer + * - Tracing and chatting + * + * Optionally, preprocessing passes can overwrite the initInteral() method to + * do work that only needs to be done once. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index fdcbbb466..6e7d253f2 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file preprocessing_pass_context.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The preprocessing pass context for passes - ** - ** The preprocessing pass context for passes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The preprocessing pass context for passes. + */ #include "preprocessing/preprocessing_pass_context.h" diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 44352519a..902db959f 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -1,20 +1,21 @@ -/********************* */ -/*! \file preprocessing_pass_context.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The preprocessing pass context for passes - ** - ** Implementation of the preprocessing pass context for passes. This context - ** allows preprocessing passes to retrieve information besides the assertions - ** from the solver and interact with it without getting full access. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The preprocessing pass context for passes + * + * Implementation of the preprocessing pass context for passes. This context + * allows preprocessing passes to retrieve information besides the assertions + * from the solver and interact with it without getting full access. + */ #include "cvc4_private.h" diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index b9434e63f..43acf5b17 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file preprocessing_pass_registry.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Yoni Zohar, Justin Xu - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level 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 preprocessing pass registry - ** - ** This file defines the classes PreprocessingPassRegistry, which keeps track - ** of the available preprocessing passes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Yoni Zohar, Justin Xu + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the 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 preprocessing pass registry + * + * This file defines the classes PreprocessingPassRegistry, which keeps track + * of the available preprocessing passes. + */ #include "preprocessing/preprocessing_pass_registry.h" diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h index 895b344ad..fdff98a90 100644 --- a/src/preprocessing/preprocessing_pass_registry.h +++ b/src/preprocessing/preprocessing_pass_registry.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file preprocessing_pass_registry.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Justin Xu, 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 The preprocessing pass registry - ** - ** This file defines the classes PreprocessingPassRegistry, which keeps track - ** of the available preprocessing passes. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Justin Xu, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The preprocessing pass registry + * + * This file defines the classes PreprocessingPassRegistry, which keeps track + * of the available preprocessing passes. + */ #include "cvc4_private.h" #ifndef CVC5__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 093f4a573..6dfce4254 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -1,22 +1,23 @@ -/********************* */ -/*! \file ite_utilities.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Aina Niemetz, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Simplifications for ITE expressions - ** - ** This module implements preprocessing phases designed to simplify ITE - ** expressions. Based on: - ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. - ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Aina Niemetz, Clark Barrett + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Simplifications for ITE expressions. + * + * This module implements preprocessing phases designed to simplify ITE + * expressions. Based on: + * Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. + * Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC *'96 - **/ + */ #include "preprocessing/util/ite_utilities.h" #include <utility> @@ -167,9 +168,7 @@ void ITEUtilities::clear() d_containsVisitor->garbageCollect(); } -/********************* */ -/* ContainsTermITEVisitor - */ +/** ContainsTermITEVisitor. */ ContainsTermITEVisitor::ContainsTermITEVisitor() : d_cache() {} ContainsTermITEVisitor::~ContainsTermITEVisitor() {} bool ContainsTermITEVisitor::containsTermITE(TNode e) @@ -240,9 +239,7 @@ bool ContainsTermITEVisitor::containsTermITE(TNode e) } void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); } -/********************* */ -/* IncomingArcCounter - */ +/** IncomingArcCounter. */ IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants) : d_reachCount(), d_skipVariables(skipVars), d_skipConstants(skipConstants) { @@ -289,9 +286,7 @@ void IncomingArcCounter::computeReachability( void IncomingArcCounter::clear() { d_reachCount.clear(); } -/********************* */ -/* ITECompressor - */ +/** ITECompressor. */ ITECompressor::ITECompressor(ContainsTermITEVisitor* contains) : d_contains(contains), d_assertions(NULL), d_incoming(true, true) { diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index a633e8d57..1c10c2ebd 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -1,22 +1,23 @@ -/********************* */ -/*! \file ite_utilities.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Aina Niemetz, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Simplifications for ITE expressions - ** - ** This module implements preprocessing phases designed to simplify ITE - ** expressions. Based on: - ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. - ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Aina Niemetz, Clark Barrett + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Simplifications for ITE expressions. + * + * This module implements preprocessing phases designed to simplify ITE + * expressions. Based on: + * Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. + * Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC *'96 - **/ + */ #include "cvc4_private.h" |