diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-10 01:20:44 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-10 01:20:44 +0000 |
| commit | 05b9f9f137028cc072538cc37df427769fd5eace (patch) | |
| tree | f4e51d4c2cd66192f667c769d1797dcde4b7c22d /src/util | |
| parent | 42e7a38f0a0b38722c2f58ff028a5d3af9337347 (diff) | |
small changes:
* smtlib2 decimal constant can be "1.", i.e. doesn't need digits after the point
* adding CVC4_PUBLIC to rational output operator, otherwise it's unusable for users
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/rational_cln_imp.h | 2 | ||||
| -rw-r--r-- | src/util/rational_gmp_imp.h | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index c2da0e7ed..583983829 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -310,7 +310,7 @@ struct RationalHashStrategy { } };/* struct RationalHashStrategy */ -std::ostream& operator<<(std::ostream& os, const Rational& n); +CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n); }/* CVC4 namespace */ diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index ef0720263..95a15bc5a 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -292,7 +292,7 @@ struct RationalHashStrategy { } };/* struct RationalHashStrategy */ -std::ostream& operator<<(std::ostream& os, const Rational& n); +CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n); }/* CVC4 namespace */ |