Removed module alias for SAT expressions

src/doc.txt

@@ -38,7 +38,6 @@ An instanciation of a pure sat solver is also provided:
 
 {!modules:
 Sat
-Expr_sat
 }
 
 Lastly, mSAT also provides an implementation of Tseitin's CNF conversion:

src/msat.mlpack

@@ -29,5 +29,4 @@ Tseitin
 
 # Pure Sat solver
 Sat
-Expr_sat
 

src/msat.odocl

@@ -28,7 +28,6 @@ backend/Backend_intf
 
 # SAT solver frontend
 sat/Sat
-sat/Expr_sat
 #sat/Type_sat
 
 # SMT solver frontend

src/sat/expr_sat.ml

@@ -1,64 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2016 Guillaume Bury
-Copyright 2016 Simon Cruanes
-*)
-
-exception Bad_atom
-
-type t = int
-type proof = unit
-
-let max_lit = max_int
-let max_fresh = ref (-1)
-let max_index = ref 0
-
-let _make i =
-  if i <> 0 && (abs i) < max_lit then begin
-    max_index := max !max_index (abs i);
-    i
-  end else
-    raise Bad_atom
-
-let dummy = 0
-
-let neg a = - a
-
-let norm a =
-  abs a, if a < 0 then
-    Formula_intf.Negated
-  else
-    Formula_intf.Same_sign
-
-let abs = abs
-
-let sign i = i > 0
-
-let apply_sign b i = if b then i else neg i
-
-let set_sign b i = if b then abs i else neg (abs i)
-
-let hash (a:int) = a land max_int
-let equal (a:int) b = a=b
-let compare (a:int) b = Pervasives.compare a b
-
-let make i = _make (2 * i)
-
-let fresh, iter =
-  let create () =
-    incr max_fresh;
-    _make (2 * !max_fresh + 1)
-  in
-  let iter: (t -> unit) -> unit = fun f ->
-    for j = 1 to !max_index do
-      f j
-    done
-  in
-  create, iter
-
-let print fmt a =
-  Format.fprintf fmt "%s%s%d"
-    (if a < 0 then "~" else "")
-    (if a mod 2 = 0 then "v" else "f")
-    ((abs a) / 2)
-

src/sat/expr_sat.mli

@@ -1,22 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2016 Guillaume Bury
-Copyright 2016 Simon Cruanes
-*)
-
-(** SAT Formulas
-
-    This modules implements formuals adequate for use in a pure SAT Solver.
-    Atomic formuals are represented using integers, that should allow
-    near optimal efficiency (both in terms of space and time).
-*)
-
-include Formula_intf.S
-(** This modules implements the requirements for implementing an SAT Solver. *)
-
-val make : int -> t
-(** Make a proposition from an integer. *)
-
-val fresh : unit -> t
-(** Make a fresh atom *)
-

src/sat/sat.ml

@@ -3,7 +3,79 @@ MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2016 Guillaume Bury
 *)
 
-module Expr = Expr_sat
+module Expr = struct
+
+  exception Bad_atom
+  (** Exception raised if an atom cannot be created *)
+
+  type proof
+  (** A empty type for proofs *)
+
+  type t = int
+  (** Atoms are represented as integers. [-i] begin the negation of [i].
+      Additionally, since we nee dot be able to create fresh atoms, we
+      use even integers for user-created atoms, and odd integers for the
+      fresh atoms. *)
+
+  let max_lit = max_int
+
+  (* Counters *)
+  let max_index = ref 0
+  let max_fresh = ref (-1)
+
+  (** Internal function for creating atoms.
+      Updates the internal counters *)
+  let _make i =
+    if i <> 0 && (abs i) < max_lit then begin
+      max_index := max !max_index (abs i);
+      i
+    end else
+      raise Bad_atom
+
+  (** A dummy atom *)
+  let dummy = 0
+
+  (** *)
+  let neg a = - a
+
+  let norm a =
+    abs a, if a < 0 then
+      Formula_intf.Negated
+    else
+      Formula_intf.Same_sign
+
+  let abs = abs
+
+  let sign i = i > 0
+
+  let apply_sign b i = if b then i else neg i
+
+  let set_sign b i = if b then abs i else neg (abs i)
+
+  let hash (a:int) = a land max_int
+  let equal (a:int) b = a=b
+  let compare (a:int) b = Pervasives.compare a b
+
+  let make i = _make (2 * i)
+
+  let fresh () =
+    incr max_fresh;
+    _make (2 * !max_fresh + 1)
+
+  (*
+  let iter: (t -> unit) -> unit = fun f ->
+    for j = 1 to !max_index do
+      f j
+    done
+  *)
+
+  let print fmt a =
+    Format.fprintf fmt "%s%s%d"
+      (if a < 0 then "~" else "")
+      (if a mod 2 = 0 then "v" else "f")
+      ((abs a) / 2)
+
+end
 
 module Make(Dummy : sig end) =
   Solver.Make(Expr)(Solver.DummyTheory(Expr))(struct end)

src/sat/sat.mli

@@ -9,9 +9,26 @@ Copyright 2016 Guillaume Bury
     atomic propositions.
 *)
 
-module Expr = Expr_sat
+module Expr : sig
+  (** SAT Formulas
+
+      This modules implements formuals adequate for use in a pure SAT Solver.
+      Atomic formuals are represented using integers, that should allow
+      near optimal efficiency (both in terms of space and time).
+  *)
+
+  include Formula_intf.S
+  (** This modules implements the requirements for implementing an SAT Solver. *)
+
+  val make : int -> t
+  (** Make a proposition from an integer. *)
+
+  val fresh : unit -> t
+  (** Make a fresh atom *)
+
+end
 (** The module defining formulas *)
 
-module Make(Dummy : sig end) : Solver.S with type St.formula = Expr_sat.t
+module Make(Dummy : sig end) : Solver.S with type St.formula = Expr.t
 (** A functor that can generate as many solvers as needed. *)
 

src/solver/solver.mli

@@ -17,7 +17,8 @@ module type S = Solver_intf.S
 module DummyTheory(F : Formula_intf.S) :
   Theory_intf.S with type formula = F.t
                  and type proof = F.proof
-(** Simple case where the proof type is [unit] and the theory is empty *)
+(** Simple case where the proof type is the one given in the formula interface
+    and the theory is empty *)
 
 module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t

tests/test_api.ml

@@ -6,7 +6,7 @@ Copyright 2014 Simon Cruanes
 
 (* Tests that require the API *)
 
-module F = Expr_sat
+module F = Sat.Expr
 module T = Tseitin.Make(F)
 
 let (|>) x f = f x