3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-25 17:04:36 +00:00
Commit graph

19973 commits

Author SHA1 Message Date
Lev Nachmanson
0baaa3f9ce relax an assert
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-18 14:44:23 -07:00
Lev Nachmanson
c2661e34fc normalize before pushing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-18 13:14:22 -07:00
Lev Nachmanson
b85cba762c create a better queue on properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-18 12:50:20 -07:00
Lev Nachmanson
b09199c6e6 fix an assert statement
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-17 18:08:01 -07:00
Lev Nachmanson
881d74278d separate the lower and upper bound root functions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-17 13:26:23 -07:00
Lev Nachmanson
7479b0296f filling the relation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-17 11:53:02 -07:00
Lev Nachmanson
1a58a155b8 prepare to fill the relation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-16 18:44:58 -07:00
Lev Nachmanson
d96edf863a t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-16 10:51:33 -07:00
Lev Nachmanson
d27ab932c2 debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-13 13:33:23 -07:00
Lev Nachmanson
744f9df9dd remove a warning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-11 16:25:15 -07:00
Lev Nachmanson
77490399a9 process level 0 as well
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-11 13:55:54 -07:00
Lev Nachmanson
81dec49492 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-10 15:04:50 -07:00
Lev Nachmanson
5e54cb6693 add a guard on m_fail
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-10 14:56:09 -07:00
Lev Nachmanson
a6d5c9762c create irreducible polynomials on init
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-10 13:58:41 -07:00
Lev Nachmanson
d235829b3d new file
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-09 17:38:11 -07:00
Lev Nachmanson
6f950d670d try iterative factoring
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-09 17:05:34 -07:00
Lev Nachmanson
391c4248d4 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-09 11:11:51 -07:00
Lev Nachmanson
2da3b591a7 produce more literals but creating sat lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-08 17:40:29 -07:00
Lev Nachmanson
7f5e7d523c adding ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-08 16:46:41 -07:00
Lev Nachmanson
49eb5625ca fixing factoring and hitting NOT_IMPLEMENTED on ir_ord
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-08 14:12:28 -07:00
Lev Nachmanson
7049eab658 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-08 07:37:39 -07:00
Lev Nachmanson
93ec3f841e comment 2025-10-05 13:40:22 -07:00
Lev Nachmanson
aca39a20a7 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-03 17:47:01 -07:00
Lev Nachmanson
fb97043cb2 add parameter to suppress/enable levelwise
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-03 12:54:53 -07:00
Lev Nachmanson
32de7c61fc t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-01 14:50:59 -07:00
Lev Nachmanson
9c006c4e42 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-01 14:00:19 -07:00
Lev Nachmanson
7fc4fe9b66 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-01 12:12:30 -07:00
Lev Nachmanson
97c28cb226 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-27 08:06:24 -08:00
Lev Nachmanson
25d0386ade remove a parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-27 07:22:33 -08:00
Lev Nachmanson
204560288e t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-27 07:02:45 -08:00
Lev Nachmanson
0274982adb t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-18 14:40:55 -07:00
Lev Nachmanson
88e86af2c6 introdure mk_prop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-18 11:34:28 -07:00
Lev Nachmanson
658cf36f09 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-13 15:09:16 -07:00
Lev Nachmanson
842e2c79dc got a section
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 17:14:26 -10:00
Lev Nachmanson
2cec8b4e9a t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 15:42:13 -10:00
Lev Nachmanson
8eec2b1932 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 12:24:47 -10:00
Lev Nachmanson
493ce3af2f t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 10:21:08 -10:00
Lev Nachmanson
82c4dbd73c t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 07:56:46 -10:00
Lev Nachmanson
3bc1873882 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 07:32:02 -10:00
Lev Nachmanson
3cf0c730b9 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 07:22:59 -10:00
Lev Nachmanson
2a3cccaec3 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-08 07:15:38 -10:00
Lev Nachmanson
87cba2279e t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-07 18:05:50 -10:00
Lev Nachmanson
1a89063bb9 ignore holds properties
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-06 10:28:44 -10:00
Lev Nachmanson
1e42f3f5a0 remove erase_from_Q
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-06 10:07:10 -10:00
Lev Nachmanson
9f72a95e9e simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-06 09:56:15 -10:00
Lev Nachmanson
ec9a01cd6e simplify
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-06 08:27:55 -10:00
Lev Nachmanson
3a06d501c8 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-05 16:04:42 -10:00
Lev Nachmanson
5f6de08b5d t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-05 13:13:27 -10:00
Lev Nachmanson
63db413a86 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-05 10:37:01 -10:00
Lev Nachmanson
1acf680646 t
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-09-05 10:35:19 -10:00