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

16522 commits

Author SHA1 Message Date
Lev Nachmanson 36a0006f59 remove testing code in is_big_term_on_no_term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-09 19:24:59 -07:00
Lev Nachmanson 97bb449a24 fix a bug in tracking the changes in dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-09 15:56:44 -07:00
Lev Nachmanson 7e88064da9 allow gcd when dio ignores some terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-09 10:23:55 -07:00
Lev Nachmanson 7ee3415150 make gcd call in dio optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-08 16:10:17 -07:00
Lev Nachmanson 019da2308e always remove the tightened term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-08 10:47:51 -07:00
Lev Nachmanson dd1b2a294f change the name of m_changed_columns to m_changed_f_columns 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-08 07:07:00 -07:00
Lev Nachmanson 0011deea5c typo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-08 06:18:57 -07:00
Lev Nachmanson df10608db8 reject more terms with big numbers 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-07 11:49:39 -07:00
Lev Nachmanson 3fd7ee93be
dio_calls_period=4 2025-04-05 10:27:49 -07:00
Lev Nachmanson cc5c98f5b0
Update lp_settings.h - m_dio_calls_period = 4 2025-04-05 10:26:35 -07:00
Lev Nachmanson baadb9bb07
Update lp_settings.cpp 
white space change
 2025-04-05 10:25:39 -07:00
Lev Nachmanson d4ba75eb79 add parameter m_dio_calls_period 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-04 19:56:13 -07:00
Lev Nachmanson 9cf5665cd6 throttle dio 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-04 13:34:16 -07:00
Lev Nachmanson d0a7aa3d43 throttle dio for big numbers 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-04 08:51:35 -07:00
Lev Nachmanson f85a5135c0 reuse dio branch 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-03 09:47:02 -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