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

compile test

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 10:52:22 +01:00
parent 17d9888d37
commit 8e94608485
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/test/viable.cpp
View file

@ -53,22 +53,22 @@ namespace polysat {
s.add_ule(x + 3, x + 5);
VERIFY_EQ(s.check_sat(), l_true);
std::cout << v << "\n";
std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
// std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
// std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
s.add_ule(x, 2);
VERIFY_EQ(s.check_sat(), l_true);
std::cout << v << "\n";
s.add_ule(1, x);
VERIFY_EQ(s.check_sat(), l_true);
std::cout << v << "\n";
std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
// std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
// std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
s.add_ule(x, 3);
VERIFY_EQ(s.check_sat(), l_true);
std::cout << v << "\n";
std::cout << v.find_viable(xv, val) << " " << val << "\n";
std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
// std::cout << "min " << v.min_viable(xv, val) << " " << val << "\n";
// std::cout << "max " << v.max_viable(xv, val) << " " << val << "\n";
s.add_ule(3, x);
VERIFY_EQ(s.check_sat(), l_false);
std::cout << v << "\n";