diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-08-28 17:39:44 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-28 17:39:44 -0700 |
| commit | d48e117199b766a9a55eaf951d4d5ed80c9b8dc0 (patch) | |
| tree | 9305e53f5e049c41792b269148c6216108c1cd1b | |
| parent | 960147384b7953a352ca9c721f9b93bdac4ff178 (diff) | |
New C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in getIndices. (#4969)
| -rw-r--r-- | src/api/cvc4cpp.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 0a35981d2..51ecea9f2 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -578,7 +578,9 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::REGEXP_OPT, REGEXP_OPT}, {CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE}, {CVC4::Kind::REGEXP_REPEAT, REGEXP_REPEAT}, + {CVC4::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT}, {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP}, + {CVC4::Kind::REGEXP_LOOP_OP, REGEXP_LOOP}, {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, @@ -1321,6 +1323,9 @@ uint32_t Op::getIndices() const i = d_node->getConst<FloatingPointToSBV>().bvs.d_size; break; case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break; + case REGEXP_REPEAT: + i = d_node->getConst<RegExpRepeat>().d_repeatAmount; + break; default: CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" << " kind " << kindToString(k); @@ -1379,6 +1384,11 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const d_node->getConst<FloatingPointToFPGeneric>(); indices = std::make_pair(ext.t.exponent(), ext.t.significand()); } + else if (k == REGEXP_LOOP) + { + CVC4::RegExpLoop ext = d_node->getConst<RegExpLoop>(); + indices = std::make_pair(ext.d_loopMinOcc, ext.d_loopMaxOcc); + } else { CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from" |