add "legacy" support for theory case splits

this replicates what was done in theory_str to add axioms excluding each
pair of literals from being assigned True at the same time;
no new heuristics are being used in smt_context (yet)

src/smt/smt_context.cpp

@@ -2939,6 +2939,27 @@ namespace smt {
         assert_expr_core(e, pr);
     }
 
+    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 {
+            NOT_IMPLEMENTED_YET();
+        }
+    }
+
     bool context::reduce_assertions() {
         if (!m_asserted_formulas.inconsistent()) {
             SASSERT(at_base_level());

src/smt/smt_context.h

@@ -805,6 +805,14 @@ 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);
 
         bool_var mk_bool_var(expr * n);
         

src/smt/theory_str.cpp

@@ -2466,8 +2466,19 @@ void theory_str::infer_len_concat_equality(expr * nn1, expr * nn2) {
     */
 }
 
-expr_ref theory_str::generate_mutual_exclusion(expr_ref_vector & terms) {
+void theory_str::generate_mutual_exclusion(expr_ref_vector & terms) {
     context & ctx = get_context();
+    // pull each literal out of the arrangement disjunction
+    literal_vector ls;
+    for (unsigned i = 0; i < terms.size(); ++i) {
+        expr * e = terms.get(i);
+        literal l = ctx.get_literal(e);
+        ls.push_back(l);
+    }
+    ctx.mk_th_case_split(ls.size(), ls.c_ptr());
+
+    // old version, without special support in the context
+    /*
     ast_manager & m = get_manager();
 
     expr_ref_vector result(m);
@@ -2482,7 +2493,8 @@ expr_ref theory_str::generate_mutual_exclusion(expr_ref_vector & terms) {
     }
 
     expr_ref final_result(mk_and(result), m);
-    return final_result;
+    assert_axiom(final_result);
+    */
 }
 
 void theory_str::print_cut_var(expr * node, std::ofstream & xout) {
@@ -3114,7 +3126,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
                 assert_implication(premise, conclusion);
             }
             // assert mutual exclusion between each branch of the arrangement
-            assert_axiom(generate_mutual_exclusion(arrangement_disjunction));
+            generate_mutual_exclusion(arrangement_disjunction);
         } else {
             TRACE("t_str", tout << "STOP: no split option found for two EQ concats." << std::endl;);
         }
@@ -3447,7 +3459,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
 			} else {
 			    assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
 			}
-			assert_axiom(generate_mutual_exclusion(arrangement_disjunction));
+			generate_mutual_exclusion(arrangement_disjunction);
 		} else {
 			TRACE("t_str", tout << "STOP: Should not split two EQ concats." << std::endl;);
 		}
@@ -3774,7 +3786,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
             } else {
                 assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
             }
-            assert_axiom(generate_mutual_exclusion(arrangement_disjunction));
+            generate_mutual_exclusion(arrangement_disjunction);
         } else {
             TRACE("t_str", tout << "STOP: should not split two eq. concats" << std::endl;);
         }
@@ -4198,7 +4210,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
     } else {
         assert_implication(ctx.mk_eq_atom(concatAst1, concatAst2), implyR);
     }
-    assert_axiom(generate_mutual_exclusion(arrangement_disjunction));
+    generate_mutual_exclusion(arrangement_disjunction);
 }
 
 void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) {
@@ -6308,7 +6320,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
         			    } else {
         			        assert_implication(implyL, implyR1);
         			    }
-        			    assert_axiom(generate_mutual_exclusion(arrangement_disjunction));
+        			    generate_mutual_exclusion(arrangement_disjunction);
         			}
         		} /* (arg1Len != 1 || arg2Len != 1) */
         	} /* if (Concat(arg1, arg2) == NULL) */

src/smt/theory_str.h

@@ -441,7 +441,7 @@ namespace smt {
 
         void print_cut_var(expr * node, std::ofstream & xout);
 
-        expr_ref generate_mutual_exclusion(expr_ref_vector & exprs);
+        void generate_mutual_exclusion(expr_ref_vector & exprs);
 
         bool new_eq_check(expr * lhs, expr * rhs);
         void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);