3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-30 15:59:52 +00:00

Commit graph

  • ec3aafd51e fixup parameter to enable pretty printing of range sort finite-sets Nikolaj Bjorner 2025-12-29 18:09:13 -08:00
  • ba13460511 add functions that create unique sets for model construction based on solving cardinality constraints Nikolaj Bjorner 2025-12-29 11:57:48 -08:00
  • ec4246463f fix #8045 master Nikolaj Bjorner 2025-12-28 10:41:27 -08:00
  • 8cf1e51b9f update tabu policy, enable more propagation arie Nikolaj Bjorner 2025-12-27 17:14:27 -08:00
  • 052631bc97
    Merge 06e38fb0b9 into e4cdbe0035 Copilot 2025-12-27 02:03:19 -05:00
  • 01f79ebb76 tweaks and fixes Nikolaj Bjorner 2025-12-26 15:00:36 -08:00
  • 4c09ab27bc tweaks and fixes Nikolaj Bjorner 2025-12-26 14:59:56 -08:00
  • e4cdbe0035 fixes to finite domain arrays Nikolaj Bjorner 2025-12-26 12:04:57 -08:00
  • 1a91e28b94
    Merge 8e8799dbd3 into c12425c86f Don Syme 2025-12-26 03:16:34 +00:00
  • c12425c86f fix #8099 (again) Nikolaj Bjorner 2025-12-25 13:52:54 -08:00
  • ce2405aab6 assert entry_invariant only when all changes are done Lev Nachmanson 2025-12-25 11:33:32 -10:00
  • f26facaf8f fix #8076 Nikolaj Bjorner 2025-12-25 12:44:08 -08:00
  • 44c0453ea2
    Merge 7c51accb30 into cb5fb390bc Don Syme 2025-12-24 00:12:58 -08:00
  • 6ec3b59ad9 clean up, add comments Nikolaj Bjorner 2025-12-23 15:15:50 -08:00
  • 9d714f0ab9 resurrect model-value based repair. Interleave with bounds splits Nikolaj Bjorner 2025-12-23 11:25:55 -08:00
  • cb5fb390bc fix #8102 Nikolaj Bjorner 2025-12-23 09:44:13 -08:00
  • 78e225f1ca fix the duplicate bug lws Lev Nachmanson 2025-12-22 20:15:09 -10:00
  • 232bae1f9b with resultant calculation ignore one of p and q with a common root Lev Nachmanson 2025-12-22 16:46:31 -10:00
  • eb56ac48b0
    Some changes to improve LIA performance (#8101) Ilana Shapiro 2025-12-22 09:47:36 -08:00
  • 65a57696af price-fee working Nikolaj Bjorner 2025-12-22 09:11:31 -08:00
  • 26119a8815 clean up code Ilana Shapiro 2025-12-21 18:58:15 -08:00
  • 97acdb85a2 remove flight test Nikolaj Bjorner 2025-12-21 14:40:43 -08:00
  • 5bc60ce055 dont pop to base level when sharing units, manual filter Ilana Shapiro 2025-12-21 14:39:19 -08:00
  • 0c8a219fc4 next flight test Nikolaj Bjorner 2025-12-21 13:36:57 -08:00
  • 079f30d160 Limit parallelism to avoid QEMU compiler crashes copilot/request-lower-glibc-baseline copilot-swe-agent[bot] 2025-12-21 21:33:49 +00:00
  • cfcd2553fd Fix ARM64 build: improve Docker command structure copilot-swe-agent[bot] 2025-12-21 21:30:34 +00:00
  • a0554b154a update to macos-latest Nikolaj Bjorner 2025-12-21 12:17:09 -08:00
  • 880cf0129b naming convention Nikolaj Bjorner 2025-12-21 12:14:13 -08:00
  • feda43a2ac indent Nikolaj Bjorner 2025-12-21 12:13:02 -08:00
  • db46a1195b flight test copilot generated slop? Nikolaj Bjorner 2025-12-21 11:56:19 -08:00
  • 903f4d9261 wip Nikolaj Bjorner 2025-12-21 10:09:37 -08:00
  • ed5312fbe4 fix #8097 Nikolaj Bjorner 2025-12-21 10:02:35 -08:00
  • 10567413d0
    Merge 7652d5a3e4 into 5ceb312f41 Don Syme 2025-12-21 15:02:51 +01:00
  • 5ceb312f41
    Update docs.yml Nikolaj Bjorner 2025-12-20 18:59:42 +00:00
  • c36cb2f516 dont collect clauses twice Ilana Shapiro 2025-12-20 09:36:30 -08:00
  • e0a71cd2b4 index bug Lev Nachmanson 2025-12-20 06:52:34 -10:00
  • 5166d9111b better sort of root functions Lev Nachmanson 2025-12-19 16:09:02 -10:00
  • 06658a1fd7
    Fix docs.yml workflow: specify working directory for npm commands (#8098) Copilot 2025-12-20 02:03:54 +00:00
  • e11bf4b9b1 collect shared clauses inside share units after pop to base level (might help NIA) Ilana Shapiro 2025-12-19 17:15:39 -08:00
  • 5fcc5efedd Fix docs.yml build by adding working-directory to npm steps copilot/fix-docs-yml-build copilot-swe-agent[bot] 2025-12-19 22:42:50 +00:00
  • b4a5a974ab t Lev Nachmanson 2025-12-19 12:37:22 -10:00
  • 05baaf4979 Initial plan copilot-swe-agent[bot] 2025-12-19 22:36:17 +00:00
  • ca62133a56 na Nikolaj Bjorner 2025-12-19 14:13:14 -08:00
  • 6584084d6a set build directory Nikolaj Bjorner 2025-12-19 13:49:24 -08:00
  • 1220352767 make build directory configurable Nikolaj Bjorner 2025-12-19 13:43:36 -08:00
  • baded7fa5a
    Refactor documentation workflow to simplify installation Nikolaj Bjorner 2025-12-19 21:14:20 +00:00
  • 8f73a29136
    Fix Z3BUILD environment variable in docs workflow Nikolaj Bjorner 2025-12-19 20:54:03 +00:00
  • 38a0cc1ef9 set build be configurable by env Nikolaj Bjorner 2025-12-19 12:51:36 -08:00
  • c817cf4cb0 cleanup and more caching Lev Nachmanson 2025-12-19 08:42:34 -10:00
  • b4c7764aad playing around with clause sharing with some arith constraints (complicated version commented out) Ilana Shapiro 2025-12-18 22:48:57 -08:00
  • abd8b51ece fix build dir Nikolaj Bjorner 2025-12-18 20:46:42 -08:00
  • 2f6f5ff227 try adding wasm as separate step Nikolaj Bjorner 2025-12-18 20:10:26 -08:00
  • 792434e45f
    Update docs.yml Nikolaj Bjorner 2025-12-19 03:52:55 +00:00
  • 5e22b82b61
    Modify docs.yml to generate JS documentation Nikolaj Bjorner 2025-12-19 03:21:47 +00:00
  • f901646e08 enable js Nikolaj Bjorner 2025-12-18 19:12:53 -08:00
  • 909e41ce9c include paramters Nikolaj Bjorner 2025-12-18 17:32:57 -08:00
  • 1dcc960368 t Lev Nachmanson 2025-12-18 13:39:21 -10:00
  • 1cccbfdcf3 updated with env ocaml Nikolaj Bjorner 2025-12-18 14:00:50 -08:00
  • 89e5e294fc update doc Nikolaj Bjorner 2025-12-18 13:39:45 -08:00
  • f291908e58
    Fix docs.yml workflow: update actions to v4 (#8095) Copilot 2025-12-18 21:33:09 +00:00
  • 3fc47dbeed Fix docs.yml workflow: update GitHub Actions to valid versions copilot-swe-agent[bot] 2025-12-18 21:22:35 +00:00
  • 0469e0b839 Initial plan copilot-swe-agent[bot] 2025-12-18 21:17:41 +00:00
  • 382d184ee2 docs with ml bindings Nikolaj Bjorner 2025-12-18 13:08:23 -08:00
  • 897724964c fix indentation Nikolaj Bjorner 2025-12-17 09:46:41 -08:00
  • 3469dda936
    Modify docs.yml for deployment settings Nikolaj Bjorner 2025-12-18 20:51:36 +00:00
  • 89f35c95c8 Revert "make normalize optional" Lev Nachmanson 2025-12-18 10:47:40 -10:00
  • 7ec6c09a14
    Update publish directory for documentation deployment Nikolaj Bjorner 2025-12-18 20:27:29 +00:00
  • 7e9dea9bc7
    Update docs.yml Nikolaj Bjorner 2025-12-18 20:27:01 +00:00
  • c80cfb0b8e make normalize optional Lev Nachmanson 2025-12-18 10:02:51 -10:00
  • 2a3f874883
    Deploy docs to z3prover.github.io organization pages (#8094) Copilot 2025-12-18 19:39:04 +00:00
  • 6129fcec6d Deploy docs to z3prover.github.io organization pages copilot-swe-agent[bot] 2025-12-18 19:08:47 +00:00
  • 1caa31386d Initial plan copilot-swe-agent[bot] 2025-12-18 19:04:40 +00:00
  • e7a107bd21 inprocessing flag Ilana Shapiro 2025-12-17 22:41:21 -08:00
  • af2ef1c171 t Lev Nachmanson 2025-12-17 20:12:48 -10:00
  • 0c0142d6bb optimizations by using cached psc Lev Nachmanson 2025-12-17 15:34:05 -10:00
  • c37adafe12 handle the zero case in add_ord_inv_resultant Lev Nachmanson 2025-12-17 10:49:31 -10:00
  • 04d9504cc3
    Simplify CI workflow by removing emscripten steps Nikolaj Bjorner 2025-12-17 20:28:16 +00:00
  • 9ffc7e4b80
    Add working directory for wasm build step Nikolaj Bjorner 2025-12-17 19:39:30 +00:00
  • a912bfe05d
    Update docs.yml Nikolaj Bjorner 2025-12-17 18:12:39 +00:00
  • 470d660cee
    Update docs.yml Nikolaj Bjorner 2025-12-17 18:09:34 +00:00
  • fc72855e55
    Fix docs.yml workflow: resolve WASM/native library conflict in documentation generation (#8093) Copilot 2025-12-17 17:18:33 +00:00
  • 543a473993
    Update nlsat_explain.cpp nl2lin Lev Nachmanson 2025-12-16 17:55:26 -10:00
  • 9933500365 use new arithmetic solver for AUFLIA, fixes #8090 Nikolaj Bjorner 2025-12-16 16:09:37 -08:00
  • dec12aa500 Fix docs.yml: Build native Z3 Python bindings before WASM to avoid library conflicts copilot-swe-agent[bot] 2025-12-17 00:06:46 +00:00
  • f6936f7c22 Initial plan copilot-swe-agent[bot] 2025-12-17 00:02:12 +00:00
  • 60926e0347 fix #8092 Nikolaj Bjorner 2025-12-16 15:49:41 -08:00
  • 24769b5ac0 Remove UNREACHABLE() macros from nra_solver.cpp constraint validation copilot/fix-assertion-violation-nra-solver copilot-swe-agent[bot] 2025-12-16 23:34:55 +00:00
  • c8d5165cac Initial plan copilot-swe-agent[bot] 2025-12-16 23:15:21 +00:00
  • 9a09b10cea
    Fix docs.yml workflow: remove conflicting native build step (#8091) Copilot 2025-12-16 23:14:55 +00:00
  • cfe120a45e Fix docs.yml workflow to properly build and deploy documentation copilot/fix-action-docs-yml copilot-swe-agent[bot] 2025-12-16 23:03:25 +00:00
  • baccd78e0a Initial plan copilot-swe-agent[bot] 2025-12-16 22:57:15 +00:00
  • 8cc1d12555 merge Nikolaj Bjorner 2025-12-16 14:15:05 -08:00
  • a6f44f8c88 Merge branch 'master' into nl2lin Lev Nachmanson 2025-12-16 11:47:13 -10:00
  • 9fc7e6cfe0 unsound state Lev Nachmanson 2025-12-16 09:17:21 -10:00
  • 55150f36c5 unsound state Lev Nachmanson 2025-12-16 09:14:52 -10:00
  • 0782563e0c add user params Ilana Shapiro 2025-12-16 10:41:06 -08:00
  • 429771e5b7
    BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) h-vetinari 2025-12-17 04:50:37 +11:00
  • 9f7e304ee8
    Update docs.yml Nikolaj Bjorner 2025-12-16 17:36:42 +00:00
  • 818afaf4b5
    Add defaults for job run working directory Nikolaj Bjorner 2025-12-16 17:16:21 +00:00
  • b82287dc25
    Update docs.yml Nikolaj Bjorner 2025-12-16 16:49:05 +00:00