mirror of
https://github.com/Z3Prover/z3
synced 2025-10-29 02:39:24 +00:00
316ed778e0
\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. |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||