simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-05-05 08:54:24 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • 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
  • 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