From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 9 Apr 2013 20:29:59 +0000 (-0400)
Subject: Change TPTP parser to not use the STRING type; this necessary to repurpose strings... 
X-Git-Tag: cvc5-1.0.0~7327
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a48d458af665175509418f434674a3865f74ed69;p=cvc5.git

Change TPTP parser to not use the STRING type; this necessary to repurpose strings for the upcoming string theory
---

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 80736caa5..9e814b358 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -290,7 +290,7 @@ simpleTerm[CVC4::Expr& expr]
   : variable[expr]
   | NUMBER { expr = PARSER_STATE->d_tmp_expr; }
   | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(
-        MK_CONST(AntlrInput::tokenText($DISTINCT_OBJECT))); }
+        AntlrInput::tokenText($DISTINCT_OBJECT)); }
 ;
 
 functionTerm[CVC4::Expr& expr]
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index adaca892f..6b7adbbf7 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -21,6 +21,7 @@
 
 #include "parser/parser.h"
 #include "expr/command.h"
+#include "util/hash.h"
 #include <ext/hash_set>
 #include <cassert>
 
@@ -42,7 +43,7 @@ class Tptp : public Parser {
   Expr d_uts_op;
   // The set of expression that already have a bridge
   std::hash_set<Expr, ExprHashFunction> d_r_converted;
-  std::hash_set<Expr, ExprHashFunction> d_s_converted;
+  std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
 
   //TPTP directory where to find includes
   // empty if none could be determined
@@ -87,32 +88,12 @@ public:
     return ret;
   }
 
-  inline Expr convertStrToUnsorted(Expr expr){
-    ExprManager * em = getExprManager();
-
-    // Create the conversion function If they doesn't exists
-    if(d_stu_op.isNull()){
-      Type t;
-      //Conversion from string to unsorted
-      t = em->mkFunctionType(em->stringType(), d_unsorted);
-      d_stu_op = em->mkVar("$$stu",t);
-      preemptCommand(new DeclareFunctionCommand("$$stu", d_stu_op, t));
-      //Conversion from unsorted to string
-      t = em->mkFunctionType(d_unsorted, em->stringType());
-      d_uts_op = em->mkVar("$$uts",t);
-      preemptCommand(new DeclareFunctionCommand("$$uts", d_uts_op, t));
+  inline Expr convertStrToUnsorted(std::string str) {
+    Expr& e = d_distinct_objects[str];
+    if(e.isNull()) {
+      e = getExprManager()->mkConst(UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1));
     }
-    // Add the inverse in order to show that over the elements that
-    // appear in the problem there is a bijection between unsorted and
-    // rational
-    Expr ret = em->mkExpr(kind::APPLY_UF,d_stu_op,expr);
-    if ( d_s_converted.find(expr) == d_s_converted.end() ){
-      d_s_converted.insert(expr);
-      Expr eq = em->mkExpr(kind::EQUAL,expr,
-                           em->mkExpr(kind::APPLY_UF,d_uts_op,ret));
-      preemptCommand(new AssertCommand(eq));
-    };
-    return ret;
+    return e;
   }
 
 public: