From aa47a442426ebefc67402a67b3ce4bae30767762 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 19 Jan 2019 15:56:36 -0600 Subject: [PATCH] feat: expose msat.sat as a proper library, with module `Int_lit` --- src/main/main.ml | 2 +- src/sat/{Expr_sat.ml => Int_lit.ml} | 0 src/sat/{Expr_sat.mli => Int_lit.mli} | 2 +- src/sat/Msat_sat.ml | 4 ++-- src/sat/Msat_sat.mli | 4 ++-- src/sat/dune | 3 ++- tests/icnf-solve/{Icnf_solve.ml => icnf_solve.ml} | 3 ++- tests/test_api.ml | 2 +- 8 files changed, 11 insertions(+), 9 deletions(-) rename src/sat/{Expr_sat.ml => Int_lit.ml} (100%) rename src/sat/{Expr_sat.mli => Int_lit.mli} (95%) rename tests/icnf-solve/{Icnf_solve.ml => icnf_solve.ml} (98%) diff --git a/src/main/main.ml b/src/main/main.ml index e2573b4f..e822dd1d 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -59,7 +59,7 @@ module Process = struct Format.printf "Unsat (%f/%f)@." t t' end - let conv_c c = List.rev_map S.Expr.make c + let conv_c c = List.rev_map S.Int_lit.make c let add_clauses cs = S.assume st @@ CCList.map conv_c cs diff --git a/src/sat/Expr_sat.ml b/src/sat/Int_lit.ml similarity index 100% rename from src/sat/Expr_sat.ml rename to src/sat/Int_lit.ml diff --git a/src/sat/Expr_sat.mli b/src/sat/Int_lit.mli similarity index 95% rename from src/sat/Expr_sat.mli rename to src/sat/Int_lit.mli index c4803bc9..6845d161 100644 --- a/src/sat/Expr_sat.mli +++ b/src/sat/Int_lit.mli @@ -1,5 +1,5 @@ -(** The module defining formulas *) +(** {1 The module defining formulas} *) (** SAT Formulas diff --git a/src/sat/Msat_sat.ml b/src/sat/Msat_sat.ml index 007f385b..bd4b3dd5 100644 --- a/src/sat/Msat_sat.ml +++ b/src/sat/Msat_sat.ml @@ -3,6 +3,6 @@ MSAT is free software, using the Apache license, see file LICENSE Copyright 2016 Guillaume Bury *) -module Expr = Expr_sat -include Msat.Make_pure_sat(Expr) +module Int_lit = Int_lit +include Msat.Make_pure_sat(Int_lit) diff --git a/src/sat/Msat_sat.mli b/src/sat/Msat_sat.mli index b36bda05..e2897626 100644 --- a/src/sat/Msat_sat.mli +++ b/src/sat/Msat_sat.mli @@ -9,8 +9,8 @@ Copyright 2016 Guillaume Bury atomic propositions. *) -module Expr = Expr_sat +module Int_lit = Int_lit -include Msat.S with type Formula.t = Expr.t and type theory = unit +include Msat.S with type Formula.t = Int_lit.t and type theory = unit (** A functor that can generate as many solvers as needed. *) diff --git a/src/sat/dune b/src/sat/dune index c321e17c..b5940271 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -1,7 +1,8 @@ (library (name msat_sat) - ; private + (public_name msat.sat) + (synopsis "purely boolean interface to Msat") (libraries msat) (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) (ocamlopt_flags :standard -O3 -color always diff --git a/tests/icnf-solve/Icnf_solve.ml b/tests/icnf-solve/icnf_solve.ml similarity index 98% rename from tests/icnf-solve/Icnf_solve.ml rename to tests/icnf-solve/icnf_solve.ml index afc8b61d..3fc3cb7f 100644 --- a/tests/icnf-solve/Icnf_solve.ml +++ b/tests/icnf-solve/icnf_solve.ml @@ -58,7 +58,7 @@ end = struct end module Solver = struct - module F = Msat_sat.Expr + module F = Msat_sat.Int_lit module S = Msat_sat type t = S.t @@ -85,6 +85,7 @@ let solve_with_solver ~debug file : unit = | Parse.Add_clause c -> if debug then ( Printf.printf "add_clause %a\n%!" pp_arr c; + Msat.Log.set_debug 5; ); let r = Solver.add_clause s c in if r then process_problem() diff --git a/tests/test_api.ml b/tests/test_api.ml index bef40497..1b3da279 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -6,7 +6,7 @@ Copyright 2014 Simon Cruanes (* Tests that require the API *) -module F = Msat_sat.Expr +module F = Msat_sat.Int_lit module S = Msat_sat let (|>) x f = f x