diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-03 00:06:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-03 00:06:25 +0000 |
commit | c0558a1625887f4761cfbad371e07af06a49b38b (patch) | |
tree | e711afb3fb25f3e7ee8225d63261407fbef7967e /src/theory/bv | |
parent | 036a23f59bbc23343dc690fd1e147541e79e9b9e (diff) |
file header documentation regenerated with contributors names; no code modified in this commit
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/equality_engine.cpp | 19 | ||||
-rw-r--r-- | src/theory/bv/equality_engine.h | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.cpp | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 19 |
8 files changed, 118 insertions, 4 deletions
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> |