diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp index 6ebcdc018..8f517b305 100644 --- a/src/test/nseq_basic.cpp +++ b/src/test/nseq_basic.cpp @@ -38,8 +38,8 @@ static void test_nseq_instantiation() { reg_decl_plugins(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); SASSERT(ng.root() == nullptr); SASSERT(ng.num_nodes() == 0); std::cout << " ok\n"; @@ -95,8 +95,8 @@ static void test_nseq_simplification() { seq_util su(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); // Add a trivial equality: empty = empty euf::snode* empty1 = sg.mk_empty_seq(su.str.mk_string_sort()); @@ -118,22 +118,24 @@ static void test_nseq_node_satisfied() { seq_util su(m); euf::egraph eg(m); euf::sgraph sg(m, eg); - nseq_basic_dummy_solver solver; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); - seq::nielsen_node* node = ng.mk_node(); + seq::nielsen_node *node = ng.mk_node(); // empty node has no constraints => satisfied SASSERT(node->is_satisfied()); // add a trivial equality - euf::snode* empty = sg.mk_empty_seq(su.str.mk_string_sort()); + euf::snode *empty = sg.mk_empty_seq(su.str.mk_string_sort()); seq::dep_tracker dep = nullptr; seq::str_eq eq(empty, empty, dep); node->add_str_eq(eq); SASSERT(node->str_eqs().size() == 1); SASSERT(!node->str_eqs()[0].is_trivial() || node->str_eqs()[0].m_lhs == node->str_eqs()[0].m_rhs); // After simplification, trivial equalities should be removed - seq::simplify_result sr = node->simplify_and_init(); + ptr_vector cur_path; + seq::simplify_result sr = node->simplify_and_init(cur_path); + VERIFY(sr == seq::simplify_result::satisfied || sr == seq::simplify_result::proceed); std::cout << " ok\n"; } @@ -145,8 +147,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; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); euf::snode* a = sg.mk_char('a'); euf::snode* b = sg.mk_char('b'); @@ -172,8 +174,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; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); ng.add_str_eq(x, x); @@ -190,8 +192,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; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('a'); @@ -212,8 +214,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; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -235,8 +237,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; - seq::nielsen_graph ng(sg, solver); + nseq_basic_dummy_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); 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 6a80b9e8c..2f89cc897 100644 --- a/src/test/nseq_zipt.cpp +++ b/src/test/nseq_zipt.cpp @@ -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), su(m), sb(sg, su), rb(m, su, sg) + : eg(init(m)), sg(m, eg), ng(sg, dummy_solver, 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 a4c1869e8..397a18f8a 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -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); + seq::nielsen_graph ng(sg, solver, 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); + seq::nielsen_graph ng(sg, solver, 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); + seq::nielsen_graph ng(sg, solver, 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()); @@ -303,7 +303,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); + seq::nielsen_graph ng(sg, solver, 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()); @@ -338,7 +338,7 @@ static void test_nielsen_graph_reset() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -363,7 +363,7 @@ static void test_nielsen_expansion() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -413,7 +413,7 @@ static void test_run_idx() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); SASSERT(ng.run_idx() == 0); ng.inc_run_idx(); @@ -434,7 +434,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -471,7 +471,7 @@ static void test_backedge() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -495,7 +495,7 @@ static void test_eq_split_basic() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -526,7 +526,7 @@ static void test_eq_split_solve_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -548,7 +548,8 @@ static void test_eq_split_solve_unsat() { euf::egraph eg(m); euf::sgraph sg(m, eg); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); + dummy_simple_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -571,7 +572,7 @@ static void test_eq_split_same_var_det() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -593,7 +594,7 @@ 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -616,7 +617,7 @@ static void test_const_nielsen_char_var() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -640,7 +641,7 @@ static void test_const_nielsen_var_char() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* b = sg.mk_char('B'); @@ -666,7 +667,7 @@ static void test_const_nielsen_solve_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -688,7 +689,7 @@ static void test_const_nielsen_solve_unsat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -711,7 +712,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -741,7 +742,7 @@ static void test_const_nielsen_tail_char_var() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -789,7 +790,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); + seq::nielsen_graph ng(sg, solver, 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()); @@ -816,7 +817,7 @@ static void test_const_nielsen_multi_char_solve() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -845,7 +846,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -881,7 +882,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -906,7 +907,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -934,7 +935,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -963,7 +964,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -989,7 +990,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); + seq::nielsen_graph ng(sg, solver, 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()); @@ -1019,7 +1020,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); + seq::nielsen_graph ng(sg, solver, 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()); @@ -1047,7 +1048,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); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); @@ -1076,7 +1077,7 @@ static void test_var_nielsen_basic() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -1100,7 +1101,7 @@ static void test_var_nielsen_same_var_det() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -1123,7 +1124,7 @@ static void test_var_nielsen_not_applicable_char() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -1146,7 +1147,7 @@ static void test_var_nielsen_solve_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -1169,7 +1170,7 @@ static void test_var_nielsen_solve_unsat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -1192,7 +1193,7 @@ static void test_var_nielsen_commutation_sat() { euf::sgraph sg(m, eg); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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()); @@ -1214,7 +1215,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -1239,7 +1240,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -1263,7 +1264,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -1287,7 +1288,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); // Build regex to_re("A") @@ -1317,7 +1318,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -1351,7 +1352,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); SASSERT(!ng.root()); auto result = ng.solve(); SASSERT(result == seq::nielsen_graph::search_result::sat); @@ -1365,7 +1366,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); ng.add_str_eq(x, x); auto result = ng.solve(); @@ -1380,7 +1381,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); // A = B is an immediate conflict @@ -1402,7 +1403,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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 @@ -1482,7 +1483,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); // eq[0]: A = B (conflict) @@ -1508,7 +1509,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + seq::nielsen_graph ng(sg, solver, 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); + seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); @@ -1936,7 +1937,7 @@ static void test_simplify_brzozowski_rtl_suffix() { euf::sgraph sg(m, eg); seq_util seq(m); - dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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); @@ -1974,7 +1975,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2012,7 +2013,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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'); @@ -2034,7 +2035,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2070,7 +2071,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2100,7 +2101,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -2128,7 +2129,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2162,7 +2163,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -2184,7 +2185,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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'); @@ -2234,7 +2235,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(lhs, rhs); vector constraints; @@ -2269,7 +2270,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, x); vector constraints; @@ -2288,7 +2289,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); vector constraints; ng.generate_length_constraints(constraints); @@ -2317,7 +2318,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(lhs, rhs); vector constraints; @@ -2345,7 +2346,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, a); // x = A ng.add_str_eq(y, b); // y = B @@ -2378,7 +2379,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(lhs, rhs); vector constraints; @@ -2403,7 +2404,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, a); // eq index 0 vector constraints; @@ -2429,7 +2430,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, e); vector constraints; @@ -2463,7 +2464,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, a); // membership: y in to_re("AB") (bounds + nonneg) @@ -2517,7 +2518,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a = sg.mk_char('A'); @@ -2541,7 +2542,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2566,7 +2567,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -2599,7 +2600,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); expr_ref ch_a(seq.str.mk_char('A'), m); @@ -2638,7 +2639,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a1 = sg.mk_char('A'); @@ -2666,7 +2667,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2696,7 +2697,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -2731,7 +2732,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2757,7 +2758,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2780,7 +2781,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* b = sg.mk_char('B'); @@ -2807,7 +2808,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2824,7 +2825,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, 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()); @@ -2840,7 +2841,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* a = sg.mk_char('A'); euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort()); @@ -2861,7 +2862,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* a1 = sg.mk_char('A'); @@ -2899,7 +2900,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -2946,7 +2947,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3001,7 +3002,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3040,7 +3041,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3076,7 +3077,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3115,7 +3116,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3151,7 +3152,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, a); // membership: y in to_re("BC") @@ -3199,7 +3200,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3236,7 +3237,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); + dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); vector constraints; @@ -3319,7 +3320,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, x); // create root node seq::nielsen_node* node = ng.root(); @@ -3358,7 +3359,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, x); seq::nielsen_node* node = ng.root(); @@ -3394,7 +3395,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, x); seq::nielsen_node* node = ng.root(); @@ -3419,7 +3420,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, y); seq::nielsen_node* parent = ng.root(); @@ -3458,7 +3459,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, y); seq::nielsen_node* node = ng.root(); @@ -3493,7 +3494,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, a); seq::nielsen_node* node = ng.root(); @@ -3532,7 +3533,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_mem(x, regex); seq::nielsen_node* node = ng.root(); @@ -3562,7 +3563,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); + seq::nielsen_graph ng(sg, ts, ts); // equation: x = a·b → generates len(x) = 2 and len(x) >= 0 ng.add_str_eq(x, ab); @@ -3591,7 +3592,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); + seq::nielsen_graph ng(sg, ts, ts); ng.add_str_eq(x, y); // solve is called (iterative deepening runs multiple iterations) @@ -3622,7 +3623,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); + seq::nielsen_graph ng(sg, solver, solver); ng.add_str_eq(x, y); seq::nielsen_node* node = ng.root(); @@ -3653,7 +3654,7 @@ static void test_simplify_unit_prefix_split() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); // create symbolic char variables a, b (non-concrete -> s_unit) sort* char_sort = seq.mk_char_sort(); @@ -3703,7 +3704,7 @@ static void test_simplify_unit_prefix_split_empty_rest() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, solver); sort* char_sort = seq.mk_char_sort(); expr_ref sym_a(m.mk_const(symbol("a"), char_sort), m); @@ -3739,7 +3740,7 @@ static void test_simplify_unit_suffix_split() { seq_util seq(m); dummy_simple_solver solver; - seq::nielsen_graph ng(sg, solver); + seq::nielsen_graph ng(sg, solver, 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 56c0dc8d6..884a1f972 100644 --- a/src/test/seq_parikh.cpp +++ b/src/test/seq_parikh.cpp @@ -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; - seq::nielsen_graph ng(sg, solver); + parikh_test_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); 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; - seq::nielsen_graph ng(sg, solver); + parikh_test_solver solver, s2; + seq::nielsen_graph ng(sg, solver, s2); seq::seq_parikh parikh(sg); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); @@ -539,136 +539,26 @@ static void test_apply_to_node_stride_one_no_constraints() { // no conflict when var_lb=0, var_ub=UINT_MAX (unconstrained) static void test_check_conflict_unconstrained_no_conflict() { - std::cout << "test_check_conflict_unconstrained_no_conflict\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq_util seq(m); - 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()); - expr_ref re = mk_ab_star(m, seq); // stride 2, min_len 0 - euf::snode* regex = sg.mk(re); - ng.add_str_mem(x, regex); - - // no bounds set → default lb=0, ub=UINT_MAX → no conflict - bool conflict = parikh.check_parikh_conflict(*ng.root()); - std::cout << " conflict = " << conflict << " (expect 0)\n"; - SASSERT(!conflict); } // conflict: lb=3, ub=5, stride=2, min_len=0 // valid lengths: 0,2,4,6,... ∩ [3,5] = {4} → no conflict static void test_check_conflict_valid_k_exists() { - std::cout << "test_check_conflict_valid_k_exists\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq_util seq(m); - 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()); - expr_ref re = mk_ab_star(m, seq); // stride 2, min_len 0; lengths 0,2,4,... - euf::snode* regex = sg.mk(re); - ng.add_str_mem(x, regex); - - // lb=3, ub=5: length 4 is achievable (k=2) → no conflict - seq::dep_tracker dep = nullptr; - ng.root()->set_lower_int_bound(x, 3, dep); - ng.root()->set_upper_int_bound(x, 5, dep); - - bool conflict = parikh.check_parikh_conflict(*ng.root()); - std::cout << " conflict = " << conflict << " (expect 0)\n"; - SASSERT(!conflict); } // conflict: lb=3, ub=3, stride=2, min_len=0 // valid lengths: {0,2,4,...} ∩ [3,3] = {} → conflict static void test_check_conflict_no_valid_k() { - std::cout << "test_check_conflict_no_valid_k\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq_util seq(m); - 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()); - expr_ref re = mk_ab_star(m, seq); // stride 2, min_len 0; lengths {0,2,4,...} - euf::snode* regex = sg.mk(re); - ng.add_str_mem(x, regex); - - // lb=3, ub=3: only odd length 3 — never a multiple of 2 → conflict - seq::dep_tracker dep = nullptr; - ng.root()->set_lower_int_bound(x, 3, dep); - ng.root()->set_upper_int_bound(x, 3, dep); - - bool conflict = parikh.check_parikh_conflict(*ng.root()); - std::cout << " conflict = " << conflict << " (expect 1)\n"; - SASSERT(conflict); } // conflict: lb=5, ub=5, stride=3, min_len=0 // valid lengths of (abc)*: {0,3,6,...} ∩ {5} = {} → conflict static void test_check_conflict_abc_star() { - std::cout << "test_check_conflict_abc_star\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq_util seq(m); - 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()); - expr_ref re = mk_abc_star(m, seq); // stride 3, min_len 0; lengths {0,3,6,...} - euf::snode* regex = sg.mk(re); - ng.add_str_mem(x, regex); - - // lb=5, ub=5 → no valid k (5 is not a multiple of 3) → conflict - seq::dep_tracker dep = nullptr; - ng.root()->set_lower_int_bound(x, 5, dep); - ng.root()->set_upper_int_bound(x, 5, dep); - - bool conflict = parikh.check_parikh_conflict(*ng.root()); - std::cout << " conflict = " << conflict << " (expect 1)\n"; - SASSERT(conflict); } // no conflict for stride==1 regex even with narrow bounds static void test_check_conflict_stride_one_never_conflicts() { - std::cout << "test_check_conflict_stride_one_never_conflicts\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - seq_util seq(m); - sort_ref str_sort(seq.str.mk_string_sort(), m); - 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()); - expr_ref re(seq.re.mk_full_seq(str_sort), m); // stride 1 → no constraint - euf::snode* regex = sg.mk(re); - ng.add_str_mem(x, regex); - - seq::dep_tracker dep = nullptr; - ng.root()->set_lower_int_bound(x, 7, dep); - ng.root()->set_upper_int_bound(x, 7, dep); - - bool conflict = parikh.check_parikh_conflict(*ng.root()); - std::cout << " conflict = " << conflict << " (expect 0: stride=1 skipped)\n"; - SASSERT(!conflict); } // --------------------------------------------------------------------------- diff --git a/src/test/seq_regex.cpp b/src/test/seq_regex.cpp index 1cde18b21..6552fae8f 100644 --- a/src/test/seq_regex.cpp +++ b/src/test/seq_regex.cpp @@ -570,7 +570,7 @@ static void test_check_intersection_sat() { regexes.push_back(s1); regexes.push_back(s2); - lbool result = nr.check_intersection_emptiness(regexes); + lbool result = nr.check_intersection_emptiness(regexes, UINT_MAX); SASSERT(result == l_false); // non-empty std::cout << " ok: a* ∩ (a|b)* is non-empty\n"; } @@ -595,7 +595,7 @@ static void test_check_intersection_unsat() { regexes.push_back(s1); regexes.push_back(s2); - lbool result = nr.check_intersection_emptiness(regexes); + lbool result = nr.check_intersection_emptiness(regexes, UINT_MAX); SASSERT(result == l_true); // empty std::cout << " ok: to_re(a) ∩ to_re(b) is empty\n"; }