diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 87684893687..da2584db743 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -813,12 +813,17 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re s = true; } - // (ite c (ite c t1 t2) t3) ==> (ite c t1 t3) + // (ite c (ite c t1 t2) t3) ==> (ite c t1 t3 if (m().is_ite(t) && to_app(t)->get_arg(0) == c) { // Remark: (ite c (ite (not c) t1 t2) t3) ==> (ite c t2 t3) does not happen if applying rewrites bottom up t = to_app(t)->get_arg(1); s = true; } + // (ite c t1 (ite c2 t1 t2)) ==> (ite (or c c2) t1 t2) + if (m().is_ite(e) && to_app(e)->get_arg(1) == t) { + result = m().mk_ite(m().mk_or(c, to_app(e)->get_arg(0)), t, to_app(e)->get_arg(2)); + return BR_REWRITE3; + } // (ite c t1 (ite c t2 t3)) ==> (ite c t1 t3) if (m().is_ite(e) && to_app(e)->get_arg(0) == c) { diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 5e41a704f41..563b56b76be 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -824,6 +824,26 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { result = m_autil.mk_add(es.size(), es.c_ptr()); return BR_REWRITE2; } +#if 0 + expr* s = nullptr, *offset = nullptr, *length = nullptr; + if (str().is_extract(a, s, offset, length)) { + expr_ref len_s(str().mk_length(s), m()); + // if offset < 0 then 0 + // elif length <= 0 then 0 + // elif offset >= len(s) then 0 + // elif offset + length > len(s) then len(s) - offset + // else length + expr_ref zero(m_autil.mk_int(0), m()); + result = length; + result = m().mk_ite(m_autil.mk_gt(m_autil.mk_add(offset, length), len_s), + m_autil.mk_sub(len_s, offset), + result); + result = m().mk_ite(m().mk_or(m_autil.mk_ge(offset, len_s), m_autil.mk_le(length, zero), m_autil.mk_lt(offset, zero)), + zero, + result); + return BR_REWRITE_FULL; + } +#endif return BR_FAILED; } diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 389dca4c767..2027698eb31 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -271,6 +271,7 @@ namespace smt2 { } scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive) : + ctx(ctx), m_interactive(interactive), m_spos(0), m_curr(0), // avoid Valgrind warning @@ -283,7 +284,6 @@ namespace smt2 { m_stream(stream), m_cache_input(false) { - m_smtlib2_compliant = ctx.params().m_smtlib2_compliant; for (int i = 0; i < 256; ++i) { m_normalized[i] = (signed char) i; @@ -366,7 +366,7 @@ namespace smt2 { if (t == NULL_TOKEN) break; return t; case '-': - if (m_smtlib2_compliant) + if (ctx.params().m_smtlib2_compliant) return read_symbol(); else return read_signed_number(); diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h index ad016354577..83a5e51259f 100644 --- a/src/parsers/smt2/smt2scanner.h +++ b/src/parsers/smt2/smt2scanner.h @@ -30,6 +30,7 @@ namespace smt2 { class scanner { private: + cmd_context& ctx; bool m_interactive; int m_spos; // position in the current line of the stream char m_curr; // current char; @@ -54,7 +55,6 @@ namespace smt2 { svector m_cache; svector m_cache_result; - bool m_smtlib2_compliant; char curr() const { return m_curr; } void new_line() { m_line++; m_spos = 0; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1ab44c1f614..ed81f036b49 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1579,6 +1579,8 @@ void theory_seq::add_length(expr* e, expr* l) { Add length limit restrictions to sequence s. */ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) { + if (m_sk.is_skolem(s)) + return; expr_ref lim_e = m_ax.add_length_limit(s, k); unsigned k0 = 0; if (m_length_limit_map.find(s, k0)) {