fixing #2443 #2445 #2447 #2448

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/ast/seq_decl_plugin.h

@@ -40,9 +40,9 @@ enum seq_op_kind {
     OP_SEQ_EXTRACT,
     OP_SEQ_REPLACE,
     OP_SEQ_AT,
-    OP_SEQ_NTH,
-    OP_SEQ_NTH_I,
-    OP_SEQ_NTH_U,
+    OP_SEQ_NTH,         // NTH function exposed over API. Rewritten to NTH(s,i) := if (0 <= i < len(s)) then NTH_I(s,i) else NTH_U(s,i)
+    OP_SEQ_NTH_I,       // Interpreted variant of Nth for indices within defined domain.
+    OP_SEQ_NTH_U,       // Uninterpreted variant of Nth for indices outside of uniquely defined domain.
     OP_SEQ_LENGTH,
     OP_SEQ_INDEX,
     OP_SEQ_LAST_INDEX,

src/smt/theory_seq.cpp

@@ -5529,9 +5529,6 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (m_util.str.is_in_re(e)) {
         propagate_in_re(e, is_true);
     }
-    else if (is_skolem(symbol("seq.split"), e)) {
-        // propagate equalities
-    }
     else if (is_skolem(symbol("seq.is_digit"), e)) {
         // no-op
     }
@@ -5541,7 +5538,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) {
         m_lts.push_back(e);
     }
-    else if (m_util.str.is_nth_i(e)) {
+    else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
         // no-op
     }
     else {