testing card_extension

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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)

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_size(lits.size())
-        m_lits(lits) {
+    {
+        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 (c.lit() != null_literal && values) {
-            if (values) {
             out << "@(" << value(c.lit());
             if (value(c.lit()) != l_undef) {
                 out << ":" << lvl(c.lit());
             }
-                out << ")";
+            out << "): ";
-            }
-            out << c.lit() << "\n";
         }
         else {
-            out << " ";
+            out << ": ";
         }
         for (unsigned i = 0; i < c.size(); ++i) {
             literal l = c[i];
@@ -658,6 +667,9 @@ namespace sat {
                 }
                 out << ") ";
             }
+            else {
+                out << " ";
+            }
         }
         out << ">= " << c.k()  << "\n";
     }

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; }

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];