ada/alt-ergo
0
0
Fork 0
mirror of https://github.com/AdaCore/alt-ergo.git synced 2026-02-12 12:39:26 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • cd90f7dcbc Merge branch 'topic/kanig-1154-262' into 'master' master Johannes Kanig 2026-01-16 09:23:16 +00:00
  • 7002844bdc Merge Alt-ergo 2.6.2 into AdaCore master Johannes Kanig 2026-01-09 11:46:19 +09:00
  • 2dbd1412dd Merge branch 'topic/kanig-854-fsf' into 'master' 26.2 26.1 26.0 Johannes Kanig 2025-05-20 09:26:18 +00:00
  • 5f88ba9237 remove zip dependency of alt-ergo Johannes Kanig 2022-06-13 17:25:19 +09:00
  • 9c343c8a81 Use the same runners as other FSF builds Johannes Kanig 2025-05-13 16:44:31 +09:00
  • ddde9db398 Build instructions for Alt-ergo 2.6 Johannes Kanig 2025-04-22 18:17:29 +09:00
  • 44298932d6 Merge branch 'topic/kanig-854-zlib' into 'fsf-15' fsf-15-1.1 fsf-15 Johannes Kanig 2025-05-19 09:23:14 +00:00
  • ce12856758 remove zip dependency of alt-ergo Johannes Kanig 2022-06-13 17:25:19 +09:00
  • 205456a620 Merge branch 'topic/kanig-854-runners' into 'fsf-15' Johannes Kanig 2025-05-15 09:09:28 +00:00
  • 56c712d725 Add Linux arm builds for FSF 15 Johannes Kanig 2025-05-15 09:23:32 +09:00
  • 558e83fd9d Merge branch 'topic/kanig-854-runners' into 'fsf-15' Johannes Kanig 2025-05-13 09:08:24 +00:00
  • ea03811720 Use correct runners for ARM and x86_64 Johannes Kanig 2025-05-13 16:44:31 +09:00
  • 24b46f6373 Merge branch 'topic/kanig-918-ci' into 'master' Johannes Kanig 2025-05-09 09:22:49 +00:00
  • dad8986276 Windows and Linux CI for alt-ergo Johannes Kanig 2025-05-09 09:51:18 +09:00
  • 24b08949af Merge branch 'topic/kanig-854-workflow' into 'fsf-15' Johannes Kanig 2025-05-08 01:23:09 +00:00
  • 0b37d822e1 Build instructions for Alt-ergo 2.6 Johannes Kanig 2025-04-22 18:17:29 +09:00
  • a7c4d23bcf Changelog for v2.6.2 Basile Clément 2025-04-30 17:21:52 +02:00
  • acb89d1bb7 Add set_produce_models backport Basile Clément 2025-04-29 15:53:33 +02:00
  • ec5dfb0329 Expose the map in ModelMap, and add find and fold functions over that map Hichem R. A. 2024-10-09 21:17:48 +02:00
  • de4fd979a4 Add Translate -> D_cnf alias Basile Clément 2025-04-29 15:49:29 +02:00
  • 5c5e5e7943 Add Loc.from_dolmen_loc Basile Clément 2025-04-29 15:46:04 +02:00
  • d01e636629 Merge branch 'topic/kanig-900-steps' into 'master' Johannes Kanig 2025-04-28 23:18:06 +00:00
  • 6a6b11bf85 Bump Alt-ergo version Johannes Kanig 2025-04-28 11:33:45 +09:00
  • a2514833be Merge 2.6.x branch into AdaCore master Johannes Kanig 2025-04-28 11:19:53 +09:00
  • 80cf48b3b8 Changelog for v2.6.1 Basile Clément 2025-04-15 19:17:20 +02:00
  • 76bfa28beb Report the number of steps that trigger the bound (#1317) Basile Clément 2025-04-15 15:46:26 +02:00
  • 07a3d2d9ae fix: Break potentially infinite loop with steps counter (#1316) Basile Clément 2025-04-15 13:52:12 +02:00
  • 4f97747fec Catch Step_limit_reached consistently with Timeout Basile Clément 2024-10-03 11:11:44 +02:00
  • 8d66087c36 packaging: Avoid Cmdliner 2.0 (#1308) Basile Clément 2025-03-10 14:02:41 +01:00
  • 335bf2d6ae Merge branch 'topic/kanig-525-merge' into 'master' Johannes Kanig 2025-03-06 00:56:34 +00:00
  • b3383f50aa fix version typo Johannes Kanig 2025-02-21 18:39:28 +09:00
  • 1f68b2fd05 Merging Upstream 2.6.x branch into AdaCore master Johannes Kanig 2025-01-21 18:52:09 +09:00
  • e3d0de5634 build: opam dependencies Basile Clément 2024-09-24 15:40:20 +02:00
  • af8193ed37 doc: Add examples for ae.float primitives (#1239) (#1240) Basile Clément 2024-09-20 10:31:48 +02:00
  • 1b9c8267e9 fix: Make sure model generation is complete for more operators (#1234) (#1238) Basile Clément 2024-09-18 09:39:00 +02:00
  • 74d1529efe fix: Do not load preludes twice (#1235) (#1237) Basile Clément 2024-09-18 09:38:32 +02:00
  • d99264b13d Update the CHANGES file (#1218) Pierrot 2024-09-05 12:12:36 +02:00
  • 8c44c7a22c Update sphinx doc 2.6.0 (#1231) Pierrot 2024-09-05 09:51:33 +02:00
  • 53520cf2d0 Add an optimize test (#1230) Pierrot 2024-08-30 16:29:37 +02:00
  • b66421ed6e fix(BV): Do not build unnormalized values in zero_extend (#1226) Basile Clément 2024-08-30 13:31:53 +02:00
  • a3f17d7ed3 feat(BV): Support binary distinct on arbitrary bit-widths (#1222) Basile Clément 2024-08-30 12:14:32 +02:00
  • 52afc73906 fix(opt): Only perform optimization when building a model (#1224) Basile Clément 2024-08-30 11:51:30 +02:00
  • 632318979a chore(warnings): Drop acts_add_lit_view (#1227) Basile Clément 2024-08-30 10:46:28 +02:00
  • 05b2d1650d fix(CP): Make sure domains do not overflow the default domain (#1225) Basile Clément 2024-08-29 12:08:42 +02:00
  • 6d544338f1 Wrap the library Alt_ergo_prelude (#1223) Pierrot 2024-08-28 17:18:15 +02:00
  • 8728bf75f7 fix(BV, CP): Run cross-propagators to completion (#1221) Basile Clément 2024-08-28 11:55:48 +02:00
  • 68850d401e Remove some polymorphic hashtables (#1219) Pierrot 2024-08-26 12:00:07 +02:00
  • 700d5e8f56 Remove instructions to install AE on Debian (#1217) Pierrot 2024-08-22 15:19:58 +02:00
  • 0f1337d4ec Add documentation for Windows support (#1216) Pierrot 2024-08-22 15:10:10 +02:00
  • 8fa8b38a60 Use logs in Adt_rel (#1207) Pierrot 2024-08-22 14:56:50 +02:00
  • dfcc9008ea Minimal Logs integration (#1206) Pierrot 2024-08-22 14:05:32 +02:00
  • 1445b14069 chore(BV, CP): Refactor propagation mechanism (#1185) Basile Clément 2024-08-20 12:20:54 +02:00
  • 28819ec677 Deprecate debug flags (#1204) Pierrot 2024-08-20 11:57:24 +02:00
  • b7c53d3c82 feat(BV): Add support for bv2nat/int2bv normal forms (#1154) Basile Clément 2024-08-20 11:55:03 +02:00
  • dbfb6ad55b Add test from issue 1008 (#1211) Pierrot 2024-08-20 11:50:52 +02:00
  • 77e01ebddd Remove gtk-lang file (#1208) Pierrot 2024-08-20 11:48:01 +02:00
  • e610f6ae3e fix(BV): Internalize sign_extend and repeat (#1192) Basile Clément 2024-08-19 09:46:00 +02:00
  • 0d6300ec27 Restore Windows CI on Cygwin (#1203) Pierrot 2024-08-09 14:46:35 +02:00
  • d70635fdfc Remove warnings (#1202) Pierrot 2024-08-09 14:45:45 +02:00
  • 4fdcf811e6 Use dynamic_include to include the generated file dune.inc (#1199) Pierrot 2024-08-09 12:57:15 +02:00
  • 59dd69976b Ignore :reproducible-resource-limit on non-Unix plateform (#1200) Pierrot 2024-08-09 09:52:39 +02:00
  • 6d8efd72e6 Do not use lock file for all OCaml versions (#1195) Pierrot 2024-08-08 10:11:42 +02:00
  • 6424e774ba feat(BV): Only store domains on variable parts (#1152) Basile Clément 2024-08-06 09:48:31 +02:00
  • cf5b9b3b45 fix(doc): Fix README links after #1176 Basile Clément 2024-08-05 15:07:34 +02:00
  • 8e61cedea9 fix(warn): Remove warnings when building Compat library (#1194) Basile Clément 2024-08-01 14:05:44 +02:00
  • 72f4c27637 Get rid of stdcompat (#1191) Pierrot 2024-07-31 17:14:59 +02:00
  • d3d48cbfcb Rewrite gen_link_flags in OCaml (#1189) Pierrot 2024-07-31 14:59:17 +02:00
  • f7796d1d27 Use separated headers (#1142) Pierrot 2024-07-30 12:24:53 +02:00
  • 518dcc8db7 fix(BV): Implement abstract_selectors Basile Clément 2024-07-26 17:53:48 +02:00
  • 7c472b9690 Fix MacOS static build (#1187) Pierrot 2024-07-29 17:18:20 +02:00
  • 536f01027e Use Unix eof for shell scripts (#1184) Pierrot 2024-07-29 15:06:45 +02:00
  • fb75290c9c fix(doc): Fix warnings when building doc (#1183) Basile Clément 2024-07-29 13:05:42 +02:00
  • 7cb31e2ff6 Remove invalid expected file (#1182) Pierrot 2024-07-26 18:20:44 +02:00
  • a3c090284c perf: Improve performance of literal de-duplication (#1179) Basile Clément 2024-07-26 11:14:47 +02:00
  • 4bc9573898 Fix optimization with incremental mode (#1178) Pierrot 2024-07-24 18:33:54 +02:00
  • dc8087713d Active fpa as default (#1177) Pierrot 2024-07-24 18:32:32 +02:00
  • 35be1380ee feat(doc): Versioned documentation pages (#1176) Basile Clément 2024-07-24 16:47:28 +02:00
  • 50c2baa302 Reorganize documentation Basile Clément 2024-07-22 19:08:44 +02:00
  • 521742d845 chore: Support bytecode-only environments Basile Clément 2024-07-23 08:39:33 +02:00
  • db4c25afe1 fix(AC, Arith): Use a separate namespace for AC abstractions (#1173) Basile Clément 2024-07-22 18:38:12 +02:00
  • 15e4a50a70 fix(CI): Ensure binary releases have proper version number (#1171) Basile Clément 2024-07-22 16:01:20 +02:00
  • c2e419f45a fix(BV): Do not lose explanations in bvmul (#1170) Basile Clément 2024-07-22 16:01:08 +02:00
  • 3946f4edb5 feat(BV, CP): Add bitlist propagators for add/sub (#1151) Basile Clément 2024-07-22 16:00:49 +02:00
  • 6f843ce35a Remove prerelease flags (#1167) Pierrot 2024-07-17 16:05:12 +02:00
  • a1f2e600c9 feat(BV, Opt): Support bit-vector optimization (#1165) Basile Clément 2024-07-17 12:29:09 +02:00
  • 4ce737689b Add maximize/minimize terms for matching (#1166) Pierrot 2024-07-16 18:02:10 +02:00
  • b26bcaabb7 Do not erase type constraints in Ty.fresh (#1164) Pierrot 2024-07-16 14:57:54 +02:00
  • 8e4eeead7d Use Array.fold_right in D_cnf (#1160) Pierrot 2024-07-16 14:37:53 +02:00
  • a7c2b43461 Better SMT-LIB printers for formulas (#1162) Pierrot 2024-07-16 11:19:44 +02:00
  • 2d87ce4945 Rename cstr into constr (#1159) Pierrot 2024-07-11 14:02:48 +02:00
  • ca7be7c876 chore: Update the changelog (#1158) Basile Clément 2024-07-11 12:55:15 +02:00
  • 98e13927e9 Use Dolmen attribute to store well founded order (#1153) Pierrot 2024-07-11 11:46:01 +02:00
  • 01f280a13a Bump the version of Dolmen to 0.10 (#1149) Pierrot 2024-07-09 11:40:19 +02:00
  • a7cf228f44 feat(BV): Do not store width in Bitlist (#1144) Basile Clément 2024-07-08 11:54:00 +02:00
  • 9c0bfa36be feat(BV, CP): Add propagators for bvshl and bvlshr Basile Clément 2024-03-29 16:08:38 +01:00
  • d1f278ec69 feat(BV, CP): Add propagators for bvudiv and bvurem (#1084) Basile Clément 2024-06-21 17:46:29 +02:00
  • 0a46f329c3 feat(BV, CP): Propagators for addition and multiplication (#1083) Basile Clément 2024-06-21 17:39:21 +02:00
  • 5c14a39928 feat(BV): Interval domains for bit-vectors (#1058) Basile Clément 2024-06-21 10:02:57 +02:00
  • bea37cd6d7 Remove Ty.Tunit (#1148) Pierrot 2024-06-20 13:26:48 +02:00
  • 2fc8d602a4 Simple ADTs with a single constructor are records (#1146) Pierrot 2024-06-18 13:13:39 +02:00