Commit graph

  • 94ba945bf3
    feat(cc.plugin): plugins have state, passed at init Simon Cruanes 2022-08-14 23:21:49 -04:00
  • e9dae47d0b
    fixup: modify benchpress for new output Simon Cruanes 2022-08-14 23:21:40 -04:00
  • 08a4ed892d
    feat(stat): improve printing Simon Cruanes 2022-08-14 23:21:22 -04:00
  • 2ab93aee04
    feat(main): fix initial time; better display (smtlib-friendly) Simon Cruanes 2022-08-14 23:21:02 -04:00
  • 6fca21bd33
    symlink in makefile Simon Cruanes 2022-08-14 22:35:34 -04:00
  • 541d0c2545
    cleanup Simon Cruanes 2022-08-14 22:33:21 -04:00
  • 6f42c060f4
    perf(util): more inlining Simon Cruanes 2022-08-14 22:32:51 -04:00
  • 23e70a192a
    perf(cc): more inlining; remove dead code Simon Cruanes 2022-08-14 22:32:28 -04:00
  • 82691069f1
    perf: dune flags Simon Cruanes 2022-08-14 22:32:21 -04:00
  • 6b09a562c5
    comment out tests for now Simon Cruanes 2022-08-14 14:17:18 -04:00
  • ba2e191882
    detail Simon Cruanes 2022-08-14 14:15:45 -04:00
  • ff6dc527bd
    comment out some profiling Simon Cruanes 2022-08-14 14:14:50 -04:00
  • 517a5d2e5f
    better tracing Simon Cruanes 2022-08-13 13:55:01 -04:00
  • 6ccabc70aa
    feat(sudoku): add stats Simon Cruanes 2022-08-13 13:45:38 -04:00
  • 63802fe3d6
    feat(stat): improve printing api Simon Cruanes 2022-08-13 13:45:21 -04:00
  • eddbf139fc
    refactor sudoku solver; make it compile; use new term repr Simon Cruanes 2022-08-13 13:30:21 -04:00
  • 92edae353d
    feat(sat): add mk_plugin_cdcl_t Simon Cruanes 2022-08-13 13:30:08 -04:00
  • c2eac5e2c3
    update doc Simon Cruanes 2022-08-13 13:30:03 -04:00
  • 632d5e3f40
    fix(core-logic): ensure store IDs fit in 5 bits Simon Cruanes 2022-08-13 13:29:49 -04:00
  • 7d46a38e2c
    fix compilation in unittest Simon Cruanes 2022-08-13 13:29:35 -04:00
  • 85314379a5
    fix type of is_a Simon Cruanes 2022-08-12 23:21:56 -04:00
  • 85eef2d117
    feat(base/data): fix types for cstor/select term builders Simon Cruanes 2022-08-12 23:17:20 -04:00
  • e99192869d
    remove debug Simon Cruanes 2022-08-12 23:17:15 -04:00
  • 593b693caf
    refactor lit a bit Simon Cruanes 2022-08-12 23:09:56 -04:00
  • 4d02e2a1c7
    fix(cc): bug in backtracking Simon Cruanes 2022-08-12 23:09:48 -04:00
  • 7bbe70b060
    bugfix in CC wip-better-cc-2022-07-21 Simon Cruanes 2022-08-12 23:07:32 -04:00
  • b73c1bf464
    feat(bool): use binary symbols for boolean operators Simon Cruanes 2022-08-10 22:41:53 -04:00
  • 67d5f244c1
    feat(Term): offer is_type and is_a_type Simon Cruanes 2022-08-10 22:41:26 -04:00
  • d14617ca77
    refactor: rush to have sidekick compile again. th-lra is commented out Simon Cruanes 2022-08-10 22:08:57 -04:00
  • 1f79ee05f2
    wip: make Base really usable, add th-data/th-bool Simon Cruanes 2022-08-10 22:08:43 -04:00
  • 8777682e07
    detail in core_logic Simon Cruanes 2022-08-10 22:08:33 -04:00
  • 81f159d25d
    feat(th-bool): add proof_rules, use std gensym Simon Cruanes 2022-08-10 22:08:09 -04:00
  • 647d66a196
    feat(th-data): use lists, not iter/array; add Proof_rules Simon Cruanes 2022-08-10 22:07:54 -04:00
  • b9c0265cb9
    feat(core): add Gensym module, add Proof_trace.close Simon Cruanes 2022-08-10 22:07:30 -04:00
  • 95dcb0ae74
    wip: refactor further Simon Cruanes 2022-08-09 22:41:13 -04:00
  • fc5ce9bf87
    wip: make it compile Simon Cruanes 2022-08-08 21:52:47 -04:00
  • 7d59846d72
    wip: refactor base Simon Cruanes 2022-08-08 21:52:39 -04:00
  • 8003cdcebb
    sidekick-mini-cc: remove functor Simon Cruanes 2022-08-08 21:52:20 -04:00
  • 95beb2bf27
    core: add better printer Simon Cruanes 2022-08-08 21:49:47 -04:00
  • f17e689a3c
    feat(cc): adapt to the new CC_view Simon Cruanes 2022-08-08 21:22:48 -04:00
  • 2a8eb0c166
    refactor tests for mini-cc Simon Cruanes 2022-08-08 21:22:33 -04:00
  • 7aa113f379
    feat(core): make CC_view part of the core library; with default CC view Simon Cruanes 2022-08-08 21:17:37 -04:00
  • 010451145c
    fix(core-logic): bad constant for ite Simon Cruanes 2022-08-08 21:16:54 -04:00
  • 97a5c8efa3
    detail Simon Cruanes 2022-08-07 22:42:35 -04:00
  • 5b6fd14dcf
    wip: refactor(base): split into several views, all based on Const Simon Cruanes 2022-08-07 22:41:26 -04:00
  • 4dcc3ea4ad
    small changes in smt Simon Cruanes 2022-08-07 22:41:13 -04:00
  • 86bc9453d5
    rename dir Simon Cruanes 2022-08-07 22:41:05 -04:00
  • c2af589282
    add core.bool_view Simon Cruanes 2022-08-07 22:40:39 -04:00
  • c873346047
    detail in th-lra Simon Cruanes 2022-08-05 21:56:45 -04:00
  • a7e7b38d1b
    core: re-export Const.t properly Simon Cruanes 2022-08-05 21:56:23 -04:00
  • 24e79df776
    wip: refactor base Simon Cruanes 2022-08-05 21:55:53 -04:00
  • 4aec4fe491
    refactor(proofs): make proof terms a recursive term Simon Cruanes 2022-08-01 20:42:45 -04:00
  • 1edf054104
    refactor(proof): use a suspension but keep uniform Proof_term.data type Simon Cruanes 2022-07-31 15:00:27 -04:00
  • dd50ab079e
    remove most proof-trace code Simon Cruanes 2022-07-30 23:59:15 -04:00
  • 06107c212f
    remove most sigs Simon Cruanes 2022-07-30 23:58:34 -04:00
  • 65e876bebc
    chore: makefile Simon Cruanes 2022-07-30 23:58:18 -04:00
  • ee2ea784ad
    remove Vec_unit Simon Cruanes 2022-07-30 23:22:25 -04:00
  • 36204c5e5e
    refactor some more Simon Cruanes 2022-07-30 23:04:49 -04:00
  • 0ff5ac9a3f
    refactor(th-lra): rename to th-lra Simon Cruanes 2022-07-30 23:03:57 -04:00
  • 0d0751b7d2
    refactor(theories): remove functors Simon Cruanes 2022-07-30 23:01:29 -04:00
  • df9fa11507
    refactor(th-lra): adapt to new code Simon Cruanes 2022-07-30 21:51:46 -04:00
  • 05faac97e7
    refactor(smt): remove functor, split into modules Simon Cruanes 2022-07-30 21:18:30 -04:00
  • 6e1da96e7e
    include solver directly in Sidekick_sat Simon Cruanes 2022-07-30 21:18:18 -04:00
  • 1e1b0f352d
    feat(simplify): add sidekick_simplify library Simon Cruanes 2022-07-30 21:17:55 -04:00
  • 83e456ef8a
    remove sidekick_lit functor Simon Cruanes 2022-07-30 21:17:37 -04:00
  • 1ecb189fd5
    refactor: core and CC Simon Cruanes 2022-07-30 21:17:20 -04:00
  • 085e37e063
    refactor(sat): remove functor, split into modules Simon Cruanes 2022-07-30 20:27:47 -04:00
  • b97582daa2
    wip: refactor(smt): remove layers of functors, split into modules Simon Cruanes 2022-07-30 00:19:29 -04:00
  • 7595f66e59
    refactor(core): add Proof_step Simon Cruanes 2022-07-29 23:27:04 -04:00
  • a9ae790d7f
    refactor(cc): split into modules, fully defunctorize Simon Cruanes 2022-07-29 23:25:48 -04:00
  • e30590955e
    refactor(sat): remove unused values, split code off main functor Simon Cruanes 2022-07-29 22:37:31 -04:00
  • d4ba4602a4
    refactor(sat): simplify interface a lot Simon Cruanes 2022-07-29 22:28:21 -04:00
  • c09650db51
    refactor(cc): continue de-functorizing Simon Cruanes 2022-07-29 00:15:05 -04:00
  • 464bc66474
    wip: refactor(cc): remove layers of functorization Simon Cruanes 2022-07-29 00:02:27 -04:00
  • 1905d2d628
    feat(core): improve Lit Simon Cruanes 2022-07-29 00:02:06 -04:00
  • 9df981d650
    feat(core): concrete lit, proof traces, proof terms Simon Cruanes 2022-07-28 23:30:56 -04:00
  • 65c6872853
    details: synopsis in dune files Simon Cruanes 2022-07-28 23:30:42 -04:00
  • c1af4374bd
    core-logic: make Types_ private Simon Cruanes 2022-07-28 23:12:18 -04:00
  • 68c03a39b3
    feat(core-logic): add a few builtins (=, bool, ite, not, true, false) Simon Cruanes 2022-07-28 20:25:17 -04:00
  • a4db8b6e94
    small improvement Simon Cruanes 2022-07-28 15:27:14 -04:00
  • c6407bfec1
    refactor a bit Simon Cruanes 2022-07-28 14:54:23 -04:00
  • e70daf4531
    remove dead code Simon Cruanes 2022-07-28 14:52:11 -04:00
  • e235a65567
    test: add more to unittest/core-logic Simon Cruanes 2022-07-28 14:51:43 -04:00
  • bfa434562e
    fix(core-logic/term): make ty unfailing; fix DB bugs Simon Cruanes 2022-07-28 14:51:24 -04:00
  • dbd20c999b
    refactor test Simon Cruanes 2022-07-28 13:55:09 -04:00
  • 6f376cfaf2
    refactor: rename core-ast to core-logic; split into modules Simon Cruanes 2022-07-28 13:54:38 -04:00
  • 435845d1d4
    update tests Simon Cruanes 2022-07-27 22:45:10 -04:00
  • 88eb2575c3
    feat(sigs): add some basic sigs Simon Cruanes 2022-07-27 22:40:46 -04:00
  • 2db3343bcd
    improve unittest for core-ast Simon Cruanes 2022-07-27 22:40:36 -04:00
  • 8950601fb2
    fix(core-ast): fix some issues in type computations; print arrows Simon Cruanes 2022-07-27 22:40:16 -04:00
  • e52a7ac0ea
    test: add basic unit-test for core-ast Simon Cruanes 2022-07-27 21:41:59 -04:00
  • 410c5b1ee2
    feat: start core-ast library Simon Cruanes 2022-07-27 21:41:00 -04:00
  • 0e5bde0f40
    detail Simon Cruanes 2022-07-23 00:24:56 -04:00
  • 4a6237191e
    wip: try to restore old model construction Simon Cruanes 2022-07-22 22:16:04 -04:00
  • 2922cca78f
    fix: proper negation when raising an acyclicity conflict Simon Cruanes 2022-07-22 21:54:22 -04:00
  • c8800fe3e2
    promote test results Simon Cruanes 2022-07-22 21:45:56 -04:00
  • 851dda696a
    feat(cc): have 2 phases of pre-merge events Simon Cruanes 2022-07-22 21:31:42 -04:00
  • 6da6284711
    refactor(cc): use explicit actions in CC, not effectful functions Simon Cruanes 2022-07-22 21:26:21 -04:00
  • e37f66c394
    feat(cc): remove same-val explanations and model mode Simon Cruanes 2022-07-21 23:29:07 -04:00
  • dc68a60151
    feat(cc): remove callbacks, return list of actions Simon Cruanes 2022-07-21 23:21:07 -04:00