diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-12 12:31:43 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-12 19:31:43 +0000 |
commit | 7ec30058750611786b1b597816c8a23e28bb5812 (patch) | |
tree | e59b1de0078dc04d3a9c212cf9e6ebfd70cbb7f4 /src/theory/booleans | |
parent | 7361b587e9a1b717dfa906d02f66feb6896e80dd (diff) |
Refactor and update copyright headers. (#6316)
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 29 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 29 | ||||
-rw-r--r-- | src/theory/booleans/proof_checker.cpp | 27 | ||||
-rw-r--r-- | src/theory/booleans/proof_checker.h | 27 | ||||
-rw-r--r-- | src/theory/booleans/proof_circuit_propagator.cpp | 29 | ||||
-rw-r--r-- | src/theory/booleans/proof_circuit_propagator.h | 29 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 29 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 29 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 33 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.h | 33 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_type_rules.h | 31 | ||||
-rw-r--r-- | src/theory/booleans/type_enumerator.h | 29 |
12 files changed, 176 insertions, 178 deletions
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index df50bccac..7920f5b7f 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file circuit_propagator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer, Morgan Deters, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A non-clausal circuit propagator for Boolean simplification - ** - ** A non-clausal circuit propagator for Boolean simplification. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Morgan Deters, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A non-clausal circuit propagator for Boolean simplification. + */ #include "theory/booleans/circuit_propagator.h" diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 6ff91e5cb..0c02ba9bd 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file circuit_propagator.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, 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 A non-clausal circuit propagator for Boolean simplification - ** - ** A non-clausal circuit propagator for Boolean simplification. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, 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. + * **************************************************************************** + * + * A non-clausal circuit propagator for Boolean simplification. + */ #include "cvc4_private.h" diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 6b9d3e44e..256ccedce 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.cpp - ** \verbatim - ** Top contributors (to current version): - ** Haniel Barbosa, Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of equality proof checker - **/ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of equality proof checker. + */ #include "theory/booleans/proof_checker.h" #include "expr/skolem_manager.h" diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h index 6b67e151d..bf503089b 100644 --- a/src/theory/booleans/proof_checker.h +++ b/src/theory/booleans/proof_checker.h @@ -1,16 +1,17 @@ -/********************* */ -/*! \file proof_checker.h - ** \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 Boolean proof checker utility - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Boolean proof checker utility. + */ #include "cvc4_private.h" diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index 9b3c6de10..d1f8bb854 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file proof_circuit_propagator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Proofs for the non-clausal circuit propagator. - ** - ** Proofs for the non-clausal circuit propagator. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Proofs for the non-clausal circuit propagator. + */ #include "theory/booleans/proof_circuit_propagator.h" diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h index 6bac0874d..d26ce3cf8 100644 --- a/src/theory/booleans/proof_circuit_propagator.h +++ b/src/theory/booleans/proof_circuit_propagator.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file proof_circuit_propagator.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Proofs for the non-clausal circuit propagator. - ** - ** Proofs for the non-clausal circuit propagator. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Proofs for the non-clausal circuit propagator. + */ #include "cvc4_private.h" diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 04d6e77f6..bac2be70c 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_bool.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The theory of booleans. - ** - ** The theory of booleans. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Dejan Jovanovic + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The theory of booleans. + */ #include "theory/booleans/theory_bool.h" diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 89090b307..10190262a 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file theory_bool.h - ** \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 The theory of booleans - ** - ** The theory of booleans. - **/ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * The theory of booleans. + */ #include "cvc4_private.h" diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 70a5674b8..0d7431a8e 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file theory_bool_rewriter.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Dejan Jovanovic, 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Dejan Jovanovic, 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. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <algorithm> #include <unordered_set> diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index c88a87b7c..03b85e947 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -1,19 +1,20 @@ -/********************* */ -/*! \file theory_bool_rewriter.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Mathias Preiner, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include "cvc4_private.h" diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 38bd13ab7..c7f9ad4ad 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -1,18 +1,19 @@ -/********************* */ -/*! \file theory_bool_type_rules.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, Christopher L. Conway - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add brief comments here ]] - ** - ** [[ Add file-specific comments here ]] - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Morgan Deters, Christopher L. Conway + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add brief comments here ]] + * + * [[ Add file-specific comments here ]] + */ #include "cvc4_private.h" diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h index a101fa040..088468d43 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -1,18 +1,17 @@ -/********************* */ -/*! \file type_enumerator.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An enumerator for Booleans - ** - ** An enumerator for Booleans. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An enumerator for Booleans. + */ #include "cvc4_private.h" |