diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.cpp | 7 | ||||
-rw-r--r-- | src/util/Assert.h | 7 | ||||
-rw-r--r-- | src/util/bitvector.cpp | 24 | ||||
-rw-r--r-- | src/util/bitvector.h | 24 | ||||
-rw-r--r-- | src/util/bool.h | 7 | ||||
-rw-r--r-- | src/util/configuration.cpp | 8 | ||||
-rw-r--r-- | src/util/configuration.h | 8 | ||||
-rw-r--r-- | src/util/debug.h | 7 | ||||
-rw-r--r-- | src/util/decision_engine.cpp | 7 | ||||
-rw-r--r-- | src/util/decision_engine.h | 7 | ||||
-rw-r--r-- | src/util/exception.h | 9 | ||||
-rw-r--r-- | src/util/gmp_util.h | 24 | ||||
-rw-r--r-- | src/util/hash.h | 24 | ||||
-rw-r--r-- | src/util/integer.cpp | 9 | ||||
-rw-r--r-- | src/util/integer.h | 9 | ||||
-rw-r--r-- | src/util/model.h | 7 | ||||
-rw-r--r-- | src/util/options.h | 7 | ||||
-rw-r--r-- | src/util/output.cpp | 7 | ||||
-rw-r--r-- | src/util/output.h | 9 | ||||
-rw-r--r-- | src/util/rational.cpp | 9 | ||||
-rw-r--r-- | src/util/rational.h | 11 | ||||
-rw-r--r-- | src/util/result.h | 7 | ||||
-rw-r--r-- | src/util/sexpr.h | 7 | ||||
-rw-r--r-- | src/util/unique_id.h | 7 |
24 files changed, 181 insertions, 71 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 1611f28d3..dbf292108 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -1,5 +1,6 @@ /********************* */ -/** Assert.cpp +/*! \file Assert.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Assertion utility classes, functions, and exceptions. ** ** Assertion utility classes, functions, and exceptions. Implementation. **/ diff --git a/src/util/Assert.h b/src/util/Assert.h index 744782ba2..5333817aa 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -1,5 +1,6 @@ /********************* */ -/** Assert.h +/*! \file Assert.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Assertion utility classes, functions, exceptions, and macros. ** ** Assertion utility classes, functions, exceptions, and macros. **/ diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 125065118..f789313b8 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -1,9 +1,21 @@ -/* - * bitvector.cpp - * - * Created on: Apr 5, 2010 - * Author: dejan - */ +/********************* */ +/*! \file bitvector.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 "bitvector.h" diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 4f6038a81..e3ba969ec 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -1,9 +1,21 @@ -/* - * bitvector.h - * - * Created on: Mar 31, 2010 - * Author: dejan - */ +/********************* */ +/*! \file bitvector.h + ** \verbatim + ** Original author: dejan + ** 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) + ** 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 + **/ #ifndef __CVC4__BITVECTOR_H_ #define __CVC4__BITVECTOR_H_ diff --git a/src/util/bool.h b/src/util/bool.h index edd45b8a0..d2a29c8d5 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -1,5 +1,6 @@ /********************* */ -/** bool.h +/*! \file bool.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multiprecision rational constant. ** ** A multiprecision rational constant. ** This stores the rational as a pair of multiprecision integers, diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 5ed13a139..2a7563f82 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -1,5 +1,6 @@ /********************* */ -/** configuration.cpp +/*! \file configuration.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Implementation of Configuration class, which provides compile-time + ** configuration information about the CVC4 library. ** ** Implementation of Configuration class, which provides compile-time ** configuration information about the CVC4 library. diff --git a/src/util/configuration.h b/src/util/configuration.h index f939d8981..00651202d 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -1,5 +1,6 @@ /********************* */ -/** configuration.h +/*! \file configuration.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,10 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Interface to a public class that provides compile-time information + ** about the CVC4 library. ** ** Interface to a public class that provides compile-time information ** about the CVC4 library. diff --git a/src/util/debug.h b/src/util/debug.h index a99652661..4fc5d5caa 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -1,5 +1,6 @@ /********************* */ -/** debug.h +/*! \file debug.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Debugging things. ** ** Debugging things. ** diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index 06ea283a8..1ef2440c9 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -1,5 +1,6 @@ /********************* */ -/** decision_engine.cpp +/*! \file decision_engine.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief . ** **/ diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 84ace55b2..e1d9e21b7 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -1,5 +1,6 @@ /********************* */ -/** decision_engine.h +/*! \file decision_engine.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A decision engine for CVC4. ** ** A decision engine for CVC4. **/ diff --git a/src/util/exception.h b/src/util/exception.h index 48dcf1244..4893bd3c2 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -1,14 +1,17 @@ /********************* */ -/** exception.h +/*! \file exception.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): 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 ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief CVC4's exception base class and some associated utilities. ** ** CVC4's exception base class and some associated utilities. **/ diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 1849974cd..de237b793 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -1,9 +1,21 @@ -/* - * gmp.h - * - * Created on: Apr 5, 2010 - * Author: dejan - */ +/********************* */ +/*! \file gmp_util.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 + **/ #ifndef __CVC4__GMP_H_ #define __CVC4__GMP_H_ diff --git a/src/util/hash.h b/src/util/hash.h index c72fe47e8..708628c24 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -1,9 +1,21 @@ -/* - * hash.h - * - * Created on: May 8, 2010 - * Author: chris - */ +/********************* */ +/*! \file hash.h + ** \verbatim + ** Original author: cconway + ** 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 + **/ #ifndef __CVC4__HASH_H_ #define __CVC4__HASH_H_ diff --git a/src/util/integer.cpp b/src/util/integer.cpp index a26f2108f..85075fd39 100644 --- a/src/util/integer.cpp +++ b/src/util/integer.cpp @@ -1,14 +1,17 @@ /********************* */ -/** integer.cpp +/*! \file integer.cpp + ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): 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 ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multiprecision rational constant. ** ** A multiprecision rational constant. ** This stores the rational as a pair of multiprecision integers, diff --git a/src/util/integer.h b/src/util/integer.h index 41582d8db..d1921f597 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -1,14 +1,17 @@ /********************* */ -/** integer.h +/*! \file integer.h + ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** 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 ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multiprecision integer constant. ** ** A multiprecision integer constant. **/ diff --git a/src/util/model.h b/src/util/model.h index f807ff963..31fed1f31 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -1,5 +1,6 @@ /********************* */ -/** model.h +/*! \file model.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A model. ** ** A model. **/ diff --git a/src/util/options.h b/src/util/options.h index c7a730b14..7fcf35f00 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,5 +1,6 @@ /********************* */ -/** options.h +/*! \file options.h + ** \verbatim ** Original author: mdeters ** Major contributors: cconway ** Minor contributors (to current version): dejan @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Global (command-line or equivalent) tuning parameters. ** ** Global (command-line or equivalent) tuning parameters. **/ diff --git a/src/util/output.cpp b/src/util/output.cpp index 5d09e1d93..501ef52fd 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -1,5 +1,6 @@ /********************* */ -/** output.cpp +/*! \file output.cpp + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Output utility classes and functions. ** ** Output utility classes and functions. **/ diff --git a/src/util/output.h b/src/util/output.h index ea96606cb..f27ec24da 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -1,14 +1,17 @@ /********************* */ -/** output.h +/*! \file output.h + ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): 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 ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Output utility classes and functions. ** ** Output utility classes and functions. **/ diff --git a/src/util/rational.cpp b/src/util/rational.cpp index 5e9141758..beaa184bb 100644 --- a/src/util/rational.cpp +++ b/src/util/rational.cpp @@ -1,14 +1,17 @@ /********************* */ -/** rational.cpp +/*! \file rational.cpp + ** \verbatim ** Original author: taking - ** 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) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A multi-precision rational constant. ** ** A multi-precision rational constant. **/ diff --git a/src/util/rational.h b/src/util/rational.h index 8218984a7..5e187de7f 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -1,14 +1,17 @@ /********************* */ -/** rational.h +/*! \file rational.h + ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: cconway + ** 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 ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Multi-precision rational constants. ** ** Multi-precision rational constants. **/ diff --git a/src/util/result.h b/src/util/result.h index 679e68763..e76e5605b 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -1,5 +1,6 @@ /********************* */ -/** result.h +/*! \file result.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Encapsulation of the result of a query. ** ** Encapsulation of the result of a query. **/ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index cf9298c4e..f00343729 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -1,5 +1,6 @@ /********************* */ -/** sexpr.cpp +/*! \file sexpr.h + ** \verbatim ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief Simple representation of SMT S-expressions. ** ** Simple representation of SMT S-expressions. **/ diff --git a/src/util/unique_id.h b/src/util/unique_id.h index 54e56da96..67a6c5cff 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -1,5 +1,6 @@ /********************* */ -/** unique_id.h +/*! \file unique_id.h + ** \verbatim ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -8,7 +9,9 @@ ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing - ** information. + ** information.\endverbatim + ** + ** \brief A mechanism for getting a compile-time unique ID. ** ** A mechanism for getting a compile-time unique ID. **/ |