Commit Graph

  • 24563ee6bd Merge branch 'topic/kanig-1153-z3-4154' into 'master' master Johannes Kanig 2026-01-08 08:57:46 +00:00
  • f1ba69ca2c Merging z3 4.15.4 into AdaCore master Johannes Kanig 2026-01-08 11:27:00 +09:00
  • 745087e237 update release notes Nikolaj Bjorner 2025-10-29 07:39:33 -07:00
  • c88295a7c7 fix C++ example and add polymorphic interface for C++ Nikolaj Bjorner 2025-10-29 03:08:49 -07:00
  • 6efffa0054 renemable Centos AMD nightly Nikolaj Bjorner 2025-10-28 18:55:36 -07:00
  • 1b9a636910 fix build break introduced when adding support for polymorphic datatypes Nikolaj Bjorner 2025-10-28 18:54:35 -07:00
  • 88fcc05d6c Bump actions/upload-artifact from 4 to 5 (#7998) dependabot[bot] 2025-10-28 15:47:26 -07:00
  • 488c712f5b Bump actions/download-artifact from 5 to 6 (#7999) dependabot[bot] 2025-10-28 15:47:15 -07:00
  • 3570073c29 Add missing mkLastIndexOf method and CharSort case to Java API (#8002) Copilot 2025-10-28 15:46:48 -07:00
  • b6e3a68839 update centos version Nikolaj Bjorner 2025-10-28 15:13:30 -07:00
  • 766eaa3376 disable centos build until resolved Nikolaj Bjorner 2025-10-20 08:33:01 +02:00
  • efd5d04af5 enable always add all coeffs in nlsat Lev Nachmanson 2025-10-24 17:47:16 -07:00
  • 887ecc0c98 throttle grobner method more actively Lev Nachmanson 2025-10-22 21:36:22 -07:00
  • 58e64ea826 try exponential delay in grobner Lev Nachmanson 2025-10-22 17:00:16 -07:00
  • 2bf1cc7d61 Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) hwisungi 2025-10-22 05:18:25 -07:00
  • 68a7d1e1b1 Bump actions/setup-node from 5 to 6 (#7994) dependabot[bot] 2025-10-21 21:17:35 +02:00
  • 9a2867aeb7 Add a fast-path to _coerce_exprs. (#7995) Nelson Elhage 2025-10-21 12:16:54 -07:00
  • 06ed96dbda add the "noexcept" keyword to value_score=(value_score&&) declaration Lev Nachmanson 2025-10-20 11:53:34 -07:00
  • f2e7abbdc1 disable manylinux until segfault is resolved Nikolaj Bjorner 2025-10-20 08:28:08 +02:00
  • aaaa32b4a0 build fixes Nikolaj Bjorner 2025-10-19 20:55:45 +02:00
  • d65c0fbcd6 add explicit constructors for nightly mac build failure Nikolaj Bjorner 2025-10-19 20:14:20 +02:00
  • fcc7e02167 Update arith_rewriter.cpp Nikolaj Bjorner 2025-10-18 13:32:49 +02:00
  • 62ee7ccf65 Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) Nikolaj Bjorner 2025-10-16 13:18:35 +02:00
  • 05ffc0a77b Add finite_set_value_factory for creating finite set values in model generation (#7981) Copilot 2025-10-16 13:16:54 +02:00
  • a179286183 restore the method behavior Lev Nachmanson 2025-10-15 16:41:32 -07:00
  • 1921260c42 restore single cell Lev Nachmanson 2025-10-14 17:43:48 -07:00
  • 3b565bb284 trim parametric datatype test Nikolaj Bjorner 2025-10-15 21:39:39 +02:00
  • 5163411f9b Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966) Copilot 2025-10-15 20:51:21 +02:00
  • e669fbe557 Bump github/codeql-action from 3 to 4 (#7971) dependabot[bot] 2025-10-14 18:08:27 +02:00
  • 641741f3a8 parameter eval order Lev Nachmanson 2025-10-07 10:30:58 -07:00
  • 8af9a20e01 parameter eval order Lev Nachmanson 2025-10-07 10:26:40 -07:00
  • 6a9520bdc2 parameter eval order Lev Nachmanson 2025-10-07 10:21:09 -07:00
  • 8ccf4cd8f7 parameter eval order Lev Nachmanson 2025-10-07 10:19:24 -07:00
  • 40b980079b parameter eval order Lev Nachmanson 2025-10-07 10:14:02 -07:00
  • a41549eee6 parameter eval order Lev Nachmanson 2025-10-07 10:06:43 -07:00
  • 2b3068d85f parameter eval order Lev Nachmanson 2025-10-07 09:17:12 -07:00
  • 3a2bbf4802 param eval order Lev Nachmanson 2025-10-07 09:13:21 -07:00
  • 6e52b9584c param eval Lev Nachmanson 2025-10-07 09:04:24 -07:00
  • 93ff8c76db parameter evaluation order Lev Nachmanson 2025-10-07 08:53:49 -07:00
  • 00f1e6af7e parameter eval order Lev Nachmanson 2025-10-07 08:40:24 -07:00
  • c154b9df90 param order evaluation Lev Nachmanson 2025-10-07 08:34:56 -07:00
  • 77c70bf812 param order Lev Nachmanson 2025-10-06 15:51:53 -07:00
  • 63bb367a10 param order Lev Nachmanson 2025-10-06 15:44:41 -07:00
  • e9a2766e6c remove AI slop Nikolaj Bjorner 2025-10-06 13:53:24 -07:00
  • 5a9663247b fix the order of parameter evaluation Lev Nachmanson 2025-10-06 13:42:38 -07:00
  • 5ae858f66b fixing the order Lev Nachmanson 2025-10-06 13:35:37 -07:00
  • aa5645b54b fixing the order Lev Nachmanson 2025-10-06 13:22:18 -07:00
  • 542e015550 Remove unused variable 'first' in mpz.cpp Nikolaj Bjorner 2025-10-06 13:39:27 -07:00
  • cd1ceb6efe [WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963) Copilot 2025-10-06 13:38:18 -07:00
  • 3ce8aca411 Bump actions/checkout from 4 to 5 (#7954) dependabot[bot] 2025-10-04 01:22:52 -07:00
  • c8bdbd2dc4 remove directory Nikolaj Bjorner 2025-10-03 11:58:57 -07:00
  • e137aaa249 add user propagators to opt_solver Nikolaj Bjorner 2025-10-02 19:44:22 -07:00
  • 0e6b3a922a Add commands for forcing preferences during search Nikolaj Bjorner 2025-10-02 10:47:10 -07:00
  • 5d8fcaa3ee update clang format Nikolaj Bjorner 2025-10-02 10:39:37 -07:00
  • 72c89e1a4e fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables Nikolaj Bjorner 2025-09-30 15:58:48 -07:00
  • 0881a71ed2 update format Nikolaj Bjorner 2025-09-30 15:42:01 -07:00
  • 65c9a18c3a fix #7956 Nikolaj Bjorner 2025-09-30 15:41:40 -07:00
  • 339f0cd5f9 Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955) Ruijie Fang 2025-09-30 11:55:14 -05:00
  • 253a7245d0 add analysis Nikolaj Bjorner 2025-09-28 13:05:04 +03:00
  • b5f79da76a add analysis Nikolaj Bjorner 2025-09-28 13:03:31 +03:00
  • ae55b6fa1e add analysis Nikolaj Bjorner 2025-09-28 13:02:05 +03:00
  • bda98d8da4 fix #7948 Nikolaj Bjorner 2025-09-28 12:45:42 +03:00
  • b7eb21efed fix #7948 Nikolaj Bjorner 2025-09-28 12:44:56 +03:00
  • 391880b6fc Add missing ::z3::sdiv to z3++.h (#7947) Wael Boutglay 2025-09-25 21:04:15 +02:00
  • 6173a0d025 propagate value initialization to atoms Nikolaj Bjorner 2025-09-24 11:01:24 +03:00
  • eae4de075b fix latent bug in factorization Nikolaj Bjorner 2025-09-23 10:47:24 +03:00
  • 04ddade2dd remove stale comment Nikolaj Bjorner 2025-09-22 04:43:41 +03:00
  • f5c28a0b76 household cleanup Nikolaj Bjorner 2025-09-22 03:58:04 +03:00
  • e26f7b900c fix unsound axiom for lower-bounding Nikolaj Bjorner 2025-09-21 19:23:55 +03:00
  • dcdae5a61c add smt debug output for nla_core Nikolaj Bjorner 2025-09-21 19:23:42 +03:00
  • ce53e06e29 Par (#7945) Nikolaj Bjorner 2025-09-21 10:11:04 +03:00
  • 2b5b985492 fix divergence regression Nikolaj Bjorner 2025-09-20 02:18:44 -07:00
  • 9876e85a45 turn on max of sums transformation Nikolaj Bjorner 2025-09-20 00:55:37 -07:00
  • 3256d1cc8b fix bug in unit test Nikolaj Bjorner 2025-09-20 00:44:49 -07:00
  • 0e8648c7d7 fix compile of lp.cpp Nikolaj Bjorner 2025-09-20 00:33:23 -07:00
  • a8ae52bfbf fix missing call change to cross-nested. Prepare for lower-bound and upper-bound cardinality constraints Nikolaj Bjorner 2025-09-19 18:57:50 -07:00
  • 2517b5a40a port improvements from ilana branch to master regarding nla Nikolaj Bjorner 2025-09-19 12:28:20 -07:00
  • 5d91294e90 update workflows Don Syme 2025-09-19 03:31:56 +01:00
  • 59bd1cf4a0 updated clang format Nikolaj Bjorner 2025-09-18 15:13:20 -07:00
  • b17df988ed Daily Test Coverage Improver: Add comprehensive API special relations tests (#7925) Don Syme 2025-09-18 17:20:14 +01:00
  • 3fa34952f0 Daily Backlog Burner: Fix bad .dylib versioning in pip packages (#7914) Don Syme 2025-09-18 16:55:56 +01:00
  • c43cb18e63 better rewriting Lev Nachmanson 2025-09-18 08:08:32 -07:00
  • 37904b9e85 fix the parameter evaluation order Lev Nachmanson 2025-09-18 07:52:13 -07:00
  • cda0a922b9 Daily Test Coverage Improver: Add comprehensive API polynomial tests (#7905) Don Syme 2025-09-18 04:47:22 +01:00
  • 82ab6741a0 Daily Test Coverage Improver: Add comprehensive API pseudo-boolean constraint tests (#7898) Don Syme 2025-09-18 04:45:43 +01:00
  • 222c64fa6f Remove Windows-only guard from hashtable unit tests (#7901) Don Syme 2025-09-18 04:23:01 +01:00
  • 635d3b7017 Add .clang-format file for C++ code formatting (#7904) Don Syme 2025-09-18 04:22:27 +01:00
  • 1b058f23e9 Daily Backlog Burner: Add include directory for easier Z3 integration (#7907) Don Syme 2025-09-18 04:21:56 +01:00
  • 4e1a9d1ef7 Daily Test Coverage Improver: Add comprehensive API Datalog tests (#7921) Don Syme 2025-09-18 04:07:24 +01:00
  • 7cb491dd6a update compiled workflows Don Syme 2025-09-17 23:49:55 +01:00
  • d989bcaebe update compiled workflows Don Syme 2025-09-17 23:47:16 +01:00
  • f300dfc425 recompile improvers Don Syme 2025-09-17 16:41:49 +01:00
  • 2d0b9e6972 recompile improvers Don Syme 2025-09-17 15:50:33 +01:00
  • aabdb407d1 latest improvers Don Syme 2025-09-17 13:49:00 +01:00
  • 2364ea42ba update improvers Don Syme 2025-09-17 13:19:24 +01:00
  • 7268136bb6 update workflows Don Syme 2025-09-17 11:33:24 +01:00
  • db8206d265 improve improvers Don Syme 2025-09-17 11:03:23 +01:00
  • 5b70f75d89 allow burner to create PRs Don Syme 2025-09-17 02:41:38 +01:00
  • 81da4be228 backlog burner Don Syme 2025-09-17 02:20:48 +01:00
  • ba4c9238c0 add daily backlog burner Don Syme 2025-09-17 02:03:48 +01:00