diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:56:45 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-28 22:59:00 -0600 |
| commit | 0e7bfa71e7bea8b832df00d00332b42bf8bca60b (patch) | |
| tree | ce0ac17a6c67030f36b1fa662535a0e84233da29 /src/printer | |
| parent | fb4104e7c5a88741f9ffd55384198af31435df9e (diff) | |
add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b709d7f80..dd6eac0ff 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -346,6 +346,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::REGEXP_PLUS: out << "re.+ "; break; case kind::REGEXP_OPT: out << "re.opt "; break; case kind::REGEXP_RANGE: out << "re.range "; break; + case kind::REGEXP_EMPTY: out << "re.nostr "; break; + case kind::REGEXP_SIGMA: out << "re.allchar "; break; // bv theory case kind::BITVECTOR_CONCAT: out << "concat "; break; |