simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

[doc] Better description for Plugin_intf.reason

Browse source
This commit is contained in:
Guillaume Bury 2017-01-24 10:54:01 +01:00
parent 1f5b5fc422
commit 204e184b86
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/core/internal.mli
View file

@ -45,6 +45,8 @@ module Make
@param assumptions list of additional local assumptions to make,
removed after the callback returns a value *)
(** {2 Propositional models} *)
val eval : St.formula -> bool
(** Returns the valuation of a formula in the current state
of the sat solver.
@ -57,6 +59,12 @@ module Make
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
val model : unit -> (St.term * St.term) list
(** Returns the model found if the formula is satisfiable. *)
val check : unit -> bool
(** Check the satisfiability of the current model. Only has meaning
if the solver finished proof search and has returned [Sat]. *)
(** {2 Proofs and Models} *)
@ -66,17 +74,10 @@ module Make
(** Returns the unsat clause found at the toplevel, if it exists (i.e if
[solve] has raised [Unsat]) *)
val model : unit -> (St.term * St.term) list
(** Returns the model found if the formula is satisfiable. *)
val full_slice : unit -> (St.term, St.formula, St.proof) Plugin_intf.slice
(** View the current state of the trail as a slice. Mainly useful when the
solver has reached a SAT conclusion. *)
val check : unit -> bool
(** Check the satisfiability of the current model. Only has meaning
if the solver finished proof search and has returned [Sat]. *)
(** {2 Internal data}
These functions expose some internal data stored by the solver, as such
great care should be taken to ensure not to mess with the values returned. *)