diff --git a/README.md b/README.md index 8be962af..025983e6 100644 --- a/README.md +++ b/README.md @@ -37,12 +37,12 @@ as shown in the following code : ```ocaml (* Module initialization *) - module F = Msat.Sat.Tseitin module Sat = Msat.Sat.Make() + module F = Msat.Tseitin.Make(Msat.Sat.Expr) (* We create here two distinct atoms *) - let a = Msat.Sat.Fsat.fresh () (* A 'new_atom' is always distinct from any other atom *) - let b = Msat.Sat.Fsat.make 1 (* Atoms can be created from integers *) + let a = Msat.Sat.Expr.fresh () (* A 'new_atom' is always distinct from any other atom *) + let b = Msat.Sat.Expr.make 1 (* Atoms can be created from integers *) (* Let's create some formulas *) let p = F.make_atom a @@ -52,12 +52,12 @@ as shown in the following code : (* We can try and check the satisfiability of the given formulas *) Sat.assume (F.make_cnf r) - let _ = Sat.solve () (* Should return Sat.Sat *) + let _ = Sat.solve () (* Should return (Sat.Sat _) *) (* The Sat solver has an incremental mutable state, so we still have * the formula 'r' in our assumptions *) Sat.assume (F.make_cnf s) - let _ = Sat.solve () (* Should return Sat.Unsat *) + let _ = Sat.solve () (* Should return (Sat.Unsat _) *) ``` ## INSTALLATION diff --git a/_tags b/_tags index 3714ec07..31793d6e 100644 --- a/_tags +++ b/_tags @@ -19,6 +19,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) +: for-pack(Msat) +: for-pack(Msat) # Testing dependencies : package(dolmen) diff --git a/src/doc.txt b/src/doc.txt index f147b970..e5fc40d6 100644 --- a/src/doc.txt +++ b/src/doc.txt @@ -32,6 +32,15 @@ Expr_intf Plugin_intf } +{4 Useful tools} + +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: {!modules: diff --git a/src/msat.mlpack b/src/msat.mlpack index eb1182bc..6053e25d 100644 --- a/src/msat.mlpack +++ b/src/msat.mlpack @@ -26,3 +26,8 @@ Dedukti # Auxiliary modules Tseitin + +# Pure Sat solver +Sat +Expr_sat + diff --git a/src/msat.odocl b/src/msat.odocl index ac01fe3f..c9f83597 100644 --- a/src/msat.odocl +++ b/src/msat.odocl @@ -27,8 +27,8 @@ backend/Dedukti backend/Backend_intf # SAT solver frontend -#sat/Sat -#sat/Expr_sat +sat/Sat +sat/Expr_sat #sat/Type_sat # SMT solver frontend diff --git a/src/sat/expr_sat.mli b/src/sat/expr_sat.mli index 7026d8e4..fad5caca 100644 --- a/src/sat/expr_sat.mli +++ b/src/sat/expr_sat.mli @@ -4,7 +4,15 @@ 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. *) diff --git a/src/sat/sat.ml b/src/sat/sat.ml index 9e0442f3..9ea4d621 100644 --- a/src/sat/sat.ml +++ b/src/sat/sat.ml @@ -1,9 +1,10 @@ (* MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes +Copyright 2016 Guillaume Bury *) -module Make(Dummy : sig end) = - Solver.Make(Expr_sat)(Solver.DummyTheory(Expr_sat))(struct end) +module Expr = Expr_sat + +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 dc20113a..2efafcdd 100644 --- a/src/sat/sat.mli +++ b/src/sat/sat.mli @@ -1,9 +1,17 @@ (* MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes +Copyright 2016 Guillaume Bury *) +(** Sat solver + + This modules instanciates a pure sat solver using integers to represent + atomic propositions. +*) + +module Expr = Expr_sat +(** The module defining formulas *) + module Make(Dummy : sig end) : Solver.S with type St.formula = Expr_sat.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 6689f7f6..6c58d98b 100644 --- a/src/sat/type_sat.ml +++ b/src/sat/type_sat.ml @@ -1,3 +1,8 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) (* Log&Module Init *) (* ************************************************************************ *) @@ -5,7 +10,7 @@ module Id = Dolmen.Id module Ast = Dolmen.Term module H = Hashtbl.Make(Id) -module Formula = Tseitin.Make(Expr_sat) +module Formula = Tseitin.Make(Sat.Expr) (* Exceptions *) (* ************************************************************************ *) @@ -21,7 +26,7 @@ let find_id id = try H.find symbols id with Not_found -> - let res = Expr_sat.fresh () in + let res = Sat.Expr.fresh () in H.add symbols id res; res diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli index 6d295a52..56fced24 100644 --- a/src/sat/type_sat.mli +++ b/src/sat/type_sat.mli @@ -1,7 +1,12 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) (** Typechecking of terms from Dolmen.Term.t 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 Type.S with type atom := Expr_sat.t +include Type.S with type atom := Sat.Expr.t