mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

refine logging for local search, add handling of <= for opb front-end

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-02 09:25:05 -08:00
parent b0a47ca897
commit a37dfd3ab9
2 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_local_search.cpp
View file

@ -340,7 +340,8 @@ namespace sat {
m_vars[flipvar].m_time_stamp = step;
//if (!m_limit.inc()) break;pick_flip();
}
IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << "(sat-local :tries " << tries << " :steps " << (tries - 1) * max_steps + step
<< " :unsat " << m_unsat_stack.size() << " :time " << timer.get_seconds() << ")\n";);
// the following is for tesing
// tell the SAT solvers about the phase of variables.
@ -351,7 +352,6 @@ namespace sat {
// remove unit clauses from assumptions.
m_constraints.shrink(num_constraints);
//print_solution();
IF_VERBOSE(1, verbose_stream() << timer.get_seconds() << " steps: " << (tries - 1) * max_steps + step << " unsat stack: " << m_unsat_stack.size() << '\n';);
if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true
verify_solution();
extract_model();

5
src/shell/opt_frontend.cpp
View file

@ -254,6 +254,11 @@ class opb {
in.parse_token(";");
break;
}
if (in.parse_token("<=")) {
t = arith.mk_le(t, parse_coeff());
in.parse_token(";");
break;
}
t = arith.mk_add(t, parse_term());
}
opt.add_hard_constraint(t);