mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 10:50:24 +00:00
Code Activity

viable::test3

Browse source
This commit is contained in:
Jakob Rath 2023-11-10 10:53:15 +01:00
parent b7ee4b0d63
commit 5a03d13913
1 changed files with 29 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/test/viable.cpp
View file

@ -144,17 +144,35 @@ namespace polysat {
rational const two_to_60 = rational::power_of_two(60); rational const two_to_60 = rational::power_of_two(60);
params_ref p;
p.set_uint("max_decisions", 1);
s.updt_polysat_params(p);
// x >= 5000
s.add_ule(5000, x); s.add_ule(5000, x);
VERIFY_EQ(s.check_sat(), l_true); VERIFY_EQ(s.check_sat(), l_undef);
rational lo, hi; rational lo, hi;
std::cout << "find_viable: " << v.find_viable2_new(xv, lo, hi) << "\n"; VERIFY_EQ(v.find_viable2_new(xv, lo, hi), l_true);
std::cout << "lo: " << lo << "\n"; std::cout << "lo: " << lo << "\n";
std::cout << "hi: " << hi << "\n"; std::cout << "hi: " << hi << "\n";
// 10 < x[3:0] p.set_uint("max_decisions", 2);
s.updt_polysat_params(p);
// x[3:0] >= 10
s.add_ule(10 * two_to_60, x * two_to_60); s.add_ule(10 * two_to_60, x * two_to_60);
VERIFY_EQ(s.check_sat(), l_true); VERIFY_EQ(s.check_sat(), l_undef);
std::cout << "find_viable: " << v.find_viable2_new(xv, lo, hi) << "\n"; VERIFY_EQ(v.find_viable2_new(xv, lo, hi), l_true);
std::cout << "lo: " << lo << "\n";
std::cout << "hi: " << hi << "\n";
p.set_uint("max_decisions", 3);
s.updt_polysat_params(p);
// x[3:0] <= 5
s.add_ule(x * two_to_60, 5 * two_to_60);
VERIFY_EQ(s.check_sat(), l_undef);
VERIFY_EQ(v.find_viable2_new(xv, lo, hi), l_false);
std::cout << "lo: " << lo << "\n"; std::cout << "lo: " << lo << "\n";
std::cout << "hi: " << hi << "\n"; std::cout << "hi: " << hi << "\n";
} }