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