remove unused code, fix unit tests

src/ast/rewriter/seq_rewriter.cpp

@@ -33,58 +33,6 @@ Authors:
 #include "params/seq_rewriter_params.hpp"
 
 
-expr_ref sym_expr::accept(expr* e) {
-    ast_manager& m = m_t.get_manager();
-    expr_ref result(m);
-    var_subst subst(m);
-    seq_util u(m);
-    unsigned r1, r2, r3;
-    switch (m_ty) {
-    case t_pred:         
-        result = subst(m_t, 1, &e);
-        break;    
-    case t_not:
-        result = m_expr->accept(e);
-        result = m.mk_not(result);
-        break;
-    case t_char:
-        SASSERT(e->get_sort() == m_t->get_sort());
-        SASSERT(e->get_sort() == m_sort);
-        result = m.mk_eq(e, m_t);
-        break;
-    case t_range: 
-        if (u.is_const_char(m_t, r1) && u.is_const_char(e, r2) && u.is_const_char(m_s, r3)) {
-            result = m.mk_bool_val((r1 <= r2) && (r2 <= r3));            
-        }
-        else {
-            auto a = u.mk_le(m_t, e);
-            result = m.mk_and(a, u.mk_le(e, m_s));
-        }
-        break;
-    }
-    
-    return result;
-}
-
-std::ostream& sym_expr::display(std::ostream& out) const {
-    switch (m_ty) {
-    case t_char: return out << m_t;
-    case t_range: return out << m_t << ":" << m_s;
-    case t_pred: return out << m_t;
-    case t_not: return m_expr->display(out << "not ");
-    }
-    return out << "expression type not recognized";
-}
-
-struct display_expr1 {
-    ast_manager& m;
-    display_expr1(ast_manager& m): m(m) {}
-    std::ostream& display(std::ostream& out, sym_expr* e) const {
-        return e->display(out);
-    }
-};
-
-
 void seq_rewriter::updt_params(params_ref const & p) {
     seq_rewriter_params sp(p);
     m_coalesce_chars = sp.coalesce_chars();

src/ast/rewriter/seq_rewriter.h

@@ -37,6 +37,7 @@ inline std::ostream& operator<<(std::ostream& out, expr_ref_pair_vector const& e
     return out;
 }
 
+#if 0
 class sym_expr {
     enum ty {
         t_char,
@@ -80,6 +81,7 @@ public:
     void inc_ref(sym_expr* s) { if (s) s->inc_ref(); }
     void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
 };
+#endif
 
 /**
    \brief Cheap rewrite rules for seq constraints

src/test/seq_monadic.cpp

@@ -44,7 +44,7 @@ class seq_monadic_test {
     seq_util         u;
     sort_ref         m_str;   // String sort
     sort_ref         m_re;    // RegEx sort over m_str
-    seq_monadic::transition_mode m_mode;
+    seq::transition_mode m_mode;
     u_dependency_manager m_dm;   // owns the leaf dependencies used in unsat-core tests
     unsigned         m_fail = 0;
 
@@ -79,8 +79,8 @@ class seq_monadic_test {
     static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; }
     char const* mode_name() const {
         switch (m_mode) {
-        case seq_monadic::transition_mode::brzozowski: return "brz";
-        case seq_monadic::transition_mode::light_antimirov: return "light-ant";
+        case seq::transition_mode::brzozowski_tm: return "brz";
+        case seq::transition_mode::light_antimirov_tm: return "light-ant";
         }
         UNREACHABLE();
         return "";
@@ -288,7 +288,7 @@ class seq_monadic_test {
     }
 
 public:
-    seq_monadic_test(seq_monadic::transition_mode mode) :
+    seq_monadic_test(seq::transition_mode mode) :
         m_reg(m), m_rw(m), m_mon(m_rw, m_trail, mode), u(m), m_str(m), m_re(m), m_mode(mode) {
         m_str = u.str.mk_string_sort();
         m_re  = re().mk_re(m_str);
@@ -297,7 +297,7 @@ public:
 
     void run() {
         std::cout << "=== seq_monadic mode: " << mode_name() << " ===\n";
-        if (m_mode == seq_monadic::transition_mode::light_antimirov)
+        if (m_mode == seq::transition_mode::light_antimirov_tm)
             check_ant_cofactors();
         expr_ref x  = var("x");
         expr_ref a  = word("a");
@@ -710,8 +710,8 @@ public:
 }
 
 void tst_seq_monadic() {
-    seq_monadic_test brz(seq_monadic::transition_mode::brzozowski);
+    seq_monadic_test brz(seq::transition_mode::brzozowski_tm);
     brz.run();
-    seq_monadic_test light_ant(seq_monadic::transition_mode::light_antimirov);
+    seq_monadic_test light_ant(seq::transition_mode::light_antimirov_tm);
     light_ant.run();
 }

src/test/seq_monadic_bench.cpp

@@ -47,20 +47,20 @@ char const* verdict_str(lbool l) {
     return l == l_true ? "sat" : l == l_false ? "unsat" : "undef";
 }
 
-char const* mode_str(seq_monadic::transition_mode mode) {
+char const* mode_str(seq::transition_mode mode) {
     switch (mode) {
-    case seq_monadic::transition_mode::brzozowski: return "brz";
-    case seq_monadic::transition_mode::light_antimirov: return "light-ant";
+    case seq::transition_mode::brzozowski_tm: return "brz";
+    case seq::transition_mode::light_antimirov_tm: return "light-ant";
     }
     UNREACHABLE();
     return "";
 }
 
-seq_monadic::transition_mode get_mode() {
+seq::transition_mode get_mode() {
     char const* mode = getenv("Z3_SEQ_MONADIC_MODE");
     if (mode && std::string(mode) == "brz")
-        return seq_monadic::transition_mode::brzozowski;
-    return seq_monadic::transition_mode::light_antimirov;
+        return seq::transition_mode::brzozowski_tm;
+    return seq::transition_mode::light_antimirov_tm;
 }
 
 bool is_seq_var(expr* t) {
@@ -80,7 +80,7 @@ std::string read_status(std::string const& path) {
 
 lbool run_file(
     std::string const& path,
-    seq_monadic::transition_mode mode,
+    seq::transition_mode mode,
     double& solve_ms,
     bool& parsed,
     bool& complete,
@@ -263,7 +263,7 @@ void display_row(
     std::string const& tier,
     std::string const& status,
     bool complete,
-    seq_monadic::transition_mode mode,
+    seq::transition_mode mode,
     lbool verdict,
     double solve_ms,
     unsigned dropped) {
@@ -279,7 +279,7 @@ void display_row(
 void tst_seq_monadic_bench() {
     namespace fs = std::filesystem;
     std::error_code ec;
-    seq_monadic::transition_mode mode = get_mode();
+    seq::transition_mode mode = get_mode();
 
     if (char const* file = getenv("Z3_SEQ_BENCH_FILE")) {
         double ms = 0;