From a04bc9974b2d2847505a37f3e9e640a082f4ed84 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 20 Dec 2016 11:14:42 -0500
Subject: [PATCH] theory case split WIP

---
 src/smt/smt_context.cpp | 26 +++++++++++++++++++++++++-
 src/smt/smt_context.h   | 12 ++++++++++++
 2 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 907ea876b..45beebc15 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1750,6 +1750,8 @@ namespace smt {
             if (inconsistent())
                 return false;
             unsigned qhead = m_qhead;
+            if (!propagate_th_case_split())
+                return false;
             if (!bcp())
                 return false;
             if (get_cancel_flag()) 
@@ -2956,10 +2958,32 @@ namespace smt {
                 }
             }
         } else {
-            NOT_IMPLEMENTED_YET();
+            int_set new_case_split; // TODO is it okay to allocate this on the stack?
+            for (unsigned i = 0; i < num_lits; ++i) {
+                literal l = lits[i];
+                // TODO do we need to enforce this invariant? can we make undo information work without it?
+                SASSERT(!m_all_th_case_split_literals.contains(l.index()));
+                m_all_th_case_split_literals.insert(l.index());
+                // TODO add undo information for this insert
+                new_case_split.insert(l.index());
+            }
+            m_th_case_split_sets.push_back(new_case_split);
+            push_trail(push_back_vector<context, vector<int_set> >(m_th_case_split_sets));
+            for (unsigned i = 0; i < num_lits; ++i) {
+                literal l = lits[i];
+                m_literal2casesplitsets[l.index()].push_back(new_case_split);
+                push_trail(push_back_vector<context, vector<int_set> >(m_literal2casesplitsets[l.index()]));
+            }
         }
     }
 
+    bool context::propagate_th_case_split() {
+        if (m_all_th_case_split_literals.empty())
+            return true;
+
+        NOT_IMPLEMENTED_YET(); return true;
+    }
+
     bool context::reduce_assertions() {
         if (!m_asserted_formulas.inconsistent()) {
             SASSERT(at_base_level());
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 5c52adc73..cdc52dc67 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -212,6 +212,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
+        //
+        // -----------------------------------
+        typedef int_hashtable<int_hash, default_eq<int> > int_set;
+        int_set m_all_th_case_split_literals;
+        vector<int_set> m_th_case_split_sets;
+        u_map< vector<int_set> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in
+
         // -----------------------------------
         //
         // Accessors
@@ -814,6 +824,8 @@ namespace smt {
          */
         void mk_th_case_split(unsigned num_lits, literal * lits);
 
+        bool propagate_th_case_split();
+
         bool_var mk_bool_var(expr * n);
         
         enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled);