diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-19 12:20:44 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-20 10:45:23 -0600 |
| commit | 392196b3fdec72302bb408d87f136761a4c9c170 (patch) | |
| tree | a86459995ad160f7a75d722bfa44f570e9d9a3d3 /src | |
| parent | cf73d7b9f09bda2356c62d16fab03853e48bacbc (diff) | |
add negative int2str
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 28 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 6 |
2 files changed, 24 insertions, 10 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6e8e9ea00..f97f4a8ae 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1270,7 +1270,14 @@ builtinOp[CVC4::Kind& kind] if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); } } - + //NEW string + //STRCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; } + //STRREVCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; } + //STRHEAD_TOK { $kind = CVC4::kind::STRING_CONCAT; } + //STRTAIL_TOK { $kind = CVC4::kind::STRING_CONCAT; } + //STRLAST_TOK { $kind = CVC4::kind::STRING_CONCAT; } + //STRFIRST_TOK { $kind = CVC4::kind::STRING_CONCAT; } + //OLD string | STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; } | STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; } | STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; } @@ -1280,8 +1287,8 @@ builtinOp[CVC4::Kind& kind] | STRREPL_TOK { $kind = CVC4::kind::STRING_STRREPL; } | STRPREF_TOK { $kind = CVC4::kind::STRING_PREFIX; } | STRSUFF_TOK { $kind = CVC4::kind::STRING_SUFFIX; } - | STRITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } - | STRSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } + | SITOS_TOK { $kind = CVC4::kind::STRING_ITOS; } + | SSTOI_TOK { $kind = CVC4::kind::STRING_STOI; } | STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; } | STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; } | RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; } @@ -1290,7 +1297,7 @@ builtinOp[CVC4::Kind& kind] | RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; } | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; } | REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; } - | RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; } + | RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; } // NOTE: Theory operators go here ; @@ -1652,7 +1659,14 @@ BV2NAT_TOK : 'bv2nat'; INT2BV_TOK : 'int2bv'; //STRING -//STRCST_TOK : 'str.cst'; +//NEW +//STRCONS_TOK : 'str.cons'; +//STRREVCONS_TOK : 'str.revcons'; +//STRHEAD_TOK : 'str.head'; +//STRTAIL_TOK : 'str.tail'; +//STRLAST_TOK : 'str.last'; +//STRFIRST_TOK : 'str.first'; +//OLD STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; STRSUB_TOK : 'str.substr' ; @@ -1662,8 +1676,8 @@ STRIDOF_TOK : 'str.indexof' ; STRREPL_TOK : 'str.replace' ; STRPREF_TOK : 'str.prefixof' ; STRSUFF_TOK : 'str.suffixof' ; -STRITOS_TOK : 'int.to.str' ; -STRSTOI_TOK : 'str.to.int' ; +SITOS_TOK : 'int.to.str' ; +SSTOI_TOK : 'str.to.int' ; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; RECON_TOK : 're.++'; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 43e7829bb..6520f5517 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -232,7 +232,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } } else if( t.getKind() == kind::STRING_ITOS ) { if(options::stringExp()) { - Node num = t[0];//NodeManager::currentNM()->mkNode(kind::ABS, t[0]); + Node num = NodeManager::currentNM()->mkNode(kind::ABS, t[0]); Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); @@ -306,13 +306,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); new_nodes.push_back( conc ); - /* + Node sign = NodeManager::currentNM()->mkNode(kind::ITE, NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero), NodeManager::currentNM()->mkConst(::CVC4::String("")), NodeManager::currentNM()->mkConst(::CVC4::String("-"))); conc = t.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sign, pret) ); - new_nodes.push_back( conc );*/ + new_nodes.push_back( conc ); d_cache[t] = t; retNode = t; |