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

re-enable LRA after fixing dispatch for LRA in smt-setup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-11 09:16:07 -07:00
parent 49d2b86d35
commit 9b3e2a9afe
3 changed files with 23 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_setup.cpp
View file

@ -471,12 +471,16 @@ namespace smt {
setup_r_arith();
}
void setup::setup_QF_LIRA(static_features const& st) {
setup_mi_arith();
}
void setup::setup_QF_LIA() {
TRACE("setup", tout << "setup_QF_LIA(st)\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
setup_i_arith();
}
@ -721,8 +725,8 @@ namespace smt {
void setup::setup_r_arith() {
// to disable theory lra
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
// m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
// m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
}
void setup::setup_mi_arith() {
@ -936,7 +940,9 @@ namespace smt {
}
if (st.num_theories() == 1 && is_arith(st)) {
if (st.m_has_real)
if (st.m_has_int && st.m_has_real)
setup_QF_LIRA(st);
else if (st.m_has_real)
setup_QF_LRA(st);
else
setup_QF_LIA(st);

1
src/smt/smt_setup.h
View file

@ -65,6 +65,7 @@ namespace smt {
void setup_QF_LRA();
void setup_QF_LRA(static_features const & st);
void setup_QF_LIA();
void setup_QF_LIRA(static_features const& st);
void setup_QF_LIA(static_features const & st);
void setup_QF_UFLIA();
void setup_QF_UFLIA(static_features & st);

12
src/tactic/smtlogics/qflra_tactic.cpp
View file

@ -72,5 +72,17 @@ tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
// using_params(mk_smt_tactic(), pivot_p)),
// p);
#if 0
params_ref simplex_0, simplex_1, simplex_2;
simplex_0.set("lp.simplex_strategy", 0);
simplex_1.set("lp.simplex_strategy", 1);
simplex_2.set("lp.simplex_strategy", 1);
tactic* lp_par = par_or(using_params(mk_smt_tactic(), simplex_0),
using_params(mk_smt_tactic(), simplex_1),
using_params(mk_smt_tactic(), simplex_2));
#endif
return using_params(using_params(mk_smt_tactic(), pivot_p), p);
}