mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity
19526 commits 23 branches 48 tags 157 MiB
Commit graph

19526 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 87810c6ad9 fix bug introduced while absstracting m_conflict_index 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-16 10:42:41 -07:00
Nikolaj Bjorner 14c672ff7d isolate m_conflict_index functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-16 10:34:30 -07:00
Nikolaj Bjorner 0b3ef828d5 add systematic way to combine lia_move results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-16 10:24:44 -07:00
Nikolaj Bjorner beee2182dd nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-15 18:17:27 -07:00
Nikolaj Bjorner 78d66b9251 print also column values 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-15 17:01:18 -07:00
Lev Nachmanson c1b1a8c3ab remove term sorting by the span 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-15 12:33:09 -10:00
Lev Nachmanson e532308b92 sort terms by weight for tightening 2025-03-15 06:18:42 -10:00
Lev Nachmanson ae30e2c49f more aggressive term tightening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-14 16:38:37 -10:00
Lev Nachmanson e846c2ac8b try another sorting of terms to tighten 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-14 09:30:32 -07:00
Lev Nachmanson 364abb656e separate m_changed_terms and m_terms_to_tighten in indexed_uint_sets 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-14 05:31:50 -10:00
Lev Nachmanson 62435b15bb detect non integral terms in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-14 05:17:33 -10:00
Lev Nachmanson 0c24536096 testing! disable gomory cut in int_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-13 19:52:11 -10:00
Lev Nachmanson 6cce535f83 optimize entrry recalculation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-13 19:22:44 -07:00
Lev Nachmanson 699049f1dc allow bounds tightening on fixed columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-12 17:31:34 -07:00
Lev Nachmanson e08a0cc29e add comments and renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-12 10:10:03 -10:00
Lev Nachmanson 3238d94813 profile and remove dead code from dioph_eq.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-10 14:58:19 -10:00
Lev Nachmanson 64901a4e4f improved dio handler 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-10 07:06:36 -10:00
Nikolaj Bjorner e05f75d74c switch to ubuntu 24 for python packaging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-09 20:53:36 -07:00
Nikolaj Bjorner 07fa36e37a fix #7466 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-09 18:50:07 -07:00
Nikolaj Bjorner ab0323c22b update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-09 17:19:02 -07:00
Nikolaj Bjorner ea1360ee46 fix #7578 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-09 17:01:42 -07:00
Nikolaj Bjorner c002c77e5a fix #7569 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-07 11:53:01 -08:00
Nikolaj Bjorner 54c6b11621
Update README.md 
redist license pointer
 2025-03-07 11:47:32 -08:00
Nikolaj Bjorner 80f00f191a fix #7572 and fix #7574 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-07 10:46:29 -08:00
Nikolaj Bjorner 8df45b442b try ubuntu 24 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-05 13:58:39 -08:00
Nikolaj Bjorner b47ec2074b try version 75 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-05 11:26:12 -08:00
Nikolaj Bjorner 3e7f4839d1 68 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-04 17:14:10 -08:00
Nikolaj Bjorner dedfe9019d remove downlevel setup in nightly.yaml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-04 07:38:28 -08:00
Nikolaj Bjorner f698dea2b0 downlevel setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 18:25:20 -08:00
Nikolaj Bjorner e6855bb299 disable setup tool install 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 16:01:45 -08:00
Nikolaj Bjorner d714f1b6c5 update path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 14:23:33 -08:00
Nikolaj Bjorner 7eb401b891 extract paths within zip file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 07:15:29 -08:00
Nikolaj Bjorner 476c5ee110 improve diagnostics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 19:36:47 -08:00
Nikolaj Bjorner f74d8460f6 use single thread for win-dist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 19:23:19 -08:00
Nikolaj Bjorner 14390eeac2 fix typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 18:44:04 -08:00
Nikolaj Bjorner 62616cf37c fixup nuget task 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 17:13:03 -08:00
Nikolaj Bjorner d24c488482 fix error in mk_nuget_task.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-28 18:19:36 -08:00
Nikolaj Bjorner a97e5fcf0e fix error in mk_nuget_task.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-28 18:18:51 -08:00
Nikolaj Bjorner cd95c7e72a add diagnostics to extraction of Microsoft.pdb/xml/dll 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-28 13:55:44 -08:00
Nikolaj Bjorner ec93972356 fixup unit tests 2025-02-27 17:18:53 -08:00
Nikolaj Bjorner b784b748d4 fix #7550 2025-02-27 14:43:11 -08:00
Nikolaj Bjorner 83ee21cd22 streamline tracing 2025-02-27 14:42:35 -08:00
Nikolaj Bjorner db997cd64d fix regression, missing idx increment in iterator loop #7566 2025-02-25 01:52:42 -08:00
Lev Nachmanson a7310462df throttle down cuts from proofs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-23 19:38:35 -08:00
Nikolaj Bjorner be8febedc3 add throttle, fixup bp.init() for proper initialization 2025-02-22 16:27:58 -08:00
Nikolaj Bjorner c79967b2b6 using iterators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-21 19:20:49 -08:00
Nikolaj Bjorner 17f239c2cb base line specbot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-21 16:07:13 -08:00
Nikolaj Bjorner 589fb1b04f base line specbot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-21 16:00:08 -08:00
Lev Nachmanson 67d77e26d2 remove a parameter when calling bound_analyzer_on_row 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-21 14:43:08 -08:00
Lev Nachmanson b985838112 do not pass row index to bound_analyzer_on_row 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-21 14:38:40 -08:00