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

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