From 0e966f21ffa13f075cd1256903f10c58e75e45d7 Mon Sep 17 00:00:00 2001 From: martin-neuhaeusser Date: Mon, 30 Jan 2017 17:28:24 +0100 Subject: [PATCH 1/3] Fix off-by-one bug in array indexing in the OCaml bindings This patch fixes an off-by-one bug that occurred in the construction of output arrays in the OCaml bindings. --- scripts/update_api.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 38b6213c1..26f19cc1c 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1477,10 +1477,10 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface pts = ml_plus_type(ts) pops = ml_plus_ops_type(ts) if ml_has_plus_type(ts): - ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i]);\n' % (pts, i, pts, ml_minus_type(ts), i)) + ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i - 1]);\n' % (pts, i, pts, ml_minus_type(ts), i)) ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%dp' % i)) else: - ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%d[_i]' % i)) + ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%d[_i - 1]' % i)) ml_wrapper.write(' _iter = caml_alloc(2,0);\n') ml_wrapper.write(' Store_field(_iter, 0, tmp_val);\n') ml_wrapper.write(' Store_field(_iter, 1, _a%s_val);\n' % i) From 76bc4f0b38ed9778c0eefdb259cb98a9f5acf905 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Jan 2017 11:30:42 -0800 Subject: [PATCH 2/3] refine parsat Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index bf3dc1988..071c0c2a8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -72,9 +72,9 @@ namespace sat { } void solver::copy(solver const & src) { + pop_to_base_level(); SASSERT(m_mc.empty() && src.m_mc.empty()); SASSERT(scope_lvl() == 0); - SASSERT(src.scope_lvl() == 0); // create new vars if (num_vars() < src.num_vars()) { for (bool_var v = num_vars(); v < src.num_vars(); v++) { @@ -120,6 +120,9 @@ namespace sat { mk_clause_core(buffer); } } + + m_user_scope_literals.reset(); + m_user_scope_literals.append(src.m_user_scope_literals); } // ----------------------- @@ -800,6 +803,9 @@ namespace sat { sat::par par; for (int i = 0; i < num_threads; ++i) { m_params.set_uint("random_seed", i); + if (i < num_threads/2) { + m_params.set_sym("phase", symbol("random")); + } solvers[i] = alloc(sat::solver, m_params, rlims[i], 0); solvers[i]->copy(*this); solvers[i]->set_par(&par); @@ -869,17 +875,18 @@ namespace sat { */ void solver::exchange_par() { if (m_par && scope_lvl() == 0) { + unsigned sz = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; unsigned num_in = 0, num_out = 0; SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD literal_vector in, out; - for (unsigned i = m_par_limit_out; i < m_trail.size(); ++i) { + for (unsigned i = m_par_limit_out; i < sz; ++i) { literal lit = m_trail[i]; if (lit.var() < m_par_num_vars) { ++num_out; out.push_back(lit); } } - m_par_limit_out = m_trail.size(); + m_par_limit_out = sz; m_par->exchange(out, m_par_limit_in, in); for (unsigned i = 0; !inconsistent() && i < in.size(); ++i) { literal lit = in[i]; From 1d1949e39597d30811ddba520f841594bd58df3e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Jan 2017 18:30:06 -0800 Subject: [PATCH 3/3] ensure that parallel threads are only invoked when thread count > 1 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 071c0c2a8..e06ed3971 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -723,7 +723,7 @@ namespace sat { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(scope_lvl() == 0); - if (m_config.m_num_parallel > 0 && !m_par) { + if (m_config.m_num_parallel > 1 && !m_par) { return check_par(num_lits, lits); } #ifdef CLONE_BEFORE_SOLVING @@ -823,7 +823,7 @@ namespace sat { bool first = false; #pragma omp critical (par_solver) { - if (finished_id == UINT_MAX) { + if (finished_id == -1) { finished_id = i; first = true; result = r;