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

19589 commits

This branch
This branch
All branches
Author SHA1 Message Date
Mark Ryan 14e2aadad0
include LICENSE.txt in wheels (#7614) 
Update setup.py so that we copy LICENSE.TXT to src/api/python before
creating the sdist.  Any wheels built from this sdist will now
contain the LICENSE.txt file.

Fixes #7604
 2025-04-07 08:41:50 -07:00
Nikolaj Bjorner 0b7a81b7c9 list[ExprRef] doesn't build for python 2025-04-05 14:45:52 -07:00
Nikolaj Bjorner 2b6055040b update agentz3 sample based on hugging face training/test data 
https://huggingface.co/datasets/CardinalOperations/IndustryOR/blob/main/IndustryOR.json
 2025-04-05 14:43:30 -07:00
Nikolaj Bjorner e7ff6009a0 #7605 
add case for linux/risc64
 2025-04-05 12:07:46 -07:00
Nikolaj Bjorner a39efbb008 fix #7607 2025-04-05 11:58:47 -07:00
Nikolaj Bjorner 9d8291a75b remove type annotation Context | None to ensure Centos ARM Build pass 2025-04-05 10:51:35 -07:00
Nikolaj Bjorner f607331856 type annotations across Python versions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-04-04 22:14:32 -07:00
Nikolaj Bjorner bd2c7aa908 remove downlevel version incompatible elements of typing 2025-04-04 20:18:23 -07:00
Nikolaj Bjorner 305f1e8498 remove references to TypeGuard 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-04-04 19:41:50 -07:00
Nikolaj Bjorner a5048e4563 add initial sample agent use case 2025-04-04 18:40:15 -07:00
Nikolaj Bjorner 0a3719447e fix #7609 2025-04-04 18:40:15 -07:00
Nikolaj Bjorner 5e10fd39fc add selected type annotations to python API 2025-04-04 18:40:15 -07:00
Nikolaj Bjorner 26ab0de8fc rename function 2025-04-04 18:40:15 -07:00
Ammar Askar eb4e28d5d4
[z3.py] Fix incorrect call to _get_ctx in SeqMapI (#7610) 2025-04-04 15:54:32 -07: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