diff options
69 files changed, 231 insertions, 79 deletions
diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 0b75ee284..76c05fd4d 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): taking, 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/context/cdvector.h b/src/context/cdvector.h index 0076d509f..cb86d5c4d 100644 --- a/src/context/cdvector.h +++ b/src/context/cdvector.h @@ -2,7 +2,7 @@ /*! \file cdvector.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/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 04ebfa94f..3fd3cce28 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -2,7 +2,7 @@ /*! \file expr_manager_template.cpp ** \verbatim ** Original author: dejan - ** Major contributors: cconway, mdeters + ** Major contributors: mdeters, 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/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index aaaaf0026..8e02c8ca4 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -2,8 +2,8 @@ /*! \file expr_manager_template.h ** \verbatim ** Original author: dejan - ** Major contributors: cconway, mdeters - ** Minor contributors (to current version): taking + ** Major contributors: mdeters + ** Minor contributors (to current version): taking, 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/expr/expr_template.h b/src/expr/expr_template.h index becdd46e2..15938b160 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: mdeters - ** Minor contributors (to current version): cconway, taking + ** Minor contributors (to current version): taking, 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/expr/node.h b/src/expr/node.h index 8b64dc781..b5f6307ed 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -2,8 +2,8 @@ /*! \file node.h ** \verbatim ** Original author: mdeters - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): taking + ** Major contributors: dejan + ** Minor contributors (to current version): taking, 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/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5d99fb31e..942906fbd 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -2,8 +2,8 @@ /*! \file node_manager.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): taking, cconway + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): acsys, 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/expr/node_manager.h b/src/expr/node_manager.h index 4f658c507..77f00ab33 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: cconway, dejan - ** Minor contributors (to current version): taking + ** Minor contributors (to current version): acsys, 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/lib/clock_gettime.c b/src/lib/clock_gettime.c index 682269458..b1bc24ed8 100644 --- a/src/lib/clock_gettime.c +++ b/src/lib/clock_gettime.c @@ -1,7 +1,7 @@ /********************* */ /*! \file clock_gettime.c ** \verbatim - ** Original author: + ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h index aac80dadf..e419e16b0 100644 --- a/src/lib/clock_gettime.h +++ b/src/lib/clock_gettime.h @@ -1,7 +1,7 @@ /********************* */ /*! \file clock_gettime.h ** \verbatim - ** Original author: + ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/lib/replacements.h b/src/lib/replacements.h index d38331b66..c930d2654 100644 --- a/src/lib/replacements.h +++ b/src/lib/replacements.h @@ -1,7 +1,7 @@ /********************* */ /*! \file replacements.h ** \verbatim - ** Original author: + ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/main/main.cpp b/src/main/main.cpp index 950e991c6..f0c04e5f6 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -2,8 +2,8 @@ /*! \file main.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): barrett, dejan, taking + ** Major contributors: taking, cconway + ** Minor contributors (to current version): barrett, 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/main/util.cpp b/src/main/util.cpp index 65f6ed329..760bd5258 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): acsys ** 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 289480e2d..fad5edc1e 100644 --- a/src/parser/bounded_token_buffer.h +++ b/src/parser/bounded_token_buffer.h @@ -2,8 +2,8 @@ /*! \file bounded_token_buffer.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/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 2e0e0087c..1bb8f0679 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): mdeters + ** 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/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index cbb9c57a3..9a349785c 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -2,8 +2,8 @@ /*! \file smt2_input.cpp ** \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/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index c719c66da..7b986cf83 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: dejan - ** Minor contributors (to current version): mdeters, cconway + ** Minor contributors (to current version): 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/prop/sat.h b/src/prop/sat.h index 63c17f513..d780230a8 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -2,8 +2,8 @@ /*! \file sat.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking, dejan, cconway - ** Minor contributors (to current version): none + ** Major contributors: taking, cconway, dejan + ** Minor contributors (to current version): barrett ** 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/normal_form.cpp b/src/theory/arith/normal_form.cpp index 14c525267..60f6fa022 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -2,7 +2,7 @@ /*! \file normal_form.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/normal_form.h b/src/theory/arith/normal_form.h index a09437160..2e20c62c5 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -2,7 +2,7 @@ /*! \file normal_form.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.cpp b/src/theory/arith/tableau.cpp index e43458a23..df80c1118 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file tableau.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/tableau.h" diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index dc2c19936..ed173a182 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -2,8 +2,8 @@ /*! \file tableau.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** 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/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8b5f7d3e7..8997138cb 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: barrett ** 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/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 5d0713a89..25083688a 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_arrays_type_rules.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: 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/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index f492041b8..d87aa95b5 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking - ** Minor contributors (to current version): none + ** Minor contributors (to current version): barrett ** 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/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index fddced8ef..20dd56fa7 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_bool_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters + ** Major contributors: mdeters, 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/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index e76b3fb4b..a08ed9b78 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): barrett ** 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 42c9902e5..5d1137d27 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -2,8 +2,8 @@ /*! \file theory_builtin_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): taking + ** Major contributors: cconway, 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/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp index b88a3cc86..fa0650506 100644 --- a/src/theory/bv/equality_engine.cpp +++ b/src/theory/bv/equality_engine.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file equality_engine.cpp + ** \verbatim + ** Original author: dejan + ** 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 "equality_engine.h" using namespace CVC4::theory::bv; diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 9f3064483..8f596723c 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file equality_engine.h + ** \verbatim + ** Original author: dejan + ** 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" #pragma once diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index f957c4f49..bd0d73865 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_bv.cpp + ** \verbatim + ** Original author: dejan + ** 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_bv.h" #include "theory_bv_utils.h" #include "theory_bv_rewrite_rules.h" diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index b71233797..ff5d4c2a2 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -2,8 +2,8 @@ /*! \file theory_bv.h ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): barrett ** 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_rewrite_rules.cpp b/src/theory/bv/theory_bv_rewrite_rules.cpp index 8c5dfc415..637a4269d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.cpp +++ b/src/theory/bv/theory_bv_rewrite_rules.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_bv_rewrite_rules.cpp + ** \verbatim + ** Original author: dejan + ** 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 <vector> #include "expr/node_builder.h" #include "theory_bv_rewrite_rules.h" diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index ea396e32c..eba8f917c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_bv_rewrite_rules.h + ** \verbatim + ** Original author: dejan + ** 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 + **/ + #pragma once #include "cvc4_private.h" diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 7c4ff495e..49b210501 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -2,8 +2,8 @@ /*! \file theory_bv_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: cconway + ** 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/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index ce8298702..6e9dbef3e 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file theory_bv_utils.h + ** \verbatim + ** Original author: dejan + ** 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 + **/ + #pragma once #include <vector> diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index ab94fbcc8..fb2fde589 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking - ** Minor contributors (to current version): none + ** Minor contributors (to current version): barrett ** 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/shared_term_manager.h b/src/theory/shared_term_manager.h index 8b5567e4e..49bd447d7 100644 --- a/src/theory/shared_term_manager.h +++ b/src/theory/shared_term_manager.h @@ -2,8 +2,8 @@ /*! \file shared_term_manager.h ** \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/theory.h b/src/theory/theory.h index 1cce09439..2711a0b95 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan, taking + ** Minor contributors (to current version): dejan, taking, barrett ** 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/theory_engine.cpp b/src/theory/theory_engine.cpp index da161097f..041b6852b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2,8 +2,8 @@ /*! \file theory_engine.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): none + ** Major contributors: barrett + ** Minor contributors (to current version): cconway, 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/theory_engine.h b/src/theory/theory_engine.h index 074d40d05..5227d32f0 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan, taking - ** Minor contributors (to current version): cconway + ** Minor contributors (to current version): cconway, barrett ** 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/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index a0b4651bb..eb6c430ba 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): 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/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 38018112a..b0f899f9b 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_uf_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters + ** Major contributors: cconway, 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/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index 1591cc05c..9a2d252c0 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_uf.h +/*! \file theory_uf_tim.h ** \verbatim ** Original author: taking ** Major contributors: mdeters diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 1435515ad..cdfdb0284 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): acsys ** 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/Assert.h b/src/util/Assert.h index 65c067b7e..87db28d44 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): acsys ** 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/configuration.cpp b/src/util/configuration.cpp index 499b0c8e2..c1b7acd71 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): acsys, 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/util/configuration.h b/src/util/configuration.h index ff89a3d6c..907cd1d31 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): acsys ** 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/configuration_private.h b/src/util/configuration_private.h index 227250745..69c22c964 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -1,8 +1,8 @@ /********************* */ /*! \file configuration_private.h ** \verbatim - ** Original author: cconway - ** Major contributors: none + ** Original author: mdeters + ** Major contributors: cconway, acsys ** 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/util/dynamic_array.h b/src/util/dynamic_array.h index 8672fa1e9..c1298500e 100644 --- a/src/util/dynamic_array.h +++ b/src/util/dynamic_array.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file dynamic_array.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/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index a6cad96d1..692520257 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -2,7 +2,7 @@ /*! \file integer_cln_imp.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/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 233b3aa08..828fb26f3 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** 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/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index 112713aa5..1c2bd7ccd 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -2,7 +2,7 @@ /*! \file integer_gmp_imp.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/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 4b2ab1a79..ecda616f4 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** 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/util/output.h b/src/util/output.h index 84e566e94..d722b10d1 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan, cconway + ** 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/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 7baf8d3bf..b9768e6f5 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -2,7 +2,7 @@ /*! \file rational_cln_imp.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/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index ae172f262..62f4d4376 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.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/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index a0af69b4c..0db1d2fff 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -2,7 +2,7 @@ /*! \file rational_gmp_imp.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/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index ce94dfe24..e4bba78c2 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.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/util/stats.h b/src/util/stats.h index 3a1b85506..43b48140e 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -2,8 +2,8 @@ /*! \file stats.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/context/cdvector_black.h b/test/unit/context/cdvector_black.h index 3e9a7b87b..37a285abe 100644 --- a/test/unit/context/cdvector_black.h +++ b/test/unit/context/cdvector_black.h @@ -2,7 +2,7 @@ /*! \file cdvector_black.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/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index ea1f40eac..5f9ea3db9 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan, cconway + ** Minor contributors (to current version): barrett, dejan, 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/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index e000e618e..32e8da287 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -2,7 +2,7 @@ /*! \file expr_public.h ** \verbatim ** Original author: mdeters - ** Major contributors: dejan + ** Major contributors: cconway, 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) diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 131d96bb9..46fb82546 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -2,7 +2,7 @@ /*! \file node_builder_black.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: cconway, mdeters ** 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/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index def2f7049..a9b902dea 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: barrett ** 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/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 763e03fdb..029bf9f06 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): barrett, 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/theory/theory_black.h b/test/unit/theory/theory_black.h index 0c6a38d0b..193ba3792 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -2,8 +2,8 @@ /*! \file theory_black.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): cconway, dejan + ** Major contributors: barrett, 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/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 148fb80e6..4365e7db2 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): barrett, 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/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h index aec999293..e831dce4a 100644 --- a/test/unit/theory/theory_uf_tim_white.h +++ b/test/unit/theory/theory_uf_tim_white.h @@ -1,9 +1,9 @@ /********************* */ -/*! \file theory_uf_white.h +/*! \file theory_uf_tim_white.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan + ** Major contributors: barrett + ** Minor contributors (to current version): cconway, 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 |