mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
local
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
abb13f8c76
commit
d4a24aff1e
|
@ -40,7 +40,7 @@ bool int_solver::has_inf_int() const {
|
|||
int int_solver::find_inf_int_base_column() {
|
||||
unsigned inf_int_count = 0;
|
||||
int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
|
||||
if (j != -1)
|
||||
if (j != -1)
|
||||
return j;
|
||||
if (inf_int_count == 0)
|
||||
return -1;
|
||||
|
@ -58,7 +58,7 @@ int int_solver::get_kth_inf_int(unsigned k) const {
|
|||
|
||||
int int_solver::find_inf_int_nbasis_column() const {
|
||||
for (unsigned j : m_lar_solver->r_nbasis())
|
||||
if (!column_is_int_inf(j))
|
||||
if (!column_is_int_inf(j))
|
||||
return j;
|
||||
return -1;
|
||||
}
|
||||
|
@ -405,7 +405,6 @@ lia_move int_solver::hnf_cut() {
|
|||
}
|
||||
|
||||
lia_move int_solver::check(lp::explanation * e) {
|
||||
++m_number_of_calls;
|
||||
SASSERT(m_lar_solver->ax_is_correct());
|
||||
if (!has_inf_int()) return lia_move::sat;
|
||||
|
||||
|
@ -428,6 +427,7 @@ lia_move int_solver::check(lp::explanation * e) {
|
|||
m_lar_solver->pivot_fixed_vars_from_basis();
|
||||
|
||||
CHECK_RET(patch_nbasic_columns());
|
||||
++m_number_of_calls;
|
||||
CHECK_RET(find_cube());
|
||||
CHECK_RET(hnf_cut());
|
||||
CHECK_RET(gomory_cut());
|
||||
|
|
|
@ -48,6 +48,7 @@ namespace smt {
|
|||
unsigned m_max_min;
|
||||
unsigned m_gb_simplify, m_gb_superpose, m_gb_compute_basis, m_gb_num_processed;
|
||||
unsigned m_nl_branching, m_nl_linear, m_nl_bounds, m_nl_cross_nested;
|
||||
unsigned m_branch_infeasible_int, m_branch_infeasible_var;
|
||||
|
||||
void reset() { memset(this, 0, sizeof(theory_arith_stats)); }
|
||||
theory_arith_stats() { reset(); }
|
||||
|
|
|
@ -1434,6 +1434,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
if (m_params.m_arith_int_eq_branching && branch_infeasible_int_equality()) {
|
||||
++m_stats.m_branch_infeasible_int;
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
|
||||
|
@ -1442,6 +1443,7 @@ namespace smt {
|
|||
TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";);
|
||||
// apply branching
|
||||
branch_infeasible_int_var(int_var);
|
||||
++m_stats.m_branch_infeasible_var;
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -38,6 +38,8 @@ namespace smt {
|
|||
st.update("arith gcd tests", m_stats.m_gcd_tests);
|
||||
st.update("arith ineq splits", m_stats.m_branches);
|
||||
st.update("arith gomory cuts", m_stats.m_gomory_cuts);
|
||||
st.update("arith branch int", m_stats.m_branch_infeasible_int);
|
||||
st.update("arith branch var", m_stats.m_branch_infeasible_var);
|
||||
st.update("arith patches", m_stats.m_patches);
|
||||
st.update("arith patches_succ", m_stats.m_patches_succ);
|
||||
st.update("arith max-min", m_stats.m_max_min);
|
||||
|
|
|
@ -121,6 +121,7 @@ struct stats {
|
|||
unsigned m_nla_explanations;
|
||||
unsigned m_nla_lemmas;
|
||||
unsigned m_assume_eqs;
|
||||
unsigned m_branch;
|
||||
stats() { reset(); }
|
||||
void reset() {
|
||||
memset(this, 0, sizeof(*this));
|
||||
|
@ -2058,6 +2059,7 @@ public:
|
|||
// at this point we have a new unassigned atom that the
|
||||
// SAT core assigns a value to
|
||||
lia_check = l_false;
|
||||
++m_stats.m_branch;
|
||||
break;
|
||||
}
|
||||
case lp::lia_move::cut: {
|
||||
|
@ -3825,6 +3827,7 @@ public:
|
|||
st.update("arith-nla-lemmas", m_stats.m_nla_lemmas);
|
||||
st.update("arith-gomory-cuts", m_stats.m_gomory_cuts);
|
||||
st.update("arith-assume-eqs", m_stats.m_assume_eqs);
|
||||
st.update("arith-branch", m_stats.m_branch);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
Loading…
Reference in a new issue