Simon Cruanes
|
5faa1d6ef7
|
chore: try to build again
|
2021-07-18 08:04:56 -04:00 |
|
Simon Cruanes
|
1aa160fe56
|
use a pure sat solver for cnf files
|
2021-07-18 02:46:04 -04:00 |
|
Simon Cruanes
|
80b50e8744
|
refactor: add solver instance in sidekick base
move some functor instantiations from `sidekick-bin.smtlib` to
`sidekick-base.solver` so they're usable from a library.
|
2021-07-03 22:28:57 -04:00 |
|
Simon Cruanes
|
79bc3def3f
|
refactor to get sidekick-base library
|
2021-07-03 20:20:19 -04:00 |
|
Simon Cruanes
|
fafb001934
|
feat: add profiling system based on TEF
- a `Sidekick_util.Profile` module, deps-free
- an optional sidekick.tef library that needs unix+mtime
|
2020-12-22 16:27:45 -05:00 |
|
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 |
|