Merge branch 'master' of https://github.com/Z3Prover/z3

src/ast/rewriter/enum2bv_rewriter.cpp

@@ -85,7 +85,7 @@ struct enum2bv_rewriter::imp {
 
         void throw_non_fd(expr* e) {
             std::stringstream strm;
-            strm << "unabled nested data-type expression " << mk_pp(e, m);
+            strm << "unable to handle nested data-type expression " << mk_pp(e, m);
             throw rewriter_exception(strm.str().c_str());
         }
 

src/ast/seq_decl_plugin.cpp

@@ -38,8 +38,16 @@ static bool is_hex_digit(char ch, unsigned& d) {
     return false;
 }
 
+static bool is_octal_digit(char ch, unsigned& d) {
+    if ('0' <= ch && ch <= '7') {
+        d = ch - '0';
+        return true;
+    }
+    return false;
+}
+
 static bool is_escape_char(char const *& s, unsigned& result) {
-    unsigned d1, d2;
+    unsigned d1, d2, d3;
     if (*s != '\\' || *(s + 1) == 0) {
         return false;
     }
@@ -49,6 +57,29 @@ static bool is_escape_char(char const *& s, unsigned& result) {
         s += 4;
         return true;
     }
+    /* C-standard octal escapes: either 1, 2, or 3 octal digits,
+     * stopping either at 3 digits or at the first non-digit character.
+     */
+    /* 1 octal digit */
+    if (is_octal_digit(*(s + 1), d1) && !is_octal_digit(*(s + 2), d2)) {
+        result = d1;
+        s += 2;
+        return true;
+    }
+    /* 2 octal digits */
+    if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) &&
+            !is_octal_digit(*(s + 3), d3)) {
+        result = d1 * 8 + d2;
+        s += 3;
+        return true;
+    }
+    /* 3 octal digits */
+    if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) &&
+            is_octal_digit(*(s + 3), d3)) {
+        result = d1*64 + d2*8 + d3;
+        s += 4;
+        return true;
+    }
     switch (*(s + 1)) {
     case 'a':
         result = '\a';
@@ -253,8 +284,54 @@ zstring zstring::operator+(zstring const& other) const {
     return result;
 }
 
-std::ostream& zstring::operator<<(std::ostream& out) const {
-    return out << encode();
+bool zstring::operator==(const zstring& other) const {
+    // two strings are equal iff they have the same length and characters
+    if (length() != other.length()) {
+        return false;
+    }
+    for (unsigned i = 0; i < length(); ++i) {
+        unsigned Xi = m_buffer[i];
+        unsigned Yi = other[i];
+        if (Xi != Yi) {
+            return false;
+        }
+    }
+
+    return true;
+}
+
+bool zstring::operator!=(const zstring& other) const {
+    return !(*this == other);
+}
+
+std::ostream& operator<<(std::ostream &os, const zstring &str) {
+    return os << str.encode();
+}
+
+bool operator<(const zstring& lhs, const zstring& rhs) {
+    // This has the same semantics as strcmp()
+    unsigned len = lhs.length();
+    if (rhs.length() < len) {
+        len = rhs.length();
+    }
+    for (unsigned i = 0; i < len; ++i) {
+        unsigned Li = lhs[i];
+        unsigned Ri = rhs[i];
+        if (Li < Ri) {
+            return true;
+        } else if (Li > Ri) {
+            return false;
+        } else {
+            continue;
+        }
+    }
+    // at this point, all compared characters are equal,
+    // so decide based on the relative lengths
+    if (lhs.length() < rhs.length()) {
+        return true;
+    } else {
+        return false;
+    }
 }
 
 
@@ -442,6 +519,7 @@ void seq_decl_plugin::init() {
     sort* str2TintT[3] = { strT, strT, intT };
     sort* seqAintT[2] = { seqA, intT };
     sort* seq3A[3] = { seqA, seqA, seqA };
+    sort* reTintT[2] = { reT, intT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq.unit",     1, 1, &A, seqA);
@@ -485,6 +563,7 @@ void seq_decl_plugin::init() {
     m_sigs[_OP_REGEXP_EMPTY]      = alloc(psig, m, "re.nostr", 0, 0, 0, reT);
     m_sigs[_OP_REGEXP_FULL]       = alloc(psig, m, "re.allchar", 0, 0, 0, reT);
     m_sigs[_OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT);
+    m_sigs[_OP_RE_UNROLL]         = alloc(psig, m, "_re.unroll", 0, 2, reTintT, strT);
 }
 
 void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
@@ -641,6 +720,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
             m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
         }
         
+    case _OP_RE_UNROLL:
+        match(*m_sigs[k], arity, domain, range, rng);
+        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
 
     case OP_STRING_CONST:
         if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {

src/ast/seq_decl_plugin.h

@@ -79,6 +79,7 @@ enum seq_op_kind {
     _OP_REGEXP_EMPTY,
     _OP_REGEXP_FULL,
     _OP_SEQ_SKOLEM,
+    _OP_RE_UNROLL,
     LAST_SEQ_OP
 };
 
@@ -113,7 +114,11 @@ public:
     int  indexof(zstring const& other, int offset) const;
     zstring extract(int lo, int hi) const;
     zstring operator+(zstring const& other) const;
-    std::ostream& operator<<(std::ostream& out) const;
+    bool operator==(const zstring& other) const;
+    bool operator!=(const zstring& other) const;
+
+    friend std::ostream& operator<<(std::ostream &os, const zstring &str);
+    friend bool operator<(const zstring& lhs, const zstring& rhs);
 };
 
 class seq_decl_plugin : public decl_plugin {
@@ -334,6 +339,7 @@ public:
         MATCH_UNARY(is_opt);
         bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi);
         bool is_loop(expr const* n, expr*& body, unsigned& lo);
+        bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); }
     };
     str str;
     re  re;