From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 10 Jul 2013 19:05:41 +0000 (-0400)
Subject: Remove auto-aritization from TPTP parser
X-Git-Tag: cvc5-1.0.0~7287^2~67
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=31ed442da0503a0653f0f7c26dfcd12318b56ccb;p=cvc5.git

Remove auto-aritization from TPTP parser
---

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;