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

update readme

Browse source
This commit is contained in:
Simon Cruanes 2018-01-22 22:14:01 -06:00
parent ac396e8cf5
commit 9e3484d2b3
1 changed files with 17 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

102
README.md
View file

@ -1,107 +1,39 @@
# MSAT [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT)
# CDCL [![Build Status](https://travis-ci.org/c-cube/cdcl.svg?branch=master)](https://travis-ci.org/c-cube/CDCL)
MSAT is an OCaml library that features a modular SAT-solver and some
extensions (including SMT).
CDCL is an OCaml library with a functor to create SMT solvers following
the CDCL(T) approach (so called "lazy SMT").
It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero)
and its fork [mSAT](https://github.com/gbury/msat).
It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
## COPYRIGHT
This program is distributed under the Apache Software License version
2.0. See the enclosed file `LICENSE`.
## Documentation
See https://gbury.github.io/mSAT/
See https://c-cube.github.io/cdcl/
## INSTALLATION
## Installation
### Via opam
Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
Once the package is on [opam](http://opam.ocaml.org), just `opam install cdcl`.
For the development version, use:
opam pin add msat https://github.com/Gbury/mSAT.git
opam pin add msat https://github.com/c-cube/cdcl.git
### Manual installation
You will need ocamlfind and ocamlbuild. The command is:
You will need jbuilder. The command is:
make install
## USAGE
## Usage
### Generic SAT/SMT Solver
The main module is `CDCL`.
A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
as a functor which takes two modules :
A modular implementation of the SMT algorithm can be found in the `CDCL.Make` functor,
as a functor which takes a `Theory_intf.S` module
- 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.
- A dummy empty module to ensure generativity of the solver (solver modules heavily relies on
side effects to their internal state)
### Sat Solver
A ready-to-use SAT solver is available in the Sat module. It can be used
as shown in the following code :
```ocaml
(* Module initialization *)
module Sat = Msat.Sat.Make()
module E = Msat.Sat.Expr (* expressions *)
(* We create here two distinct atoms *)
let a = E.fresh () (* A 'new_atom' is always distinct from any other atom *)
let b = E.make 1 (* Atoms can be created from integers *)
(* We can try and check the satisfiability of some clauses --
here, the clause [a or b].
Sat.assume adds a list of clauses to the solver. *)
let() = Sat.assume [[a; b]]
let res = Sat.solve () (* Should return (Sat.Sat _) *)
(* The Sat solver has an incremental mutable state, so we still have
the clause [a or b] in our assumptions.
We add [not a] and [not b] to the state. *)
let () = Sat.assume [[E.neg a]; [E.neg b]]
let res = Sat.solve () (* Should return (Sat.Unsat _) *)
```
#### Formulas API
Writing clauses by hand can be tedious and error-prone.
The functor `Msat.Tseitin.Make` proposes a formula AST (parametrized by
atoms) and a function to convert these formulas into clauses:
```ocaml
(* Module initialization *)
module Sat = Msat.Sat.Make()
module E = Msat.Sat.Expr (* expressions *)
module F = Msat.Tseitin.Make(E)
(* We create here two distinct atoms *)
let a = E.fresh () (* A fresh atom is always distinct from any other atom *)
let b = E.make 1 (* Atoms can be created from integers *)
(* Let's create some formulas *)
let p = F.make_atom a
let q = F.make_atom b
let r = F.make_and [p; q]
let s = F.make_or [F.make_not p; F.make_not q]
(* We can try and check the satisfiability of the given formulas *)
let () = Sat.assume (F.make_cnf r)
let _ = Sat.solve () (* Should return (Sat.Sat _) *)
(* The Sat solver has an incremental mutable state, so we still have
* the formula 'r' in our assumptions *)
let () = Sat.assume (F.make_cnf s)
let _ = Sat.solve () (* Should return (Sat.Unsat _) *)
```
## Copyright
This program is distributed under the Apache Software License version
2.0. See the enclosed file `LICENSE`.