mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

disable branches when arguments are non-integral #1824

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-11 04:14:28 -07:00
parent ef310648ae
commit 3bf072557e
1 changed files with 11 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/smt/theory_lra.cpp
View file

@ -1517,6 +1517,17 @@ public:
continue;
}
if (!r1.is_int() || !r2.is_int()) {
// std::cout << r1 << " " << r2 << " " << r << " " << expr_ref(n, m) << "\n";
// TBD
// r1 = 223/4, r2 = 2, r = 219/8
// take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0
// then
// p/q <= ceil(r1)/floor(r2) => n <= div(ceil(r1), floor(r2))
// p/q >= floor(r1)/ceil(r2) => n >= div(floor(r1), ceil(r2))
continue;
}
if (a.is_numeral(q, r3)) {
SASSERT(r3 == r2 && r2.is_int());
@ -1542,16 +1553,6 @@ public:
continue;
}
if (!r1.is_int() || !r2.is_int()) {
// std::cout << r1 << " " << r2 << " " << r << " " << expr_ref(n, m) << "\n";
// TBD
// r1 = 223/4, r2 = 2, r = 219/8
// take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0
// then
// p/q <= ceil(r1)/floor(r2) => n <= div(ceil(r1), floor(r2))
// p/q >= floor(r1)/ceil(r2) => n >= div(floor(r1), ceil(r2))
continue;
}
all_divs_valid = false;