/
opam
38 lines (37 loc) · 1.18 KB
/
opam
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
opam-version: "2.0"
maintainer: ["guillaume.bury@gmail.com" "simon.cruanes@inria.fr"]
authors: [
"Sylvain Conchon"
"Alain Mebsout"
"Stephane Lecuyer"
"Simon Cruanes"
"Guillaume Bury"
]
homepage: "https://github.com/Gbury/mSAT"
bug-reports: "https://github.com/Gbury/mSAT/issues/"
license: "Apache-1.0+"
tags: ["sat" "smt"]
dev-repo: "git+https://github.com/Gbury/mSAT.git"
build: [
[make "disable_log"]
[make "lib"]
]
install: [make "install"]
remove: ["ocamlfind" "remove" "msat"]
depends: [
"ocaml" {>= "4.00.1" & < "5.0.0"}
"ocamlfind" {build}
"ocamlbuild" {build}
]
synopsis: "Modular sat/smt solver"
description: """
This library provides functor to easily build a SAT, SMT and/or McSAT solver given an implementation of terms. Current features of the solver are:
- proof output
- push/pop operations
- CNF transformation tools
This project derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero), but does not provide any built-in theories, it is designed to let the users use their own implementation of terms and theories."""
flags: light-uninstall
url {
src: "https://github.com/Gbury/mSAT/archive/v0.4.1.tar.gz"
checksum: "md5=e5a09e49d9bc9f5358af94c84e53a822"
}