Added feature (?) to SAT core to prefer the Nielsen assumptions during splitting

src/smt/seq/seq_nielsen.h

@@ -501,9 +501,9 @@ namespace seq {
         dep_tracker dep;   // tracks which input constraints contributed
 
         static expr_ref simplify(expr* f, ast_manager& m) {
-            //th_rewriter th(m);
+            th_rewriter th(m);
             expr_ref fml(f, m);
-            //th(fml);
+            th(fml);
             return fml;
         }
 

src/smt/smt_context.cpp

@@ -59,6 +59,7 @@ namespace smt {
         m_qmanager(alloc(quantifier_manager, *this, p, _p)),
         m_model_generator(alloc(model_generator, m)),
         m_relevancy_propagator(mk_relevancy_propagator(*this)),
+        m_privileged_split_idx(0),
         m_user_propagator(nullptr),
         m_random(p.m_random_seed),
         m_flushing(false),
@@ -1912,7 +1913,6 @@ namespace smt {
 
         if (!is_pos) l.neg();
         TRACE(decide, tout << "case split " << l << "\n" << "activity: " << get_activity(var) << "\n";);
-        std::cout << "Deciding " << mk_pp(literal2expr(l), m) << std::endl;
         assign(l, b_justification::mk_axiom(), true);
         return true;
     }
@@ -2970,11 +2970,31 @@ namespace smt {
     }
 
     bool context::has_split_candidate(bool_var& var, bool& is_pos) {
-        if (!m_user_propagator)
+        if (m_user_propagator) {
-            return false;
+            if (!m_user_propagator->get_case_split(var, is_pos))
-        if (!m_user_propagator->get_case_split(var, is_pos))
+                return false;
-            return false;
+            return get_assignment(var) == l_undef;
-        return get_assignment(var) == l_undef;
+        }
+        if (m_privileged_split_idx < m_privileged_splits.size()) {
+            const unsigned prev = m_privileged_split_idx;
+            do {
+                const literal lit = m_privileged_splits[m_privileged_split_idx];
+                m_privileged_split_idx++;
+                if (get_assignment(lit) != l_undef)
+                    continue;
+                push_trail(value_trail(m_privileged_split_idx, prev));
+                var = lit.var();
+                is_pos = !lit.sign();
+                return true;
+            } while (m_privileged_split_idx < m_privileged_splits.size());
+            push_trail(value_trail(m_privileged_split_idx, prev));
+        }
+        return false;
+    }
+
+    void context::privileged_split(literal l) {
+        m_privileged_splits.push_back(l);
+        push_trail(push_back_vector<literal_vector>(m_privileged_splits));
     }
     
     bool context::decide_user_interference(bool_var& var, bool& is_pos) {

src/smt/smt_context.h

@@ -107,6 +107,8 @@ namespace smt {
         scoped_ptr<quantifier_manager>   m_qmanager;
         scoped_ptr<model_generator>      m_model_generator;
         scoped_ptr<relevancy_propagator> m_relevancy_propagator;
+        literal_vector                   m_privileged_splits; // literals that need to be splitted on first
+        unsigned                         m_privileged_split_idx; // where to split
         theory_user_propagator*          m_user_propagator;
         random_gen                  m_random;
         bool                        m_flushing; // (debug support) true when flushing
@@ -1837,6 +1839,8 @@ namespace smt {
         bool watches_fixed(enode* n) const;
 
         bool has_split_candidate(bool_var& var, bool& is_pos);
+
+        void privileged_split(literal l);
         
         bool decide_user_interference(bool_var& var, bool& is_pos);
 

src/smt/theory_nseq.cpp

@@ -866,7 +866,7 @@ namespace smt {
                 // std::cout << "Undef [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
                 // Commit the chosen Nielsen assumption to the SAT core so it
                 // cannot remain permanently undefined in a partial model.
-                ctx.force_phase(lit);
+                ctx.privileged_split(lit);
                 all_sat = false;
                 IF_VERBOSE(2, verbose_stream() << 
                     "nseq final_check: adding nielsen assumption " << c.fml << "\n";);