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

fix #1665

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-08 10:30:20 -07:00
parent 29c2672407
commit 63a1b2e714
3 changed files with 17 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/static_features.cpp
View file

@ -81,6 +81,7 @@ void static_features::reset() {
m_has_str = false;
m_has_seq_non_str = false;
m_has_arrays = false;
m_has_ext_arrays = false;
m_arith_k_sum .reset();
m_num_arith_terms = 0;
m_num_arith_eqs = 0;
@ -271,8 +272,11 @@ void static_features::update_core(expr * e) {
m_has_bv = true;
if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e)))
m_has_fpa = true;
if (!m_has_arrays && m_arrayutil.is_array(e))
if (!m_has_arrays && m_arrayutil.is_array(e))
m_has_arrays = true;
if (!m_has_ext_arrays && m_arrayutil.is_array(e) &&
!m_arrayutil.is_select(e) && !m_arrayutil.is_store(e))
m_has_ext_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.str.is_non_string_sequence(e)) {

1
src/ast/static_features.h
View file

@ -82,6 +82,7 @@ struct static_features {
bool m_has_str; // has String-typed terms
bool m_has_seq_non_str; // has non-String-typed Sequence terms
bool m_has_arrays; //
bool m_has_ext_arrays; // does this use extended array theory.
rational m_arith_k_sum; // sum of the numerals in arith atoms.
unsigned m_num_arith_terms;
unsigned m_num_arith_eqs; // equalities of the form t = k where k is a numeral

21
src/smt/smt_setup.cpp
View file

@ -576,17 +576,18 @@ namespace smt {
m_params.m_nnf_cnf = false;
m_params.m_propagate_booleans = true;
m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params));
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AX() {
TRACE("setup", tout << "QF_AX\n";);
m_params.m_array_mode = AR_SIMPLE;
m_params.m_nnf_cnf = false;
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AX(static_features const & st) {
m_params.m_array_mode = AR_SIMPLE;
m_params.m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
m_params.m_nnf_cnf = false;
if (st.m_num_clauses == st.m_num_units) {
m_params.m_relevancy_lvl = 0;
@ -595,7 +596,7 @@ namespace smt {
else {
m_params.m_relevancy_lvl = 2;
}
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AUFLIA() {
@ -607,11 +608,11 @@ namespace smt {
m_params.m_restart_factor = 1.5;
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
setup_i_arith();
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_QF_AUFLIA(static_features const & st) {
m_params.m_array_mode = AR_SIMPLE;
m_params.m_array_mode = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
if (st.m_has_real)
throw default_exception("Benchmark has real variables but it is marked as QF_AUFLIA (arrays, uninterpreted functions and linear integer arithmetic).");
m_params.m_nnf_cnf = false;
@ -631,7 +632,7 @@ namespace smt {
// m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params));
// else
setup_i_arith();
m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
setup_arrays();
}
void setup::setup_AUFLIA(bool simple_array) {
@ -992,17 +993,17 @@ namespace smt {
}
if (st.num_theories() == 1 && st.m_has_arrays) {
setup_QF_AX();
setup_QF_AX(st);
return;
}
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_bv) {
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && !st.m_has_ext_arrays && st.m_has_bv) {
setup_QF_AUFBV();
return;
}
if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_int) {
setup_QF_AUFLIA();
setup_QF_AUFLIA(st);
return;
}