mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

remove print directive that doesn't compile

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-03 20:48:13 -08:00
parent 0c0e79a937
commit 5c13acbf9f
2 changed files with 18 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_lra.cpp
View file

@ -1704,9 +1704,13 @@ public:
continue; continue;
} }
if (a.is_numeral(q, r2) && r2.is_pos() && is_bounded(n)) { if (a.is_numeral(q, r2) && r2.is_pos()) {
rational val_v = get_value(v); rational val_v = get_value(v);
if (val_v == div(r1, r2)) continue; if (val_v == div(r1, r2)) continue;
if (!is_bounded(n)) {
TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
continue;
}
TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";); TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);
rational div_r = div(r1, r2); rational div_r = div(r1, r2);

27
src/util/lp/lp_primal_core_solver_def.h
View file

@ -357,20 +357,20 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>::try_jump_to_
bool & unlimited) { bool & unlimited) {
switch(this->m_column_types[entering]){ switch(this->m_column_types[entering]){
case column_type::boxed: case column_type::boxed:
if (m_sign_of_entering_delta > 0) { if (m_sign_of_entering_delta > 0) {
t = this->m_upper_bounds[entering] - this->m_x[entering]; t = this->m_upper_bounds[entering] - this->m_x[entering];
if (unlimited || t <= theta){ if (unlimited || t <= theta){
lp_assert(t >= zero_of_type<X>()); lp_assert(t >= zero_of_type<X>());
return true; return true;
}
} else { // m_sign_of_entering_delta == -1
t = this->m_x[entering] - this->m_lower_bounds[entering];
if (unlimited || t <= theta) {
lp_assert(t >= zero_of_type<X>());
return true;
}
} }
return false; } else { // m_sign_of_entering_delta == -1
t = this->m_x[entering] - this->m_lower_bounds[entering];
if (unlimited || t <= theta) {
lp_assert(t >= zero_of_type<X>());
return true;
}
}
return false;
case column_type::upper_bound: case column_type::upper_bound:
if (m_sign_of_entering_delta > 0) { if (m_sign_of_entering_delta > 0) {
t = this->m_upper_bounds[entering] - this->m_x[entering]; t = this->m_upper_bounds[entering] - this->m_x[entering];
@ -863,7 +863,6 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
// returns the number of iterations // returns the number of iterations
template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() { template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
TRACE("lar_solver", pretty_print(tout););
if (numeric_traits<T>::precise() && this->m_settings.use_tableau()) if (numeric_traits<T>::precise() && this->m_settings.use_tableau())
return solve_with_tableau(); return solve_with_tableau();