3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00

Commit graph

  • fda842146a
    Merge a012953985 into 81f10912ae mikulas-patocka 2025-04-15 08:39:06 +0100
  • bd5d80fac8
    Merge bcd615f3c5 into 81f10912ae mikulas-patocka 2025-04-15 08:38:59 +0100
  • 67c8644b44
    Merge b5821f6e5e into 81f10912ae mikulas-patocka 2025-04-15 08:38:51 +0100
  • 8f35436b2a
    Merge 36a0006f59 into 81f10912ae Lev Nachmanson 2025-04-15 15:11:02 +0800
  • 76675b2ec3
    Merge 4b3207505b into 81f10912ae Shiwei Weng 翁士伟 2025-04-14 20:44:44 -0400
  • 81f10912ae remove unused bdd based variable elimination master Nikolaj Bjorner 2025-04-14 16:07:41 -0700
  • e41090df83 fix #7602 Nikolaj Bjorner 2025-04-14 15:38:22 -0700
  • 8035edbe65 remove lp_assert Nikolaj Bjorner 2025-04-14 11:10:26 -0700
  • 1510b3112e fix build warnings Nikolaj Bjorner 2025-04-14 10:33:14 -0700
  • 5ad79f2864
    Add Iterators as acceptable arguments to functions (#7620) Kyle Bloom 2025-04-12 18:32:56 +0100
  • 8f05d2e3cb Add Iterators as acceptable arguments to functions Kyle Bloom 2025-04-12 15:34:30 +0100
  • 6ecc7a2dd4
    Fix a race condition in scoped_timer::finalize (#7618) mikulas-patocka 2025-04-11 09:08:27 +0200
  • a83efa68eb spacing Nikolaj Bjorner 2025-04-09 20:23:51 -0700
  • 8138829231 fix #7616 Nikolaj Bjorner 2025-04-09 20:23:26 -0700
  • 36a0006f59 remove testing code in is_big_term_on_no_term dio Lev Nachmanson 2025-04-09 19:24:59 -0700
  • 97bb449a24 fix a bug in tracking the changes in dio Lev Nachmanson 2025-04-09 15:56:44 -0700
  • 7e88064da9 allow gcd when dio ignores some terms Lev Nachmanson 2025-04-09 10:23:55 -0700
  • b5821f6e5e Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling Mikulas Patocka 2025-04-09 19:03:26 +0200
  • b007eb30ab Fix a race condition in scoped_timer::finalize Mikulas Patocka 2025-04-09 18:46:10 +0200
  • bcd615f3c5 Make Ctrl-C handling thread-safe (#7603) Mikulas Patocka 2025-04-09 18:29:08 +0200
  • 7ee3415150 make gcd call in dio optional Lev Nachmanson 2025-04-08 16:10:17 -0700
  • d792840739
    Add Z3_is_recursive_datatype_sort to the API (#7615) Josh Berdine 2025-04-08 22:36:57 +0100
  • 019da2308e always remove the tightened term Lev Nachmanson 2025-04-08 10:47:51 -0700
  • 386c331eb9 Add Z3_is_recursive_datatype_sort to the API Josh Berdine 2025-04-08 16:50:59 +0100
  • dd1b2a294f change the name of m_changed_columns to m_changed_f_columns Lev Nachmanson 2025-04-08 07:07:00 -0700
  • 0011deea5c typo Lev Nachmanson 2025-04-08 06:18:57 -0700
  • df10608db8 reject more terms with big numbers Lev Nachmanson 2025-04-07 11:49:39 -0700
  • 14e2aadad0
    include LICENSE.txt in wheels (#7614) Mark Ryan 2025-04-07 17:41:50 +0200
  • 93a08a56f6 include LICENSE.txt in wheels Mark Ryan 2025-04-07 11:51:28 +0000
  • a012953985 Add an option "ctrl_c" that can be used to disable Ctrl-C signal handling Mikulas Patocka 2025-04-06 19:11:45 +0200
  • 95d90a7be5 Fix a race condition in scoped_timer::finalize Mikulas Patocka 2025-04-06 19:11:29 +0200
  • a4e7bf82da Fix grabbing a mutex from a signal handler Mikulas Patocka 2025-04-06 19:11:04 +0200
  • 88eb4634d0 Fix a race condition between timer and Ctrl-C Mikulas Patocka 2025-04-06 19:10:44 +0200
  • bb81f26fcb Make Ctrl-C handling thread-safe (#7603) Mikulas Patocka 2025-04-06 19:10:19 +0200
  • 0b7a81b7c9 list[ExprRef] doesn't build for python agent-updates Nikolaj Bjorner 2025-04-05 14:45:52 -0700
  • 2b6055040b update agentz3 sample based on hugging face training/test data Nikolaj Bjorner 2025-04-05 14:43:30 -0700
  • e7ff6009a0 #7605 Nikolaj Bjorner 2025-04-05 12:07:46 -0700
  • a39efbb008 fix #7607 Nikolaj Bjorner 2025-04-05 11:58:47 -0700
  • 9d8291a75b remove type annotation Context | None to ensure Centos ARM Build pass Nikolaj Bjorner 2025-04-05 10:51:35 -0700
  • 3fd7ee93be
    dio_calls_period=4 Lev Nachmanson 2025-04-05 10:27:49 -0700
  • cc5c98f5b0
    Update lp_settings.h - m_dio_calls_period = 4 Lev Nachmanson 2025-04-05 10:26:35 -0700
  • baadb9bb07
    Update lp_settings.cpp Lev Nachmanson 2025-04-05 10:25:39 -0700
  • f607331856 type annotations across Python versions Nikolaj Bjorner 2025-04-04 22:14:32 -0700
  • bd2c7aa908 remove downlevel version incompatible elements of typing Nikolaj Bjorner 2025-04-04 20:18:23 -0700
  • d4ba75eb79 add parameter m_dio_calls_period Lev Nachmanson 2025-04-04 19:56:13 -0700
  • 305f1e8498 remove references to TypeGuard Nikolaj Bjorner 2025-04-04 19:41:50 -0700
  • a5048e4563 add initial sample agent use case Nikolaj Bjorner 2025-04-04 18:40:06 -0700
  • 0a3719447e fix #7609 Nikolaj Bjorner 2025-04-04 18:39:48 -0700
  • 5e10fd39fc add selected type annotations to python API Nikolaj Bjorner 2025-04-04 18:39:39 -0700
  • 26ab0de8fc rename function Nikolaj Bjorner 2025-04-04 18:39:12 -0700
  • eb4e28d5d4
    [z3.py] Fix incorrect call to _get_ctx in SeqMapI (#7610) Ammar Askar 2025-04-04 15:54:32 -0700
  • d52561dcd6
    [z3.py] Fix incorrect call to _get_ctx in SeqMapI Ammar Askar 2025-04-04 15:23:50 -0700
  • 9cf5665cd6 throttle dio Lev Nachmanson 2025-04-04 13:34:16 -0700
  • d0a7aa3d43 throttle dio for big numbers Lev Nachmanson 2025-04-04 08:51:35 -0700
  • f85a5135c0 reuse dio branch Lev Nachmanson 2025-04-03 09:47:02 -0700
  • 8d81a2dcaf
    Note that Z3_get_numeral_small is essentially redundant (#7599) Josh Berdine 2025-03-29 17:02:32 +0000
  • e2d3f39735 Note that Z3_get_numeral_small is essentially redundant Josh Berdine 2025-03-29 12:57:14 +0000
  • 9b5a9b2089 Check that Z3_get_numeral_small is given non-null out params Josh Berdine 2025-03-29 12:56:04 +0000
  • 63ad2837e2
    Add Z3_get_array_arity (#7598) Josh Berdine 2025-03-28 21:42:51 +0000
  • 5bb35d1a4f Add Z3_get_array_arity Josh Berdine 2023-07-15 01:19:34 +0100
  • 934455a24b
    Remove vestiges of old ml api (#7597) Josh Berdine 2025-03-27 23:41:31 +0000
  • 02df5a1a47 Remove vestiges of old ml api Josh Berdine 2023-07-14 10:25:15 +0100
  • e4897fff00 replace Exists by ForAll in the mathematica lemmas Lev Nachmanson 2025-03-27 12:32:37 -0700
  • 39df8999c8 enable shorterter mathematica printouts in nlsat Lev Nachmanson 2025-03-27 12:23:32 -0700
  • e86a918ae7 turn on ite simplification by default Nikolaj Bjorner 2025-03-26 11:30:08 -0700
  • 8368094618 fix indentation Nikolaj Bjorner 2025-03-25 21:27:38 -0700
  • 4fd6ba442a replace costly ite reduction by disjointnes check Nikolaj Bjorner 2025-03-25 21:15:03 -0700
  • 392bc166a3 optimize bool rewriter Nikolaj Bjorner 2025-03-25 14:07:52 -0700
  • 29712503a0 add option to rewrite ite value trees Nikolaj Bjorner 2025-03-25 11:09:44 -0700
  • e92ccddb23 change line breaks Lev Nachmanson 2025-03-24 15:38:57 -1000
  • 17bd02d1a3 change a comment Lev Nachmanson 2025-03-24 15:29:19 -1000
  • 8bbe752d7d remove dead code Nikolaj Bjorner 2025-03-24 12:47:23 -0700
  • 7e4a1f246e fix crash in elim_constr2 Nikolaj Bjorner 2025-03-24 12:35:57 -0700
  • 93cf989b78 household chores - move to iterators Nikolaj Bjorner 2025-03-24 12:35:46 -0700
  • dee3cf8de4 remove an unused field Lev Nachmanson 2025-03-22 08:59:38 -0700
  • 9302a02a81 reintroduce m_var_register, and avoid modulo gcd in normalize conflicts Lev Nachmanson 2025-03-21 15:35:14 -0700
  • 9a62ed5ab2 added some comments Nikolaj Bjorner 2025-03-20 18:07:25 -1000
  • c634701b8f formatting Nikolaj Bjorner 2025-03-20 17:16:47 -1000
  • f073da9edd cleaning up the inner tightening code Lev Nachmanson 2025-03-20 17:22:23 -0700
  • 8c96178c0b avoid the variable mapping to m_ematrix and suppressing redundand constraints Lev Nachmanson 2025-03-20 09:57:26 -0700
  • 29c5c20267 use more descriptive functions than casting comparisons Nikolaj Bjorner 2025-03-19 21:03:36 -1000
  • 7fb40e86eb tidy Nikolaj Bjorner 2025-03-19 17:57:52 -1000
  • a41bd38a3a use pattern of matching with undef instead of matching with conflict to reduce assumptions on procedure contracts Nikolaj Bjorner 2025-03-19 17:40:43 -1000
  • 676a536e9e fix a print out Lev Nachmanson 2025-03-19 19:55:36 -0700
  • d507d0fdb4 attempt to use the gcd of fixed vars Lev Nachmanson 2025-03-19 13:56:55 -0700
  • f181e3aa81 add comment on derivation of bound Nikolaj Bjorner 2025-03-18 17:39:59 -1000
  • dd19b381d8 detect more m_terms_to_tighten Lev Nachmanson 2025-03-18 10:28:43 -0700
  • 307af0fd97 remove an unused field Lev Nachmanson 2025-03-18 10:08:02 -0700
  • fc1c8c4cc4 add public access to bijection key_val iterator Lev Nachmanson 2025-03-18 09:54:02 -0700
  • 8b5510bcd6 nit Nikolaj Bjorner 2025-03-16 20:48:32 -0700
  • 7577f6fea0 neatify loops Nikolaj Bjorner 2025-03-16 20:41:07 -0700
  • f091b6ffdd remove 'unsat' move, we already have 'conflict'. Add display for cancelled Nikolaj Bjorner 2025-03-16 19:14:29 -0700
  • 1af2474f7b code review updates, tidy pretty printer for column info Nikolaj Bjorner 2025-03-16 18:44:40 -0700
  • 32028083fb fix bug introduced while absstracting m_conflict_index Nikolaj Bjorner 2025-03-16 10:42:41 -0700
  • f3b34fd835 isolate m_conflict_index functionality Nikolaj Bjorner 2025-03-16 10:34:30 -0700
  • ff5ae4d1ed add systematic way to combine lia_move results Nikolaj Bjorner 2025-03-16 10:24:44 -0700
  • 00277ba3cf nits Nikolaj Bjorner 2025-03-15 18:17:27 -0700
  • 488c74d3cc print also column values Nikolaj Bjorner 2025-03-15 17:01:18 -0700
  • 22cfab3d42 remove term sorting by the span Lev Nachmanson 2025-03-15 12:33:09 -1000
  • 12203fc69a sort terms by weight for tightening Lev Nachmanson 2025-03-15 06:18:42 -1000