summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/array.h12
-rw-r--r--src/expr/array_store_all.cpp12
-rw-r--r--src/expr/array_store_all.h12
-rw-r--r--src/expr/ascription_type.h12
-rw-r--r--src/expr/attribute.cpp12
-rw-r--r--src/expr/attribute.h12
-rw-r--r--src/expr/attribute_internals.h12
-rw-r--r--src/expr/attribute_unique_id.h12
-rw-r--r--src/expr/chain.h12
-rw-r--r--src/expr/convenience_node_builders.h12
-rw-r--r--src/expr/datatype.cpp12
-rw-r--r--src/expr/datatype.h12
-rw-r--r--src/expr/emptyset.cpp12
-rw-r--r--src/expr/emptyset.h12
-rw-r--r--src/expr/expr_iomanip.cpp12
-rw-r--r--src/expr/expr_iomanip.h12
-rw-r--r--src/expr/expr_manager_scope.h12
-rw-r--r--src/expr/expr_manager_template.cpp12
-rw-r--r--src/expr/expr_manager_template.h12
-rw-r--r--src/expr/expr_stream.h12
-rw-r--r--src/expr/expr_template.cpp12
-rw-r--r--src/expr/expr_template.h12
-rw-r--r--src/expr/kind_map.h12
-rw-r--r--src/expr/kind_template.h12
-rw-r--r--src/expr/matcher.h12
-rw-r--r--src/expr/metakind_template.h12
-rw-r--r--src/expr/node.cpp12
-rw-r--r--src/expr/node.h12
-rw-r--r--src/expr/node_builder.h12
-rw-r--r--src/expr/node_manager.cpp12
-rw-r--r--src/expr/node_manager.h12
-rw-r--r--src/expr/node_manager_attributes.h12
-rw-r--r--src/expr/node_manager_listeners.cpp14
-rw-r--r--src/expr/node_manager_listeners.h12
-rw-r--r--src/expr/node_self_iterator.h12
-rw-r--r--src/expr/node_value.cpp12
-rw-r--r--src/expr/node_value.h12
-rw-r--r--src/expr/pickle_data.cpp12
-rw-r--r--src/expr/pickle_data.h12
-rw-r--r--src/expr/pickler.cpp12
-rw-r--r--src/expr/pickler.h12
-rw-r--r--src/expr/predicate.cpp12
-rw-r--r--src/expr/predicate.h12
-rw-r--r--src/expr/record.cpp12
-rw-r--r--src/expr/record.h12
-rw-r--r--src/expr/symbol_table.cpp12
-rw-r--r--src/expr/symbol_table.h12
-rw-r--r--src/expr/type.cpp12
-rw-r--r--src/expr/type.h12
-rw-r--r--src/expr/type_checker.h12
-rw-r--r--src/expr/type_checker_template.cpp12
-rw-r--r--src/expr/type_node.cpp12
-rw-r--r--src/expr/type_node.h12
-rw-r--r--src/expr/type_properties_template.h12
-rw-r--r--src/expr/uninterpreted_constant.cpp12
-rw-r--r--src/expr/uninterpreted_constant.h12
-rw-r--r--src/expr/variable_type_map.h12
57 files changed, 343 insertions, 343 deletions
diff --git a/src/expr/array.h b/src/expr/array.h
index ab554171f..cf050e077 100644
--- a/src/expr/array.h
+++ b/src/expr/array.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file array.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Array types.
**
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 6ac07c81d..c8e346e48 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file array_store_all.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Representation of a constant array (an array in which the
** element is the same for all indices)
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index 293b785a9..0a9c8344a 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file array_store_all.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Representation of a constant array (an array in which the
** element is the same for all indices)
diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index 42906e557..46d2871ff 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file ascription_type.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A class representing a type ascription
**
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index cd5b35384..3cf242988 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file attribute.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Tim King
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 AttributeManager implementation.
**
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 432fbbac9..13bedeaf8 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file attribute.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Node attributes.
**
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index dae11fd74..60d2069e7 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file attribute_internals.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Node attributes' internals.
**
diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h
index 45dc368a5..4875bdf50 100644
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file attribute_unique_id.h
** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
**
diff --git a/src/expr/chain.h b/src/expr/chain.h
index e052a2ed8..703aa76ed 100644
--- a/src/expr/chain.h
+++ b/src/expr/chain.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file chain.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
**
diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h
index 0c3b690b2..611a88e6f 100644
--- a/src/expr/convenience_node_builders.h
+++ b/src/expr/convenience_node_builders.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file convenience_node_builders.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Convenience node builders.
**
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index b52ceb856..d14ac26d4 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file datatype.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A class representing a Datatype definition
**
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index c64b71f5a..1197b4a3b 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file datatype.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A class representing a Datatype definition
**
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index a6e2c1ece..23e6df7dc 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file emptyset.cpp
** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King, Kshitij Bansal, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
**
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index cf9d050f8..a606951f0 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file emptyset.h
** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King, Kshitij Bansal, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
**
diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp
index 4c7ab3c8b..1d6df2a4e 100644
--- a/src/expr/expr_iomanip.cpp
+++ b/src/expr/expr_iomanip.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_iomanip.cpp
** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2015 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Expr IO manipulation classes.
**
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
index b3370e75a..94e2b46ea 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_iomanip.h
** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2015 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Expr IO manipulation classes.
**
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index a8e8f04be..cd4c274e5 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_manager_scope.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
**
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 39a2a268c..4475554b1 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_manager_template.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Christopher L. Conway
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Public-facing expression manager interface, implementation
**
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 37ef128f4..72fa5d1b6 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_manager_template.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Public-facing expression manager interface
**
diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h
index 20977011c..d3dbd2902 100644
--- a/src/expr/expr_stream.h
+++ b/src/expr/expr_stream.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_stream.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 stream interface for expressions
**
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index a6cdedd00..43e4a7b76 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_template.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Kshitij Bansal
- ** Minor contributors (to current version): Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ ** Morgan Deters, Kshitij Bansal, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Public-facing expression interface, implementation.
**
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index d037a6bb9..5c3f89e9c 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file expr_template.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Liana Hadarean, Kshitij Bansal, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Public-facing expression interface.
**
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index 02e9728f0..6858f8ab9 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file kind_map.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 bitmap of Kinds
**
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 799d1ac33..440d6b586 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file kind_template.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Template for the Node kind header
**
diff --git a/src/expr/matcher.h b/src/expr/matcher.h
index 8cb092a64..308ad06df 100644
--- a/src/expr/matcher.h
+++ b/src/expr/matcher.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file matcher.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A class representing a type matcher
**
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 539db1c91..9025aa02a 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file metakind_template.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Template for the metakind header.
**
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index cf9a772b7..793b6af97 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file node.cpp
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Reference-counted encapsulation of a pointer to node information.
**
diff --git a/src/expr/node.h b/src/expr/node.h
index a51de6d66..998294da3 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file node.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot, Clark Barrett, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Reference-counted encapsulation of a pointer to node information
**
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index e1a083a78..0dd4e44e8 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_builder.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 builder interface for Nodes.
**
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index db4269ca6..0809a0331 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_manager.cpp
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): ACSYS, Kshitij Bansal, Tim King, Christopher L. Conway
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Expression manager implementation.
**
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 974a1ed94..7fa93d38d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_manager.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 manager for Nodes
**
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index 1f67a09a5..20e1c6c50 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_manager_attributes.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
**
diff --git a/src/expr/node_manager_listeners.cpp b/src/expr/node_manager_listeners.cpp
index ec2de105a..3915aa9bd 100644
--- a/src/expr/node_manager_listeners.cpp
+++ b/src/expr/node_manager_listeners.cpp
@@ -1,13 +1,13 @@
/********************* */
-/*! \file node_manager_listeners.h
+/*! \file node_manager_listeners.cpp
** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Listeners that NodeManager registers to its Options object.
**
diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h
index fc7c2f65f..caff3a545 100644
--- a/src/expr/node_manager_listeners.h
+++ b/src/expr/node_manager_listeners.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_manager_listeners.h
** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Listeners that NodeManager registers to its Options object.
**
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 77fc05e3b..9d37f6e6e 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_self_iterator.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Iterator supporting Node "self-iteration"
**
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index ab18973cb..a40075ca9 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_value.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 expression node.
**
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index c39c14604..fbf3ff76e 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file node_value.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Christopher L. Conway, Tim King, Dejan Jovanovic
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 expression node.
**
diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp
index e273bcece..2050d2d15 100644
--- a/src/expr/pickle_data.cpp
+++ b/src/expr/pickle_data.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file pickle_data.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 This is a "pickle" for expressions, CVC4-internal view
**
diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h
index acf0dccdd..6c283719a 100644
--- a/src/expr/pickle_data.h
+++ b/src/expr/pickle_data.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file pickle_data.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 This is a "pickle" for expressions, CVC4-internal view
**
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index d0501ca2b..ab8037a9a 100644
--- a/src/expr/pickler.cpp
+++ b/src/expr/pickler.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file pickler.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King, Kshitij Bansal
+ ** Top contributors (to current version):
+ ** Morgan Deters, Kshitij Bansal, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 This is a "pickler" for expressions
**
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
index cf1754d93..abd927788 100644
--- a/src/expr/pickler.h
+++ b/src/expr/pickler.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file pickler.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 This is a "pickler" for expressions
**
diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp
index 5ccc3484a..52b580148 100644
--- a/src/expr/predicate.cpp
+++ b/src/expr/predicate.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file predicate.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Representation of predicates for predicate subtyping
**
diff --git a/src/expr/predicate.h b/src/expr/predicate.h
index 669ecc29f..a7003fbd1 100644
--- a/src/expr/predicate.h
+++ b/src/expr/predicate.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file predicate.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Representation of predicates for predicate subtyping
**
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index ec5ef96f1..0d2fd6527 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file record.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A class representing a record definition
**
diff --git a/src/expr/record.h b/src/expr/record.h
index d30536fb0..84feb7e1d 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file record.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A class representing a Record definition
**
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index c0a80b7ce..185006e73 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file symbol_table.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
+ ** Top contributors (to current version):
+ ** Morgan Deters, Christopher L. Conway, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Convenience class for scoping variable and type
** declarations (implementation)
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 451a482dc..efd0f1a13 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file symbol_table.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic, Francois Bobot
+ ** Top contributors (to current version):
+ ** Morgan Deters, Christopher L. Conway, Francois Bobot
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Convenience class for scoping variable and type declarations.
**
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 6b5bdf07c..5b4fef395 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file type.cpp
** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Dejan Jovanovic, Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 expression types
**
diff --git a/src/expr/type.h b/src/expr/type.h
index 67d259fec..a2d6207fb 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file type.h
** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Dejan Jovanovic, Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Martin Brain
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Interface for expression types.
**
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index 4b04adfc9..3df73b268 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file type_checker.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 type checker
**
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 061e1b4e0..8ed894a22 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file type_checker_template.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 TypeChecker implementation
**
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 0c9445051..5d672e6ac 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file type_node.cpp
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Reference-counted encapsulation of a pointer to node information.
**
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 099be5d80..cfb61a085 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file type_node.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett, Andrew Reynolds, Tianyi Liang, Kshitij Bansal, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Martin Brain
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Reference-counted encapsulation of a pointer to node information.
**
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index bc780a7e5..4874a84b8 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file type_properties_template.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Template for the Type properties header
**
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 97bc3ae4b..c88c3b591 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file uninterpreted_constant.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Representation of constants of uninterpreted sorts
**
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 5b2293df6..7d7a3759b 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file uninterpreted_constant.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 Representation of constants of uninterpreted sorts
**
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
index 59ce5c606..00d2c3eac 100644
--- a/src/expr/variable_type_map.h
+++ b/src/expr/variable_type_map.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file variable_type_map.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback