mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

Another possible case for subsumption

Browse source
This commit is contained in:
Jakob Rath 2022-10-04 14:13:51 +02:00
parent e18dfb2253
commit a0fe568561
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/polysat/simplify_clause.cpp
View file

@ -24,6 +24,20 @@ Notes:
v0 \not\in [0;12[ intersect [13;10[ == [0;10[ v0 \not\in [0;12[ intersect [13;10[ == [0;10[
==> replace 2, 3 by single constraint 10 <= v0 ==> replace 2, 3 by single constraint 10 <= v0
TODO: from bench1:
Lemma: 12 \/ -26 \/ 292 \/ 294 \/ 295
12: v11 <= v10 + v0 [ l_false assert@0 pwatched active ]
-26: v12 + -1*v11 != 0 [ l_false assert@0 pwatched active ]
292: v10 + v0 + 1 == 0 [ l_false eval@6 pwatched active ]
294: v12 + -1*v10 + -1*v0 + -1 == 0 [ l_undef ]
295: v10 + v0 + 1 <= v12 [ l_undef ]
294: v10 + v0 + 1 == v12
295: v10 + v0 + 1 <= v12
==> drop 294
--*/ --*/
#include "math/polysat/solver.h" #include "math/polysat/solver.h"
#include "math/polysat/simplify_clause.h" #include "math/polysat/simplify_clause.h"