diff --git a/CHANGELOG.md b/CHANGELOG.md index 6f96f69..9c86e74 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/dune-project b/dune-project index 929c696..6b689d5 100644 --- a/dune-project +++ b/dune-project @@ -1 +1,2 @@ (lang dune 2.0) +(name minisat) diff --git a/minisat.opam b/minisat.opam index 8175424..e0495e8 100644 --- a/minisat.opam +++ b/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." diff --git a/src/minisat.mli b/src/minisat.mli index 3241fdb..2713df3 100644 --- a/src/minisat.mli +++ b/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,12 +114,12 @@ 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 @@ -127,24 +127,24 @@ val set_verbose : t -> int -> unit 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