Commit Graph

  • 4dec7b1324 simplify skill scripts: expose find_repo_root, fix split string, simplify label code-simplifier/skill-scripts-cleanup-4bc53e9e7fe7fe0e github-actions[bot] 2026-06-08 05:59:22 +00:00
  • 59bb444694 include skills master Nightly Nikolaj Bjorner 2026-06-07 14:18:21 -07:00
  • 1f5132c396 refactor solver to include settable stats Nikolaj Bjorner 2026-06-07 14:17:25 -07:00
  • 2738e4317f tuning derive Nikolaj Bjorner 2026-06-07 09:10:02 -07:00
  • 37ce61ddc2 remove local copies of benchmarks Nikolaj Bjorner 2026-06-06 15:31:19 -07:00
  • 3b9dee1a7f Delete benchmarks/instance08315.smt2 Nikolaj Bjorner 2026-06-06 15:30:20 -07:00
  • 357a15cd25 Delete benchmarks/instance08175.smt2 Nikolaj Bjorner 2026-06-06 15:29:58 -07:00
  • 241c6211d6 Fix build-and-report failure by removing unsupported default FStar HO-matching flag (#9748) Copilot 2026-06-06 15:26:49 -07:00
  • ee67a94a9c tuning simplification processing Nikolaj Bjorner 2026-06-06 15:26:12 -07:00
  • d5779a6993 sls_seq_plugin: remove hard aborts in is_sat for str.len and seq.last_indexof (#9736) Copilot 2026-06-06 13:26:01 -07:00
  • 206569c0d6 fix: negate offset on swap in seq_offset_eq::find (#9722) c3 Copilot 2026-06-06 13:25:16 -07:00
  • cf58fa027d python: make Statistics doctests robust to optional ":time" counter (#9729) Julien Stephan 2026-06-06 22:24:19 +02:00
  • 2f280a7baf sls_seq_plugin: fix breakcontinue in add_substr_edit_updates (#9735) Copilot 2026-06-06 13:23:44 -07:00
  • 69c3b2e5a4 fix(ci): initialize FStar submodules in fstar-master-build workflow (#9746) Copilot 2026-06-06 13:20:12 -07:00
  • 2140f76881 Initial plan copilot/fix-failing-build-and-report-job copilot-swe-agent[bot] 2026-06-06 20:19:49 +00:00
  • 60ae0a81b7 Replace agentic F* build pipeline with standard GitHub Actions workflow (#9745) Copilot 2026-06-06 12:44:11 -07:00
  • 0d26f31ae1 Add regression coverage for root-aware seq simplifications copilot/copilotfix-euf-snode-support copilot-swe-agent[bot] 2026-06-06 19:02:45 +00:00
  • 7c6d7217d5 Fix root-aware seq plugin simplifications and loop overflow handling copilot-swe-agent[bot] 2026-06-06 19:01:07 +00:00
  • 488c9b1b37 remove AW for F* Nikolaj Bjorner 2026-06-06 11:43:13 -07:00
  • dd3c7d0d96 Initial plan copilot-swe-agent[bot] 2026-06-06 18:39:25 +00:00
  • e561387900 Handle choice_k in SMT pretty-printer switch to remove macOS -Wswitch warning (#9734) Copilot 2026-06-06 11:37:56 -07:00
  • 583775129f conservative expansions Nikolaj Bjorner 2026-06-06 11:34:26 -07:00
  • 7c7ca27822 Sounder? CEisenhofer 2026-06-06 15:24:25 +02:00
  • 3db78f043a Add agentic workflow to build FStar master against Z3 master (#9737) Copilot 2026-06-05 14:57:09 -07:00
  • 25e3db4aa3 Add agentic workflow to build latest F* master against latest Z3 master (#9733) Copilot 2026-06-05 14:45:00 -07:00
  • 001d9c9d90 init aw Nikolaj Bjorner 2026-06-05 14:35:02 -07:00
  • 7fd2a3b29b Clarify OCaml snapshot and timeout in fstar-build.md copilot/latest-master-z3-fstar-build copilot-swe-agent[bot] 2026-06-05 21:16:43 +00:00
  • d9f68584b2 Add fstar-build.md agentic workflow copilot-swe-agent[bot] 2026-06-05 21:15:48 +00:00
  • f40eb62e83 handle more cass with intervals Nikolaj Bjorner 2026-06-05 11:49:35 -07:00
  • eee5a9dcef A bit of cleanup CEisenhofer 2026-06-05 20:26:58 +02:00
  • 67906da97a Corrected string extraction CEisenhofer 2026-06-05 19:57:00 +02:00
  • 8ac7a242eb Z3 arguments got ignored in the Nielsen graph CEisenhofer 2026-06-05 19:19:08 +02:00
  • c20bc0e631 First attempt for monadic decomposition CEisenhofer 2026-06-05 18:40:36 +02:00
  • 120b4e4712 cr updates Nikolaj Bjorner 2026-06-05 01:37:10 -07:00
  • ed2c64208d intervals Nikolaj Bjorner 2026-06-04 18:21:26 -07:00
  • 40c8bf1dcd Initial plan copilot/zipt-review-sls-seq-plugin-code-quality-improvemen copilot-swe-agent[bot] 2026-06-05 01:16:42 +00:00
  • 108ee49bfc Initial plan copilot/zipt-review-sls-seq-plugin-code-improvements copilot-swe-agent[bot] 2026-06-05 01:15:34 +00:00
  • dc8179212e Add interval-based range simplification for ITE conditions Nikolaj Bjorner 2026-06-04 16:59:59 -07:00
  • cfc5b4d096 Bump github/gh-aw-actions from 0.77.0 to 0.78.1 (#9714) dependabot[bot] 2026-06-04 16:14:19 -07:00
  • ab85754eb3 Bump actions/checkout from 6.0.2 to 6.0.3 (#9715) dependabot[bot] 2026-06-04 16:14:05 -07:00
  • 5ebf5a0d9f Fix quoting in low-level pretty printer (#9716) Can Cebeci 2026-06-04 15:48:27 -07:00
  • ebdbf83314 Fix regression timeouts via range condition simplification Nikolaj Bjorner 2026-06-04 12:16:56 -07:00
  • 87c22204a4 ci(nightly): remove issue-oracle steps (moved to Z3Prover/bench) (#9712) Lev Nachmanson 2026-06-04 18:01:34 +00:00
  • 98ce7f5d05 Cleanup thanks to Copilot (#9709) Hari Govind V K 2026-06-04 18:46:33 +01:00
  • 6aea54fdad Fix derivative instability and recursion bugs Nikolaj Bjorner 2026-06-04 10:43:08 -07:00
  • d4530b2f0e ci(nightly): authenticate clone of private Z3Prover/bench repo fix/nightly-bench-private-auth Lev Nachmanson 2026-06-04 10:25:09 -07:00
  • 07cea49e4b Address PR review: push_path helper, lbool eval_cond, fix year Nikolaj Bjorner 2026-06-04 08:29:44 -07:00
  • ca238a9107 Address PR review: subsumption, is_value, simplify_ite fixes Nikolaj Bjorner 2026-06-04 07:45:19 -07:00
  • 400fe313d9 ci(nightly): always-on issue-oracle smoke test (~2 min, never fails the build) (#9688) Lev Nachmanson 2026-06-04 00:35:43 +00:00
  • 3afd83103a Address PR review comments: cache, simplify_ite_rec, itos Nikolaj Bjorner 2026-06-03 17:16:23 -07:00
  • a77155a5c4 Port reverse normalization into derive class Nikolaj Bjorner 2026-06-03 15:29:30 -07:00
  • f8925ca6fa Add simplify_ite_rec and eval for two-phase derivative Nikolaj Bjorner 2026-06-03 14:25:03 -07:00
  • b2401b87db Remove redundant min_gen_match search (#9696) Can Cebeci 2026-06-03 13:36:51 -07:00
  • 14746d7fb6 Update used_enodes properly (#9695) Can Cebeci 2026-06-03 13:36:37 -07:00
  • 7dc25e73d5 make reset private Nikolaj Bjorner 2026-06-03 11:41:37 -07:00
  • 9aca2edcfc updates per PR comments Nikolaj Bjorner 2026-06-03 11:32:32 -07:00
  • cb2cf913e3 move seq_derive and fix include paths, remove antimirov code Nikolaj Bjorner 2026-06-03 11:04:19 -07:00
  • 1f28fd0e6b Add seq::derive class for symbolic regex derivatives Nikolaj Bjorner 2026-06-03 10:36:19 -07:00
  • 9de196b3cb Some signatures changed after merging in master CEisenhofer 2026-06-03 17:39:09 +02:00
  • 043c6c0ad1 Merge branch 'master' into c3 CEisenhofer 2026-06-03 17:33:26 +02:00
  • d64ce41b2e Remove unused defined_names artifacts and simplify fingerprint_set::contains (#9702) Copilot 2026-06-03 08:16:46 -07:00
  • 1d706e875c Handle SIGXCPU like a regular timeout (#9697) Clément Pit-Claudel 2026-06-03 16:26:38 +02:00
  • 922f49e187 Fix MBP QEL soundness bug in datatype accessor elimination (#9571) (#9692) Hari Govind V K 2026-06-03 15:23:21 +01:00
  • e94b6db8e5 Removed assertion to make the build dependencies acyclic CEisenhofer 2026-06-03 10:58:25 +02:00
  • bc4e26233d Remove unused defined_names and simplify contains return code-simplifier/remove-unused-defined-names-fed46dd0fdcfc07b github-actions[bot] 2026-06-03 05:59:33 +00:00
  • a0a3047e36 remove side definitions Nikolaj Bjorner 2026-06-02 21:43:55 -07:00
  • ab259b6830 add depth guard Nikolaj Bjorner 2026-05-31 17:41:34 -07:00
  • 77f8b33794 re-enable unit tests Nikolaj Bjorner 2026-06-02 10:39:41 -07:00
  • 2dbe233f6a fix condition that skipped mbqi Nikolaj Bjorner 2026-06-01 19:56:54 -07:00
  • eaf7562a1d disable test in tptp, move to native lambdas Nikolaj Bjorner 2026-06-01 19:05:28 -07:00
  • 3e0a350411 Comment out ho_curried_application and ho_choice_expression tests Nikolaj Bjorner 2026-06-02 08:47:43 -07:00
  • 3908016651 Potentially fixed termination problem with projection operators CEisenhofer 2026-06-02 17:04:31 +02:00
  • 156bf81349 simplify model_core.h: remove unused typedef, fix trailing whitespace, simplify get_some_const_interp code-simplifier/model-core-cleanup-53966070efa0376a github-actions[bot] 2026-06-02 05:55:22 +00:00
  • 78a7b4d3a6 Update model_core.h Nikolaj Bjorner 2026-06-01 19:47:40 -07:00
  • 358378a6f0 remove tptp from all Nikolaj Bjorner 2026-06-01 19:36:18 -07:00
  • 94b981024e set up udoc relation to use datalog engine Nikolaj Bjorner 2026-06-01 17:19:50 -07:00
  • c4366e57f8 Update udoc_relation.cpp Nikolaj Bjorner 2026-06-01 17:22:06 -07:00
  • 947af23fc4 [code-simplifier] Align choice axiom naming in theory_array_full (#9660) Copilot 2026-06-01 16:03:42 -07:00
  • b0536c3998 Bump github/gh-aw-actions from 0.76.1 to 0.77.0 (#9661) dependabot[bot] 2026-06-01 16:01:32 -07:00
  • 8ddd435835 Fix misleading generation number in trace (#9687) Can Cebeci 2026-06-01 16:00:59 -07:00
  • d025b34606 prepare for enodes over lambdas Nikolaj Bjorner 2026-06-01 13:00:35 -07:00
  • 705569df24 add include directive Nikolaj Bjorner 2026-06-01 11:39:18 -07:00
  • 5b41c6eb9f Better tracking for debugging CEisenhofer 2026-06-01 19:50:34 +02:00
  • 2da7c7b3db Cache result of Z3 emptiness checks CEisenhofer 2026-06-01 17:53:28 +02:00
  • 1637b006c5 Output automaton CEisenhofer 2026-06-01 17:29:09 +02:00
  • ebdf031c8f ensure engine is datalog for dl_table and dl_util tests Nikolaj Bjorner 2026-05-31 15:32:23 -07:00
  • 24e5a6ae3f ensure base class has propagation Nikolaj Bjorner 2026-05-30 22:21:15 -07:00
  • a595e98707 fix regression: m_tmp_diseq has 0 arguments, you have to access the expression Nikolaj Bjorner 2026-05-30 18:57:21 -07:00
  • dbe986fdf7 move closure conversion to solver internalization Nikolaj Bjorner 2026-05-30 18:41:37 -07:00
  • 2cc4422018 use expr based access to enodes to allow for storing first-class lambas Nikolaj Bjorner 2026-05-30 15:12:56 -07:00
  • 5f3088f3b5 CI: validate libz3.dylib architecture on macOS to prevent #9662 regression (#9669) Lev Nachmanson 2026-05-29 16:00:36 -07:00
  • 767caa8e97 Add macOS artifact architecture checks in release workflow copilot/fix-z3-on-macos-x86-64 copilot-swe-agent[bot] 2026-05-29 21:05:47 +00:00
  • dacb3758bf Initial plan copilot-swe-agent[bot] 2026-05-29 20:51:16 +00:00
  • 30df8e7ece build warnings Nikolaj Bjorner 2026-05-29 10:14:16 -07:00
  • cebe57dffa Avoid unnecessary regex cycle splits CEisenhofer 2026-05-29 19:14:08 +02:00
  • 70031b674c Added real projection operator CEisenhofer 2026-05-29 15:51:35 +02:00
  • 48bcee8e62 add lambda-t case in addition to p-lambda case Nikolaj Bjorner 2026-05-29 01:15:59 -07:00
  • ff99cb442a Unique name for decomposed regex CEisenhofer 2026-05-28 18:45:48 +02:00
  • e5d5b493d3 Remove trivial membership constraints also after simplifications CEisenhofer 2026-05-28 18:26:50 +02:00
  • b74e35f4fb Fix mpz_manager leak in algebraic root comparison (#9654) Copilot 2026-05-28 09:06:05 -07:00