diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 7765a3e2e..bb183ba96 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/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) - return false; + SASSERT(n && var); 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); diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 7d6373eb2..49b1b997c 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/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& 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:
"; any = true; } + if (!hasEq) { out << "Eq:
"; 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:
"; any = true; } + if (!hasMem) { out << "Mem:
"; hasMem = true; } out << snode_label_html(mem.m_str, names, next_id, m) << " ∈ " << 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:
"; any = true; } + if (!hasRange) { out << "Ranges:
"; hasRange = true; } out << "?" << kv.m_key << " ∈ "; kv.m_value.display(out); out << "
"; @@ -488,6 +511,7 @@ namespace seq { // character disequalities for (auto const& kv : m_char_diseqs) { if (!any) { out << "Cnstr:
"; any = true; } + if (!hasDiseq) { out << "Diseq:
"; hasDiseq = true; } for (euf::snode* d : kv.m_value) { out << "?" << kv.m_key << " ≠ ?" << d->id() << "
"; } @@ -495,6 +519,7 @@ namespace seq { // integer constraints for (auto const& ic : m_constraints) { if (!any) { out << "Cnstr:
"; any = true; } + if (!hasInt) { out << "Int:
"; hasInt = true; } out << constraint_html(ic, names, next_id, m) << "
"; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 9f27d7b85..2ccba32e3 100644 --- a/src/smt/theory_nseq.cpp +++ b/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)) {