diff --git a/src/test/slicing.cpp b/src/test/slicing.cpp index b8cf02a32..ee5d3c3ca 100644 --- a/src/test/slicing.cpp +++ b/src/test/slicing.cpp @@ -55,6 +55,32 @@ namespace polysat { // x = y // y[5:0] = b static void test2() { + std::cout << __func__ << "\n"; + scoped_solver_slicing s; + slicing& sl = s.sl(); + pvar x = s.add_var(8); + pvar y = s.add_var(8); + pvar a = s.add_var(5); + pvar b = s.add_var(6); + + slicing::slice_vector x_7_3; + sl.mk_slice(sl.var2slice(x), 7, 3, x_7_3); + slicing::slice_vector a_4_0; + sl.mk_slice(sl.var2slice(a), 4, 0, a_4_0); + sl.merge(x_7_3, a_4_0); + std::cout << sl << "\n"; + + slicing::slice_vector x_base; + sl.find_base(sl.var2slice(x), x_base); + slicing::slice_vector y_base; + sl.find_base(sl.var2slice(y), y_base); + sl.merge(x_base, y_base); + std::cout << sl << "\n"; + + slicing::slice_vector y_5_0; + sl.mk_slice(sl.var2slice(y), 5, 0, y_5_0); + sl.merge(y_5_0, sl.var2slice(b)); + std::cout << sl << "\n"; } }; @@ -65,5 +91,6 @@ namespace polysat { void tst_slicing() { using namespace polysat; test_slicing::test1(); + test_slicing::test2(); std::cout << "ok\n"; }