From 527980e44064b213453e5b08a96b5f521d924a5e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Oct 2016 08:57:10 -0700 Subject: [PATCH 1/8] 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); } From 33e7dccd428ab194533811951a1412b49e1e44b1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Oct 2016 09:11:02 -0700 Subject: [PATCH 2/8] merge Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index d4f7bf30e..73e427b0b 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1292,8 +1292,8 @@ namespace smt { IF_VERBOSE(1, verbose_stream() << "(smt.pb compile sorting network bound: " << k << " literals: " << in.size() - << " clauses: " << num_compiled_clauses - << " vars: " << num_compiled_vars << ")\n";); + << " clauses: " << sortnw.m_stats.m_num_compiled_clauses + << " vars: " << sortnw.m_stats.m_num_compiled_vars << ")\n";); // auxiliary clauses get removed when popping scopes. // we have to recompile the circuit after back-tracking. From c68c56b0e7190fa220ad7e0741a6c5eec2b7efa6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Oct 2016 13:09:27 -0700 Subject: [PATCH 3/8] fix incorrect assertion when checking signs of literals, exposed by mitls regressions Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 9 +++++---- src/smt/smt_internalizer.cpp | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5f258fc61..912bbeb36 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3773,15 +3773,16 @@ namespace smt { #ifdef Z3DEBUG for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; - if (m_manager.is_not(expr_lits.get(i))) { + expr* real_atom; + if (expr_signs[i] != l.sign()) { + + VERIFY(m_manager.is_not(expr_lits.get(i), real_atom)); // the sign must have flipped when internalizing - expr * real_atom = to_app(expr_lits.get(i))->get_arg(0); + CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";); SASSERT(real_atom == bool_var2expr(l.var())); - SASSERT(expr_signs[i] != l.sign()); } else { SASSERT(expr_lits.get(i) == bool_var2expr(l.var())); - SASSERT(expr_signs[i] == l.sign()); } } #endif diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 94ce453b4..8028feae6 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -840,7 +840,7 @@ namespace smt { } #endif TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << "\n";); - TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";); + TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";); set_bool_var(id, v); m_bdata.reserve(v+1); m_activity.reserve(v+1); From 6fb358a432ef411341cc18202a52da749dbd76f5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Oct 2016 13:45:10 +0100 Subject: [PATCH 4/8] Build fix for libz3.vcxproj. --- scripts/mk_util.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0fac30e35..84931b47e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3076,6 +3076,11 @@ def mk_vs_proj_property_groups(f, name, target_ext, type): f.write(' Unicode\n') f.write(' false\n') f.write(' \n') + f.write(' \n') + f.write(' %s\n' % type) + f.write(' Unicode\n') + f.write(' false\n') + f.write(' \n') f.write(' \n') f.write(' \n') f.write(' \n') From 02e1bae9cbf1dd386c9ee89631958292ad27e7e0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Oct 2016 14:22:27 +0100 Subject: [PATCH 5/8] whitespace --- .../portfolio/bounded_int2bv_solver.cpp | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index f8b2f5325..8be0788e3 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -14,7 +14,7 @@ Author: Nikolaj Bjorner (nbjorner) 2016-10-23 Notes: - + --*/ #include "bounded_int2bv_solver.h" @@ -76,7 +76,7 @@ public: virtual solver* translate(ast_manager& m, params_ref const& p) { return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p)); } - + virtual void assert_expr(expr * t) { m_assertions.push_back(t); } @@ -89,7 +89,7 @@ public: } virtual void pop_core(unsigned n) { - m_assertions.reset(); + m_assertions.reset(); m_solver->pop(n); if (n > 0) { @@ -109,7 +109,7 @@ public: while (n > 0) { dealloc(m_bounds.back()); - m_bounds.pop_back(); + m_bounds.pop_back(); --n; } } @@ -120,25 +120,25 @@ public: } virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } - virtual void get_model(model_ref & mdl) { + virtual void get_model(model_ref & mdl) { m_solver->get_model(mdl); if (mdl) { extend_model(mdl); - filter_model(mdl); + filter_model(mdl); } - } + } virtual proof * get_proof() { return m_solver->get_proof(); } virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } - virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } - virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { flush_assertions(); expr_ref_vector bvars(m); for (unsigned i = 0; i < vars.size(); ++i) { @@ -201,7 +201,7 @@ private: value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true)); } TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";); - ext.insert(it->m_key, value); + ext.insert(it->m_key, value); } ext(mdl, 0); } @@ -224,7 +224,7 @@ private: if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) { func_decl* fbv; rational offset; - if (!m_int2bv.find(f, fbv)) { + if (!m_int2bv.find(f, fbv)) { rational n = hi - lo + rational::one(); unsigned num_bits = get_num_bits(n); expr_ref b(m); @@ -253,11 +253,11 @@ private: sub.insert(e, t); } else { - IF_VERBOSE(1, + IF_VERBOSE(1, verbose_stream() << "unprocessed entry: " << mk_pp(e, m) << "\n"; if (bm.has_lower(e, lo, s1)) { verbose_stream() << "lower: " << lo << " " << s1 << "\n"; - } + } if (bm.has_upper(e, hi, s2)) { verbose_stream() << "upper: " << hi << " " << s2 << "\n"; }); @@ -284,7 +284,7 @@ private: bm(m_assertions[i].get()); } expr_safe_replace sub(m); - accumulate_sub(sub); + accumulate_sub(sub); proof_ref proof(m); expr_ref fml1(m), fml2(m); if (sub.empty()) { @@ -292,7 +292,7 @@ private: } else { for (unsigned i = 0; i < m_assertions.size(); ++i) { - sub(m_assertions[i].get(), fml1); + sub(m_assertions[i].get(), fml1); m_rewriter(fml1, fml2, proof); m_solver->assert_expr(fml2); TRACE("int2bv", tout << fml2 << "\n";); From f1412d3f3249529224f4180f601652da210b274a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Oct 2016 14:23:01 +0100 Subject: [PATCH 6/8] Bugfix for bouned_int2bv_solver --- src/tactic/portfolio/bounded_int2bv_solver.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 8be0788e3..0b136dda7 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -294,6 +294,10 @@ private: for (unsigned i = 0; i < m_assertions.size(); ++i) { sub(m_assertions[i].get(), fml1); m_rewriter(fml1, fml2, proof); + if (m.canceled()) { + m_rewriter.reset(); + return; + } m_solver->assert_expr(fml2); TRACE("int2bv", tout << fml2 << "\n";); } From 2475f3bff59a0e15fbc9560e0896856f817faf87 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Oct 2016 07:41:27 -0700 Subject: [PATCH 7/8] ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/enum2bv_solver.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index b0f11cb91..e89f9d188 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -102,9 +102,20 @@ public: datatype_util dt(m); bv_util bv(m); + expr_ref_vector bvars(m), conseq(m), bounds(m); + + // ensure that enumeration variables that + // don't occur in the constraints + // are also internalized. + for (unsigned i = 0; i < vars.size(); ++i) { + expr_ref tmp(m.mk_eq(vars[i], vars[i]), m); + proof_ref proof(m); + m_rewriter(tmp, tmp, proof); + } + m_rewriter.flush_side_constraints(bounds); + m_solver->assert_expr(bounds); // translate enumeration constants to bit-vectors. - expr_ref_vector bvars(m), conseq(m); for (unsigned i = 0; i < vars.size(); ++i) { func_decl* f; if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { From 7764148dd3a247dc1f799dbcdaf67e5a0e7d3443 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Oct 2016 07:42:27 -0700 Subject: [PATCH 8/8] merge Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 459c11a32..154f3a6a3 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3778,14 +3778,8 @@ namespace smt { #ifdef Z3DEBUG for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; -<<<<<<< HEAD - expr* real_atom; - if (expr_signs[i] != l.sign()) { - -======= if (expr_signs[i] != l.sign()) { expr* real_atom; ->>>>>>> f1412d3f3249529224f4180f601652da210b274a VERIFY(m_manager.is_not(expr_lits.get(i), real_atom)); // the sign must have flipped when internalizing CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";);