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

string/sequence static features test

Browse source
This commit is contained in:
Murphy Berzish 2017-04-24 21:02:22 -04:00
parent 3fe49137d0
commit 54e28a4fe7
3 changed files with 26 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/seq_decl_plugin.h
View file

@ -278,6 +278,17 @@ public:
return is_sort_of(s, m_fid, _STRING_SORT);
}
bool is_non_string_sequence(expr const * n) const {
if (is_string_term(n))
return false;
sort * s = get_sort(n);
if (u.is_seq(s) && !u.is_string(s)) {
return true;
}
return false;
}
MATCH_BINARY(is_concat);
MATCH_UNARY(is_length);
MATCH_TERNARY(is_extract);

3
src/ast/static_features.cpp
View file

@ -284,8 +284,9 @@ void static_features::update_core(expr * e) {
m_has_arrays = true;
if (!m_has_str && m_sequtil.str.is_string_term(e))
m_has_str = true;
if (!m_has_seq_non_str && m_sequtil.is_seq(e))
if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
m_has_seq_non_str = true;
}
if (is_app(e)) {
family_id fid = to_app(e)->get_family_id();
mark_theory(fid);

16
src/smt/smt_setup.cpp
View file

@ -832,6 +832,7 @@ namespace smt {
m_context.register_plugin(alloc(theory_seq, m_manager));
} else if (m_params.m_string_solver == "auto") {
if (st.m_has_seq_non_str) {
NOT_IMPLEMENTED_YET();
m_context.register_plugin(alloc(theory_seq, m_manager));
} else {
setup_str();
@ -856,13 +857,15 @@ namespace smt {
}
void setup::setup_unknown() {
static_features st(m_manager);
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
setup_arith();
setup_arrays();
setup_bv();
setup_datatypes();
setup_dl();
// setup_seq()
m_context.register_plugin(alloc(theory_seq, m_manager));
setup_seq(st);
setup_card();
setup_fpa();
}
@ -966,7 +969,14 @@ namespace smt {
return;
}
// TODO setup_str() by features
if (st.num_theories() == 2 && st.m_has_str && !st.m_has_seq_non_str) {
setup_QF_S();
return;
}
if (st.num_theories() == 2 && st.m_has_seq_non_str) {
m_context.register_plugin(alloc(theory_seq, m_manager));
}
setup_unknown();
}