From 2d5714a5d4b854ea2bcb48f7749954a7a356f985 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Aug 2019 01:21:09 +0800 Subject: [PATCH] fixing #2443 #2445 #2447 #2448 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.h | 6 +++--- src/smt/theory_seq.cpp | 5 +---- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 38db9c078..471ed0229 100644 --- a/src/ast/seq_decl_plugin.h +++ b/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, diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index cf4fd9ebf..b49987222 100644 --- a/src/smt/theory_seq.cpp +++ b/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 {