mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

z3str3: add is_var() similar to theory_seq's implementation

Browse source
This commit is contained in:
Murphy Berzish 2019-09-26 12:33:04 -04:00 • committed by Nikolaj Bjorner
parent 1c70bcee69
commit f29b033253
2 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_str.cpp
View file

@ -8374,6 +8374,21 @@ namespace smt {
}
}
bool theory_str::is_var(expr * e) const {
ast_manager & m = get_manager();
sort * ex_sort = m.get_sort(e);
sort * str_sort = u.str.mk_string_sort();
// non-string-sort terms cannot be string variables
if (ex_sort != str_sort) return false;
// string constants cannot be variables
if (u.str.is_string(e)) return false;
if (u.str.is_concat(e) || u.str.is_at(e) || u.str.is_extract(e) || u.str.is_replace(e) || u.str.is_itos(e))
return false;
if (m.is_ite(e))
return false;
return true;
}
void theory_str::set_up_axioms(expr * ex) {
ast_manager & m = get_manager();
context & ctx = get_context();
@ -8417,7 +8432,7 @@ namespace smt {
TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
string_int_conversion_terms.push_back(ap);
m_library_aware_axiom_todo.push_back(n);
} else if (/*ap->get_num_args() == 0 &&*/ !u.str.is_string(ap)) {
} else if (is_var(ex)) {
// if ex is a variable, add it to our list of variables
TRACE("str", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;);
variable_set.insert(ex);

1
src/smt/theory_str.h
View file

@ -572,6 +572,7 @@ protected:
expr * z3str2_get_eqc_value(expr * n , bool & hasEqcValue);
bool in_same_eqc(expr * n1, expr * n2);
expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
bool is_var(expr * e) const;
bool get_arith_value(expr* e, rational& val) const;
bool get_len_value(expr* e, rational& val);