split some features into minismt lib

minismt.opam

@@ -0,0 +1,23 @@
+opam-version: "1.2"
+name: "minismt"
+license: "Apache"
+version: "dev"
+author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
+maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
+build: ["jbuilder" "build" "@install" "-p" name]
+build-doc: ["jbuilder" "build" "@doc" "-p" name]
+install: ["jbuilder" "install" name]
+remove: ["jbuilder" "uninstall" name]
+depends: [
+  "ocamlfind" {build}
+  "jbuilder" {build}
+  "dolmen"
+]
+available: [
+  ocaml-version >= "4.03.0"
+]
+tags: [ "sat" "smt" ]
+homepage: "https://github.com/Gbury/mSAT"
+dev-repo: "https://github.com/Gbury/mSAT.git"
+bug-reports: "https://github.com/Gbury/mSAT/issues/"
+

src/main/jbuild

@@ -6,7 +6,7 @@
   ((name main)
    (public_name msat_solver)
    (package msat_solver)
-   (libraries (msat msat.backend msat.sat msat.smt msat.mcsat dolmen))
+   (libraries (msat msat.backend minismt.sat minismt.smt minismt.mcsat dolmen))
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
    (ocamlopt_flags (:standard -O3 -color always
                     -unbox-closures -unbox-closures-factor 20))

src/main/main.ml

@@ -28,7 +28,7 @@ end
 
 module Make
     (S : Msat.S)
-    (T : Msat_solver.Type.S with type atom := S.atom)
+    (T : Minismt.Type.S with type atom := S.atom)
   : sig
     val do_task : Dolmen.Statement.t -> unit
   end = struct
@@ -106,9 +106,9 @@ module Make
         Dolmen.Statement.print s
 end
 
-module Sat = Make(Msat_sat.Make(struct end))(Msat_sat.Type)
-module Smt = Make(Msat_smt.Make(struct end))(Msat_smt.Type)
-module Mcsat = Make(Msat_mcsat.Make(struct end))(Msat_smt.Type)
+module Sat = Make(Minismt_sat.Make(struct end))(Minismt_sat.Type)
+module Smt = Make(Minismt_smt.Make(struct end))(Minismt_smt.Type)
+module Mcsat = Make(Minismt_mcsat.Make(struct end))(Minismt_smt.Type)
 
 let solver = ref (module Sat : S)
 let solver_list = [
@@ -227,8 +227,8 @@ let () =
   | Incorrect_model ->
     Format.printf "Internal error : incorrect *sat* model@.";
     exit 4
-  | Msat_sat.Type.Typing_error (msg, t)
-  | Msat_smt.Type.Typing_error (msg, t) ->
+  | Minismt_sat.Type.Typing_error (msg, t)
+  | Minismt_smt.Type.Typing_error (msg, t) ->
     let b = Printexc.get_backtrace () in
     let loc = match t.Dolmen.Term.loc with
       | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0

src/mcsat/Minismt_mcsat.ml

@@ -5,9 +5,9 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make() =
-  Msat_solver.Mcsolver.Make(struct
+  Minismt.Mcsolver.Make(struct
     type proof = unit
-    module Term = Msat_smt.Expr.Term
-    module Formula = Msat_smt.Expr.Atom
+    module Term = Minismt_smt.Expr.Term
+    module Formula = Minismt_smt.Expr.Atom
   end)(Plugin_mcsat)()
 

src/mcsat/Minismt_mcsat.mli

@@ -4,5 +4,5 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make() : Msat_solver.Solver.S with type St.formula = Msat_smt.Expr.atom
+module Make() : Minismt.Solver.S with type St.formula = Minismt_smt.Expr.atom
 

src/mcsat/jbuild

@@ -1,9 +1,9 @@
 ; vim:ft=lisp:
 
 (library
-  ((name msat_mcsat)
-   (public_name msat.mcsat)
-   (libraries (msat msat.solver msat.smt))
+  ((name minismt_mcsat)
+   (public_name minismt.mcsat)
+   (libraries (msat minismt minismt.smt))
    (synopsis "mcsat interface")
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
    (ocamlopt_flags (:standard -O3 -bin-annot

src/mcsat/plugin_mcsat.ml

@@ -1,7 +1,7 @@
 
 (* Module initialization *)
 
-module Expr_smt = Msat_smt.Expr
+module Expr_smt = Minismt_smt.Expr
 
 module E = Eclosure.Make(Expr_smt.Term)
 module H = Backtrack.Hashtbl(Expr_smt.Term)

src/sat/Minismt_sat.ml

@@ -7,5 +7,5 @@ module Expr = Expr_sat
 module Type = Type_sat
 
 module Make() =
-  Msat_solver.Solver.Make(Expr)(Msat_solver.Solver.DummyTheory(Expr))()
+  Minismt.Solver.Make(Expr)(Minismt.Solver.DummyTheory(Expr))()
 

src/sat/Minismt_sat.mli

@@ -12,6 +12,6 @@ Copyright 2016 Guillaume Bury
 module Expr = Expr_sat
 module Type = Type_sat
 
-module Make() : Msat_solver.Solver.S with type St.formula = Expr.t
+module Make() : Minismt.Solver.S with type St.formula = Expr.t
 (** A functor that can generate as many solvers as needed. *)
 

src/sat/jbuild

@@ -1,9 +1,9 @@
 ; vim:ft=lisp:
 
 (library
-  ((name msat_sat)
-   (public_name msat.sat)
-   (libraries (msat msat.tseitin msat.solver))
+  ((name minismt_sat)
+   (public_name minismt.sat)
+   (libraries (msat msat.tseitin minismt dolmen))
    (synopsis "sat interface")
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
    (ocamlopt_flags (:standard -O3 -bin-annot

src/sat/type_sat.mli

@@ -8,5 +8,5 @@ Copyright 2014 Simon Cruanes
     This module provides functions to parse terms from the untyped syntax tree
     defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
 
-include Msat_solver.Type.S with type atom := Expr_sat.t
+include Minismt.Type.S with type atom := Expr_sat.t
 

src/smt/Minismt_smt.ml

@@ -7,8 +7,7 @@ Copyright 2014 Simon Cruanes
 module Expr = Expr_smt
 module Type = Type_smt
 
-module Th = Msat_solver.Solver.DummyTheory(Expr_smt.Atom)
+module Th = Minismt.Solver.DummyTheory(Expr.Atom)
 
-module Make() =
-  Msat_solver.Solver.Make(Expr_smt.Atom)(Th)()
+module Make() = Minismt.Solver.Make(Expr.Atom)(Th)()
 

src/smt/Minismt_smt.mli

@@ -7,5 +7,5 @@ Copyright 2014 Simon Cruanes
 module Expr = Expr_smt
 module Type = Type_smt
 
-module Make() : Msat_solver.Solver.S with type St.formula = Expr_smt.atom
+module Make() : Minismt.Solver.S with type St.formula = Expr_smt.atom
 

src/smt/jbuild

@@ -1,9 +1,9 @@
 ; vim:ft=lisp:
 
 (library
-  ((name msat_smt)
-   (public_name msat.smt)
-   (libraries (msat msat.solver msat.tseitin dolmen))
+  ((name minismt_smt)
+   (public_name minismt.smt)
+   (libraries (msat minismt msat.tseitin dolmen))
    (synopsis "smt interface")
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
    (ocamlopt_flags (:standard -O3 -bin-annot

src/smt/type_smt.mli

@@ -3,5 +3,5 @@
     This module provides functions to parse terms from the untyped syntax tree
     defined in Dolmen, and generate formulas as defined in the Expr_smt module. *)
 
-include Msat_solver.Type.S with type atom := Expr_smt.Atom.t
+include Minismt.Type.S with type atom := Expr_smt.Atom.t
 

src/solver/jbuild

@@ -1,10 +1,10 @@
 ; vim:ft=lisp:
 
 (library
-  ((name msat_solver)
-   (public_name msat.solver)
+  ((name minismt)
+   (public_name minismt)
    (libraries (msat dolmen))
-   (synopsis "mcsat solver util")
+   (synopsis "minismt")
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
    (ocamlopt_flags (:standard -O3 -bin-annot
                     -unbox-closures -unbox-closures-factor 20))

tests/jbuild

@@ -2,7 +2,7 @@
 
 (executable
   ((name test_api)
-   (libraries (msat msat.backend msat.sat msat.smt msat.mcsat dolmen))
+   (libraries (msat msat.tseitin msat.backend minismt.sat minismt.smt minismt.mcsat dolmen))
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
    (ocamlopt_flags (:standard -O3 -color always
                     -unbox-closures -unbox-closures-factor 20))

tests/test_api.ml

@@ -8,7 +8,7 @@ Copyright 2014 Simon Cruanes
 
 open Msat
 
-module F = Msat_sat.Expr
+module F = Minismt_sat.Expr
 module T = Msat_tseitin.Make(F)
 
 let (|>) x f = f x
@@ -46,7 +46,7 @@ end
 
 let mk_solver (): (module BASIC_SOLVER) =
   let module S = struct
-    include Msat_sat.Make(struct end)
+    include Minismt_sat.Make(struct end)
     let solve ?assumptions ()= match solve ?assumptions() with
       | Sat _ ->
         R_sat