Simon Cruanes
|
3449404964
|
refactor: move base-term to sidekick-arith
|
2020-10-10 17:43:42 -04:00 |
|
Simon Cruanes
|
349d884664
|
chore: add sidekick-arith library, depends on zarith
|
2020-10-10 17:18:20 -04:00 |
|
Simon Cruanes
|
e9931b377c
|
remove bloody warn-error
|
2020-10-10 16:00:21 -04:00 |
|
Simon Cruanes
|
95edfd9aa9
|
wip: LRA theory
|
2020-09-23 21:58:54 -04:00 |
|
Simon Cruanes
|
8c5e28da28
|
wip: theory of datatypes
|
2019-12-28 05:17:47 -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
|
8162a841fe
|
refactor: depend on smtlib-utils instead of having custom parser
|
2019-11-05 17:11:32 -06:00 |
|
Simon Cruanes
|
70e4c655a2
|
refactor: split smtlib+bin into their own opam package
|
2019-06-07 17:59:07 -05:00 |
|
Simon Cruanes
|
357dc73426
|
feat(check): use mini-cc to check CC conflicts on the fly
|
2019-06-07 14:47:52 -05:00 |
|
Simon Cruanes
|
2e7ab9ba9b
|
wip: simplify a lot and only keep th-bool-static in the functor
|
2019-06-05 16:53:13 -05:00 |
|
Simon Cruanes
|
080a20480f
|
refactor: continue functorization of sidekick
|
2019-05-27 19:55:21 -05:00 |
|
Simon Cruanes
|
6e9e95c233
|
wip: functorize everything
|
2019-05-26 23:20:47 -05:00 |
|
Simon Cruanes
|
342dba4533
|
wip: new micro-theories in CC
|
2019-02-26 22:46:40 -06:00 |
|
Simon Cruanes
|
27d1841f6b
|
wip: migrate to msat 0.8
|
2019-01-28 21:09:57 -06:00 |
|
Simon Cruanes
|
4fadbeb04d
|
chore: migrate to dune
|
2019-01-18 18:37:26 -06:00 |
|