3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 10:33:48 +00:00

Commit graph

  • aa03ac64b6
    Merge 8e8799dbd3 into a252121945 Don Syme 2026-03-17 01:59:25 -07:00
  • 2a3b3053e9
    Merge 7d78a19f1c into ef22ae8871 Copilot 2026-03-16 21:08:47 -07:00
  • 7d78a19f1c Convert dep_source to std::variant<dep_eq, dep_mem> copilot/change-dep-source-to-variant copilot-swe-agent[bot] 2026-03-17 03:47:48 +00:00
  • af3729ef31 Initial plan copilot-swe-agent[bot] 2026-03-17 03:24:13 +00:00
  • a252121945
    Bump actions/download-artifact from 8.0.0 to 8.0.1 (#9016) master Nightly dependabot[bot] 2026-03-16 16:11:55 -07:00
  • 103bf6dc35
    Bump github/gh-aw from 0.53.4 to 0.59.0 (#9015) dependabot[bot] 2026-03-16 16:07:29 -07:00
  • cc1a801992
    Bump actions/download-artifact from 8.0.0 to 8.0.1 dependabot[bot] 2026-03-16 22:54:14 +00:00
  • 9d033f304a
    Bump actions/setup-python from 5 to 6 (#9017) dependabot[bot] 2026-03-16 15:52:45 -07:00
  • 0564dfe32b
    Bump actions/checkout from 5.0.1 to 6.0.2 (#9018) dependabot[bot] 2026-03-16 15:52:35 -07:00
  • ef22ae8871
    Replace dep_tracker uint_set with scoped_dependency_manager<dep_source> in seq_nielsen (#9014) c3 Copilot 2026-03-16 15:52:18 -07:00
  • cb1a26c668
    Bump actions/checkout from 5.0.1 to 6.0.2 dependabot[bot] 2026-03-16 22:15:28 +00:00
  • 82291afa8b
    Bump actions/setup-python from 5 to 6 dependabot[bot] 2026-03-16 22:14:45 +00:00
  • 0b535bb000
    Bump github/gh-aw from 0.53.4 to 0.59.0 dependabot[bot] 2026-03-16 22:14:07 +00:00
  • 5125858a00 fix test build: update dep_tracker usages in test files and seq_state.h copilot-swe-agent[bot] 2026-03-16 21:56:40 +00:00
  • 39bf6af870 Missing file edits CEisenhofer 2026-03-16 21:10:40 +01:00
  • e439504ec8 Delete cached substitutions completely (for now) to avoid dangling pointers after backtracking CEisenhofer 2026-03-16 21:04:47 +01:00
  • f4adcde585 add regression test for #9012: box mode mod optimization Lev Nachmanson 2026-03-16 09:47:09 -10:00
  • cdcdf263f1 replace dep_tracker uint_set with scoped_dependency_manager<dep_source> copilot-swe-agent[bot] 2026-03-16 19:05:35 +00:00
  • 84d371f2e9 Bugfix in regex overapproximation CEisenhofer 2026-03-16 19:54:12 +01:00
  • 1c232b96fd Initial plan copilot-swe-agent[bot] 2026-03-16 18:40:15 +00:00
  • f03cac6e51 fix #9012: incorrect optimization of mod in box mode Lev Nachmanson 2026-03-16 07:28:34 -10:00
  • 16f693b09a Regex intersection bug fixe CEisenhofer 2026-03-16 16:30:20 +01:00
  • 256f1bdf1a remove non-compiling timeout code Nikolaj Bjorner 2026-03-15 21:39:14 -07:00
  • 32eedde897 disable rewrite that makes nseq solving harder Nikolaj Bjorner 2026-03-15 21:36:22 -07:00
  • db8a2f4f9e update print and cancelation Nikolaj Bjorner 2026-03-15 20:43:49 -07:00
  • 7dea14f732 move statistics Nikolaj Bjorner 2026-03-15 20:09:19 -07:00
  • d137f25b65 na Nikolaj Bjorner 2026-03-15 19:58:21 -07:00
  • d15aed0d04 code organization in theory_nseq Nikolaj Bjorner 2026-03-15 19:39:53 -07:00
  • fe6efef808
    Add monthly Academic Citation & Research Trend Tracker workflow (#9007) Copilot 2026-03-15 15:39:37 -07:00
  • 99099255b6 Fix inconsistent optimization with scaled objectives (#8998) Lev Nachmanson 2026-03-15 07:02:13 -10:00
  • 5df80705aa Fix inconsistent optimization with scaled objectives (#8998) Lev Nachmanson 2026-03-15 07:02:13 -10:00
  • 47fd5ef9c6 nseq: refactor to propagate_length_constraints called from propagate() copilot/update-c3-branch-for-nseq copilot-swe-agent[bot] 2026-03-15 20:41:48 +00:00
  • dfd75ec2de nseq: use theory propagation in propagate_regex_length_bounds copilot-swe-agent[bot] 2026-03-15 20:19:38 +00:00
  • a8d91cbec0 Replace get_power_exponent() with snode::get_power_exp() across seq_nielsen copilot/update-euf-snode-support copilot-swe-agent[bot] 2026-03-15 20:01:36 +00:00
  • fbeb4b22eb
    Add missing Go Goal/FuncEntry/Model APIs and TypeScript Seq higher-order operations (#9006) Copilot 2026-03-15 12:57:44 -07:00
  • daac7d3417 Add academic-citation-tracker workflow and compiled lock file copilot-swe-agent[bot] 2026-03-15 19:43:55 +00:00
  • f01287db46 Initial plan copilot-swe-agent[bot] 2026-03-15 19:39:10 +00:00
  • 9f061b4707 refactor: use arg() accessor in get_power_base/get_power_exp copilot-swe-agent[bot] 2026-03-15 19:34:47 +00:00
  • 8fdb491c1b refactor: use arg(0)/arg(1) instead of seq_util in power accessors copilot-swe-agent[bot] 2026-03-15 19:33:01 +00:00
  • a4c9a5b2b0 add review comments Nikolaj Bjorner 2026-03-15 12:23:17 -07:00
  • 5d02828c9d Initial plan copilot-swe-agent[bot] 2026-03-15 19:14:25 +00:00
  • 6893674392
    fix: correct misleading API comments in fp.go and JavaExample.java (#9003) Copilot 2026-03-15 12:08:59 -07:00
  • 77fafec3ff Fix nseq regex gap: increase BFS limit, eager length propagation, relax precheck SAT condition copilot-swe-agent[bot] 2026-03-15 19:03:47 +00:00
  • 8105cd21c3 Fix inconsistent optimization with scaled objectives (#8998) Lev Nachmanson 2026-03-15 07:02:13 -10:00
  • ee1ebed1cf fix: correct misleading API comments in fp.go and JavaExample.java copilot-swe-agent[bot] 2026-03-15 18:17:57 +00:00
  • bb8eb7f779 fix: add missing API bindings from discussion #8992 for Go and TypeScript copilot-swe-agent[bot] 2026-03-15 18:17:24 +00:00
  • b549c50af6 Initial plan copilot-swe-agent[bot] 2026-03-15 18:14:46 +00:00
  • d5a74647c3 Initial plan copilot-swe-agent[bot] 2026-03-15 18:12:30 +00:00
  • 5fcb673c58 Initial plan copilot-swe-agent[bot] 2026-03-15 18:09:09 +00:00
  • bebad7da50
    Add numeral extraction helpers to Java API (#8978) Angelica Moreira 2026-03-15 10:36:17 -07:00
  • 1a8570ed3f
    Refactor seq_nielsen: address NSB review comments (#8993) Copilot 2026-03-15 10:35:45 -07:00
  • 9256dd66e6
    Switch memory-safety workflow from push to weekly Monday schedule (#9001) Copilot 2026-03-15 10:26:10 -07:00
  • d9298af8b8 Replace push trigger with weekly Monday schedule in memory-safety.yml copilot-swe-agent[bot] 2026-03-15 17:15:31 +00:00
  • 4e42b006f0 Initial plan copilot-swe-agent[bot] 2026-03-15 17:14:38 +00:00
  • db46d52056
    fix memory-safety-report to download artifacts via MCP tools (#8979) Angelica Moreira 2026-03-15 10:12:49 -07:00
  • d53846d501
    nseq: port ZIPT regex pre-check to fix benchmark discrepancy on regex-only problems (#8994) Copilot 2026-03-15 10:10:53 -07:00
  • bc54d45c99 Fix inconsistent optimization with scaled objectives (#8998) Lev Nachmanson 2026-03-15 07:02:13 -10:00
  • 6fb68ac010
    Nl2lin - integrate a linear under approximation of a CAD cell by Valentin Promies. (#8982) Lev Nachmanson 2026-03-15 06:13:04 -10:00
  • 702776276a
    Merge e6607df831 into cb13fa2325 Copilot 2026-03-15 13:44:49 +01:00
  • eb49d10519
    Merge 6b12bffd55 into cb13fa2325 Copilot 2026-03-15 13:44:49 +01:00
  • 9812ec2aa4
    Merge 9e96ee91dc into cb13fa2325 Copilot 2026-03-15 13:44:49 +01:00
  • cca9fe3549
    Merge f0612ab7e0 into cb13fa2325 Copilot 2026-03-15 13:44:49 +01:00
  • 5859a8c62a Fix CI: update test files for simplified simplify_and_init signature copilot-swe-agent[bot] 2026-03-15 05:14:26 +00:00
  • 2212f59704
    seq_model: address NSB review comments (#8995) Copilot 2026-03-14 21:55:32 -07:00
  • 6ee4714a5d fix a memory leak Lev Nachmanson 2026-03-14 18:35:16 -10:00
  • b2b811749a fix restore_x by recalulating new column values Lev Nachmanson 2026-03-14 14:55:44 -10:00
  • a930a8d5d4 fix restore_x by recalulating new column values Lev Nachmanson 2026-03-14 14:50:22 -10:00
  • 7b747a4d5f Port ZIPT regex pre-check and DFS node budget to address nseq benchmark discrepancy copilot-swe-agent[bot] 2026-03-14 23:55:23 +00:00
  • 0938563198 Refactor seq_nielsen: m_graph reference, accessor methods, seq_util.is_power, m.are_equal/are_distinct copilot-swe-agent[bot] 2026-03-14 23:30:43 +00:00
  • 891b2e6c8e Address code review feedback: improve null-sort handling in seq_model and some_seq_in_re copilot-swe-agent[bot] 2026-03-14 23:17:32 +00:00
  • fdec148903 Address NSB review comments in seq_model.cpp copilot-swe-agent[bot] 2026-03-14 23:15:50 +00:00
  • 988baeba05 Initial plan copilot-swe-agent[bot] 2026-03-14 23:03:36 +00:00
  • 6947698d65 add notes Nikolaj Bjorner 2026-03-14 16:03:04 -07:00
  • 36cb28b7bc Initial plan copilot-swe-agent[bot] 2026-03-14 22:54:57 +00:00
  • dc5c7750f2 Initial plan copilot-swe-agent[bot] 2026-03-14 22:54:15 +00:00
  • b5dae574ad add review notes to seq_model Nikolaj Bjorner 2026-03-14 15:49:00 -07:00
  • a66448f1c5 set check_assignment to true Lev Nachmanson 2026-03-14 12:18:46 -10:00
  • 602932e3d1 Add numeral extraction helpers to Java API Angelica Moreira 2026-03-14 20:59:11 +00:00
  • ab9d762863 disable linear approximation by default to check the merge Lev Nachmanson 2026-03-14 10:27:48 -10:00
  • cb13fa2325
    fix: create missing agentics/qf-s-benchmark.md agent prompt (#8989) Copilot 2026-03-14 12:42:11 -07:00
  • 6737fe6899 fix: create missing agentics/qf-s-benchmark.md agent prompt copilot-swe-agent[bot] 2026-03-14 19:38:45 +00:00
  • 5af2b5caa0 Initial plan copilot-swe-agent[bot] 2026-03-14 19:33:55 +00:00
  • 4c64c82cef update workflow Nikolaj Bjorner 2026-03-14 12:32:29 -07:00
  • 9026f6c952 Merge branch 'nl2lin' Lev Nachmanson 2026-03-14 09:26:20 -10:00
  • b8ac856bd3
    qf-s-benchmark: debug build + seq tracing + seq-fast/nseq-slow trace analysis (#8988) Copilot 2026-03-14 12:21:42 -07:00
  • 40b9d80ae5 more review Nikolaj Bjorner 2026-03-14 12:20:01 -07:00
  • 8ab14b4f03 Update qf-s-benchmark: debug build, seq tracing, trace analysis copilot-swe-agent[bot] 2026-03-14 19:19:13 +00:00
  • 86c4567299 Initial plan copilot-swe-agent[bot] 2026-03-14 19:15:11 +00:00
  • 744d75e8cc more review Nikolaj Bjorner 2026-03-14 12:10:12 -07:00
  • 0dc5b4eef5 add review comments Nikolaj Bjorner 2026-03-14 11:59:40 -07:00
  • 5a3dbaf9f3
    Move nseq_regex/state into smt/seq and seq_model into smt/; rename to seq_* prefix (#8984) Copilot 2026-03-14 11:45:32 -07:00
  • 7c80c3b3aa move seq_model from smt/seq/ to smt/; fix seq_state.h add_str_mem typo copilot-swe-agent[bot] 2026-03-14 18:32:12 +00:00
  • 10a6029c0e
    Remove unnecessary include for smt_context.h Nikolaj Bjorner 2026-03-14 11:09:56 -07:00
  • de2cfb82e3
    Update seq_state.h Nikolaj Bjorner 2026-03-14 11:07:41 -07:00
  • cbdf49815b seq_state: remove sgraph dep; seq_model: use snode sort for is_empty; remove NSB review comments copilot-swe-agent[bot] 2026-03-14 17:53:27 +00:00
  • 21bfb115ea
    Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983) Copilot 2026-03-14 10:46:03 -07:00
  • 9c36e9ce62
    Revise comments for clarity on sort usage Nikolaj Bjorner 2026-03-14 10:30:12 -07:00
  • aa5267cb9c
    Add comments for large exponent handling Nikolaj Bjorner 2026-03-14 10:28:21 -07:00
  • 1e27af9f7a change the default number of failures in check_assignment to 7 Lev Nachmanson 2026-03-14 07:26:58 -10:00
  • ba7b0392fe
    Add comments for regex enhancements in seq_model Nikolaj Bjorner 2026-03-14 10:26:50 -07:00