diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-15 17:20:27 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-15 17:21:18 -0600 |
| commit | 0619ddd0da84b91218dbef492e1abb09a4558c3f (patch) | |
| tree | 432d9879d204d35a18dccbe6decc6ac0b443d463 /src/printer/smt2/smt2_printer.cpp | |
| parent | 0ba5fd5e3f44ec5d3f45596662d6e573ec9b93ed (diff) | |
adds smt2 print for strings
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c56d87da6..409c9b4dd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -273,6 +273,24 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::STORE: case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; + // string theory + case kind::STRING_CONCAT: out << "str.++ "; break; + case kind::STRING_IN_REGEXP: out << "str.in.re "; break; + case kind::STRING_LENGTH: out << "str.len "; break; + case kind::STRING_SUBSTR: out << "str.substr "; break; + case kind::STRING_STRCTN: out << "str.contain "; break; + case kind::STRING_CHARAT: out << "str.at "; break; + case kind::STRING_STRIDOF: out << "str.indexof "; break; + case kind::STRING_STRREPL: out << "str.replace "; break; + case kind::STRING_TO_REGEXP: out << "str.to.re "; break; + case kind::REGEXP_CONCAT: out << "re.++ "; break; + case kind::REGEXP_OR: out << "re.or "; break; + case kind::REGEXP_INTER: out << "re.itr "; break; + case kind::REGEXP_STAR: out << "re.* "; break; + case kind::REGEXP_PLUS: out << "re.+ "; break; + case kind::REGEXP_OPT: out << "re.opt "; break; + case kind::REGEXP_RANGE: out << "re.range "; break; + // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; break; case kind::BITVECTOR_AND: out << "bvand "; break; |