mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

disable quadratic moves for non-integers as sqrt isn't currently defined for rationals

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 16:53:12 -08:00
parent d8430810fe
commit fe713eb8e9
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sls_arith_base.cpp
View file

@ -204,7 +204,7 @@ namespace sls {
template<typename num_t> template<typename num_t>
static num_t sqrt(num_t d) { static num_t sqrt(num_t d) {
if (d <= 1) if (d <= 1)
return d; return d;
auto sq = 2*sqrt(div(d, num_t(4))) + 1; auto sq = 2*sqrt(div(d, num_t(4))) + 1;
if (sq * sq <= d) if (sq * sq <= d)
return sq; return sq;
@ -217,6 +217,8 @@ namespace sls {
template<typename num_t> template<typename num_t>
void arith_base<num_t>::find_quadratic_moves(ineq const& ineq, var_t x, num_t const& a, num_t const& b, num_t const& sum) { void arith_base<num_t>::find_quadratic_moves(ineq const& ineq, var_t x, num_t const& a, num_t const& b, num_t const& sum) {
num_t c, d; num_t c, d;
if (!is_int(x)) // sqrt is not defined for non-integers
return;
try { try {
c = sum - a * value(x) * value(x) - b * value(x); c = sum - a * value(x) * value(x) - b * value(x);
d = b * b - 4 * a * c; d = b * b - 4 * a * c;