diff options
Diffstat (limited to 'src/theory/arith')
40 files changed, 173 insertions, 156 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 ** |