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

add common utility to set up seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-02 20:52:39 -07:00
parent 52dfdedb9b
commit 1177be6391
2 changed files with 21 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/smt/smt_setup.cpp
View file

@ -205,7 +205,7 @@ namespace smt {
void setup::setup_QF_BVRE() { void setup::setup_QF_BVRE() {
setup_QF_BV(); setup_QF_BV();
setup_QF_LIA(); setup_QF_LIA();
m_context.register_plugin(alloc(theory_seq, m_manager)); setup_seq();
} }
void setup::setup_QF_UF(static_features const & st) { void setup::setup_QF_UF(static_features const & st) {
@ -705,7 +705,7 @@ namespace smt {
} }
void setup::setup_QF_S() { void setup::setup_QF_S() {
m_context.register_plugin(alloc(smt::theory_seq, m_manager)); setup_seq();
} }
bool is_arith(static_features const & st) { bool is_arith(static_features const & st) {
@ -822,19 +822,23 @@ namespace smt {
m_context.register_plugin(mk_theory_dl(m_manager)); m_context.register_plugin(mk_theory_dl(m_manager));
} }
void setup::setup_seq(static_features const & st) { void setup::setup_seq_str(static_features const & st) {
// check params for what to do here when it's ambiguous // check params for what to do here when it's ambiguous
if (m_params.m_string_solver == "z3str3") { if (m_params.m_string_solver == "z3str3") {
setup_str(); setup_str();
} else if (m_params.m_string_solver == "seq") { }
m_context.register_plugin(alloc(smt::theory_seq, m_manager)); else if (m_params.m_string_solver == "seq") {
} else if (m_params.m_string_solver == "auto") { setup_seq();
}
else if (m_params.m_string_solver == "auto") {
if (st.m_has_seq_non_str) { if (st.m_has_seq_non_str) {
m_context.register_plugin(alloc(smt::theory_seq, m_manager)); setup_seq();
} else { }
else {
setup_str(); setup_str();
} }
} else { }
else {
throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'"); throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
} }
} }
@ -852,6 +856,10 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_seq, m_manager)); m_context.register_plugin(alloc(smt::theory_seq, m_manager));
} }
void setup::setup_seq() {
m_context.register_plugin(alloc(smt::theory_seq, m_manager));
}
void setup::setup_unknown() { void setup::setup_unknown() {
static_features st(m_manager); static_features st(m_manager);
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
@ -861,7 +869,7 @@ namespace smt {
setup_bv(); setup_bv();
setup_datatypes(); setup_datatypes();
setup_dl(); setup_dl();
setup_seq(st); setup_seq_str(st);
setup_card(); setup_card();
setup_fpa(); setup_fpa();
} }
@ -876,7 +884,7 @@ namespace smt {
setup_datatypes(); setup_datatypes();
setup_bv(); setup_bv();
setup_dl(); setup_dl();
setup_seq(st); setup_seq_str(st);
setup_card(); setup_card();
setup_fpa(); setup_fpa();
return; return;

3
src/smt/smt_setup.h
View file

@ -94,7 +94,8 @@ namespace smt {
void setup_bv(); void setup_bv();
void setup_arith(); void setup_arith();
void setup_dl(); void setup_dl();
void setup_seq(static_features const & st); void setup_seq_str(static_features const & st);
void setup_seq();
void setup_card(); void setup_card();
void setup_i_arith(); void setup_i_arith();
void setup_mi_arith(); void setup_mi_arith();