From 1d46d5c8708185726581d0acba5f389f8b24334b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Jun 2019 15:53:32 -0700 Subject: [PATCH] use signed char per porting issue for ARM/64 Signed-off-by: Nikolaj Bjorner --- src/api/z3_replayer.cpp | 6 +++--- src/parsers/util/scanner.cpp | 22 +++++++++++----------- src/parsers/util/scanner.h | 8 ++++---- src/smt/mam.cpp | 2 +- src/smt/theory_seq.cpp | 8 +++++--- 5 files changed, 24 insertions(+), 22 deletions(-) diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 97b88c9d7..a2682fc35 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -36,7 +36,7 @@ void throw_invalid_reference() { struct z3_replayer::imp { z3_replayer & m_owner; std::istream & m_stream; - char m_curr; // current char; + signed char m_curr; // current char; int m_line; // line svector m_string; symbol m_id; @@ -158,7 +158,7 @@ struct z3_replayer::imp { } } - char curr() const { return m_curr; } + signed char curr() const { return m_curr; } void new_line() { m_line++; } void next() { m_curr = m_stream.get(); } @@ -168,7 +168,7 @@ struct z3_replayer::imp { m_string.reset(); next(); while (true) { - char c = curr(); + signed char c = curr(); if (c == EOF) { throw z3_replayer_exception("unexpected end of file"); } diff --git a/src/parsers/util/scanner.cpp b/src/parsers/util/scanner.cpp index 4ed47e81f..c0947fa24 100644 --- a/src/parsers/util/scanner.cpp +++ b/src/parsers/util/scanner.cpp @@ -18,7 +18,7 @@ Revision History: --*/ #include "parsers/util/scanner.h" -inline char scanner::read_char() { +inline signed char scanner::read_char() { if (m_is_interactive) { ++m_pos; return m_stream.get(); @@ -58,7 +58,7 @@ inline bool scanner::state_ok() { void scanner::comment(char delimiter) { while(state_ok()) { - char ch = read_char(); + signed char ch = read_char(); if ('\n' == ch) { ++m_line; } @@ -68,7 +68,7 @@ void scanner::comment(char delimiter) { } } -scanner::token scanner::read_symbol(char ch) { +scanner::token scanner::read_symbol(signed char ch) { bool escape = false; if (m_smt2) m_string.pop_back(); // remove leading '|' @@ -94,7 +94,7 @@ scanner::token scanner::read_symbol(char ch) { scanner::token scanner::read_id(char first_char) { - char ch; + signed char ch; m_string.reset(); m_params.reset(); m_string.push_back(first_char); @@ -159,7 +159,7 @@ bool scanner::read_params() { unsigned param_num = 0; while (state_ok()) { - char ch = read_char(); + signed char ch = read_char(); switch (m_normalized[(unsigned char) ch]) { case '0': param_num = 10*param_num + (ch - '0'); @@ -208,7 +208,7 @@ scanner::token scanner::read_number(char first_char, bool is_pos) { m_state = INT_TOKEN; while (true) { - char ch = read_char(); + signed char ch = read_char(); if (m_normalized[(unsigned char) ch] == '0') { m_number = rational(10)*m_number + rational(ch - '0'); if (m_state == FLOAT_TOKEN) { @@ -236,7 +236,7 @@ scanner::token scanner::read_string(char delimiter, token result) { m_string.reset(); m_params.reset(); while (true) { - char ch = read_char(); + signed char ch = read_char(); if (!state_ok()) { return m_state; @@ -265,7 +265,7 @@ scanner::token scanner::read_string(char delimiter, token result) { scanner::token scanner::read_bv_literal() { TRACE("scanner", tout << "read_bv_literal\n";); if (m_bv_token) { - char ch = read_char(); + signed char ch = read_char(); if (ch == 'x') { ch = read_char(); m_number = rational(0); @@ -315,7 +315,7 @@ scanner::token scanner::read_bv_literal() { } else { // hack for the old parser - char ch = read_char(); + signed char ch = read_char(); bool is_hex = false; m_state = ID_TOKEN; @@ -342,7 +342,7 @@ scanner::token scanner::read_bv_literal() { } while (true) { - ch = read_char(); + signed ch = read_char(); if (ch == '0' || ch == '1' || (is_hex && (('0' <= ch && ch <= '9') || @@ -449,7 +449,7 @@ scanner::scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_tok scanner::token scanner::scan() { while (state_ok()) { - char ch = read_char(); + signed char ch = read_char(); switch (m_normalized[(unsigned char) ch]) { case ' ': break; diff --git a/src/parsers/util/scanner.h b/src/parsers/util/scanner.h index cd074479c..2871eb901 100644 --- a/src/parsers/util/scanner.h +++ b/src/parsers/util/scanner.h @@ -63,7 +63,7 @@ private: rational m_number; unsigned m_bv_size; token m_state; - char m_normalized[256]; + char m_normalized[256]; vector m_string; std::istream& m_stream; std::ostream& m_err; @@ -71,13 +71,13 @@ private: buffer m_buffer; unsigned m_bpos; unsigned m_bend; - char m_last_char; + char m_last_char; bool m_is_interactive; bool m_smt2; bool m_bv_token; - char read_char(); - token read_symbol(char ch); + signed char read_char(); + token read_symbol(signed char ch); void unread_char(); void comment(char delimiter); token read_id(char first_char); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 836c1dfcc..445f49244 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -79,7 +79,7 @@ namespace smt { // // ------------------------------------ class label_hasher { - svector m_lbl2hash; // cache: lbl_id -> hash + svector m_lbl2hash; // cache: lbl_id -> hash void mk_lbl_hash(unsigned lbl_id) { unsigned a = 17; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 23b9da9dc..f084cffd1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3972,7 +3972,7 @@ public: else { for (source_t src : m_source) { switch (src) { - case unit_source: + case unit_source: args.push_back(th.m_util.str.mk_unit(values[j++])); break; case string_source: @@ -5130,8 +5130,10 @@ void theory_seq::add_nth_axiom(expr* e) { add_axiom(mk_eq(ch, e, false)); } else if (!m_internal_nth_table.contains(e)) { - expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m); - add_axiom(mk_eq(s, emp, false), mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false)); + expr_ref zero(m_autil.mk_int(0), m); + literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero)); + literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero)); + add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false)); } }