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

Put info about Msat.Solver higher in the readme

Browse source
This commit is contained in:
Guillaume Bury 2016-04-15 13:39:09 +02:00
parent f88a5dd514
commit e3fc66919d
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
README.md
View file

@ -15,6 +15,15 @@ This program is distributed under the Apache Software License version
## USAGE ## USAGE
### Generic SAT/SMT Solver
A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
as a functor which takes two modules :
- A representation of formulas (which implements the `Formula_intf.S` signature)
- A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions.
### Sat Solver ### Sat Solver
A ready-to-use SAT solver is available in the Sat module. It can be used A ready-to-use SAT solver is available in the Sat module. It can be used
@ -45,15 +54,6 @@ as shown in the following code :
let _ = Sat.solve () (* Should return Sat.Unsat *) let _ = Sat.solve () (* Should return Sat.Unsat *)
``` ```
### Generic SAT/SMT Solver
A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
as a functor which takes two modules :
- A representation of formulas (which implements the `Formula_intf.S` signature)
- A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions.
## INSTALLATION ## INSTALLATION
### Via opam ### Via opam