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

Commit graph

  • bfab613d58
         refactor(th-bool): no need for gensym Simon Cruanes 2022-10-19 22:26:37 -04:00
  • 5eab4bbb0d
         feat(gensym): nicer names for gensym symbols Simon Cruanes 2022-10-19 22:25:29 -04:00
  • f591b6e28a
         fix(main): do not produce traces if it's not asked Simon Cruanes 2022-10-19 22:25:07 -04:00
  • d9b9f79b75
         fix(smtlib/model): fix construction of models Simon Cruanes 2022-10-18 22:47:50 -04:00
  • 297615b61b
         feat(model): improve printing of smtlib models Simon Cruanes 2022-10-18 22:47:33 -04:00
  • 09d569ee68
         fix test: restore printing for basic smt solver model Simon Cruanes 2022-10-15 23:17:49 -04:00
  • 24bbcb3fbb
         improve model printing so it's more smtlib2.6 compatible Simon Cruanes 2022-10-15 23:15:42 -04:00
  • 4546b7cff2
         feat(smt): produce better model, with eval function Simon Cruanes 2022-10-15 23:11:27 -04:00
  • 08541613af
         refactor: model building in smtlib, for smtlib Simon Cruanes 2022-10-15 22:42:10 -04:00
  • 55042ab1cb deploy: 5ca966a827 c-cube 2022-10-15 00:44:25 +00:00
  • 5ca966a827
         depth-restricted printing for terms and pterms wip-use-trace-for-proofs Simon Cruanes 2022-10-13 21:43:16 -04:00
  • fb8614f304
         feat: decode proofs from traces; print them in show_trace Simon Cruanes 2022-10-13 00:03:08 -04:00
  • 4e1272d64a
         test: update doc guide Simon Cruanes 2022-10-12 22:45:47 -04:00
  • 032be221a3
         refactor: fix sudoku example Simon Cruanes 2022-10-12 22:20:43 -04:00
  • a6d3ed259f
         refactor: make it compile again (driver, main) Simon Cruanes 2022-10-12 22:19:41 -04:00
  • 48ebeb37fb
         refactor(proof): serialize pterms; tracer inherits term tracer Simon Cruanes 2022-10-12 22:19:13 -04:00
  • ad0165242f
         refactor: update remaining theories for new proof style Simon Cruanes 2022-10-12 22:19:00 -04:00
  • f275129967
         refactor(smt): use sidekick.proof for proof tracing Simon Cruanes 2022-10-12 16:30:39 -04:00
  • 6f576e7d8b
         adapt bin Simon Cruanes 2022-10-12 15:51:37 -04:00
  • 85ba423e8c
         wip: refactor(smt): use sidekick.proof for proof tracing Simon Cruanes 2022-10-12 12:22:19 -04:00
  • 46c44648e1
         feat(core-logic): add builtin Proof type Simon Cruanes 2022-10-12 12:22:04 -04:00
  • 7db5e1a902
         refactor(sat): use new proof tracer from sidekick,proof Simon Cruanes 2022-10-12 12:21:45 -04:00
  • 5135d9920a
         refactor(asolver): use new proof tracer from sidekick.proof Simon Cruanes 2022-10-12 12:21:20 -04:00
  • ef3f2713dc
         refactor(cc): use new proof trace from sidekick.proof Simon Cruanes 2022-10-12 12:21:06 -04:00
  • 8a3e7528c3
         refactor(simplify): use new proof trace from sidekick.proof Simon Cruanes 2022-10-12 12:20:50 -04:00
  • 4b359a40f2
         improve Int_id for tracing Simon Cruanes 2022-10-12 12:20:20 -04:00
  • 2726a3afe2
         refactor: remove proof-trace infra from base to use sidekick.trace instead Simon Cruanes 2022-10-12 12:19:20 -04:00
  • 842a7de435
         wip: refactor(core): remove proof representation from core Simon Cruanes 2022-10-12 12:18:52 -04:00
  • 82727cd7ad
         wip: feat(core): term references Simon Cruanes 2022-10-12 12:18:40 -04:00
  • 51c48453ab
         wip: feat(proof): lib sidekick.proof with tracing Simon Cruanes 2022-10-12 12:17:35 -04:00
  • ccd506e387
         test Simon Cruanes 2022-10-10 20:15:18 -04:00
  • e9a698b686 deploy: 89c9e00500 c-cube 2022-10-10 20:07:35 +00:00
  • 89c9e00500
         chore: fix opam file Simon Cruanes 2022-10-10 16:06:02 -04:00
  • b577389acf
         test Simon Cruanes 2022-10-10 15:45:53 -04:00
  • a47bbf45e8
         refactor: use abstract-solver in smtlib driver; CDCL(T) implements asolver Simon Cruanes 2022-10-10 15:44:13 -04:00
  • d08c8fe165
         feat: add sidekick.abstract solver Simon Cruanes 2022-10-10 15:43:37 -04:00
  • e3e71f3d76
         refactor: smtlib driver now part of base; make it stateful Simon Cruanes 2022-10-10 14:21:10 -04:00
  • ff2600a4e9
         test: add test for proof syntax wip-parser Simon Cruanes 2022-10-07 21:41:18 -04:00
  • 1bc6f0ef5c
         fix(parser): handle {} properly Simon Cruanes 2022-10-07 21:40:50 -04:00
  • 32d268822d
         feat(parser): use pp_loc to print locations, if asked Simon Cruanes 2022-10-06 23:08:17 -04:00
  • 057854e734
         feat(parser): improve rendering of groups of typed variables Simon Cruanes 2022-10-06 22:42:20 -04:00
  • edc96cc9c1
         chore: add sidekick-parser opam package Simon Cruanes 2022-10-06 22:04:43 -04:00
  • 6e423e3f75
         test: update parser test Simon Cruanes 2022-10-06 22:04:32 -04:00
  • 8866f032fe
         feat(parser): move to menhir Simon Cruanes 2022-10-06 22:03:26 -04:00
  • 3317171971
         add another test, improve parser AST Simon Cruanes 2022-10-05 23:19:05 -04:00
  • 4140739b93
         fix test Simon Cruanes 2022-10-05 23:05:25 -04:00
  • ea755e5bc6
         test: basic test for parser Simon Cruanes 2022-10-05 23:02:42 -04:00
  • 1c2c9deefd
         wip: feat: basic term parser Simon Cruanes 2022-10-05 23:02:32 -04:00
  • f88ab01982
         fix warnings Simon Cruanes 2022-10-05 23:02:17 -04:00
  • 2f96f36e75
         chore: generate opam files from dune-package Simon Cruanes 2022-10-06 19:51:43 -04:00
  • 4cb3299804
         chore: ocamlformat Simon Cruanes 2022-10-05 09:16:32 -04:00
  • 2381aa24a3 deploy: 656d93d5fb c-cube 2022-10-05 02:44:18 +00:00
  • 656d93d5fb
         smt tracer is now a clause tracer Simon Cruanes 2022-10-02 23:23:34 -04:00
  • 06a0089a8c
         feat: add Clause_tracer, works both for SMT and SAT Simon Cruanes 2022-10-02 23:07:53 -04:00
  • d9b76814dd
         ignore Simon Cruanes 2022-10-02 23:07:45 -04:00
  • 96dddb5383
         feat: show_trace, and trace_reader, can now display a QF_UF trace Simon Cruanes 2022-09-30 23:05:00 -04:00
  • 3aadc640c4
         improve tracing, add show_trace Simon Cruanes 2022-09-30 22:11:41 -04:00
  • 8f563c838f
         wip: Tracer for SMT Simon Cruanes 2022-09-26 22:44:28 -04:00
  • 342bf87759
         refactor(core/term): tracer is now a class Simon Cruanes 2022-09-26 22:43:49 -04:00
  • 40e124931c
         doc: update readme Simon Cruanes 2022-09-26 21:00:09 -04:00
  • 1c11a82a7d
         test: update doc guide Simon Cruanes 2022-09-26 20:57:55 -04:00
  • dbe64f5975
         feat: decoders for LRA terms Simon Cruanes 2022-09-26 20:55:29 -04:00
  • 17ac25d314
         update tracing test Simon Cruanes 2022-09-26 20:47:48 -04:00
  • 45eebaae0f
         some todos Simon Cruanes 2022-09-26 20:31:57 -04:00
  • 59306d2e01
         fix sudoku solve Simon Cruanes 2022-09-26 20:14:26 -04:00
  • a99fbed159
         test: repair test Simon Cruanes 2022-09-25 23:13:45 -04:00
  • 8cbb200f18
         basic test for tracer/trace reader using bencode Simon Cruanes 2022-09-25 23:04:51 -04:00
  • c2e5f31645
         change signature of Const.decoders; add bencode decoder Simon Cruanes 2022-09-25 23:04:23 -04:00
  • 9ea8ba9bd1
         feat: implement some const decoders Simon Cruanes 2022-09-25 22:25:40 -04:00
  • 798993fee2
         feat(trace): start basic trace reader for terms, using Source Simon Cruanes 2022-09-25 21:29:53 -04:00
  • f2471fd78c
         feat(trace): add Source, to read traces Simon Cruanes 2022-09-25 21:28:10 -04:00
  • ca3262eac3
         minor change in term tracer Simon Cruanes 2022-09-25 21:27:42 -04:00
  • 27b0374c62
         feat(util): more functions in Ser_decode Simon Cruanes 2022-09-25 21:26:35 -04:00
  • 15bc5c4b60
         feat(core): add LRU to support entry decoding in term reader Simon Cruanes 2022-09-25 23:04:07 -04:00
  • 7b4404fb78
         feat(tracing): introduce term/const serialization Simon Cruanes 2022-09-23 22:13:21 -04:00
  • dcad86963d
         wip: sidekick_trace Simon Cruanes 2022-09-19 22:27:03 -04:00
  • 72990de373
         wip: feat(core): tracing terms, make constants (de)serializable Simon Cruanes 2022-09-19 22:26:31 -04:00
  • 7232d43d99
         feat(util): basic Ser_decode for deserialization Simon Cruanes 2022-09-19 22:24:04 -04:00
  • adcb6233a3
         feat(ser_value): print Simon Cruanes 2022-09-19 22:23:45 -04:00
  • 9a2249292f
         feat: add sidekick.bencode for serialization Simon Cruanes 2022-09-19 21:50:13 -04:00
  • d518511c64
         feat(util): add Ser_value Simon Cruanes 2022-09-19 21:50:01 -04:00
  • a313918e74
         doc Simon Cruanes 2022-09-19 21:49:47 -04:00
  • 88a10dcf3a
         feat(Error): add Error.result/try_ Simon Cruanes 2022-09-19 21:49:05 -04:00
  • e73bf4d3e5
         util: add Str_map Simon Cruanes 2022-09-19 21:48:45 -04:00
  • 1c07b027ef
         refactor(const): remove opaque_to_cc Simon Cruanes 2022-09-19 21:33:25 -04:00
  • d58c81e83f
         wip: tracing system Simon Cruanes 2022-09-18 15:54:22 -04:00
  • 86106f182b
         chore: makefile targets for some incremental benchs wip-preprocess-2022-08-31 Simon Cruanes 2022-09-16 21:08:58 -04:00
  • c50a373d2e
         refactor: extract Model into its own library Simon Cruanes 2022-09-16 20:27:01 -04:00
  • 24251399bf
         comments Simon Cruanes 2022-09-16 19:51:10 -04:00
  • c49edd8d70
         fix debug msg Simon Cruanes 2022-09-16 19:49:58 -04:00
  • 0b951b92d3
         fix some warnings Simon Cruanes 2022-09-14 18:20:10 -04:00
  • e9eab74b1e
         fix(lra): preprocess in the right order Simon Cruanes 2022-09-12 22:45:07 -04:00
  • 2764882f50
         fix(preprocess): type check was invalid Simon Cruanes 2022-09-11 14:50:18 -04:00
  • c18b824037
         fix(lra): preprocess was returning wrong term Simon Cruanes 2022-09-11 14:36:38 -04:00
  • 469b97934a
         fix: more type checks in preprocess Simon Cruanes 2022-09-11 14:26:34 -04:00
  • 3d0461936f
         fix: remove spurious check? Simon Cruanes 2022-09-11 14:10:01 -04:00
  • abff92d972
         fix warning Simon Cruanes 2022-09-11 14:09:56 -04:00
  • 67c9ffa2ac
         fix(lit): add type checking assertion Simon Cruanes 2022-09-11 14:09:03 -04:00
  • fad651a4cb
         fix(find_foreign): memoization needs to account for is_sub Simon Cruanes 2022-09-11 13:55:25 -04:00
  • 337a0696f1
         update guide Simon Cruanes 2022-09-10 22:22:30 -04:00