\brief convert p == 0 into a solved form v == r, such that
v has bounds [lo, oo) iff r has bounds [lo', oo)
v has bounds (oo,hi] iff r has bounds (oo,hi']
The solved form allows the Grobner solver identify more bounds conflicts.
A bad leading term can miss bounds conflicts.
For example for x + y + z == 0 where x, y : [0, oo) and z : (oo,0]
we prefer to solve z == -x - y instead of x == -z - y
because the solution -z - y has neither an upper, nor a lower bound.
The Grobner solver is augmented with a notion of a substitution that is applied before the solver is run.
For Grobner we want to preserve directions of intervals for finding sign conflicts. This means that it makes sense to have external control over linear solutions.
this update integrates inferences to smt.arith.solver=6 related to grobner basis computation and handling of div/mod axioms to reconcile performance with smt.arith.solver=2.
The default of smt.arth.nl.grobner_subs_fixed is changed to 1 to make comparison with solver=2 more direct.
The selection of cluster equalities for solver=6 was reconciled with how it is done for solver=2.
* Subtle bug in kernel computation
Coefficient was being passed by reference and, therefore, was
being changed indirectly.
In the process, updated the code to be more generic to avoid rational
computation in the middle of matrix manipulation.
* sparse_matrix: fixed handling of 0 in add_var() and add()
particularly in add_var(), without the fix the user is responsible for checking
coefficients for 0.
In some cases, Z3_algebraic_get_i() returned 0. For example, in the following
Python snippet, the last assert would fail:
import z3
x = z3.Real('x')
s = z3.Solver()
s.add( (x * x) - 2 == 0, x <= 0)
s.check()
val_x = s.model().get_interp(x)
assert val_x.index() == 1
The problem was that `algebraic_numbers::manager:👿:get_i()` did not
check whether the root index was properly initialized.
This commit fixes this issue by checking whether root index is initialized
the same way various other routines do.
Fixes issue #5807.
Signed-off-by: Jan Vrany <jan.vrany@labware.com>
* remove the bound on total iterations in simplex
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* remove unncesseray checks in get_freedom_interval_for_column()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix the build of test-z3
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Revert "remove unncesseray checks in get_freedom_interval_for_column()"
This reverts commit 6770ed85e3.
* optimize get_freedom_interval_for_column() for feasible case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add function lar_solver::status_feasible
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* rename status_is_feasible() to is_feasible()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix the linux build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
- it resets row checks after backtracking even though they could still propagate
- it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.
FYI @levnach
