diff options
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
-rw-r--r-- | src/parser/tptp/tptp.cpp | 63 |
1 files changed, 60 insertions, 3 deletions
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); |