simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 03:35:38 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix typo of Plugin_intf.reason

Browse source
This commit is contained in:
Guillaume Bury 2017-01-17 15:59:29 +01:00
parent ea2c905644
commit d538e19411
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/core/plugin_intf.ml
View file

@ -54,12 +54,11 @@ type ('term, 'formula) assumption =
(** Asusmptions made by the core SAT solver. *)
type ('term, 'formula, 'proof) reason =
| Eval of 'term list
| Consequence of 'formula list * 'proof
(** The type of reasons for propagations of a formula [f].
[Semantic lvl] means that [f] is true because of the assignments whose level is [<= lvl].
[Consequence (l, p)] means that the formulas in [l] imply [f]. The proof should be a proof
of the clause "[l] implies [f]". *)
| Eval of 'term list (** The formula can be evalutaed using the terms in the list *)
| Consequence of 'formula list * 'proof (** [Consequence (l, p)] means that the formulas in [l] imply
the propagated formula [f]. The proof should be a proof of
the clause "[l] implies [f]". *)
(** The type of reasons for propagations of a formula [f]. *)
type ('term, 'formula, 'proof) slice = {
start : int; (** Start of the slice *)