From f9d7981c1eb81aa7121c0ae5f637ca712864847a Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 3 Jan 2017 15:45:04 -0500
Subject: [PATCH] add theory case split to theory_str binary search

---
 src/smt/theory_str.cpp | 22 ++++++++++++++++++----
 src/smt/theory_str.h   |  3 ++-
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index d3d680717..278f692f8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -2507,6 +2507,7 @@ void theory_str::generate_mutual_exclusion(expr_ref_vector & terms) {
     literal_vector ls;
     for (unsigned i = 0; i < terms.size(); ++i) {
         expr * e = terms.get(i);
+        // TODO make sure the terms are internalized, etc.?
         literal l = ctx.get_literal(e);
         ls.push_back(l);
     }
@@ -9199,7 +9200,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
 // Return an expression of the form
 // (tester = "less" | tester = "N" | tester = "more") &
 //   (tester = "less" iff len(freeVar) < N) & (tester = "more" iff len(freeVar) > N) & (tester = "N" iff len(freeVar) = N))
-expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds) {
+expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split) {
     context & ctx = get_context();
     ast_manager & m = get_manager();
     rational N = bounds.midPoint;
@@ -9227,6 +9228,16 @@ expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, bin
 
     combinedCaseSplit.push_back(mk_or(testerCases));
 
+    // force internalization on all terms in testerCases so we can extract literals
+    for (unsigned i = 0; i < testerCases.size(); ++i) {
+        expr * testerCase = testerCases.get(i);
+        if (!ctx.b_internalized(testerCase)) {
+            ctx.internalize(testerCase, false);
+        }
+        literal l = ctx.get_literal(testerCase);
+        case_split.push_back(l);
+    }
+
     expr_ref final_term(mk_and(combinedCaseSplit), m);
     SASSERT(final_term);
     TRACE("t_str_binary_search", tout << "final term: " << mk_pp(final_term, m) << std::endl;);
@@ -9339,9 +9350,10 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT
             binary_search_len_tester_info.insert(newTester, newBounds);
             m_trail_stack.push(insert_obj_map<theory_str, expr, binary_search_info>(binary_search_len_tester_info, newTester));
 
-            expr_ref next_case_split(binary_search_case_split(freeVar, newTester, newBounds));
+            literal_vector case_split_literals;
+            expr_ref next_case_split(binary_search_case_split(freeVar, newTester, newBounds, case_split_literals));
             m_trail.push_back(next_case_split);
-            // TODO assert a precondition about all previous length testers that got us here
+            ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr());
             return next_case_split;
         } else { // lastTesterConstant is a concrete value
             TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;);
@@ -9384,8 +9396,10 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT
         binary_search_len_tester_info.insert(firstTester, new_info);
         m_trail_stack.push(insert_obj_map<theory_str, expr, binary_search_info>(binary_search_len_tester_info, firstTester));
 
-        expr_ref initial_case_split(binary_search_case_split(freeVar, firstTester, new_info));
+        literal_vector case_split_literals;
+        expr_ref initial_case_split(binary_search_case_split(freeVar, firstTester, new_info, case_split_literals));
         m_trail.push_back(initial_case_split);
+        ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr());
         return initial_case_split;
     }
 }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 4ac054c52..fdd1a9c84 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -84,6 +84,7 @@ namespace smt {
             target(target), entry(entry) {}
         virtual ~binary_search_trail() {}
         virtual void undo(Ctx & ctx) {
+            TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
             if (target.contains(entry)) {
                 if (!target[entry].empty()) {
                     target[entry].pop_back();
@@ -533,7 +534,7 @@ namespace smt {
 
         // binary search heuristic
         expr * binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue);
-        expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds);
+        expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split_lits);
 
         bool free_var_attempt(expr * nn1, expr * nn2);
         void more_len_tests(expr * lenTester, std::string lenTesterValue);