diff options
Diffstat (limited to 'src/util/stats.i')
| -rw-r--r-- | src/util/stats.i | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/util/stats.i b/src/util/stats.i index 5d3b81d4d..6f1ef5367 100644 --- a/src/util/stats.i +++ b/src/util/stats.i @@ -2,6 +2,14 @@ #include "util/stats.h" %} +namespace CVC4 { + template <class T> class CVC4_PUBLIC BackedStat; + + %template(int64_t_BackedStat) BackedStat<int64_t>; + %template(double_BackedStat) BackedStat<double>; + %template(timespec_BackedStat) BackedStat<timespec>; +}/* CVC4 namespace */ + %ignore CVC4::operator<<(std::ostream&, const timespec&); %rename(increment) CVC4::IntStat::operator++(); @@ -19,3 +27,4 @@ %rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&); %include "util/stats.h" + |