mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

test

Browse source
This commit is contained in:
Jakob Rath 2023-06-28 10:41:22 +02:00
parent 05ea32f17d
commit 7d7735b010
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/test/slicing.cpp
View file

@ -101,8 +101,14 @@ namespace polysat {
VERIFY(sl.merge(sl.var2slice(x), sl.var2slice(y), sat::literal(1)));
std::cout << "v" << x << " = v" << y << "\n" << sl << "\n";
std::cout << "v" << b << " = v" << c << "? " << sl.is_equal(sl.var2slice(b), sl.var2slice(c)) << "\n";
std::cout << "v" << b << " = " << d << "? " << sl.is_equal(sl.var2slice(b), sl.pdd2slice(d)) << "\n";
std::cout << "v" << b << " = v" << c << "? " << sl.is_equal(sl.var2slice(b), sl.var2slice(c))
<< " find(v" << b << ") = " << sl.find(sl.var2slice(b))
<< " find(v" << c << ") = " << sl.find(sl.var2slice(c))
<< "\n";
std::cout << "v" << b << " = " << d << "? " << sl.is_equal(sl.var2slice(b), sl.pdd2slice(d))
<< " find(v" << b << ") = " << sl.find(sl.var2slice(b))
<< " find(" << d << ") = " << sl.find(sl.pdd2slice(d))
<< "\n";
}
};