diff options
Diffstat (limited to 'src/theory/arith')
35 files changed, 246 insertions, 76 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 0f5a0fd4e..1b3099842 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file approx_simplex.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters + ** 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 "cvc4autoconfig.h" #include "theory/arith/approx_simplex.h" diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index a34c8981d..b32fdef2d 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file approx_simplex.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters + ** 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 "cvc4_private.h" diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp index 62b5fdff1..8a1d2b557 100644 --- a/src/theory/arith/arith_heuristic_pivot_rule.cpp +++ b/src/theory/arith/arith_heuristic_pivot_rule.cpp @@ -2,7 +2,7 @@ /*! \file arith_heuristic_pivot_rule.cpp ** \verbatim ** Original author: Morgan Deters - ** Major contributors: none + ** Major contributors: Tim King ** 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 diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h index 705c3e2f3..78313b81b 100644 --- a/src/theory/arith/arith_heuristic_pivot_rule.h +++ b/src/theory/arith/arith_heuristic_pivot_rule.h @@ -2,7 +2,7 @@ /*! \file arith_heuristic_pivot_rule.h ** \verbatim ** Original author: Morgan Deters - ** Major contributors: none + ** Major contributors: Tim King ** 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 diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 247c09294..f72537965 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -2,8 +2,8 @@ /*! \file arith_rewriter.cpp ** \verbatim ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): Dejan Jovanovic ** 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 diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index bf5261439..8f6f75295 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -2,7 +2,7 @@ /*! \file arith_static_learner.cpp ** \verbatim ** Original author: Tim King - ** Major contributors: Dejan Jovanovic, Morgan Deters + ** Major contributors: Morgan Deters, Dejan Jovanovic ** 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 diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 6b297f2ab..11626c1de 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -2,8 +2,8 @@ /*! \file arith_utilities.h ** \verbatim ** Original author: Tim King - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters ** 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 diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp index ce05383da..d035dde2b 100644 --- a/src/theory/arith/arithvar.cpp +++ b/src/theory/arith/arithvar.cpp @@ -2,7 +2,7 @@ /*! \file arithvar.cpp ** \verbatim ** Original author: Tim King - ** Major contributors: none + ** Major contributors: Morgan Deters ** 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 diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index f0cecc24b..01137a33c 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file attempt_solution_simplex.cpp + ** \verbatim + ** Original author: Tim King + ** 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/attempt_solution_simplex.h" #include "theory/arith/options.h" diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 5bcdc6aab..6e2d86f8a 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.h +/*! \file attempt_solution_simplex.h ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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): 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/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 49c1a94ce..d3793432d 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Morgan Deters ** 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 diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 1e827d316..d4a445b70 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file callbacks.cpp + ** \verbatim + ** Original author: Tim King + ** 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/callbacks.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 718799e9f..fd9369bf1 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file callbacks.h + ** \verbatim + ** Original author: Tim King + ** 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 + **/ + #pragma once diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index e3e9055a7..a828b9e7f 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters + ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic ** 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 diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index a9304ae76..b5acb9149 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.cpp +/*! \file dual_simplex.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 0ec4bc238..9d2152800 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.h +/*! \file dual_simplex.h ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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): 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/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index e99e62505..c0bffdf07 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.cpp +/*! \file fc_simplex.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 51514bcfb..2397ccdba 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.h +/*! \file fc_simplex.h ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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): Morgan Deters + ** 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 899a3a7c6..a72ced0bc 100644 --- a/src/theory/arith/options_handlers.h +++ b/src/theory/arith/options_handlers.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Tim King ** 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 diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index deafb559a..c497adb75 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -2,8 +2,8 @@ /*! \file partial_model.h ** \verbatim ** Original author: Tim King - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters ** 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 diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index d646ca889..b61cadaf8 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters + ** Minor contributors (to current version): Morgan Deters ** 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 diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp index cc3b6a460..ba19d01b1 100644 --- a/src/theory/arith/simplex_update.cpp +++ b/src/theory/arith/simplex_update.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file simplex_update.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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/simplex_update.h b/src/theory/arith/simplex_update.h index 64aa193dd..5a313e305 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file linear_equality.h +/*! \file simplex_update.h ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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 + ** 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/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index c0ee7ad20..2eb258d3b 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.cpp +/*! \file soi_simplex.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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 + ** 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/soi_simplex.h b/src/theory/arith/soi_simplex.h index de565df64..cee6cf81d 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file simplex.h +/*! \file soi_simplex.h ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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): Morgan Deters + ** 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/tableau.cpp b/src/theory/arith/tableau.cpp index 9d06fadc4..22fbf8713 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file tableau.cpp + ** \verbatim + ** Original author: Tim King + ** 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/tableau.h" using namespace std; diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index deed7e7be..3e4cb819b 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file tableau.h + ** \verbatim + ** Original author: Tim King + ** 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 "cvc4_private.h" #pragma once diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp index 7c44f6791..bc0aa4dcd 100644 --- a/src/theory/arith/tableau_sizes.cpp +++ b/src/theory/arith/tableau_sizes.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file tableau_sizes.cpp + ** \verbatim + ** Original author: Tim King + ** 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/tableau_sizes.h" #include "theory/arith/tableau.h" diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h index d6b820300..66b091fab 100644 --- a/src/theory/arith/tableau_sizes.h +++ b/src/theory/arith/tableau_sizes.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file tableau_sizes.h + ** \verbatim + ** Original author: Tim King + ** 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 "cvc4_private.h" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6c7f622ec..395d51d3e 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 - ** 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 + ** Original author: Tim King + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Dejan Jovanovic + ** 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 451f1e8ff..2408094d8 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -2,8 +2,8 @@ /*! \file theory_arith.h ** \verbatim ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic + ** Major contributors: Dejan Jovanovic, Tim King + ** Minor contributors (to current version): Tianyi Liang, Andrew Reynolds ** 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 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index aa2b2a557..002d503d0 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_arith.cpp +/*! \file theory_arith_private.cpp ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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): Andrew Reynolds, Tianyi Liang, Morgan Deters + ** 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_private.h b/src/theory/arith/theory_arith_private.h index 86de3c1a9..710610346 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_arith.cpp +/*! \file theory_arith_private.h ** \verbatim - ** Original author: taking + ** Original author: Tim King ** 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): Andrew Reynolds, Tianyi Liang, Morgan Deters + ** 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_private_forward.h b/src/theory/arith/theory_arith_private_forward.h index 0dc7cdd5b..62980d83d 100644 --- a/src/theory/arith/theory_arith_private_forward.h +++ b/src/theory/arith/theory_arith_private_forward.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file theory_arith_private_forward.h + ** \verbatim + ** Original author: Tim King + ** 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 "cvc4_private.h" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 0d3a578a6..70f55c476 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -2,8 +2,8 @@ /*! \file theory_arith_type_rules.h ** \verbatim ** Original author: Dejan Jovanovic - ** Major contributors: Tim King, Christopher L. Conway, Morgan Deters - ** Minor contributors (to current version): none + ** Major contributors: Christopher L. Conway, Morgan Deters + ** Minor contributors (to current version): Tim King ** 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 |