diff --git a/minismt.opam b/minismt.opam new file mode 100644 index 00000000..1236ffbb --- /dev/null +++ b/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/" + diff --git a/src/main/jbuild b/src/main/jbuild index 08a42162..19dae05d 100644 --- a/src/main/jbuild +++ b/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)) diff --git a/src/main/main.ml b/src/main/main.ml index 69a2e727..f018d8fa 100644 --- a/src/main/main.ml +++ b/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 diff --git a/src/mcsat/Msat_mcsat.ml b/src/mcsat/Minismt_mcsat.ml similarity index 62% rename from src/mcsat/Msat_mcsat.ml rename to src/mcsat/Minismt_mcsat.ml index b0e2e2b8..fcd928e3 100644 --- a/src/mcsat/Msat_mcsat.ml +++ b/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)() diff --git a/src/mcsat/Msat_mcsat.mli b/src/mcsat/Minismt_mcsat.mli similarity index 62% rename from src/mcsat/Msat_mcsat.mli rename to src/mcsat/Minismt_mcsat.mli index 8055abc1..254699a6 100644 --- a/src/mcsat/Msat_mcsat.mli +++ b/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 diff --git a/src/mcsat/jbuild b/src/mcsat/jbuild index 5c4061d3..692db5f8 100644 --- a/src/mcsat/jbuild +++ b/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 diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml index 460b49fe..d1c588c7 100644 --- a/src/mcsat/plugin_mcsat.ml +++ b/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) diff --git a/src/sat/Msat_sat.ml b/src/sat/Minismt_sat.ml similarity index 69% rename from src/sat/Msat_sat.ml rename to src/sat/Minismt_sat.ml index a706355a..d1e8b933 100644 --- a/src/sat/Msat_sat.ml +++ b/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))() diff --git a/src/sat/Msat_sat.mli b/src/sat/Minismt_sat.mli similarity index 83% rename from src/sat/Msat_sat.mli rename to src/sat/Minismt_sat.mli index a8c5fa5d..8c34b184 100644 --- a/src/sat/Msat_sat.mli +++ b/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. *) diff --git a/src/sat/jbuild b/src/sat/jbuild index 86386d7a..82068bfb 100644 --- a/src/sat/jbuild +++ b/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 diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli index ae32ddd2..a088602c 100644 --- a/src/sat/type_sat.mli +++ b/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 diff --git a/src/smt/Msat_smt.ml b/src/smt/Minismt_smt.ml similarity index 59% rename from src/smt/Msat_smt.ml rename to src/smt/Minismt_smt.ml index 2cae3821..6d25bf9b 100644 --- a/src/smt/Msat_smt.ml +++ b/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)() diff --git a/src/smt/Msat_smt.mli b/src/smt/Minismt_smt.mli similarity index 70% rename from src/smt/Msat_smt.mli rename to src/smt/Minismt_smt.mli index 39f1231d..d2e99f39 100644 --- a/src/smt/Msat_smt.mli +++ b/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 diff --git a/src/smt/jbuild b/src/smt/jbuild index 843fa9c3..9999f849 100644 --- a/src/smt/jbuild +++ b/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 diff --git a/src/smt/type_smt.mli b/src/smt/type_smt.mli index 7593432b..1613debb 100644 --- a/src/smt/type_smt.mli +++ b/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 diff --git a/src/solver/jbuild b/src/solver/jbuild index f9e40772..f3176323 100644 --- a/src/solver/jbuild +++ b/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)) diff --git a/tests/jbuild b/tests/jbuild index 988fae01..deab296d 100644 --- a/tests/jbuild +++ b/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)) diff --git a/tests/test_api.ml b/tests/test_api.ml index 2d9aa422..69c1e526 100644 --- a/tests/test_api.ml +++ b/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