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

Added full_slice function in Internal

Browse source
This commit is contained in:
Guillaume Bury 2016-12-07 13:21:12 +01:00
parent 32128749b2
commit 58e6b924a8
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/core/internal.mli
View file

@ -69,6 +69,10 @@ module Make
val model : unit -> (St.term * St.term) list val model : unit -> (St.term * St.term) list
(** Returns the model found if the formula is satisfiable. *) (** 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 val check : unit -> bool
(** Check the satisfiability of the current model. Only has meaning (** Check the satisfiability of the current model. Only has meaning
if the solver finished proof search and has returned [Sat]. *) if the solver finished proof search and has returned [Sat]. *)