mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

use get_sign

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-21 11:15:13 -06:00
parent 4e81085292
commit 683eed0c1e
2 changed files with 22 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/nlsat/nlsat_evaluator.cpp
View file

@ -226,7 +226,7 @@ namespace nlsat {
} }
// Return the sign idx of pinfo // Return the sign idx of pinfo
::sign sign(poly_info const & pinfo, unsigned i) const { ::sign get_sign(poly_info const & pinfo, unsigned i) const {
return m_poly_signs[pinfo.m_first_sign + i]; return m_poly_signs[pinfo.m_first_sign + i];
} }
@ -243,19 +243,19 @@ namespace nlsat {
else if (section_cell_id > c) else if (section_cell_id > c)
break; break;
} }
return sign(pinfo, i); return get_sign(pinfo, i);
} }
else { else {
if (num_roots == 0) if (num_roots == 0)
return sign(pinfo, 0); return get_sign(pinfo, 0);
unsigned root_1_cell_id = cell_id(pinfo, 0); unsigned root_1_cell_id = cell_id(pinfo, 0);
unsigned root_n_cell_id = cell_id(pinfo, num_roots - 1); unsigned root_n_cell_id = cell_id(pinfo, num_roots - 1);
if (c < root_1_cell_id) if (c < root_1_cell_id)
return sign(pinfo, 0); return get_sign(pinfo, 0);
else if (c == root_1_cell_id || c == root_n_cell_id) else if (c == root_1_cell_id || c == root_n_cell_id)
return sign_zero; return sign_zero;
else if (c > root_n_cell_id) else if (c > root_n_cell_id)
return sign(pinfo, num_roots); return get_sign(pinfo, num_roots);
int low = 0; int low = 0;
int high = num_roots-1; int high = num_roots-1;
while (true) { while (true) {
@ -265,7 +265,7 @@ namespace nlsat {
if (high == low + 1) { if (high == low + 1) {
SASSERT(cell_id(pinfo, low) < c); SASSERT(cell_id(pinfo, low) < c);
SASSERT(c < cell_id(pinfo, low+1)); SASSERT(c < cell_id(pinfo, low+1));
return sign(pinfo, low+1); return get_sign(pinfo, low+1);
} }
SASSERT(high > low + 1); SASSERT(high > low + 1);
int mid = low + ((high - low)/2); int mid = low + ((high - low)/2);
@ -381,7 +381,7 @@ namespace nlsat {
\pre All variables of p are assigned in the current interpretation. \pre All variables of p are assigned in the current interpretation.
*/ */
sign eval_sign(poly * p) { ::sign eval_sign(poly * p) {
// TODO: check if it is useful to cache results // TODO: check if it is useful to cache results
SASSERT(m_assignment.is_assigned(max_var(p))); SASSERT(m_assignment.is_assigned(max_var(p)));
return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment); return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment);

26
src/util/lp/int_solver.cpp
View file

@ -285,6 +285,7 @@ lia_move int_solver::run_gcd_test() {
TRACE("int_solver", tout << "gcd-test " << settings().st().m_gcd_calls << "\n";); TRACE("int_solver", tout << "gcd-test " << settings().st().m_gcd_calls << "\n";);
if (!gcd_test()) { if (!gcd_test()) {
settings().st().m_gcd_conflicts++; settings().st().m_gcd_conflicts++;
TRACE("gcd_test", tout << "gcd conflict\n";);
return lia_move::conflict; return lia_move::conflict;
} }
} }
@ -404,29 +405,30 @@ lia_move int_solver::hnf_cut() {
lia_move int_solver::check() { lia_move int_solver::check() {
if (!has_inf_int()) return lia_move::sat; if (!has_inf_int()) return lia_move::sat;
#define CHECK_RET(fn) \
r = fn; \
if (r != lia_move::undef) { TRACE("int_solver", tout << #fn << "\n";); return r; }
m_t.clear(); m_t.clear();
m_k.reset(); m_k.reset();
m_ex.clear(); m_ex.clear();
m_upper = false; m_upper = false;
lia_move r = run_gcd_test(); lia_move r;
if (r != lia_move::undef) return r;
CHECK_RET(run_gcd_test());
check_return_helper pc(m_lar_solver, r); check_return_helper pc(m_lar_solver, r);
if (settings().m_int_pivot_fixed_vars_from_basis) if (settings().m_int_pivot_fixed_vars_from_basis)
m_lar_solver->pivot_fixed_vars_from_basis(); m_lar_solver->pivot_fixed_vars_from_basis();
r = patch_nbasic_columns(); CHECK_RET(patch_nbasic_columns());
if (r != lia_move::undef) return r;
++m_number_of_calls; ++m_number_of_calls;
r = find_cube(); CHECK_RET(find_cube());
if (r != lia_move::undef) return r; CHECK_RET(hnf_cut());
CHECK_RET(gomory_cut());
r = hnf_cut(); CHECK_RET(branch_or_sat());
if (r != lia_move::undef) return r; return r;
r = gomory_cut();
return (r == lia_move::undef)? branch_or_sat() : r;
} }
lia_move int_solver::branch_or_sat() { lia_move int_solver::branch_or_sat() {