From 1796fc32f5cd0c38c1399bac759e993b2e0cb852 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Mar 2020 10:16:48 -0700
Subject: [PATCH] breaking change to fix #3062 #3147 #2896 #2937 #3105

This moves handling of contains into an axiomatization that unfolds on demand.
The previous handling, based on rewriting, proved too brittle. While it simplifies how contains is handled, it is likely to introduce regressions in terms of what constraints can now be handled.
---
 src/smt/theory_seq.cpp | 66 ++++++++++++++++++++++++++++++++++--------
 1 file changed, 54 insertions(+), 12 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 94270ddb8..8fee8fe3c 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -25,6 +25,7 @@ Outline:
    - solve_itos: itos(i) = "" -> i < 0   
 
  - check_contains
+   Original
    - (f,dep) = canonize(contains(a, b))
      lit := |b| > |a|
      f := true -> conflict
@@ -33,6 +34,14 @@ Outline:
      f := s = t -> dep -> s != t
      f := f1 & f2 -> dep -> ~f1 | ~f2
      f := f1 | f2 -> dep -> ~f1 & ~f2
+   Revised:
+   - contains(a,b) or len(a) < len(b)
+   - contains(a,b) or ~prefix(b, a) 
+   - contains(a,b) or ~contains(tail(a,0), b)
+   - a = empty or a = unit(nth_i(a,0)) + tail(a,0)
+   Note that
+     len(a) < len(b) implies ~prefix(b, a) and ~contains(tail(a,0),b)
+     So the recursive axioms are not instantiated in this case.
 
  - solve_nqs
    - s_i = t_i, d_i <- solve(s = t)
@@ -3456,12 +3465,45 @@ bool theory_seq::solve_nc(unsigned idx) {
     literal len_gt = n.len_gt();
     context& ctx = get_context();
     expr_ref c(m);
+#if 1
+    expr* a = nullptr, *b = nullptr;
+    VERIFY(m_util.str.is_contains(n.contains(), a, b));
+    expr_ref head(m), tail(m);
+    literal pre, cnt, ctail, emp;
+    lbool is_gt = ctx.get_assignment(len_gt);
+    TRACE("seq", ctx.display_literal_smt2(tout << len_gt << " := " << is_gt << "\n", len_gt) << "\n";);    
+    switch (is_gt) {
+    case l_true:
+        add_length_to_eqc(a);
+        add_length_to_eqc(b);
+        return true;
+    case l_undef:
+        ctx.mark_as_relevant(len_gt);
+        m_new_propagation = true;
+        return false;
+    case l_false: {
+        mk_decompose(a, head, tail);
+        pre = mk_literal(m_util.str.mk_prefix(b, a));
+        cnt = mk_literal(n.contains());
+        ctail = mk_literal(m_util.str.mk_contains(tail, b));
+        emp = mk_literal(m_util.str.mk_is_empty(a));
+        //expr_ref one(m_autil.mk_int(1), m);
+        add_axiom(cnt, ~pre);
+        add_axiom(cnt, ~ctail);
+        add_axiom(emp, mk_eq(a, m_util.str.mk_concat(head, tail), false));
+        return true;
+    }
+    }
+    
+#else
     if (!canonize(n.contains(), deps, c)) {
         return false;
     }
     expr* a = nullptr, *b = nullptr;
 
-    CTRACE("seq", c != n.contains(), tout << n.contains() << " =>\n" << c << "\n";);    
+    CTRACE("seq", c != n.contains(), 
+           tout << n.contains() << " =>\n" << c << "\n";
+           display_deps(tout, deps););    
 
     
     if (m.is_true(c)) {
@@ -3474,16 +3516,10 @@ bool theory_seq::solve_nc(unsigned idx) {
         return true;
     }
 
-    if (ctx.get_assignment(len_gt) == l_true) {
-        VERIFY(m_util.str.is_contains(n.contains(), a, b));
-        add_length_to_eqc(a);
-        add_length_to_eqc(b);
-        TRACE("seq", tout << len_gt << " is true\n";);
-        return true;
-    }
 
     if (m.is_eq(c, a, b)) {
         literal eq = mk_eq(a, b, false);
+        ctx.mark_as_relevant(eq);
         propagate_lit(deps, 0, nullptr, ~eq);        
         return true;
     }
@@ -3539,7 +3575,7 @@ bool theory_seq::solve_nc(unsigned idx) {
         m_new_propagation = true;
         return true;
     }
-    
+#endif    
     return false;
 }
 
@@ -4729,7 +4765,7 @@ bool theory_seq::expand1(expr* e0, dependency*& eqs, expr_ref& result) {
     else if (m_util.str.is_contains(e, e1, e2)) {
         arg1 = try_expand(e1, deps);
         arg2 = try_expand(e2, deps);
-        if (!arg1 || !arg2) return true;
+        if (!arg1 || !arg2) return true;        
         result = m_util.str.mk_contains(arg1, arg2);
     }
     else if (m_util.str.is_unit(e, e1)) {
@@ -5996,6 +6032,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     literal lit(v, !is_true);
     TRACE("seq", tout << (is_true?"":"not ") << mk_bounded_pp(e, m) << "\n";);
 
+
     if (m_util.str.is_prefix(e, e1, e2)) {
         if (is_true) {
             f = mk_skolem(m_prefix, e1, e2);
@@ -6017,7 +6054,11 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
         }
     }
     else if (m_util.str.is_contains(e, e1, e2)) {
-        expr_ref_vector disj(m);
+        // TBD: move this to cover all cases
+        if (canonizes(is_true, e)) {
+            return;
+        }        
+
         if (is_true) {
             expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
             expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
@@ -6026,9 +6067,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             //literal len2_le_len1 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(0)));
             //add_axiom(~lit, len2_le_len1);
         }
-        else if (!canonizes(false, e)) {
+        else {
             propagate_non_empty(lit, e2);
             dependency* dep = m_dm.mk_leaf(assumption(lit));
+            // |e1| - |e2| <= -1
             literal len_gt = mk_simplified_literal(m_autil.mk_le(mk_sub(mk_len(e1), mk_len(e2)), 
                                                                  m_autil.mk_int(-1)));
             ctx.force_phase(len_gt);