mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixups to theory_str for regex

Browse source
This commit is contained in:
Murphy Berzish 2018-02-12 17:45:07 -05:00
parent 54206e3674
commit 762129d4c7
2 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_str.cpp
View file

@ -6571,7 +6571,7 @@ namespace smt {
SASSERT(str1.length() == 1); SASSERT(str1.length() == 1);
SASSERT(str2.length() == 1); SASSERT(str2.length() == 1);
return 1 + str2[0] - str1[0]; return 1 + str2[0] - str1[0];
} else if (u.re.is_full(re)) { } else if (u.re.is_full_char(re) || u.re.is_full_seq(re)) {
return 1; return 1;
} else { } else {
TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;); TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);
@ -6613,7 +6613,7 @@ namespace smt {
SASSERT(str1.length() == 1); SASSERT(str1.length() == 1);
SASSERT(str2.length() == 1); SASSERT(str2.length() == 1);
return 1 + str2[0] - str1[0]; return 1 + str2[0] - str1[0];
} else if (u.re.is_full(re)) { } else if (u.re.is_full_char(re) || u.re.is_full_seq(re)) {
return 1; return 1;
} else { } else {
TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;); TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);
@ -6649,8 +6649,10 @@ namespace smt {
} }
} else if (u.re.is_range(re)) { } else if (u.re.is_range(re)) {
return true; return true;
} else if (u.re.is_full(re)) { } else if (u.re.is_full_char(re)) {
return true; return true;
} else if (u.re.is_full_seq(re)) {
return false; // generally unbounded
} else if (u.re.is_complement(re)) { } else if (u.re.is_complement(re)) {
// TODO can we do better? // TODO can we do better?
return false; return false;
@ -6712,8 +6714,10 @@ namespace smt {
SASSERT(str1.length() == 1); SASSERT(str1.length() == 1);
SASSERT(str2.length() == 1); SASSERT(str2.length() == 1);
lens.insert(1); lens.insert(1);
} else if (u.re.is_full(re)) { } else if (u.re.is_full_char(re)) {
lens.insert(1); lens.insert(1);
} else if (u.re.is_full_seq(re)) {
lens.reset();
} else if (u.re.is_complement(re)) { } else if (u.re.is_complement(re)) {
lens.reset(); lens.reset();
} else { } else {
@ -6828,9 +6832,13 @@ namespace smt {
SASSERT(str2.length() == 1); SASSERT(str2.length() == 1);
expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_numeral(rational::one(), true)), m); expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_numeral(rational::one(), true)), m);
return retval; return retval;
} else if (u.re.is_full(re)) { } else if (u.re.is_full_char(re)) {
expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_numeral(rational::one(), true)), m); expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_numeral(rational::one(), true)), m);
return retval; return retval;
} else if (u.re.is_full_seq(re)) {
// match any unbounded string
expr_ref retval(m_autil.mk_ge(lenVar, m_autil.mk_numeral(rational::zero(), true)), m);
return retval;
} else if (u.re.is_complement(re)) { } else if (u.re.is_complement(re)) {
// skip complement for now, in general this is difficult to predict // skip complement for now, in general this is difficult to predict
expr_ref retval(m_autil.mk_ge(lenVar, m_autil.mk_numeral(rational::zero(), true)), m); expr_ref retval(m_autil.mk_ge(lenVar, m_autil.mk_numeral(rational::zero(), true)), m);

1
src/smt/theory_str.h
View file

@ -745,6 +745,7 @@ protected:
void new_diseq_eh(theory_var, theory_var) override; void new_diseq_eh(theory_var, theory_var) override;
theory* mk_fresh(context*) override { return alloc(theory_str, get_manager(), m_params); } theory* mk_fresh(context*) override { return alloc(theory_str, get_manager(), m_params); }
void init(context * ctx) override;
void init_search_eh() override; void init_search_eh() override;
void add_theory_assumptions(expr_ref_vector & assumptions) override; void add_theory_assumptions(expr_ref_vector & assumptions) override;
lbool validate_unsat_core(expr_ref_vector & unsat_core) override; lbool validate_unsat_core(expr_ref_vector & unsat_core) override;