simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 04:05:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
1392 commits 53 branches 1 tag 17 MiB
Commit graph

1392 commits

This branch
This branch
All branches
Author SHA1 Message Date
Simon Cruanes
b4ef8e4e67 chore: use a different travis script 2020-02-24 18:03:38 -06:00
Simon Cruanes
65bd7e7744 prepare for 0.8.2 2020-02-24 17:40:49 -06:00
Simon Cruanes
0b283a384d test: add some regression tests 2020-02-21 16:46:57 -06:00
Simon Cruanes
da3cb275be chore: version bump on containers 2020-02-21 13:53:41 -06:00
Simon Cruanes
7cfdb3507c fix(th-data): fix acyclicity 2020-02-20 19:32:33 -06:00
Simon Cruanes
4e1b35d2c3 test: add regression test 2020-02-17 12:30:58 -06:00
Simon Cruanes
bb449257d8 fix(solver): in final-check, fixpoint until CC has no merges 2020-02-15 14:40:57 -06:00
Simon Cruanes
93b993825b chore(make): also remove trailing spaces in make reindent 2020-02-15 14:36:39 -06:00
Simon Cruanes
11d8f8e879 remove dead code, some printing info 2020-02-15 14:33:44 -06:00
Simon Cruanes
6aae70f15a test: add more regression tests for datatypes 2020-01-17 19:12:50 -06:00
Simon Cruanes
b2c047190f fix(data): check is-a lits in final-check 2020-01-17 19:12:06 -06:00
Simon Cruanes
eb64acb31f fix(data): reimplement acyclicity check 2020-01-17 19:10:46 -06:00
Simon Cruanes
e21dea4780 feat(cc): flag some explanations as being theory-induced 2020-01-17 18:49:14 -06:00
Simon Cruanes
5bcecfd68c Merge branch 'wip-data' 2020-01-14 23:02:49 -06:00
Simon Cruanes
c4a4edde3a chore: fix opam file 2020-01-14 23:00:07 -06:00
Simon Cruanes
407a7e83f7 fix: allow conflicts below decision level in Make_cdcl_t 2020-01-14 22:56:01 -06:00
Simon Cruanes
a31b2b36ef fixes: add missing expl in monoids; handle is-c t 2020-01-14 22:41:33 -06:00
Simon Cruanes
ef60d1466f feat: better debug message 2020-01-14 21:23:02 -06:00
Simon Cruanes
b332e8ceb0 fix: preprocess away "ite" 2020-01-14 20:23:23 -06:00
Simon Cruanes
17a09f2cbc test: add some regression tests 2020-01-14 20:23:14 -06:00
Simon Cruanes
48d6b57383 test: enable progress by default 2020-01-08 19:51:25 -06:00
Simon Cruanes
dbf88279a1 test: more reg tests 2019-12-28 09:19:17 -06:00
Simon Cruanes
10b9febe9d fix(th-data): avoid redundant explanations 2019-12-28 09:00:59 -06:00
Simon Cruanes
e58b29da02 fix(term): hashconsing error leading to non termination 2019-12-28 08:49:14 -06:00
Simon Cruanes
8749cfff0a test: add reg test 2019-12-28 08:49:04 -06:00
Simon Cruanes
b250587a5f tst: add some regression tests; remove dead file 2019-12-28 08:34:42 -06:00
Simon Cruanes
6f67593be1 feat(data): fixes (decide args of is-a/select; rearrange reduction rules) 2019-12-28 08:31:52 -06:00
Simon Cruanes
9ba5f508ce feat(main): simpler computation of version 2019-12-28 08:31:41 -06:00
Simon Cruanes
62b1d83cd6 debug: add type checking in CC.merge 2019-12-28 08:19:59 -06:00
Simon Cruanes
91e9b6cc2c feat: initial support for is-a/select 2019-12-28 07:08:23 -06:00
Simon Cruanes
6aafaad48f feat(data): store is-a/select parents in a monoid 2019-12-28 06:15:50 -06:00
Simon Cruanes
858ffb6f25 chore: add --progress in makefile 2019-12-28 05:19:19 -06:00
Simon Cruanes
9293553925 feat(th-data): first draft of acyclicity 2019-12-28 05:19:01 -06:00
Simon Cruanes
6061b5843e fix(th-data): fix merge explanation in cstor monoid 2019-12-28 05:19:01 -06:00
Simon Cruanes
d52fb1e5fd core: add iter_all in monoid class 2019-12-28 05:19:01 -06:00
Simon Cruanes
bf23f7c826 fix(cc): remove too powerful assertion in CC 2019-12-28 05:19:01 -06:00
Simon Cruanes
c54ee2310e test: better conf for sidekick 2019-12-28 05:19:01 -06:00
Simon Cruanes
c4d2a800ab test: update test config to use $cur_dir 2019-12-28 05:17:47 -06:00
Simon Cruanes
0ec9c1683f test: modify logitest config file 2019-12-28 05:17:47 -06:00
Simon Cruanes
787b9404af refactor: change debug levels 2019-12-28 05:17:47 -06:00
Simon Cruanes
a4e3fd5a69 feat: provide simple repr->monoid mapping in core 2019-12-28 05:17:47 -06:00
Simon Cruanes
7c951c08ff wip: use t=c instead of (is _ c) t for nullary constructors 2019-12-28 05:17:47 -06:00
Simon Cruanes
c55e7a613b test: add some basic datatype tests 2019-12-28 05:17:47 -06:00
Simon Cruanes
444a0b9f85 wip: theory of datatypes 2019-12-28 05:17:47 -06:00
Simon Cruanes
8c5e28da28 wip: theory of datatypes 2019-12-28 05:17:47 -06:00
Simon Cruanes
949e079867 wip: add datatypes 2019-12-28 05:17:47 -06:00
Simon Cruanes
88550716d8 prepare for 0.8.1 2019-12-16 16:43:49 -06:00
Simon Cruanes
14f68749a5 add more tests 2019-12-13 17:55:10 -06:00
Simon Cruanes
d6c003390d rename logitest to benchpress 2019-12-13 16:38:01 -06:00
Simon Cruanes
85b0066660 test: update logitest config and makefile 2019-12-11 18:37:37 -06:00