diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-09 16:29:59 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-09 16:29:59 -0400 |
commit | a48d458af665175509418f434674a3865f74ed69 (patch) | |
tree | 9b3ec5f74e75bd7711a5f9250ccc084f8d5e556b | |
parent | 4f94986c1eb2a8d5c1ba98528fdcbba1b909d9c8 (diff) |
Change TPTP parser to not use the STRING type; this necessary to repurpose strings for the upcoming string theory
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 33 |
2 files changed, 8 insertions, 27 deletions
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: |