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) diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index 756e9642c..2ce39e6fd 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -26,8 +26,11 @@ namespace sat { m_index(index), m_lit(lit), m_k(k), - m_size(lits.size()), - m_lits(lits) { + m_size(lits.size()) + { + for (unsigned i = 0; i < lits.size(); ++i) { + m_lits[i] = lits[i]; + } } void card_extension::card::negate() { @@ -453,7 +456,7 @@ namespace sat { void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) { unsigned index = m_constraints.size(); - card* c = alloc(card, index, literal(v, false), lits, k); + card* c = new (memory::allocate(__FILE__,__LINE__, "card", card::get_obj_size(lits.size()))) card(index, literal(v, false), lits, k); m_constraints.push_back(c); init_watch(v); m_var_infos[v].m_card = c; @@ -617,6 +620,15 @@ namespace sat { } result->add_at_least(c.lit().var(), lits, c.k()); } + for (unsigned i = 0; i < m_var_trail.size(); ++i) { + bool_var v = m_var_trail[i]; + if (v != null_bool_var) { + card* c = m_var_infos[v].m_card; + card* c2 = m_constraints[c->index()]; + result->m_var_trail.reserve(v + 10); + NOT_IMPLEMENTED_YET(); + } + } return result; } @@ -635,18 +647,15 @@ namespace sat { void card_extension::display(std::ostream& out, card& c, bool values) const { out << c.lit(); - if (c.lit() != null_literal) { - if (values) { - out << "@(" << value(c.lit()); - if (value(c.lit()) != l_undef) { - out << ":" << lvl(c.lit()); - } - out << ")"; + if (c.lit() != null_literal && values) { + out << "@(" << value(c.lit()); + if (value(c.lit()) != l_undef) { + out << ":" << lvl(c.lit()); } - out << c.lit() << "\n"; + out << "): "; } else { - out << " "; + out << ": "; } for (unsigned i = 0; i < c.size(); ++i) { literal l = c[i]; @@ -658,8 +667,11 @@ namespace sat { } out << ") "; } + else { + out << " "; + } } - out << " >= " << c.k() << "\n"; + out << ">= " << c.k() << "\n"; } std::ostream& card_extension::display(std::ostream& out) const { diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index 5c3f1e293..e1ed197d1 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -32,13 +32,17 @@ namespace sat { void reset() { memset(this, 0, sizeof(*this)); } }; + // class card_allocator; class card { + //friend class card_allocator; unsigned m_index; literal m_lit; unsigned m_k; unsigned m_size; - literal_vector m_lits; + literal m_lits[0]; + public: + static size_t get_obj_size(unsigned num_lits) { return sizeof(card) + num_lits * sizeof(literal); } card(unsigned index, literal lit, literal_vector const& lits, unsigned k); unsigned index() const { return m_index; } literal lit() const { return m_lit; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d4349d2c2..ec224e6b8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -73,9 +73,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++) { @@ -128,6 +128,8 @@ namespace sat { if (src.get_extension()) { m_ext = src.get_extension()->copy(this); } + m_user_scope_literals.reset(); + m_user_scope_literals.append(src.m_user_scope_literals); } // ----------------------- @@ -728,7 +730,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 @@ -808,6 +810,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); @@ -825,7 +830,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; @@ -877,17 +882,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];