From 79a8e9aab0e1c0b3f2d70037b21e2bca09cc816c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 May 2017 12:09:51 -0700 Subject: [PATCH] fix build break #1029 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 29 +---------------------------- src/smt/theory_seq.cpp | 2 ++ src/smt/theory_seq.h | 2 +- src/util/lp/mps_reader.h | 2 +- 4 files changed, 5 insertions(+), 30 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 01f4f924f..dc1931bac 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1423,37 +1423,10 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { } /* - * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn)) + * (re.range c_1 c_n) */ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { return BR_FAILED; - TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";); - zstring str_lo, str_hi; - if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) { - if (str_lo.length() == 1 && str_hi.length() == 1) { - unsigned int c1 = str_lo[0]; - unsigned int c2 = str_hi[0]; - if (c1 > c2) { - // exchange c1 and c2 - unsigned int tmp = c1; - c2 = c1; - c1 = tmp; - } - zstring s(c1); - expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m()); - for (unsigned int ch = c1 + 1; ch <= c2; ++ch) { - zstring s_ch(ch); - expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m()); - acc = m_util.re.mk_union(acc, acc2); - } - result = acc; - return BR_REWRITE2; - } else { - m().raise_exception("string constants in re.range must have length 1"); - } - } - - return BR_FAILED; } /* diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7a9369fd3..3f8845546 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2176,6 +2176,8 @@ bool theory_seq::simplify_and_solve_eqs() { return m_new_propagation || ctx.inconsistent(); } +void theory_seq::internalize_eq_eh(app * atom, bool_var v) {} + bool theory_seq::internalize_term(app* term) { context & ctx = get_context(); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 2b8fb2fd7..e145d3077 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -343,7 +343,7 @@ namespace smt { virtual final_check_status final_check_eh(); virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } virtual bool internalize_term(app*); - virtual void internalize_eq_eh(app * atom, bool_var v) {} + virtual void internalize_eq_eh(app * atom, bool_var v); virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); virtual void assign_eh(bool_var v, bool is_true); diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h index 4c08ec8e6..af9ae6b4e 100644 --- a/src/util/lp/mps_reader.h +++ b/src/util/lp/mps_reader.h @@ -655,7 +655,7 @@ class mps_reader { sense interval G [rhs, rhs + |range|] L [rhs - |range|, rhs] - E [rhs, rhs + |range|] if range ¡Ý 0 [rhs - |range|, rhs] if range < 0 + E [rhs, rhs + |range|] if range in [rhs - |range|, rhs] if range < 0 where |range| is range's absolute value. */