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

update index

Browse source
This commit is contained in:
Simon Cruanes 2021-08-27 09:49:42 -04:00
parent e9675743b0
commit 744f8d60b8
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
index.md
View file

@ -14,15 +14,16 @@ Sidekick is composed of a few libraries:
and a solver implementation based on [mSAT](https://github.com/Gbury/mSAT). and a solver implementation based on [mSAT](https://github.com/Gbury/mSAT).
`Sidekick_core` is the most important module to read there. `Sidekick_core` is the most important module to read there.
- `sidekick-arith` depends on [Zarith](https://github.com/ocaml/Zarith) - `sidekick-base` provides a concrete implementation of terms, types,
for arbitrary-precision computations, and provides a LRA theory based literals, etc. as well as an instantiation the SMT solver.
on an implementation of the Simplex algorithm. It also depends on [Zarith](https://github.com/ocaml/Zarith)
for arbitrary-precision computations.
- `sidekick-bin` is an executable that uses the previous building blocks - `sidekick-bin` is an executable that uses the previous building blocks
to implement a concrete SMT solver. It is useful for testing, but to implement a concrete SMT solver executable. It is useful for testing, but
can also be used as a normal SMT solver on the command line. can also be used as a normal SMT solver on the command line.
It contains examples of how to instantiate the functors of `sidekick` It contains examples of how to instantiate the functors of `sidekick`
and `sidekick-arith`. and `sidekick-base`.
## API Documentation ## API Documentation