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

Added info about solver functor

Browse source
This commit is contained in:
Guillaume Bury 2015-03-03 17:06:16 +01:00
parent 926948d693
commit cdf8371394
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
README.md
View file

@ -45,7 +45,14 @@ as shown in the following code :
### Generic SAT/SMT Solver ### Generic SAT/SMT Solver
A modular implementation of the SMT algorithm can be found in the `Msat.` A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
as a functor which takes three modules :
- A log module for debug output
- 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