diff options
Diffstat (limited to 'src/theory')
197 files changed, 867 insertions, 854 deletions
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp index 2755f3a90..6d0794d27 100644 --- a/src/theory/arith/arith_heuristic_pivot_rule.cpp +++ b/src/theory/arith/arith_heuristic_pivot_rule.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_heuristic_pivot_rule.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h index 58b638aa9..6c1b17a5b 100644 --- a/src/theory/arith/arith_heuristic_pivot_rule.h +++ b/src/theory/arith/arith_heuristic_pivot_rule.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_heuristic_pivot_rule.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 5c8b89e15..d9bdde5d5 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_priority_queue.cpp ** \verbatim - ** Original author: taking - ** Major contributors: mdeters + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index b6b462db9..695a981cb 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_priority_queue.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_propagation_mode.cpp b/src/theory/arith/arith_propagation_mode.cpp index 030b7792e..bd87bbab8 100644 --- a/src/theory/arith/arith_propagation_mode.cpp +++ b/src/theory/arith/arith_propagation_mode.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_propagation_mode.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_propagation_mode.h b/src/theory/arith/arith_propagation_mode.h index 0a862fdd7..0d3db014e 100644 --- a/src/theory/arith/arith_propagation_mode.h +++ b/src/theory/arith/arith_propagation_mode.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_propagation_mode.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index ee9ff9e1b..41e8c2542 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_rewriter.cpp ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 9b3f37d31..8c9aba83e 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_rewriter.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters, dejan + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 124fa8e2a..551fd819b 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_static_learner.cpp ** \verbatim - ** Original author: taking - ** Major contributors: dejan, mdeters + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 48ee6a3bb..0414e2f09 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_static_learner.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_unate_lemma_mode.cpp b/src/theory/arith/arith_unate_lemma_mode.cpp index 559137e15..b3efaf1a0 100644 --- a/src/theory/arith/arith_unate_lemma_mode.cpp +++ b/src/theory/arith/arith_unate_lemma_mode.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_unate_lemma_mode.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_unate_lemma_mode.h b/src/theory/arith/arith_unate_lemma_mode.h index b1689fb16..3f8214889 100644 --- a/src/theory/arith/arith_unate_lemma_mode.h +++ b/src/theory/arith/arith_unate_lemma_mode.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_unate_lemma_mode.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 76210fc7c..a68eb6568 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arith_utilities.h ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp index 76b143fff..cbcdfb866 100644 --- a/src/theory/arith/arithvar.cpp +++ b/src/theory/arith/arithvar.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file arithvar.cpp + ** \verbatim + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 + **/ + #include "theory/arith/arithvar.h" #include <limits> diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index 95614a011..7e2573394 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arithvar.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index e0e589e57..17e9a8f56 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -1,11 +1,11 @@ /********************* */ /*! \file arithvar_node_map.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index de4c7eac3..8af9152db 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file congruence_manager.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 5e2c80a63..5edcbe435 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -1,11 +1,11 @@ /********************* */ /*! \file congruence_manager.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 4655ea34e..3132f869f 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file constraint.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 82023a48b..26af01e63 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -1,11 +1,11 @@ /********************* */ /*! \file constraint.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h index e11052c5e..65c950ab5 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/constraint_forward.h @@ -1,11 +1,11 @@ /********************* */ /*! \file constraint_forward.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 39b99d625..b6394887d 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file delta_rational.cpp ** \verbatim - ** Original author: taking - ** Major contributors: mdeters + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 51c1e5138..2a280f634 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -1,11 +1,11 @@ /********************* */ /*! \file delta_rational.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 4d9d66cec..e090e5b62 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file dio_solver.cpp ** \verbatim - ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Tim King <taking@cs.nyu.edu> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index bfcd19021..87e9f5215 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -1,11 +1,11 @@ /********************* */ /*! \file dio_solver.h ** \verbatim - ** Original author: mdeters - ** Major contributors: taking + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Tim King <taking@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 5063a05c7..81501fc53 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file linear_equality.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 7df5ee9c3..39da88faa 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -1,11 +1,11 @@ /********************* */ /*! \file linear_equality.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp index cd7a8a9aa..3ddc73666 100644 --- a/src/theory/arith/matrix.cpp +++ b/src/theory/arith/matrix.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file matrix.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 027397b6a..9d4cee0e1 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -1,11 +1,11 @@ /********************* */ /*! \file matrix.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 9bd0a3b6c..b0c225461 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file normal_form.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index d4f867099..24d295fb5 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -1,11 +1,11 @@ /********************* */ /*! \file normal_form.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h index f8f851964..06c367687 100644 --- a/src/theory/arith/options_handlers.h +++ b/src/theory/arith/options_handlers.h @@ -1,11 +1,11 @@ /********************* */ /*! \file options_handlers.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 5dccd8747..33ce5dcdf 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file partial_model.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index fdb4a8ffa..f3cf5164b 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -1,11 +1,11 @@ /********************* */ /*! \file partial_model.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index c71965c5d..8f8a9b261 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file simplex.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 5a3985ee2..a1f451059 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -1,11 +1,11 @@ /********************* */ /*! \file simplex.h ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): kshitij, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Kshitij Bansal <kshitij@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e0d95627d..0ed10d4aa 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arith.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King <taking@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Kshitij Bansal <kshitij@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 50061579a..a63a0bbb3 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arith.h ** \verbatim - ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): ajreynol, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Tim King <taking@cs.nyu.edu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 30b5e279a..32def6116 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arith_type_rules.h ** \verbatim - ** Original author: dejan - ** Major contributors: taking, cconway, mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Tim King <taking@cs.nyu.edu>, Christopher L. Conway <christopherleeconway@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 55ebc38c9..dc6ff4b1f 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 32eaff355..da34b8a8b 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file array_info.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: barrett, mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 10c15fd0e..69f2957ed 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -1,11 +1,11 @@ /********************* */ /*! \file array_info.h ** \verbatim - ** Original author: lianah - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan, barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp index bf15d379b..e220d279b 100644 --- a/src/theory/arrays/static_fact_manager.cpp +++ b/src/theory/arrays/static_fact_manager.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file static_fact_manager.cpp ** \verbatim - ** Original author: barrett + ** Original author: Clark Barrett <barrett@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index 5e7587348..3ced3db6d 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -1,11 +1,11 @@ /********************* */ /*! \file static_fact_manager.h ** \verbatim - ** Original author: barrett + ** Original author: Clark Barrett <barrett@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9c28b3a42..7b727c35b 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arrays.cpp ** \verbatim - ** Original author: barrett - ** Major contributors: mdeters - ** Minor contributors (to current version): ajreynol, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Clark Barrett <barrett@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index b659a8e68..b82d30cbf 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arrays.h ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): ajreynol, barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com>, Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp index 4f7584ac1..ec2bacc4b 100644 --- a/src/theory/arrays/theory_arrays_model.cpp +++ b/src/theory/arrays/theory_arrays_model.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arrays_model.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 9cbb0c9e8..b1e8ea664 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arrays_rewriter.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters, barrett - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 5d7bbbe0b..8c833bc75 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_arrays_type_rules.h ** \verbatim - ** Original author: mdeters - ** Major contributors: barrett - ** Minor contributors (to current version): cconway - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Christopher L. Conway <christopherleeconway@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index ab0f2b366..f7d8b3637 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: mdeters - ** Major contributors: barrett + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index 4801e5ae2..ad9dc2f5d 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file union_find.cpp ** \verbatim - ** Original author: lianah + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index 4b02608ef..b86805a72 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -1,11 +1,11 @@ /********************* */ /*! \file union_find.h ** \verbatim - ** Original author: lianah + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp index f9d80835c..305c41125 100644 --- a/src/theory/booleans/boolean_term_conversion_mode.cpp +++ b/src/theory/booleans/boolean_term_conversion_mode.cpp @@ -1,10 +1,10 @@ /********************* */ /*! \file boolean_term_conversion_mode.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. + ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h index 6ca908df4..e36cc0af1 100644 --- a/src/theory/booleans/boolean_term_conversion_mode.h +++ b/src/theory/booleans/boolean_term_conversion_mode.h @@ -1,10 +1,10 @@ /********************* */ /*! \file boolean_term_conversion_mode.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index a37b03238..d4755d8c4 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file circuit_propagator.cpp ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index de4bb30d2..0e45a53c8 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file circuit_propagator.h ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h index 2bf53b3d2..d06fac0d0 100644 --- a/src/theory/booleans/options_handlers.h +++ b/src/theory/booleans/options_handlers.h @@ -1,11 +1,11 @@ /********************* */ /*! \file options_handlers.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index bb8e0f220..7bcedfdce 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bool.cpp ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index d291e79d6..e41f95c52 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bool.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): ajreynol, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 7a4e91035..911b49ea0 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bool_rewriter.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters, barrett - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Tim King <taking@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index ee46f9c4b..33f24b6d1 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bool_rewriter.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 196a8d749..38d8da259 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bool_type_rules.h ** \verbatim - ** Original author: dejan - ** Major contributors: cconway, mdeters - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Christopher L. Conway <christopherleeconway@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h index 693a20a31..5d5509fb8 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index bc396fae8..c1e5a044e 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_builtin.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index a51cad959..b40aa289f 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_builtin.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index e4703e74c..846c6b23a 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_builtin_rewriter.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index f8483219a..198cea40c 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_builtin_rewriter.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index a369fb572..1eba0da9a 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_builtin_type_rules.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): taking, ajreynol, cconway - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Christopher L. Conway <christopherleeconway@gmail.com>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 9be9d60c1..493ddc535 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index a952b2929..265523c18 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bitblast_strategies.cpp ** \verbatim - ** Original author: lianah + ** Original author: Liana Hadarean <lianahady@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): barrett, dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu>, lianah <lianahady@gmail.com>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h index 749a4c21f..3d9ba5936 100644 --- a/src/theory/bv/bitblast_strategies.h +++ b/src/theory/bv/bitblast_strategies.h @@ -1,11 +1,11 @@ /********************* */ /*! \file bitblast_strategies.h ** \verbatim - ** Original author: lianah + ** Original author: Liana Hadarean <lianahady@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index d3a54a3e4..5f99e33db 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bitblaster.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu>, lianah <lianahady@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 84a67e884..d4ba482ed 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -1,11 +1,11 @@ /********************* */ /*! \file bitblaster.h ** \verbatim - ** Original author: lianah + ** Original author: Liana Hadarean <lianahady@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): mdeters, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): lianah <lianahady@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index ec4b223cf..760a38a16 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_inequality_graph.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: lianah <lianahady@gmail.com> + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index d402b1561..fcb48ed61 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_inequality_graph.h ** \verbatim - ** Original author: lianah - ** Major contributors: none + ** Original author: lianah <lianahady@gmail.com> + ** Major contributors: Liana Hadarean <lianahady@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index ed90e0ebe..ea0eedabb 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_subtheory.h ** \verbatim - ** Original author: lianah - ** Major contributors: dejan - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com>, lianah <lianahady@gmail.com> + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 30eaaa764..1fbab8514 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_subtheory_bitblast.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): lianah, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: lianah <lianahady@gmail.com> + ** Minor contributors (to current version): Dejan Jovanović <dejan@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index b6be84df5..d295b0ee7 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_subtheory_bitblast.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): lianah - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, lianah <lianahady@gmail.com> + ** Minor contributors (to current version): Dejan Jovanović <dejan@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 00777af5c..5853eed50 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file bv_subtheory_eq.cpp +/*! \file bv_subtheory_core.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): lianah - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: lianah <lianahady@gmail.com> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index d314b2fbf..a460c91fa 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file bv_subtheory_eq.h +/*! \file bv_subtheory_core.h ** \verbatim - ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): lianah, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: lianah <lianahady@gmail.com> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 17ac8a2e5..15b51d2c8 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_subtheory_inequality.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: none + ** Original author: lianah <lianahady@gmail.com> + ** Major contributors: Liana Hadarean <lianahady@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index b02233b74..d79ea6e1c 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_subtheory_inequality.h ** \verbatim - ** Original author: lianah + ** Original author: lianah <lianahady@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Liana Hadarean <lianahady@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index ec7f6d66d..518043ec0 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -1,11 +1,11 @@ /********************* */ /*! \file cd_set_collection.h ** \verbatim - ** Original author: dejan + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 2837b075f..fd344aed5 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -1,13 +1,11 @@ /********************* */ -/*! \file slicer.h +/*! \file slicer.cpp ** \verbatim - ** Original author: lianah - ** Major contributors: none + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: lianah <lianahady@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 88254b983..7da12fc6d 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -1,13 +1,11 @@ /********************* */ /*! \file slicer.h ** \verbatim - ** Original author: lianah - ** Major contributors: none + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: lianah <lianahady@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index b202b7eca..39fc68823 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters, lianah - ** Minor contributors (to current version): barrett, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com>, lianah <lianahady@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ff8b3a8b1..c0c8823c1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv.h ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan, lianah - ** Minor contributors (to current version): barrett, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: lianah <lianahady@gmail.com>, Dejan Jovanović <dejan.jovanovic@gmail.com>, Liana Hadarean <lianahady@gmail.com> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu>, Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index bd7a8131a..4000fe77e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewrite_rules.h ** \verbatim - ** Original author: dejan - ** Major contributors: lianah - ** Minor contributors (to current version): barrett, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Liana Hadarean <lianahady@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 178b17b43..c7ce164eb 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewrite_rules_constant_evaluation.h ** \verbatim - ** Original author: lianah - ** Major contributors: barrett - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): lianah <lianahady@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index ade345d1c..e6260e074 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewrite_rules_core.h ** \verbatim - ** Original author: dejan + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): mdeters, barrett, lianah - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 39f55f26c..28ae9d0b3 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewrite_rules_normalization.h ** \verbatim - ** Original author: lianah - ** Major contributors: barrett - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 4202f8c2e..6f54f5a52 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewrite_rules_operator_elimination.h ** \verbatim - ** Original author: lianah - ** Major contributors: barrett - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 9d1cafab9..20e143d2f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewrite_rules_simplification.h ** \verbatim - ** Original author: lianah - ** Major contributors: barrett - ** Minor contributors (to current version): mdeters, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 23018605f..b16c426e6 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewriter.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: lianah - ** Minor contributors (to current version): taking, mdeters, barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Liana Hadarean <lianahady@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 3e7fc272b..1ef936028 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_rewriter.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters, lianah - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index d34e45c63..af331237c 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_type_rules.h ** \verbatim - ** Original author: dejan - ** Major contributors: lianah, mdeters, cconway + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Liana Hadarean <lianahady@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu>, Christopher L. Conway <christopherleeconway@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index f8b9f010e..77e36860d 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_bv_utils.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters, lianah - ** Minor contributors (to current version): barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: lianah <lianahady@gmail.com>, Liana Hadarean <lianahady@gmail.com> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index ff9b8af7c..b68d199ec 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index b503087c9..c0bcf2560 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file datatypes_rewriter.h ** \verbatim - ** Original author: mdeters - ** Major contributors: ajreynol + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a3bec7af0..6be8b5ce8 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_datatypes.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 46212ccbf..236bc0327 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_datatypes.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): dejan, bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): François Bobot <francois@bobot.eu>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 9b4f24566..bed697e5d 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_datatypes_type_rules.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index a4facdefe..bc4f7736a 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/example/ecdata.cpp b/src/theory/example/ecdata.cpp index 06a3aaf97..d6c87b3a0 100644 --- a/src/theory/example/ecdata.cpp +++ b/src/theory/example/ecdata.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file ecdata.cpp ** \verbatim - ** Original author: taking - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/example/ecdata.h b/src/theory/example/ecdata.h index 72b03619c..07f4e551b 100644 --- a/src/theory/example/ecdata.h +++ b/src/theory/example/ecdata.h @@ -1,11 +1,11 @@ /********************* */ /*! \file ecdata.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp index 6caf02e3c..b27bb165f 100644 --- a/src/theory/example/theory_uf_tim.cpp +++ b/src/theory/example/theory_uf_tim.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_tim.cpp ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h index a5e560462..8a2bb4766 100644 --- a/src/theory/example/theory_uf_tim.h +++ b/src/theory/example/theory_uf_tim.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_tim.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index 26d0f5269..39edd8461 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -1,11 +1,11 @@ /********************* */ /*! \file interrupted.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp index 24c6a641a..e799f27ef 100644 --- a/src/theory/ite_simplifier.cpp +++ b/src/theory/ite_simplifier.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file ite_simplifier.cpp ** \verbatim - ** Original author: barrett + ** Original author: Clark Barrett <barrett@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h index 12e88c2ef..6f787b3ff 100644 --- a/src/theory/ite_simplifier.h +++ b/src/theory/ite_simplifier.h @@ -1,11 +1,11 @@ /********************* */ /*! \file ite_simplifier.h ** \verbatim - ** Original author: barrett + ** Original author: Clark Barrett <barrett@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index f90bee19d..16e8aea6c 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file logic_info.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index fd81ea629..12e23fd53 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -1,11 +1,11 @@ /********************* */ /*! \file logic_info.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/model.cpp b/src/theory/model.cpp index b4ac8d27e..26cd11eac 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file model.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters, barrett - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/model.h b/src/theory/model.h index 98eeda97a..15bf42895 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -1,11 +1,11 @@ /********************* */ /*! \file model.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters, barrett - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/options_handlers.h b/src/theory/options_handlers.h index 09b4fddfd..2b6a66366 100644 --- a/src/theory/options_handlers.h +++ b/src/theory/options_handlers.h @@ -1,11 +1,11 @@ /********************* */ /*! \file options_handlers.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 1bb6b5a9c..0b5ee58e2 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -1,11 +1,11 @@ /********************* */ /*! \file output_channel.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): taking, dejan, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Dejan Jovanović <dejan.jovanovic@gmail.com>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index ddcc2b1ae..58c4d2557 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file candidate_generator.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 0f52dc7c3..e185b67d5 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file candidate_generator.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 8272ce168..aa2e342b7 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file first_order_model.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 50a941968..0ccde0746 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -1,11 +1,11 @@ /********************* */ /*! \file first_order_model.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 5a80512cd..64aa212c1 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file inst_match.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): barrett, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu>, François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index b9e61be20..3a3da248c 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -1,11 +1,11 @@ /********************* */ /*! \file inst_match.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: François Bobot <francois@bobot.eu>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 75cc10615..e1fb29440 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file instantiation_engine.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index a7ae1ae8e..eac522aa9 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -1,11 +1,11 @@ /********************* */ /*! \file instantiation_engine.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index d8b154b95..310cd4eed 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file model_builder.cpp ** \verbatim - ** Original author: ajreynol + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Kshitij Bansal <kshitij@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 5490d17dd..4df3e57b0 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -1,11 +1,11 @@ /********************* */ /*! \file model_builder.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 1522d0828..8af0ce501 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file model_engine.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): bobot - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 394ceaf42..c0598dc37 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -1,11 +1,11 @@ /********************* */ /*! \file model_engine.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index c09bfbad4..6b8ea2061 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file modes.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 5be0f2f73..0460cbb41 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -1,11 +1,11 @@ /********************* */ /*! \file modes.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 01538d8cb..ba5f31d99 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -1,11 +1,11 @@ /********************* */ /*! \file options_handlers.h ** \verbatim - ** Original author: mdeters - ** Major contributors: ajreynol + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 35ab3e647..94a178f83 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file quantifiers_rewriter.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 73f5d391f..f7250ca42 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file quantifiers_rewriter.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index ad6c241e7..a8245652e 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file relevant_domain.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 9a080f9f9..7e30e9d92 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -1,11 +1,11 @@ /********************* */ /*! \file relevant_domain.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index f6518cfd3..d638321c6 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file term_database.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e232a382e..c2bdf3cf8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -1,11 +1,11 @@ /********************* */ /*! \file term_database.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index be6dd5b08..523186a4d 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_quantifiers.cpp ** \verbatim - ** Original author: ajreynol + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index b4c8966c7..40609c445 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_quantifiers.h ** \verbatim - ** Original author: ajreynol + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): François Bobot <francois@bobot.eu>, Dejan Jovanović <dejan.jovanovic@gmail.com>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 7671e7e0f..d0741bd63 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_quantifiers_type_rules.h ** \verbatim - ** Original author: ajreynol + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 125829e06..630812e12 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file trigger.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): bobot - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 9ecac0120..1c82f47e9 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -1,11 +1,11 @@ /********************* */ /*! \file trigger.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f12143bbe..955f9c55f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file quantifiers_engine.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot, mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5f288a186..9699dc1f9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -1,11 +1,11 @@ /********************* */ /*! \file quantifiers_engine.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters, bobot - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 5555abef8..def41975b 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file rewriter.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 42579fc0e..2c1ea4c5a 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file rewriter.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index 580a68500..73bde7c12 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -1,11 +1,11 @@ /********************* */ /*! \file rewriter_attributes.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index bdd240c52..8387d3975 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -1,11 +1,11 @@ /********************* */ /*! \file rewriter_tables_template.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp index 3f2895397..1e072d2ad 100644 --- a/src/theory/rewriterules/rr_candidate_generator.cpp +++ b/src/theory/rewriterules/rr_candidate_generator.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file rr_candidate_generator.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h index d12c67f6a..264c44334 100644 --- a/src/theory/rewriterules/rr_candidate_generator.h +++ b/src/theory/rewriterules/rr_candidate_generator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file rr_candidate_generator.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com>, François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index 5c3a55831..fca2780c8 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file rr_inst_match.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h index 636a4dbc1..2314615cf 100644 --- a/src/theory/rewriterules/rr_inst_match.h +++ b/src/theory/rewriterules/rr_inst_match.h @@ -1,11 +1,11 @@ /********************* */ /*! \file rr_inst_match.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/rr_inst_match_impl.h b/src/theory/rewriterules/rr_inst_match_impl.h index 388d1a702..f885333f6 100644 --- a/src/theory/rewriterules/rr_inst_match_impl.h +++ b/src/theory/rewriterules/rr_inst_match_impl.h @@ -1,11 +1,11 @@ /********************* */ /*! \file rr_inst_match_impl.h ** \verbatim - ** Original author: bobot - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp index 4f48a72ae..3583772d7 100644 --- a/src/theory/rewriterules/rr_trigger.cpp +++ b/src/theory/rewriterules/rr_trigger.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file rr_trigger.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): bobot - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com>, François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h index f11d6ed66..49c8021b1 100644 --- a/src/theory/rewriterules/rr_trigger.h +++ b/src/theory/rewriterules/rr_trigger.h @@ -1,11 +1,11 @@ /********************* */ /*! \file rr_trigger.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com>, François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): Tianyi Liang <tianyi-liang@uiowa.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index a82b94f73..4a93dc01b 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index e7a24bb79..f83e549ce 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: bobot - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h index ba37c4843..3c3904f98 100644 --- a/src/theory/rewriterules/theory_rewriterules_params.h +++ b/src/theory/rewriterules/theory_rewriterules_params.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules_params.h ** \verbatim - ** Original author: bobot + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h index 9987b5f17..a826342dd 100644 --- a/src/theory/rewriterules/theory_rewriterules_preprocess.h +++ b/src/theory/rewriterules/theory_rewriterules_preprocess.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules_preprocess.h ** \verbatim - ** Original author: bobot - ** Major contributors: mdeters - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h index 8ddb971a0..1eb08095a 100644 --- a/src/theory/rewriterules/theory_rewriterules_rewriter.h +++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules_rewriter.h ** \verbatim - ** Original author: bobot - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index 20e5fa084..ed549a5d3 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules_rules.cpp ** \verbatim - ** Original author: bobot - ** Major contributors: none - ** Minor contributors (to current version): ajreynol, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: François Bobot <francois@bobot.eu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules_rules.h b/src/theory/rewriterules/theory_rewriterules_rules.h index a7de797f7..0e9360ecf 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules_rules.h ** \verbatim - ** Original author: bobot - ** Major contributors: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h index dd89b054b..35ab30b60 100644 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_rewriterules_type_rules.h ** \verbatim - ** Original author: bobot - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: none + ** Minor contributors (to current version): François Bobot <francois@bobot.eu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index ced845a27..723aca8c9 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file shared_terms_database.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): ajreynol, barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index c7036a9ad..b10941b8f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -1,11 +1,11 @@ /********************* */ /*! \file shared_terms_database.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 8858cc34b..791abaf53 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file substitutions.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters, barrett + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index a199256e7..79cfd3964 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -1,11 +1,11 @@ /********************* */ /*! \file substitutions.h ** \verbatim - ** Original author: mdeters - ** Major contributors: barrett, dejan + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 61b7209f6..56c6eb9f4 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file term_registration_visitor.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters, ajreynol - ** Minor contributors (to current version): taking, barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Clark Barrett <barrett@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 75c4d354c..d68d69c9b 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -1,11 +1,11 @@ /********************* */ /*! \file term_registration_visitor.h ** \verbatim - ** Original author: dejan + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index f513b0d78..187287c71 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory.cpp ** \verbatim - ** Original author: mdeters - ** Major contributors: ajreynol, dejan - ** Minor contributors (to current version): taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Clark Barrett <barrett@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theory.h b/src/theory/theory.h index 94cf9accd..517efbaca 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory.h ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): bobot, taking, barrett, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): François Bobot <francois@bobot.eu>, Dejan Jovanović <dejan@cs.nyu.edu>, Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1c297eda6..e03c3f35c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_engine.cpp ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway, kshitij, taking, barrett, lianah, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Christopher L. Conway <christopherleeconway@gmail.com>, Kshitij Bansal <kshitij@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu>, Tim King <taking@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com>, Clark Barrett <barrett@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f72b824cd..8d5236f18 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_engine.h ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway, bobot, kshitij, taking, barrett, lianah, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Christopher L. Conway <christopherleeconway@gmail.com>, Dejan Jovanović <dejan@cs.nyu.edu>, François Bobot <francois@bobot.eu>, Kshitij Bansal <kshitij@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com>, Clark Barrett <barrett@cs.nyu.edu>, Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h index 0577e9524..dd2702eab 100644 --- a/src/theory/theory_registrar.h +++ b/src/theory/theory_registrar.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_registrar.h ** \verbatim - ** Original author: lianah - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Liana Hadarean <lianahady@gmail.com> + ** Major contributors: Tim King <taking@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 48323ee88..6c79a1c3f 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_test_utils.h ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): ajreynol, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index c2fcedbe0..ab141a7c5 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_traits_template.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h index 9cc3fc026..728dac657 100644 --- a/src/theory/theoryof_mode.h +++ b/src/theory/theoryof_mode.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theoryof_mode.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index 42cb998be..be8557d8f 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index 00faeebd5..712e18237 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file type_enumerator_template.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 016abb2ac..7cc81697a 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file equality_engine.cpp ** \verbatim - ** Original author: dejan + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): taking, bobot, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, François Bobot <francois@bobot.eu>, Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 34cb2443f..f7f803435 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -1,11 +1,11 @@ /********************* */ /*! \file equality_engine.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): bobot, lianah, taking, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Liana Hadarean <lianahady@gmail.com>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Dejan Jovanović <dejan@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 9caa8b1f1..ed543640b 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -1,11 +1,11 @@ /********************* */ /*! \file equality_engine_types.h ** \verbatim - ** Original author: dejan + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/options_handlers.h b/src/theory/uf/options_handlers.h index 5039886e0..85164a843 100644 --- a/src/theory/uf/options_handlers.h +++ b/src/theory/uf/options_handlers.h @@ -1,11 +1,11 @@ /********************* */ /*! \file options_handlers.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 07aafc28d..032ab59cb 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file symmetry_breaker.cpp ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 0b555b01e..7be208fdf 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -1,11 +1,11 @@ /********************* */ /*! \file symmetry_breaker.h ** \verbatim - ** Original author: mdeters + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> ** Major contributors: none ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index bdbb79195..1d492003a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf.cpp ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): barrett, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>, Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 00e270bd0..f03f3e843 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf.h ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking, ajreynol - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Tim King <taking@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index efe3aebf4..6e10c09dd 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_model.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 9e4a3bc00..2644fd517 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_model.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 50d50ae19..c69915f02 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_rewriter.h ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu> ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 25cb8b66c..53403dd60 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_strong_solver.cpp ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 33493248d..6d4144dbb 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_strong_solver.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com> + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 5cc988617..c019a6894 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf_type_rules.h ** \verbatim - ** Original author: dejan - ** Major contributors: cconway, mdeters - ** Minor contributors (to current version): ajreynol, taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Major contributors: Christopher L. Conway <christopherleeconway@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index b9f23cce2..682bbf30c 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file unconstrained_simplifier.cpp ** \verbatim - ** Original author: barrett + ** Original author: Clark Barrett <barrett@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index 5edbdb682..66751375a 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -1,11 +1,11 @@ /********************* */ /*! \file unconstrained_simplifier.h ** \verbatim - ** Original author: barrett + ** Original author: Clark Barrett <barrett@cs.nyu.edu> ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Minor contributors (to current version): Morgan Deters <mdeters@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index c5d2845bd..fdd798f22 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file valuation.cpp ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): ajreynol, barrett, taking - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Andrew Reynolds <andrew.j.reynolds@gmail.com>, Clark Barrett <barrett@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu>, Tim King <taking@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 36e62a402..5f8994493 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -1,11 +1,11 @@ /********************* */ /*! \file valuation.h ** \verbatim - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking, ajreynol, barrett - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** Original author: Morgan Deters <mdeters@cs.nyu.edu> + ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com> + ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Clark Barrett <barrett@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** |