Fixed to_dot for integer constraints

src/smt/seq/seq_nielsen.cpp

@@ -1536,6 +1536,7 @@ namespace seq {
 
     nielsen_graph::search_result nielsen_graph::search_dfs(nielsen_node* node, unsigned depth) {
         ++m_stats.m_num_dfs_nodes;
+        std::cout << m_stats.m_num_dfs_nodes << std::endl;
         m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
 
         // check for external cancellation (timeout, user interrupt)
@@ -1561,7 +1562,7 @@ namespace seq {
         node->set_eval_idx(m_run_idx);
 
         // simplify constraints (idempotent after first call)
-        simplify_result sr = node->simplify_and_init();
+        const simplify_result sr = node->simplify_and_init();
 
         if (sr == simplify_result::conflict) {
             ++m_stats.m_num_simplify_conflict;
@@ -1597,7 +1598,9 @@ namespace seq {
             return search_result::unsat;
         }
 
-        if (sr == simplify_result::satisfied || node->is_satisfied()) {
+        SASSERT(sr != simplify_result::satisfied || node->is_satisfied());
+
+        if (node->is_satisfied()) {
             // Before declaring SAT, check leaf-node regex feasibility:
             // for each variable with multiple regex constraints, verify
             // that the intersection of all its regexes is non-empty.
@@ -1682,8 +1685,7 @@ namespace seq {
 
     // Returns true if variable snode `var` appears anywhere in the token list of `n`.
     static bool snode_contains_var(euf::snode const* n, euf::snode const* var) {
-        if (!n || !var)
+        SASSERT(n && var);
-            return false;
         euf::snode_vector tokens;
         n->collect_tokens(tokens);
         for (const euf::snode* t : tokens) {
@@ -1694,6 +1696,10 @@ namespace seq {
     }
 
     bool nielsen_graph::apply_det_modifier(nielsen_node* node) {
+        // resist the temptation to add rules that "simplify" primitive membership constraints!
+        // pretty much all of them could cause divergence!
+        // e.g., x \in aa* => don't apply substitution x / ax even though it looks "safe" to do
+        // there might be another constraint x \in a* and they would just push the "a" back and forth!
         ast_manager& m = m_sg.get_manager();
         seq_util& seq = m_sg.get_seq_util();
         arith_util arith(m);

src/smt/seq/seq_nielsen_pp.cpp

@@ -151,6 +151,21 @@ namespace seq {
         }
         app* a = to_app(e);
         expr* x, * y;
+        if (arith.is_le(e, x, y)) {
+            return arith_expr_html(x, names, next_id, m) + " < " + arith_expr_html(y, names, next_id, m);
+        }
+        if (arith.is_gt(e, x, y)) {
+            return arith_expr_html(x, names, next_id, m) + " > " + arith_expr_html(y, names, next_id, m);
+        }
+        if (arith.is_le(e, x, y)) {
+            return arith_expr_html(x, names, next_id, m) + " ≤ " + arith_expr_html(y, names, next_id, m);
+        }
+        if (arith.is_ge(e, x, y)) {
+            return arith_expr_html(x, names, next_id, m) + " ≥ " + arith_expr_html(y, names, next_id, m);
+        }
+        if (m.is_eq(e, x, y)) {
+            return arith_expr_html(x, names, next_id, m) + " = " + arith_expr_html(y, names, next_id, m);
+        }
         if (arith.is_add(e)) {
             std::string r = arith_expr_html(a->get_arg(0), names, next_id, m);
             for (unsigned i = 1; i < a->get_num_args(); ++i) {
@@ -403,7 +418,7 @@ namespace seq {
             if (!e) {
                 result += "#" + std::to_string(tok->id());
             } else if (tok->is_var()) {
-                if (to_app(e)->get_num_args() > 0) {
+                if (to_app(e)->get_num_args() == 0) {
                     result += to_app(e)->get_decl()->get_name().str();
                 }
                 else if (names.contains(e))
@@ -461,10 +476,16 @@ namespace seq {
 
     std::ostream& nielsen_node::to_html(std::ostream& out, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m) const {
         bool any = false;
+        bool hasEq = false;
+        bool hasMem = false;
+        bool hasRange = false;
+        bool hasDiseq = false;
+        bool hasInt = false;
 
         // string equalities
         for (auto const& eq : m_str_eq) {
             if (!any) { out << "Cnstr:<br/>"; any = true; }
+            if (!hasEq) { out << "Eq:<br/>"; hasEq = true; }
             out << snode_label_html(eq.m_lhs, names, next_id, m)
                 << " = "
                 << snode_label_html(eq.m_rhs, names, next_id, m)
@@ -473,6 +494,7 @@ namespace seq {
         // regex memberships
         for (auto const& mem : m_str_mem) {
             if (!any) { out << "Cnstr:<br/>"; any = true; }
+            if (!hasMem) { out << "Mem:<br/>"; hasMem = true; }
             out << snode_label_html(mem.m_str, names, next_id, m)
                 << " &#8712; "
                 << snode_label_html(mem.m_regex, names, next_id, m)
@@ -481,6 +503,7 @@ namespace seq {
         // character ranges
         for (auto const& kv : m_char_ranges) {
             if (!any) { out << "Cnstr:<br/>"; any = true; }
+            if (!hasRange) { out << "Ranges:<br/>"; hasRange = true; }
             out << "?" << kv.m_key << " &#8712; ";
             kv.m_value.display(out);
             out << "<br/>";
@@ -488,6 +511,7 @@ namespace seq {
         // character disequalities
         for (auto const& kv : m_char_diseqs) {
             if (!any) { out << "Cnstr:<br/>"; any = true; }
+            if (!hasDiseq) { out << "Diseq:<br/>"; hasDiseq = true; }
             for (euf::snode* d : kv.m_value) {
                 out << "?" << kv.m_key << " &#8800; ?" << d->id() << "<br/>";
             }
@@ -495,6 +519,7 @@ namespace seq {
         // integer constraints
         for (auto const& ic : m_constraints) {
             if (!any) { out << "Cnstr:<br/>"; any = true; }
+            if (!hasInt) { out << "Int:<br/>"; hasInt = true; }
             out << constraint_html(ic, names, next_id, m) << "<br/>";
         }
 

src/smt/theory_nseq.cpp

@@ -95,6 +95,7 @@ namespace smt {
     // -----------------------------------------------------------------------
 
     bool theory_nseq::internalize_atom(app* atom, bool /*gate_ctx*/) {
+        // std::cout << "internalize_atom: " << mk_pp(atom, m) << std::endl;
         // str.in_re atoms are boolean predicates: register as bool_var
         // so that assign_eh fires when the SAT solver assigns them.
         // Following theory_seq: create a bool_var directly without an enode
@@ -126,6 +127,7 @@ namespace smt {
     }
 
     bool theory_nseq::internalize_term(app* term) {
+        // std::cout << "internalize_term: " << mk_pp(term, m) << std::endl;
         // ensure ALL children are internalized (following theory_seq pattern)
         for (auto arg : *term) {
             mk_var(ensure_enode(arg));
@@ -207,6 +209,7 @@ namespace smt {
 
     void theory_nseq::assign_eh(bool_var v, bool is_true) {
         expr* e = ctx.bool_var2expr(v);
+        // std::cout << "assigned " << mk_pp(e, m) << " = " << is_true << std::endl;
         expr* s = nullptr, *re = nullptr;
         TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";);
         if (m_seq.str.is_in_re(e, s, re)) {