Commit graph

865 commits

Author SHA1 Message Date
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
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
Simon Cruanes
682edc4640 test: update logitest config 2019-12-09 17:40:57 -06:00
Simon Cruanes
ef77e1e729 add promoted sidekick-version 2019-12-09 12:12:24 -06:00
Simon Cruanes
c63887a1f0 feat: add --version flag 2019-12-09 11:56:22 -06:00
Simon Cruanes
10cfa137b6 feat: handle parsing of .cnf files 2019-11-23 13:41:03 -06:00
Simon Cruanes
678bf5e03d test: update expect field in toml 2019-11-23 13:23:30 -06:00
Simon Cruanes
f1fc429b5a add basic test for th-cstor 2019-11-23 13:23:30 -06:00
Simon Cruanes
e414112010 test: add some basic datatype tests 2019-11-23 13:23:30 -06:00
Simon Cruanes
c3be2411bf wip: th data 2019-11-23 13:23:30 -06:00
Simon Cruanes
9b99560130 feat: handle typechecking and term building for datatypes 2019-11-23 13:23:30 -06:00
Simon Cruanes
3327c86841 refactor(smtlib): remove intermediate typed AST, type directly into terms 2019-11-23 13:23:30 -06:00
Simon Cruanes
1a71535178
chore: try github actions (#3)
* chore: try github actions
2019-11-21 13:35:52 -06:00
Simon Cruanes
61b5e9cee2 chore: simplify dune file 2019-11-19 16:22:49 -06:00
Simon Cruanes
0aa7a4ea25 chore: update test config 2019-11-19 16:16:47 -06:00
Simon Cruanes
801e3d25b4 chore: update travis 2019-11-07 10:37:00 -06:00
Simon Cruanes
409fe49ff0 feat(bin): use stmlib-utils 0.1, with versionned API and new statements 2019-11-07 10:35:59 -06:00
Simon Cruanes
239cff7445 chore: update travis 2019-11-05 17:12:11 -06:00
Simon Cruanes
8162a841fe refactor: depend on smtlib-utils instead of having custom parser 2019-11-05 17:11:32 -06:00
Simon Cruanes
721b1874b7 fix: re-check CC after calling on-final-check 2019-11-01 17:04:36 -05:00
Simon Cruanes
3cd79ee4c9 refactor(th_bool): cache tseitin on absolute values 2019-11-01 15:53:12 -05:00
Simon Cruanes
b9965ca709 feat(th-cstor): reimplement the theory 2019-11-01 15:11:19 -05:00
Simon Cruanes
2d1d6ee937 feat: in main, --dot forces --check 2019-11-01 15:10:57 -05:00
Simon Cruanes
5b3cadf1e1 fix: missing type equality 2019-11-01 15:10:43 -05:00
Simon Cruanes
d4c3d3e443 cleanup: remove a few functions 2019-11-01 14:17:28 -05:00
Simon Cruanes
4875b07d0b feat: add Ite constructor in base-term, handle it in mini-cc 2019-10-30 15:41:52 -05:00
Simon Cruanes
09ead7c41a feat(mini-cc): add clear operation 2019-10-30 15:32:45 -05:00