diff --git a/Makefile b/Makefile index 1f8914c8..7a091109 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind -package num,zarith,unix -classic-display FLAGS= -DIRS=-Is smt,common +DIRS=-Is sat,smt,common DOC=msat.docdir/index.html NAME=msat diff --git a/README.md b/README.md index 0dcd0fac..fc46d9b0 100644 --- a/README.md +++ b/README.md @@ -19,8 +19,17 @@ This program is distributed under the Apache Software License version ## 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 + diff --git a/sat/solver.ml b/sat/solver.ml index b1e0b45c..474dfd6b 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -14,7 +14,7 @@ open Format 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) open Stypes @@ -23,8 +23,6 @@ exception Sat exception Unsat of clause list exception Restart - - type env = { (* si vrai, les contraintes sont deja fausses *)