3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 07:05:35 +00:00

Commit graph

  • ff49d60e64 lexicographical version lll_cube Lev Nachmanson 2026-05-15 19:20:02 -07:00
  • c0d554362a
    Refactor static_features::update_core into auxiliary helpers copilot/refactor-complex-functions copilot-swe-agent[bot] 2026-05-15 22:24:53 +00:00
  • 2ba7d7ed70 lll-cube: weight C(B) by column tightness to favor tight-box rows Lev Nachmanson 2026-05-15 14:43:41 -07:00
  • 66231210a9 cube heuristics: count bail-infeasible SAT escape Lev Nachmanson 2026-05-15 14:32:44 -07:00
  • 8da9fc9779 lll_cube: exponential delay throttle on bail Lev Nachmanson 2026-05-15 14:08:51 -07:00
  • da9c720542 Enable lll_cube by default for testing Lev Nachmanson 2026-05-15 13:25:42 -07:00
  • 5336b2c601 Add LLL cube heuristic for integer LP (experimental, default off) Lev Nachmanson 2026-05-15 11:34:16 -07:00
  • 402643e2c2
    Merge 8e8799dbd3 into bed73a3f43 Don Syme 2026-05-15 16:50:38 +02:00
  • febe12fec2
    Merge 6b12bffd55 into bed73a3f43 Copilot 2026-05-15 16:50:37 +02:00
  • 8d21c7e857
    Merge 9e96ee91dc into bed73a3f43 Copilot 2026-05-15 16:50:37 +02:00
  • ec3a02bdf3
    Merge d3f5fd6825 into bed73a3f43 Lev Nachmanson 2026-05-15 16:50:37 +02:00
  • 89bd9ebdfe
    Merge a37003fa2d into bed73a3f43 Lev Nachmanson 2026-05-15 16:50:37 +02:00
  • 08017578dd
    Merge e503ead008 into bed73a3f43 Copilot 2026-05-15 16:50:37 +02:00
  • bed73a3f43
    Bump dotnet example target framework from netcoreapp2.0 to net8.0 (#9531) master Copilot 2026-05-14 15:17:41 -07:00
  • 83362fd098
    Merge 034fc881bb into 4f40c3d888 ValentinPromies 2026-05-14 23:14:03 +02:00
  • 4f40c3d888 fixes to tptp Nikolaj Bjorner 2026-05-14 07:31:48 -07:00
  • c34332f1c5 fixes Nikolaj Bjorner 2026-05-14 07:29:52 -07:00
  • bd9326134c
    Fix sat.smt=true model reconstruction for QF_UFBV with Bool-valued UF predicates (#9519) Copilot 2026-05-14 04:19:37 -04:00
  • d9a48ae91d fix timeout event handler Nikolaj Bjorner 2026-05-14 01:16:14 -07:00
  • a9ba041a2b
    Fix netcoreapp2.0 references in FindDotnet.cmake, CMakeLists.txt, and mk_util.py copilot-swe-agent[bot] 2026-05-14 07:26:56 +00:00
  • 7ea6e9bed4
    simplify parallel_tactical2: use std::min and consistent mk_not code-simplifier/parallel-tactical2-cleanup-4523a748528db749 github-actions[bot] 2026-05-14 05:35:11 +00:00
  • 09b75d2122 connect parallel tactical2 as side load Nightly Nikolaj Bjorner 2026-05-13 14:58:55 -07:00
  • 14174bb471 fixes to tptp front-end Nikolaj Bjorner 2026-05-13 14:56:28 -07:00
  • a5e1078172
    Silence GCC false positives in bound propagation and mpz sign-cell paths (#9530) Copilot 2026-05-13 17:24:13 -04:00
  • 20c057446c
    Update dotnet example target framework from netcoreapp2.0 to net8.0 copilot-swe-agent[bot] 2026-05-13 20:57:53 +00:00
  • 5fa7d6d63d
    Simplify parallel_tactical2.cpp for naming consistency and minor expression cleanup (#9526) Copilot 2026-05-13 16:57:52 -04:00
  • 153c6a017a fixes Nikolaj Bjorner 2026-05-13 13:40:32 -07:00
  • 61e95e5457
    Merge branch 'Z3Prover:master' into master Adriteyo Das 2026-05-14 01:34:55 +05:30
  • 8027b11427 Fix soundness bug in sat.smt incremental mode (#7990) tryh4rd-26 2026-05-14 01:33:24 +05:30
  • 1405547dc0 iterate on model construction c3 Nikolaj Bjorner 2026-05-13 11:38:02 -07:00
  • ce07160d64
    TPTP frontend: enforce implicit universal quantification for free variables and add regression coverage (#9527) Copilot 2026-05-13 13:19:14 -04:00
  • 6b69c2c048 updated code Nikolaj Bjorner 2026-05-13 10:18:51 -07:00
  • 7658141c0b
    Clean up implicit variable handling helpers in TPTP parser copilot-swe-agent[bot] 2026-05-13 15:57:34 +00:00
  • e50c22099d
    Harden scoped implicit-variable RAII in TPTP frontend copilot-swe-agent[bot] 2026-05-13 15:56:14 +00:00
  • 31269243ae
    Refine implicit variable scope handling in TPTP frontend copilot-swe-agent[bot] 2026-05-13 15:54:48 +00:00
  • 3b8a5efbac
    Fix TPTP implicit variable quantification and add regressions copilot-swe-agent[bot] 2026-05-13 15:52:06 +00:00
  • 343012eda7
    simplify parallel_tactical2 naming cast and expr_ref construction copilot-swe-agent[bot] 2026-05-13 15:49:41 +00:00
  • eac80afa3c
    Initial plan copilot-swe-agent[bot] 2026-05-13 15:29:45 +00:00
  • c2ddd27765
    Merge e6607df831 into 2f7ff62173 Copilot 2026-05-13 16:39:22 +02:00
  • bba87df6df
    Fix uninitialized and array-bounds build warnings copilot-swe-agent[bot] 2026-05-13 10:40:59 +00:00
  • 2f7ff62173
    Fix soundness bug in fpa2bv mk_to_real: wrong exponent power for negative exponents (#9513) Copilot 2026-05-13 06:11:36 -04:00
  • 6dfb5ab44f
    Add weekly TPTP front-end benchmark workflow (#9523) Copilot 2026-05-13 06:05:08 -04:00
  • 36fffb3a2f
    TPTP frontend: fix TFF numeric atom typing, decimal literals, and $uminus (#9518) Copilot 2026-05-13 06:03:53 -04:00
  • 62c8273a87
    Move Z3 build to YAML preamble steps (runs before agent loads) copilot-swe-agent[bot] 2026-05-13 10:02:19 +00:00
  • a2a3c520b3
    Fix comment discrepancies found in code review (timeout buffer 3s, clarify -T: flag and date units) copilot-swe-agent[bot] 2026-05-13 09:30:49 +00:00
  • df0abab788
    Add TPTP benchmark workflow (tptp-benchmark.md + lock file) copilot-swe-agent[bot] 2026-05-13 09:29:35 +00:00
  • 4626b7cf22
    Simplify parallel_tactical2.cpp: fix naming, cast, and expr_ref construction code-simplify/parallel-tactical2-cleanup-b3bfc19dbe2c3209 github-actions[bot] 2026-05-13 05:35:41 +00:00
  • cfb62479d1
    Fix elim_unconstrained model trail substitution for sat.smt UFBV models copilot-swe-agent[bot] 2026-05-13 02:01:48 +00:00
  • 975d34e290
    fix tptp frontend numerals decimals and uminus copilot-swe-agent[bot] 2026-05-13 01:42:53 +00:00
  • 0bd911c70d
    Initial plan copilot-swe-agent[bot] 2026-05-13 01:37:35 +00:00
  • 85465dcc66
    Add parallel_tactical2.cpp: portfolio parallel solver using the solver API (#9515) Copilot 2026-05-12 21:19:27 -04:00
  • fe84156ad7
    Initial plan copilot-swe-agent[bot] 2026-05-13 01:17:11 +00:00
  • 6b22e37606
    fix(fp): correct negative exponent handling in fp.to_real conversion copilot/fix-soundness-bug-fp-to-real copilot-swe-agent[bot] 2026-05-13 00:40:18 +00:00
  • e5e7cea767
    Improve readability: split variable declaration in mk_to_real copilot-swe-agent[bot] 2026-05-13 00:12:06 +00:00
  • a26a0da1dc
    Fix soundness bug in fpa2bv_converter::mk_to_real for negative exponents copilot-swe-agent[bot] 2026-05-13 00:11:00 +00:00
  • a4e2d91713
    Update publish workflow to use master-branch report and new discussion title copilot/test-copilot-integration copilot-swe-agent[bot] 2026-05-13 00:07:11 +00:00
  • 215f298536
    Add TPTP master-branch re-run report (500 files, z3 -T:5, 43.8% correct) copilot-swe-agent[bot] 2026-05-13 00:06:50 +00:00
  • 2894808dea
    address code review: cap conflict growth, clarify cube/split comments, use mk_or for conflict clause copilot-swe-agent[bot] 2026-05-13 00:01:08 +00:00
  • 7313174b6a
    add parallel_tactical2.cpp: portfolio parallel solver using solver API copilot-swe-agent[bot] 2026-05-12 23:59:31 +00:00
  • bb9a714124
    Fix: add mod simplification rule for (mod (+ ... k*y ...) y) = (mod (+ ...) y) copilot/investigate-z3-hang-on-constraint copilot-swe-agent[bot] 2026-05-12 23:52:29 +00:00
  • fb7a9f83d7
    Fix FPA/BV model-validation soundness bug for Array + Datatype theories (Fixes #9488) (#9500) Adriteyo Das 2026-05-13 05:03:48 +05:30
  • 4e3fbbe0d2
    Initial plan copilot-swe-agent[bot] 2026-05-12 23:32:37 +00:00
  • 4a14a67b0e
    Initial plan copilot-swe-agent[bot] 2026-05-12 23:32:18 +00:00
  • 1a2d3e0ebb
    Integrate TPTP with internal APIs via cmd_context, add embedded-string TPTP regression tests, and fix TFF arithmetic/timeout regressions (#9483) Copilot 2026-05-12 19:29:58 -04:00
  • 0814bcb7e4
    Initial plan copilot-swe-agent[bot] 2026-05-12 23:23:27 +00:00
  • a002d027a7
    Fix nightly build: use dynamic manylinux Python selection instead of hardcoded cp38-cp38 (#9511) Copilot 2026-05-12 19:09:57 -04:00
  • c7f8e52eb0
    Fix nightly build: use dynamic manylinux Python selection instead of hardcoded cp38-cp38 copilot-swe-agent[bot] 2026-05-12 23:06:21 +00:00
  • b4ddfd32ea
    Fix missing g_display_* symbol definitions for non-shell link targets copilot-swe-agent[bot] 2026-05-12 23:00:14 +00:00
  • 37bfafa407
    Add rational zero-denominator regression test for TPTP copilot-swe-agent[bot] 2026-05-12 18:54:41 +00:00
  • e0c13aee15
    Refine digit-check helper naming in TPTP frontend copilot-swe-agent[bot] 2026-05-12 18:52:50 +00:00
  • 72dae76464
    Polish TPTP parser diagnostics and type parsing details copilot-swe-agent[bot] 2026-05-12 18:51:19 +00:00
  • 4116a8acb0
    Fix TPTP parsing, arithmetic builtin mapping, and timeout handling copilot-swe-agent[bot] 2026-05-12 18:48:33 +00:00
  • 98153a8f30
    Simplify parallel SMT code: clean comments and deduplicate stat computation (#9507) Copilot 2026-05-12 14:41:20 -04:00
  • 1be583f30c
    Simplify parallel SMT code: clean comments and deduplicate stat computation copilot-swe-agent[bot] 2026-05-12 18:02:44 +00:00
  • ddf912d8a6
    Improve publish-tptp-report workflow: read report from file, dedup checks copilot-swe-agent[bot] 2026-05-12 17:45:56 +00:00
  • 3b5d075a7c
    Add workflow to publish TPTP test report as GitHub discussion copilot-swe-agent[bot] 2026-05-12 17:44:27 +00:00
  • a07922f2b7
    Add TPTP integration test report (500 files, z3 -T:5) copilot-swe-agent[bot] 2026-05-12 17:40:32 +00:00
  • 27cd086d24
    Fix python build: remove circular smt_enode.h include from seq_nielsen.cpp (#9508) Copilot 2026-05-12 13:33:02 -04:00
  • fc5095a94f
    Fix python build: remove circular smt_enode.h include from seq_nielsen.cpp copilot-swe-agent[bot] 2026-05-12 17:28:22 +00:00
  • dbbc8d1956
    Initial plan copilot-swe-agent[bot] 2026-05-12 17:26:55 +00:00
  • ed7c9b7785
    Update CMakeLists.txt Nikolaj Bjorner 2026-05-12 12:54:26 -04:00
  • 57e0a12e3a
    Bump github/gh-aw-actions from 0.71.5 to 0.74.0 (#9503) dependabot[bot] 2026-05-12 12:42:25 -04:00
  • a101c098ae
    Make manylinux Python selection dynamic in CI and release workflows (#9502) Copilot 2026-05-12 12:42:04 -04:00
  • 71d7d70080 Missing dependency bug. Still not fixed, but better now CEisenhofer 2026-05-12 14:00:50 +02:00
  • c9fb432191 The side-condition of the "if"-split belongs on the edges CEisenhofer 2026-05-12 10:30:29 +02:00
  • bb639af485 Bit more pp CEisenhofer 2026-05-12 09:29:49 +02:00
  • 22583a7abd Typo in pp: lt != le CEisenhofer 2026-05-12 09:08:47 +02:00
  • 3c82e00ff4
    Simplify parallel SMT code: clean comments and deduplicate stat computation code-simplifier/2026-05-12-parallel-cleanup-f8f49e50b64075b4 github-actions[bot] 2026-05-12 05:31:30 +00:00
  • 3991f5a2a3
    Bump github/gh-aw-actions from 0.71.5 to 0.74.0 dependabot[bot] 2026-05-12 04:23:26 +00:00
  • 8b98967451 Refactor FPA/BV soundness bug fix to be self-contained in theory_fpa tryh4rd-26 2026-05-12 09:15:53 +05:30
  • 759ab463b9
    Merge branch 'Z3Prover:master' into master Adriteyo Das 2026-05-12 09:14:06 +05:30
  • df04d935bd
    Fix mk_make include resolution for moved tptp frontend copilot-swe-agent[bot] 2026-05-12 02:02:07 +00:00
  • bdfab8528e
    Improve manylinux Python selection diagnostics in workflows copilot-swe-agent[bot] 2026-05-11 22:41:58 +00:00
  • 8161065781
    Harden manylinux Python discovery in workflows copilot-swe-agent[bot] 2026-05-11 22:41:04 +00:00
  • 9db3064f27
    Fix manylinux Python selection in CI and release workflows copilot-swe-agent[bot] 2026-05-11 22:40:05 +00:00
  • d02e9fcfab
    Final version of parallel architecture for FMCAD26 submission (#9476) Ilana Shapiro 2026-05-11 15:08:23 -07:00
  • 13a82b7c4c
    Polish tptp stream parser naming and simplify test asserts copilot-swe-agent[bot] 2026-05-11 21:11:49 +00:00
  • a8c6b0bf1b
    Move tptp frontend to cmd_context and add string API copilot-swe-agent[bot] 2026-05-11 21:10:12 +00:00
  • 30d81d3cb9 Fix FPA/BV model-validation soundness bug for Array + Datatype theories tryh4rd-26 2026-05-11 20:56:44 +05:30
  • 55ea1929e9 A bit more "dot" improvements CEisenhofer 2026-05-11 19:22:45 +02:00