From 4159a34c20f5e00b6a5cc61f04ae9496aad12d4c Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 2 Dec 2016 15:49:49 +0100 Subject: [PATCH] Removed module alias for SAT expressions --- src/doc.txt | 1 - src/msat.mlpack | 1 - src/msat.odocl | 1 - src/sat/expr_sat.ml | 64 ------------------------------------- src/sat/expr_sat.mli | 22 ------------- src/sat/sat.ml | 74 ++++++++++++++++++++++++++++++++++++++++++- src/sat/sat.mli | 21 ++++++++++-- src/solver/solver.mli | 3 +- tests/test_api.ml | 2 +- 9 files changed, 95 insertions(+), 94 deletions(-) delete mode 100644 src/sat/expr_sat.ml delete mode 100644 src/sat/expr_sat.mli diff --git a/src/doc.txt b/src/doc.txt index e5fc40d6..f3f0f2a2 100644 --- a/src/doc.txt +++ b/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: diff --git a/src/msat.mlpack b/src/msat.mlpack index 6053e25d..15089cbd 100644 --- a/src/msat.mlpack +++ b/src/msat.mlpack @@ -29,5 +29,4 @@ Tseitin # Pure Sat solver Sat -Expr_sat diff --git a/src/msat.odocl b/src/msat.odocl index c9f83597..60c485dc 100644 --- a/src/msat.odocl +++ b/src/msat.odocl @@ -28,7 +28,6 @@ backend/Backend_intf # SAT solver frontend sat/Sat -sat/Expr_sat #sat/Type_sat # SMT solver frontend diff --git a/src/sat/expr_sat.ml b/src/sat/expr_sat.ml deleted file mode 100644 index 23c0498d..00000000 --- a/src/sat/expr_sat.ml +++ /dev/null @@ -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) - diff --git a/src/sat/expr_sat.mli b/src/sat/expr_sat.mli deleted file mode 100644 index fad5caca..00000000 --- a/src/sat/expr_sat.mli +++ /dev/null @@ -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 *) - diff --git a/src/sat/sat.ml b/src/sat/sat.ml index 9ea4d621..83de3bc9 100644 --- a/src/sat/sat.ml +++ b/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) diff --git a/src/sat/sat.mli b/src/sat/sat.mli index 2efafcdd..961e45cc 100644 --- a/src/sat/sat.mli +++ b/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. *) diff --git a/src/solver/solver.mli b/src/solver/solver.mli index 1fbb30b0..0b1ae4df 100644 --- a/src/solver/solver.mli +++ b/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 diff --git a/tests/test_api.ml b/tests/test_api.ml index 02483d34..e575758e 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 = Expr_sat +module F = Sat.Expr module T = Tseitin.Make(F) let (|>) x f = f x