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

add tracing for 2157

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-12 20:12:17 -07:00
parent 519e83bce4
commit 75b1e8fe27
5 changed files with 17 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/opt/optsmt.cpp
View file

@ -191,7 +191,10 @@ namespace opt {
SASSERT(delta_per_step.is_int()); SASSERT(delta_per_step.is_int());
SASSERT(delta_per_step.is_pos()); SASSERT(delta_per_step.is_pos());
is_sat = m_s->check_sat(0, nullptr); is_sat = m_s->check_sat(0, nullptr);
TRACE("opt", tout << "check " << is_sat << "\n";); TRACE("opt", tout << "check " << is_sat << "\n";
tout << "lower: " << m_lower[obj_index] << "\n";
tout << "upper: " << m_upper[obj_index] << "\n";
);
if (is_sat == l_true) { if (is_sat == l_true) {
m_s->maximize_objective(obj_index, bound); m_s->maximize_objective(obj_index, bound);
m_s->get_model(m_model); m_s->get_model(m_model);
@ -232,6 +235,8 @@ namespace opt {
} }
m_s->pop(num_scopes); m_s->pop(num_scopes);
TRACE("opt", tout << is_sat << " " << num_scopes << "\n";);
if (is_sat == l_false && !m_model) { if (is_sat == l_false && !m_model) {
return l_false; return l_false;
} }

2
src/smt/theory_lra.cpp
View file

@ -955,6 +955,7 @@ public:
} }
void push_scope_eh() { void push_scope_eh() {
TRACE("arith", tout << "push\n";);
m_scopes.push_back(scope()); m_scopes.push_back(scope());
scope& s = m_scopes.back(); scope& s = m_scopes.back();
s.m_bounds_lim = m_bounds_trail.size(); s.m_bounds_lim = m_bounds_trail.size();
@ -969,6 +970,7 @@ public:
} }
void pop_scope_eh(unsigned num_scopes) { void pop_scope_eh(unsigned num_scopes) {
TRACE("arith", tout << "pop " << num_scopes << "\n";);
if (num_scopes == 0) { if (num_scopes == 0) {
return; return;
} }

6
src/util/lp/lar_core_solver_def.h
View file

@ -278,6 +278,7 @@ void lar_core_solver::solve() {
CASSERT("A_off", !m_r_solver.A_mult_x_is_off()); CASSERT("A_off", !m_r_solver.A_mult_x_is_off());
lp_assert((!settings().use_tableau()) || r_basis_is_OK()); lp_assert((!settings().use_tableau()) || r_basis_is_OK());
if (need_to_presolve_with_double_solver()) { if (need_to_presolve_with_double_solver()) {
TRACE("lar_solver", tout << "presolving\n";);
prefix_d(); prefix_d();
lar_solution_signature solution_signature; lar_solution_signature solution_signature;
vector<unsigned> changes_of_basis = find_solution_signature_with_doubles(solution_signature); vector<unsigned> changes_of_basis = find_solution_signature_with_doubles(solution_signature);
@ -293,6 +294,7 @@ void lar_core_solver::solve() {
lp_assert(!settings().use_tableau() || r_basis_is_OK()); lp_assert(!settings().use_tableau() || r_basis_is_OK());
} else { } else {
if (!settings().use_tableau()) { if (!settings().use_tableau()) {
TRACE("lar_solver", tout << "no tablau\n";);
bool snapped = m_r_solver.snap_non_basic_x_to_bound(); bool snapped = m_r_solver.snap_non_basic_x_to_bound();
lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
if (snapped) if (snapped)
@ -300,8 +302,10 @@ void lar_core_solver::solve() {
} }
if (m_r_solver.m_look_for_feasible_solution_only) if (m_r_solver.m_look_for_feasible_solution_only)
m_r_solver.find_feasible_solution(); m_r_solver.find_feasible_solution();
else else {
TRACE("lar_solver", tout << "solve\n";);
m_r_solver.solve(); m_r_solver.solve();
}
lp_assert(!settings().use_tableau() || r_basis_is_OK()); lp_assert(!settings().use_tableau() || r_basis_is_OK());
} }
if (m_r_solver.get_status() == lp_status::INFEASIBLE) { if (m_r_solver.get_status() == lp_status::INFEASIBLE) {

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

@ -863,6 +863,7 @@ 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", tout << "solve " << this->get_status() << "\n";);
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();
@ -882,6 +883,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve()
} }
one_iteration(); one_iteration();
TRACE("lar_solver", tout << "one iteration: " << this->get_status() << "\n";);
lp_assert(!this->m_using_infeas_costs || this->costs_on_nbasis_are_zeros()); lp_assert(!this->m_using_infeas_costs || this->costs_on_nbasis_are_zeros());
switch (this->get_status()) { switch (this->get_status()) {
case lp_status::OPTIMAL: // double check that we are at optimum case lp_status::OPTIMAL: // double check that we are at optimum

2
src/util/lp/lp_primal_core_solver_tableau_def.h
View file

@ -35,6 +35,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
X t; X t;
int leaving = find_leaving_and_t_tableau(entering, t); int leaving = find_leaving_and_t_tableau(entering, t);
if (leaving == -1) { if (leaving == -1) {
TRACE("lar_solver", tout << "nothing leaving " << entering << "\n";);
this->set_status(lp_status::UNBOUNDED); this->set_status(lp_status::UNBOUNDED);
return; return;
} }
@ -117,6 +118,7 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
} }
else else
one_iteration_tableau(); one_iteration_tableau();
TRACE("lar_solver", tout << "one iteration tableau " << this->get_status() << "\n";);
switch (this->get_status()) { switch (this->get_status()) {
case lp_status::OPTIMAL: // double check that we are at optimum case lp_status::OPTIMAL: // double check that we are at optimum
case lp_status::INFEASIBLE: case lp_status::INFEASIBLE: