mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
force the new arithmetic solver for QF_LIA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
567fbac27f
commit
fc4627a24f
|
@ -166,7 +166,7 @@ namespace opt {
|
|||
return true;
|
||||
}
|
||||
|
||||
#define PASSERT(_e_) if (!(_e_)) { TRACE("opt", display(tout, r);); SASSERT(_e_); }
|
||||
#define PASSERT(_e_) if (!(_e_)) { TRACE("opt1", display(tout, r); display(tout);); SASSERT(_e_); }
|
||||
|
||||
bool model_based_opt::invariant(unsigned index, row const& r) {
|
||||
vector<var> const& vars = r.m_vars;
|
||||
|
@ -539,7 +539,7 @@ namespace opt {
|
|||
rational slack = (abs_src_c - rational::one()) * (abs_dst_c - rational::one());
|
||||
rational dst_val = dst.m_value - x_val*dst_c;
|
||||
rational src_val = src.m_value - x_val*src_c;
|
||||
rational distance = src_c * dst_val + dst_c * src_val + slack;
|
||||
rational distance = abs_src_c * dst_val + abs_dst_c * src_val + slack;
|
||||
bool use_case1 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one();
|
||||
|
||||
#if 0
|
||||
|
@ -655,7 +655,10 @@ namespace opt {
|
|||
|
||||
void model_based_opt::normalize(unsigned row_id) {
|
||||
row& r = m_rows[row_id];
|
||||
if (r.m_vars.empty()) return;
|
||||
if (r.m_vars.empty()) {
|
||||
retire_row(row_id);
|
||||
return;
|
||||
}
|
||||
if (r.m_type == t_mod) return;
|
||||
rational g(abs(r.m_vars[0].m_coeff));
|
||||
bool all_int = g.is_int();
|
||||
|
@ -1092,6 +1095,7 @@ namespace opt {
|
|||
for (unsigned idx : mod_rows) {
|
||||
replace_var(idx, x, u);
|
||||
SASSERT(invariant(idx, m_rows[idx]));
|
||||
normalize(idx);
|
||||
}
|
||||
TRACE("opt1", display(tout << "tableau after replace x under mod\n"););
|
||||
//
|
||||
|
@ -1113,6 +1117,7 @@ namespace opt {
|
|||
// x |-> D*y + u
|
||||
replace_var(row_id, x, D, y, u);
|
||||
visited.insert(row_id);
|
||||
normalize(row_id);
|
||||
}
|
||||
}
|
||||
TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
|
||||
|
|
|
@ -777,7 +777,11 @@ namespace smt {
|
|||
IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
|
||||
bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum;
|
||||
bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only;
|
||||
switch(m_params.m_arith_mode) {
|
||||
auto mode = m_params.m_arith_mode;
|
||||
if (m_logic == "QF_LIA") {
|
||||
mode = AS_NEW_ARITH;
|
||||
}
|
||||
switch(mode) {
|
||||
case AS_NO_ARITH:
|
||||
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
|
||||
break;
|
||||
|
|
|
@ -60,6 +60,7 @@ probe * mk_is_quasi_pb_probe() {
|
|||
// Create SMT solver that does not use cuts
|
||||
static tactic * mk_no_cut_smt_tactic(unsigned rs) {
|
||||
params_ref solver_p;
|
||||
solver_p.set_sym(symbol("smt.logic"), symbol("QF_LIA")); // force smt_setup to use the new solver
|
||||
solver_p.set_uint("arith.branch_cut_ratio", 10000000);
|
||||
solver_p.set_uint("random_seed", rs);
|
||||
return annotate_tactic("no-cut-smt-tactic", using_params(mk_smt_tactic_using(false), solver_p));
|
||||
|
@ -209,15 +210,8 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
|
|||
params_ref quasi_pb_p;
|
||||
quasi_pb_p.set_uint("lia2pb_max_bits", 64);
|
||||
|
||||
params_ref no_cut_p;
|
||||
no_cut_p.set_uint("arith.branch_cut_ratio", 10000000);
|
||||
|
||||
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
#if 0
|
||||
mk_smt_tactic()),
|
||||
#else
|
||||
or_else(mk_ilp_model_finder_tactic(m),
|
||||
mk_pb_tactic(m),
|
||||
and_then(fail_if_not(mk_is_quasi_pb_probe()),
|
||||
|
@ -225,7 +219,6 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
|
|||
mk_fail_if_undecided_tactic()),
|
||||
mk_bounded_tactic(m),
|
||||
mk_smt_tactic())),
|
||||
#endif
|
||||
main_p);
|
||||
|
||||
|
||||
|
|
|
@ -366,8 +366,6 @@ Notes:
|
|||
if (cmp == LE || cmp == EQ || cmp == LE_FULL) {
|
||||
last = k + 1;
|
||||
}
|
||||
bool full = cmp == LE_FULL || cmp == GE_FULL;
|
||||
|
||||
literal_vector carry;
|
||||
for (unsigned i = 0; i < last; ++i) {
|
||||
carry.push_back(ctx.mk_false());
|
||||
|
|
Loading…
Reference in a new issue