Commit graph

  • 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
  • 7dac9781bf
    feat(sat): phase saving. remember polarity of decisions Simon Cruanes 2022-08-21 13:52:52 -04:00
  • 65f8a61913
    feat(pure-sat): correct timing printing Simon Cruanes 2022-08-21 13:52:33 -04:00
  • 08606f4be0
    refactor: use proper type in sat.store Simon Cruanes 2022-08-21 13:40:53 -04:00
  • ca1abd8134
    fix(smt): perform CC check after theory actions Simon Cruanes 2022-08-20 22:07:21 -04:00
  • e0faf6ba72
    feat: some spans in main/process Simon Cruanes 2022-08-20 00:21:45 -04:00
  • 28ce38002f
    feat(profile): add ?args to spans Simon Cruanes 2022-08-20 00:21:28 -04:00
  • 3e39232696
    fix build temporarily Simon Cruanes 2022-08-19 21:33:49 -04:00
  • 4d97f1a525
    fix build Simon Cruanes 2022-08-19 21:32:55 -04:00
  • 5fa5fb5bd7
    fix(th-data): need to propagate from is-a eagerly Simon Cruanes 2022-08-19 21:31:27 -04:00
  • 177cd70fac
    feat(e_node): remove useless assertion Simon Cruanes 2022-08-19 21:31:04 -04:00
  • c643e547f6
    wip: refactor(th-data): remove some model building, cleanup code Simon Cruanes 2022-08-19 00:08:57 -04:00
  • 1c30fb1f95
    feat(sat): add counters for decision level/trail depth Simon Cruanes 2022-08-18 22:03:15 -04:00
  • a21389063a
    feat(log): if Profile is enabled, forward messages to it Simon Cruanes 2022-08-18 22:02:52 -04:00
  • 2bd555d11b
    feat(profile): proper string handling Simon Cruanes 2022-08-18 22:02:36 -04:00
  • 0c658e3ee4
    feat(term): add replace Simon Cruanes 2022-08-18 22:01:41 -04:00
  • 1b0d47a01d
    feat(profile): add basic counters Simon Cruanes 2022-08-18 20:56:17 -04:00
  • 27ccd367b2
    fix output so benchpress can parse it Simon Cruanes 2022-08-16 23:34:08 -04:00
  • 663f291bd5
    port fix for bug introduced in 1946a5e7 Simon Cruanes 2022-08-16 23:25:44 -04:00
  • 7fb557ae8b
    fix bug introduced in 1946a5e7 Simon Cruanes 2022-08-16 23:23:21 -04:00
  • 6a4947a25c
    feat(term): printer Simon Cruanes 2022-08-16 23:21:07 -04:00
  • b7eb6749a1
    add missing files from th-bool-dyn Simon Cruanes 2022-08-16 21:58:38 -04:00
  • a446af49be
    doc Simon Cruanes 2022-08-16 21:58:00 -04:00
  • b23a031519
    fix: time measurements were wrong Simon Cruanes 2022-08-16 21:45:16 -04:00
  • b61ec35451
    fix(th-bool-dyn): do not propagate, just add clauses depending on polarity Simon Cruanes 2022-08-16 21:37:56 -04:00
  • e4acb2cfca
    fix(th-bool-dyn): add clauses in partial check; register simplifier Simon Cruanes 2022-08-16 21:35:13 -04:00
  • 57941a952a
    add th-bool-dyn for dynamic boolean clausification Simon Cruanes 2022-08-16 21:30:17 -04:00
  • 5b87ff3e46
    feat(theory): add name accessor Simon Cruanes 2022-08-16 21:29:58 -04:00
  • 310d2183c4
    add Lit.Tbl,Lit.Set,Lit.Map Simon Cruanes 2022-08-16 21:29:45 -04:00
  • 947f790f9f
    debug in sat Simon Cruanes 2022-08-16 21:29:29 -04:00
  • 99dc9743a3
    doc Simon Cruanes 2022-08-16 21:29:12 -04:00
  • 6c14690fba
    cleanup code Simon Cruanes 2022-08-16 21:27:46 -04:00
  • e233c846ec
    refactor: cleanup config a bit Simon Cruanes 2022-08-16 21:27:32 -04:00
  • d5b7c2b0ee
    feat(printer): always put (), do not box applications Simon Cruanes 2022-08-16 21:27:09 -04:00