diff options
69 files changed, 192 insertions, 74 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 761dd6d24..edc4c5fa8 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index a6947c536..2318699e7 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index cb983b006..b0b704de4 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -2,7 +2,7 @@ /*! \file expr_manager_scope.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 80bf37220..ad698975f 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan, cconway + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 8add462e0..a10b43c48 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -2,8 +2,8 @@ /*! \file node_value.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 069f38ce0..225e5f9e0 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -2,8 +2,8 @@ /*! \file type.cpp ** \verbatim ** Original author: cconway - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/type.h b/src/expr/type.h index 2862286ae..be8a57be3 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -2,8 +2,8 @@ /*! \file type.h ** \verbatim ** Original author: cconway - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h index 0f5b522b6..3d5ca229a 100644 --- a/src/expr/type_constant.h +++ b/src/expr/type_constant.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 43d3c761e..b32555b9d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -2,7 +2,7 @@ /*! \file type_node.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/expr/type_node.h b/src/expr/type_node.h index a58d9dc89..1d5f89c60 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -2,7 +2,7 @@ /*! \file type_node.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/main/main.cpp b/src/main/main.cpp index 4dc62f8d3..855bcbdde 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: cconway - ** Minor contributors (to current version): barrett, dejan + ** Minor contributors (to current version): barrett, dejan, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/main/usage.h b/src/main/usage.h index b56f083a5..9fdc6a67b 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -2,8 +2,8 @@ /*! \file usage.h ** \verbatim ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index e621c92de..740d7fae5 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index ca9b2b747..0d5fda89a 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h index 9634f016b..fede14bd1 100644 --- a/src/parser/bounded_token_buffer.h +++ b/src/parser/bounded_token_buffer.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser.h b/src/parser/parser.h index 3e10f632f..1c02aa482 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters, dejan + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 3b62cbc57..139795494 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index ed1ab807b..b63f39d78 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index bbec3299f..bb592857a 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index d08e25ba9..23881c8b9 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 79d5ccb3a..e25b8217b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index b54fe82e9..fe152a7f6 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 829d6a5f8..5156ea2e5 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 1fa8cff1c..c9d0d5ec5 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index ba87cf269..c88b1e265 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -2,8 +2,8 @@ /*! \file cnf_stream.h ** \verbatim ** Original author: taking - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): mdeters, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 64efedd8a..4cc7f1902 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -2,7 +2,7 @@ /*! \file sat.cpp ** \verbatim ** Original author: cconway - ** Major contributors: none + ** Major contributors: mdeters, taking ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/prop/sat.h b/src/prop/sat.h index 992d8ecd2..9e09727e3 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -2,7 +2,7 @@ /*! \file sat.h ** \verbatim ** Original author: mdeters - ** Major contributors: dejan, cconway + ** Major contributors: taking, dejan, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h index 1dc0e900b..f347105e3 100644 --- a/src/theory/arith/arith_activity.h +++ b/src/theory/arith/arith_activity.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_activity.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \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_constants.h b/src/theory/arith/arith_constants.h index c34e86191..4a8fec56f 100644 --- a/src/theory/arith/arith_constants.h +++ b/src/theory/arith/arith_constants.h @@ -2,7 +2,7 @@ /*! \file arith_constants.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp index e40575054..c5068c9fb 100644 --- a/src/theory/arith/arith_propagator.cpp +++ b/src/theory/arith/arith_propagator.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_propagator.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/arith_propagator.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h index a623517fb..7ffcec747 100644 --- a/src/theory/arith/arith_propagator.h +++ b/src/theory/arith/arith_propagator.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_propagator.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \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_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 5c2a1e996..9cd65b2d9 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 704b57ca6..38c72d38d 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -2,7 +2,7 @@ /*! \file arith_rewriter.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index dcfedb7e8..fa3356c60 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -2,7 +2,7 @@ /*! \file arith_utilities.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h index 963f2b969..11f0f71f0 100644 --- a/src/theory/arith/basic.h +++ b/src/theory/arith/basic.h @@ -2,7 +2,7 @@ /*! \file basic.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 55e6b3dc9..f6a460fee 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -2,7 +2,7 @@ /*! \file delta_rational.cpp ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 78d5fb665..26212ec66 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -2,7 +2,7 @@ /*! \file delta_rational.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/ordered_bounds_list.h b/src/theory/arith/ordered_bounds_list.h index d21283afa..4393a382e 100644 --- a/src/theory/arith/ordered_bounds_list.h +++ b/src/theory/arith/ordered_bounds_list.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file ordered_bounds_list.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \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/partial_model.cpp b/src/theory/arith/partial_model.cpp index bd2d5d61e..18993c748 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 44631fdef..bd945002e 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h index 5cf391e64..87bf83e32 100644 --- a/src/theory/arith/slack.h +++ b/src/theory/arith/slack.h @@ -2,7 +2,7 @@ /*! \file slack.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index f270dacb4..7f414db66 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index cb9dc85f7..5d719aa6f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 9b22b14bb..9fb30bdb4 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -1,8 +1,9 @@ /********************* */ -/*! \file theory_arith_type_rules.cpp +/*! \file theory_arith_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 106d1a8da..ab72a0a8c 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2,8 +2,8 @@ /*! \file theory_arrays.cpp ** \verbatim ** Original author: barrett - ** Major contributors: - ** Minor contributors (to current version): + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 69498cfb2..7bc57bcfb 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -2,7 +2,7 @@ /*! \file theory_arrays.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: barrett ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 8843a38c1..b947cee10 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -1,8 +1,9 @@ /********************* */ -/*! \file theory_bool_type_rules.cpp +/*! \file theory_bool_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 0f4fda1a6..19d6e268b 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -1,8 +1,9 @@ /********************* */ -/*! \file builtin_type_rules.cpp +/*! \file theory_builtin_type_rules.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 7dd6c3e60..7aaae7349 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_bv_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 5e83d3728..ba46e18e2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -2,7 +2,7 @@ /*! \file theory.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: taking ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 79eec4301..865fd83a9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -2,7 +2,7 @@ /*! \file theory_engine.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking, dejan + ** Major contributors: dejan, taking ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index cd0b4ef66..a7f6e98ae 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_test_utils.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_public.h" diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 419e3d078..e77de7d33 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -2,7 +2,8 @@ /*! \file theory_uf_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 9440b6df3..7c837083c 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 0febfddfd..928592d9e 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: cconway - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 692d3d742..a425690a5 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/hash.h b/src/util/hash.h index 6a6130886..73c793951 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/integer.h b/src/util/integer.h index f3431334d..d1921f597 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -2,8 +2,8 @@ /*! \file integer.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan, cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan, cconway, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 607075658..6b32c46bb 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 1677e0ce5..8ce82ee7f 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/util/stats.h b/src/util/stats.h index 6efe7f856..f917e8b52 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h index 923df2afb..b1e77c614 100644 --- a/test/unit/expr/declaration_scope_black.h +++ b/test/unit/expr/declaration_scope_black.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index 4d3958278..3b1e96084 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index e839360d7..b130501f5 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index def0a12ed..ee3d9c200 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index d6614b87e..d8c41bf3a 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_arith_white.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include <cxxtest/TestSuite.h> diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index c4e77852b..14fb3406a 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -2,8 +2,8 @@ /*! \file bitvector_black.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h index cd9244996..1c6b03cdf 100644 --- a/test/unit/util/integer_white.h +++ b/test/unit/util/integer_white.h @@ -2,8 +2,8 @@ /*! \file integer_white.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h index 17bd7b245..dcae800d1 100644 --- a/test/unit/util/rational_black.h +++ b/test/unit/util/rational_black.h @@ -2,7 +2,7 @@ /*! \file rational_black.h ** \verbatim ** Original author: cconway - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) |