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

Fixed typo + added ocaml annotation in markdown

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

10
README.md
View file

@ -15,16 +15,19 @@ This program is distributed under the Apache Software License version
## USAGE ## USAGE
### 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
as shown in the following code : as shown in the following code :
```ocaml
(* Module initialization *) (* Module initialization *)
module F = Msat.Sat.Tseitin module F = Msat.Sat.Tseitin
module Sat = Msat.Sat.Make(Msat.Log) module Sat = Msat.Sat.Make(Msat.Log)
(* We create here two distinct atoms *) (* We create here two distinct atoms *)
let a = Sat.new_atom () (* A 'new_atom' is always distinct from any other atom *) let a = Sat.new_atom () (* A 'new_atom' is always distinct from any other atom *)
let b = Sat.make 1 (* Atoms can be creted from integers *) let b = Sat.make 1 (* Atoms can be created from integers *)
(* Let's create some formulas *) (* Let's create some formulas *)
let p = F.make_and [a; b] let p = F.make_and [a; b]
@ -38,6 +41,11 @@ as shown in the following code :
* the formula 'p' in our assumptions *) * the formula 'p' in our assumptions *)
Sat.assume (F.make_cnf q) Sat.assume (F.make_cnf q)
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.`
## INSTALLATION ## INSTALLATION