Signature optimization

Kernel/Signature.hpp

@@ -523,15 +523,6 @@ class Signature
     return result;
   }
 
-  unsigned addIntegerConstant(const std::string& number, bool defaultSort)
-  { return addNumeralConstant(IntegerConstantType(number), defaultSort); }
-
-  unsigned addRationalConstant(const std::string& numerator, const std::string& denominator,bool defaultSort)
-  { return addNumeralConstant(RationalConstantType(IntegerConstantType(numerator), IntegerConstantType(denominator)), defaultSort); }
-
-  unsigned addRealConstant(const std::string& number,bool defaultSort)
-  { return addNumeralConstant(RealConstantType(number), defaultSort); }
-
  private:
   void noteOccurrence(IntegerConstantType const&)  { _integers++; }
   void noteOccurrence(RationalConstantType const&)  { _rationals++; }

Kernel/Theory.cpp

@@ -54,14 +54,17 @@ using namespace Lib;
 
 namespace Kernel {
 
-IntegerConstantType::IntegerConstantType(std::string const& str)
-  : Kernel::IntegerConstantType()
+Option<IntegerConstantType> IntegerConstantType::parse(std::string const& str)
 {
-  if (-1 == mpz_set_str(_val, str.c_str(), /* base */ 10)) {
-    throw UserErrorException("not a valid integer literal: ", str);
+  auto out = IntegerConstantType(0);
+  if (-1 == mpz_set_str(out._val, str.c_str(), /* base */ 10)) {
+    return {};
+  } else {
+    return some(out);
   }
 }
 
+
 #define IMPL_BIN_OP(fun, mpz_fun)                                                              \
   IntegerConstantType IntegerConstantType::fun(const IntegerConstantType& num) const \
   { auto out = IntegerConstantType(0); mpz_fun(out._val, this->_val, num._val); return out; } \
@@ -358,20 +361,18 @@ bool RealConstantType::parseDouble(const std::string& num, RationalConstantType&
   if (neg) {
     newNum = '-'+newNum;
   }
-  IntegerConstantType numerator(newNum);
+  auto numerator = IntegerConstantType::parse(newNum).unwrap();
   res = RationalConstantType(numerator, denominator);
   return true;
 }
 
 
-RealConstantType::RealConstantType(const std::string& number)
-  : RealConstantType()
+Option<RealConstantType> RealConstantType::parse(std::string const& number)
 {
 
   RationalConstantType value;
   if (parseDouble(number, value))  {
-    *this = RealConstantType(std::move(value));
-    return;
+    return some(RealConstantType(std::move(value)));
   } else {
     throw UserErrorException("invalid decimal literal");
   }
@@ -1616,34 +1617,6 @@ Term* Theory::representConstant(const RealConstantType& num)
   return Term::create(func, 0, 0);
 }
 
-Term* Theory::representIntegerConstant(std::string str)
-{
-  try {
-    return Theory::instance()->representConstant(IntegerConstantType(str));
-  }
-  catch(ArithmeticException&) {
-    NOT_IMPLEMENTED;
-//    bool added;
-//    unsigned fnNum = env.signature->addFunction(str, 0, added);
-//    if (added) {
-//      env.signature->getFunction(fnNum)->setType(new FunctionType(Sorts::SRT_INTEGER));
-//      env.signature->addToDistinctGroup(fnNum, Signature::INTEGER_DISTINCT_GROUP);
-//    }
-//    else {
-//      ASS(env.signature->getFunction(fnNum))
-//    }
-  }
-}
-
-Term* Theory::representRealConstant(std::string str)
-{
-  try {
-    return Theory::instance()->representConstant(RealConstantType(str));
-  } catch(ArithmeticException&) {
-    NOT_IMPLEMENTED;
-  }
-}
-
 /**
  * Register that a predicate pred with a given polarity has the given
  * template. See tryGetInterpretedLaTeXName for explanation of templates 

Kernel/Theory.hpp

@@ -148,7 +148,6 @@ class IntegerConstantType
 
   IntegerConstantType() { mpz_init(_val); }
   explicit IntegerConstantType(int v) : IntegerConstantType() { mpz_set_si(_val, v); }
-  explicit IntegerConstantType(const std::string& str);
 
   IntegerConstantType(IntegerConstantType     && o) : IntegerConstantType() { mpz_swap(_val, o._val); }
   IntegerConstantType(IntegerConstantType const& o) : IntegerConstantType() {  mpz_set(_val, o._val); }
@@ -160,6 +159,8 @@ class IntegerConstantType
   IntegerConstantType operator+(const IntegerConstantType& num) const;
   IntegerConstantType operator-(const IntegerConstantType& num) const;
 
+  static Option<IntegerConstantType> parse(std::string const&);
+
   IntegerConstantType operator-() const;
   IntegerConstantType operator*(const IntegerConstantType& num) const;
   IntegerConstantType& operator++() { mpz_add_ui(_val,_val,1); return *this; }
@@ -238,13 +239,32 @@ struct RationalConstantType {
 
   static TermList getSort() { return AtomicSort::rationalSort(); }
 
+
+
   RationalConstantType() {}
 
   explicit RationalConstantType(int n);
   explicit RationalConstantType(IntegerConstantType num);
   RationalConstantType(int num, int den);
   RationalConstantType(IntegerConstantType num, IntegerConstantType den);
 
+  static Option<RationalConstantType> parse(std::string const& number)
+  {
+    size_t i = number.find_first_of("/");
+    if (i == std::string::npos) {
+      return IntegerConstantType::parse(number)
+        .map([](auto x) { return RationalConstantType(std::move(x)); });
+    } else {
+      return IntegerConstantType::parse(number.substr(0,i))
+        .map([&](auto a) {
+            return IntegerConstantType::parse(number.substr(i + 1))
+               .map([&](auto b) {
+                   return RationalConstantType(std::move(a),std::move(b));
+               });
+            }).flatten();
+    }
+  }
+
   RationalConstantType operator+(const RationalConstantType& num) const;
   RationalConstantType operator-(const RationalConstantType& num) const;
   RationalConstantType operator-() const;
@@ -310,7 +330,7 @@ class RealConstantType : public RationalConstantType
   RealConstantType(const RealConstantType&) = default;
   RealConstantType& operator=(const RealConstantType&) = default;
 
-  explicit RealConstantType(const std::string& number);
+  static Option<RealConstantType> parse(std::string const&);
   explicit RealConstantType(const RationalConstantType& rat) : RationalConstantType(rat) {}
   RealConstantType(IntegerConstantType num) : RationalConstantType(num) {}
   RealConstantType(int num, int den) : RationalConstantType(num, den) {}
@@ -644,8 +664,6 @@ class Theory
   Term* representConstant(const RationalConstantType& num);
   Term* representConstant(const RealConstantType& num);
 
-  Term* representIntegerConstant(std::string str);
-  Term* representRealConstant(std::string str);
 private:
   Theory();
   static OperatorType* getConversionOperationType(Interpretation i);

Parse/SMTLIB2.cpp

@@ -1976,7 +1976,7 @@ bool SMTLIB2::parseAsSpecConstant(const std::string& id)
       goto real_constant; // just below
     }
 
-    unsigned symb = TPTP::addIntegerConstant(id,false);
+    unsigned symb = TPTP::addNumeralConstant<IntegerConstantType>(id,false);
     TermList res = TermList(Term::createConstant(symb));
     _results.push(ParseResult(AtomicSort::intSort(),res));
 
@@ -1986,7 +1986,7 @@ bool SMTLIB2::parseAsSpecConstant(const std::string& id)
   if (StringUtils::isPositiveDecimal(id)) {
     real_constant:
 
-    unsigned symb = TPTP::addRealConstant(id,false);
+    unsigned symb = TPTP::addNumeralConstant<RealConstantType>(id,false);
     TermList res = TermList(Term::createConstant(symb));
     _results.push(ParseResult(AtomicSort::realSort(),res));
 
@@ -2624,7 +2624,7 @@ void SMTLIB2::parseRankedFunctionApplication(LExpr* exp)
       USER_ERROR_EXPR("Expected numeral as an argument of a ranked function in "+head->toString());
     }
 
-    unsigned divisorSymb = TPTP::addIntegerConstant(numeral,false);
+    unsigned divisorSymb = TPTP::addNumeralConstant<IntegerConstantType>(numeral,false);
     TermList divisorTerm = TermList(Term::createConstant(divisorSymb));
 
     TermList arg;

Parse/TPTP.cpp

@@ -2893,13 +2893,13 @@ void TPTP::term()
           );
           break;
         case T_INT:
-          number = addIntegerConstant(tok.content,_isFof);
+          number = addNumeralConstant<IntegerConstantType>(tok.content,_isFof);
           break;
         case T_REAL:
-          number = addRealConstant(tok.content,_isFof);
+          number = addNumeralConstant<RealConstantType>(tok.content,_isFof);
           break;
         case T_RAT:
-          number = addRationalConstant(tok.content,_isFof);
+          number = addNumeralConstant<RationalConstantType>(tok.content,_isFof);
           break;
         default:
           ASSERTION_VIOLATION;
@@ -4737,34 +4737,6 @@ TermList TPTP::sortOf(TermList t)
   }
 } // sortOf
 
-/**
- * Add an integer constant by reading it from the std::string name.
- */
-unsigned TPTP::addIntegerConstant(const std::string& name, bool defaultSort)
-{
-  return env.signature->addNumeralConstant(IntegerConstantType(name),defaultSort);
-} // TPTP::addIntegerConstant
-
-/**
- * Add an rational constant by reading it from the std::string name.
- */
-unsigned TPTP::addRationalConstant(const std::string& name, bool defaultSort)
-{
-  size_t i = name.find_first_of("/");
-  ASS(i != std::string::npos);
-  return env.signature->addNumeralConstant(RationalConstantType(
-        IntegerConstantType(name.substr(0,i)),
-        IntegerConstantType(name.substr(i+1))), defaultSort);
-} // TPTP::addRationalConstant
-
-/**
- * Add an real constant by reading it from the std::string name.
- */
-unsigned TPTP::addRealConstant(const std::string& name, bool defaultSort)
-{
-  return env.signature->addNumeralConstant(RealConstantType(name),defaultSort);
-}  // TPTP::addRealConstant
-
 
 /**
  * Add an uninterpreted constant by reading it from the std::string name.

Parse/TPTP.hpp

@@ -815,9 +815,21 @@ class TPTP
   OperatorType* constructOperatorType(Type* t, VList* vars = 0);
 
 public:
-  static unsigned addIntegerConstant(const std::string&, bool defaultSort);
-  static unsigned addRationalConstant(const std::string&, bool defaultSort);
-  static unsigned addRealConstant(const std::string&, bool defaultSort);
+
+  /**
+   * Add a numeral constant by reading it from the std::string name.
+   */
+  template<class Numeral>
+  static unsigned addNumeralConstant(const std::string& name, bool defaultSort)
+  {
+    if (auto n = Numeral::parse(name)) {
+      return env.signature->addNumeralConstant(*n,defaultSort);
+    } else {
+      throw UserErrorException("not a valid ", Numeral::getSort(), " literal: ", name);
+    }
+  } 
+
+
   static unsigned addUninterpretedConstant(const std::string& name, bool& added);
 
   // also here, simply made public static to share the code with another use site

UnitTests/tIntegerConstantType.cpp

@@ -39,6 +39,6 @@ TEST_FUN(to_string)
       "-1111111111111111111111111111111111111111111",
       "1111111189123097123890102111111111111111111",
       }) {
-    ASS_EQ(Output::toString(IntegerConstantType(str)), str);
+    ASS_EQ(Output::toString(IntegerConstantType::parse(str).unwrap()), str);
   }
 }