more doc

src/msat-solver/Sidekick_msat_solver.ml

@@ -1,7 +1,15 @@
 (** {1 Implementation of a Solver using Msat} *)
 
-module Log = Msat.Log
+(** {{: https://github.com/Gbury/mSAT/} Msat} is a modular SAT solver in
+    pure OCaml.
 
+    This builds a {!Sidekick_core.SOLVER} on top of it. *)
+
+module Log = Msat.Log
+(** A logging module *)
+
+(** Argument to pass to the functor {!Make} in order to create a
+    new Msat-based SMT solver. *)
 module type ARG = sig
   open Sidekick_core
   module T : TERM
@@ -16,6 +24,7 @@ end
 
 module type S = Sidekick_core.SOLVER
 
+(** Main functor to get a solver. *)
 module Make(A : ARG)
   : S
     with module T = A.T

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -1,5 +1,9 @@
-(** {2 Signatures for booleans} *)
+(** Theory of boolean formulas.
 
+    This handles formulas containing "and", "or", "=>", "if-then-else", etc.
+    *)
+
+(** Boolean-oriented view of terms *)
 type ('a, 'args) bool_view =
   | B_bool of bool
   | B_not of 'a
@@ -14,16 +18,17 @@ type ('a, 'args) bool_view =
   | B_opaque_bool of 'a (* do not enter *)
   | B_atom of 'a
 
+(** Argument to the theory *)
 module type ARG = sig
   module S : Sidekick_core.SOLVER
 
   type term = S.T.Term.t
 
   val view_as_bool : term -> (term, term Iter.t) bool_view
-  (** Project the term into the boolean view *)
+  (** Project the term into the boolean view. *)
 
   val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term
-  (** Make a term from the given boolean view *)
+  (** Make a term from the given boolean view. *)
 
   val check_congruence_classes : bool
   (** Configuration: add final-check handler to verify if new boolean formulas
@@ -31,16 +36,23 @@ module type ARG = sig
       Only enable if some theories are susceptible to
       create boolean formulas during the proof search. *)
 
+  (** Fresh symbol generator.
+
+      The theory needs to be able to create new terms with fresh names,
+      to be used as placeholders for complex formulas during Tseitin
+      encoding. *)
   module Gensym : sig
     type t
 
     val create : S.T.Term.state -> t
+    (** New (stateful) generator instance. *)
 
     val fresh_term : t -> pre:string -> S.T.Ty.t -> term
     (** Make a fresh term of the given type *)
   end
 end
 
+(** Signature *)
 module type S = sig
   module A : ARG
 
@@ -52,9 +64,16 @@ module type S = sig
   (** Simplify given term *)
 
   val cnf : state -> A.S.Solver_internal.preprocess_hook
-  (** add clauses for the booleans within the term. *)
+  (** preprocesses formulas by giving them names and
+      adding clauses to equate the name with the boolean formula. *)
 
   val theory : A.S.theory
+  (** A theory that can be added to the solver {!A.S}.
+
+      This theory does most of its work during preprocessing,
+      turning boolean formulas into SAT clauses via
+      the {{: https://en.wikipedia.org/wiki/Tseytin_transformation}
+          Tseitin encoding} . *)
 end
 
 module Make(A : ARG) : S with module A = A = struct

src/th-data/Sidekick_th_data.ml

@@ -1,12 +1,6 @@
 
-(** {1 Theory for datatypes} *)
+(** Theory for datatypes. *)
 
-(** {2 Views} *)
-
-(** Datatype-oriented view of terms.
-    ['c] is the representation of constructors
-    ['t] is the representation of terms
-*)
 type ('c,'t) data_view =
   | T_cstor of 'c * 't IArray.t
   | T_select of 'c * int * 't

src/th-data/Sidekick_th_data.mli

@@ -1,3 +1,4 @@
+(** Theory for datatypes. *)
 
 (** Datatype-oriented view of terms.
     ['c] is the representation of constructors
@@ -20,14 +21,25 @@ type ('c, 'ty) data_ty_view =
     }
   | Ty_other
 
+(** Argument to the functor *)
 module type ARG = sig
   module S : Sidekick_core.SOLVER
 
+(** Constructor symbols.
+
+    A constructor is an injective symbol, part of a datatype (or "sum type").
+    For example, in [type option a = Some a | None],
+    the constructors are [Some] and [None]. *)
   module Cstor : sig
     type t
+    (** Constructor *)
+
     val ty_args : t -> S.T.Ty.t Iter.t
+    (** Type arguments, for a polymorphic constructor *)
+
     val pp : t Fmt.printer
     val equal : t -> t -> bool
+    (** Comparison *)
   end
 
   val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view
@@ -49,15 +61,19 @@ module type ARG = sig
   (** Make a term equality *)
 
   val ty_is_finite : S.T.Ty.t -> bool
-  (** Is the given type known to be finite? *)
+  (** Is the given type known to be finite? For example a finite datatype
+      (an "enum" in C parlance), or [Bool], or [Array Bool Bool]. *)
 
   val ty_set_is_finite : S.T.Ty.t -> bool -> unit
   (** Modify the "finite" field (see {!ty_is_finite}) *)
+
+  (* TODO: should we store this ourself? would be simpler… *)
 end
 
 module type S = sig
   module A : ARG
   val theory : A.S.theory
+  (** A theory that can be added to {!A.S} to perform datatype reasoning. *)
 end
 
 module Make(A : ARG) : S with module A = A