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

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

Browse source
This commit is contained in:
Guillaume Bury 2014-10-29 18:52:18 +01:00
commit 4acd669d6f
3 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Makefile
View file

@ -3,7 +3,7 @@
LOG=build.log LOG=build.log
COMP=ocamlbuild -log $(LOG) -use-ocamlfind -package num,zarith,unix -classic-display COMP=ocamlbuild -log $(LOG) -use-ocamlfind -package num,zarith,unix -classic-display
FLAGS= FLAGS=
DIRS=-Is smt,common DIRS=-Is sat,smt,common
DOC=msat.docdir/index.html DOC=msat.docdir/index.html
NAME=msat NAME=msat

13
README.md
View file

@ -19,8 +19,17 @@ This program is distributed under the Apache Software License version
## INSTALLATION ## INSTALLATION
============
You will need ocamlfind. ### 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

4
sat/solver.ml
View file

@ -14,7 +14,7 @@ open Format
module Make(F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) = struct module Make(F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) = struct
module Stypes = Solver_types.Make(F) module Stypes = Solver_types.Make(F)
module Ex = Explanation.Make(Stypes) module Ex = Explanation.Make(Stypes)
open Stypes open Stypes
@ -23,8 +23,6 @@ exception Sat
exception Unsat of clause list exception Unsat of clause list
exception Restart exception Restart
type env = type env =
{ {
(* si vrai, les contraintes sont deja fausses *) (* si vrai, les contraintes sont deja fausses *)