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

19500 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson 6cee4ae225 change a printout 2025-03-06 14:05:16 -10:00
Lev Nachmanson 57f87e1abe work on the outer loop 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-06 15:27:33 -08:00
Lev Nachmanson 6cdaa90486 trying the standard handling of m_new_fixed_columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-05 21:44:43 -08:00
Lev Nachmanson c3668701e4 debug tighten_bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-05 10:58:39 -08:00
Lev Nachmanson e4e4e8c7b8 debug tighten_bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-05 10:45:35 -08:00
Lev Nachmanson f4f199faf7 debug tighten_bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-04 10:46:07 -10:00
Lev Nachmanson 1612eafaeb transfer work 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-04 08:29:41 -08:00
Lev Nachmanson d7d7241cd9 debug bound propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-02 17:58:32 -08:00
Lev Nachmanson 3224c19154 adjust printing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-01 12:10:17 -08:00
Lev Nachmanson 7cfecaa0b4 debug dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-01 11:32:00 -08:00
Lev Nachmanson aa57ee7b62 toward bound prop 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-28 17:08:06 -08:00
Lev Nachmanson a3d9803fa5 experiment with cuts in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-27 16:04:36 -10:00
Lev Nachmanson 3d65e9c2fc trying tighten_bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-25 20:05:30 -10:00
Lev Nachmanson 530990ee64 experiment with tighten_bound 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-25 12:59:33 -10:00
Lev Nachmanson f9b4f68982 Merge branch 'dio' of https://github.com/Z3Prover/Z3 into dio 2025-02-25 10:58:24 -10:00
Lev Nachmanson 8850ea6cab cosmetics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-25 10:58:05 -10:00
Lev Nachmanson 94fb868332 support mixed case 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-24 18:03:21 -08:00
Lev Nachmanson 447af0f548 allow fixed variables is term tightening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-24 13:07:40 -08:00
Lev Nachmanson 3271f2fad9 remove unnecessery dependency when tightening a bound 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-24 10:38:25 -08:00
Lev Nachmanson 8414e18647 change in tracing dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-22 09:30:32 -08:00
Lev Nachmanson 4ad8ab42ae propagate on undef 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-21 23:16:26 -08:00
Lev Nachmanson c3461c60eb prepare bound_analyzer for using in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-21 16:59:24 -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
Nikolaj Bjorner 10c2af85c1 try for mixed-mode 2025-02-21 13:24:37 -08:00
Nikolaj Bjorner ead8478046 fix build per new API for analyze_row 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-21 12:48:34 -08:00
Nikolaj Bjorner 1a3d1ad69d add base line bounds tightening utility 2025-02-21 12:46:51 -08:00
Lev Nachmanson 7044bb8485 remove an unused parameter in bound_analyzer_on_row 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-21 10:17:43 -10:00
Nikolaj Bjorner fbfbfa5d76 print column value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-20 09:55:39 -08:00
Hari Govind V K f50f21198e
Fix #7505 (#7565) 
* fix #7505

* rename
 2025-02-20 09:54:59 -08:00
Lev Nachmanson bd3d288a08 tighten only core constrants 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-20 08:40:16 -08:00
Nikolaj Bjorner 45ad61438a added logging 2025-02-19 17:40:59 -08:00
Nikolaj Bjorner 1fec0fa35b remove verbose output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-19 15:35:51 -08:00
Nikolaj Bjorner 01fbc0e8e7 fix #7563 2025-02-19 14:55:27 -08:00
Nikolaj Bjorner 712231dcda fix #7560 2025-02-19 09:39:17 -08:00
Nikolaj Bjorner 075773e519 remove proviso for single index arrays 2025-02-19 00:02:38 -08:00
Nikolaj Bjorner 3e5abef145 fix #7549 2025-02-18 21:38:06 -08:00
Nikolaj Bjorner e0945f57bb fix #7554 
mbp_qel  uses two iterations of saturation.
The first iteration uses only congruences, not the model.
The second iteration uses the model.
Terms are marked as "seen" during either iteration and will not be reprocessed if they are "seen".
All select terms get marked as "seen" to avoid reproducing Ackerman axioms.
But this conflicts with expanding select-store axioms during
the phase of saturation where use_model is allowed.
 2025-02-18 21:04:34 -08:00
Nikolaj Bjorner 28f3f8046e #7559 2025-02-18 20:50:06 -08:00
Nikolaj Bjorner 11066486d7 #7559 2025-02-18 20:48:13 -08:00
Nikolaj Bjorner 991cffb519 handle multi-arity arrays 2025-02-18 20:38:45 -08:00
Nikolaj Bjorner 674e1b8f98 remove equality check on container 2025-02-18 20:15:42 -08:00
Nikolaj Bjorner ce69b54b5f adjust select/store rule for n-ary arrays 2025-02-18 20:08:56 -08:00
Nikolaj Bjorner 42f6e1300a more review of mbp_arrays 2025-02-18 19:48:54 -08:00
Nikolaj Bjorner a4a84ed083 arrays are not necessarily unary 2025-02-18 19:13:12 -08:00
Nikolaj Bjorner a5e5a35755 code simplification 2025-02-18 19:07:58 -08:00
Nikolaj Bjorner a143ed3bff taking a look at mbp_qel for arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 16:28:49 -08:00
Nikolaj Bjorner dda60737dc updated release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 15:03:24 -08:00
Nikolaj Bjorner fb6ec7d5e7 increase version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 15:00:26 -08:00
Nikolaj Bjorner 30dba9bde7 use down-level setup tools on hosted machines to avoid https://stackoverflow.com/questions/79252233/canonicalize-versionversion-strip-trailing-zero-false-while-doing-colcon-buil 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 14:36:16 -08:00