diff options
Diffstat (limited to 'src/theory')
26 files changed, 158 insertions, 25 deletions
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 |