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 /src/parser/tptp/Tptp.g | |
| parent | 4f94986c1eb2a8d5c1ba98528fdcbba1b909d9c8 (diff) | |
Change TPTP parser to not use the STRING type; this necessary to repurpose strings for the upcoming string theory
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 2 |
1 files changed, 1 insertions, 1 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] |