simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 1530b761b0
         wip: leancheck wip-levels-in-kernel Simon Cruanes 2023-04-20 22:05:15 -04:00
  • 8d70c10e18
         wip: ciclib: start checking types and inductive specs Simon Cruanes 2023-03-07 23:38:31 -05:00
  • 401365e1bb
         fix Simon Cruanes 2023-03-06 23:42:37 -05:00
  • 42c6d2f770
         ciclib: beta-reduction Simon Cruanes 2023-03-06 23:38:00 -05:00
  • 6fee09848b
         leancheck: parse ind Simon Cruanes 2023-03-06 21:51:13 -05:00
  • 38133dc163
         wip: leancheck: use colors, better debug Simon Cruanes 2023-03-06 20:50:44 -05:00
  • 8f02f14d37
         feat(leancheck): handle term constructors Simon Cruanes 2023-03-05 23:08:38 -05:00
  • 0d948a9324
         feat(ciclib): adapt AST to be closer to lean proof format Simon Cruanes 2023-03-05 23:08:24 -05:00
  • b1aaff4e9f
         feat: add sidekick.cic_lib with non-hashconsed terms Simon Cruanes 2023-03-04 23:30:18 -05:00
  • a8f69a834f
         wip: feat(leancheck): parse universe commands Simon Cruanes 2023-03-02 00:07:20 -05:00
  • 75e42072f4
         wip: feat(leancheck): store intermediate objects of the proof Simon Cruanes 2023-03-01 22:37:04 -05:00
  • 39aa3d7f64
         feat(level): more judgements Simon Cruanes 2023-03-01 22:36:56 -05:00
  • 2c435a5c18
         fix(level): missing cases, inspiration from Trepplein Simon Cruanes 2023-03-01 22:16:58 -05:00
  • cd07d6924b
         details for leancheck Simon Cruanes 2023-02-28 23:38:04 -05:00
  • 70f0b3874c
         wip: feat(leancheck): start binary to check lean proofs Simon Cruanes 2023-02-28 23:28:12 -05:00
  • 0b51dd172e
         feat(level): implement level comparison Simon Cruanes 2023-02-28 22:38:12 -05:00
  • 1eeb5a464d
         test: update test with levels Simon Cruanes 2023-02-23 22:08:50 -05:00
  • 9ea96a6b61
         refactor: adapt to new levels in core Simon Cruanes 2023-02-23 22:07:55 -05:00
  • b8cbe0cf06
         feat(core-logic): add level expressions, modify type checker Simon Cruanes 2023-02-23 22:07:34 -05:00
  • 4363fc47b6
         update smtlib Simon Cruanes 2025-01-27 21:51:51 -05:00
  • 6c8d6840f8
         chore: update workflows main Simon Cruanes 2025-01-27 21:49:09 -05:00
  • 90a5c7bc06
         ocamlforamt Simon Cruanes 2025-01-27 21:49:05 -05:00
  • 8e6036bf3f
         chore: CI Simon Cruanes 2023-12-27 19:38:24 -05:00
  • 13440d60f6
         chore: CI Simon Cruanes 2023-12-27 19:31:55 -05:00
  • 2c7065e7fd deploy: eff6016151 gh-pages c-cube 2023-12-27 22:31:52 +00:00
  • eff6016151
         support trace-fuchsia if present master Simon Cruanes 2023-12-27 17:24:35 -05:00
  • 54077446ca
         require ocaml 4.08, compat with containers 3.13 Simon Cruanes 2023-12-07 00:14:16 -05:00
  • aeb7ff8b4f deploy: 85c39d3642 c-cube 2023-12-07 05:10:29 +00:00
  • 85c39d3642
         faster CI Simon Cruanes 2023-12-07 00:03:36 -05:00
  • a3e9ecf974 deploy: 43c8e60790 c-cube 2023-10-07 02:14:09 +00:00
  • 43c8e60790
         use trace instead of our own custom tracing setup Simon Cruanes 2023-10-06 22:04:15 -04:00
  • 4bb15f8b5e
         comments Simon Cruanes 2023-10-06 21:35:23 -04:00
  • c35d721c6d fix: compute model even if (potentially) new interface eqns are produced Simon Cruanes 2023-06-23 10:44:12 -04:00
  • da5cd7fbc2
         fix: compute model even if (potentially) new interface eqns are produced wip-19 Simon Cruanes 2023-06-23 10:44:12 -04:00
  • 088fe6e281 deploy: 3ebc532486 c-cube 2023-06-26 19:47:10 +00:00
  • 3ebc532486 more tests Simon Cruanes 2023-06-26 00:44:51 -04:00
  • 923cbec6e5 remove debug msg Simon Cruanes 2023-06-26 00:40:39 -04:00
  • 8d8ef4211b fix sign error Simon Cruanes 2023-06-26 00:40:31 -04:00
  • 67e9eabf43 add another bug repro Simon Cruanes 2023-06-25 15:39:28 -04:00
  • 477c780f18 CI Simon Cruanes 2023-06-23 21:42:43 -04:00
  • d8612f84c9 doc Simon Cruanes 2023-06-23 21:39:58 -04:00
  • 2e29ab20dd fix benchpress config Simon Cruanes 2023-06-23 21:26:55 -04:00
  • 3ba2583966 fix lra: define expressions occurring in subterms properly Simon Cruanes 2023-06-23 21:23:50 -04:00
  • c4d3c44c49 warnings and comments Simon Cruanes 2023-06-23 21:23:42 -04:00
  • c64bebaf6f fix warning Simon Cruanes 2023-06-23 21:22:55 -04:00
  • dcdc55ee1f add non reduced test too Simon Cruanes 2023-06-23 17:20:39 -04:00
  • 87f9be7fe0 test: add regression test for LRA bug Simon Cruanes 2023-06-23 15:54:06 -04:00
  • 7937a38416
         more tests Simon Cruanes 2023-06-26 00:44:51 -04:00
  • 55b2fa00f4
         remove debug msg Simon Cruanes 2023-06-26 00:40:39 -04:00
  • 5d07d456dc
         fix sign error Simon Cruanes 2023-06-26 00:40:31 -04:00
  • 0841e0e767
         add another bug repro Simon Cruanes 2023-06-25 15:39:28 -04:00
  • 3b78fdda87
         CI Simon Cruanes 2023-06-23 21:42:43 -04:00
  • 1d1fc88f1c
         doc Simon Cruanes 2023-06-23 21:39:58 -04:00
  • 66a155a155 deploy: 619da6fbcb c-cube 2023-06-24 01:36:40 +00:00
  • 27937b664a
         fix benchpress config Simon Cruanes 2023-06-23 21:26:55 -04:00
  • a767ca1603
         fix lra: define expressions occurring in subterms properly Simon Cruanes 2023-06-23 21:23:50 -04:00
  • 68c4acde4e
         warnings and comments Simon Cruanes 2023-06-23 21:23:42 -04:00
  • 1fe814a046
         fix warning Simon Cruanes 2023-06-23 21:22:55 -04:00
  • 0b80cdb1dc
         add non reduced test too Simon Cruanes 2023-06-23 17:20:39 -04:00
  • 4be08675a1
         test: add regression test for LRA bug Simon Cruanes 2023-06-23 15:54:06 -04:00
  • 619da6fbcb
         fix warnings Simon Cruanes 2023-06-23 20:44:01 -04:00
  • 0393fae090
         cdsat wip-ccsat Simon Cruanes 2023-05-09 20:42:24 -04:00
  • 8fbfa98fc8
         wip: union find in ccsat Simon Cruanes 2023-05-09 20:42:12 -04:00
  • 566d0d64a2
         detail wip-cdsat Simon Cruanes 2022-11-16 22:30:54 -05:00
  • f2a7489d39
         feat(cdsat): decide new variables Simon Cruanes 2022-11-06 22:37:10 -05:00
  • 3412b272fb
         fix(tvar): remove redundant has_value bitvec Simon Cruanes 2022-11-08 11:46:46 -05:00
  • 1153c21a52
         feat(cdsat): add variables (to plugins, to-decide set) Simon Cruanes 2022-11-08 11:43:38 -05:00
  • c5f00b5204
         feat(cdsat): revamp watches Simon Cruanes 2022-11-08 10:53:38 -05:00
  • c34e648148
         feat(cdsat): use Vars_to_decide to decide in main outer loop Simon Cruanes 2022-11-05 22:40:22 -04:00
  • 299acc184c
         feat(cdsat): add basic VMTF Vars_to_decide to track undecided vars Simon Cruanes 2022-11-05 22:39:48 -04:00
  • 6374fd7d5f
         wip(cdsat): start implementing propagation Simon Cruanes 2022-11-04 22:04:42 -04:00
  • 6f1abedb44
         feat(cdsat): embryo of plugins for bool and UF Simon Cruanes 2022-11-01 22:22:14 -04:00
  • 91d5c0fa85
         detail in sidekick_base Simon Cruanes 2022-11-01 22:22:06 -04:00
  • 5a7ca4ca2e
         feat(util): improve debug printer wrt newlines Simon Cruanes 2022-11-01 22:20:56 -04:00
  • b68ce33b86
         feat(cdsat): term_to_var conversion, with hooks; solver wrapper Simon Cruanes 2022-11-01 20:59:03 -04:00
  • 2b4cbd9c05
         wip: feat(cdsat): core solver Simon Cruanes 2022-10-29 22:49:04 -04:00
  • 903d12c39b
         feat(main): with --cdsat, use cdsat solver Simon Cruanes 2022-10-29 22:48:49 -04:00
  • 8f2e2ac6de
         feat(asolver): add pp_stats Simon Cruanes 2022-10-29 22:48:41 -04:00
  • 811c06b566
         wip: feat(cdsat): plugins, main solver->Asolver.t Simon Cruanes 2022-10-28 23:33:52 -04:00
  • b6a6e96f51
         feat(cdsat): basic watch system Simon Cruanes 2022-10-26 23:03:16 -04:00
  • adfe52bf1f
         utils Simon Cruanes 2022-10-26 23:03:36 -04:00
  • 01a15ef0ed
         fix(CC): give proper explanations to on-merge hook conflicts Simon Cruanes 2022-10-24 23:00:06 -04:00
  • cd9aa883b2
         wip: feat: start cdsat solver Simon Cruanes 2022-10-23 23:51:16 -04:00
  • 4a5ccffc7a
         small change in sigs Simon Cruanes 2022-10-23 23:51:42 -04:00
  • 7fbfb8439b
         Merge branch 'master' into wip-produce-smtlib-models wip-produce-smtlib-models Simon Cruanes 2023-04-20 22:10:03 -04:00
  • 659f69f989
         opam Simon Cruanes 2023-04-20 10:39:45 -04:00
  • 97dab9ef8c deploy: 40a743badb c-cube 2023-02-24 02:08:35 +00:00
  • 40a743badb
         update to handle mtime 2.0 Simon Cruanes 2023-02-23 21:01:38 -05:00
  • 4c330e4ed6
         ocamlformat Simon Cruanes 2023-02-23 21:01:34 -05:00
  • 37e82adeeb deploy: 651f2c1150 c-cube 2022-10-24 01:03:48 +00:00
  • c498c6dc32 deploy: f905b754aa c-cube 2022-10-24 01:01:34 +00:00
  • f5ccbb476b
         add todo Simon Cruanes 2022-10-23 20:58:25 -04:00
  • 651f2c1150
         warnings Simon Cruanes 2022-10-20 16:12:52 -04:00
  • 7f5c6d4131
         wip: check models Simon Cruanes 2022-10-23 20:55:25 -04:00
  • f905b754aa
         wip: check models Simon Cruanes 2022-10-23 20:55:25 -04:00
  • 173908cadc
         warnings Simon Cruanes 2022-10-20 16:12:52 -04:00
  • 61f1854b80
         feat(smtlib.model): improve printing of deeply nested ite Simon Cruanes 2022-10-19 22:29:19 -04:00
  • 082bfdd43a
         better error Simon Cruanes 2022-10-19 22:29:13 -04:00
  • cc090a4574
         fix(main): consistent printing of models Simon Cruanes 2022-10-19 22:28:52 -04:00
  • 9c9a6e0da5
         refactor(model build): remove redundant class stuff Simon Cruanes 2022-10-19 22:28:38 -04:00