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