From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 10 Jul 2012 01:20:44 +0000 (+0000)
Subject: small changes:
X-Git-Tag: cvc5-1.0.0~7939
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=05b9f9f137028cc072538cc37df427769fd5eace;p=cvc5.git

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 84d75ceac..2b331c58a 100644
--- 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 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 */