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

Some mli doc updates

Browse source
This commit is contained in:
Guillaume Bury 2016-12-02 15:57:56 +01:00
parent 4159a34c20
commit 32128749b2
3 changed files with 15 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/core/formula_intf.ml
View file

@ -39,13 +39,15 @@ module type S = sig
(** Formula constant. A valid formula should never be physically equal to [dummy] *) (** Formula constant. A valid formula should never be physically equal to [dummy] *)
val neg : t -> t val neg : t -> t
(** Formula negation *) (** Formula negation. Should be an involution, i.e. [equal a (neg neg a)] should
always hold. *)
val norm : t -> t * negated val norm : t -> t * negated
(** Returns a 'normalized' form of the formula, possibly negated (** Returns a 'normalized' form of the formula, possibly negated
(in which case return [Negated]). (in which case return [Negated]). This function is used to recognize
[norm] must be so that [a] and [neg a] normalise to the same formula, the link between a formula [a] and its negation [neg a], so the goal is
but one returns [Same_sign] and one returns [Negated] *) that [a] and [neg a] normalise to the same formula,
but one returns [Same_sign] and the other one returns [Negated] *)
end end

10
src/doc.txt
View file

@ -2,14 +2,18 @@
{2 License} {2 License}
This code is free, under the Apache 2.0 license. This code is free, under the {{:https://github.com/Gbury/mSAT/blob/master/LICENSE}Apache 2.0 license}.
{2 Contents} {2 Contents}
mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely, mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely,
what mSAT provides are functors to easily create such solvers. Indeed, the core what mSAT provides are functors to easily create such solvers. Indeed, the core
of a sat solver does not need much information about neither the exact representation of a sat solver does not need much information about either the exact representation
of terms nor the inner workings of a theory. of terms or the inner workings of a theory.
Most modules in mSAT actually define functors. These functors usually take one
or two arguments, usually an implementation of Terms and formulas used, and an implementation
of the theory used during solving.
{4 Solver creation} {4 Solver creation}

4
src/solver/solver.mli
View file

@ -17,8 +17,8 @@ module type S = Solver_intf.S
module DummyTheory(F : Formula_intf.S) : module DummyTheory(F : Formula_intf.S) :
Theory_intf.S with type formula = F.t Theory_intf.S with type formula = F.t
and type proof = F.proof and type proof = F.proof
(** Simple case where the proof type is the one given in the formula interface (** Simple case where the theory is empty and
and the theory is empty *) the proof type is the one given in the formula interface *)
module Make (F : Formula_intf.S) module Make (F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t (Th : Theory_intf.S with type formula = F.t