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

  • 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
  • f024fe821e
         add regression test Simon Cruanes 2022-09-10 21:55:49 -04:00
  • c9127c6cd7
         fix(base/form): fix CNF for equiv Simon Cruanes 2022-09-10 21:48:51 -04:00
  • fd39a414c3
         fix(smt): sign error in literal Simon Cruanes 2022-09-10 21:45:43 -04:00
  • 7876820d4d
         remove dead code Simon Cruanes 2022-09-10 15:02:44 -04:00
  • 87e91660ad
         doc: update guide for now Simon Cruanes 2022-09-10 15:02:17 -04:00
  • b8ee815d9d
         update tools Simon Cruanes 2022-09-10 14:59:52 -04:00
  • 721ed2eac0
         refactor(preprocess): introduce Find_foreign, runs after preprocess Simon Cruanes 2022-09-10 14:10:36 -04:00
  • 3d95fc16c4
         feat(cc): use Term.pp. not Term.pp_debug Simon Cruanes 2022-09-10 14:10:13 -04:00
  • 8811699410
         feat(term): add open_eq Simon Cruanes 2022-09-10 14:09:55 -04:00
  • 659fa7ba5b
         wip: feat(lra): update to newer preprocessing Simon Cruanes 2022-09-09 22:16:59 -04:00
  • e9c2491380
         feat(th-bool): properly preprocess in equiv Simon Cruanes 2022-09-09 22:16:48 -04:00
  • e94a7bd31c
         refactor(preprocess): directly forward preprocess actions to solver Simon Cruanes 2022-09-08 22:05:40 -04:00
  • c9138144f3
         refactor(preprocess): break infinite recursion Simon Cruanes 2022-09-08 21:55:09 -04:00
  • 317f406620
         wip: refactor(preprocess): recursive preprocess guided by theories Simon Cruanes 2022-09-07 19:35:09 -04:00
  • 6101e029b3
         feat(core): add box, with a box constant Simon Cruanes 2022-09-07 19:34:31 -04:00
  • f7daf7e45e
         wip: add theory combination to Preprocess, based on claim hooks Simon Cruanes 2022-09-03 14:45:09 -04:00
  • 16eb12fac2
         wip: preprocess in its own file Simon Cruanes 2022-08-31 00:12:44 -04:00
  • e74439cf2a
         wip: new attempt at theory combination wip-optim-lra-2022-08-31 Simon Cruanes 2022-09-01 22:34:27 -04:00
  • 47a0b075f0
         fix(model builder): allow multiple add Simon Cruanes 2022-09-01 22:33:59 -04:00
  • d741b4160d
         remove is_valid_literal concept Simon Cruanes 2022-09-01 22:33:40 -04:00
  • efc01f507b
         feat(term): add is_pi and weak containers Simon Cruanes 2022-09-01 22:33:00 -04:00
  • 2092bbef3f
         feat(gensym): add reset Simon Cruanes 2022-09-01 22:32:52 -04:00
  • 0797ff0409
         tiny helper Simon Cruanes 2022-09-01 22:32:24 -04:00
  • 8db63dbdc4
         th-comb: remove claim-term, add claim-type Simon Cruanes 2022-09-01 22:31:50 -04:00
  • 1ce1bd31b9
         theory for uninterpreted types Simon Cruanes 2022-09-01 22:27:10 -04:00
  • 985a004dcf deploy: 80b08e03cb c-cube 2022-08-31 04:51:18 +00:00
  • 52b60c4114
         fix(main): method for measuring memory overhead was wrong Simon Cruanes 2022-08-31 00:47:11 -04:00
  • 34ad038d9a
         temp: disable partial checks in LRA Simon Cruanes 2022-08-31 00:42:17 -04:00
  • 80b08e03cb
         feat(const): add opaque_to_cc property, to control CC Simon Cruanes 2022-08-31 00:41:42 -04:00
  • 4dca7df629
         actions: run tests on 4.14 only Simon Cruanes 2022-08-29 20:48:57 -04:00
  • 1ce76c76ef deploy: 737a11504d c-cube 2022-08-30 00:33:56 +00:00
  • 0f21cf069e
         test: update expected results Simon Cruanes 2022-08-29 20:28:42 -04:00
  • 737a11504d
         Merge branch 'wip-defunctorize-terms' Simon Cruanes 2022-08-29 20:27:27 -04:00
  • 83a4ae46c1
         fix: use standard = even for LRA terms wip-th-comb wip-defunctorize-terms Simon Cruanes 2022-08-28 00:20:06 -04:00
  • 28ad97d2b7
         fix: typecheck issue Simon Cruanes 2022-08-27 23:42:19 -04:00
  • 4c90405391
         refactor a bit Simon Cruanes 2022-08-27 23:09:29 -04:00
  • 01d0668fc6
         fix(sat): check for new atoms in termination check in final_check Simon Cruanes 2022-08-27 23:08:58 -04:00
  • 5feb5d8e73
         refactor: new API for combination, with theories claiming terms Simon Cruanes 2022-08-27 22:51:16 -04:00
  • ccb3753668
         wip(smt): theory combination Simon Cruanes 2022-08-27 21:38:20 -04:00
  • 2a0feed32c
         format Simon Cruanes 2022-08-27 20:48:32 -04:00
  • df287e4ef7
         update doc/guide Simon Cruanes 2022-08-27 20:44:30 -04:00
  • 137183f2fe
         small fixes, warnings Simon Cruanes 2022-08-27 20:44:13 -04:00
  • e3aa43f817
         cleanup Simon Cruanes 2022-08-27 20:39:06 -04:00
  • 40734d5074
         doc: update guide (temporarily) Simon Cruanes 2022-08-27 15:01:33 -04:00
  • 90f100d9b1
         helpers to build terms and solvers Simon Cruanes 2022-08-27 15:01:25 -04:00
  • f96967b0da
         delete todo todo Simon Cruanes 2022-08-27 14:01:41 -04:00
  • ad8c6a9351
         more Simon Cruanes 2022-08-27 14:01:18 -04:00
  • 5f91d0bd76
         fix spurious \r Simon Cruanes 2022-08-27 12:36:45 -04:00
  • f0041f9dae
         feat: reinstate LRA theory and terms Simon Cruanes 2022-08-26 22:17:02 -04:00
  • e66a27229b
         detail in printing Simon Cruanes 2022-08-26 22:16:45 -04:00
  • e03e5e77a9
         add LRA_term to base Simon Cruanes 2022-08-25 23:03:12 -04:00
  • 28173c1852
         feat(term): replace E_app_uncurried with E_app_fold Simon Cruanes 2022-08-25 20:50:56 -04:00
  • f6efc8f575
         more unsat tests Simon Cruanes 2022-08-25 20:50:50 -04:00
  • 4d78be0c52
         wip: model builder Simon Cruanes 2022-08-25 20:13:49 -04:00
  • 6ad07921c4
         details Simon Cruanes 2022-08-22 22:09:58 -04:00
  • dde63a9ef2
         refactor: stats, small changes Simon Cruanes 2022-08-22 22:09:36 -04:00
  • 279ceade78
         feat(base): in Form, use uncurried forms for and/or Simon Cruanes 2022-08-22 22:09:05 -04:00
  • 9762968373
         feat(bool): use lists for B_and/B_or, along with App_uncurried Simon Cruanes 2022-08-22 22:08:19 -04:00
  • dd66efb772
         feat(term): add App_uncurried constructor Simon Cruanes 2022-08-22 22:06:34 -04:00
  • dff65c5d26
         refactor: Term.abs takes store again, so abs false can be false,true Simon Cruanes 2022-08-22 22:04:58 -04:00
  • 0ff197d56c
         perf(core): have eq and not_ be simplying Simon Cruanes 2022-08-22 22:01:02 -04:00
  • cca2c48f07
         feat(cc): add small union-find on the side to make expls smaller wip-defunctorize-terms-UF-in-CC-expl Simon Cruanes 2022-08-21 22:57:10 -04:00
  • 9c57dad3f1
         perf: small changes in Event Simon Cruanes 2022-08-21 22:56:38 -04:00
  • 1eb26e5091
         refactor(cc): cleanup a bit, smaller closures for backtracking Simon Cruanes 2022-08-21 22:34:15 -04:00
  • 30cf71522c
         small refactor of CC Simon Cruanes 2022-08-21 22:01:07 -04:00
  • e34f5a5c3c
         cleanup Simon Cruanes 2022-08-21 13:53:48 -04:00
  • 007fbad243
         fix some stats Simon Cruanes 2022-08-21 13:53:36 -04:00