From 527980e44064b213453e5b08a96b5f521d924a5e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Oct 2016 08:57:10 -0700 Subject: [PATCH] local Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 15 ++++++++++----- src/util/sorting_network.h | 4 ++-- 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 2461a9db2..973586bcd 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1265,6 +1265,7 @@ namespace smt { } } + unsigned num_compiled_vars, num_compiled_clauses; if (ctx.get_assignment(thl) == l_true && ctx.get_assign_level(thl) == ctx.get_base_level()) { @@ -1273,8 +1274,8 @@ namespace smt { sortnw.m_stats.reset(); at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr()); ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k)); - m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars; - m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses; + num_compiled_vars = sortnw.m_stats.m_num_compiled_vars; + num_compiled_clauses = sortnw.m_stats.m_num_compiled_clauses; } else { psort_expr ps(ctx, *this); @@ -1283,12 +1284,16 @@ namespace smt { literal at_least_k = sortnw.ge(true, k, in.size(), in.c_ptr()); ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k)); ctx.mk_clause(~at_least_k, thl, justify(thl, ~at_least_k)); - m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars; - m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses; + num_compiled_vars = sortnw.m_stats.m_num_compiled_vars; + num_compiled_clauses = sortnw.m_stats.m_num_compiled_clauses; } + m_stats.m_num_compiled_vars += num_compiled_vars; + m_stats.m_num_compiled_clauses += num_compiled_clauses; IF_VERBOSE(1, verbose_stream() << "(smt.pb compile sorting network bound: " - << k << " literals: " << in.size() << ")\n";); + << k << " literals: " << in.size() + << " clauses: " << num_compiled_clauses + << " vars: " << num_compiled_vars << ")\n";); TRACE("pb", tout << thl << "\n";); // auxiliary clauses get removed when popping scopes. diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index 242d4f43e..0a1c0ad55 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -235,7 +235,7 @@ Notes: literal mk_at_most_1(bool full, unsigned n, literal const* xs) { literal_vector in(n, xs); - literal result = ctx.fresh(); + literal result = fresh(); unsigned inc_size = 4; while (!in.empty()) { literal_vector ors; @@ -260,7 +260,7 @@ Notes: void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ors) { if (!last) { - literal ex = ctx.fresh(); + literal ex = fresh(); for (unsigned j = 0; j < n; ++j) { add_clause(ctx.mk_not(xs[j]), ex); }