mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

Fixed setup_QF_S(): using configuration to choose the corresponding string solver

Browse source
This commit is contained in:
Thai Trinh 2017-12-08 13:41:18 +08:00
parent b6806eb1c2
commit 2c48ffe7a7
1 changed files with 16 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/smt_setup.cpp
View file

@ -123,8 +123,8 @@ namespace smt {
setup_QF_FP();
else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
setup_QF_FPBV();
// else if (m_logic == "QF_S")
// setup_QF_S();
else if (m_logic == "QF_S")
setup_QF_S();
else if (m_logic == "QF_DT")
setup_QF_DT();
else
@ -170,8 +170,8 @@ namespace smt {
setup_QF_BVRE();
else if (m_logic == "QF_AUFLIA")
setup_QF_AUFLIA(st);
// else if (m_logic == "QF_S")
// setup_QF_S();
else if (m_logic == "QF_S")
setup_QF_S();
else if (m_logic == "AUFLIA")
setup_AUFLIA(st);
else if (m_logic == "AUFLIRA")
@ -723,8 +723,18 @@ namespace smt {
}
void setup::setup_QF_S() {
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
if (m_params.m_string_solver == "z3str3") {
setup_str();
}
else if (m_params.m_string_solver == "seq") {
setup_seq();
}
else if (m_params.m_string_solver == "auto") {
setup_seq();
}
else {
throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
}
}
bool is_arith(static_features const & st) {