more docs

src/base/Base_types.ml

@@ -1,3 +1,5 @@
+(** Basic type definitions for Sidekick_base *)
+
 module Vec = Msat.Vec
 module Log = Msat.Log
 module Fmt = CCFormat
@@ -16,14 +18,20 @@ type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
   | LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
   | LRA_other of 'a
 
-(* main term cell. *)
+(** Term.
+
+    A term, with its own view, type, and a unique identifier.
+    Do not create directly, see {!Term}. *)
 type term = {
   mutable term_id: int; (* unique ID *)
   mutable term_ty: ty;
   term_view : term term_view;
 }
 
-(* term shallow structure *)
+(** Shallow structure of a term.
+
+    A term is a DAG (direct acyclic graph) of nodes, each of which has a
+    term view. *)
 and 'a term_view =
   | Bool of bool
   | App_fun of fun_ * 'a IArray.t (* full, first-order application *)
@@ -36,6 +44,7 @@ and fun_ = {
   fun_id: ID.t;
   fun_view: fun_view;
 }
+(** type of function symbols *)
 
 and fun_view =
   | Fun_undef of fun_ty (* simple undefined constant *)
@@ -258,6 +267,7 @@ let pp_term_top ~ids out t =
 let pp_term = pp_term_top ~ids:false
 let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term
 
+(** Types *)
 module Ty : sig
   type t = ty
   type state = unit
@@ -436,6 +446,7 @@ end = struct
   end
 end
 
+(** Function symbols *)
 module Fun : sig
   type view = fun_view =
     | Fun_undef of fun_ty (* simple undefined constant *)
@@ -758,6 +769,7 @@ end = struct
     end)
 end
 
+(** Term creation and manipulation *)
 module Term : sig
   type t = term = {
     mutable term_id : int;
@@ -999,6 +1011,7 @@ end = struct
     | LRA l -> lra tst (Sidekick_arith_lra.map_view f l)
 end
 
+(** Values (used in models) *)
 module Value : sig
   type t = value =
     | V_bool of bool
@@ -1070,6 +1083,7 @@ end = struct
     mk_elt (ID.makef "v_%d" t.term_id) t.term_ty
 end
 
+(** Datatypes *)
 module Data = struct
   type t = data = {
     data_id: ID.t;
@@ -1080,6 +1094,10 @@ module Data = struct
   let pp out d = ID.pp out d.data_id
 end
 
+(** Datatype selectors.
+
+    A selector is a kind of function that allows to obtain an argument
+    of a given constructor. *)
 module Select = struct
   type t = select = {
     select_id: ID.t;
@@ -1091,6 +1109,10 @@ module Select = struct
   let ty sel = Lazy.force sel.select_ty
 end
 
+(** Datatype constructors.
+
+    A datatype has one or more constructors, each of which is a special
+    kind of function symbol. Constructors are injective and pairwise distinct. *)
 module Cstor = struct
   type t = cstor = {
     cstor_id: ID.t;
@@ -1107,6 +1129,13 @@ module Cstor = struct
   let pp out c = ID.pp out c.cstor_id
 end
 
+(* TODO: check-sat-assuming, get-unsat-assumptions, push, pop *)
+
+(** Statements.
+
+    A statement is an instruction for the SMT solver to do something,
+    like asserting that a formula is true, declaring a new constant,
+    or checking satisfiabilty of the current set of assertions. *)
 module Statement = struct
   type t = statement =
     | Stmt_set_logic of string
@@ -1121,6 +1150,7 @@ module Statement = struct
     | Stmt_check_sat of (bool * term) list
     | Stmt_exit
 
+  (** Pretty print a statement *)
   let pp out = function
     | Stmt_set_logic s -> Fmt.fprintf out "(set-logic %s)" s
     | Stmt_set_option l -> Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l

src/base/ID.ml

@@ -38,8 +38,3 @@ end
 module Map = CCMap.Make(AsKey)
 module Set = CCSet.Make(AsKey)
 module Tbl = CCHashtbl.Make(AsKey)
-
-module B = struct
-  let int = make "int"
-  let rat = make "rat"
-end

src/base/ID.mli

@@ -1,18 +1,42 @@
 
 (* This file is free software. See file "license" for more details. *)
 
-(** {1 Unique Identifiers} *)
+(** Unique Identifiers *)
+
+(**
+    We use generative identifiers everywhere in [Sidekick_base]. Unlike
+    strings, there are no risk of collision: during parsing, a new
+    declaration or definition should create a fresh [ID.t] and associate
+    it with the string name, and later references should look into some hashtable
+    or map to get the ID corresponding to a string.
+
+    This allows us to handle definition shadowing or binder shadowing easily.
+*)
 
 type t
+(** The opaque type of unique identifiers *)
 
 val make : string -> t
+(** [make s] creates a new identifier with name [s]
+    and some internal information. It is different than any other identifier
+    created before or after, even with the same name. *)
+
 val makef : ('a, Format.formatter, unit, t) format4 -> 'a
+(** [makef "foo %d bar %b" 42 true] is like
+    [make (Format.asprintf "foo %d bar %b" 42 true)]. *)
+
 val copy : t -> t
+(** Fresh copy of the identifier, distinct from it, but with the
+    same name. *)
 
 val id : t -> int
+(** Unique integer counter for this identifier. *)
 
 val to_string : t -> string
+(** Print identifier. *)
+
 val to_string_full : t -> string
+(** Printer name and unique counter for this ID. *)
 
 include Intf.EQ with type t := t
 include Intf.ORD with type t := t
@@ -25,11 +49,3 @@ module Map : CCMap.S with type key = t
 module Set : CCSet.S with type elt = t
 module Tbl : CCHashtbl.S with type key = t
 
-
-module B : sig
-  val rat : t
-  val int : t
-
-end
-
-

src/base/Model.ml

@@ -1,7 +1,5 @@
 (* This file is free software. See file "license" for more details. *)
 
-(** {1 Model} *)
-
 open Base_types
 
 module Val_map = struct

src/base/Model.mli

@@ -1,6 +1,14 @@
 (* This file is free software. See file "license" for more details. *)
 
-(** {1 Model} *)
+(** Models
+
+    A model is a solution to the satisfiability question, created by the
+    SMT solver when it proves the formula to be {b satisfiable}.
+
+    A model gives a value to each term of the original formula(s), in
+    such a way that  the formula(s) is true when the term is replaced by its
+    value.
+*)
 
 open Base_types
 
@@ -14,6 +22,14 @@ module Val_map : sig
   val add : key -> 'a -> 'a t -> 'a t
 end
 
+(** Model for function symbols.
+
+    Function models are a finite map from argument tuples to values,
+    accompanied with a default value that every other argument tuples
+    map to. In other words, it's of the form:
+
+    [lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault]
+*)
 module Fun_interpretation : sig
   type t = {
     cases: Value.t Val_map.t;
@@ -29,11 +45,13 @@ module Fun_interpretation : sig
     t
 end
 
+(** Model *)
 type t = {
   values: Value.t Term.Map.t;
   funs: Fun_interpretation.t Fun.Map.t;
 }
 
+(** Empty model *)
 val empty : t
 
 val add : Term.t -> Value.t -> t -> t
@@ -46,4 +64,6 @@ val merge : t -> t -> t
 
 val pp : t CCFormat.printer
 
+(** [eval m t] tries to evaluate term [t] in the model.
+    If it succeeds, the value is returned, otherwise [None] is. *)
 val eval : t -> Term.t -> Value.t option

src/base/Proof.ml

@@ -1,3 +1,4 @@
+
 open Base_types
 
 module T = Term

src/base/Proof.mli

@@ -1,3 +1,14 @@
+(** Proofs of unsatisfiability
+
+    Proofs are used in sidekick when the problem is found {b unsatisfiable}.
+    A proof collects inferences made by the solver into a list of steps,
+    each with its own kind of justification (e.g. "by congruence"),
+    and outputs it in some kind of format.
+
+    Currently we target {{: https://c-cube.github.io/quip-book/ } Quip}
+    as an experimental proof backend.
+*)
+
 open Base_types
 
 include Sidekick_core.PROOF

src/base/Sidekick_base.ml

@@ -6,7 +6,8 @@
     It provides a representation of terms, boolean formulas,
     linear arithmetic expressions, datatypes for the functors in Sidekick.
 
-    In addition, it has a notion of {!Statement}. Statements are instructions
+    In addition, it has a notion of {{!Base_types.Statement} Statement}.
+    Statements are instructions
     for the SMT solver to do something, such as: define a new constant,
     declare a new constant, assert a formula as being true,
     set an option, check satisfiability of the set of statements added so far,

src/core/Sidekick_core.ml

@@ -145,10 +145,15 @@ module type TERM = sig
   end
 end
 
+(** Proofs of unsatisfiability *)
 module type PROOF = sig
+  type t
+  (** The abstract representation of a proof. A proof always proves
+      a clause to be {b valid} (true in every possible interpretation
+      of the problem's assertions, and the theories) *)
+
   type term
   type ty
-  type t
 
   type hres_step
   (** hyper-resolution steps: resolution, unit resolution;
@@ -179,6 +184,7 @@ module type PROOF = sig
   val lit_sign : lit -> bool
 
   type composite_step
+
   val stepc : name:string -> lit list -> t -> composite_step
   val deft : term -> term -> composite_step (** define a (new) atomic term *)