Merge branch 'wip-vendored-msat'

.github/workflows/main.yml

@@ -1,5 +1,11 @@
 name: Build sidekick-bin
-on: [push]
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
 jobs:
   run:
     name: Build

.header

@@ -1,5 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)

Makefile

@@ -67,7 +67,7 @@ reindent:
 
 WATCH=@all
 watch:
-	@dune build $(WATCH) -w
+	@dune build $(WATCH) -w $(OPTS) --profile=release
 	#@dune build @all -w # TODO: once tests pass
 
 .PHONY: clean doc all bench install uninstall remove reinstall bin test

sidekick-bin.opam

@@ -19,10 +19,13 @@ depends: [
   "sidekick" { = version }
   "sidekick-base" { = version }
   "menhir"
-  "mtime"
   "ocaml" { >= "4.04" }
   "odoc" {with-doc}
 ]
+depopts: [
+  "memtrace"
+  "mtime"
+]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"
 dev-repo: "git+https://github.com/c-cube/sidekick.git"

sidekick.opam

@@ -14,7 +14,6 @@ depends: [
   "dune" { >= "1.1" }
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
-  "msat" { >= "0.9" < "0.10" }
   "ocaml" { >= "4.04" }
   "alcotest" {with-test}
   "odoc" {with-doc}

src/backend/Backend_intf.ml

@@ -0,0 +1,27 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Backend interface
+
+    This modules defines the interface of the modules providing
+    export of proofs.
+*)
+
+module type S = sig
+  (** Proof exporting
+
+      Currently, exporting a proof means printing it into a file
+      according to the conventions of a given format.
+  *)
+
+  type t
+  (** The type of proofs. *)
+
+  val pp : Format.formatter -> t -> unit
+  (** A function for printing proofs in the desired format. *)
+
+end
+

src/backend/Dot.ml

@@ -0,0 +1,191 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Output interface for the backend *)
+module type S = Backend_intf.S
+
+(** Input module for the backend *)
+module type Arg = sig
+
+  type atom
+  (* Type of atoms *)
+
+  type hyp
+  type lemma
+  type assumption
+  (** Types for hypotheses, lemmas, and assumptions. *)
+
+  val print_atom : Format.formatter -> atom -> unit
+  (** Printing function for atoms *)
+
+  val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list
+  val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
+  val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list
+  (** Functions to return information about hypotheses and lemmas *)
+
+end
+
+module Default(S : Sidekick_sat.S) = struct
+  module Atom = S.Atom
+  module Clause = S.Clause
+
+  let print_atom = Atom.pp
+
+  let hyp_info c =
+    "hypothesis", Some "LIGHTBLUE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
+
+  let lemma_info c =
+    "lemma", Some "BLUE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
+
+  let assumption_info c =
+    "assumption", Some "PURPLE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
+
+end
+
+(** Functor to provide dot printing *)
+module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
+                                and type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) = struct
+  module Atom = S.Atom
+  module Clause = S.Clause
+  module P = S.Proof
+
+  let node_id n = Clause.short_name n.P.conclusion
+  let proof_id p = node_id (P.expand p)
+  let res_nn_id n1 n2 = node_id n1 ^ "_" ^ node_id n2 ^ "_res"
+  let res_np_id n1 n2 = node_id n1 ^ "_" ^ proof_id n2 ^ "_res"
+
+  let print_clause fmt c =
+    let v = Clause.atoms c in
+    if Array.length v = 0 then
+      Format.fprintf fmt "⊥"
+    else
+      let n = Array.length v in
+      for i = 0 to n - 1 do
+        Format.fprintf fmt "%a" A.print_atom v.(i);
+        if i < n - 1 then
+          Format.fprintf fmt ", "
+      done
+
+  let print_edge fmt i j =
+    Format.fprintf fmt "%s -> %s;@\n" j i
+
+  let print_edges fmt n =
+    match P.(n.step) with
+    | P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *)
+    | P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} ->
+      print_edge fmt (res_np_id n p0) (proof_id hr_init);
+      List.iter
+        (fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2))
+        l;
+    | _ -> ()
+
+  let table_options fmt color =
+    Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
+
+  let table fmt (c, rule, color, l) =
+    Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" print_clause c;
+    match l with
+    | [] ->
+      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
+    | f :: r ->
+      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD><TD>%a</TD></TR>"
+        color (List.length l) rule f ();
+      List.iter (fun f -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" f ()) r
+
+  let print_dot_node fmt id color c rule rule_color l =
+    Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %a>%a</TABLE>>];@\n"
+      id table_options color table (c, rule, rule_color, l)
+
+  let print_dot_res_node fmt id a =
+    Format.fprintf fmt "%s [label=<%a>];@\n" id A.print_atom a
+
+  let ttify f c = fun fmt () -> f fmt c
+
+  let print_contents fmt n =
+    match P.(n.step) with
+    (* Leafs of the proof tree *)
+    | P.Hypothesis _ ->
+      let rule, color, l = A.hyp_info P.(n.conclusion) in
+      let color = match color with None -> "LIGHTBLUE" | Some c -> c in
+      print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
+    | P.Assumption ->
+      let rule, color, l = A.assumption_info P.(n.conclusion) in
+      let color = match color with None -> "LIGHTBLUE" | Some c -> c in
+      print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
+    | P.Lemma _ ->
+      let rule, color, l = A.lemma_info P.(n.conclusion) in
+      let color = match color with None -> "YELLOW" | Some c -> c in
+      print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
+
+    (* Tree nodes *)
+    | P.Duplicate (p, l) ->
+      print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Duplicate" "GREY"
+        ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) ::
+         List.map (ttify A.print_atom) l);
+      print_edge fmt (node_id n) (node_id (P.expand p))
+    | P.Hyper_res {P.hr_steps=l; _} ->
+      print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY"
+        [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
+      List.iter
+        (fun (a,p2) ->
+          print_dot_res_node fmt (res_np_id n p2) a;
+          print_edge fmt (node_id n) (res_np_id n p2))
+        l
+
+  let print_node fmt n =
+    print_contents fmt n;
+    print_edges fmt n
+
+  let pp fmt p =
+    Format.fprintf fmt "digraph proof {@\n";
+    P.fold (fun () -> print_node fmt) () p;
+    Format.fprintf fmt "}@."
+
+end
+
+module Simple(S : Sidekick_sat.S)
+    (A : Arg with type atom := S.formula
+              and type hyp = S.formula list
+              and type lemma := S.lemma
+              and type assumption = S.formula) =
+  Make(S)(struct
+    module Atom = S.Atom
+    module Clause = S.Clause
+    module P = S.Proof
+
+    (* Some helpers *)
+    let lit = Atom.formula
+
+    let get_assumption c =
+      match S.Clause.atoms_l c with
+      | [ x ] -> x
+      | _ -> assert false
+
+    let get_lemma c =
+      match P.expand (P.prove c) with
+      | {P.step=P.Lemma p;_} -> p
+      | _ -> assert false
+
+    (* Actual functions *)
+    let print_atom fmt a =
+      A.print_atom fmt (lit a)
+
+    let hyp_info c =
+      A.hyp_info (List.map lit (S.Clause.atoms_l c))
+
+    let lemma_info c =
+      A.lemma_info (get_lemma c)
+
+    let assumption_info c =
+      A.assumption_info (lit (get_assumption c))
+
+  end)
+

src/backend/Dot.mli

@@ -0,0 +1,70 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Dot backend for proofs
+
+    This module provides functions to export proofs into the dot graph format.
+    Graphs in dot format can be used to generates images using the graphviz tool.
+*)
+
+module type S = Backend_intf.S
+(** Interface for exporting proofs. *)
+
+module type Arg = sig
+  (** Term printing for DOT
+
+      This module defines what functions are required in order to export
+      a proof to the DOT format.
+  *)
+
+  type atom
+  (** The type of atomic formuals *)
+
+  type hyp
+  type lemma
+  type assumption
+  (** The type of theory-specifi proofs (also called lemmas). *)
+
+  val print_atom : Format.formatter -> atom -> unit
+  (** Print the contents of the given atomic formulas.
+      WARNING: this function should take care to escape and/or not output special
+      reserved characters for the dot format (such as quotes and so on). *)
+
+  val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list
+  val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
+  val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list
+  (** Generate some information about the leafs of the proof tree. Currently this backend
+      print each lemma/assumption/hypothesis as a single leaf of the proof tree.
+      These function should return a triplet [(rule, color, l)], such that:
+      - [rule] is a name for the proof (arbitrary, does not need to be unique, but
+        should rather be descriptive)
+      - [color] is a color name (optional) understood by DOT
+      - [l] is a list of printers that will be called to print some additional information
+  *)
+
+end
+
+module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom
+                                 and type hyp := S.clause
+                                 and type lemma := S.clause
+                                 and type assumption := S.clause
+(** Provides a reasonnable default to instantiate the [Make] functor, assuming
+    the original printing functions are compatible with DOT html labels. *)
+
+module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
+                                and type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) : S with type t := S.Proof.t
+(** Functor for making a module to export proofs to the DOT format. *)
+
+module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.formula
+                                  and type hyp = S.formula list
+                                  and type lemma := S.lemma
+                                  and type assumption = S.formula) : S with type t := S.Proof.t
+(** Functor for making a module to export proofs to the DOT format.
+    The substitution of the hyp type is non-destructive due to a restriction
+    of destructive substitutions on earlier versions of ocaml. *)
+

src/backend/dune

@@ -0,0 +1,6 @@
+(library
+  (name sidekick_backend)
+  (public_name sidekick.backend)
+  (synopsis "Proof backends for sidekick")
+  (libraries sidekick.sat))
+

src/base/Base_types.ml

@@ -1,7 +1,7 @@
 (** Basic type definitions for Sidekick_base *)
 
-module Vec = Msat.Vec
-module Log = Msat.Log
+module Vec = Sidekick_util.Vec
+module Log = Sidekick_util.Log
 module Fmt = CCFormat
 
 module CC_view = Sidekick_core.CC_view

src/main/dune

@@ -4,8 +4,9 @@
  (name main)
  (public_name sidekick)
  (package sidekick-bin)
- (libraries containers iter result msat sidekick.core sidekick-base
-            sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
+ (libraries containers iter result sidekick.sat sidekick.core sidekick-base
+            sidekick.msat-solver sidekick-bin.smtlib sidekick.tef
+            sidekick.memtrace)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (rule

src/main/main.ml

@@ -4,14 +4,13 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-open CCResult.Infix
-
 module E = CCResult
 module Fmt = CCFormat
 module Term = Sidekick_base.Term
 module Solver = Sidekick_smtlib.Solver
 module Process = Sidekick_smtlib.Process
-module Vec = Msat.Vec
+
+open E.Infix
 
 type 'a or_error = ('a, string) E.t
 
@@ -84,43 +83,10 @@ let argspec = Arg.align [
     "--time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
     "-t", Arg.String (int_arg time_limit), " short for --time";
     "--version", Arg.Unit (fun () -> Printf.printf "version: %s\n%!" Sidekick_version.version; exit 0), " show version and exit";
-    "-d", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
-    "--debug", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
+    "-d", Arg.Int Log.set_debug, "<lvl> sets the debug verbose level";
+    "--debug", Arg.Int Log.set_debug, "<lvl> sets the debug verbose level";
   ] |> List.sort compare
 
-module Dimacs = struct
-  open Sidekick_base
-  module T = Term
-
-  let parse_file tst (file:string) : Statement.t list or_error =
-    let atoms = Util.Int_tbl.create 32 in
-    let get_lit i =
-      let v =
-        match Util.Int_tbl.find atoms (abs i) with
-        | x -> Term.const tst x
-        | exception Not_found ->
-          let f = Sidekick_base.Fun.mk_undef_const
-              (ID.makef "%d" (abs i)) (Ty.bool()) in
-          Util.Int_tbl.add atoms (abs i) f;
-          Term.const tst f
-      in
-      if i<0 then Term.not_ tst v else v
-    in
-    try
-      CCIO.with_in file
-        (fun ic ->
-           let p = Dimacs_parser.create ic in
-           let stmts = ref [] in
-           Dimacs_parser.iter p
-             (fun c ->
-                let lits = List.rev_map get_lit c in
-                stmts := Statement.Stmt_assert_clause lits :: !stmts);
-           stmts := Statement.Stmt_check_sat [] :: !stmts;
-           Ok (List.rev !stmts))
-    with e ->
-      E.of_exn_trace e
-end
-
 (* Limits alarm *)
 let check_limits () =
   let t = Sys.time () in
@@ -131,25 +97,12 @@ let check_limits () =
   else if s > !size_limit then
     raise Out_of_space
 
-let main () =
-  Sidekick_tef.setup();
-  at_exit Sidekick_tef.teardown;
-  CCFormat.set_color_default true;
-  (* Administrative duties *)
-  Arg.parse argspec input_file usage;
-  if !file = "" then (
-    Arg.usage argspec usage;
-    exit 2
-  );
-  let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
-  check := !check || CCOpt.is_some dot_proof; (* dot requires a proof *)
-  let al = Gc.create_alarm check_limits in
-  Util.setup_gc();
+let main_smt ~dot_proof () : _ result =
   let tst = Term.create ~size:4_096 () in
-  let is_cnf = Filename.check_suffix !file ".cnf" in
   let solver =
     let theories =
-      if is_cnf then [] else [
+      (* TODO: probes, to load only required theories *)
+      [
         Process.th_bool;
         Process.th_data;
         Process.th_lra;
@@ -164,8 +117,7 @@ let main () =
     Solver.add_theory solver Process.Check_cc.theory;
   );
   begin
-    if is_cnf then Dimacs.parse_file tst !file
-    else Sidekick_smtlib.parse tst !file
+    Sidekick_smtlib.parse tst !file
   end
   >>= fun input ->
   (* process statements *)
@@ -187,6 +139,39 @@ let main () =
   if !p_stat then (
     Format.printf "%a@." Solver.pp_stats solver;
   );
+  res
+
+let main_cnf () : _ result =
+  let solver = Pure_sat_solver.SAT.create ~size:`Big () in
+  Pure_sat_solver.Dimacs.parse_file solver !file >>= fun () ->
+  Pure_sat_solver.solve solver
+
+let main () =
+
+  (* instrumentation and tracing *)
+  Sidekick_tef.setup();
+  at_exit Sidekick_tef.teardown;
+  Sidekick_memtrace.trace_if_requested ~context:"sidekick" ();
+
+  CCFormat.set_color_default true;
+  (* Administrative duties *)
+  Arg.parse argspec input_file usage;
+  if !file = "" then (
+    Arg.usage argspec usage;
+    exit 2
+  );
+  let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
+  check := !check || CCOpt.is_some dot_proof; (* dot requires a proof *)
+  let al = Gc.create_alarm check_limits in
+  Util.setup_gc();
+  let is_cnf = Filename.check_suffix !file ".cnf" in
+  let res =
+    if is_cnf then (
+      main_cnf ()
+    ) else (
+      main_smt ~dot_proof ()
+    )
+  in
   if !p_gc_stat then (
     Printf.printf "(gc_stats\n%t)\n" Gc.print_stat;
   );

src/main/pure_sat_solver.ml

@@ -0,0 +1,58 @@
+
+(* pure SAT solver *)
+
+module E = CCResult
+module SS = Sidekick_sat
+
+module Arg = struct
+  module Formula = struct
+    type t = int
+    let norm t = if t>0 then t, SS.Same_sign else -t, SS.Negated
+    let abs = abs
+    let sign t = t>0
+    let equal = CCInt.equal
+    let hash = CCHash.int
+    let neg x = -x
+    let pp = Fmt.int
+  end
+  type proof=unit
+end
+
+module SAT = Sidekick_sat.Make_pure_sat(Arg)
+
+module Dimacs = struct
+  open Sidekick_base
+  module T = Term
+
+  let parse_file (solver:SAT.t) (file:string) : (unit, string) result =
+    let get_lit i : SAT.atom = SAT.make_atom solver i in
+
+    try
+      CCIO.with_in file
+        (fun ic ->
+           let p = Dimacs_parser.create ic in
+           Dimacs_parser.iter p
+             (fun c ->
+                let atoms = List.rev_map get_lit c in
+                SAT.add_clause solver atoms ());
+           Ok ())
+    with e ->
+      E.of_exn_trace e
+end
+
+let solve (solver:SAT.t) : (unit, string) result =
+  let res =
+    Profile.with_ "solve" (fun () -> SAT.solve solver)
+  in
+  let t2 = Sys.time () in
+  Printf.printf "\r"; flush stdout;
+  begin match res with
+    | SAT.Sat _ ->
+      let t3 = Sys.time () -. t2 in
+      Format.printf "Sat (%.3f/%.3f)@." t2 t3;
+    | SAT.Unsat _ ->
+
+      let t3 = Sys.time () -. t2 in
+      Format.printf "Unsat (%.3f/%.3f)@." t2 t3;
+  end;
+  Ok ()

src/memtrace/dune

@@ -0,0 +1,10 @@
+
+(library
+  (name sidekick_memtrace)
+  (public_name sidekick.memtrace)
+  (libraries
+    (select sidekick_memtrace.ml from
+            (memtrace -> sidekick_memtrace.real.ml)
+            (-> sidekick_memtrace.dummy.ml)))
+  (flags :standard -warn-error -a+8))
+

src/memtrace/sidekick_memtrace.dummy.ml

@@ -0,0 +1,2 @@
+
+let trace_if_requested ?context:_ ?sampling_rate:_ () = ()

src/memtrace/sidekick_memtrace.mli

@@ -0,0 +1,3 @@
+
+
+val trace_if_requested : ?context:string -> ?sampling_rate:float -> unit -> unit

src/memtrace/sidekick_memtrace.real.ml

@@ -0,0 +1 @@
+let trace_if_requested = Memtrace.trace_if_requested

src/msat-solver/Sidekick_msat_solver.ml

@@ -1,12 +1,10 @@
-(** {1 Implementation of a Solver using Msat} *)
+(** Core of the SMT solver using Sidekick_sat
 
-(** {{: https://github.com/Gbury/mSAT/} Msat} is a modular SAT solver in
+    Sidekick_sat (in src/sat/) 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 *)
+    This builds a {!Sidekick_core.SOLVER} on top of it.
+*)
 
 (** Argument to pass to the functor {!Make} in order to create a
     new Msat-based SMT solver. *)
@@ -76,7 +74,7 @@ module Make(A : ARG)
   type lit = Lit_.t
 
   (* actions from msat *)
-  type msat_acts = (Msat.void, lit, Msat.void, P.t) Msat.acts
+  type msat_acts = (lit, P.t) Sidekick_sat.acts
 
   (* the full argument to the congruence closure *)
   module CC_actions = struct
@@ -90,11 +88,13 @@ module Make(A : ARG)
       module P = P
       module Lit = Lit
       type t = msat_acts
-      let[@inline] raise_conflict a lits pr =
-        a.Msat.acts_raise_conflict lits pr
-      let[@inline] propagate a lit ~reason =
-        let reason = Msat.Consequence reason in
-        a.Msat.acts_propagate lit reason
+      let[@inline] raise_conflict (a:t) lits pr =
+        let (module A) = a in
+        A.raise_conflict lits pr
+      let[@inline] propagate (a:t) lit ~reason =
+        let (module A) = a in
+        let reason = Sidekick_sat.Consequence reason in
+        A.propagate lit reason
     end
   end
 
@@ -218,7 +218,7 @@ module Make(A : ARG)
       include Lit
       let norm lit =
         let lit', sign = norm_sign lit in
-        lit', if sign then Msat.Same_sign else Msat.Negated
+        lit', if sign then Sidekick_sat.Same_sign else Sidekick_sat.Negated
     end
     module Eq_class = CC.N
     module Expl = CC.Expl
@@ -243,23 +243,27 @@ module Make(A : ARG)
     let on_model_gen self f = self.mk_model <- f :: self.mk_model
 
     let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
+      let (module A) = acts in
       let sign = Lit.sign lit in
-      acts.Msat.acts_add_decision_lit (Lit.abs lit) sign
+      A.add_decision_lit (Lit.abs lit) sign
 
-    let[@inline] raise_conflict self acts c proof : 'a =
+    let[@inline] raise_conflict self (acts:actions) c proof : 'a =
+      let (module A) = acts in
       Stat.incr self.count_conflict;
-      acts.Msat.acts_raise_conflict c proof
+      A.raise_conflict c proof
 
-    let[@inline] propagate self acts p ~reason : unit =
+    let[@inline] propagate self (acts:actions) p ~reason : unit =
+      let (module A) = acts in
       Stat.incr self.count_propagate;
-      acts.Msat.acts_propagate p (Msat.Consequence reason)
+      A.propagate p (Sidekick_sat.Consequence reason)
 
     let[@inline] propagate_l self acts p cs proof : unit =
       propagate self acts p ~reason:(fun()->cs,proof)
 
-    let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit =
+    let add_sat_clause_ self (acts:actions) ~keep lits (proof:P.t) : unit =
+      let (module A) = acts in
       Stat.incr self.count_axiom;
-      acts.Msat.acts_add_clause ~keep lits proof
+      A.add_clause ~keep lits proof
 
     let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof =
       let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
@@ -377,7 +381,9 @@ module Make(A : ARG)
     let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit =
       add_sat_clause_ self acts ~keep:true lits proof
 
-    let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit
+    let[@inline] add_lit _self (acts:actions) lit : unit =
+      let (module A) = acts in
+      A.mk_lit lit
 
     let add_lit_t self acts ?sign t =
       let lit = mk_lit self acts ?sign t in
@@ -429,7 +435,7 @@ module Make(A : ARG)
 
     (* handle a literal assumed by the SAT solver *)
     let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
-      Msat.Log.debugf 2
+      Log.debugf 2
         (fun k->k "(@[<hv1>@{<green>msat-solver.assume_lits@}%s[lvl=%d]@ %a@])"
             (if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
       (* transmit to CC *)
@@ -456,28 +462,26 @@ module Make(A : ARG)
       );
       ()
 
-    let[@inline] iter_atoms_ acts : _ Iter.t =
+    let[@inline] iter_atoms_ (acts:actions) : _ Iter.t =
       fun f ->
-      acts.Msat.acts_iter_assumptions
-        (function
-          | Msat.Lit a -> f a
-          | Msat.Assign _ -> assert false)
+        let (module A) = acts in
+        A.iter_assumptions f
 
     (* propagation from the bool solver *)
     let check_ ~final (self:t) (acts: msat_acts) =
       let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
       let iter = iter_atoms_ acts in
-      Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
+      Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
       self.on_progress();
       assert_lits_ ~final self acts iter;
       Profile.exit pb
 
     (* propagation from the bool solver *)
-    let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
+    let[@inline] partial_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
       check_ ~final:false self acts
 
     (* perform final check of the model *)
-    let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
+    let[@inline] final_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
       check_ ~final:true self acts
 
     let create ~stat (tst:Term.store) (ty_st:Ty.store) () : t =
@@ -510,7 +514,7 @@ module Make(A : ARG)
   module Lit = Solver_internal.Lit
 
   (** the parametrized SAT Solver *)
-  module Sat_solver = Msat.Make_cdcl_t(Solver_internal)
+  module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
 
   module Atom = Sat_solver.Atom
 
@@ -519,7 +523,7 @@ module Make(A : ARG)
     module SC = Sat_solver.Clause
 
     type t = {
-      msat: Sat_solver.proof;
+      msat: Sat_solver.Proof.t;
       tdefs: (term*term) list; (* term definitions *)
       p: P.t lazy_t;
     }
@@ -528,7 +532,7 @@ module Make(A : ARG)
 
     let pp_dot =
       let module Dot =
-        Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) in
+        Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in
       let pp out self = Dot.pp out self.msat in
       Some pp
 
@@ -541,7 +545,7 @@ module Make(A : ARG)
          clause [c] under given assumptions (each assm is a lit),
          and return [-a1 \/ … \/ -an \/ c], discharging assumptions
     *)
-    let conv_proof (msat:Sat_solver.proof) (t_defs:_ list) : P.t =
+    let conv_proof (msat:Sat_solver.Proof.t) (t_defs:_ list) : P.t =
       let assms = ref [] in
       let steps = ref [] in
 
@@ -549,7 +553,7 @@ module Make(A : ARG)
       let n_tbl_: string SC.Tbl.t = SC.Tbl.create 32 in (* node.concl -> unique idx *)
 
       (* name of an already processed proof node *)
-      let find_proof_name (p:Sat_solver.proof) : string =
+      let find_proof_name (p:Sat_solver.Proof.t) : string =
         try SC.Tbl.find n_tbl_ (SP.conclusion p)
         with Not_found ->
           Error.errorf
@@ -633,7 +637,7 @@ module Make(A : ARG)
       let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in
       P.composite_l ~assms (CCList.append t_defs (List.rev !steps))
 
-    let make (msat: Sat_solver.proof) (tdefs: _ list) : t =
+    let make (msat: Sat_solver.Proof.t) (tdefs: _ list) : t =
       { msat; tdefs; p=lazy (conv_proof msat tdefs) }
 
     let check self = SP.check self.msat
@@ -912,22 +916,22 @@ module Make(A : ARG)
     let r = Sat_solver.solve ~assumptions (solver self) in
     Stat.incr self.count_solve;
     match r with
-    | Sat_solver.Sat st ->
+    | Sat_solver.Sat (module SAT) ->
       Log.debug 1 "sidekick.msat-solver: SAT";
-      let _lits f = st.iter_trail f (fun _ -> ()) in
+      let _lits f = SAT.iter_trail f in
       (* TODO: theory combination *)
       let m = mk_model self _lits in
       do_on_exit ();
       Sat m
-    | Sat_solver.Unsat us ->
+    | Sat_solver.Unsat (module UNSAT) ->
       let proof = lazy (
         try
-          let pr = us.get_proof () in
+          let pr = UNSAT.get_proof () in
           if check then Sat_solver.Proof.check pr;
           Some (Pre_proof.make pr (List.rev self.si.t_defs))
-        with Msat.Solver_intf.No_proof -> None
+        with Sidekick_sat.Solver_intf.No_proof -> None
       ) in
-      let unsat_core = lazy (us.Msat.unsat_assumptions ()) in
+      let unsat_core = lazy (UNSAT.unsat_assumptions ()) in
       do_on_exit ();
       Unsat {proof; unsat_core}
 

src/msat-solver/dune

@@ -2,5 +2,5 @@
  (name Sidekick_msat_solver)
  (public_name sidekick.msat-solver)
  (libraries containers iter sidekick.core sidekick.util
-   sidekick.cc msat msat.backend)
+            sidekick.cc sidekick.sat sidekick.backend)
  (flags :standard -open Sidekick_util))

src/sat/.gitignore

@@ -0,0 +1,13 @@
+_build/
+*.annot
+*.native
+*.log
+*.status
+.*.swp
+.session
+*.docdir
+src/util/log.ml
+doc/index.html
+*.exe
+.merlin
+*.install

src/sat/CHANGELOG.md

@@ -0,0 +1,118 @@
+# CHANGES
+
+## 0.9.1
+
+- add `on_conflit` callback
+- fix termination issue when using `push_decision_lit` from plugin
+
+## 0.9
+
+- feat: allow the theory to ask for some literals to be decided on
+- feat: allow to set the default polarity of variables at creation time
+
+## 0.8.3
+
+- support containers 3.0
+
+## 0.8.2
+
+- fix opam file
+- fix: allow conflicts below decision level in `Make_cdcl_t`
+
+## 0.8.1
+
+- fixes in `Heap`
+- package for `msat-bin`
+- use `iter` instead of `sequence` in dune and opam files
+- more docs
+
+## 0.8
+
+big refactoring, change of API with fewer functions, etc.
+see `git log` for more details.
+
+## 0.6.1
+
+- add simple functor for DOT backend
+- various bugfixes
+
+## 0.6
+
+### Feature
+
+- An already instantiated sat solver in the Sat module
+- A `full_slice` function for running possibly expensive satisfiability
+  tests (in SMT) when a propositional model has been found
+- Forgetful propagations: propagations whose reason (i.e clause) is not watched
+
+## 0.5.1
+
+### Bug
+
+- Removed some needless allocations
+
+### Breaking
+
+- Better interface for mcsat propagations
+
+### Feature
+
+- Allow level 0 semantic propagations
+
+## 0.5
+
+### Bug
+
+- Grow heap when adding local hyps
+- Avoid forgetting some one atom clauses
+- Fixed a bug for propagations at level 0
+- Late propagations need to be re-propagated
+- Fixed conflict at level 0
+- Avoid forgetting some theory conflict clauses
+
+### Breaking
+
+- Changed `if_sat` interface
+
+## 0.4.1
+
+### Bug
+
+- fix bug in `add_clause`
+
+## 0.4
+
+- performance improvements
+- many bugfixes
+- more tests
+
+### Breaking
+
+- remove push/pop (source of many bugs)
+- replaced by solve : assumptions:lit list -> unit -> result
+
+### Features
+
+- Accept late conflict clauses
+- cleaner API, moving some types outside the client-required interface
+
+## 0.3
+
+### Features
+
+- Proofs for atoms at level 0
+- Compatibility with ocaml >= 4.00
+- Released some restrictions on dummy sat theories
+
+## 0.2
+
+### Breaking
+
+- Log argument has been removed from functors
+- All the functors now take a dummy last argument to ensure the solver modules are unique
+
+### Features
+
+- push/pop operations
+- access to decision level when evaluating literals
+

src/sat/Heap.ml

@@ -0,0 +1,145 @@
+
+module type RANKED = Heap_intf.RANKED
+
+module type S = Heap_intf.S
+
+module Make(Elt : RANKED) = struct
+  type elt = Elt.t
+
+  type t = {
+    heap : elt Vec.t;
+  } [@@unboxed]
+
+  let _absent_index = -1
+
+  let create () =
+    { heap = Vec.create(); }
+
+  let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
+  let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
+  let[@inline] parent i = (i - 1) asr 1 (* (i-1) / 2 *)
+
+  (*
+  let rec heap_property cmp ({heap=heap} as s) i =
+    i >= (Vec.size heap)  ||
+      ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
+       && heap_property cmp s (left i) && heap_property cmp s (right i))
+
+  let heap_property cmp s = heap_property cmp s 1
+  *)
+
+  (* [elt] is above or at its expected position. Move it up the heap
+     (towards high indices) to restore the heap property *)
+  let percolate_up {heap} (elt:Elt.t) : unit =
+    let pi = ref (parent (Elt.idx elt)) in
+    let i = ref (Elt.idx elt) in
+    while !i <> 0 && Elt.cmp elt (Vec.get heap !pi) do
+      Vec.set heap !i (Vec.get heap !pi);
+      Elt.set_idx (Vec.get heap !i) !i;
+      i  := !pi;
+      pi := parent !i
+    done;
+    Vec.set heap !i elt;
+    Elt.set_idx elt !i
+
+  let percolate_down {heap} (elt:Elt.t): unit =
+    let sz = Vec.size heap in
+    let li = ref (left (Elt.idx elt)) in
+    let ri = ref (right (Elt.idx elt)) in
+    let i = ref (Elt.idx elt) in
+    begin
+      try
+        while !li < sz do
+          let child =
+            if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li)
+            then !ri
+            else !li
+          in
+          if not (Elt.cmp (Vec.get heap child) elt) then raise Exit;
+          Vec.set heap !i (Vec.get heap child);
+          Elt.set_idx (Vec.get heap !i) !i;
+          i  := child;
+          li := left !i;
+          ri := right !i
+        done;
+      with Exit -> ()
+    end;
+    Vec.set heap !i elt;
+    Elt.set_idx elt !i
+
+  let[@inline] in_heap x = Elt.idx x >= 0
+
+  let[@inline] decrease s x = assert (in_heap x); percolate_up s x
+
+  (*
+  let increase cmp s n =
+    assert (in_heap s n); percolate_down cmp s (V.get s.indices n)
+  *)
+
+  let filter s filt =
+    let j = ref 0 in
+    let lim = Vec.size s.heap in
+    for i = 0 to lim - 1 do
+      if filt (Vec.get s.heap i) then (
+        Vec.set s.heap !j (Vec.get s.heap i);
+        Elt.set_idx (Vec.get s.heap i) !j;
+        incr j;
+      ) else (
+        Elt.set_idx (Vec.get s.heap i) _absent_index;
+      );
+    done;
+    Vec.shrink s.heap (lim - !j);
+    for i = (lim / 2) - 1 downto 0 do
+      percolate_down s (Vec.get s.heap i)
+    done
+
+  let size s = Vec.size s.heap
+
+  let is_empty s = Vec.is_empty s.heap
+
+  let clear {heap} =
+    Vec.iter (fun e -> Elt.set_idx e _absent_index) heap;
+    Vec.clear heap;
+    ()
+
+  let insert s elt =
+    if not (in_heap elt) then (
+      Elt.set_idx elt (Vec.size s.heap);
+      Vec.push s.heap elt;
+      percolate_up s elt;
+    )
+
+  (*
+  let update cmp s n =
+    assert (heap_property cmp s);
+    begin
+      if in_heap s n then
+        begin
+          percolate_up cmp s (Vec.get s.indices n);
+          percolate_down cmp s (Vec.get s.indices n)
+        end
+      else insert cmp s n
+    end;
+    assert (heap_property cmp s)
+  *)
+
+  let remove_min ({heap} as s) =
+    match Vec.size heap with
+    | 0 -> raise Not_found
+    | 1 ->
+      let x = Vec.pop heap in
+      Elt.set_idx x _absent_index;
+      x
+    | _ ->
+      let x = Vec.get heap 0 in
+      let new_hd = Vec.pop heap in (* heap.last() *)
+      Vec.set heap 0 new_hd;
+      Elt.set_idx x _absent_index;
+      Elt.set_idx new_hd 0;
+      (* enforce heap property again *)
+      if Vec.size heap > 1 then (
+        percolate_down s new_hd;
+      );
+      x
+
+end [@@inline]

src/sat/Heap.mli

@@ -0,0 +1,5 @@
+module type RANKED = Heap_intf.RANKED
+
+module type S = Heap_intf.S
+
+module Make(X : RANKED) : S with type elt = X.t

src/sat/Heap_intf.ml

@@ -0,0 +1,51 @@
+
+module type RANKED = sig
+  type t
+
+  val idx: t -> int
+  (** Index in heap. return -1 if never set *)
+
+  val set_idx : t -> int -> unit
+  (** Update index in heap *)
+
+  val cmp : t -> t -> bool
+end
+
+module type S = sig
+  type elt
+  (** Type of elements *)
+
+  type t
+  (** Heap of {!elt}, whose priority is increased or decreased
+      incrementally (see {!decrease} for instance) *)
+
+  val create : unit -> t
+  (** Create a heap *)
+
+  val decrease : t -> elt -> unit
+  (** [decrease h x] decreases the value associated to [x] within [h] *)
+
+  val in_heap : elt -> bool
+
+  (*val increase : (int -> int -> bool) -> t -> int -> unit*)
+
+  val size : t -> int
+  (** Number of integers within the heap *)
+
+  val is_empty : t -> bool
+
+  val clear : t -> unit
+  (** Clear the content of the heap *)
+
+  val insert : t -> elt -> unit
+  (** Insert a new element into the heap *)
+
+  (*val update : (int -> int -> bool) -> t -> int -> unit*)
+
+  val remove_min : t -> elt
+  (** Remove and return the integer that has the lowest value from the heap
+      @raise Not_found if the heap is empty *)
+
+  val filter : t -> (elt -> bool) -> unit
+  (** Filter out values that don't satisfy the predicate *)
+end

src/sat/README.md

@@ -0,0 +1,188 @@
+# MSAT  [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT)
+
+MSAT is an OCaml library that features a modular SAT-solver and some
+extensions (including SMT), derived from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
+
+It was presented at [ICFP 2017](https://icfp17.sigplan.org/event/ocaml-2017-papers-msat-an-ocaml-sat-solver),
+using a [poster](https://github.com/Gbury/mSAT/blob/master/articles/icfp_2017.pdf)
+
+
+## COPYRIGHT
+
+This program is distributed under the Apache Software License version
+2.0. See the enclosed file `LICENSE`.
+
+## Documentation
+
+See https://gbury.github.io/mSAT/
+
+## INSTALLATION
+
+### Via opam
+
+Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
+For the development version, use:
+
+```
+opam pin add msat https://github.com/Gbury/mSAT.git
+```
+
+### Manual installation
+
+You will need `dune` and `iter`. The command is:
+
+```
+$ make install
+```
+
+## USAGE
+
+### Generic SAT/SMT Solver
+
+A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
+as a functor which takes two modules :
+
+  - A representation of formulas (which implements the `Formula_intf.S` signature)
+
+  - A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions.
+
+  - A dummy empty module to ensure generativity of the solver (solver modules heavily relies on
+  side effects to their internal state)
+
+### Sat Solver
+
+A ready-to-use SAT solver is available in the `Msat_sat` module
+using the `msat.sat` library. It can be loaded
+as shown in the following code :
+
+```ocaml
+# #require "msat";;
+# #require "msat.sat";;
+# #print_depth 0;; (* do not print details *)
+```
+
+Then we can create a solver and create some boolean variables:
+
+```ocaml
+module Sat = Msat_sat
+module E = Sat.Int_lit (* expressions *)
+
+let solver = Sat.create()
+
+(* We create here two distinct atoms *)
+let a = E.fresh ()    (* A 'new_atom' is always distinct from any other atom *)
+let b = E.make 1      (* Atoms can be created from integers *)
+```
+
+We can try and check the satisfiability of some clauses — here, the clause `a or b`.
+`Sat.assume` adds a list of clauses to the solver. Calling `Sat.solve`
+will check the satisfiability of the current set of clauses, here "Sat".
+
+```ocaml
+# a <> b;;
+- : bool = true
+# Sat.assume solver [[a; b]] ();;
+- : unit = ()
+# let res = Sat.solve solver;;
+val res : Sat.res = Sat.Sat ...
+```
+
+The Sat solver has an incremental mutable state, so we still have
+the clause `a or b` in our assumptions.
+We add `not a` and `not b` to the state, and get "Unsat".
+
+```ocaml
+# Sat.assume solver [[E.neg a]; [E.neg b]] () ;;
+- : unit = ()
+# let res = Sat.solve solver ;;
+val res : Sat.res = Sat.Unsat ...
+```
+
+#### Formulas API
+
+Writing clauses by hand can be tedious and error-prone.
+The functor `Msat_tseitin.Make` in the library `msat.tseitin`
+proposes a formula AST (parametrized by
+atoms) and a function to convert these formulas into clauses:
+
+```ocaml
+# #require "msat.tseitin";;
+```
+
+```ocaml
+(* Module initialization *)
+module F = Msat_tseitin.Make(E)
+
+let solver = Sat.create ()
+
+(* We create here two distinct atoms *)
+let a = E.fresh ()    (* A fresh atom is always distinct from any other atom *)
+let b = E.make 1      (* Atoms can be created from integers *)
+
+(* Let's create some formulas *)
+let p = F.make_atom a
+let q = F.make_atom b
+let r = F.make_and [p; q]
+let s = F.make_or [F.make_not p; F.make_not q]
+```
+
+We can try and check the satisfiability of the given formulas, by turning
+it into clauses using `make_cnf`:
+
+```ocaml
+# Sat.assume solver (F.make_cnf r) ();;
+- : unit = ()
+# Sat.solve solver;;
+- : Sat.res = Sat.Sat ...
+```
+
+```ocaml
+# Sat.assume solver (F.make_cnf s) ();;
+- : unit = ()
+# Sat.solve solver ;;
+- : Sat.res = Sat.Unsat ...
+```
+
+### CDCL(T): a Sudoku solver as an example
+
+The directory `src/sudoku/` contains a simple Sudoku solver that
+uses the interface `Msat.Make_cdcl_t`.
+In essence, it implements the logical theory `CDCL(Sudoku)`.
+The script `sudoku_solve.sh` compiles and runs the solver,
+as does `dune exec src/sudoku/sudoku_solve.exe`.
+
+It's able to parse sudoku grids denoted as 81 integers
+(see `tests/sudoku/sudoku.txt` for example).
+
+Here is a sample grid and the output from the solver (in roughly .5s):
+
+```sh non-deterministic=command
+$ echo '..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9' > sudoku.txt
+$ dune exec src/sudoku/sudoku_solve.exe -- sudoku.txt
+...
+#########################
+solve grid:
+  .........
+  .....3.85
+  ..1.2....
+  ...5.7...
+  ..4...1..
+  .9.......
+  5......73
+  ..2.1....
+  ....4...9
+  
+...
+  987654321
+  246173985
+  351928746
+  128537694
+  634892157
+  795461832
+  519286473
+  472319568
+  863745219
+  
+###################
+...
+```

src/sat/Sidekick_sat.ml

@@ -0,0 +1,39 @@
+(** Main API *)
+
+
+module Solver_intf = Solver_intf
+
+module type S = Solver_intf.S
+module type FORMULA = Solver_intf.FORMULA
+module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
+module type PROOF = Solver_intf.PROOF
+
+type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
+
+module type SAT_STATE = Solver_intf.SAT_STATE
+type 'form sat_state = 'form Solver_intf.sat_state
+
+type ('formula, 'proof) reason = ('formula, 'proof) Solver_intf.reason =
+  | Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
+
+module type ACTS = Solver_intf.ACTS
+type ('formula, 'proof) acts = ('formula, 'proof) Solver_intf.acts
+
+type negated = Solver_intf.negated = Negated | Same_sign
+
+(** Print {!negated} values *)
+let pp_negated out = function
+  | Negated -> Format.fprintf out "negated"
+  | Same_sign -> Format.fprintf out "same-sign"
+
+(** Print {!lbool} values *)
+let pp_lbool out = function
+  | L_true -> Format.fprintf out "true"
+  | L_false -> Format.fprintf out "false"
+  | L_undefined -> Format.fprintf out "undefined"
+
+exception No_proof = Solver_intf.No_proof
+
+module Solver = Solver
+module Make_cdcl_t = Solver.Make_cdcl_t
+module Make_pure_sat = Solver.Make_pure_sat

src/sat/Solver_intf.ml

@@ -0,0 +1,426 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
+
+(** Interface for Solvers
+
+    This modules defines the safe external interface for solvers.
+    Solvers that implements this interface can be obtained using the [Make]
+    functor in {!Solver} or {!Mcsolver}.
+*)
+
+type 'a printer = Format.formatter -> 'a -> unit
+
+module type SAT_STATE = sig
+  type formula
+
+  val eval : formula -> bool
+  (** Returns the valuation of a formula in the current state
+      of the sat solver.
+      @raise UndecidedLit if the literal is not decided *)
+
+  val eval_level : formula -> bool * int
+  (** Return the current assignement of the literals, as well as its
+      decision level. If the level is 0, then it is necessary for
+      the atom to have this value; otherwise it is due to choices
+      that can potentially be backtracked.
+      @raise UndecidedLit if the literal is not decided *)
+
+  val iter_trail : (formula -> unit) -> unit
+  (** Iter through the formulas in order of decision/propagation
+      (starting from the first propagation, to the last propagation). *)
+end
+
+type 'form sat_state = (module SAT_STATE with type formula = 'form)
+(** The type of values returned when the solver reaches a SAT state. *)
+
+module type UNSAT_STATE = sig
+  type atom
+  type clause
+  type proof
+
+  val unsat_conflict : unit -> clause
+  (** Returns the unsat clause found at the toplevel *)
+
+  val get_proof : unit -> proof
+  (** returns a persistent proof of the empty clause from the Unsat result. *)
+
+  val unsat_assumptions: unit -> atom list
+  (** Subset of assumptions responsible for "unsat" *)
+end
+
+type ('atom, 'clause, 'proof) unsat_state =
+  (module UNSAT_STATE with type atom = 'atom
+                       and type clause = 'clause
+                       and type proof = 'proof)
+(** The type of values returned when the solver reaches an UNSAT state. *)
+
+type negated =
+  | Negated     (** changed sign *)
+  | Same_sign   (** kept sign *)
+(** This type is used during the normalisation of formulas.
+    See {!val:Expr_intf.S.norm} for more details. *)
+
+type ('formula, 'proof) reason =
+  | Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
+  (** [Consequence (l, p)] means that the formulas in [l] imply the propagated
+      formula [f]. The proof should be a proof of the clause "[l] implies [f]".
+
+      invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in
+      the current trail.
+
+      {b note} on lazyiness: the justification is suspended (using [unit -> …])
+      to avoid potentially costly computations that might never be used
+      if this literal is backtracked without participating in a conflict.
+      Therefore the function that produces [(l,p)] needs only be safe in
+      trails (partial models) that are conservative extensions of the current
+      trail.
+      If the theory isn't robust w.r.t. extensions of the trail (e.g. if
+      its internal state undergoes significant changes),
+      it can be easier to produce the explanation eagerly when
+      propagating, and then use [Consequence (fun () -> expl, proof)] with
+      the already produced [(expl,proof)] tuple.
+  *)
+(** The type of reasons for propagations of a formula [f]. *)
+
+type lbool = L_true | L_false | L_undefined
+(** Valuation of an atom *)
+
+module type ACTS = sig
+  type formula
+  type proof
+
+  val iter_assumptions: (formula -> unit) -> unit
+  (** Traverse the new assumptions on the boolean trail. *)
+
+  val eval_lit: formula -> lbool
+  (** Obtain current value of the given literal *)
+
+  val mk_lit: ?default_pol:bool -> formula -> unit
+  (** Map the given formula to a literal, which will be decided by the
+      SAT solver. *)
+
+  val add_clause: ?keep:bool -> formula list -> proof -> unit
+  (** Add a clause to the solver.
+      @param keep if true, the clause will be kept by the solver.
+        Otherwise the solver is allowed to GC the clause and propose this
+        partial model again.
+  *)
+
+  val raise_conflict: formula list -> proof -> 'b
+  (** Raise a conflict, yielding control back to the solver.
+      The list of atoms must be a valid theory lemma that is false in the
+      current trail. *)
+
+  val propagate: formula -> (formula, proof) reason -> unit
+  (** Propagate a formula, i.e. the theory can evaluate the formula to be true
+      (see the definition of {!type:eval_res} *)
+
+  val add_decision_lit: formula -> bool -> unit
+  (** Ask the SAT solver to decide on the given formula with given sign
+      before it can answer [SAT]. The order of decisions is still unspecified.
+      Useful for theory combination. This will be undone on backtracking. *)
+end
+
+(* TODO: find a way to use atoms instead of formulas here *)
+type ('formula, 'proof) acts =
+  (module ACTS with type formula = 'formula
+                and type proof = 'proof)
+(** The type for a slice of assertions to assume/propagate in the theory. *)
+
+exception No_proof
+
+module type FORMULA = sig
+  (** formulas *)
+
+  type t
+  (** The type of atomic formulas over terms. *)
+
+  val equal : t -> t -> bool
+  (** Equality over formulas. *)
+
+  val hash : t -> int
+  (** Hashing function for formulas. Should be such that two formulas equal according
+      to {!val:Expr_intf.S.equal} have the same hash. *)
+
+  val pp : t printer
+  (** Printing function used among other thing for debugging.  *)
+
+  val neg : t -> t
+  (** Formula negation *)
+
+  val norm : t -> t * negated
+  (** Returns a 'normalized' form of the formula, possibly negated
+      (in which case return [Negated]).
+      [norm] must be so that [a] and [neg a] normalise to the same formula,
+      but one returns [Negated] and the other [Same_sign]. *)
+end
+
+(** Signature for theories to be given to the CDCL(T) solver *)
+module type PLUGIN_CDCL_T = sig
+  type t
+  (** The plugin state itself *)
+
+  module Formula : FORMULA
+
+  type proof
+
+  val push_level : t -> unit
+  (** Create a new backtrack level *)
+
+  val pop_levels : t -> int -> unit
+  (** Pop [n] levels of the theory *)
+
+  val partial_check : t -> (Formula.t, proof) acts -> unit
+  (** Assume the formulas in the slice, possibly using the [slice]
+      to push new formulas to be propagated or to raising a conflict or to add
+      new lemmas. *)
+
+  val final_check : t -> (Formula.t, proof) acts -> unit
+  (** Called at the end of the search in case a model has been found.
+      If no new clause is pushed, then proof search ends and "sat" is returned;
+      if lemmas are added, search is resumed;
+      if a conflict clause is added, search backtracks and then resumes. *)
+end
+
+(** Signature for pure SAT solvers *)
+module type PLUGIN_SAT = sig
+  module Formula : FORMULA
+
+  type proof
+end
+
+module type PROOF = sig
+  (** Signature for a module handling proof by resolution from sat solving traces *)
+
+  (** {3 Type declarations} *)
+
+  exception Resolution_error of string
+  (** Raised when resolution failed. *)
+
+  type formula
+  type atom
+  type lemma
+  type clause
+  (** Abstract types for atoms, clauses and theory-specific lemmas *)
+
+  type t
+  (** Lazy type for proof trees. Proofs are persistent objects, and can be
+      extended to proof nodes using functions defined later. *)
+
+  and proof_node = {
+    conclusion : clause;  (** The conclusion of the proof *)
+    step : step;          (** The reasoning step used to prove the conclusion *)
+  }
+  (** A proof can be expanded into a proof node, which show the first step of the proof. *)
+
+  (** The type of reasoning steps allowed in a proof. *)
+  and step =
+    | Hypothesis of lemma
+    (** The conclusion is a user-provided hypothesis *)
+    | Assumption
+    (** The conclusion has been locally assumed by the user *)
+    | Lemma of lemma
+    (** The conclusion is a tautology provided by the theory, with associated proof *)
+    | Duplicate of t * atom list
+    (** The conclusion is obtained by eliminating multiple occurences of the atom in
+        the conclusion of the provided proof. *)
+    | Hyper_res of hyper_res_step
+
+  and hyper_res_step = {
+    hr_init: t;
+    hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
+  }
+
+  (** {3 Proof building functions} *)
+
+  val prove : clause -> t
+  (** Given a clause, return a proof of that clause.
+      @raise Resolution_error if it does not succeed. *)
+
+  val prove_unsat : clause -> t
+  (** Given a conflict clause [c], returns a proof of the empty clause.
+      @raise Resolution_error if it does not succeed. *)
+
+  val prove_atom : atom -> t option
+  (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *)
+
+  val res_of_hyper_res : hyper_res_step -> t * t * atom
+  (** Turn an hyper resolution step into a resolution step.
+      The conclusion can be deduced by performing a resolution between the conclusions
+      of the two given proofs.
+      The atom on which to perform the resolution is also given. *)
+
+  (** {3 Proof Nodes} *)
+
+  val parents : step -> t list
+  (** Returns the parents of a proof node. *)
+
+  val is_leaf : step -> bool
+  (** Returns wether the the proof node is a leaf, i.e. an hypothesis,
+      an assumption, or a lemma.
+      [true] if and only if {!parents} returns the empty list. *)
+
+  val expl : step -> string
+  (** Returns a short string description for the proof step; for instance
+      ["hypothesis"] for a [Hypothesis]
+      (it currently returns the variant name in lowercase). *)
+
+
+  (** {3 Proof Manipulation} *)
+
+  val expand : t -> proof_node
+  (** Return the proof step at the root of a given proof. *)
+
+  val conclusion : t -> clause
+  (** What is proved at the root of the clause *)
+
+  val fold : ('a -> proof_node -> 'a) -> 'a -> t -> 'a
+  (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
+      [f] is executed exactly once on each proof node in the tree, and that the execution of
+      [f] on a proof node happens after the execution on the parents of the nodes. *)
+
+  val unsat_core : t -> clause list
+  (** Returns the unsat_core of the given proof, i.e the lists of conclusions
+      of all leafs of the proof.
+      More efficient than using the [fold] function since it has
+      access to the internal representation of proofs *)
+
+  (** {3 Misc} *)
+
+  val check_empty_conclusion : t -> unit
+  (** Check that the proof's conclusion is the empty clause,
+      @raise Resolution_error otherwise *)
+
+  val check : t -> unit
+  (** Check the contents of a proof. Mainly for internal use. *)
+
+  module Tbl : Hashtbl.S with type key = t
+end
+
+(** The external interface implemented by safe solvers, such as the one
+    created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
+module type S = sig
+  (** {2 Internal modules}
+      These are the internal modules used, you should probably not use them
+      if you're not familiar with the internals of mSAT. *)
+
+  module Formula : FORMULA
+
+  type formula = Formula.t (** user formulas *)
+
+  type atom
+  (** The type of atoms given by the module argument for formulas.
+      An atom is a user-defined atomic formula whose truth value is
+      picked by Msat. *)
+
+  type clause
+
+  type theory
+
+  type lemma
+  (** A theory lemma or an input axiom *)
+
+  type solver
+
+  (* TODO: keep this internal *)
+  module Atom : sig
+    type t = atom
+
+    val equal : t -> t -> bool
+    val compare : t -> t -> int
+    val hash : t -> int
+    val neg : t -> t
+    val sign : t -> bool
+    val abs : t -> t
+    val formula : t -> formula
+    val pp : t printer
+  end
+
+  module Clause : sig
+    type t = clause
+
+    val atoms : t -> atom array
+    val atoms_l : t -> atom list
+    val equal : t -> t -> bool
+
+    val short_name : t -> string
+    val pp : t printer
+
+    module Tbl : Hashtbl.S with type key = t
+  end
+
+  module Proof : PROOF
+    with type clause = clause
+     and type atom = atom
+     and type formula = formula
+     and type lemma = lemma
+  (** A module to manipulate proofs. *)
+
+  type t = solver
+  (** Main solver type, containing all state for solving. *)
+
+  val create :
+    ?on_conflict:(atom array -> unit) ->
+    ?on_decision:(atom -> unit) ->
+    ?on_new_atom:(atom -> unit) ->
+    ?store_proof:bool ->
+    ?size:[`Tiny|`Small|`Big] ->
+    theory ->
+    t
+  (** Create new solver
+      @param theory the theory
+      @param store_proof if true, stores proof (default [true]). Otherwise
+        the functions that return proofs will fail with [No_proof]
+      @param size the initial size of internal data structures. The bigger,
+        the faster, but also the more RAM it uses. *)
+
+  val theory : t -> theory
+  (** Access the theory state *)
+
+  (** {2 Types} *)
+
+  (** Result type for the solver *)
+  type res =
+    | Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *)
+    | Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
+
+  exception UndecidedLit
+  (** Exception raised by the evaluating functions when a literal
+      has not yet been assigned a value. *)
+
+  (** {2 Base operations} *)
+
+  val assume : t -> formula list list -> lemma -> unit
+  (** Add the list of clauses to the current set of assumptions.
+      Modifies the sat solver state in place. *)
+
+  val add_clause : t -> atom list -> lemma -> unit
+  (** Lower level addition of clauses *)
+
+  val add_clause_a : t -> atom array -> lemma -> unit
+  (** Lower level addition of clauses *)
+
+  val solve :
+    ?assumptions:atom list ->
+    t -> res
+  (** Try and solves the current set of clauses.
+      @param assumptions additional atomic assumptions to be temporarily added.
+        The assumptions are just used for this call to [solve], they are
+        not saved in the solver's state. *)
+
+  val make_atom : t -> formula -> atom
+  (** Add a new atom (i.e propositional formula) to the solver.
+      This formula will be decided on at some point during solving,
+      wether it appears in clauses or not. *)
+
+  val true_at_level0 : t -> atom -> bool
+  (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
+      it must hold in all models *)
+
+  val eval_atom : t -> atom -> lbool
+  (** Evaluate atom in current state *)
+end
+

src/sat/dune

@@ -0,0 +1,10 @@
+
+(library
+  (name sidekick_sat)
+  (public_name sidekick.sat)
+  (libraries iter sidekick.util)
+  (synopsis "Pure OCaml SAT solver implementation for sidekick")
+  (flags :standard -open Sidekick_util)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+  )

src/smtlib/Typecheck.ml

@@ -5,7 +5,6 @@
 open Sidekick_base
 module Loc = Smtlib_utils.V_2_6.Loc
 module Fmt = CCFormat
-module Log = Msat.Log
 
 module PA = Smtlib_utils.V_2_6.Ast
 module BT = Sidekick_base

src/smtlib/dune

@@ -1,8 +1,8 @@
 (library
  (name sidekick_smtlib)
  (public_name sidekick-bin.smtlib)
- (libraries containers zarith msat sidekick.core sidekick.util
+ (libraries containers zarith sidekick.core sidekick.util
             sidekick-base sidekick-base.solver
-            msat.backend smtlib-utils
+            sidekick.backend smtlib-utils
             sidekick.tef)
  (flags :standard -warn-error -a+8 -open Sidekick_util))

src/tef/Sidekick_tef.dummy.ml

@@ -0,0 +1,3 @@
+
+let setup() = ()
+let teardown() = ()

src/tef/dune

@@ -3,6 +3,10 @@
   (name sidekick_tef)
   (public_name sidekick.tef)
   (synopsis "profiling backend based on TEF")
-  (optional)
   (flags :standard -warn-error -a+8)
-  (libraries sidekick.util unix threads mtime mtime.clock.os))
+  (libraries
+    sidekick.util unix threads
+    (select Sidekick_tef.ml from
+      (mtime mtime.clock.os -> Sidekick_tef.real.ml)
+      (-> Sidekick_tef.dummy.ml)))
+  (optional))

src/util/Backtrack_stack.ml

@@ -1,6 +1,4 @@
 
-module Vec = Msat.Vec
-
 type 'a t = {
   vec: 'a Vec.t;
   lvls: int Vec.t;

src/util/Log.ml

@@ -0,0 +1,28 @@
+
+(** {1 Logging functions, real version} *)
+
+let enabled = true (* NOTE: change here for 0-overhead *)
+
+let debug_level_ = ref 0
+let set_debug l = debug_level_ := l
+let get_debug () = !debug_level_
+
+let debug_fmt_ = ref Format.err_formatter
+
+let set_debug_out f = debug_fmt_ := f
+
+(* does the printing, inconditionally *)
+let debug_real_ l k =
+  k (fun fmt ->
+    Format.fprintf !debug_fmt_ "@[<2>@{<Blue>[%d|%.3f]@}@ "
+      l (Sys.time());
+    Format.kfprintf
+      (fun fmt -> Format.fprintf fmt "@]@.")
+      !debug_fmt_ fmt)
+
+let[@inline] debugf l k =
+  if enabled && l <= !debug_level_ then (
+    debug_real_ l k;
+  )
+
+let[@inline] debug l msg = debugf l (fun k->k "%s" msg)

src/util/Log.mli

@@ -0,0 +1,24 @@
+
+(** Logging function, for debugging *)
+
+val enabled : bool
+
+val set_debug : int -> unit
+(** Set debug level *)
+
+val get_debug : unit -> int
+(** Current debug level *)
+
+val debugf :
+  int ->
+  ((('a, Format.formatter, unit, unit) format4 -> 'a) -> unit) ->
+  unit
+(** Emit a debug message at the given level. If the level is lower
+    than [get_debug ()], the message will indeed be emitted *)
+
+val debug : int -> string -> unit
+(** Simpler version of {!debug}, without formatting *)
+
+val set_debug_out : Format.formatter -> unit
+(** Change the output formatter. *)
+

src/util/Sidekick_util.ml

@@ -1,9 +1,10 @@
 (* re-exports *)
 module Fmt = CCFormat
-module Vec = Msat.Vec
-module Log = Msat.Log
+
 
 module Util = Util
+module Vec = Vec
+module Log = Log
 module Backtrack_stack = Backtrack_stack
 module Backtrackable_tbl = Backtrackable_tbl
 module Error = Error

src/util/Vec.ml

@@ -0,0 +1,113 @@
+
+type 'a t = {
+  mutable data : 'a array;
+  mutable sz : int;
+}
+
+let make n x = {data=Array.make n x; sz=0}
+
+let[@inline] create () = {data = [||]; sz = 0}
+
+let[@inline] clear s = s.sz <- 0
+
+let[@inline] shrink t i =
+  assert (i >= 0);
+  assert (i<=t.sz);
+  t.sz <- i
+
+let[@inline] pop t =
+  if t.sz = 0 then invalid_arg "vec.pop";
+  let x = Array.unsafe_get t.data (t.sz - 1) in
+  t.sz <- t.sz - 1;
+  x
+
+let[@inline] size t = t.sz
+
+let[@inline] is_empty t = t.sz = 0
+
+let[@inline] is_full t = Array.length t.data = t.sz
+
+let[@inline] copy t : _ t =
+  let data = Array.copy t.data in
+  {t with data}
+
+(* grow the array *)
+let[@inline never] grow_to_double_size t x : unit =
+  if Array.length t.data = Sys.max_array_length then (
+    failwith "vec: cannot resize";
+  );
+  let size =
+    min Sys.max_array_length (max 4 (2 * Array.length t.data))
+  in
+  let arr' = Array.make size x in
+  Array.blit t.data 0 arr' 0 (Array.length t.data);
+  t.data <- arr';
+  assert (Array.length t.data > t.sz);
+  ()
+
+let[@inline] push t x : unit =
+  if is_full t then grow_to_double_size t x;
+  Array.unsafe_set t.data t.sz x;
+  t.sz <- t.sz + 1
+
+let[@inline] get t i =
+  if i < 0 || i >= t.sz then invalid_arg "vec.get";
+  Array.unsafe_get t.data i
+
+let[@inline] set t i v =
+  if i < 0 || i > t.sz then invalid_arg "vec.set";
+  if i = t.sz then (
+    push t v
+  ) else (
+    Array.unsafe_set t.data i v
+  )
+
+let[@inline] fast_remove t i =
+  assert (i>= 0 && i < t.sz);
+  Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1);
+  t.sz <- t.sz - 1
+
+let filter_in_place f vec =
+  let i = ref 0 in
+  while !i < size vec do
+    if f (Array.unsafe_get vec.data !i) then incr i else fast_remove vec !i
+  done
+
+let sort t f : unit =
+  let sub_arr = if is_full t then t.data else Array.sub t.data 0 t.sz in
+  Array.fast_sort f sub_arr;
+  t.data <- sub_arr
+
+let[@inline] iter f t =
+  for i = 0 to size t - 1 do
+    f (Array.unsafe_get t.data i)
+  done
+
+let[@inline] iteri f t =
+  for i = 0 to size t - 1 do
+    f i (Array.unsafe_get t.data i)
+  done
+
+let[@inline] to_seq a k = iter k a
+
+let exists p t = Iter.exists p @@ to_seq t
+let for_all p t = Iter.for_all p @@ to_seq t
+let fold f acc a = Iter.fold f acc @@ to_seq a
+let to_list a = Iter.to_list @@ to_seq a
+let to_array a = Array.sub a.data 0 a.sz
+
+let of_list l : _ t =
+  match l with
+  | [] -> create()
+  | x :: tl ->
+    let v = make (List.length tl+1) x in
+    List.iter (push v) l;
+    v
+
+let pp ?(sep=", ") pp out v =
+  let first = ref true in
+  iter
+    (fun x ->
+       if !first then first := false else Format.fprintf out "%s@," sep;
+       pp out x)
+    v

src/util/Vec.mli

@@ -0,0 +1,90 @@
+
+(** Vectors
+
+    A resizable array, workhorse of imperative programming :-).
+    This implementation originated in alt-ergo-zero but has been basically rewritten
+    from scratch several times since.
+*)
+
+type 'a t
+(** Abstract type of vectors of 'a *)
+
+val make : int -> 'a -> 'a t
+(** [make cap dummy] creates a new vector filled with [dummy]. The vector
+    is initially empty but its underlying array has capacity [cap].
+    [dummy] will stay alive as long as the vector *)
+
+val create : unit -> 'a t
+
+val to_list : 'a t -> 'a list
+(** Returns the list of elements of the vector *)
+
+val to_array : 'a t -> 'a array
+
+val of_list : 'a list -> 'a t
+
+val to_seq : 'a t -> 'a Iter.t
+
+val clear : 'a t -> unit
+(** Set size to 0, doesn't free elements *)
+
+val shrink : 'a t -> int -> unit
+(** [shrink vec sz] resets size of [vec] to [sz].
+    Assumes [sz >=0 && sz <= size vec] *)
+
+val pop : 'a t -> 'a
+(** Pop last element and return it.
+    @raise Invalid_argument if the vector is empty *)
+
+val size : 'a t -> int
+
+val is_empty : 'a t -> bool
+
+val is_full : 'a t -> bool
+(** Is the capacity of the vector equal to the number of its elements? *)
+
+val push : 'a t -> 'a -> unit
+(** Push element into the vector *)
+
+val get : 'a t -> int -> 'a
+(** get the element at the given index, or
+    @raise Invalid_argument if the index is not valid *)
+
+val set : 'a t -> int -> 'a -> unit
+(** set the element at the given index, either already set or the first
+    free slot if [not (is_full vec)], or
+    @raise Invalid_argument if the index is not valid *)
+
+val copy : 'a t -> 'a t
+(** Fresh copy *)
+
+val fast_remove : 'a t -> int -> unit
+(** Remove element at index [i] without preserving order
+    (swap with last element) *)
+
+val filter_in_place : ('a -> bool) -> 'a t -> unit
+(** [filter_in_place f v] removes from [v] the elements that do
+    not satisfy [f] *)
+
+val sort : 'a t -> ('a -> 'a -> int) -> unit
+(** Sort in place the array *)
+
+val iter : ('a -> unit) -> 'a t -> unit
+(** Iterate on elements *)
+
+val iteri : (int -> 'a -> unit) -> 'a t -> unit
+(** Iterate on elements with their index *)
+
+val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
+(** Fold over elements *)
+
+val exists : ('a -> bool) -> 'a t -> bool
+(** Does there exist an element that satisfies the predicate? *)
+
+val for_all : ('a -> bool) -> 'a t -> bool
+(** Do all elements satisfy the predicate? *)
+
+val pp :
+  ?sep:string ->
+  (Format.formatter -> 'a -> unit) ->
+  Format.formatter -> 'a t -> unit

src/util/dune

@@ -1,4 +1,4 @@
 (library
   (name sidekick_util)
   (public_name sidekick.util)
-  (libraries containers iter msat sidekick.sigs))
+  (libraries containers iter sidekick.sigs))