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

remove stdout

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-25 19:37:19 -07:00
parent bd2ed196e3
commit 88e777748a
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/opt/opt_solver.cpp
View file

@ -229,7 +229,6 @@ namespace opt {
inf_eps val = get_optimizer().maximize(v, blocker, has_shared); inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
get_model(m_model); get_model(m_model);
inf_eps val2; inf_eps val2;
std::cout << m_valid_objectives.size() << " " << i << "\n";
m_valid_objectives[i] = true; m_valid_objectives[i] = true;
TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";); TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";);
if (!m_models[i]) { if (!m_models[i]) {
@ -342,7 +341,6 @@ namespace opt {
smt::theory_var opt_solver::add_objective(app* term) { smt::theory_var opt_solver::add_objective(app* term) {
smt::theory_var v = get_optimizer().add_objective(term); smt::theory_var v = get_optimizer().add_objective(term);
std::cout << "add objective " << v << "\n";
m_objective_vars.push_back(v); m_objective_vars.push_back(v);
m_objective_values.push_back(inf_eps(rational(-1), inf_rational())); m_objective_values.push_back(inf_eps(rational(-1), inf_rational()));
m_objective_terms.push_back(term); m_objective_terms.push_back(term);
@ -438,7 +436,6 @@ namespace opt {
} }
void opt_solver::reset_objectives() { void opt_solver::reset_objectives() {
std::cout << "reset-objectives\n";
m_objective_vars.reset(); m_objective_vars.reset();
m_objective_values.reset(); m_objective_values.reset();
m_objective_terms.reset(); m_objective_terms.reset();