diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-11-03 11:55:52 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-03 13:55:52 -0600 |
commit | 81ac7cd609ef011b615dccefde702fd5b3a5c39f (patch) | |
tree | 1e8e494825322e13cf891aff78cfeb52dcef9b5e /src/printer | |
parent | e2aff722e0b1072e90bd0c77e7030957364283cc (diff) |
Add support for printing `re.loop` and `re.^` (#5392)
In the new SMT-LIB string standard, re.loop and re.^ are indexed
operators but the printer was not updated to print them correctly. This
commit adds support for printing re.loop and re.^.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cdaa61295..5ef1eca2b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -367,6 +367,13 @@ void Smt2Printer::toStream(std::ostream& out, out << "(_ fp.to_sbv_total " << n.getConst<FloatingPointToSBVTotal>().bvs.d_size << ")"; break; + case kind::REGEXP_REPEAT_OP: + out << "(_ re.^ " << n.getConst<RegExpRepeat>().d_repeatAmount << ")"; + break; + case kind::REGEXP_LOOP_OP: + out << "(_ re.loop " << n.getConst<RegExpLoop>().d_loopMinOcc << " " + << n.getConst<RegExpLoop>().d_loopMaxOcc << ")"; + break; default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -669,7 +676,6 @@ void Smt2Printer::toStream(std::ostream& out, case kind::REGEXP_PLUS: case kind::REGEXP_OPT: case kind::REGEXP_RANGE: - case kind::REGEXP_LOOP: case kind::REGEXP_COMPLEMENT: case kind::REGEXP_DIFF: case kind::REGEXP_EMPTY: @@ -677,6 +683,13 @@ void Smt2Printer::toStream(std::ostream& out, case kind::SEQ_UNIT: case kind::SEQ_NTH: case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break; + case kind::REGEXP_REPEAT: + case kind::REGEXP_LOOP: + { + out << n.getOperator() << ' '; + stillNeedToPrintParams = false; + break; + } case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; @@ -1262,6 +1275,7 @@ static string smtKindString(Kind k, Variant v) case kind::REGEXP_PLUS: return "re.+"; case kind::REGEXP_OPT: return "re.opt"; case kind::REGEXP_RANGE: return "re.range"; + case kind::REGEXP_REPEAT: return "re.^"; case kind::REGEXP_LOOP: return "re.loop"; case kind::REGEXP_COMPLEMENT: return "re.comp"; case kind::REGEXP_DIFF: return "re.diff"; |