diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-07-02 00:09:52 +0000 |
| commit | 83a143b1dd78e5d7f07666fbec1362dd60348116 (patch) | |
| tree | 08400222d94f4760c7155fea787ac7e78b7b0dfc /src/util/stats.h | |
| parent | a8566c313e9b5eb8248eaeea642a9c72c803dcfa (diff) | |
* Added white-box TheoryEngine test that tests the rewriter
* Added regression documentation to test/regress/README
* Added ability to print types of vars in expr printouts
with iomanipulator Node::printtypes(true)... for example,
Warning() << Node::printtypes(true) << n << std::endl;
* Types-printing can be specified on the command line with
--print-expr-types
* Improved type handling facilities and theoryOf().
For now, SORT_TYPE moved from builtin theory to UF theory
to match old behavior.
* Additional gdb debug functionality. Now we have:
debugPrintNode(Node) debugPrintRawNode(Node)
debugPrintTNode(TNode) debugPrintRawTNode(TNode)
debugPrintTypeNode(TypeNode) debugPrintRawTypeNode(TypeNode)
debugPrintNodeValue(NodeValue*) debugPrintRawNodeValue(NodeValue*)
they all print a {Node,TNode,NodeValue*} from the debugger.
The "Raw" versions print a very low-level AST-like form.
The regular versions do the same as operator<<, but force
full printing on (no depth-limiting).
* Other trivial fixes
Diffstat (limited to 'src/util/stats.h')
| -rw-r--r-- | src/util/stats.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/util/stats.h b/src/util/stats.h index 8d3d4cfda..6efe7f856 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** rief [[ Add one-line brief description here ]] + ** \brief [[ Add one-line brief description here ]] ** ** [[ Add lengthier description here ]] ** \todo document this file @@ -31,9 +31,9 @@ namespace CVC4 { #ifdef CVC4_STATISTICS_ON -#define USE_STATISTICS true +# define USE_STATISTICS true #else -#define USE_STATISTICS false +# define USE_STATISTICS false #endif class CVC4_PUBLIC Stat; @@ -50,7 +50,7 @@ public: static inline void registerStat(Stat* s) throw (AssertionException); static inline void unregisterStat(Stat* s) throw (AssertionException); -}; /* class StatisticsRegistry */ +};/* class StatisticsRegistry */ class CVC4_PUBLIC Stat { @@ -106,7 +106,7 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionExceptio /** - * class T must have stream insertion operation defined. + * class T must have stream insertion operation defined. * std::ostream& operator<<(std::ostream&, const T&); */ template<class T> |