summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine_scope.cpp23
-rw-r--r--src/smt/smt_engine_scope.h23
-rw-r--r--src/theory/candidate_generator.cpp6
-rw-r--r--src/theory/rr_inst_match.cpp8
-rw-r--r--src/theory/rr_inst_match.h8
-rw-r--r--src/theory/rr_inst_match_impl.h4
-rw-r--r--src/theory/rr_trigger.cpp8
-rw-r--r--src/theory/rr_trigger.h6
8 files changed, 62 insertions, 24 deletions
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 03298e99a..ec987c25f 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -1,3 +1,22 @@
+/********************* */
+/*! \file smt_engine_scope.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
@@ -6,5 +25,5 @@ namespace smt {
CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL;
-}
-}
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index bcdaefd9f..f10f4e767 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -1,3 +1,22 @@
+/********************* */
+/*! \file smt_engine_scope.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "smt/smt_engine.h"
#include "util/tls.h"
#include "util/Assert.h"
@@ -36,5 +55,5 @@ public:
}
};/* class SmtScope */
-}
-}
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp
index 2563ef0d7..de98d709d 100644
--- a/src/theory/candidate_generator.cpp
+++ b/src/theory/candidate_generator.cpp
@@ -1,11 +1,11 @@
/********************* */
-/*! \file theory_uf_candidate_generator.cpp
+/*! \file candidate_generator.cpp
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp
index 21a309610..0e3e7b9fa 100644
--- a/src/theory/rr_inst_match.cpp
+++ b/src/theory/rr_inst_match.cpp
@@ -1,11 +1,11 @@
/********************* */
-/*! \file inst_match.cpp
+/*! \file rr_inst_match.cpp
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
diff --git a/src/theory/rr_inst_match.h b/src/theory/rr_inst_match.h
index 68b6e1bfd..468fe6a89 100644
--- a/src/theory/rr_inst_match.h
+++ b/src/theory/rr_inst_match.h
@@ -1,11 +1,11 @@
/********************* */
-/*! \file inst_match.h
+/*! \file rr_inst_match.h
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
diff --git a/src/theory/rr_inst_match_impl.h b/src/theory/rr_inst_match_impl.h
index 28bc8c7eb..4bf04cb96 100644
--- a/src/theory/rr_inst_match_impl.h
+++ b/src/theory/rr_inst_match_impl.h
@@ -1,9 +1,9 @@
/********************* */
-/*! \file inst_match_impl.h
+/*! \file rr_inst_match_impl.h
** \verbatim
** Original author: bobot
** Major contributors: none
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): ajreynol, mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp
index ece68d137..5d56147e8 100644
--- a/src/theory/rr_trigger.cpp
+++ b/src/theory/rr_trigger.cpp
@@ -1,11 +1,11 @@
/********************* */
-/*! \file trigger.cpp
+/*! \file rr_trigger.cpp
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): bobot
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
diff --git a/src/theory/rr_trigger.h b/src/theory/rr_trigger.h
index 7ea4ee1a3..bc12666d0 100644
--- a/src/theory/rr_trigger.h
+++ b/src/theory/rr_trigger.h
@@ -1,11 +1,11 @@
/********************* */
-/*! \file trigger.h
+/*! \file rr_trigger.h
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: bobot
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback