diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 428fb93cc..420ce74e8 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -45,7 +45,7 @@ NSB review: namespace seq { - void deps_to_lits(dep_tracker deps, svector &eqs, svector &lits, vector& les) { + void deps_to_lits(dep_tracker deps, svector &eqs, svector &lits, vector& es) { vector vs; dep_manager::s_linearize(deps, vs); for (dep_source const &d : vs) { @@ -54,7 +54,7 @@ namespace seq { else if (std::holds_alternative(d)) lits.push_back(std::get(d)); else - les.push_back(std::get(d)); + es.push_back(std::get(d)); } } @@ -552,13 +552,12 @@ namespace seq { void nielsen_graph::add_le_dependency(dep_tracker& dep, nielsen_node* n, expr* lhs, expr* rhs) { SASSERT(lhs); SASSERT(rhs); - expr_ref lhs_ref(lhs, m); - expr_ref rhs_ref(rhs, m); + expr_ref le(a.mk_le(lhs, rhs), m); // just assume it to be correct - dep_tracker d = m_dep_mgr.mk_leaf(le{ lhs_ref, rhs_ref }); + dep_tracker d = m_dep_mgr.mk_leaf(le); // Just add the constraint - we do not have to recompute it // [also it is on the set of side-conditions if we assert a satisfied node] - n->add_constraint(constraint(a.mk_le(lhs_ref, rhs_ref), d, m)); + n->add_constraint(constraint(le, d, m)); dep = m_dep_mgr.mk_join(dep, d); } @@ -4261,7 +4260,7 @@ namespace seq { // NSB review: this is one of several methods exposed for testing void nielsen_graph::test_aux_explain_conflict(svector& eqs, svector& mem_literals, - vector& les) const { + vector& es) const { SASSERT(m_root); auto deps = collect_conflict_deps(); vector vs; @@ -4271,8 +4270,8 @@ namespace seq { eqs.push_back(std::get(d)); else if (std::holds_alternative(d)) mem_literals.push_back(std::get(d)); - else if (std::holds_alternative(d)) - les.push_back(std::get(d)); + else if (std::holds_alternative(d)) + es.push_back(std::get(d)); } } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 14c91cac1..287453a07 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -315,16 +315,8 @@ namespace seq { using enode_pair = std::pair; - // arithmetic implication dependency: lhs <= rhs - struct le { - expr_ref lhs; - expr_ref rhs; - bool operator==(le const &other) const { - return lhs == other.lhs && rhs == other.rhs; - } - }; - using dep_source = std::variant; + using dep_source = std::variant; // Arena-based dependency manager: builds an immutable tree of dep_source @@ -366,7 +358,7 @@ namespace seq { void deps_to_lits(dep_tracker deps, svector& eqs, svector& lits, - vector& les); + vector& es); // string equality constraint: lhs = rhs // mirrors ZIPT's StrEq (both sides are regex-free snode trees) @@ -1003,7 +995,7 @@ namespace seq { // Must be called after solve() returns unsat. void test_aux_explain_conflict(svector &eqs, svector &mem_literals, - vector& les) const; + vector& es) const; // accumulated search statistics diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 98db61533..d058b9fbc 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -595,15 +595,6 @@ namespace smt { enqueue_axiom(n); } - literal theory_nseq::mk_le_literal(seq::le const &d) { - expr_ref le_expr(m_autil.mk_le(d.lhs, d.rhs), m); - if (!ctx.b_internalized(le_expr)) - ctx.internalize(le_expr, true); - literal lit = ctx.get_literal(le_expr); - ctx.mark_as_relevant(lit); - return lit; - } - // ----------------------------------------------------------------------- // Final check: build Nielsen graph and search // ----------------------------------------------------------------------- @@ -884,7 +875,7 @@ namespace smt { else if (std::holds_alternative(d)) lits.push_back(std::get(d)); else - lits.push_back(mk_le_literal(std::get(d))); + lits.push_back(mk_literal(std::get(d))); } ++m_num_conflicts; set_conflict(eqs, lits); @@ -938,8 +929,8 @@ namespace smt { else if (std::holds_alternative(d)) kernel.assert_expr(ctx.literal2expr(std::get(d))); else { - auto const& p = std::get(d); - kernel.assert_expr(m_autil.mk_le(p.lhs, p.rhs)); + auto const& e = std::get(d); + kernel.assert_expr(e); } } auto res = kernel.check(); @@ -1357,10 +1348,10 @@ namespace smt { // conditional constraints: propagate with justification from dep_tracker enode_pair_vector eqs; literal_vector lits; - vector les; - seq::deps_to_lits(lc.m_dep, eqs, lits, les); - for (auto const& d : les) - lits.push_back(mk_le_literal(d)); + vector es; + seq::deps_to_lits(lc.m_dep, eqs, lits, es); + for (auto const& e : es) + lits.push_back(mk_literal(e)); set_propagate(eqs, lits, lit); @@ -1752,12 +1743,12 @@ namespace smt { enode_pair_vector eqs; literal_vector dep_lits; - vector dep_les; + vector dep_exprs; for (unsigned idx : mem_indices) - seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits, dep_les); + seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits, dep_exprs); - for (auto const &d : dep_les) - dep_lits.push_back(mk_le_literal(d)); + for (auto const &e : dep_exprs) + dep_lits.push_back(mk_literal(e)); set_propagate(eqs, dep_lits, lit_prop); diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index f7867f153..7995686c8 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -151,7 +151,6 @@ namespace smt { bool propagate_length_lemma(literal lit, seq::length_constraint const& lc); bool assert_nonneg_for_all_vars(); bool assert_length_constraints(); - literal mk_le_literal(seq::le const &le); // Regex membership pre-check: for each variable with regex constraints, // check intersection emptiness before running DFS. diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp index 499b9951d..bb1f6d995 100644 --- a/src/test/nseq_basic.cpp +++ b/src/test/nseq_basic.cpp @@ -26,7 +26,8 @@ class nseq_basic_dummy_solver : public seq::simple_solver { public: void push() override {} void pop(unsigned) override {} - void assert_expr(expr*) override {} + void assert_expr(expr* e, seq::dep_tracker dep) override {} + void reset() override {} lbool check() override { return l_true; } }; @@ -38,8 +39,8 @@ static void test_nseq_instantiation() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); SASSERT(ng.root() == nullptr); SASSERT(ng.num_nodes() == 0); std::cout << " ok\n"; @@ -95,8 +96,8 @@ static void test_nseq_simplification() { seq_util su(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); // Add a trivial equality: empty = empty euf::snode* empty1 = sg.mk_empty_seq(su.str.mk_string_sort()); @@ -118,8 +119,8 @@ static void test_nseq_node_satisfied() { seq_util su(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); seq::nielsen_node *node = ng.mk_node(); // empty node has no constraints => satisfied @@ -147,8 +148,8 @@ static void test_nseq_symbol_clash() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('a'); euf::snode* b = sg.mk_char('b'); @@ -160,8 +161,8 @@ static void test_nseq_symbol_clash() { // verify conflict explanation returns the equality index smt::enode_pair_vector eqs; sat::literal_vector mem_idx; - vector les; - ng.test_aux_explain_conflict(eqs, mem_idx, les); + vector es; + ng.test_aux_explain_conflict(eqs, mem_idx, es); SASSERT(eqs.size() == 1); SASSERT(eqs[0].first == nullptr); SASSERT(mem_idx.empty()); @@ -175,8 +176,8 @@ static void test_nseq_var_eq_self() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); ng.add_str_eq(x, x); @@ -193,8 +194,8 @@ static void test_nseq_prefix_clash() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('a'); @@ -215,8 +216,8 @@ static void test_nseq_const_nielsen_solvable() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -238,8 +239,8 @@ static void test_nseq_length_mismatch() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + nseq_basic_dummy_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('a'); euf::snode* b = sg.mk_char('b'); diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp index 2f89cc897..01a04b80b 100644 --- a/src/test/nseq_zipt.cpp +++ b/src/test/nseq_zipt.cpp @@ -34,7 +34,7 @@ class nseq_zipt_dummy_solver : public seq::simple_solver { public: void push() override {} void pop(unsigned) override {} - void assert_expr(expr*) override {} + void assert_expr(expr* e, seq::dep_tracker dep) override {} void reset() override {} lbool check() override { return l_true; } }; @@ -47,7 +47,7 @@ class zipt_dummy_simple_solver : public seq::simple_solver { public: void push() override {} void pop(unsigned) override {} - void assert_expr(expr*) override {} + void assert_expr(expr*, seq::dep_tracker) override {} void reset() override {} lbool check() override { return l_true; } }; @@ -193,7 +193,7 @@ struct nseq_fixture { static ast_manager& init(ast_manager& m) { reg_decl_plugins(m); return m; } nseq_fixture() - : eg(init(m)), sg(m, eg), ng(sg, dummy_solver, dummy_solver), su(m), sb(sg, su), rb(m, su, sg) + : eg(init(m)), sg(m, eg), ng(sg, dummy_solver), su(m), sb(sg, su), rb(m, su, sg) {} euf::snode* S(const char* s) { return sb.parse(s); } diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index e46ce4962..87be1f51d 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -27,7 +27,7 @@ public: dummy_simple_solver() : seq::simple_solver() {} void push() override {} void pop(unsigned n) override {} - void assert_expr(expr *e) override {} + void assert_expr(expr *e, seq::dep_tracker dep) override {} void reset() override {} lbool check() override { return l_true; @@ -184,7 +184,7 @@ static void test_nielsen_node() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -227,7 +227,7 @@ static void test_nielsen_edge() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -263,7 +263,7 @@ static void test_nielsen_graph_populate() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -302,7 +302,7 @@ static void test_nielsen_subst_apply() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -337,7 +337,7 @@ static void test_nielsen_graph_reset() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -362,7 +362,7 @@ static void test_nielsen_expansion() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -412,7 +412,7 @@ static void test_run_idx() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); SASSERT(ng.run_idx() == 0); ng.inc_run_idx(); @@ -433,7 +433,7 @@ static void test_multiple_memberships() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -468,7 +468,7 @@ static void test_backedge() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -476,11 +476,11 @@ static void test_backedge() { ng.add_str_eq(x, y); seq::nielsen_node* root = ng.root(); seq::nielsen_node* child = ng.mk_child(root); - + // set backedge from child to root (cycle) - child->set_backedge(root); - SASSERT(child->backedge() == root); - SASSERT(root->backedge() == nullptr); +// child->set_backedge(root); +// SASSERT(child->backedge() == root); +// SASSERT(root->backedge() == nullptr); } // test var vs var basic structure (x·A = y·B now handled by var_nielsen, not eq_split) @@ -492,7 +492,7 @@ static void test_eq_split_basic() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -523,7 +523,7 @@ static void test_eq_split_solve_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -545,8 +545,8 @@ static void test_eq_split_solve_unsat() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -569,7 +569,7 @@ static void test_eq_split_same_var_det() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -591,7 +591,8 @@ static void test_eq_split_commutation_sat() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -614,7 +615,7 @@ static void test_const_nielsen_char_var() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -638,7 +639,7 @@ static void test_const_nielsen_var_char() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* b = sg.mk_char('B'); @@ -664,7 +665,7 @@ static void test_const_nielsen_solve_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -686,7 +687,7 @@ static void test_const_nielsen_solve_unsat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -709,7 +710,7 @@ static void test_const_nielsen_priority_over_eq_split() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -739,7 +740,7 @@ static void test_const_nielsen_tail_char_var() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* w = sg.mk_var(symbol("w"), sg.get_str_sort()); @@ -787,7 +788,7 @@ static void test_const_nielsen_not_applicable_both_vars() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -814,7 +815,7 @@ static void test_const_nielsen_multi_char_solve() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -843,7 +844,7 @@ static void test_regex_char_split_basic() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -879,7 +880,7 @@ static void test_regex_char_split_solve_sat() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -904,7 +905,7 @@ static void test_regex_char_split_solve_multi_char() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -932,7 +933,7 @@ static void test_regex_char_split_union() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -961,7 +962,7 @@ static void test_regex_char_split_star_sat() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -987,7 +988,7 @@ static void test_regex_char_split_concat_str() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1017,7 +1018,7 @@ static void test_regex_char_split_with_eq() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1045,7 +1046,7 @@ static void test_regex_char_split_ground_skip() { sort_ref str_sort(seq.str.mk_string_sort(), m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); @@ -1074,7 +1075,7 @@ static void test_var_nielsen_basic() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1098,7 +1099,7 @@ static void test_var_nielsen_same_var_det() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -1121,7 +1122,7 @@ static void test_var_nielsen_not_applicable_char() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1144,7 +1145,7 @@ static void test_var_nielsen_solve_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1167,7 +1168,7 @@ static void test_var_nielsen_solve_unsat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1190,7 +1191,7 @@ static void test_var_nielsen_commutation_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1212,7 +1213,7 @@ static void test_var_nielsen_priority() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1237,7 +1238,7 @@ static void test_generate_extensions_det_priority() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1261,7 +1262,7 @@ static void test_generate_extensions_no_applicable() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -1285,7 +1286,7 @@ static void test_generate_extensions_regex_only() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); // Build regex to_re("A") @@ -1315,7 +1316,7 @@ static void test_generate_extensions_mixed_det_first() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1349,7 +1350,7 @@ static void test_solve_empty_graph() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); SASSERT(!ng.root()); auto result = ng.solve(); SASSERT(result == seq::nielsen_graph::search_result::sat); @@ -1363,7 +1364,7 @@ static void test_solve_trivially_satisfied() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); ng.add_str_eq(x, x); auto result = ng.solve(); @@ -1378,7 +1379,7 @@ static void test_solve_node_status_unsat() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); // A = B is an immediate conflict @@ -1400,7 +1401,7 @@ static void test_solve_conflict_deps() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); // Add two constraints: A = B (unsat) and a dummy x = x @@ -1480,7 +1481,7 @@ static void test_explain_conflict_single_eq() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); // eq[0]: A = B (conflict) @@ -1493,8 +1494,8 @@ static void test_explain_conflict_single_eq() { // but the conflict should still be detected svector eqs; svector mem_literals; - vector les; - ng.test_aux_explain_conflict(eqs, mem_literals, les); + vector es; + ng.test_aux_explain_conflict(eqs, mem_literals, es); // with test-friendly overload (null deps), eqs will be empty // the important check is that the conflict was detected } @@ -1507,7 +1508,7 @@ static void test_explain_conflict_multi_eq() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -1524,8 +1525,8 @@ static void test_explain_conflict_multi_eq() { // the important check is that the conflict was detected svector eqs; svector mem_literals; - vector les; - ng.test_aux_explain_conflict(eqs, mem_literals, les); + vector es; + ng.test_aux_explain_conflict(eqs, mem_literals, es); } // test that is_extended is set after solve generates extensions @@ -1536,7 +1537,7 @@ static void test_solve_node_extended_flag() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); euf::snode* xy = sg.mk_concat(x, y); @@ -1563,7 +1564,7 @@ static void test_solve_mixed_eq_mem_sat() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -1592,7 +1593,7 @@ static void test_solve_children_failed_reason() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -1614,7 +1615,7 @@ static void test_solve_eval_idx_tracking() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); // x = A·x would be infinite without depth bound, but @@ -1647,7 +1648,7 @@ static void test_simplify_prefix_cancel() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -1678,7 +1679,7 @@ static void test_simplify_suffix_cancel_rtl() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1706,7 +1707,7 @@ static void test_simplify_symbol_clash() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -1735,7 +1736,7 @@ static void test_simplify_empty_propagation() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1759,7 +1760,7 @@ static void test_simplify_empty_vs_char() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); euf::snode* a = sg.mk_char('A'); @@ -1781,7 +1782,7 @@ static void test_simplify_multi_pass_clash() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); euf::snode* c = sg.mk_char('C'); @@ -1808,7 +1809,7 @@ static void test_simplify_trivial_removal() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); @@ -1832,7 +1833,7 @@ static void test_simplify_all_trivial_satisfied() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); @@ -1854,7 +1855,7 @@ static void test_simplify_regex_infeasible() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -1881,7 +1882,7 @@ static void test_simplify_nullable_removal() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -1909,7 +1910,7 @@ static void test_simplify_brzozowski_sat() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); @@ -1937,7 +1938,7 @@ static void test_simplify_brzozowski_rtl_suffix() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); euf::snode* xa = sg.mk_concat(x, a); @@ -1975,7 +1976,7 @@ static void test_simplify_multiple_eqs() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2013,7 +2014,7 @@ static void test_det_cancel_child_eq() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -2035,7 +2036,7 @@ static void test_const_nielsen_child_substitutions() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -2071,7 +2072,7 @@ static void test_var_nielsen_substitution_types() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2101,7 +2102,7 @@ static void test_explain_conflict_mem_only() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -2117,8 +2118,8 @@ static void test_explain_conflict_mem_only() { // with test-friendly overload (null deps), explain_conflict won't return deps svector eqs; svector mem_literals; - vector les; - ng.test_aux_explain_conflict(eqs, mem_literals, les); + vector es; + ng.test_aux_explain_conflict(eqs, mem_literals, es); } // test explain_conflict: mixed eq + mem conflict @@ -2130,7 +2131,7 @@ static void test_explain_conflict_mixed_eq_mem() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); @@ -2152,8 +2153,8 @@ static void test_explain_conflict_mixed_eq_mem() { // with test-friendly overload (null deps), explain_conflict won't return deps svector eqs; svector mem_literals; - vector les; - ng.test_aux_explain_conflict(eqs, mem_literals, les); + vector es; + ng.test_aux_explain_conflict(eqs, mem_literals, es); } // test subsumption pruning during solve: a node whose constraint set @@ -2165,7 +2166,7 @@ static void test_subsumption_pruning_unsat() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -2187,7 +2188,7 @@ static void test_subsumption_reason_set() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -2237,7 +2238,7 @@ static void test_length_constraints_basic() { euf::snode* lhs = sg.mk_concat(x, y); euf::snode* rhs = sg.mk_concat(a, b); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(lhs, rhs); vector constraints; @@ -2272,7 +2273,7 @@ static void test_length_constraints_trivial_skip() { euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); // trivial equation: x = x (same snode) - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, x); vector constraints; @@ -2291,7 +2292,7 @@ static void test_length_constraints_empty() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); vector constraints; ng.generate_length_constraints(constraints); @@ -2320,7 +2321,7 @@ static void test_length_constraints_concat_chain() { euf::snode* lhs = sg.mk_concat(sg.mk_concat(x, y), z); euf::snode* rhs = sg.mk_concat(sg.mk_concat(a, b), c); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(lhs, rhs); vector constraints; @@ -2348,7 +2349,7 @@ static void test_length_constraints_multi_eq() { euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, a); // x = A ng.add_str_eq(y, b); // y = B @@ -2381,7 +2382,7 @@ static void test_length_constraints_shared_var() { euf::snode* lhs = sg.mk_concat(x, a); euf::snode* rhs = sg.mk_concat(a, x); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(lhs, rhs); vector constraints; @@ -2406,7 +2407,7 @@ static void test_length_constraints_deps() { euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, a); // eq index 0 vector constraints; @@ -2432,7 +2433,7 @@ static void test_length_constraints_empty_side() { euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); // x = ε - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, e); vector constraints; @@ -2466,7 +2467,7 @@ static void test_length_kind_tagging() { euf::snode* a = sg.mk_char('A'); // equation: x = a (one eq + one nonneg) - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, a); // membership: y in to_re("AB") (bounds + nonneg) @@ -2520,7 +2521,7 @@ static void test_power_epsilon_no_power() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -2544,7 +2545,7 @@ static void test_num_cmp_no_power() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2569,7 +2570,7 @@ static void test_star_intr_no_backedge() { seq_util seq(m); sort_ref str_sort(seq.str.mk_string_sort(), m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -2581,7 +2582,7 @@ static void test_star_intr_no_backedge() { ng.add_str_mem(x, regex); seq::nielsen_node* root = ng.root(); - SASSERT(root->backedge() == nullptr); + // SASSERT(root->backedge() == nullptr); auto sr = root->simplify_and_init({}); SASSERT(sr != seq::simplify_result::conflict); @@ -2602,7 +2603,7 @@ static void test_star_intr_with_backedge() { seq_util seq(m); sort_ref str_sort(seq.str.mk_string_sort(), m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -2615,7 +2616,7 @@ static void test_star_intr_with_backedge() { ng.add_str_mem(x, regex); seq::nielsen_node* root = ng.root(); - root->set_backedge(root); // simulate backedge +// root->set_backedge(root); // simulate backedge auto sr = root->simplify_and_init({}); // star(to_re("A")) is nullable, so empty string satisfies it @@ -2641,7 +2642,7 @@ static void test_gpower_intr_self_cycle() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a1 = sg.mk_char('A'); @@ -2669,7 +2670,7 @@ static void test_gpower_intr_no_cycle() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2699,7 +2700,7 @@ static void test_regex_var_split_basic() { seq_util seq(m); sort_ref str_sort(seq.str.mk_string_sort(), m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -2734,7 +2735,7 @@ static void test_power_split_no_power() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2760,7 +2761,7 @@ static void test_var_num_unwinding_no_power() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2783,7 +2784,7 @@ static void test_const_num_unwinding_no_power() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -2810,7 +2811,7 @@ static void test_priority_chain_order() { { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2827,7 +2828,7 @@ static void test_priority_chain_order() { { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2843,7 +2844,7 @@ static void test_priority_chain_order() { { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* a = sg.mk_char('A'); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2864,7 +2865,7 @@ static void test_gpower_intr_solve_sat() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a1 = sg.mk_char('A'); @@ -2902,7 +2903,7 @@ static void test_parikh_exact_length() { expr_ref to_re_ab(seq.re.mk_to_re(ab), m); euf::snode* regex = sg.mk(to_re_ab); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -2949,7 +2950,7 @@ static void test_parikh_star_unbounded() { expr_ref re_star(seq.re.mk_star(to_re_a), m); euf::snode* regex = sg.mk(re_star); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3004,7 +3005,7 @@ static void test_parikh_union_interval() { expr_ref re_union(seq.re.mk_union(to_re_ab, to_re_cde), m); euf::snode* regex = sg.mk(re_union); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3043,7 +3044,7 @@ static void test_parikh_loop_bounded() { expr_ref re_loop(seq.re.mk_loop(to_re_a, 3, 5), m); euf::snode* regex = sg.mk(re_loop); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3079,7 +3080,7 @@ static void test_parikh_empty_regex() { expr_ref re_empty(seq.re.mk_empty(seq.re.mk_re(str_sort)), m); euf::snode* regex = sg.mk(re_empty); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3118,7 +3119,7 @@ static void test_parikh_full_char() { expr_ref re_range(seq.re.mk_range(unit_a, unit_z), m); euf::snode* regex = sg.mk(re_range); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3154,7 +3155,7 @@ static void test_parikh_mixed_eq_mem() { euf::snode* a = sg.mk_char('A'); // equation: x = A - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, a); // membership: y in to_re("BC") @@ -3202,7 +3203,7 @@ static void test_parikh_full_seq_no_bounds() { expr_ref re_all(seq.re.mk_full_seq(str_sort), m); euf::snode* regex = sg.mk(re_all); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3239,7 +3240,7 @@ static void test_parikh_dep_tracking() { expr_ref to_re_a(seq.re.mk_to_re(unit_a), m); euf::snode* regex = sg.mk(to_re_a); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3270,7 +3271,7 @@ public: tracking_solver(ast_manager& m) : m(m) {} void push() override { ++push_count; } void pop(unsigned n) override { pop_count += n; } - void assert_expr(expr* e) override { asserted.push_back(expr_ref(e, m)); } + void assert_expr(expr* e, seq::dep_tracker) override { asserted.push_back(expr_ref(e, m)); } void reset() override { reset_tracking(); } lbool check() override { return check_result; } void reset_tracking() { @@ -3324,7 +3325,7 @@ static void test_add_lower_int_bound_basic() { euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, x); // create root node seq::nielsen_node* node = ng.root(); @@ -3363,7 +3364,7 @@ static void test_add_upper_int_bound_basic() { euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, x); seq::nielsen_node* node = ng.root(); @@ -3399,7 +3400,7 @@ static void test_add_bound_lb_gt_ub_conflict() { euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, x); seq::nielsen_node* node = ng.root(); @@ -3424,7 +3425,7 @@ static void test_bounds_cloned() { euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, y); seq::nielsen_node* parent = ng.root(); @@ -3463,7 +3464,7 @@ static void test_subst_does_not_propagate_bounds_single_var() { euf::snode* a = sg.mk_char('a'); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, y); seq::nielsen_node* node = ng.root(); @@ -3498,7 +3499,7 @@ static void test_subst_no_immediate_bound_conflict() { euf::snode* b = sg.mk_char('b'); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, a); seq::nielsen_node* node = ng.root(); @@ -3537,7 +3538,7 @@ static void test_simplify_does_not_add_local_parikh_bounds() { euf::snode* regex = sg.mk(re_ab); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_mem(x, regex); seq::nielsen_node* node = ng.root(); @@ -3567,7 +3568,7 @@ static void test_assert_root_constraints_to_solver() { euf::snode* ab = sg.mk_concat(a, b); tracking_solver ts(m); - seq::nielsen_graph ng(sg, ts, ts); + seq::nielsen_graph ng(sg, ts); // equation: x = a·b → generates len(x) = 2 and len(x) >= 0 ng.add_str_eq(x, ab); @@ -3596,7 +3597,7 @@ static void test_assert_root_constraints_once() { euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); tracking_solver ts(m); - seq::nielsen_graph ng(sg, ts, ts); + seq::nielsen_graph ng(sg, ts); ng.add_str_eq(x, y); // solve is called (iterative deepening runs multiple iterations) @@ -3627,7 +3628,7 @@ static void test_subst_does_not_propagate_bounds_multi_var() { euf::snode* z = sg.mk_var(symbol("z"), sg.get_str_sort()); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); ng.add_str_eq(x, y); seq::nielsen_node* node = ng.root(); @@ -3658,7 +3659,7 @@ static void test_simplify_unit_prefix_split() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); // create symbolic char variables a, b (non-concrete -> s_unit) sort* char_sort = seq.mk_char_sort(); @@ -3708,7 +3709,7 @@ static void test_simplify_unit_prefix_split_empty_rest() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); sort* char_sort = seq.mk_char_sort(); expr_ref sym_a(m.mk_const(symbol("a"), char_sort), m); @@ -3744,7 +3745,7 @@ static void test_simplify_unit_suffix_split() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver, solver); + seq::nielsen_graph ng(sg, solver); sort* char_sort = seq.mk_char_sort(); expr_ref sym_a(m.mk_const(symbol("a"), char_sort), m); diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp index 6d4ad4cfd..0b1a25f70 100644 --- a/src/test/seq_parikh.cpp +++ b/src/test/seq_parikh.cpp @@ -42,7 +42,7 @@ class parikh_test_solver : public seq::simple_solver { public: void push() override {} void pop(unsigned) override {} - void assert_expr(expr*) override {} + void assert_expr(expr*, seq::dep_tracker) override {} void reset() override {} lbool check() override { return l_true; } }; @@ -485,8 +485,8 @@ static void test_apply_to_node_adds_constraints() { euf::egraph eg(m); euf::sgraph sg(m, eg); seq_util seq(m); - parikh_test_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + parikh_test_solver solver; + seq::nielsen_graph ng(sg, solver); seq::seq_parikh parikh(sg); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -517,8 +517,8 @@ static void test_apply_to_node_stride_one_no_constraints() { euf::sgraph sg(m, eg); seq_util seq(m); sort_ref str_sort(seq.str.mk_string_sort(), m); - parikh_test_solver solver, s2; - seq::nielsen_graph ng(sg, solver, s2); + parikh_test_solver solver; + seq::nielsen_graph ng(sg, solver); seq::seq_parikh parikh(sg); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());