Use new copyright header format.

diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index e74d83882b88da086c61e92a0d058ea1dfee0e31..434ff3d24437ef8dc0619948fa1d5ec7a8c0d144 100644 (file)
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file antlr_input_imports.cpp
  ** \verbatim
- ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** 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/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b5bad6a2d83440d3cf5bea6937a3e5313cb8a28a..368a6db82172f7280b3f9ca39294b269deb95ea9 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -489,10 +489,11 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** 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.
  **/
 }/* @header */
 

diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 28c54fc804c409a7253154150f549e80b2ba2ac4..c7548db71fbad2f2a58251ff9c32766828d8e2c8 100644 (file)
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -31,10 +31,11 @@ options {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** 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.
  **/
 }/* @header */
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1b96d9bd387b121b79e293cdda9f78f9c4405419..01b2ab7da2a7d1104f9a5ea030be285cc7fc5677 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -31,10 +31,11 @@ options {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** 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.
  **/
 }/* @header */
 

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index dcee5233772fe0e23d572eefaf3a8d6bb74ae25d..6f1af9c74cdc9219024baea2344baef55263f6b9 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -32,10 +32,11 @@ options {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** 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.
  **/
 }/* @header */
 

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 368a79b80d99f499085c88c96591545112d59657..95f8dca5b898bd0aa0b3dffac797d28cacfc86a0 100644 (file)
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file bvminisat.cpp
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** 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 SAT Solver.
  **

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 732bd0313f4f2470163d3f10ec2028a752efa76f..1a9ee3f9650407b02f72c67d9d99aa3cd83c7270 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file bvminisat.h
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** 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 SAT Solver.
  **

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index eff079cc9a705d04f1eb5e675dd1a56632cab575..efd3cd5cc37221c27538bf03266c9c8568b85c48 100644 (file)
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file cryptominisat.cpp
  ** \verbatim
- ** Original author: lianah
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** 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 SAT Solver.
  **

diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 7ad861defb0cc09b350e8d235872628e3d1003ce..c3f5edbb12f4b7176a2bae135de038f3cc2e5cdc 100644 (file)
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file cryptominisat.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** 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 SAT Solver.
  **

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index a88a872c83cb9da555c68b073cf0f89f9b57b454..f7a8f22cba3cb4d6f7932fdc3cbb983bf1414ad1 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file minisat.cpp
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** 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 SAT Solver.
  **

diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 1627a657560fbcdd2ec99ef84717c77e3980edf0..d649ad894052725cdc5d26fb3d7864914dea733b 100644 (file)
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file minisat.h
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** 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 SAT Solver.
  **

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 9d064d74d4a379fe559812e224407b3d2c946e76..4c6cd3eb42f776099545ee65c4eedc901ba86d20 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** 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 the theory of sep.
  **

diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 8dd1ed356d22bd8ffe568c0c72ea36dd581aa00c..00e67f5ff195708216550b5d9759fb59e773c81d 100644 (file)
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Dejan Jovanovic, Clark Barrett
- ** Minor contributors (to current version): Tim King, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   none 
  ** 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 Theory of sep
  **

diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 0faf7b176c6ee56b5d0c68ef59a7b6510e6d7a7a..2e6a54ebdf600e2ca9fc77f0c250ecac74c8b105 100644 (file)
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep_rewriter.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** 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/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
index 58b79c7fd940c1883daabaec2604c91882be682b..c71248319b6e13f04a7b65b874ef3e1d01a90579 100644 (file)
--- a/src/theory/sep/theory_sep_rewriter.h
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep_rewriter.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** 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/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index 0eae782c80d60293ac3c42ad86f5ff7b040b792a..8de0783e23655168ba581b5f2add984804340161 100644 (file)
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep_type_rules.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** 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 Typing and cardinality rules for the theory of sep
  **

diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index df14bf53bd8c6a84671ef1af0f9934dbed40df94..9863b9734209441b8a6fc77135903650b76a2afa 100644 (file)
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file rels_utils.h
  ** \verbatim
- ** Original author: Paul Meng
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** 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 Sets theory implementation.
  **

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 03e0c64f8c0effea209ecb7a846a11ef1447ac32..5f9243b33631da20452ce1919dc2010f40dcfb83 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sets_rels.cpp
  ** \verbatim
- ** Original author: Paul Meng
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** 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 Sets theory implementation.
  **

diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 576430eb12fd973e620ae73ddf87824577009418..24c744203bdb90a1dc468c706f522587973d3c97 100644 (file)
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sets_rels.h
  ** \verbatim
- ** Original author: Paul Meng
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** 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 Sets theory implementation.
  **

diff --git a/src/util/channel.h b/src/util/channel.h
index 39aed425b74d10c21784efd4fc62ae4055b927cf..5a561041080cf09c9bb2bad7adceeed5ca245651 100644 (file)
--- a/src/util/channel.h
+++ b/src/util/channel.h
@@ -1,9 +1,8 @@
 /*********************                                                        */
 /*! \file channel.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** This file is part of the CVC4 project but is excluded from the
  ** standard CVC4 licensing because it is a derivative work of
  ** circular_buffer.hpp in the BOOST 1.46.1 distribution.
@@ -13,6 +12,7 @@
  ** The combined work is:
  **   Copyright (c) 2009-2014  New York University and The University of Iowa
  **   Copyright (c) 2003-2008  Jan Gaspar
+ ** \endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **