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

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