From a649c2f95ee929a6d922b9f44cadb4f909b5da6b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 30 Mar 2021 08:52:56 -0500
Subject: [PATCH] Eliminate use of rational from tptp parser (#6239)

---
 src/parser/tptp/Tptp.g   | 18 +-----------
 src/parser/tptp/tptp.cpp | 63 ++++++++++++++++++++++++++++++++++++++--
 src/parser/tptp/tptp.h   | 11 +++++--
 3 files changed, 69 insertions(+), 23 deletions(-)

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 20e57d3a5..08e37392a 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -1759,24 +1759,8 @@ NUMBER
       {
         std::string snum = AntlrInput::tokenText($num);
         std::string sden = AntlrInput::tokenText($den);
-        /* compute the numerator */
-        Integer inum(snum + sden);
-        // The sign
-        inum = pos ? inum : -inum;
-        // The exponent
         size_t exp = ($e == NULL ? 0 : AntlrInput::tokenToUnsigned($e));
-        // Decimal part
-        size_t dec = sden.size();
-        /* multiply it by 10 raised to the exponent reduced by the
-         * number of decimal place in den (dec) */
-        Rational r;
-        if(!posE) r = Rational(inum, Integer(10).pow(exp + dec));
-        else if(exp == dec) r = Rational(inum);
-        else if(exp > dec) r = Rational(inum * Integer(10).pow(exp - dec));
-        else r = Rational(inum, Integer(10).pow(dec - exp));
-        std::stringstream ss;
-        ss << r;
-        PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
+        PARSER_STATE->d_tmp_expr = PARSER_STATE->mkDecimal(snum, sden, pos, exp, posE);
       }
     | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
       { std::stringstream ss;
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 42aac2865..1177c8010 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -9,9 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Definitions of TPTP constants.
- **
- ** Definitions of TPTP constants.
+ ** \brief Definition of TPTP parser.
  **/
 
 // Do not #include "parser/antlr_input.h" directly. Rely on the header.
@@ -369,6 +367,65 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   return d_solver->mkTerm(kind, args);
 }
 
+api::Term Tptp::mkDecimal(
+    std::string& snum, std::string& sden, bool pos, size_t exp, bool posE)
+{
+  // the numerator and the denominator
+  std::stringstream ssn;
+  std::stringstream ssd;
+  if (exp != 0)
+  {
+    if (posE)
+    {
+      // see if we need to pad zeros on the end, e.g. 1.2E5 ---> 120000
+      if (exp >= sden.size())
+      {
+        ssn << snum << sden;
+        for (size_t i = 0, nzero = (exp - sden.size()); i < nzero; i++)
+        {
+          ssn << "0";
+        }
+        ssd << "0";
+      }
+      else
+      {
+        ssn << snum << sden.substr(0, exp);
+        ssd << sden.substr(exp);
+      }
+    }
+    else
+    {
+      // see if we need to pad zeros on the beginning, e.g. 1.2E-5 ---> 0.000012
+      if (exp >= snum.size())
+      {
+        ssn << "0";
+        for (size_t i = 0, nzero = (exp - snum.size()); i < nzero; i++)
+        {
+          ssd << "0";
+        }
+        ssd << snum << sden;
+      }
+      else
+      {
+        ssn << snum.substr(0, exp);
+        ssd << snum.substr(exp) << sden;
+      }
+    }
+  }
+  else
+  {
+    ssn << snum;
+    ssd << sden;
+  }
+  std::stringstream ss;
+  if (!pos)
+  {
+    ss << "-";
+  }
+  ss << ssn.str() << "." << ssd.str();
+  return d_solver->mkReal(ss.str());
+}
+
 void Tptp::forceLogic(const std::string& logic)
 {
   Parser::forceLogic(logic);
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index d0459553f..76ae4ee3e 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -9,9 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Definitions of TPTP constants.
- **
- ** Definitions of TPTP constants.
+ ** \brief Definition of TPTP parser
  **/
 
 #include "parser/antlr_input.h" // Needs to go first.
@@ -176,6 +174,13 @@ class Tptp : public Parser {
    * what is necessary in parsing SMT-LIB.
    */
   api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args);
+  /**
+   * Make decimal, returns a real corresponding to string ( snum "." sden ),
+   * negated if pos is false, having exponent exp, negated exponent if posE is
+   * false.
+   */
+  api::Term mkDecimal(
+      std::string& snum, std::string& sden, bool pos, size_t exp, bool posE);
 
  private:
   void addArithmeticOperators();
-- 
2.30.2