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

Manual re-indent

Browse source
This commit is contained in:
Guillaume Bury 2017-08-25 19:15:12 +02:00
parent 679d928b88
commit 7749f7aaac
2 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/core/plugin_intf.ml
View file

@ -27,8 +27,7 @@ type 'term eval_res =
| Unknown (** The given formula does not have an evaluation *) | Unknown (** The given formula does not have an evaluation *)
| Valued of bool * ('term list) (** The given formula can be evaluated to the given bool. | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool.
The list of terms to give is the list of terms that The list of terms to give is the list of terms that
were effectively used for the evaluation. were effectively used for the evaluation. *)
*)
(** The type of evaluation results for a given formula. (** The type of evaluation results for a given formula.
For instance, let's suppose we want to evaluate the formula [x * y = 0], the For instance, let's suppose we want to evaluate the formula [x * y = 0], the
following result are correct: following result are correct:
@ -67,8 +66,8 @@ type ('term, 'formula, 'proof) slice = {
Should only be called on integers [i] s.t. Should only be called on integers [i] s.t.
[start <= i < start + length] *) [start <= i < start + length] *)
push : 'formula list -> 'proof -> unit; (** Add a clause to the solver. *) push : 'formula list -> 'proof -> unit; (** Add a clause to the solver. *)
propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; propagate : 'formula ->
(** Propagate a formula, i.e. the theory can ('term, 'formula, 'proof) reason -> unit; (** Propagate a formula, i.e. the theory can
evaluate the formula to be true (see the evaluate the formula to be true (see the
definition of {!type:eval_res} *) definition of {!type:eval_res} *)
} }

4
src/core/solver_types_intf.ml
View file

@ -119,7 +119,7 @@ module type S = sig
(** {2 Decisions and propagations} *) (** {2 Decisions and propagations} *)
type t = type t =
| Lit of lit | Lit of lit
| Atom of atom | Atom of atom (**)
(** Either a lit of an atom *) (** Either a lit of an atom *)
val of_lit : lit -> t val of_lit : lit -> t
@ -130,7 +130,7 @@ module type S = sig
type elt = type elt =
| E_lit of lit | E_lit of lit
| E_var of var | E_var of var (**)
(** Either a lit of a var *) (** Either a lit of a var *)
val nb_elt : unit -> int val nb_elt : unit -> int