fix spelling

src/ast/rewriter/seq_rewriter.cpp

@@ -552,9 +552,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
             st = mk_re_concat(args[0], args[1], result); 
         }
         break;
-    case _OP_RE_ANTIMOROV_UNION:
+    case _OP_RE_ANTIMIROV_UNION:
         SASSERT(num_args == 2);
-        // Rewrite Antimorov union to real union
+        // Rewrite antimirov union to real union
         result = re().mk_union(args[0], args[1]);
         st = BR_REWRITE1;
         break;
@@ -2723,7 +2723,7 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) {
         re().is_intersection(r, r1, r2)) { 
         m_br.mk_and(is_nullable(r1), is_nullable(r2), result);
     }
-    else if (re().is_union(r, r1, r2) || re().is_antimorov_union(r, r1, r2)) {
+    else if (re().is_union(r, r1, r2) || re().is_antimirov_union(r, r1, r2)) {
         m_br.mk_or(is_nullable(r1), is_nullable(r2), result);
     }
     else if (re().is_diff(r, r1, r2)) {
@@ -2908,7 +2908,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
     Once the derivative is built, we return BR_REWRITE_FULL so that
     any remaining possible simplification is performed from the bottom up.
 
-    Rewriting also replaces _OP_RE_ANTIMOROV_UNION, which is produced
+    Rewriting also replaces _OP_RE_antimirov_UNION, which is produced
     by is_derivative, with real union.
 */
 br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
@@ -2924,16 +2924,16 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
     When computing derivatives recursively, we preserve the following
     BDD normal form:
 
-    - At the top level, the derivative is a union of Antimorov derivatives
+    - At the top level, the derivative is a union of antimirov derivatives
       (Conceptually each element of the union is a different derivative).
       We currently express this derivative using an internal op code:
-          _OP_RE_ANTIMOROV_UNION
-    - An Antimorov derivative is a nested if-then-else term.
+          _OP_RE_antimirov_UNION
+    - An antimirov derivative is a nested if-then-else term.
       if-then-elses are pushed outwards and sorted by condition ID
       (cond->get_id()), from largest on the outside to smallest on the
       inside. Duplicate nested conditions are eliminated.
     - The leaves of the if-then-else BDD can have unions themselves,
-      but these are interpreted as Regex union, not as separate Antimorov
+      but these are interpreted as Regex union, not as separate antimirov
       derivatives.
 
     To debug the normal form, call Z3 with -dbg:seq_regex:
@@ -2962,7 +2962,7 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) {
     unsigned lo = 0, hi = 0;
     STRACE("seq_verbose", tout << " (level " << level << ")";);
     int new_level = 0;
-    if (re().is_antimorov_union(r)) {
+    if (re().is_antimirov_union(r)) {
         SASSERT(level >= 2);
         new_level = 2;
     }
@@ -2975,7 +2975,7 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) {
     SASSERT(!re().is_opt(r));
     SASSERT(!re().is_plus(r));
 
-    if (re().is_antimorov_union(r, r1, r2) ||
+    if (re().is_antimirov_union(r, r1, r2) ||
         re().is_concat(r, r1, r2) ||
         re().is_union(r, r1, r2) ||
         re().is_intersection(r, r1, r2) ||
@@ -3410,8 +3410,8 @@ expr_ref  seq_rewriter::simplify_path(expr* path) {
 }
 
 
-expr_ref seq_rewriter::mk_der_antimorov_union(expr* r1, expr* r2) {
-    return mk_der_op(_OP_RE_ANTIMOROV_UNION, r1, r2);
+expr_ref seq_rewriter::mk_der_antimirov_union(expr* r1, expr* r2) {
+    return mk_der_op(_OP_RE_ANTIMIROV_UNION, r1, r2);
 }
 
 expr_ref seq_rewriter::mk_der_union(expr* r1, expr* r2) {
@@ -3512,7 +3512,7 @@ bool seq_rewriter::ite_bdds_compatabile(expr* a, expr* b) {
             OP_RE_INTERSECT
             OP_RE_UNION
             OP_RE_CONCAT
-            _OP_RE_ANTIMOROV_UNION
+            _OP_RE_antimirov_UNION
         - a and b are in normal form (check_deriv_normal_form)
 
     Postcondition:
@@ -3542,44 +3542,44 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
     };
 
     // Choose when to lift a union to the top level, by converting
-    // it to an Antimorov union
-    // This implements a restricted form of Antimorov derivatives
+    // it to an antimirov union
+    // This implements a restricted form of antimirov derivatives
     if (k == OP_RE_UNION) {
-        if (re().is_antimorov_union(a) || re().is_antimorov_union(b)) {
-            k = _OP_RE_ANTIMOROV_UNION;
+        if (re().is_antimirov_union(a) || re().is_antimirov_union(b)) {
+            k = _OP_RE_ANTIMIROV_UNION;
         }
         #if 0
-        // Disabled: eager Antimorov lifting unless BDDs are compatible
+        // Disabled: eager antimirov lifting unless BDDs are compatible
         // Note: the check for BDD compatibility could be made more
-        // sophisticated: in an Antimorov union of n terms, we really
+        // sophisticated: in an antimirov union of n terms, we really
         // want to check if any pair of them is compatible.
         else if (m().is_ite(a) && m().is_ite(b) &&
                  !ite_bdds_compatabile(a, b)) {
-            k = _OP_RE_ANTIMOROV_UNION;
+            k = _OP_RE_ANTIMIROV_UNION;
         }
         #endif
     }
-    if (k == _OP_RE_ANTIMOROV_UNION) {
-        result = re().mk_antimorov_union(a, b);
+    if (k == _OP_RE_ANTIMIROV_UNION) {
+        result = re().mk_antimirov_union(a, b);
         return result;
     }
-    if (re().is_antimorov_union(a, a1, a2)) {
+    if (re().is_antimirov_union(a, a1, a2)) {
         expr_ref r1(m()), r2(m());
         r1 = mk_der_op(k, a1, b);
         r2 = mk_der_op(k, a2, b);
-        result = re().mk_antimorov_union(r1, r2);
+        result = re().mk_antimirov_union(r1, r2);
         return result;
     }
-    if (re().is_antimorov_union(b, b1, b2)) {
+    if (re().is_antimirov_union(b, b1, b2)) {
         expr_ref r1(m()), r2(m());
         r1 = mk_der_op(k, a, b1);
         r2 = mk_der_op(k, a, b2);
-        result = re().mk_antimorov_union(r1, r2);
+        result = re().mk_antimirov_union(r1, r2);
         return result;
     }
 
     // Remaining non-union case: combine two if-then-else BDDs
-    // (underneath top-level Antimorov unions)
+    // (underneath top-level antimirov unions)
     if (m().is_ite(a, ca, a1, a2)) {
         expr_ref r1(m()), r2(m());
         expr_ref notca(m().mk_not(ca), m());
@@ -3688,9 +3688,9 @@ expr_ref seq_rewriter::mk_der_compl(expr* r) {
     expr_ref result(m_op_cache.find(OP_RE_COMPLEMENT, r, nullptr, nullptr), m());
     if (!result) {
         expr* c = nullptr, * r1 = nullptr, * r2 = nullptr;
-        if (re().is_antimorov_union(r, r1, r2)) {
+        if (re().is_antimirov_union(r, r1, r2)) {
             // Convert union to intersection
-            // Result: Antimorov union at top level is lost, pushed inside ITEs
+            // Result: antimirov union at top level is lost, pushed inside ITEs
             expr_ref res1(m()), res2(m());
             res1 = mk_der_compl(r1);
             res2 = mk_der_compl(r2);
@@ -3796,11 +3796,11 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             return result;
         }
         else {
-            // Instead of mk_der_union here, we use mk_der_antimorov_union to
+            // Instead of mk_der_union here, we use mk_der_antimirov_union to
             // force the two cases to be considered separately and lifted to
             // the top level. This avoids blowup in cases where determinization
             // is expensive.
-            return mk_der_antimorov_union(result, mk_der_concat(is_n, dr2));
+            return mk_der_antimirov_union(result, mk_der_concat(is_n, dr2));
         }
     }
     else if (re().is_star(r, r1)) {

src/ast/rewriter/seq_rewriter.h

@@ -200,7 +200,7 @@ class seq_rewriter {
     expr_ref mk_der_inter(expr* a, expr* b);
     expr_ref mk_der_compl(expr* a);
     expr_ref mk_der_cond(expr* cond, expr* ele, sort* seq_sort);
-    expr_ref mk_der_antimorov_union(expr* r1, expr* r2);
+    expr_ref mk_der_antimirov_union(expr* r1, expr* r2);
     bool ite_bdds_compatabile(expr* a, expr* b);
     /* if r has the form deriv(en..deriv(e1,to_re(s))..) returns 's = [e1..en]' else returns '() in r'*/
     expr_ref is_nullable_symbolic_regex(expr* r, sort* seq_sort);

src/ast/seq_decl_plugin.cpp

@@ -243,7 +243,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA);
     m_sigs[OP_RE_REVERSE]        = alloc(psig, m, "re.reverse", 1, 1, &reA, reA);
     m_sigs[OP_RE_DERIVATIVE]     = alloc(psig, m, "re.derivative", 1, 2, AreA, reA);
-    m_sigs[_OP_RE_ANTIMOROV_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA);
+    m_sigs[_OP_RE_ANTIMIROV_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA);
     m_sigs[OP_SEQ_TO_RE]         = alloc(psig, m, "seq.to.re",  1, 1, &seqA, reA);
     m_sigs[OP_SEQ_IN_RE]         = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT);
     m_sigs[OP_SEQ_REPLACE_RE_ALL] = alloc(psig, m, "str.replace_re_all", 1, 3, seqAreAseqA, seqA);
@@ -414,7 +414,7 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     case OP_RE_COMPLEMENT:
     case OP_RE_REVERSE:
     case OP_RE_DERIVATIVE:
-    case _OP_RE_ANTIMOROV_UNION:
+    case _OP_RE_ANTIMIROV_UNION:
         m_has_re = true;
         // fall-through
     case OP_SEQ_UNIT:
@@ -1283,7 +1283,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
         print(out, r1);
         print(out, r2);
     }
-    else if (re.is_antimorov_union(e, r1, r2) || re.is_union(e, r1, r2)) {
+    else if (re.is_antimirov_union(e, r1, r2) || re.is_union(e, r1, r2)) {
         out << "(";
         print(out, r1);
         out << (html_encode ? "&#x22C3;" : "|");

src/ast/seq_decl_plugin.h

@@ -103,7 +103,7 @@ enum seq_op_kind {
     _OP_REGEXP_EMPTY,
     _OP_REGEXP_FULL_CHAR,
     _OP_RE_IS_NULLABLE,
-    _OP_RE_ANTIMOROV_UNION, // Lifted union for antimorov-style derivatives
+    _OP_RE_ANTIMIROV_UNION, // Lifted union for antimirov-style derivatives
     _OP_SEQ_SKOLEM,
     LAST_SEQ_OP
 };
@@ -525,7 +525,7 @@ class seq_util {
         app* mk_of_pred(expr* p);
         app* mk_reverse(expr* r) { return m.mk_app(m_fid, OP_RE_REVERSE, r); }
         app* mk_derivative(expr* ele, expr* r) { return m.mk_app(m_fid, OP_RE_DERIVATIVE, ele, r); }
-        app* mk_antimorov_union(expr* r1, expr* r2) { return m.mk_app(m_fid, _OP_RE_ANTIMOROV_UNION, r1, r2); }
+        app* mk_antimirov_union(expr* r1, expr* r2) { return m.mk_app(m_fid, _OP_RE_ANTIMIROV_UNION, r1, r2); }
 
         bool is_to_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
         bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
@@ -557,7 +557,7 @@ class seq_util {
         bool is_of_pred(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OF_PRED); }
         bool is_reverse(expr const* n) const { return is_app_of(n, m_fid, OP_RE_REVERSE); }
         bool is_derivative(expr const* n) const { return is_app_of(n, m_fid, OP_RE_DERIVATIVE); }
-        bool is_antimorov_union(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_ANTIMOROV_UNION); }
+        bool is_antimirov_union(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_ANTIMIROV_UNION); }
         MATCH_UNARY(is_to_re);
         MATCH_BINARY(is_concat);
         MATCH_BINARY(is_union);
@@ -571,7 +571,7 @@ class seq_util {
         MATCH_UNARY(is_of_pred);
         MATCH_UNARY(is_reverse);
         MATCH_BINARY(is_derivative);
-        MATCH_BINARY(is_antimorov_union);
+        MATCH_BINARY(is_antimirov_union);
         bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const;
         bool is_loop(expr const* n, expr*& body, unsigned& lo) const;
         bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const;