From f461369ab8e7cc8a2a598917585d73330da2dbe3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Apr 2026 08:23:26 -0700 Subject: [PATCH] fix tests Signed-off-by: Nikolaj Bjorner --- src/test/nseq_basic.cpp | 3 ++- src/test/seq_nielsen.cpp | 34 +++++++++++++++++++--------------- 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp index 160a7ecd8..499b9951d 100644 --- a/src/test/nseq_basic.cpp +++ b/src/test/nseq_basic.cpp @@ -160,7 +160,8 @@ static void test_nseq_symbol_clash() { // verify conflict explanation returns the equality index smt::enode_pair_vector eqs; sat::literal_vector mem_idx; - ng.test_aux_explain_conflict(eqs, mem_idx); + vector les; + ng.test_aux_explain_conflict(eqs, mem_idx, les); SASSERT(eqs.size() == 1); SASSERT(eqs[0].first == nullptr); SASSERT(mem_idx.empty()); diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index c664f35cc..e46ce4962 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -156,20 +156,20 @@ static void test_nielsen_subst() { euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); seq::dep_tracker dep = nullptr; - seq::nielsen_subst s1(x, a, dep); + seq::nielsen_subst s1(x, a, nullptr, dep); SASSERT(s1.is_eliminating()); // eliminating substitution: x -> empty - seq::nielsen_subst s2(x, e, dep); + seq::nielsen_subst s2(x, e, nullptr, dep); SASSERT(s2.is_eliminating()); // non-eliminating substitution: x -> concat(A, x) euf::snode* ax = sg.mk_concat(a, x); - seq::nielsen_subst s3(x, ax, dep); + seq::nielsen_subst s3(x, ax, nullptr, dep); SASSERT(!s3.is_eliminating()); // eliminating substitution: x -> y (x not in y) - seq::nielsen_subst s4(x, y, dep); + seq::nielsen_subst s4(x, y, nullptr, dep); SASSERT(s4.is_eliminating()); } @@ -242,7 +242,7 @@ static void test_nielsen_edge() { // create edge with substitution x -> A seq::nielsen_edge* edge = ng.mk_edge(parent, child, true); - edge->add_subst(seq::nielsen_subst(x, a, dep)); + edge->add_subst(seq::nielsen_subst(x, a, nullptr, dep)); SASSERT(edge->src() == parent); SASSERT(edge->tgt() == child); @@ -318,7 +318,7 @@ static void test_nielsen_subst_apply() { node->add_str_eq(seq::str_eq(xa, by, dep)); // apply substitution x -> empty - seq::nielsen_subst s(x, e, dep); + seq::nielsen_subst s(x, e, nullptr, dep); node->apply_subst(sg, s); // after x -> empty: lhs should be just A, rhs still concat(B, y) @@ -379,7 +379,7 @@ static void test_nielsen_expansion() { // branch 1: x -> eps (eliminating, progress) euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort()); seq::nielsen_node* child1 = ng.mk_child(root); - seq::nielsen_subst s1(x, e, dep); + seq::nielsen_subst s1(x, e, nullptr, dep); child1->apply_subst(sg, s1); seq::nielsen_edge* edge1 = ng.mk_edge(root, child1, true); edge1->add_subst(s1); @@ -387,7 +387,7 @@ static void test_nielsen_expansion() { // branch 2: x -> Ax (non-eliminating, non-progress) euf::snode* ax = sg.mk_concat(a, x); seq::nielsen_node* child2 = ng.mk_child(root); - seq::nielsen_subst s2(x, ax, dep); + seq::nielsen_subst s2(x, ax, nullptr, dep); child2->apply_subst(sg, s2); seq::nielsen_edge* edge2 = ng.mk_edge(root, child2, false); edge2->add_subst(s2); @@ -1493,7 +1493,8 @@ static void test_explain_conflict_single_eq() { // but the conflict should still be detected svector eqs; svector mem_literals; - ng.test_aux_explain_conflict(eqs, mem_literals); + vector les; + ng.test_aux_explain_conflict(eqs, mem_literals, les); // with test-friendly overload (null deps), eqs will be empty // the important check is that the conflict was detected } @@ -1523,7 +1524,8 @@ static void test_explain_conflict_multi_eq() { // the important check is that the conflict was detected svector eqs; svector mem_literals; - ng.test_aux_explain_conflict(eqs, mem_literals); + vector les; + ng.test_aux_explain_conflict(eqs, mem_literals, les); } // test that is_extended is set after solve generates extensions @@ -2115,7 +2117,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; - ng.test_aux_explain_conflict(eqs, mem_literals); + vector les; + ng.test_aux_explain_conflict(eqs, mem_literals, les); } // test explain_conflict: mixed eq + mem conflict @@ -2149,7 +2152,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; - ng.test_aux_explain_conflict(eqs, mem_literals); + vector les; + ng.test_aux_explain_conflict(eqs, mem_literals, les); } // test subsumption pruning during solve: a node whose constraint set @@ -3471,7 +3475,7 @@ static void test_subst_does_not_propagate_bounds_single_var() { // apply substitution x → a·y euf::snode* ay = sg.mk_concat(a, y); - seq::nielsen_subst s(x, ay, dep); + seq::nielsen_subst s(x, ay, nullptr, dep); node->apply_subst(sg, s); // No local propagation anymore: y keeps conservative defaults. @@ -3505,7 +3509,7 @@ static void test_subst_no_immediate_bound_conflict() { // apply substitution x → a·b (no eager bound check at this stage) euf::snode* ab = sg.mk_concat(a, b); - seq::nielsen_subst s(x, ab, dep); + seq::nielsen_subst s(x, ab, nullptr, dep); node->apply_subst(sg, s); SASSERT(!node->is_general_conflict()); @@ -3634,7 +3638,7 @@ static void test_subst_does_not_propagate_bounds_multi_var() { // apply substitution x → y·z (two vars, no constants) euf::snode* yz = sg.mk_concat(y, z); - seq::nielsen_subst s(x, yz, dep); + seq::nielsen_subst s(x, yz, nullptr, dep); node->apply_subst(sg, s); SASSERT(queried_ub(node, y) == UINT_MAX);