Update copyright headers to 2021. (#6081)

1 files changed, 12 insertions, 9 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 70b2cad20..6a73d69d2 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -4,12 +4,13 @@
  ** Top contributors (to current version):
  **   Tim King, Alex Ozdemir, Haniel Barbosa
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
  ** in the 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 Defines Constraint and ConstraintDatabase which is the internal representation of variables in arithmetic
+ ** \brief Defines Constraint and ConstraintDatabase which is the internal
+ ** representation of variables in arithmetic
  **
  ** This file defines Constraint and ConstraintDatabase.
  ** A Constraint is the internal representation of literals in TheoryArithmetic.
@@ -36,15 +37,16 @@
  **  - Whether a constraint, be be used in explanations sent to the context
  **
  ** Looking up constraints:
- **  - All of the Constraints with associated nodes in the ConstraintDatabase can
- **    be accessed via a single hashtable lookup until the Constraint is removed.
+ **  - All of the Constraints with associated nodes in the ConstraintDatabase
+ **    can be accessed via a single hashtable lookup until the Constraint is
+ **    removed.
  **  - Nodes that have not been associated to a constraints can be
  **    inserted/associated to existing nodes in O(log n) time.
  **
  ** Implications:
  **  - A Constraint can be used to find unate implications.
- **  - A unate implication is an implication based purely on the ArithVar matching
- **    and the DeltaRational value.
+ **  - A unate implication is an implication based purely on the ArithVar
+ **    matching  and the DeltaRational value.
  **    (implies (<= x c) (<= x d)) given c <= d
  **  - This is done using the iterator into the sorted set of constraints.
  **  - Given a tight constraint and previous tightest constraint, this will
@@ -58,16 +60,17 @@
  ** Internals:
  **  - Constraints are pointers to ConstraintValues.
  **  - Undefined Constraints are NullConstraint.
-
  **
  ** Assumption vs. Assertion:
  ** - An assertion is anything on the theory d_fact queue.
  **   This includes any thing propagated and returned to the fact queue.
- **   These can be used in external conflicts and propagations of earlier proofs.
+ **   These can be used in external conflicts and propagations of earlier
+ **   proofs.
  ** - An assumption is anything on the theory d_fact queue that has no further
  **   explanation i.e. this theory did not propagate it.
  ** - To set something an assumption, first set it as being as assertion.
- ** - Internal assumptions have no explanations and must be regressed out of the proof.
+ ** - Internal assumptions have no explanations and must be regressed out of the
+ **   proof.
  **/
 
 #include "cvc4_private.h"