From 31ed442da0503a0653f0f7c26dfcd12318b56ccb Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 10 Jul 2013 15:05:41 -0400
Subject: [PATCH] Remove auto-aritization from TPTP parser

---
 src/parser/tptp/Tptp.g |  4 ++--
 src/parser/tptp/tptp.h | 26 +-------------------------
 2 files changed, 3 insertions(+), 27 deletions(-)

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index beeca818e..2ae31e810 100644
--- 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 79092e98f..96c608f77 100644
--- 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;
-- 
2.30.2