more cleanup, add doc

README.md

@@ -42,15 +42,16 @@ Sidekick comes in several components (as in, opam packages):
 
 - `sidekick` is the core library, with core type definitions (see `src/core/`),
   an implementation of CDCL(T) based on [mSat](https://github.com/Gbury/mSAT/),
-  a congruence closure, and the theories of boolean formulas and datatypes.
+  a congruence closure, and the theories of boolean formulas, LRA (linear rational
-- `sidekick-arith` is a library with an additional dependency
+  arithmetic, using a simplex algorithm), and datatypes.
-  on [zarith](https://github.com/ocaml/Zarith)
+- `sidekick-base` is a library with concrete implementations for terms,
-  (a GMP wrapper for arbitrary precision numbers).
+  arithmetic functions, and proofs.
-  It currently implements LRA (linear rational arithmetic)
+  It comes with an additional dependency on
-  using a Simplex algorithm.
+  [zarith](https://github.com/ocaml/Zarith) to represent numbers (zarith is a
+  GMP wrapper for arbitrary precision numbers).
 - `sidekick-bin` is an executable that is able to parse problems in
   the SMT-LIB-2.6 format, in the `QF_UFLRA` fragment, and solves them using
-  the libraries previously listed.
+  `sidekick` instantiated with `sidekick-base`.
   It is mostly useful as a test tool for the libraries and as a starting point
   for writing custom solvers.
 

src/base/Base_types.ml

@@ -816,7 +816,7 @@ module Term : sig
 
   val pp : t Fmt.printer
 
-  (** {6 Views} *)
+  (** {3 Views} *)
 
   val is_true : t -> bool
   val is_false : t -> bool
@@ -828,7 +828,7 @@ module Term : sig
   val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
   val as_bool : t -> bool option
 
-  (** {6 Containers} *)
+  (** {3 Containers} *)
 
   module Tbl : CCHashtbl.S with type key = t
   module Map : CCMap.S with type key = t

src/base/Sidekick_base.ml

@@ -1,3 +1,21 @@
+(** {1 Sidekick base}
+
+    This library is a starting point for writing concrete implementations
+    of SMT solvers with Sidekick.
+
+    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
+    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,
+    etc. Logic formats such as SMT-LIB 2.6 are in fact based on a similar
+    notion of statements, and a [.smt2] files contains a list of statements.
+
+    *)
+
+
 module Base_types = Base_types
 module ID = ID
 module Fun = Base_types.Fun

src/core/Sidekick_core.ml

@@ -213,6 +213,9 @@ module type PROOF = sig
   val default : t [@@alert cstor "do not use default constructor"]
 
   val pp_debug : sharing:bool -> t Fmt.printer
+  (** Pretty print a proof.
+      @param sharing if true, try to compact the proof by introducing
+      definitions for common terms, clauses, and steps as needed. Safe to ignore. *)
 
   module Quip : sig
     val output : out_channel -> t -> unit
@@ -662,11 +665,6 @@ module type SOLVER_INTERNAL = sig
 
   (** {3 hooks for the theory} *)
 
-  val propagate : t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit
-  (** Propagate a literal for a reason. This is similar to asserting
-      the clause [reason => lit], but more lightweight, and in a way
-      that is backtrackable. *)
-
   val raise_conflict : t -> actions -> lit list -> proof -> 'a
   (** Give a conflict clause to the solver *)
 
@@ -676,7 +674,7 @@ module type SOLVER_INTERNAL = sig
       If the SAT solver backtracks, this (potential) decision is removed
       and forgotten. *)
 
-  val propagate: t -> actions -> lit -> (unit -> lit list * proof) -> unit
+  val propagate: t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 

src/lra/sidekick_arith_lra.ml

@@ -433,7 +433,7 @@ module Make(A : ARG) : S with module A = A = struct
     in
     (* TODO: more detailed proof certificate *)
     let pr =
-      A.(S.P.(proof_lra (Iter.of_list confl |> Iter.map plit_of_lit))) in
+      A.(proof_lra (Iter.of_list confl |> Iter.map plit_of_lit)) in
     SI.raise_conflict si acts confl pr
 
   let on_propagate_ si acts lit ~reason =
@@ -441,7 +441,7 @@ module Make(A : ARG) : S with module A = A = struct
     | Tag.Lit lit ->
       (* TODO: more detailed proof certificate *)
       SI.propagate si acts lit
-        (fun() ->
+        ~reason:(fun() ->
            let lits = CCList.flat_map (Tag.to_lits si) reason in
            let proof = A.proof_lra Iter.(cons lit (of_list lits) |> map plit_of_lit) in
            CCList.flat_map (Tag.to_lits si) reason, proof)

src/lra/simplex2.ml

@@ -148,7 +148,7 @@ module Make(Q : RATIONAL)(Var: VAR)
   module V_map = CCMap.Make(Var)
   module Q = Q
 
-  type num = Q.t (** Numbers *)
+  type num = Q.t
   let pp_q_dbg = Q.pp_approx 1
 
   module Constraint = struct

src/msat-solver/Sidekick_msat_solver.ml

@@ -70,9 +70,7 @@ module Make(A : ARG)
       if l.lit_sign then Term.pp out l.lit_term
       else Format.fprintf out "(@[@<1>¬@ %a@])" Term.pp l.lit_term
 
-    let apply_sign t s = if s then t else neg t
     let norm_sign l = if l.lit_sign then l, true else neg l, false
-    let norm l = let l, sign = norm_sign l in l, if sign then Msat.Same_sign else Msat.Negated
   end
 
   type lit = Lit_.t
@@ -252,12 +250,12 @@ module Make(A : ARG)
       Stat.incr self.count_conflict;
       acts.Msat.acts_raise_conflict c proof
 
-    let[@inline] propagate self acts p reason : unit =
+    let[@inline] propagate self acts p ~reason : unit =
       Stat.incr self.count_propagate;
       acts.Msat.acts_propagate p (Msat.Consequence reason)
 
     let[@inline] propagate_l self acts p cs proof : unit =
-      propagate self acts p (fun()->cs,proof)
+      propagate self acts p ~reason:(fun()->cs,proof)
 
     let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit =
       Stat.incr self.count_axiom;

src/smtlib/Sidekick_smtlib.ml

@@ -20,10 +20,6 @@ module Parse = struct
   let parse_file_exn file : Parse_ast.statement list =
     CCIO.with_in file (parse_chan_exn ~filename:file)
 
-  let parse_file file =
-    try Result.Ok (parse_file_exn file)
-    with e -> Result.Error (Printexc.to_string e)
-
   let parse_file_exn ctx file : Stmt.t list =
     (* delegate parsing to [Tip_parser] *)
     parse_file_exn file

src/smtlib/Typecheck.ml

@@ -29,7 +29,6 @@ module Ctx = struct
 
   and ty_kind =
     | K_atomic of Ty.def
-    | K_bool
 
   type t = {
     tst: T.state;
@@ -63,13 +62,8 @@ module Ctx = struct
     match StrTbl.get self.names s with
     | Some (_, K_ty (K_atomic def)) -> def
     | _ -> Error.errorf "expected %s to be an atomic type" s
-
-  let pp_kind out = function
-    | K_ty _ -> Format.fprintf out "type"
-    | K_fun f -> Fun.pp out f
 end
 
-let error_loc ctx : string = Fmt.sprintf "at %a: " pp_loc_opt (Ctx.loc ctx)
 let errorf_ctx ctx msg =
   Error.errorf ("at %a:@ " ^^ msg) pp_loc_opt (Ctx.loc ctx)
 

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -109,10 +109,6 @@ module Make(A : ARG) : S with module A = A = struct
     }
 
   let[@inline] not_ tst t = A.mk_bool tst (B_not t)
-  let[@inline] and_a tst a = A.mk_bool tst (B_and a)
-  let[@inline] or_a tst a = A.mk_bool tst (B_or a)
-  let[@inline] ite tst a b c = A.mk_bool tst (B_ite (a,b,c))
-  let[@inline] equiv tst a b = A.mk_bool tst (B_equiv (a,b))
   let[@inline] eq tst a b = A.mk_bool tst (B_eq (a,b))
 
   let is_true t = match T.as_bool t with Some true -> true | _ -> false