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

Merge branch 'master' of github.com:Gbury/mSAT

Browse source
This commit is contained in:
Guillaume Bury 2017-01-12 13:41:26 +01:00
commit a5733c818d
6 changed files with 41 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
README.md
View file

@ -1,7 +1,7 @@
# MSAT [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT)
MSAT is an OCaml library that features a modular SAT-solver and some
extensions (including SMT). This is **work in progress**.
extensions (including SMT).
It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
@ -16,6 +16,21 @@ This program is distributed under the Apache Software License version
See https://gbury.github.io/mSAT/
## INSTALLATION
### Via opam
Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
For the development version, use:
opam pin add msat https://github.com/Gbury/mSAT.git
### Manual installation
You will need ocamlfind and ocamlbuild. The command is:
make install
## USAGE
### Generic SAT/SMT Solver
@ -60,20 +75,3 @@ as shown in the following code :
let _ = Sat.solve () (* Should return (Sat.Unsat _) *)
```
## INSTALLATION
### Via opam
Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
For the development version, use:
opam pin add msat https://github.com/Gbury/mSAT.git
### Manual installation
You will need ocamlfind. The command is:
make install

5
src/core/plugin_intf.ml
View file

@ -11,6 +11,11 @@
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
(** McSat Theory

5
src/core/solver_types.ml
View file

@ -10,6 +10,11 @@
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
open Printf

5
src/core/solver_types.mli
View file

@ -10,6 +10,11 @@
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
(** Internal types (implementation)

5
src/core/solver_types_intf.ml
View file

@ -10,6 +10,11 @@
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
(** Internal types (interface)

5
src/core/theory_intf.ml
View file

@ -11,6 +11,11 @@
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
(** SMT Theory