prepare for 0.6

CHANGELOG.md

@@ -1,3 +1,14 @@
+## 0.6
+
+- migrate from minisat-c 1.14 to minisat 2.2 (in C++); refactor it to build with C++11
+
+- add `Lit.{apply_sign,hash,equal,compare}`
+- add `ensure_lit_exists`
+- do not call `simplify` implicitly before `solve`
+- add `value_at_level_0`
+- add `unsat_core`
+- add `okay`
+
 ## 0.5
 
 - format C and OCaml code

dune-project

@@ -1 +1,2 @@
 (lang dune 2.0)
+(name minisat)

minisat.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "0.5"
+version: "0.6"
 author: "simon.cruanes.2007@m4x.org"
 maintainer: "simon.cruanes.2007@m4x.org"
 synopsis: "Bindings to the SAT solver Minisat, with the solver included."

src/minisat.mli

@@ -15,13 +15,13 @@ module Lit : sig
       integers. *)
 
   val equal : t -> t -> bool
-  (** @since NEXT_RELEASE *)
+  (** @since 0.6 *)
 
   val compare : t -> t -> int
-  (** @since NEXT_RELEASE *)
+  (** @since 0.6 *)
 
   val hash : t -> int
-  (** @since NEXT_RELEASE *)
+  (** @since 0.6 *)
 
   val make : int -> t
   (** [make n] creates the literal whose index is [n].
@@ -37,7 +37,7 @@ module Lit : sig
 
   val apply_sign : bool -> t -> t
   (** [apply_sign true lit] is [lit]; [apply_sign false lit] is [neg lit] 
-      @since NEXT_RELEASE *)
+      @since 0.6 *)
 
   val sign : t -> bool
   (** Sign: [true] if the literal is positive, [false] for a negated literal.
@@ -58,13 +58,13 @@ val create : unit -> t
 
 val okay : t -> bool
 (** [true] if the solver isn't known to be in an unsat state
-    @since NEXT_RELEASE *)
+    @since 0.6 *)
 
 exception Unsat
 
 val ensure_lit_exists : t -> Lit.t -> unit
 (** Make sure the solver decides this literal.
-    @since NEXT_RELEASE *)
+    @since 0.6 *)
 
 val add_clause_l : t -> Lit.t list -> unit
 (** Add a clause (as a list of literals) to the solver state.
@@ -114,37 +114,37 @@ val value_at_level_0 : t -> Lit.t -> value
     there, or [V_undef].
     If [lit] is not assigned at level 0, this returns [V_undef] even when the
     literal has a value in the current model.
-    @since NEXT_RELEASE *)
+    @since 0.6 *)
 
 val unsat_core : t -> Lit.t array
 (** Returns the subset of assumptions of a solver that returned "unsat"
     when called with [solve ~assumptions s].
-    @since NEXT_RELEASE
+    @since 0.6
 *)
 
 val set_verbose : t -> int -> unit
 (** Verbose mode. *)
 
 val interrupt : t -> unit
 (** Interrupt the solver, typically from another thread.
-    @since NEXT_RELEASE *)
+    @since 0.6 *)
 
 val clear_interrupt : t -> unit
 (** Clear interrupt flag so that we can use the solver again.
-    @since NEXT_RELEASE *)
+    @since 0.6 *)
 
 val n_clauses : t -> int
-(** @since NEXT_RELEASE *)
+(** @since 0.6 *)
 
 val n_vars : t -> int
-(** @since NEXT_RELEASE *)
+(** @since 0.6 *)
 
 val n_conflicts : t -> int
-(** @since NEXT_RELEASE *)
+(** @since 0.6 *)
 
 module Debug : sig
   val to_dimacs_file : t -> string -> unit
   (** [to_dimacs_file solver path] writes the solver's set of clauses into the
     file at [path].
-    @since NEXT_RELEASE *)
+    @since 0.6 *)
 end