mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
19577 commits 23 branches 48 tags 157 MiB
Commit graph

19577 commits

This branch
This branch
All branches
Author SHA1 Message Date
Mikulas Patocka
ac03cc0529 Add an option "ctrl_c" that can be used to disable ctrl-c signal handling 
Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
 2025-04-03 19:17:50 +02:00
Mikulas Patocka
95c55ae76b Make Ctrl-C handling thread-safe (#7603) 
Signed-off-by: Mikulas Patocka <mikulas@twibright.com>
 2025-04-03 19:14:01 +02:00
Josh Berdine
8d81a2dcaf
Note that Z3_get_numeral_small is essentially redundant (#7599) 
* Check that Z3_get_numeral_small is given non-null out params

Analogous to other Z3_get_numeral_* functions with out params.

* Note that Z3_get_numeral_small is essentially redundant

The error behavior of Z3_get_numeral_small does not follow the pattern of
the other functions. The functions that have out params and return a bool
indicating success (such as Z3_get_numeral_rational_int64) return false
rather than signaling an error when given an unsupported expression
argument (such as a rounding mode value). The functions that do not have out
params signal an error in such cases. Z3_get_numeral_small is the odd one
out in that it signals errors and returns a status bool.

This error handling is the only difference between Z3_get_numeral_small and
Z3_get_numeral_rational_int64, so this patch adds a comment to the
documentation.
 2025-03-29 10:02:32 -07:00
Josh Berdine
63ad2837e2
Add Z3_get_array_arity (#7598) 2025-03-28 14:42:51 -07:00
Josh Berdine
934455a24b
Remove vestiges of old ml api (#7597) 2025-03-27 16:41:31 -07:00
Lev Nachmanson
e4897fff00 replace Exists by ForAll in the mathematica lemmas 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-27 12:32:37 -07:00
Lev Nachmanson
39df8999c8 enable shorterter mathematica printouts in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-27 12:23:32 -07:00
Nikolaj Bjorner
e86a918ae7 turn on ite simplification by default 2025-03-26 11:30:08 -07:00
Nikolaj Bjorner
8368094618 fix indentation 2025-03-25 21:27:38 -07:00
Nikolaj Bjorner
4fd6ba442a replace costly ite reduction by disjointnes check 2025-03-25 21:15:03 -07:00
Nikolaj Bjorner
392bc166a3 optimize bool rewriter 2025-03-25 14:07:52 -07:00
Nikolaj Bjorner
29712503a0 add option to rewrite ite value trees 2025-03-25 11:09:56 -07:00
Lev Nachmanson
e92ccddb23 change line breaks 2025-03-24 15:38:57 -10:00
Lev Nachmanson
17bd02d1a3 change a comment 2025-03-24 15:29:19 -10:00
Nikolaj Bjorner
8bbe752d7d remove dead code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 12:47:23 -07:00
Nikolaj Bjorner
7e4a1f246e fix crash in elim_constr2 2025-03-24 12:36:13 -07:00
Nikolaj Bjorner
93cf989b78 household chores - move to iterators 2025-03-24 12:36:13 -07:00
Lev Nachmanson
dee3cf8de4 remove an unused field 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
9302a02a81 reintroduce m_var_register, and avoid modulo gcd in normalize conflicts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
9a62ed5ab2 added some comments 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
c634701b8f formatting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
f073da9edd cleaning up the inner tightening code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
8c96178c0b avoid the variable mapping to m_ematrix and suppressing redundand constraints 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
29c5c20267 use more descriptive functions than casting comparisons 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
7fb40e86eb tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
a41bd38a3a use pattern of matching with undef instead of matching with conflict to reduce assumptions on procedure contracts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
676a536e9e fix a print out 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
d507d0fdb4 attempt to use the gcd of fixed vars 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Nikolaj Bjorner
f181e3aa81 add comment on derivation of bound 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
dd19b381d8 detect more m_terms_to_tighten 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
Lev Nachmanson
307af0fd97 remove an unused field 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-03-24 07:44:13 -10:00
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