mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

local

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-19 08:57:10 -07:00
parent d8ea3023fc
commit 527980e440
2 changed files with 12 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_pb.cpp
View file

@ -1265,6 +1265,7 @@ namespace smt {
} }
} }
unsigned num_compiled_vars, num_compiled_clauses;
if (ctx.get_assignment(thl) == l_true && if (ctx.get_assignment(thl) == l_true &&
ctx.get_assign_level(thl) == ctx.get_base_level()) { ctx.get_assign_level(thl) == ctx.get_base_level()) {
@ -1273,8 +1274,8 @@ namespace smt {
sortnw.m_stats.reset(); sortnw.m_stats.reset();
at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr()); at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr());
ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k)); 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; 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_clauses = sortnw.m_stats.m_num_compiled_clauses;
} }
else { else {
psort_expr ps(ctx, *this); psort_expr ps(ctx, *this);
@ -1283,12 +1284,16 @@ namespace smt {
literal at_least_k = sortnw.ge(true, k, in.size(), in.c_ptr()); 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(~thl, at_least_k, justify(~thl, at_least_k));
ctx.mk_clause(~at_least_k, thl, 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; 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_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() IF_VERBOSE(1, verbose_stream()
<< "(smt.pb compile sorting network bound: " << "(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";); TRACE("pb", tout << thl << "\n";);
// auxiliary clauses get removed when popping scopes. // auxiliary clauses get removed when popping scopes.

4
src/util/sorting_network.h
View file

@ -235,7 +235,7 @@ Notes:
literal mk_at_most_1(bool full, unsigned n, literal const* xs) { literal mk_at_most_1(bool full, unsigned n, literal const* xs) {
literal_vector in(n, xs); literal_vector in(n, xs);
literal result = ctx.fresh(); literal result = fresh();
unsigned inc_size = 4; unsigned inc_size = 4;
while (!in.empty()) { while (!in.empty()) {
literal_vector ors; 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) { void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ors) {
if (!last) { if (!last) {
literal ex = ctx.fresh(); literal ex = fresh();
for (unsigned j = 0; j < n; ++j) { for (unsigned j = 0; j < n; ++j) {
add_clause(ctx.mk_not(xs[j]), ex); add_clause(ctx.mk_not(xs[j]), ex);
} }