3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00

Commit graph

  • b0f7604e07 dump smt lemmas from nla_core tm Lev Nachmanson 2025-06-24 13:02:17 -07:00
  • d7f439430c compile Lev Nachmanson 2025-06-24 08:45:50 -07:00
  • e64aabafe8 dump lemmas from nla_core Lev Nachmanson 2025-06-24 07:40:06 -07:00
  • bd3e722b6b remove nuget signing steps master Nikolaj Bjorner 2025-06-24 07:18:49 -07:00
  • 23bd844212 Update RELEASE_NOTES.md Nikolaj Bjorner 2025-06-24 07:17:34 -07:00
  • 3916c451e5
    Fix: typo in z3 python api (#7693) Dongjae Lee 2025-06-24 23:13:44 +09:00
  • 756f70852e
    Fix: typo in z3 python api Dongjae Lee 2025-06-24 16:18:23 +09:00
  • d5c0ffd62e
    Merge a0c2a6a92b into 98043873d0 mikulas-patocka 2025-06-23 18:21:41 +02:00
  • 98043873d0 add -> as another array sort constructor Nikolaj Bjorner 2025-06-22 21:35:23 -07:00
  • 5ad1647061 missing ; Nikolaj Bjorner 2025-06-22 21:31:55 -07:00
  • 95ffad80c6 dealloc m_imp Nikolaj Bjorner 2025-06-20 20:21:05 -07:00
  • 218379aaca
    [WIP] Leaks (#7691) Copilot 2025-06-20 20:26:43 -07:00
  • ae21d2d98e
    Update lar_solver.cpp copilot/fix-7690 Nikolaj Bjorner 2025-06-20 20:26:02 -07:00
  • 701896afb2
    Delete leak.smt2 Nikolaj Bjorner 2025-06-20 20:25:26 -07:00
  • 43c35e4320 Complete memory leak fix: add dealloc(m_imp) to lar_solver destructor copilot-swe-agent[bot] 2025-06-20 23:47:19 +00:00
  • 3a1a8a9f14 Fix memory leak in lar_solver by adding var_register cleanup copilot-swe-agent[bot] 2025-06-20 23:16:05 +00:00
  • 6eeed84383 Initial analysis of memory leak issue copilot-swe-agent[bot] 2025-06-20 22:48:42 +00:00
  • 8babdb32ef throttle line and plane lemmas in nla_tangents_lemmas Lev Nachmanson 2025-06-20 15:22:24 -07:00
  • 5e86c97565 Initial plan for issue copilot-swe-agent[bot] 2025-06-20 22:19:55 +00:00
  • ad9d9d12fb Add normalization for to_int expressions in division by zero contexts copilot/fix-7677 copilot-swe-agent[bot] 2025-06-20 21:55:35 +00:00
  • b821aebbac Fix division by zero handling inconsistency in arithmetic rewriter copilot-swe-agent[bot] 2025-06-20 21:46:57 +00:00
  • ed34556beb Initial plan for issue copilot-swe-agent[bot] 2025-06-20 21:14:51 +00:00
  • 71289d8c48 add a parameter for debugging throttling Lev Nachmanson 2025-06-20 12:32:02 -07:00
  • e66113d4c7 replace print to std::cout by a TRACE Lev Nachmanson 2025-06-20 07:30:53 -07:00
  • 521f6a6543 throttle tangent plane lemmas Lev Nachmanson 2025-06-20 07:25:56 -07:00
  • a3c8bbb461
    Update build-win-signed-cmake.yml Nikolaj Bjorner 2025-06-19 10:18:03 -07:00
  • bce1be47b8
    Update build-win-signed.yml Nikolaj Bjorner 2025-06-19 10:17:39 -07:00
  • ffb0bd9f11
    Update nightly.yaml Nikolaj Bjorner 2025-06-19 10:12:26 -07:00
  • e37c7068ec Update nightly.yaml pr-test Nikolaj Bjorner 2025-06-19 10:08:09 -07:00
  • 740c6945c6 start throttle the repeate lemmas on monics Lev Nachmanson 2025-06-18 11:29:28 -07:00
  • ca0da698ab remove empty implementation Nikolaj Bjorner 2025-06-17 17:23:35 -07:00
  • 4203d954c6 ematching skeleton Nikolaj Bjorner 2025-06-17 17:07:39 -07:00
  • f81d9735e9
    Update prd.yml 7677-potential-issue-in-arithmetic-optimization Nikolaj Bjorner 2025-06-17 17:03:24 -07:00
  • 8f88bf9998 use is_square_free_at_sample instead of is_well_oriented Lev Nachmanson 2025-06-17 07:20:05 -07:00
  • f2912b25a2 remove debug output Lev Nachmanson 2025-06-16 20:02:12 -07:00
  • 126e06b8b6 fix the test-z3 build Lev Nachmanson 2025-06-16 18:29:08 -07:00
  • 0e71a9d11c comment and restore Lev Nachmanson 2025-06-16 17:26:26 -07:00
  • 84c8a93ca5 renaming Lev Nachmanson 2025-06-16 15:49:33 -07:00
  • 945eef7ab6 work on well-orientedness Lev Nachmanson 2025-06-16 14:07:19 -07:00
  • d4d98a76b8 use is_square_free_at_sample instead of is_well_oriented Lev Nachmanson 2025-06-17 07:20:05 -07:00
  • 411fef05d4 remove debug output Lev Nachmanson 2025-06-16 20:02:12 -07:00
  • d3e05b271c fix the test-z3 build Lev Nachmanson 2025-06-16 18:29:08 -07:00
  • 3439945a7b comment and restore Lev Nachmanson 2025-06-16 17:26:26 -07:00
  • 1a68c3f0a7 renaming Lev Nachmanson 2025-06-16 15:49:33 -07:00
  • ef965574e2 work on well-orientedness Lev Nachmanson 2025-06-16 14:07:19 -07:00
  • b2f01706be euf_completion with AC: add first cut of AC matching for top-level, add plugins and fix shared expression rewriting in ac-plugin Nikolaj Bjorner 2025-06-16 11:46:03 -07:00
  • bc312768c8 remove dependency on pattern inference Nikolaj Bjorner 2025-06-15 14:07:50 -07:00
  • cb22cdc98f remove dependency on pattern inference Nikolaj Bjorner 2025-06-15 14:00:19 -07:00
  • 20ddfc7795 sketch possible AC functionality Nikolaj Bjorner 2025-06-15 13:49:13 -07:00
  • f932d480a0 use propagation queues and hash-tables to schedule bindings Nikolaj Bjorner 2025-06-15 13:21:08 -07:00
  • 7b432ae608
    Rename labeler.yml to labeller.yml Nikolaj Bjorner 2025-06-13 10:51:04 -07:00
  • 638921457d
    Create dedup.yml Nikolaj Bjorner 2025-06-13 07:59:31 -07:00
  • 8d1e954709 introduce notion of auxiliary constraints created by nla_solver lemmas Nikolaj Bjorner 2025-06-12 20:37:51 -07:00
  • 93d5e3f28e use mk_ite utility instead of custom local function Nikolaj Bjorner 2025-06-12 16:10:08 -07:00
  • a2ad90cba1 Update bit_blaster_tpl_def.h Nikolaj Bjorner 2025-06-12 16:07:28 -07:00
  • a15e4ad1e3 #7673 Nikolaj Bjorner 2025-06-12 15:16:28 -07:00
  • e018b024c5 adding proofs to euf-completion Nikolaj Bjorner 2025-06-12 11:31:50 -07:00
  • bba10c7a88 dampen order lemmas Nikolaj Bjorner 2025-06-12 11:30:54 -07:00
  • 3927fdb55f
    enable debug logging on labeler workflow (#7681) Peli de Halleux 2025-06-12 09:39:58 -07:00
  • 077730d0cf
    enable debug logging on labeler workflow Peli de Halleux 2025-06-12 09:38:24 -07:00
  • 4584d1d78f
    Create labeler.yml Nikolaj Bjorner 2025-06-12 07:36:21 -07:00
  • 423930dbad missing files Nikolaj Bjorner 2025-06-10 16:31:13 -07:00
  • e1661759db update version to 4.15.2 Nikolaj Bjorner 2025-06-10 15:55:54 -07:00
  • b665c99d06 add missing dependencies z3-4.15.1 Nikolaj Bjorner 2025-06-09 13:05:09 -07:00
  • c387b20ac6 move smt params to params directory, update release.yml Nikolaj Bjorner 2025-06-09 10:47:22 -07:00
  • dc420332b8 use userSpecifiedTag instead of gitTag Nikolaj Bjorner 2025-06-08 20:51:06 -07:00
  • 81f4125f05 update to @1 for githubpublish action Nikolaj Bjorner 2025-06-08 19:10:19 -07:00
  • 602cfafd96 update version number of github release Nikolaj Bjorner 2025-06-08 12:57:35 -07:00
  • e8f627cde9 disable pypi publishing Nikolaj Bjorner 2025-06-08 12:46:18 -07:00
  • d37336eb07 remove trace by default from tests Nikolaj Bjorner 2025-06-08 09:22:43 -07:00
  • 98d86c6687 disable tracing in test code Nikolaj Bjorner 2025-06-08 08:08:10 -07:00
  • 4bd999c295 update release notes Nikolaj Bjorner 2025-06-07 16:18:50 -07:00
  • befbd8d702 add parameter Nikolaj Bjorner 2025-06-07 15:48:34 -07:00
  • 9d35a8c702 updates to euf-completion to Nikolaj Bjorner 2025-06-07 15:39:31 -07:00
  • 9db227dbf1 fix bug in trim code missing dependecy Nikolaj Bjorner 2025-06-07 15:39:05 -07:00
  • 2897661bb3 register completion with solver Nikolaj Bjorner 2025-06-06 20:45:49 +02:00
  • 1cd162203d make rule processing fully incremental Nikolaj Bjorner 2025-06-06 20:45:10 +02:00
  • 590b79dc54
    Fix #7623 (#7672) Christoph M. Wintersteiger 2025-06-06 19:29:04 +01:00
  • 3e75b22c94 fix build Nikolaj Bjorner 2025-06-06 19:21:11 +02:00
  • d33d6ebe83 handle build warnings Nikolaj Bjorner 2025-06-06 15:13:31 +02:00
  • 7566f088f9 vtable Nikolaj Bjorner 2025-06-06 15:02:34 +02:00
  • 08c4f73e32 add dependencies to fix build Nikolaj Bjorner 2025-06-06 13:02:48 +02:00
  • e2cf4d99fb add better bit-blasting for rotation #7673 Nikolaj Bjorner 2025-06-06 12:30:00 +02:00
  • 564830ab31 enable conditional euf-completion with (optional) solver Nikolaj Bjorner 2025-06-06 11:42:31 +02:00
  • 16452fec43 pretty printing for lp Nikolaj Bjorner 2025-06-06 11:34:28 +02:00
  • f43e26d489
    Fix #7623 Christoph M. Wintersteiger 2025-06-04 18:20:21 +01:00
  • ef284cca5d for Arie Nikolaj Bjorner 2025-06-04 14:23:52 +02:00
  • bcedb66911
    Expose z3_static target for Bazel build (#7660) Nikhil Idiculla 2025-06-03 02:51:18 -07:00
  • 043328577c Expose z3_static target for Bazel build Nikhil Idiculla 2025-05-25 19:50:46 -07:00
  • e2e54527db remove trace that accesses stale data #7668 Nikolaj Bjorner 2025-06-02 08:58:35 +02:00
  • 7f5427b839 disable assertion that checks nl lemmas if using nra core Nikolaj Bjorner 2025-05-30 14:47:31 +01:00
  • 2fc3b0730d some cleanup and functionality for tracing Nikolaj Bjorner 2025-05-30 14:46:55 +01:00
  • b4c2b455bd #7667 - add API documentation Nikolaj Bjorner 2025-05-30 11:05:51 +01:00
  • 2714dc2623 fix #7661 Nikolaj Bjorner 2025-05-29 17:46:51 +01:00
  • 819c2079cb use array instead of hash-table to track trace Nikolaj Bjorner 2025-05-29 17:40:35 +01:00
  • 257b8e91e6
    Fix out of bounds error in OCaml API (#7665) (#7666) Brandon Stride 2025-05-29 12:06:48 -04:00
  • a6a6f0323e Fix out of bounds error in OCaml API (#7665) Brandon Stride 2025-05-29 10:45:37 -04:00
  • 4b2e5adc11 enable tag classes Nikolaj Bjorner 2025-05-28 17:57:58 +01:00
  • bbb3d5379b initialize tag class circular linked list Nikolaj Bjorner 2025-05-28 17:10:23 +01:00
  • a3aee0247a remove commented out include directives to avoid confusing build scripts Nikolaj Bjorner 2025-05-28 16:07:45 +01:00