mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
19546 commits 49 branches 53 tags 182 MiB
Commit graph

1835 commits

Author SHA1 Message Date
Lev Nachmanson
fc1c8c4cc4 add public access to bijection key_val iterator 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
8b5510bcd6 nit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
7577f6fea0 neatify loops 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
f091b6ffdd remove 'unsat' move, we already have 'conflict'. Add display for cancelled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
1af2474f7b code review updates, tidy pretty printer for column info 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
32028083fb fix bug introduced while absstracting m_conflict_index 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
f3b34fd835 isolate m_conflict_index functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
ff5ae4d1ed add systematic way to combine lia_move results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
00277ba3cf nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
488c74d3cc print also column values 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
22cfab3d42 remove term sorting by the span 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
12203fc69a sort terms by weight for tightening 2025-03-24 07:44:13 -10:00
Lev Nachmanson
0a3c118701 more aggressive term tightening 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
50418fa170 try another sorting of terms to tighten 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
ec7c61569d separate m_changed_terms and m_terms_to_tighten in indexed_uint_sets 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
7c12a029e2 detect non integral terms in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
a62d664ae4 testing! disable gomory cut in int_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
5e2d000369 optimize entrry recalculation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
ecfbdbbd23 allow bounds tightening on fixed columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
f501aea3eb add comments and renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
a522e81652 profile and remove dead code from dioph_eq.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
6f7b749ff9 improved dio handler 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10: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
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
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
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
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
11066486d7 #7559 2025-02-18 20:48:13 -08:00
Nikolaj Bjorner
f8f26788ad convert def into expression tree 
prior data-structure could not represent
((1 + x) div 2) * 2
It is possible to have nested expressions with div.
To deal with this, replace original def by an expression tree data-structure.
 2025-02-17 18:47:00 -08:00
Nikolaj Bjorner
f977b48161 adjust solve_for to handle rationals 2025-02-17 13:59:23 -08:00
Lev Nachmanson
bedc95c4c7 use static_cast to avoid the warnings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-13 07:07:12 -10:00
Lev Nachmanson
e920291393 fixing the default parameters of dio and rename m_gomory_cuts to m_cuts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
5ec10e0250 address the review 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
79e3f8ab39 disabling dio handler by default, and fix a print out 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
2131e9b4e4 more accurate work with Markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
bdb8f54150 Revert "revert the term sorting" 
This reverts commit c79d4708cb.
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
5ebee24850 revert the term sorting 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
f2c1fd4c14 try markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
cec8dc2e6e try markovich number 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-02-11 12:23:00 -10:00
Lev Nachmanson
3f2d2e8348 test 2025-02-11 12:23:00 -10:00