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

Commit graph

  • f77123c13c enable passive, add check for bloom up-to-date master Nikolaj Bjorner 2025-07-27 17:18:23 -07:00
  • c22ea174b5
    Merge a0c2a6a92b into 67695b4cd6 mikulas-patocka 2025-07-28 06:17:55 +08:00
  • 79178f3c1b
    Merge bf771eb5a4 into 67695b4cd6 Nikolaj Bjorner 2025-07-28 06:17:51 +08:00
  • 67695b4cd6 updates to ac-plugin Nikolaj Bjorner 2025-07-27 13:38:24 -07:00
  • 07613942da Add parameter validation for selected API functions Nikolaj Bjorner 2025-07-27 13:37:19 -07:00
  • e3139d4e03 #7750 Nikolaj Bjorner 2025-07-27 10:21:39 -07:00
  • eb24488c3e
    FreshConst is_sort (#7748) humnrdble 2025-07-27 12:19:43 +02:00
  • 6b5d351248
    FreshConst is_sort humnrdble 2025-07-27 09:37:48 +02:00
  • abf92228a1
    Merge 12d4ec7eda into ad2934f8cf Copilot 2025-07-27 09:20:22 +02:00
  • a9b4e35938
    Update PARALLEL_PROJECT_NOTES.md ilana Nikolaj Bjorner 2025-07-26 17:44:29 -07:00
  • 9d0a2ae355
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-26 17:40:43 -07:00
  • ad2934f8cf fix unsound len(substr) axiom Nikolaj Bjorner 2025-07-26 15:38:25 -07:00
  • 1f8b08108c #7739 optimization Nikolaj Bjorner 2025-07-26 14:02:34 -07:00
  • 8e1a528796 ensure atomic constraints are processed by arithmetic solver Nikolaj Bjorner 2025-07-26 12:52:48 -07:00
  • 0528c86905 fix #7745 Nikolaj Bjorner 2025-07-26 12:30:42 -07:00
  • 95be0cf9ba remove verbose output Nikolaj Bjorner 2025-07-25 20:22:52 -07:00
  • 27c1ffc7fb
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 20:17:19 -07:00
  • 4c229d057d
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 20:16:12 -07:00
  • c3da87ca12
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 20:15:29 -07:00
  • 964363504c
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 20:13:06 -07:00
  • f6ec7f5381
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 20:03:52 -07:00
  • 82b4c3ea23
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 20:02:37 -07:00
  • e1eb3ace3c
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 19:35:51 -07:00
  • e54928679f add option to selectively disable variable solving for only ground expressions Nikolaj Bjorner 2025-07-25 19:15:20 -07:00
  • f2ff0adc79 more notes Nikolaj Bjorner 2025-07-25 15:52:46 -07:00
  • 9bba708f9b fix compilation Nikolaj Bjorner 2025-07-25 15:36:37 -07:00
  • f6fc5045d2
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 15:12:13 -07:00
  • 202807b317
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 15:09:03 -07:00
  • e732354259
    Update PARALLEL_PROJECT_NOTES.md Nikolaj Bjorner 2025-07-25 15:00:32 -07:00
  • 138ac63dd0 added notes Nikolaj Bjorner 2025-07-25 11:23:05 -07:00
  • 1a488bb67a indentation Nikolaj Bjorner 2025-07-25 11:00:30 -07:00
  • 01633f7ce2 respect smt configuration parameter in elim_unconstrained simplifier Nikolaj Bjorner 2025-07-24 16:22:08 -07:00
  • a6c51df144 ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Nikolaj Bjorner 2025-07-24 14:54:15 -07:00
  • ac857aaf72 add score access and reset Nikolaj Bjorner 2025-07-23 15:32:49 -07:00
  • 20b9690b01
    very basic setup (#7741) Ilana Shapiro 2025-07-23 15:26:02 -07:00
  • 41b5c64c80 very basic setup Ilana Shapiro 2025-07-23 15:24:12 -07:00
  • a2f17420ff moving to active/passive division Nikolaj Bjorner 2025-07-23 15:22:06 -07:00
  • 44cd38c9ff
    Update msvc-static-build.yml Nikolaj Bjorner 2025-07-23 10:32:56 -07:00
  • fc51067207 compile warnings Nikolaj Bjorner 2025-07-21 16:20:08 -07:00
  • 1d1a01c6cc update logging Nikolaj Bjorner 2025-07-21 16:14:14 -07:00
  • dbcbc6c3ac revamp ac plugin and plugin propagation Nikolaj Bjorner 2025-07-21 07:35:06 -07:00
  • ef93867edb Add test case for quantifier weight fix copilot/fix-7735 copilot-swe-agent[bot] 2025-07-15 16:11:15 +00:00
  • 93f9353e9c Fix default quantifier weight to prevent performance regression copilot-swe-agent[bot] 2025-07-15 16:10:18 +00:00
  • 55873e17e3 Initial plan copilot-swe-agent[bot] 2025-07-15 15:24:08 +00:00
  • b983524afc add diagnostics instrumentation to mam Nikolaj Bjorner 2025-07-12 17:52:06 -07:00
  • 383f4db14c update pretty printer to show lambdas Nikolaj Bjorner 2025-07-12 17:51:37 -07:00
  • 47a2376172 bugfix to ac-plugin Nikolaj Bjorner 2025-07-12 17:51:19 -07:00
  • 12d4ec7eda Complete datatype implementation with full Context integration and tests copilot/fix-7621 copilot-swe-agent[bot] 2025-07-12 08:09:48 +00:00
  • 46f7b5edc8 Implement core datatype functionality with TypeScript compilation success copilot-swe-agent[bot] 2025-07-12 08:05:57 +00:00
  • 695ab0c298 Complete datatype type definitions with working TypeScript compilation copilot-swe-agent[bot] 2025-07-12 07:57:09 +00:00
  • fd9d9a3323 Add datatype type definitions to types.ts (work in progress) copilot-swe-agent[bot] 2025-07-12 07:53:44 +00:00
  • 1a03669f95 Initial plan copilot-swe-agent[bot] 2025-07-12 07:32:03 +00:00
  • fd5455422e fix #7725 - proofs are only possible if context was created with proofs enabled Nikolaj Bjorner 2025-07-12 09:14:12 +02:00
  • e575919657
    debug : Add support for selecting LLDB via invoke on macOS (#7726) LeeYoungJoon 2025-07-12 16:02:09 +09:00
  • d2ada6a772 tidy nl2lin Nikolaj Bjorner 2025-07-11 22:40:55 +02:00
  • 10cb358f9f add marshaling from nlsat lemmas into core solver Nikolaj Bjorner 2025-07-11 22:29:33 +02:00
  • c3488fcfa9 add material in nra-solver to interface Nikolaj Bjorner 2025-07-11 20:02:28 +02:00
  • 5f25eb5aa2 remove confusing construction Nikolaj Bjorner 2025-07-11 19:18:35 +02:00
  • 6bcee13158 outline of interface contract Nikolaj Bjorner 2025-07-11 18:44:41 +02:00
  • 46284c434a outline of signature for assignment based conflict generation Nikolaj Bjorner 2025-07-11 18:36:28 +02:00
  • 6d1baffe16 Restrict SHA256 hash generation to source code archives only copilot/fix-7728 copilot-swe-agent[bot] 2025-07-11 16:23:40 +00:00
  • 62fa8cc12f Add SHA256 hash generation for ZIP archives in nightly and release builds copilot-swe-agent[bot] 2025-07-11 14:15:15 +00:00
  • e2eaf4ac24 Initial plan copilot-swe-agent[bot] 2025-07-11 14:09:32 +00:00
  • 0995928f6e wip - throttle AC completion, enable congruences over bound bodies Nikolaj Bjorner 2025-07-11 12:48:27 +02:00
  • 37afa6bd69 debug : Add support for selecting LLDB via invoke on macOS LeeYoungJoon 2025-07-09 13:56:29 +09:00
  • 35b1d09425 working on ho-matcher Nikolaj Bjorner 2025-07-08 04:50:43 +02:00
  • 195f3c9110 update build dependencies Nikolaj Bjorner 2025-07-07 16:50:35 +02:00
  • 0c5b0c3724 turn on ho-matcher for completion Nikolaj Bjorner 2025-07-07 14:08:51 +02:00
  • 1b3c3c2716 initial pattern abstraction and move matching to src Nikolaj Bjorner 2025-07-06 00:53:46 -07:00
  • 2d1a42d53f fixes to ho-matcher Nikolaj Bjorner 2025-07-05 16:24:45 -07:00
  • 3ccf7a695b make concurrent collect_statistics in a timeout thread safe Nikolaj Bjorner 2025-07-04 18:58:29 -07:00
  • 951554e883 ho matcher draft Nikolaj Bjorner 2025-07-04 18:01:37 -07:00
  • 0ee1ee54bd Update azure-pipelines.yml for Azure Pipelines Nikolaj Bjorner 2025-07-04 14:25:53 -07:00
  • 47714163cb try permanent ban thr Lev Nachmanson 2025-07-03 10:01:43 -07:00
  • 74f4639f0c permanent throttling Lev Nachmanson 2025-07-03 09:54:59 -07:00
  • 2b3d2ea055 another try to avoid the race with atomic swap m_ctx Lev Nachmanson 2025-07-02 18:14:29 -07:00
  • bee55f1466 Fix race condition in smt_tactic::collect_statistics copilot-swe-agent[bot] 2025-07-02 23:34:49 +00:00
  • f094053cd0 Initial plan copilot-swe-agent[bot] 2025-07-02 23:19:43 +00:00
  • 5b2226127e make sure that we do no access a null m_ctx Lev Nachmanson 2025-07-02 15:18:29 -07:00
  • d2990e2f68 use usize to suppress the data loss warnings Lev Nachmanson 2025-07-02 14:42:55 -07:00
  • f544dd4ab2 deal with warnings Nikolaj Bjorner 2025-07-02 10:59:56 -07:00
  • bb100a40d5 c is non-null Nikolaj Bjorner 2025-07-02 10:57:54 -07:00
  • 75678fc2c2
    Fix O(n²) performance issue in CLI datatype declaration processing (#7712) Copilot 2025-07-02 09:54:36 -07:00
  • 53c48f7226
    trace : Sort and reorder trace tags by tag_class and tag_name (#7714) LeeYoungJoon 2025-07-03 01:53:35 +09:00
  • 755c39873b Fix git describe command in CMake configuration copilot/fix-7715 copilot-swe-agent[bot] 2025-07-02 16:01:33 +00:00
  • e66c3f8a40 Initial plan copilot-swe-agent[bot] 2025-07-02 15:49:21 +00:00
  • 2788b8f49d Optimize get_constructor_by_name: use func_decl* parameter, add linear search optimization for small datatypes, and ensure non-null postcondition copilot/fix-7709-2 copilot-swe-agent[bot] 2025-07-02 15:11:32 +00:00
  • 0218fb75a2 fixup pipleline to support testing packaging Nikolaj Bjorner 2025-07-02 07:58:58 -07:00
  • 51c88c26ad trace : Sort and reorder trace tags by tag_class and tag_name LeeYoungJoon 2025-07-02 14:36:40 +09:00
  • dfdc31ae3b Fix the real O(n²) bottleneck with lazy hash table for constructor name lookups copilot-swe-agent[bot] 2025-07-02 04:57:04 +00:00
  • 0928a1fdf0
    trace : Classify tag_names unique to smt_internalize.cpp (#7713) LeeYoungJoon 2025-07-02 13:30:07 +09:00
  • e1cc617c4d trace : Classify tag_names unique to smt_internalize.cpp LeeYoungJoon 2025-07-02 11:26:47 +09:00
  • b518327650 Implement batch initialization fix for O(n²) datatype performance issue copilot-swe-agent[bot] 2025-07-01 21:56:53 +00:00
  • 115da30317 Initial plan copilot-swe-agent[bot] 2025-07-01 21:28:06 +00:00
  • 8de80e666b #7710 Nikolaj Bjorner 2025-07-01 14:23:23 -07:00
  • 97193b4a1d call into collect_statistics in case of -T interrupt Nikolaj Bjorner 2025-07-01 14:15:15 -07:00
  • a28f55a3bc log scope level of lemma Nikolaj Bjorner 2025-07-01 14:14:30 -07:00
  • bfed237a6c expose scope level Nikolaj Bjorner 2025-07-01 14:14:16 -07:00
  • ac27b4d6a2 fix the debug build stats Lev Nachmanson 2025-07-01 12:34:02 -07:00
  • 4c62c8a040 remove a comment Lev Nachmanson 2025-07-01 11:41:46 -07:00