Merge branch 'upstream-master' into develop

Conflicts:
	src/smt/params/smt_params.h
	src/smt/params/smt_params_helper.pyg
	src/smt/smt_case_split_queue.cpp
	src/smt/smt_context.h
	src/smt/smt_setup.cpp
	src/smt/smt_setup.h

src/opt/wmax.cpp

@@ -61,13 +61,12 @@ namespace opt {
                 return is_sat;
             }
             m_upper = m_lower;
-            bool was_sat = false;
             expr_ref_vector asms(m);
             vector<expr_ref_vector> cores;
 
             obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
             for (; it != end; ++it) {
-                expr* c = assert_weighted(wth(), it->m_key, it->m_value);
+                assert_weighted(wth(), it->m_key, it->m_value);
                 if (!is_true(it->m_key)) {
                     m_upper += it->m_value;
                 }
@@ -97,7 +96,6 @@ namespace opt {
                     expr_ref fml = wth().mk_block();
                     //DEBUG_CODE(verify_cores(cores););
                     s().assert_expr(fml);
-                    was_sat = true;
                 }
                 else {
                     //DEBUG_CODE(verify_cores(cores););

src/sat/sat_solver.cpp

@@ -3141,42 +3141,42 @@ namespace sat {
     //
     // -----------------------
 
-static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
+    static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
-    for (unsigned i = 0; i < lambda.size(); ++i) {
+        for (unsigned i = 0; i < lambda.size(); ++i) {
-        if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
+            if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
-            lambda[i] = lambda.back();
+                lambda[i] = lambda.back();
-            lambda.pop_back();
+                lambda.pop_back();
+                --i;
+            }
+        }
+    }
+    
+    // Algorithm 7: Corebased Algorithm with Chunking
+    
+    static void back_remove(sat::literal_vector& lits, sat::literal l) {
+        for (unsigned i = lits.size(); i > 0; ) {
             --i;
+            if (lits[i] == l) {
+                lits[i] = lits.back();
+                lits.pop_back();
+                return;
+            }
         }
+        UNREACHABLE();
     }
-}
-
-// Algorithm 7: Corebased Algorithm with Chunking
-
-static void back_remove(sat::literal_vector& lits, sat::literal l) {
-    for (unsigned i = lits.size(); i > 0; ) {
-        --i;
-        if (lits[i] == l) {
-            lits[i] = lits.back();
-            lits.pop_back();
-            return;
-        }
-    }
-    std::cout << "UNREACHABLE\n";
-}
 
     static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector<sat::literal_vector>& conseq) {
-    for (unsigned i = 0; i < gamma.size(); ++i) {
+        for (unsigned i = 0; i < gamma.size(); ++i) {
-        sat::literal nlit = ~gamma[i];
+            sat::literal nlit = ~gamma[i];
-        sat::literal_vector asms1(asms);
+            sat::literal_vector asms1(asms);
-        asms1.push_back(nlit);
+            asms1.push_back(nlit);
-        lbool r = s.check(asms1.size(), asms1.c_ptr());
+            lbool r = s.check(asms1.size(), asms1.c_ptr());
-        if (r == l_false) {
+            if (r == l_false) {
-            conseq.push_back(s.get_core());
+                conseq.push_back(s.get_core());
+            }
         }
     }
-}
+    
-
     static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
         sat::literal_vector lambda;
         for (unsigned i = 0; i < vars.size(); i++) {
@@ -3259,9 +3259,12 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
             }
         }
 
-        // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
+        if (false && asms.empty()) {
-
+            is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
-        is_sat = get_consequences(asms, lits, conseq);
+        }
+        else {
+            is_sat = get_consequences(asms, lits, conseq);
+        }
         set_model(mdl);
         return is_sat;
     }
@@ -3390,8 +3393,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
                 literal lit = *it;                
                 if (value(lit) != l_undef) {
                     ++num_fixed;
-                    if (lvl(lit) <= 1) {
+                    if (lvl(lit) <= 1 && value(lit) == l_true) {
-                        SASSERT(value(lit) == l_true);
                         extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
                     }
                     continue;
@@ -3498,8 +3500,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
         literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
         for (; it != end; ++it) {
             literal lit = *it;
-            if (lvl(lit) <= 1) {
+            TRACE("sat", tout << "extract: " << lit << " " << value(lit) << " " << lvl(lit) << "\n";);
-                SASSERT(value(lit) == l_true);
+
+            if (lvl(lit) <= 1 && value(lit) == l_true) {
                 extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
             }
         }
@@ -3508,8 +3511,8 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
     bool solver::check_domain(literal lit, literal lit2) {
         if (!m_antecedents.contains(lit2.var())) {
             SASSERT(value(lit2) == l_true);
+            SASSERT(m_todo_antecedents.empty() || m_todo_antecedents.back() != lit2);
             m_todo_antecedents.push_back(lit2);
-            TRACE("sat", tout << "todo: " << lit2 << " " << value(lit2) << "\n";);
             return false;
         }
         else {
@@ -3520,6 +3523,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
     bool solver::extract_assumptions(literal lit, index_set& s) {
         justification js = m_justification[lit.var()];
         TRACE("sat", tout << lit << " " << js << "\n";);
+        bool all_found = true;
         switch (js.get_kind()) {
         case justification::NONE:
             break;
@@ -3537,8 +3541,12 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
             clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
             for (unsigned i = 0; i < c.size(); ++i) {
                 if (c[i] != lit) {
-                    if (!check_domain(lit, ~c[i])) return false;
+                    if (check_domain(lit, ~c[i]) && all_found) {
-                    s |= m_antecedents.find(c[i].var());
+                        s |= m_antecedents.find(c[i].var());
+                    }
+                    else {
+                        all_found = false;
+                    }
                 }
             }
             break;
@@ -3548,8 +3556,12 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
             literal_vector::iterator it  = m_ext_antecedents.begin();
             literal_vector::iterator end = m_ext_antecedents.end();
             for (; it != end; ++it) {
-                if (!check_domain(lit, *it)) return false;
+                if (check_domain(lit, *it) && all_found) {
-                s |= m_antecedents.find(it->var());
+                    s |= m_antecedents.find(it->var());
+                }
+                else {
+                    all_found = false;
+                }
             }
             break;
         }
@@ -3558,7 +3570,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
             break;
         }
         TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";);
-        return true;
+        return all_found;
     }
 
     std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const {

src/smt/params/smt_params.h

@@ -67,7 +67,8 @@ enum case_split_strategy {
     CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
     CS_RELEVANCY, // case split based on relevancy
     CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
-    CS_RELEVANCY_GOAL // based on relevancy and the current goal
+    CS_RELEVANCY_GOAL, // based on relevancy and the current goal
+    CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
 };
 
 struct smt_params : public preprocessor_params, 

src/smt/params/smt_params_helper.pyg

@@ -11,7 +11,7 @@ def_module_params(module_name='smt',
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
                           ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
-                          ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
+                          ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
@@ -61,8 +61,9 @@ def_module_params(module_name='smt',
                           ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
+                          ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
+                          ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
-                          ('string_solver', SYMBOL, 'auto', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'),
                           ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
                           ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
                           ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'),
@@ -72,7 +73,6 @@ def_module_params(module_name='smt',
                           ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
                           ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
                           ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
-                          ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
                           ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
                           ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),
                           ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'),

src/smt/smt_case_split_queue.cpp

@@ -1164,9 +1164,10 @@ namespace smt {
         virtual void pop_scope(unsigned num_scopes) {}
 
         virtual void next_case_split(bool_var & next, lbool & phase) {
-            phase = l_undef;
+            int threshold = static_cast<int>(m_params.m_random_var_freq * random_gen::max_value());
-
+            SASSERT(threshold >= 0);
-            if (m_context.get_random_value() < static_cast<int>(m_params.m_random_var_freq * random_gen::max_value())) {
+            if (m_context.get_random_value() < threshold) {
+                SASSERT(m_context.get_num_b_internalized() > 0);
                 next = m_context.get_random_value() % m_context.get_num_b_internalized(); 
                 TRACE("random_split", tout << "next: " << next << " get_assignment(next): " << m_context.get_assignment(next) << "\n";);
                 if (m_context.get_assignment(next) == l_undef)
@@ -1237,25 +1238,21 @@ namespace smt {
             warning_msg("auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5");
             p.m_case_split_strategy = CS_ACTIVITY;
         }
-
+        switch (p.m_case_split_strategy) {
-        if (p.m_theory_aware_branching) {
+        case CS_ACTIVITY_DELAY_NEW:
-            // override
+            return alloc(dact_case_split_queue, ctx, p);
+        case CS_ACTIVITY_WITH_CACHE:
+            return alloc(cact_case_split_queue, ctx, p);
+        case CS_RELEVANCY:
+            return alloc(rel_case_split_queue, ctx, p);
+        case CS_RELEVANCY_ACTIVITY:
+            return alloc(rel_act_case_split_queue, ctx, p);
+        case CS_RELEVANCY_GOAL:
+            return alloc(rel_goal_case_split_queue, ctx, p);
+        case CS_ACTIVITY_THEORY_AWARE_BRANCHING:
             return alloc(theory_aware_branching_queue, ctx, p);
-        } else {
+        default:
-            switch (p.m_case_split_strategy) {
+            return alloc(act_case_split_queue, ctx, p);
-            case CS_ACTIVITY_DELAY_NEW:
-                return alloc(dact_case_split_queue, ctx, p);
-            case CS_ACTIVITY_WITH_CACHE:
-                return alloc(cact_case_split_queue, ctx, p);
-            case CS_RELEVANCY:
-                return alloc(rel_case_split_queue, ctx, p);
-            case CS_RELEVANCY_ACTIVITY:
-                return alloc(rel_act_case_split_queue, ctx, p);
-            case CS_RELEVANCY_GOAL:
-                return alloc(rel_goal_case_split_queue, ctx, p);
-            default:
-                return alloc(act_case_split_queue, ctx, p);
-            }
         }
     }
 

src/smt/smt_context.h

@@ -838,6 +838,7 @@ namespace smt {
          */
         void mk_th_case_split(unsigned num_lits, literal * lits);
 
+
         /*
          * Provide a hint to the branching heuristic about the priority of a "theory-aware literal".
          * Literals marked in this way will always be branched on before unmarked literals,

src/smt/smt_setup.cpp

@@ -824,19 +824,23 @@ namespace smt {
         m_context.register_plugin(mk_theory_dl(m_manager));
     }
 
-    void setup::setup_seq(static_features const & st) {
+    void setup::setup_seq_str(static_features const & st) {
         // check params for what to do here when it's ambiguous
         if (m_params.m_string_solver == "z3str3") {
             setup_str();
-        } else if (m_params.m_string_solver == "seq") {
+        } 
-            m_context.register_plugin(alloc(theory_seq, m_manager));
+        else if (m_params.m_string_solver == "seq") {
-        } else if (m_params.m_string_solver == "auto") {
+            setup_seq();
+        } 
+        else if (m_params.m_string_solver == "auto") {
             if (st.m_has_seq_non_str) {
-                m_context.register_plugin(alloc(theory_seq, m_manager));
+                setup_seq();
-            } else {
+            } 
+            else {
                 setup_str();
             }
-        } else {
+        } 
+        else {
             throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
         }
     }
@@ -855,6 +859,10 @@ namespace smt {
         m_context.register_plugin(alloc(theory_str, m_manager, m_params));
     }
 
+    void setup::setup_seq() {
+        m_context.register_plugin(alloc(smt::theory_seq, m_manager));
+    }
+
     void setup::setup_unknown() {
         static_features st(m_manager);
         st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
@@ -864,7 +872,7 @@ namespace smt {
         setup_bv();
         setup_datatypes();
         setup_dl();
-        setup_seq(st);
+        setup_seq_str(st);
         setup_card();
         setup_fpa();
     }
@@ -879,7 +887,7 @@ namespace smt {
             setup_datatypes();
             setup_bv();
             setup_dl();
-            setup_seq(st);
+            setup_seq_str(st);
             setup_card();
             setup_fpa();
             return;

src/smt/smt_setup.h

@@ -94,7 +94,8 @@ namespace smt {
         void setup_bv();
         void setup_arith();
         void setup_dl();
-        void setup_seq(static_features const & st);
+        void setup_seq_str(static_features const & st);
+        void setup_seq();
         void setup_card();
         void setup_i_arith();
         void setup_mi_arith();

src/test/cnf_backbones.cpp

@@ -246,13 +246,15 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
     vector<sat::literal_vector> conseq;
     sat::bool_var_vector vars;
     sat::literal_vector assumptions;
+    unsigned num_vars = solver.num_vars();
     if (p.get_bool("dimacs.core", false)) {
         g_solver = &solver2;        
         vector<sat::literal_vector> tracking_clauses;
         track_clauses(solver, solver2, assumptions, tracking_clauses);
     }
-
+    // remove this line to limit variables to exclude assumptions
-    for (unsigned i = 1; i < g_solver->num_vars(); ++i) {
+    num_vars = g_solver->num_vars();
+    for (unsigned i = 1; i < num_vars; ++i) {
         vars.push_back(i);        
         g_solver->set_external(i);
     }