Merge pull request #995 from mtrberzi/theory-case-split

Theory case split heuristic (for theory_str)

src/smt/params/smt_params.cpp

@@ -31,6 +31,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
     m_restart_factor = p.restart_factor();
     m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
+    m_theory_case_split = p.theory_case_split();
     m_delay_units = p.delay_units();
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
@@ -155,4 +156,4 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_check_at_labels);
     DISPLAY_PARAM(m_dump_goal_as_smt);
     DISPLAY_PARAM(m_auto_config);
-}
+}

src/smt/params/smt_params.h

@@ -109,6 +109,7 @@ struct smt_params : public preprocessor_params,
     case_split_strategy m_case_split_strategy;
     unsigned            m_rel_case_split_order;
     bool                m_lookahead_diseq;
+    bool                m_theory_case_split;
 
     // -----------------------------------
     //

src/smt/params/smt_params_helper.pyg

@@ -61,6 +61,7 @@ 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.'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
                           ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
                           ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),

src/smt/smt_context.cpp

@@ -74,6 +74,7 @@ namespace smt {
         m_unsat_proof(m),
         m_unknown("unknown"),
         m_unsat_core(m),
+        m_th_case_split_qhead(0),
 #ifdef Z3DEBUG
         m_trail_enabled(true),
 #endif
@@ -339,6 +340,7 @@ namespace smt {
     
     bool context::bcp() {
         SASSERT(!inconsistent());
+        m_th_case_split_qhead = m_qhead;
         while (m_qhead < m_assigned_literals.size()) {
             if (get_cancel_flag()) {
                 return true;
@@ -1768,6 +1770,8 @@ namespace smt {
             unsigned qhead = m_qhead;
             if (!bcp())
                 return false;
+            if (!propagate_th_case_split())
+                return false;
             if (get_cancel_flag()) {
                 m_qhead = qhead;
                 return true;
@@ -2960,6 +2964,114 @@ namespace smt {
         assert_expr_core(e, pr);
     }
 
+    class case_split_insert_trail : public trail<context> {
+        literal l;
+    public:
+        case_split_insert_trail(literal l):
+            l(l) {
+        }
+        virtual void undo(context & ctx) {
+            ctx.undo_th_case_split(l);
+        }
+    };
+
+    void context::mk_th_case_split(unsigned num_lits, literal * lits) {
+        TRACE("theory_case_split", display_literals_verbose(tout << "theory case split: ", num_lits, lits); tout << std::endl;);
+        // If we don't use the theory case split heuristic,
+        // for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2)
+        // to enforce the condition that more than one literal can't be
+        // assigned 'true' simultaneously.
+        if (!m_fparams.m_theory_case_split) {
+            for (unsigned i = 0; i < num_lits; ++i) {
+                for (unsigned j = i+1; j < num_lits; ++j) {
+                    literal l1 = lits[i];
+                    literal l2 = lits[j];
+                    literal excl[2] = {~l1, ~l2};
+                    justification * j_excl = 0;
+                    mk_clause(2, excl, j_excl);
+                }
+            }
+        } else {
+            literal_vector new_case_split;
+            for (unsigned i = 0; i < num_lits; ++i) {
+                literal l = lits[i];
+                SASSERT(!m_all_th_case_split_literals.contains(l.index()));
+                m_all_th_case_split_literals.insert(l.index());
+                push_trail(case_split_insert_trail(l));
+                new_case_split.push_back(l);
+            }
+            m_th_case_split_sets.push_back(new_case_split);
+            push_trail(push_back_vector<context, vector<literal_vector> >(m_th_case_split_sets));
+            for (unsigned i = 0; i < num_lits; ++i) {
+                literal l = lits[i];
+                if (!m_literal2casesplitsets.contains(l.index())) {
+                    m_literal2casesplitsets.insert(l.index(), vector<literal_vector>());
+                }
+                m_literal2casesplitsets[l.index()].push_back(new_case_split);
+            }
+            TRACE("theory_case_split", tout << "tracking case split literal set { ";
+            for (unsigned i = 0; i < num_lits; ++i) {
+                tout << lits[i].index() << " ";
+            }
+            tout << "}" << std::endl;
+            );
+        }
+    }
+
+    void context::undo_th_case_split(literal l) {
+        m_all_th_case_split_literals.remove(l.index());
+        if (m_literal2casesplitsets.contains(l.index())) {
+            if (!m_literal2casesplitsets[l.index()].empty()) {
+                m_literal2casesplitsets[l.index()].pop_back();
+            }
+        }
+    }
+
+    bool context::propagate_th_case_split() {
+        if (m_all_th_case_split_literals.empty())
+            return true;
+
+        // iterate over all literals assigned since the last time this method was called,
+        // not counting any literals that get assigned by this method
+        // this relies on bcp() to give us its old m_qhead and therefore
+        // bcp() should always be called before this method
+        unsigned assigned_literal_idx = m_th_case_split_qhead;
+        unsigned assigned_literal_end = m_assigned_literals.size();
+        while(assigned_literal_idx < assigned_literal_end) {
+            literal l = m_assigned_literals[assigned_literal_idx];
+            TRACE("theory_case_split", tout << "check literal " << l.index() << std::endl; display_literal_verbose(tout, l); tout << std::endl;);
+            ++assigned_literal_idx;
+            // check if this literal participates in any theory case split
+            if (m_all_th_case_split_literals.contains(l.index())) {
+                TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
+                // now find the sets of literals which contain l
+                vector<literal_vector> & case_split_sets = m_literal2casesplitsets.get(l.index(), vector<literal_vector>());
+                for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) {
+                    literal_vector case_split_set = *it;
+                    TRACE("theory_case_split", tout << "found case split set { ";
+                    for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
+                        tout << set_it->index() << " ";
+                    }
+                    tout << "}" << std::endl;);
+                    for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
+                        literal l2 = *set_it;
+                        if (l2 != l) {
+                            b_justification js(l);
+                            TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr()););
+                            assign(~l2, js);
+                            if (inconsistent()) {
+                                TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);
+                                return false;
+                            }
+                        }
+                    }
+                }
+            }
+        }
+        // if we get here without detecting a conflict, we're fine
+        return true;
+    }
+
     bool context::reduce_assertions() {
         if (!m_asserted_formulas.inconsistent()) {
             SASSERT(at_base_level());

src/smt/smt_context.h

@@ -226,6 +226,16 @@ namespace smt {
         literal2assumption         m_literal2assumption; // maps an expression associated with a literal to the original assumption
         expr_ref_vector            m_unsat_core;
 
+        // -----------------------------------
+        //
+        // Theory case split
+        //
+        // -----------------------------------
+        uint_set m_all_th_case_split_literals;
+        vector<literal_vector> m_th_case_split_sets;
+        u_map< vector<literal_vector> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in
+        unsigned m_th_case_split_qhead;
+
         // -----------------------------------
         //
         // Accessors
@@ -820,6 +830,21 @@ namespace smt {
 
         void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = 0);
 
+        /*
+         * Provide a hint to the core solver that the specified literals form a "theory case split".
+         * The core solver will enforce the condition that exactly one of these literals can be
+         * assigned 'true' at any time.
+         * We assume that the theory solver has already asserted the disjunction of these literals
+         * or some other axiom that means at least one of them must be assigned 'true'.
+         */
+        void mk_th_case_split(unsigned num_lits, literal * lits);
+
+    public:
+
+        // helper function for trail
+        void undo_th_case_split(literal l);
+
+	bool propagate_th_case_split();
 
         bool_var mk_bool_var(expr * n);