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

Commit graph

  • 407a7e83f7 fix: allow conflicts below decision level in Make_cdcl_t Simon Cruanes 2020-01-14 22:56:01 -06:00
  • a31b2b36ef fixes: add missing expl in monoids; handle is-c t Simon Cruanes 2020-01-14 22:41:33 -06:00
  • ef60d1466f feat: better debug message Simon Cruanes 2020-01-14 21:23:02 -06:00
  • b332e8ceb0 fix: preprocess away "ite" Simon Cruanes 2020-01-14 20:23:23 -06:00
  • 17a09f2cbc test: add some regression tests Simon Cruanes 2020-01-14 20:23:14 -06:00
  • 48d6b57383 test: enable progress by default Simon Cruanes 2020-01-08 19:51:12 -06:00
  • dbf88279a1 test: more reg tests Simon Cruanes 2019-12-28 09:19:17 -06:00
  • 10b9febe9d fix(th-data): avoid redundant explanations Simon Cruanes 2019-12-28 09:00:59 -06:00
  • e58b29da02 fix(term): hashconsing error leading to non termination Simon Cruanes 2019-12-28 08:49:14 -06:00
  • 8749cfff0a test: add reg test Simon Cruanes 2019-12-28 08:49:04 -06:00
  • b250587a5f tst: add some regression tests; remove dead file Simon Cruanes 2019-12-28 08:34:20 -06:00
  • 6f67593be1 feat(data): fixes (decide args of is-a/select; rearrange reduction rules) Simon Cruanes 2019-12-28 08:31:52 -06:00
  • 9ba5f508ce feat(main): simpler computation of version Simon Cruanes 2019-12-28 08:31:41 -06:00
  • 62b1d83cd6 debug: add type checking in CC.merge Simon Cruanes 2019-12-28 08:19:59 -06:00
  • 91e9b6cc2c feat: initial support for is-a/select Simon Cruanes 2019-12-28 07:08:23 -06:00
  • 6aafaad48f feat(data): store is-a/select parents in a monoid Simon Cruanes 2019-12-28 06:15:50 -06:00
  • 858ffb6f25 chore: add --progress in makefile Simon Cruanes 2019-12-09 22:38:26 -06:00
  • 9293553925 feat(th-data): first draft of acyclicity Simon Cruanes 2019-12-09 21:50:22 -06:00
  • 6061b5843e fix(th-data): fix merge explanation in cstor monoid Simon Cruanes 2019-12-09 21:50:09 -06:00
  • d52fb1e5fd core: add iter_all in monoid class Simon Cruanes 2019-12-09 21:49:48 -06:00
  • bf23f7c826 fix(cc): remove too powerful assertion in CC Simon Cruanes 2019-12-09 21:49:29 -06:00
  • c54ee2310e test: better conf for sidekick Simon Cruanes 2019-12-09 19:11:29 -06:00
  • c4d2a800ab test: update test config to use $cur_dir Simon Cruanes 2019-12-07 18:53:46 -06:00
  • 0ec9c1683f test: modify logitest config file Simon Cruanes 2019-12-07 18:03:31 -06:00
  • 787b9404af refactor: change debug levels Simon Cruanes 2019-12-01 19:40:31 -06:00
  • a4e3fd5a69 feat: provide simple repr->monoid mapping in core Simon Cruanes 2019-12-01 19:26:12 -06:00
  • 7c951c08ff wip: use t=c instead of (is _ c) t for nullary constructors Simon Cruanes 2019-12-01 18:14:20 -06:00
  • c55e7a613b test: add some basic datatype tests Simon Cruanes 2019-12-01 17:38:24 -06:00
  • 444a0b9f85 wip: theory of datatypes Simon Cruanes 2019-12-01 17:17:37 -06:00
  • 8c5e28da28 wip: theory of datatypes Simon Cruanes 2019-11-23 16:20:53 -06:00
  • 949e079867 wip: add datatypes Simon Cruanes 2019-11-23 10:51:04 -06:00
  • 88550716d8 prepare for 0.8.1 Simon Cruanes 2019-12-14 19:44:38 -06:00
  • 14f68749a5 add more tests Simon Cruanes 2019-12-13 17:55:10 -06:00
  • d6c003390d rename logitest to benchpress Simon Cruanes 2019-12-13 16:38:01 -06:00
  • 85b0066660 test: update logitest config and makefile Simon Cruanes 2019-12-11 18:35:15 -06:00
  • 682edc4640 test: update logitest config Simon Cruanes 2019-12-09 17:40:57 -06:00
  • ef77e1e729 add promoted sidekick-version Simon Cruanes 2019-12-09 12:11:00 -06:00
  • c63887a1f0 feat: add --version flag Simon Cruanes 2019-12-09 11:55:45 -06:00
  • 079144cc98 update todo Simon Cruanes 2019-12-01 18:26:16 -06:00
  • 99fed971d6 fix heap Simon Cruanes 2019-11-29 14:44:01 -06:00
  • 0266a39b04 fix deprecation warnings related to pervasives Simon Cruanes 2019-11-29 14:03:52 -06:00
  • ca9d5447e0 fix(heap): handle case with one element properly Simon Cruanes 2019-11-29 14:02:36 -06:00
  • 87a2936f75 doc: add an index file Simon Cruanes 2019-11-27 16:56:36 -06:00
  • 10cfa137b6 feat: handle parsing of .cnf files Simon Cruanes 2019-11-23 13:41:03 -06:00
  • 678bf5e03d test: update expect field in toml Simon Cruanes 2019-11-20 17:53:18 -06:00
  • f1fc429b5a add basic test for th-cstor Simon Cruanes 2019-11-19 19:48:09 -06:00
  • e414112010 test: add some basic datatype tests Simon Cruanes 2019-11-19 19:41:45 -06:00
  • c3be2411bf wip: th data Simon Cruanes 2019-11-19 19:41:21 -06:00
  • 9b99560130 feat: handle typechecking and term building for datatypes Simon Cruanes 2019-11-19 19:40:59 -06:00
  • 3327c86841 refactor(smtlib): remove intermediate typed AST, type directly into terms Simon Cruanes 2019-11-19 17:30:30 -06:00
  • a85730b8ee Set theme jekyll-theme-minimal Simon Cruanes 2019-11-21 13:50:10 -06:00
  • 1a71535178
         chore: try github actions (#3) Simon Cruanes 2019-11-21 13:35:52 -06:00
  • 591337855e
         wip wip-github-action Simon Cruanes 2019-11-21 13:15:12 -06:00
  • 789f787df2
         try on 4.05 for now Simon Cruanes 2019-11-21 13:09:56 -06:00
  • 9ef87a59e5
         chore: try github actions Simon Cruanes 2019-11-21 13:06:14 -06:00
  • 61b5e9cee2 chore: simplify dune file Simon Cruanes 2019-11-19 16:22:49 -06:00
  • 0aa7a4ea25 chore: update test config Simon Cruanes 2019-11-19 16:16:47 -06:00
  • 801e3d25b4 chore: update travis Simon Cruanes 2019-11-07 10:37:00 -06:00
  • 409fe49ff0 feat(bin): use stmlib-utils 0.1, with versionned API and new statements Simon Cruanes 2019-11-07 10:35:59 -06:00
  • 239cff7445 chore: update travis Simon Cruanes 2019-11-05 17:12:11 -06:00
  • 8162a841fe refactor: depend on smtlib-utils instead of having custom parser Simon Cruanes 2019-11-05 17:11:32 -06:00
  • 721b1874b7 fix: re-check CC after calling on-final-check Simon Cruanes 2019-11-01 16:07:05 -05:00
  • 3cd79ee4c9 refactor(th_bool): cache tseitin on absolute values Simon Cruanes 2019-11-01 15:53:12 -05:00
  • b9965ca709 feat(th-cstor): reimplement the theory Simon Cruanes 2019-11-01 15:11:09 -05:00
  • 2d1d6ee937 feat: in main, --dot forces --check Simon Cruanes 2019-11-01 15:10:57 -05:00
  • 5b3cadf1e1 fix: missing type equality Simon Cruanes 2019-11-01 15:10:43 -05:00
  • d4c3d3e443 cleanup: remove a few functions Simon Cruanes 2019-11-01 14:17:28 -05:00
  • 4875b07d0b feat: add Ite constructor in base-term, handle it in mini-cc Simon Cruanes 2019-10-30 15:41:52 -05:00
  • 09ead7c41a feat(mini-cc): add clear operation Simon Cruanes 2019-10-30 15:32:45 -05:00
  • 71db47f9ac test: more CC tests Simon Cruanes 2019-10-30 15:03:24 -05:00
  • c9f0141591 fix(mini-cc): handle not properly Simon Cruanes 2019-10-30 15:00:57 -05:00
  • be2bc6e0f6 fix(term): missing type constraint Simon Cruanes 2019-10-30 15:00:49 -05:00
  • 1428d43369 test: add some unit tests for mini-cc Simon Cruanes 2019-10-30 15:00:34 -05:00
  • 17aba9461c refactor(mini-cc): remove distinct API Simon Cruanes 2019-10-30 13:41:09 -05:00
  • 44e168495b cleanup: remove dead code Simon Cruanes 2019-10-30 13:41:02 -05:00
  • 9ddce6a186 feat(check-cc): add statistics Simon Cruanes 2019-10-30 13:31:04 -05:00
  • 7d8589accd refactor: change the functor stack Simon Cruanes 2019-10-29 15:06:19 -05:00
  • 94ba04a49e wip: resume work on th-cstors Simon Cruanes 2019-10-29 14:32:31 -05:00
  • 4ab1997b45 chore: add 4.09 in travis Simon Cruanes 2019-10-29 14:32:24 -05:00
  • 0031c64ea9 feat(th-bool-static): check for new terms in the CC in final check Simon Cruanes 2019-10-08 09:08:05 -05:00
  • d0b9c76629 Merge branch 'master' of github.com:c-cube/sidekick Simon Cruanes 2019-10-07 09:25:21 -05:00
  • 49a7446631 feat(th-bool-static): add non-traversable opaque boolean term Simon Cruanes 2019-10-05 18:37:49 -05:00
  • 1658887ea3 feat: basic production of models Simon Cruanes 2019-10-02 18:44:02 -05:00
  • 7552808c33 feat: add is_valid_literal filter to add_term_rec Simon Cruanes 2019-10-02 18:15:06 -05:00
  • 238226500a feat: add is_valid_literal filter to add_term_rec Simon Cruanes 2019-10-02 18:15:06 -05:00
  • 7fe6f07c0b split on_merge into two events: pre and post merge Alexander Bentkamp 2019-08-21 10:31:43 +02:00
  • cde983df86 add assert for Expl.mk_merge Alexander Bentkamp 2019-08-20 13:17:39 +02:00
  • a49b0295bc split on_merge into two events: pre and post merge Alexander Bentkamp 2019-08-21 10:31:43 +02:00
  • de85efe036 add assert for Expl.mk_merge Alexander Bentkamp 2019-08-20 13:17:39 +02:00
  • c766ebb61f feat: add skeleton for LRA feat-lra Simon Cruanes 2019-08-19 18:13:32 -05:00
  • 769b80030a feat: progress bar in solver Simon Cruanes 2019-07-31 04:36:32 -05:00
  • d527b2b945 fix: remove some module aliases for 4.08 Simon Cruanes 2019-07-31 03:25:04 -05:00
  • 2b40bd9db1 chore: add 4.08 to travis Simon Cruanes 2019-07-31 03:24:58 -05:00
  • 40464e4fe7 style: fix a typo Arnaud Spiwack 2019-06-22 00:55:01 +02:00
  • 33a7843162 feat: expose more from atoms Simon Cruanes 2019-06-13 10:43:04 -05:00
  • 2430eb754d feat(cc): make bitfields non-global; remove dead code Simon Cruanes 2019-06-11 11:08:44 -05:00
  • ed4ba4057f feat: solver actions are the same as CC actions Simon Cruanes 2019-06-11 10:28:00 -05:00
  • 3e7ef47fab feat: add CC.merge_t Simon Cruanes 2019-06-11 10:26:04 -05:00
  • 1212e219eb refactor: make backtrackable table polymorphic in values Simon Cruanes 2019-06-11 10:19:07 -05:00
  • 7b62dbcb4d wip: stats for msat wip-sat-stat Simon Cruanes 2019-06-10 16:04:14 -05:00