mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-23 14:57:56 -08:00
parent 50cbe2659a
commit d18a2427a4
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/saturation.cpp
View file

@ -1262,6 +1262,14 @@ namespace polysat {
* The result should be a forbidden interval around v25 based on bounds for * The result should be a forbidden interval around v25 based on bounds for
* v85 and v81. * v85 and v81.
* *
* The example also illustrates that presumably just a combination of forbidden intervals for v85 used in the conflict
* are sufficient for narrowing the bounds on v81. Querying for upper/lower bounds of v85 doesn't produce the strongest
* assumption. 2397 and -1195 come from unit intervals with fixed lo/hi.
*
* On the other hand, the bound v25 > -1*v85*v25 + v81 was obtained by evaluating v25 and v81
* and the quantifier elimination based on viable::resolve_lemma didn't produce the most general lemma.
* Instead it relied on the evaluation at 353 and -1, respectively.
*
*/ */
bool saturation::try_add_mul_bound(pvar x, conflict& core, inequality const& a_l_b) { bool saturation::try_add_mul_bound(pvar x, conflict& core, inequality const& a_l_b) {