From: Morgan Deters 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 #include @@ -42,7 +43,7 @@ class Tptp : public Parser { Expr d_uts_op; // The set of expression that already have a bridge std::hash_set d_r_converted; - std::hash_set d_s_converted; + std::hash_map 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: