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

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 84d75ceac1ff23f085ad2a4c0c7de3b1ed28a4f4..2b331c58a1f79019fbb43b33ae1ba00d6eb0a87c 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1196,7 +1196,7 @@ fragment NUMERAL
  * Matches a decimal constant from the input.
  */
 DECIMAL_LITERAL
-  : NUMERAL '.' DIGIT+
+  : NUMERAL '.' DIGIT*
   ;
 
 /**

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index c2da0e7ed8d7c43b91d45b0406fcec2797d49089..583983829834ae9f1a915fa98c6422f310624bbd 100644 (file)
--- 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 ef0720263268bec1ed73965948065ed44cdb0281..95a15bc5a852c2d519f1fc8183f4f1288e70e0bc 100644 (file)
--- 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 */