3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-04 17:17:41 +00:00

Commit graph

  • af978d7c6e simplify lws Lev Nachmanson 2025-09-03 20:15:44 -10:00
  • 6eee8688c2
    Add Windows ARM64 builds to NuGet packages for nightly and release pipelines (#7847) master Copilot 2025-09-03 19:03:51 -07:00
  • 626c6e74dc Add Windows ARM64 builds to NuGet packages for nightly and release pipelines copilot/fix-18b45c8d-a44e-4dd1-8c17-ddca7b1bc5c0 copilot-swe-agent[bot] 2025-09-04 01:50:26 +00:00
  • 3224b75767 Initial plan copilot-swe-agent[bot] 2025-09-04 01:44:31 +00:00
  • e0c315bc3e filter pseudo-linear monomials Nikolaj Bjorner 2025-09-03 17:51:01 -07:00
  • 449704ef64
    Enable ARM64 support in .NET NuGet package (#7846) Copilot 2025-09-03 15:20:54 -07:00
  • 857cc974e8 t Lev Nachmanson 2025-09-03 12:17:11 -10:00
  • d8ce5c6795 t Lev Nachmanson 2025-09-03 11:39:11 -10:00
  • a9bd34c867 Enable ARM64 support in .NET NuGet package by adding Linux ARM64 and macOS ARM64 to os_info mapping copilot/fix-aa5a6b9d-9e08-422a-8863-5baf6c20e618 copilot-swe-agent[bot] 2025-09-03 21:10:48 +00:00
  • abdb760090 Initial plan copilot-swe-agent[bot] 2025-09-03 20:49:22 +00:00
  • e126362ba6
    Parallel solving (#7845) ilana Ilana Shapiro 2025-09-03 12:58:37 -07:00
  • 228bc1b90c remove the incorrect preselection functions for march and heule-schur. update explicit-hardness with bugfixes. now it works but i am not sure there is a good perf increase based on my handpicked examples. i tried several variations of hardness ratios as you can see commented out. there are debug prints still commented out. also return_cubes now takes in a single cube instead of a list C_worker to align with the single-cube hardness/should_split metrics, it doesn't change anything bc we only pass in 1 cube to begin with Ilana Shapiro 2025-09-03 12:11:57 -07:00
  • 4fec287107
    clean up (#7844) nl2lin ValentinPromies 2025-09-03 18:52:51 +02:00
  • 14fb08d54c clean up Valentin Promies 2025-09-03 13:44:03 +02:00
  • a4f9eee822 t Lev Nachmanson 2025-09-02 18:00:56 -10:00
  • 254416c4a0 merge Ilana Shapiro 2025-09-02 19:29:47 -07:00
  • a7c948088a debug in progress Ilana Shapiro 2025-09-02 19:28:29 -07:00
  • 7005d04755 propagate mod over ite even if it hurts Nikolaj Bjorner 2025-09-02 18:39:29 -07:00
  • a382ddbd8a add rewrite for mod over negation, refine axioms for grobner quotients Nikolaj Bjorner 2025-09-02 18:26:22 -07:00
  • bce5ad38a9 t Lev Nachmanson 2025-09-02 14:27:54 -10:00
  • 1f5fa63030 t Lev Nachmanson 2025-09-02 14:21:41 -10:00
  • 7e45f25364 t Lev Nachmanson 2025-09-02 12:49:57 -10:00
  • 7907e0ecaa t Lev Nachmanson 2025-09-02 12:46:00 -10:00
  • b4d94b84aa t Lev Nachmanson 2025-09-02 12:36:23 -10:00
  • 6cb86db68e t Lev Nachmanson 2025-09-02 12:16:02 -10:00
  • a7df159ea2
    Parallel solving (#7840) Ilana Shapiro 2025-09-02 14:36:35 -07:00
  • f243963927 add a lot of debug prints that need to be removed. some bugs are resolved but others remain Ilana Shapiro 2025-09-02 14:02:23 -07:00
  • de99704d42 merge Ilana Shapiro 2025-09-01 19:07:53 -07:00
  • ded70a7550 implement march and heule schur hardness functions based on sat_lookahead.cpp implementations. they seem to be buggy, need to revisit. also set up experimental params for running on polytest Ilana Shapiro 2025-09-01 18:58:50 -07:00
  • e2235d81d3 add option for gcd-test to grobner Nikolaj Bjorner 2025-09-01 16:37:21 -07:00
  • 28d316fa22
    Parallel solving (#7838) Ilana Shapiro 2025-09-01 16:36:11 -07:00
  • 042ebf5156 attempt to add different hardness functions including heule schur and march, need to re-examine/debug/evaluate Ilana Shapiro 2025-09-01 12:43:13 -07:00
  • a3024b7c77 add new attempt at hardness function Ilana Shapiro 2025-09-01 12:16:13 -07:00
  • 7af7ba6495 fix some bugs and the PQ approach is working for now. the depth sets approach is actually unsound, but I am going to focus on the PQ approach for now since it has more potential for SAT problems with the right hardness metric Ilana Shapiro 2025-08-31 18:49:14 -07:00
  • 49703f8bba remove debug out Nikolaj Bjorner 2025-08-31 17:41:42 -07:00
  • 4c0c199e32 take into account integer coefficients Nikolaj Bjorner 2025-08-31 16:07:37 -07:00
  • e91e432496 add option to propagation quotients Nikolaj Bjorner 2025-08-31 14:41:23 -07:00
  • c2c0194f3f Merge remote-tracking branch 'upstream/ilana' into parallel-solving Ilana Shapiro 2025-08-31 11:47:38 -07:00
  • 91b4873b79 categorize lp stats Nikolaj Bjorner 2025-08-29 17:05:59 -07:00
  • 06de5f422c remove str parameters Nikolaj Bjorner 2025-08-29 17:05:41 -07:00
  • a3acd962a0
    Parallel solving (#7836) Ilana Shapiro 2025-08-29 16:26:10 -07:00
  • 67f5962a81 merge Ilana Shapiro 2025-08-29 16:17:01 -07:00
  • 651b86000f debug iterative deepening some more and add first attempt at PQ (untested) Ilana Shapiro 2025-08-29 15:41:05 -07:00
  • 9d16020a06
    Use '--tags' rather than '--long' for git describe. Closes #6823 (#7833) Andrew V. Teylu 2025-08-29 22:15:38 +01:00
  • 4095d85fbc
    Use '--tags' rather than '--long' for git describe. Closes #6823 Andrew V. Teylu 2025-08-29 20:01:04 +01:00
  • 506112595a
    Parallel solving (#7832) Ilana Shapiro 2025-08-29 11:28:25 -07:00
  • a42d21fe80 fix iterative deepening bug: unsolved cube needs to get re-enqueued even if we don't split it further Ilana Shapiro 2025-08-29 10:30:15 -07:00
  • 1fae0dea16 iterative deepening experiment (no PQ yet). the hardness heuristic is still naive! Ilana Shapiro 2025-08-28 21:05:17 -07:00
  • cb4c739ee0 t Lev Nachmanson 2025-08-28 17:18:15 -10:00
  • 61d8e7d035 move a comment Lev Nachmanson 2025-08-28 17:00:47 -10:00
  • 1e6b8c55d7 Add Genaiscript for quantifier callbacks podcast generation copilot/fix-7826 copilot-swe-agent[bot] 2025-08-29 02:59:14 +00:00
  • 92b42c4b55 Add Genaiscript podcast generator for quantifier instantiation callbacks feature copilot-swe-agent[bot] 2025-08-29 02:57:42 +00:00
  • 70aafea26c work on seed_properties Lev Nachmanson 2025-08-28 16:53:57 -10:00
  • 345091d97e work on seed_properties Lev Nachmanson 2025-08-28 16:44:52 -10:00
  • 7150fdafa6 work on seed_properties Lev Nachmanson 2025-08-28 16:29:12 -10:00
  • ca2620e6ec Add implementation summary for quantifier instantiation callback documentation copilot-swe-agent[bot] 2025-08-29 01:51:04 +00:00
  • 2e031bc7fc Add comprehensive documentation and examples for UserPropagator quantifier instantiation callbacks copilot-swe-agent[bot] 2025-08-29 01:49:26 +00:00
  • f3f0171f35 Initial plan copilot-swe-agent[bot] 2025-08-29 01:23:26 +00:00
  • 3e216dbb20
    Fix method signature for onBindingWrapper, again (#7829) Karlheinz Friedberger 2025-08-29 03:21:51 +02:00
  • 645ad099ab
    Fix method signature for onBindingWrapper, again Karlheinz Friedberger 2025-08-28 22:33:21 +02:00
  • 25ce7ccfd8 rename Lev Nachmanson 2025-08-28 10:30:57 -10:00
  • bd987e4399 renaming Lev Nachmanson 2025-08-28 10:22:59 -10:00
  • a5609364dd
    Fix method signature for onBindingWrapper Nikolaj Bjorner 2025-08-28 13:04:04 -07:00
  • 187f013224
    Nl2lin (#7827) ValentinPromies 2025-08-28 17:17:37 +02:00
  • b094921dd9 use an explicit cell description in check_assignment Valentin Promies 2025-08-28 15:24:53 +02:00
  • 3a7df119be fix linear projection Valentin Promies 2025-08-28 12:52:36 +02:00
  • 8ead9e753b ttt Lev Nachmanson 2025-08-27 15:30:49 -10:00
  • 98d8083d15 preprocess the input of levelwise to drop a level Lev Nachmanson 2025-08-27 13:16:14 -10:00
  • 9ea6f2ea86 merge Ilana Shapiro 2025-08-27 15:26:14 -07:00
  • c87e7c312a rename explain::main_operator to compute_conflict_explanation Lev Nachmanson 2025-08-27 10:05:31 -10:00
  • 631a3a27cf make sure that worker state is properly deallocated Nikolaj Bjorner 2025-08-27 12:59:26 -07:00
  • ef8d2020ca comment out Nikolaj Bjorner 2025-08-27 09:30:46 -07:00
  • a57f87fbe9
    Parallel solving (#7824) Ilana Shapiro 2025-08-27 10:10:27 -07:00
  • e6afc50fdf Merge branch 'parallel-solving' of github.com:ilanashapiro/z3 into parallel-solving Ilana Shapiro 2025-08-27 10:09:11 -07:00
  • 44e3f22c8b debug the backbone crash (it was references not being counted) Ilana Shapiro 2025-08-27 10:08:48 -07:00
  • 04ef9dc655 Merge remote-tracking branch 'upstream/ilana' into parallel-solving Ilana Shapiro 2025-08-27 10:07:43 -07:00
  • 2337e68169 fix #7822 Nikolaj Bjorner 2025-08-27 09:17:55 -07:00
  • b8b9327a70
    [CMake] Document hybrid approach and fix FetchContent C++ header path issue (#7819) Copilot 2025-08-27 08:45:10 -07:00
  • a6a4ed5ea8
    Update README-CMake.md copilot/fix-7818 Nikolaj Bjorner 2025-08-27 08:44:57 -07:00
  • 92c3f32f08
    Update README-CMake.md Nikolaj Bjorner 2025-08-27 08:44:47 -07:00
  • a3bb2f070c
    Update README-CMake.md Nikolaj Bjorner 2025-08-27 08:44:40 -07:00
  • 7f559b5831
    Parallel solving (#7821) Ilana Shapiro 2025-08-26 22:22:16 -07:00
  • 7a1c5e30be
    Merge branch 'Z3Prover:master' into parallel-solving Ilana Shapiro 2025-08-26 20:07:43 -07:00
  • 5c2f244a85 depth splitting now applies to greedy+frugal unless specified otherwise Ilana Shapiro 2025-08-26 20:07:24 -07:00
  • c010a38244 attempting to add backbone code, it does not work. still debugging the error: ASSERTION VIOLATION File: /home/t-ilshapiro/z3/src/ast/ast.cpp Line: 388 UNEXPECTED CODE WAS REACHED. I left a comment on the line where it's crashing Ilana Shapiro 2025-08-26 19:44:05 -07:00
  • 1bed5a4306 remove double tweak versioning Nikolaj Bjorner 2025-08-26 09:51:11 -07:00
  • 09973c6f7a Fix NuGet package version format to use semantic versioning copilot/fix-a6d7c194-b3f3-4976-8e47-2c2a87539e70 copilot-swe-agent[bot] 2025-08-26 16:44:36 +00:00
  • 3ebd6eb97a Initial plan copilot-swe-agent[bot] 2025-08-26 16:21:43 +00:00
  • 1f92ccfe72 Fix FetchContent C++ header include path issue copilot-swe-agent[bot] 2025-08-26 02:01:41 +00:00
  • 307a8c5932 merge Ilana Shapiro 2025-08-25 15:56:41 -07:00
  • 5db6571acf sketch backbone code Nikolaj Bjorner 2025-08-25 15:23:01 -07:00
  • 6a356f78c1 Add hybrid approach documentation for CMake copilot-swe-agent[bot] 2025-08-25 19:01:51 +00:00
  • 25ff5d1446 Initial plan copilot-swe-agent[bot] 2025-08-25 18:45:53 +00:00
  • 43d2a1f5b1 rename variables Ilana Shapiro 2025-08-25 10:15:56 -07:00
  • 0fdf5bcb3f
    Fix configuration for depth splitting in notes Ilana Shapiro 2025-08-24 22:39:00 -07:00
  • 12dd705898
    Rename configuration from 'shareconflicts' to 'depthsplitting' Ilana Shapiro 2025-08-24 22:38:08 -07:00
  • 894c0e9fbe
    Bugfix: post-build sanity check when an old version of ocaml-z3 is installed (#7815) Shiwei Weng 翁士伟 2025-08-24 22:49:04 -05:00
  • 8cb093752a
    Parallel solving (#7814) Ilana Shapiro 2025-08-24 20:48:28 -07:00
  • b9256ba336
    Add new configurations for SMT parallel settings Ilana Shapiro 2025-08-24 19:45:44 -07:00
  • 0901711629 Merge branch 'parallel-solving' of github.com:ilanashapiro/z3 into parallel-solving Ilana Shapiro 2025-08-24 18:08:58 -07:00