Remove auto-aritization from TPTP parser

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index beeca818e6a890bb53591a4b94dd6a299730a33b..2ae31e8104e80dbff4cdd398d65c889957f80bf8 100644 (file)
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -631,9 +631,9 @@ tffTypedAtom[CVC4::Command*& cmd]
           // as yet, it's undeclared
           CVC4::Expr expr;
           if(type.isFunction()) {
-            expr = PARSER_STATE->mkTffFunction(name, type);
+            expr = PARSER_STATE->mkFunction(name, type);
           } else {
-            expr = PARSER_STATE->mkTffVar(name, type);
+            expr = PARSER_STATE->mkVar(name, type);
           }
           cmd = new DeclareFunctionCommand(name, expr, type);
         }

diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 79092e98fa44196474e8d9a177961bd04e24a6a4..96c608f77c87ef15facfc78858eb5eee3d8b5a4d 100644 (file)
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -154,26 +154,6 @@ public:
 
   inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf);
 
-  inline Expr mkTffVar(std::string& name, const Type& type) {
-    std::string orig = name;
-    std::stringstream ss;
-    ss << name << "_0";
-    name = ss.str();
-    Expr var = mkVar(name, type);
-    defineFunction(orig, var);
-    return var;
-  }
-
-  inline Expr mkTffFunction(std::string& name, const FunctionType& type) {
-    std::string orig = name;
-    std::stringstream ss;
-    ss << name << "_" << type.getArity();
-    name = ss.str();
-    Expr fun = mkFunction(name, type);
-    defineFunction(orig, fun);
-    return fun;
-  }
-
   /** Ugly hack because I don't know how to return an expression from a
       token */
   Expr d_tmp_expr;
@@ -192,10 +172,6 @@ private:
 
 inline void Tptp::makeApplication(Expr& expr, std::string& name,
                                   std::vector<Expr>& args, bool term) {
-  // We distinguish the symbols according to their arities
-  std::stringstream ss;
-  ss << name << "_" << args.size();
-  name = ss.str();
   if(args.empty()) { // Its a constant
     if(isDeclared(name)) { // already appeared
       expr = getVariable(name);
@@ -227,7 +203,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name,
 
 inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) {
   // For SZS ontology compliance.
-  // if we're in cnf() though, conjectures don't result in "Theorem" or
+  // If we're in cnf() though, conjectures don't result in "Theorem" or
   // "CounterSatisfiable".
   if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
     d_hasConjecture = true;