mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-25 01:50:33 +00:00
Code Activity

remove NOT_IMPLEMENTED_YET

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-22 19:00:04 -07:00
parent cb3d058067
commit f8bf10af4f
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/seq_axioms.cpp
View file

@ -1060,7 +1060,7 @@ namespace seq {
void axioms::replace_re_axiom(expr* e) {
expr* s = nullptr, *r = nullptr, *t = nullptr;
VERIFY(seq.str.is_replace_re(e, s, r, t));
NOT_IMPLEMENTED_YET();
throw default_exception("no support for replace-re");
}
// A basic strategy for supporting replace_all and other
@ -1105,7 +1105,7 @@ namespace seq {
expr_ref branch1(m.mk_eq(len_r, vj), m);
expr_ref test2(m.mk_and(a.mk_gt(len_s, vi), m.mk_eq(vi, a.mk_int(0)), seq.str.mk_is_empty(vp)), m);
expr_ref branch2(m.mk_eq(vr, seq.str.mk_concat(vt, vs)), m);
NOT_IMPLEMENTED_YET();
throw default_exception("no support for replace-all");
#if 0
expr_ref test3(, m);
expr_ref s1(m_sk.mk_prefix_inv(vp, vs), m);
@ -1135,7 +1135,7 @@ namespace seq {
void axioms::replace_re_all_axiom(expr* e) {
expr* s = nullptr, *p = nullptr, *t = nullptr;
VERIFY(seq.str.is_replace_re_all(e, s, p, t));
NOT_IMPLEMENTED_YET();
throw default_exception("no support for replace-re-all");
}