From 1037c0663679adc5d5a7b505cd2cccd8f964195a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 28 Dec 2017 19:12:41 +0100 Subject: [PATCH] use generative functors, remove a layer of nesting for SMT libs --- src/core/BitField.ml | 2 +- src/core/BitField.mli | 2 +- src/core/External.ml | 3 +- src/core/External.mli | 2 +- src/core/Solver_types.ml | 4 +- src/core/Solver_types.mli | 4 +- src/core/Solver_types_intf.ml | 2 +- src/main/main.ml | 10 +-- src/mcsat/{mcsat.ml => Msat_mcsat.ml} | 8 +-- src/{smt/smt.mli => mcsat/Msat_mcsat.mli} | 2 +- src/mcsat/plugin_mcsat.ml | 2 +- src/sat/Expr_sat.ml | 70 +++++++++++++++++++ src/sat/Expr_sat.mli | 31 +++++++++ src/sat/Msat_sat.ml | 11 +++ src/sat/Msat_sat.mli | 17 +++++ src/sat/sat.ml | 82 ----------------------- src/sat/sat.mli | 47 ------------- src/sat/type_sat.ml | 4 +- src/sat/type_sat.mli | 2 +- src/smt/{smt.ml => Msat_smt.ml} | 7 +- src/{mcsat/mcsat.mli => smt/Msat_smt.mli} | 5 +- src/solver/mcsolver.ml | 4 +- src/solver/mcsolver.mli | 2 +- src/solver/solver.ml | 4 +- src/solver/solver.mli | 2 +- tests/test_api.ml | 5 +- 26 files changed, 170 insertions(+), 164 deletions(-) rename src/mcsat/{mcsat.ml => Msat_mcsat.ml} (56%) rename src/{smt/smt.mli => mcsat/Msat_mcsat.mli} (60%) create mode 100644 src/sat/Expr_sat.ml create mode 100644 src/sat/Expr_sat.mli create mode 100644 src/sat/Msat_sat.ml create mode 100644 src/sat/Msat_sat.mli delete mode 100644 src/sat/sat.ml delete mode 100644 src/sat/sat.mli rename src/smt/{smt.ml => Msat_smt.ml} (63%) rename src/{mcsat/mcsat.mli => smt/Msat_smt.mli} (52%) diff --git a/src/core/BitField.ml b/src/core/BitField.ml index bbb1f632..697320a8 100644 --- a/src/core/BitField.ml +++ b/src/core/BitField.ml @@ -107,7 +107,7 @@ let get_then_incr n = incr n; x -module Make(X : sig end) : S = struct +module Make() : S = struct type t = int let empty = 0 diff --git a/src/core/BitField.mli b/src/core/BitField.mli index 6821855e..ac92ffd8 100644 --- a/src/core/BitField.mli +++ b/src/core/BitField.mli @@ -62,7 +62,7 @@ module type S = sig end (** Create a new bitfield type *) -module Make(X : sig end) : S +module Make() : S (**/**) val all_bits_ : int -> int -> int diff --git a/src/core/External.ml b/src/core/External.ml index e14e03a7..5cc0994b 100644 --- a/src/core/External.ml +++ b/src/core/External.ml @@ -42,7 +42,8 @@ module Make (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) - (Dummy : sig end) = struct + () += struct module St = St diff --git a/src/core/External.mli b/src/core/External.mli index 7a2c9ed8..38c2ca9e 100644 --- a/src/core/External.mli +++ b/src/core/External.mli @@ -18,7 +18,7 @@ module Make (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) - (Dummy : sig end) : + () : S with module St = St (** Functor to make a safe external interface. *) diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml index 7d39f029..29245d33 100644 --- a/src/core/Solver_types.ml +++ b/src/core/Solver_types.ml @@ -27,7 +27,7 @@ let () = Var_fields.freeze() (* Solver types for McSat Solving *) (* ************************************************************************ *) -module McMake (E : Expr_intf.S)(Dummy : sig end) = struct +module McMake (E : Expr_intf.S)() = struct (* Flag for Mcsat v.s Pure Sat *) let mcsat = true @@ -375,7 +375,7 @@ end (* Solver types for pure SAT Solving *) (* ************************************************************************ *) -module SatMake (E : Formula_intf.S)(Dummy : sig end) = struct +module SatMake (E : Formula_intf.S)() = struct include McMake(struct include E module Term = E diff --git a/src/core/Solver_types.mli b/src/core/Solver_types.mli index 1892d53c..62f1baaa 100644 --- a/src/core/Solver_types.mli +++ b/src/core/Solver_types.mli @@ -30,11 +30,11 @@ module type S = Solver_types_intf.S module Var_fields = Solver_types_intf.Var_fields -module McMake (E : Expr_intf.S)(Dummy : sig end): +module McMake (E : Expr_intf.S)(): S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof (** Functor to instantiate the types of clauses for a solver. *) -module SatMake (E : Formula_intf.S)(Dummy : sig end): +module SatMake (E : Formula_intf.S)(): S with type term = E.t and type formula = E.t and type proof = E.proof (** Functor to instantiate the types of clauses for a solver. *) diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml index ee97b4fb..6e69c570 100644 --- a/src/core/Solver_types_intf.ml +++ b/src/core/Solver_types_intf.ml @@ -22,7 +22,7 @@ Copyright 2016 Simon Cruanes used in the core solver. *) -module Var_fields = BitField.Make(struct end) +module Var_fields = BitField.Make() module type S = sig (** The signatures of clauses used in the Solver. *) diff --git a/src/main/main.ml b/src/main/main.ml index 4d593cad..9ca05d85 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -105,9 +105,9 @@ module Make Dolmen.Statement.print s end -module Sat = Make(Msat_sat.Sat.Make(struct end))(Msat_sat.Type_sat) -module Smt = Make(Msat_smt.Smt.Make(struct end))(Msat_smt.Type_smt) -module Mcsat = Make(Msat_mcsat.Mcsat.Make(struct end))(Msat_smt.Type_smt) +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) let solver = ref (module Sat : S) let solver_list = [ @@ -226,8 +226,8 @@ let () = | Incorrect_model -> Format.printf "Internal error : incorrect *sat* model@."; exit 4 - | Msat_sat.Type_sat.Typing_error (msg, t) - | Msat_smt.Type_smt.Typing_error (msg, t) -> + | Msat_sat.Type.Typing_error (msg, t) + | Msat_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/mcsat.ml b/src/mcsat/Msat_mcsat.ml similarity index 56% rename from src/mcsat/mcsat.ml rename to src/mcsat/Msat_mcsat.ml index 10ad9720..b0e2e2b8 100644 --- a/src/mcsat/mcsat.ml +++ b/src/mcsat/Msat_mcsat.ml @@ -4,10 +4,10 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make(Dummy:sig end) = +module Make() = Msat_solver.Mcsolver.Make(struct type proof = unit - module Term = Msat_smt.Expr_smt.Term - module Formula = Msat_smt.Expr_smt.Atom - end)(Plugin_mcsat)(struct end) + module Term = Msat_smt.Expr.Term + module Formula = Msat_smt.Expr.Atom + end)(Plugin_mcsat)() diff --git a/src/smt/smt.mli b/src/mcsat/Msat_mcsat.mli similarity index 60% rename from src/smt/smt.mli rename to src/mcsat/Msat_mcsat.mli index 5cec2966..8055abc1 100644 --- a/src/smt/smt.mli +++ b/src/mcsat/Msat_mcsat.mli @@ -4,5 +4,5 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make(Dummy: sig end) : Msat_solver.Solver.S with type St.formula = Expr_smt.atom +module Make() : Msat_solver.Solver.S with type St.formula = Msat_smt.Expr.atom diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml index 610d7fc2..460b49fe 100644 --- a/src/mcsat/plugin_mcsat.ml +++ b/src/mcsat/plugin_mcsat.ml @@ -1,7 +1,7 @@ (* Module initialization *) -open Msat_smt +module Expr_smt = Msat_smt.Expr module E = Eclosure.Make(Expr_smt.Term) module H = Backtrack.Hashtbl(Expr_smt.Term) diff --git a/src/sat/Expr_sat.ml b/src/sat/Expr_sat.ml new file mode 100644 index 00000000..efb92778 --- /dev/null +++ b/src/sat/Expr_sat.ml @@ -0,0 +1,70 @@ + +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) diff --git a/src/sat/Expr_sat.mli b/src/sat/Expr_sat.mli new file mode 100644 index 00000000..a48603af --- /dev/null +++ b/src/sat/Expr_sat.mli @@ -0,0 +1,31 @@ + +(** The module defining formulas *) + +(** 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 *) + +val compare : t -> t -> int +(** Compare atoms *) + +val sign : t -> bool +(** Is the given atom positive ? *) + +val apply_sign : bool -> t -> t +(** [apply_sign b] is the identity if [b] is [true], and the negation + function if [b] is [false]. *) + +val set_sign : bool -> t -> t +(** Return the atom with the sign set. *) diff --git a/src/sat/Msat_sat.ml b/src/sat/Msat_sat.ml new file mode 100644 index 00000000..a706355a --- /dev/null +++ b/src/sat/Msat_sat.ml @@ -0,0 +1,11 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +*) + +module Expr = Expr_sat +module Type = Type_sat + +module Make() = + Msat_solver.Solver.Make(Expr)(Msat_solver.Solver.DummyTheory(Expr))() + diff --git a/src/sat/Msat_sat.mli b/src/sat/Msat_sat.mli new file mode 100644 index 00000000..a8c5fa5d --- /dev/null +++ b/src/sat/Msat_sat.mli @@ -0,0 +1,17 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +*) + +(** Sat solver + + This modules instanciates a pure sat solver using integers to represent + atomic propositions. +*) + +module Expr = Expr_sat +module Type = Type_sat + +module Make() : Msat_solver.Solver.S with type St.formula = Expr.t +(** A functor that can generate as many solvers as needed. *) + diff --git a/src/sat/sat.ml b/src/sat/sat.ml deleted file mode 100644 index 5da9cebd..00000000 --- a/src/sat/sat.ml +++ /dev/null @@ -1,82 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -*) - -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) = - Msat_solver.Solver.Make(Expr)(Msat_solver.Solver.DummyTheory(Expr))(struct end) - diff --git a/src/sat/sat.mli b/src/sat/sat.mli deleted file mode 100644 index 500f740f..00000000 --- a/src/sat/sat.mli +++ /dev/null @@ -1,47 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -*) - -(** Sat solver - - This modules instanciates a pure sat solver using integers to represent - atomic propositions. -*) - -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 *) - - val compare : t -> t -> int - (** Compare atoms *) - - val sign : t -> bool - (** Is the given atom positive ? *) - - val apply_sign : bool -> t -> t - (** [apply_sign b] is the identity if [b] is [true], and the negation - function if [b] is [false]. *) - - val set_sign : bool -> t -> t - (** Return the atom with the sign set. *) - -end -(** The module defining formulas *) - -module Make(Dummy : sig end) : Msat_solver.Solver.S with type St.formula = Expr.t -(** A functor that can generate as many solvers as needed. *) - diff --git a/src/sat/type_sat.ml b/src/sat/type_sat.ml index 426b16d7..b809cb4f 100644 --- a/src/sat/type_sat.ml +++ b/src/sat/type_sat.ml @@ -10,7 +10,7 @@ Copyright 2014 Simon Cruanes module Id = Dolmen.Id module Ast = Dolmen.Term module H = Hashtbl.Make(Id) -module Formula = Msat_tseitin.Make(Sat.Expr) +module Formula = Msat_tseitin.Make(Expr_sat) (* Exceptions *) (* ************************************************************************ *) @@ -26,7 +26,7 @@ let find_id id = try H.find symbols id with Not_found -> - let res = Sat.Expr.fresh () in + let res = Expr_sat.fresh () in H.add symbols id res; res diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli index 512d358b..ae32ddd2 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 := Sat.Expr.t +include Msat_solver.Type.S with type atom := Expr_sat.t diff --git a/src/smt/smt.ml b/src/smt/Msat_smt.ml similarity index 63% rename from src/smt/smt.ml rename to src/smt/Msat_smt.ml index 1321f5bd..2cae3821 100644 --- a/src/smt/smt.ml +++ b/src/smt/Msat_smt.ml @@ -4,8 +4,11 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +module Expr = Expr_smt +module Type = Type_smt + module Th = Msat_solver.Solver.DummyTheory(Expr_smt.Atom) -module Make(Dummy:sig end) = - Msat_solver.Solver.Make(Expr_smt.Atom)(Th)(struct end) +module Make() = + Msat_solver.Solver.Make(Expr_smt.Atom)(Th)() diff --git a/src/mcsat/mcsat.mli b/src/smt/Msat_smt.mli similarity index 52% rename from src/mcsat/mcsat.mli rename to src/smt/Msat_smt.mli index ddd06949..39f1231d 100644 --- a/src/mcsat/mcsat.mli +++ b/src/smt/Msat_smt.mli @@ -4,5 +4,8 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make(Dummy: sig end) : Msat_solver.Solver.S with type St.formula = Msat_smt.Expr_smt.atom +module Expr = Expr_smt +module Type = Type_smt + +module Make() : Msat_solver.Solver.S with type St.formula = Expr_smt.atom diff --git a/src/solver/mcsolver.ml b/src/solver/mcsolver.ml index a0d7f62a..4c68e07c 100644 --- a/src/solver/mcsolver.ml +++ b/src/solver/mcsolver.ml @@ -10,10 +10,10 @@ module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) - (Dummy: sig end) = + () = External.Make (Solver_types.McMake(E)(struct end)) (Th) - (struct end) + () diff --git a/src/solver/mcsolver.mli b/src/solver/mcsolver.mli index 455eb92e..383fcc8f 100644 --- a/src/solver/mcsolver.mli +++ b/src/solver/mcsolver.mli @@ -16,7 +16,7 @@ module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) - (Dummy: sig end) : + () : S with type St.term = E.Term.t and type St.formula = E.Formula.t and type St.proof = E.proof diff --git a/src/solver/solver.ml b/src/solver/solver.ml index eee3afba..8f86a1f1 100644 --- a/src/solver/solver.ml +++ b/src/solver/solver.ml @@ -76,10 +76,10 @@ end module Make (E : Formula_intf.S) (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) - (Dummy: sig end) = + () = External.Make (Solver_types.SatMake(E)(struct end)) (Plugin(E)(Th)) - (struct end) + () diff --git a/src/solver/solver.mli b/src/solver/solver.mli index e3400d36..2480e453 100644 --- a/src/solver/solver.mli +++ b/src/solver/solver.mli @@ -23,7 +23,7 @@ module DummyTheory(F : Formula_intf.S) : module Make (F : Formula_intf.S) (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) - (Dummy: sig end) : + () : S with type St.formula = F.t and type St.proof = F.proof (** Functor to create a SMT Solver parametrised by the atomic diff --git a/tests/test_api.ml b/tests/test_api.ml index 8984c12d..fc41286e 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -7,9 +7,8 @@ Copyright 2014 Simon Cruanes (* Tests that require the API *) open Msat -open Msat_sat -module F = Sat.Expr +module F = Msat_sat.Expr module T = Msat_tseitin.Make(F) let (|>) x f = f x @@ -47,7 +46,7 @@ end let mk_solver (): (module BASIC_SOLVER) = let module S = struct - include Sat.Make(struct end) + include Msat_sat.Make(struct end) let solve ?assumptions ()= match solve ?assumptions() with | Sat _ -> R_sat