vendor current msat in src/sat for further modifications

2026-01-23 01:46:43 -05:00 · 2021-07-18 01:26:11 -04:00 · 2021-07-18 01:26:11 -04:00 · 1a58ab0bfc
commit 1a58ab0bfc
parent 1c2b37eb72 d024a6a3f0
48 changed files with 5799 additions and 5 deletions
--- a/.header
+++ b/.header
@ -1,5 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
--- a/src/sat/.gitignore
+++ b/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
--- a/src/sat/CHANGELOG.md
+++ b/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
+
--- a/src/sat/README.md
+++ b/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
+  
+###################
+...
+```
--- a/src/sat/dune
+++ b/src/sat/dune
@ -0,0 +1,10 @@
+
+(alias
+ (name runtest)
+ (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src))
+ (locks test)
+ (package msat)
+ (action (progn
+          (run mdx test README.md)
+          (diff? README.md README.md.corrected))))
+
--- a/src/sat/src/backend/Backend_intf.ml
+++ b/src/sat/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
+
--- a/src/sat/src/backend/Coq.ml
+++ b/src/sat/src/backend/Coq.ml
@ -0,0 +1,193 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+
+  type hyp
+  type lemma
+  type assumption
+
+  val prove_hyp : Format.formatter -> string -> hyp -> unit
+  val prove_lemma : Format.formatter -> string -> lemma -> unit
+  val prove_assumption : Format.formatter -> string -> assumption -> unit
+
+end
+
+module Make(S : Msat.S)(A : Arg with type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) = struct
+
+  module Atom = S.Atom
+  module Clause = S.Clause
+  module M = Map.Make(S.Atom)
+  module C_tbl = S.Clause.Tbl
+  module P = S.Proof
+
+  let name = Clause.name
+
+  let clause_map c =
+    let rec aux acc a i =
+      if i >= Array.length a then acc
+      else begin
+        let name = Format.sprintf "A%d" i in
+        aux (M.add a.(i) name acc) a (i + 1)
+      end
+    in
+    aux M.empty (Clause.atoms c) 0
+
+  let clause_iter m format fmt clause =
+    let aux atom = Format.fprintf fmt format (M.find atom m) in
+    Array.iter aux (Clause.atoms clause)
+
+  let elim_duplicate fmt goal hyp _ =
+    (** Printing info comment in coq *)
+    Format.fprintf fmt
+      "(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n"
+      (name goal) (name hyp);
+    (** Prove the goal: intro the atoms, then use them with the hyp *)
+    let m = clause_map goal in
+    Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %s%a) as %s@].@\n"
+      (clause_iter m "%s@ ") goal (name hyp)
+      (clause_iter m "@ %s") hyp (name goal)
+
+  let resolution_aux m a h1 h2 fmt () =
+    Format.fprintf fmt "%s%a" (name h1)
+      (fun fmt -> Array.iter (fun b ->
+           if b == a then begin
+             Format.fprintf fmt "@ (fun p =>@ %s%a)"
+               (name h2) (fun fmt -> (Array.iter (fun c ->
+                   if Atom.equal c (Atom.neg a) then
+                     Format.fprintf fmt "@ (fun np => np p)"
+                   else
+                     Format.fprintf fmt "@ %s" (M.find c m)))
+                 ) (Clause.atoms h2)
+           end else
+             Format.fprintf fmt "@ %s" (M.find b m)
+         )) (Clause.atoms h1)
+
+  let resolution fmt goal hyp1 hyp2 atom =
+    let a = Atom.abs atom in
+    let h1, h2 =
+      if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2
+      else (
+        assert (Array.exists (Atom.equal a) (Clause.atoms hyp2));
+        hyp2, hyp1
+      )
+    in
+    (** Print some debug info *)
+    Format.fprintf fmt
+      "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
+      (name goal) (name h1) (name h2);
+    (** Prove the goal: intro the axioms, then perform resolution *)
+    if Array.length (Clause.atoms goal) = 0 then (
+      let m = M.empty in
+      Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
+      false
+    ) else (
+      let m = clause_map goal in
+      Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n"
+        (clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal);
+      true
+    )
+
+  (* Count uses of hypotheses *)
+  let incr_use h c =
+    let i = try C_tbl.find h c with Not_found -> 0 in
+    C_tbl.add h c (i + 1)
+
+  let decr_use h c =
+    let i = C_tbl.find h c - 1 in
+    assert (i >= 0);
+    let () = C_tbl.add h c i in
+    i <= 0
+
+  let clear fmt c =
+    Format.fprintf fmt "clear %s." (name c)
+
+  let rec clean_aux fmt = function
+    | [] -> ()
+    | [x] ->
+      Format.fprintf fmt "%a@\n" clear x
+    | x :: ((_ :: _) as r) ->
+      Format.fprintf fmt "%a@ %a" clear x clean_aux r
+
+  let clean h fmt l =
+    match List.filter (decr_use h) l with
+    | [] -> ()
+    | l' ->
+      Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l'
+
+  let prove_node t fmt node =
+    let clause = node.P.conclusion in
+    match node.P.step with
+    | P.Hypothesis _ ->
+      A.prove_hyp fmt (name clause) clause
+    | P.Assumption ->
+      A.prove_assumption fmt (name clause) clause
+    | P.Lemma _ ->
+      A.prove_lemma fmt (name clause) clause
+    | P.Duplicate (p, l) ->
+      let c = P.conclusion p in
+      let () = elim_duplicate fmt clause c l in
+      clean t fmt [c]
+    | P.Hyper_res hr ->
+      let (p1, p2, a) = P.res_of_hyper_res hr in
+      let c1 = P.conclusion p1 in
+      let c2 = P.conclusion p2 in
+      if resolution fmt clause c1 c2 a then clean t fmt [c1; c2]
+
+  let count_uses p =
+    let h = C_tbl.create 128 in
+    let aux () node =
+      List.iter (fun p' -> incr_use h P.(conclusion p')) (P.parents node.P.step)
+    in
+    let () = P.fold aux () p in
+    h
+
+  (* Here the main idea is to always try and have exactly
+     one goal to prove, i.e False. So each  *)
+  let pp fmt p =
+    let h = count_uses p in
+    let aux () node =
+      Format.fprintf fmt "%a" (prove_node h) node
+    in
+    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
+    P.fold aux () p
+end
+
+
+module Simple(S : Msat.S)
+    (A : Arg with type hyp = S.formula list
+              and type lemma := S.lemma
+              and type assumption := S.formula) =
+  Make(S)(struct
+    module P = S.Proof
+
+    (* Some helpers *)
+    let lit = S.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
+
+    let prove_hyp fmt name c =
+      A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c))
+
+    let prove_lemma fmt name c =
+      A.prove_lemma fmt name (get_lemma c)
+
+    let prove_assumption fmt name c =
+      A.prove_assumption fmt name (lit (get_assumption c))
+
+  end)
+
--- a/src/sat/src/backend/Coq.mli
+++ b/src/sat/src/backend/Coq.mli
@ -0,0 +1,46 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+(** Coq Backend
+
+    This module provides an easy way to produce coq scripts
+    corresponding to the resolution proofs output by the
+    sat solver. *)
+
+module type S = Backend_intf.S
+(** Interface for exporting proofs. *)
+
+module type Arg = sig
+  (** Term printing for Coq *)
+
+  type hyp
+  type lemma
+  type assumption
+  (** The types of hypotheses, lemmas, and assumptions *)
+
+  val prove_hyp : Format.formatter -> string -> hyp -> unit
+  val prove_lemma : Format.formatter -> string -> lemma -> unit
+  val prove_assumption : Format.formatter -> string -> assumption -> unit
+  (** Proving function for hypotheses, lemmas and assumptions.
+      [prove_x fmt name x] should prove [x], and be such that after
+      executing it, [x] is among the coq hypotheses under the name [name].
+      The hypothesis should be the encoding of the given clause, i.e
+      for a clause [a \/ not b \/ c], the proved hypothesis should be:
+      [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the
+      one in the atoms array of the clause. *)
+
+end
+
+module Make(S : Msat.S)(A : Arg with type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) : S with type t := S.proof
+(** Base functor to output Coq proofs *)
+
+
+module Simple(S : Msat.S)(A : Arg with type hyp = S.formula list
+                                  and type lemma := S.lemma
+                                  and type assumption := S.formula) : S with type t := S.proof
+(** Simple functor to output Coq proofs *)
+
--- a/src/sat/src/backend/Dedukti.ml
+++ b/src/sat/src/backend/Dedukti.ml
@ -0,0 +1,62 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+
+  type proof
+  type lemma
+  type formula
+
+  val pp : Format.formatter -> formula -> unit
+  val prove : Format.formatter -> lemma -> unit
+  val context : Format.formatter -> proof -> unit
+end
+
+module Make(S : Msat.S)(A : Arg with type formula := S.formula
+                                and type lemma := S.lemma
+                                and type proof := S.proof) = struct
+  module P = S.Proof
+
+  let pp_nl fmt = Format.fprintf fmt "@\n"
+  let fprintf fmt format = Format.kfprintf pp_nl fmt format
+
+  let _clause_name = S.Clause.name
+
+  let _pp_clause fmt c =
+    let rec aux fmt = function
+      | [] -> ()
+      | a :: r ->
+        let f, pos =
+          if S.Atom.sign a then
+            S.Atom.formula a, true
+          else
+            S.Atom.formula (S.Atom.neg a), false
+        in
+        fprintf fmt "%s _b %a ->@ %a"
+          (if pos then "_pos" else "_neg") A.pp f aux r
+    in
+    fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c)
+
+  let context fmt p =
+    fprintf fmt "(; Embedding ;)";
+    fprintf fmt "Prop : Type.";
+    fprintf fmt "_proof : Prop -> Type.";
+    fprintf fmt "(; Notations for clauses ;)";
+    fprintf fmt "_pos : Prop -> Prop -> Type.";
+    fprintf fmt "_neg : Prop -> Prop -> Type.";
+    fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
+    fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b.";
+    A.context fmt p
+
+  let pp fmt p =
+    fprintf fmt "#NAME Proof.";
+    fprintf fmt "(; Dedukti file automatically generated by mSAT ;)";
+    context fmt p;
+    ()
+
+end
+
--- a/src/sat/src/backend/Dedukti.mli
+++ b/src/sat/src/backend/Dedukti.mli
@ -0,0 +1,32 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Deduki backend for proofs
+
+    Work in progress...
+*)
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+
+  type lemma
+  type proof
+  type formula
+
+  val pp : Format.formatter -> formula -> unit
+  val prove : Format.formatter -> lemma -> unit
+  val context : Format.formatter -> proof -> unit
+end
+
+module Make :
+  functor(S : Msat.S) ->
+  functor(A : Arg
+          with type formula := S.formula
+           and type lemma := S.lemma
+           and type proof := S.proof) ->
+    S with type t := S.proof
+(** Functor to generate a backend to output proofs for the dedukti type checker. *)
--- a/src/sat/src/backend/Dot.ml
+++ b/src/sat/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 : Msat.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.name c]
+
+  let lemma_info c =
+    "lemma", Some "BLUE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+
+  let assumption_info c =
+    "assumption", Some "PURPLE",
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+
+end
+
+(** Functor to provide dot printing *)
+module Make(S : Msat.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.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 : Msat.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)
+
--- a/src/sat/src/backend/Dot.mli
+++ b/src/sat/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 : Msat.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 : Msat.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
+(** Functor for making a module to export proofs to the DOT format. *)
+
+module Simple(S : Msat.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
+(** 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. *)
+
--- a/src/sat/src/backend/dune
+++ b/src/sat/src/backend/dune
@ -0,0 +1,10 @@
+(library
+  (name msat_backend)
+  (public_name msat.backend)
+  (synopsis "proof backends for msat")
+  (libraries msat)
+  (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -warn-error -27 -color always -safe-string)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+  )
+
--- a/src/sat/src/backtrack/Backtrackable_ref.ml
+++ b/src/sat/src/backtrack/Backtrackable_ref.ml
@ -0,0 +1,29 @@
+
+type 'a t = {
+  mutable cur: 'a;
+  stack: 'a Vec.t;
+  copy: ('a -> 'a) option;
+}
+
+let create ?copy x: _ t =
+  {cur=x; stack=Vec.create(); copy}
+
+let[@inline] get self = self.cur
+let[@inline] set self x = self.cur <- x
+let[@inline] update self f = self.cur <- f self.cur
+
+let[@inline] n_levels self = Vec.size self.stack
+
+let[@inline] push_level self : unit =
+  let x = self.cur in
+  let x = match self.copy with None -> x | Some f -> f x in
+  Vec.push self.stack x
+
+let pop_levels self n : unit =
+  assert (n>=0);
+  if n > Vec.size self.stack then invalid_arg "Backtrackable_ref.pop_levels";
+  let i = Vec.size self.stack-n in
+  let x = Vec.get self.stack i in
+  self.cur <- x;
+  Vec.shrink self.stack i;
+  ()
--- a/src/sat/src/backtrack/Backtrackable_ref.mli
+++ b/src/sat/src/backtrack/Backtrackable_ref.mli
@ -0,0 +1,30 @@
+
+(** {1 Backtrackable ref} *)
+
+type 'a t
+
+val create : ?copy:('a -> 'a) -> 'a -> 'a t
+(** Create a backtrackable reference holding the given value initially.
+    @param copy if provided, will be used to copy the value when [push_level]
+    is called. *)
+
+val set : 'a t -> 'a -> unit
+(** Set the reference's current content *)
+
+val get : 'a t -> 'a
+(** Get the reference's current content *)
+
+val update : 'a t -> ('a -> 'a) -> unit
+(** Update the reference's current content *)
+  
+val push_level : _ t -> unit
+(** Push a backtracking level, copying the current value on top of some
+    stack. The [copy] function will be used if it was provided in {!create}. *)
+
+val n_levels : _ t -> int
+(** Number of saved values *)
+
+val pop_levels : _ t -> int -> unit
+(** Pop [n] levels, restoring to the value the reference was storing [n] calls
+    to [push_level] earlier.
+    @raise Invalid_argument if [n] is bigger than [n_levels]. *)
--- a/src/sat/src/backtrack/Msat_backtrack.ml
+++ b/src/sat/src/backtrack/Msat_backtrack.ml
@ -0,0 +1,2 @@
+
+module Ref = Backtrackable_ref
--- a/src/sat/src/backtrack/dune
+++ b/src/sat/src/backtrack/dune
@ -0,0 +1,11 @@
+
+(library
+  (name msat_backtrack)
+  (public_name msat.backtrack)
+  (libraries msat)
+  (synopsis "backtrackable data structures for msat")
+  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8
+         -color always -safe-string -open Msat)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+  )
--- a/src/sat/src/core/Heap.ml
+++ b/src/sat/src/core/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]
--- a/src/sat/src/core/Heap.mli
+++ b/src/sat/src/core/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
--- a/src/sat/src/core/Heap_intf.ml
+++ b/src/sat/src/core/Heap_intf.ml
@ -0,0 +1,46 @@
+
+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
--- a/src/sat/src/core/Internal.ml
+++ b/src/sat/src/core/Internal.ml
--- a/src/sat/src/core/Log.ml
+++ b/src/sat/src/core/Log.ml
@ -0,0 +1,33 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** {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)
--- a/src/sat/src/core/Log.mli
+++ b/src/sat/src/core/Log.mli
@ -0,0 +1,26 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** {1 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. *)
+
--- a/src/sat/src/core/Msat.ml
+++ b/src/sat/src/core/Msat.ml
@ -0,0 +1,76 @@
+(** Main API *)
+
+
+module Solver_intf = Solver_intf
+
+module type S = Solver_intf.S
+module type FORMULA = Solver_intf.FORMULA
+module type EXPR = Solver_intf.EXPR
+module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
+module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT
+module type PROOF = Solver_intf.PROOF
+
+(** Empty type *)
+type void = (unit,bool) Solver_intf.gadt_eq
+
+type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
+
+type ('term, 'form, 'value) sat_state = ('term, 'form, 'value) Solver_intf.sat_state = {
+  eval : 'form -> bool;
+  eval_level : 'form -> bool * int;
+  iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
+  model : unit -> ('term * 'value) list;
+}
+
+type ('atom,'clause, 'proof) unsat_state = ('atom,'clause, 'proof) Solver_intf.unsat_state = {
+  unsat_conflict : unit -> 'clause;
+  get_proof : unit -> 'proof;
+  unsat_assumptions: unit -> 'atom list;
+}
+type 'clause export = 'clause Solver_intf.export = {
+  hyps : 'clause Vec.t;
+  history : 'clause Vec.t;
+}
+
+type ('term, 'formula, 'value) assumption = ('term, 'formula, 'value) Solver_intf.assumption =
+  | Lit of 'formula  (** The given formula is asserted true by the solver *)
+  | Assign of 'term * 'value (** The term is assigned to the value *)
+
+type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason =
+  | Eval of 'term list
+  | Consequence of (unit -> 'formula list * 'proof)
+
+type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) Solver_intf.acts = {
+  acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
+  acts_eval_lit: 'formula -> lbool;
+  acts_mk_lit: ?default_pol:bool -> 'formula -> unit;
+  acts_mk_term: 'term -> unit;
+  acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit;
+  acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b;
+  acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
+  acts_add_decision_lit: 'formula -> bool -> unit;
+}
+
+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 Make_mcsat = Solver.Make_mcsat
+module Make_cdcl_t = Solver.Make_cdcl_t
+module Make_pure_sat = Solver.Make_pure_sat
+
+(**/**)
+module Vec = Vec
+module Log = Log
+(**/**)
--- a/src/sat/src/core/Solver.ml
+++ b/src/sat/src/core/Solver.ml
@ -0,0 +1,12 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
+
+module type S = Solver_intf.S
+
+module Make_cdcl_t = Internal.Make_cdcl_t
+module Make_mcsat = Internal.Make_mcsat
+module Make_pure_sat = Internal.Make_pure_sat
+
--- a/src/sat/src/core/Solver.mli
+++ b/src/sat/src/core/Solver.mli
@ -0,0 +1,34 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** mSAT safe interface
+
+    This module defines a safe interface for the core solver.
+    It is the basis of the {!module:Solver} and {!module:Mcsolver} modules.
+*)
+
+module type S = Solver_intf.S
+(** Safe external interface of solvers. *)
+
+module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
+  : S with type Term.t = Solver_intf.void
+       and module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = Th.t
+
+module Make_mcsat(Th : Solver_intf.PLUGIN_MCSAT)
+  : S with module Term = Th.Term
+       and module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = Th.t
+
+module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
+  : S with type Term.t = Solver_intf.void
+       and module Formula = Th.Formula
+       and type lemma = Th.proof
+       and type theory = unit
+
+
--- a/src/sat/src/core/Solver_intf.ml
+++ b/src/sat/src/core/Solver_intf.ml
@ -0,0 +1,514 @@
+(*
+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
+
+type ('term, 'form, 'value) sat_state = {
+  eval: 'form -> bool;
+  (** Returns the valuation of a formula in the current state
+      of the sat solver.
+      @raise UndecidedLit if the literal is not decided *)
+  eval_level: 'form -> 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 *)
+  iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
+  (** Iter thorugh the formulas and terms in order of decision/propagation
+      (starting from the first propagation, to the last propagation). *)
+  model: unit -> ('term * 'value) list;
+  (** Returns the model found if the formula is satisfiable. *)
+}
+(** The type of values returned when the solver reaches a SAT state. *)
+
+type ('atom, 'clause, 'proof) unsat_state = {
+  unsat_conflict : unit -> 'clause;
+  (** Returns the unsat clause found at the toplevel *)
+  get_proof : unit -> 'proof;
+  (** returns a persistent proof of the empty clause from the Unsat result. *)
+  unsat_assumptions: unit -> 'atom list;
+  (** Subset of assumptions responsible for "unsat" *)
+}
+(** The type of values returned when the solver reaches an UNSAT state. *)
+
+type 'clause export = {
+  hyps: 'clause Vec.t;
+  history: 'clause Vec.t;
+}
+(** Export internal 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 'term eval_res =
+  | Unknown                       (** The given formula does not have an evaluation *)
+  | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool.
+                                      The list of terms to give is the list of terms that
+                                      were effectively used for the evaluation. *)
+(** The type of evaluation results for a given formula.
+    For instance, let's suppose we want to evaluate the formula [x * y = 0], the
+    following result are correct:
+    - [Unknown] if neither [x] nor [y] are assigned to a value
+    - [Valued (true, [x])] if [x] is assigned to [0]
+    - [Valued (true, [y])] if [y] is assigned to [0]
+    - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
+*)
+
+type ('term, 'formula, 'value) assumption =
+  | Lit of 'formula  (** The given formula is asserted true by the solver *)
+  | Assign of 'term * 'value (** The term is assigned to the value *)
+(** Asusmptions made by the core SAT solver. *)
+
+type ('term, 'formula, 'proof) reason =
+  | Eval of 'term list
+  (** The formula can be evalutaed using the terms in the list *)
+  | Consequence of (unit -> 'formula list * 'proof)
+  (** [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 *)
+
+(* TODO: find a way to use atoms instead of formulas here *)
+type ('term, 'formula, 'value, 'proof) acts = {
+  acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit;
+  (** Traverse the new assumptions on the boolean trail. *)
+
+  acts_eval_lit: 'formula -> lbool;
+  (** Obtain current value of the given literal *)
+
+  acts_mk_lit: ?default_pol:bool -> 'formula -> unit;
+  (** Map the given formula to a literal, which will be decided by the
+      SAT solver. *)
+
+  acts_mk_term: 'term -> unit;
+  (** Map the given term (and its subterms) to decision variables,
+      for the MCSAT solver to decide. *)
+
+  acts_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.
+  *)
+
+  acts_raise_conflict: 'b. '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. *)
+
+  acts_propagate: 'formula -> ('term, '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} *)
+
+  acts_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. *)
+}
+(** The type for a slice of assertions to assume/propagate in the theory. *)
+
+type ('a, 'b) gadt_eq = GADT_EQ : ('a, 'a) gadt_eq
+
+type void = (unit,bool) gadt_eq
+(** A provably empty type *)
+
+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
+
+(** Formulas and Terms required for mcSAT *)
+module type EXPR = sig
+  type proof
+  (** An abstract type for proofs *)
+
+  module Term : sig
+    type t
+    (** The type of terms *)
+
+    val equal : t -> t -> bool
+    (** Equality over terms. *)
+
+    val hash : t -> int
+    (** Hashing function for terms. Should be such that two terms equal according
+        to {!equal} have the same hash. *)
+
+    val pp : t printer
+    (** Printing function used among other for debugging. *)
+  end
+
+  module Value : sig
+    type t
+    (** The type of semantic values (domain elements) *)
+
+    val pp : t printer
+    (** Printing function used among other for debugging. *)
+  end
+
+  module Formula : FORMULA
+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 -> (void, Formula.t, void, 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 -> (void, Formula.t, void, 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 theories to be given to the Model Constructing Solver. *)
+module type PLUGIN_MCSAT = sig
+  type t
+  (** The plugin state itself *)
+
+  include EXPR
+
+  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 -> (Term.t, Formula.t, Value.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 -> (Term.t, Formula.t, Value.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. *)
+
+  val assign : t -> Term.t -> Value.t
+  (** Returns an assignment value for the given term. *)
+
+  val iter_assignable : t -> (Term.t -> unit) -> Formula.t -> unit
+  (** An iterator over the subTerm.ts of a Formula.t that should be assigned a value (usually the poure subTerm.ts) *)
+
+  val eval : t -> Formula.t -> Term.t eval_res
+  (** Returns the evaluation of the Formula.t in the current assignment *)
+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. *)
+
+  include EXPR
+
+  type term = Term.t (** user terms *)
+
+  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
+
+  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 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
+     and type t = proof
+  (** 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 (term,formula,Value.t) 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_term : t -> term -> unit
+  (** Add a new term (i.e. decision variable) to the solver. This term will
+      be decided on at some point during solving, wether it appears
+      in clauses or not. *)
+
+  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 *)
+
+  val export : t -> clause export
+end
+
--- a/src/sat/src/core/Vec.ml
+++ b/src/sat/src/core/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
--- a/src/sat/src/core/Vec.mli
+++ b/src/sat/src/core/Vec.mli
@ -0,0 +1,83 @@
+
+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
--- a/src/sat/src/core/dune
+++ b/src/sat/src/core/dune
@ -0,0 +1,10 @@
+
+(library
+  (name msat)
+  (public_name msat)
+  (libraries iter)
+  (synopsis "core data structures and algorithms for msat")
+  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+  )
--- a/src/sat/src/core/msat.mld
+++ b/src/sat/src/core/msat.mld
@ -0,0 +1,92 @@
+{1 mSAT}
+
+{2 License}
+
+This code is free, under the {{:https://github.com/Gbury/mSAT/blob/master/LICENSE}Apache 2.0 license}.
+
+{2 Contents}
+
+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
+of a sat solver does not need much information about either the exact representation
+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}
+
+The following modules allow to easily create a SAT or SMT solver (remark: a SAT solver is
+simply an SMT solver with an empty theory).
+
+{!modules:
+Msat
+}
+
+The following modules allow the creation of a McSat solver (Model Constructing solver):
+
+{!modules:
+Msat_mcsolver
+}
+
+{4 Useful tools}
+
+An instanciation of a pure sat solver is also provided:
+
+{!modules:
+Msat_sat
+}
+
+Lastly, mSAT also provides an implementation of Tseitin's CNF conversion:
+
+{!modules:
+Msat_tseitin
+}
+
+{4 Proof Management}
+
+mSAT solvers are able to provide detailed proofs when an unsat state is reached. To do
+so, it require the provided theory to give proofs of the tautologies it gives the solver.
+These proofs will be called lemmas. The type of lemmas is defined by the theory and can
+very well be [unit].
+
+In this context a proof is a resolution tree, whose conclusion (i.e. root) is the
+empty clause, effectively allowing to deduce [false] from the hypotheses.
+A resolution tree is a binary tree whose nodes are clauses. Inner nodes' clauses are
+obtained by performing resolution between the two clauses of the children nodes, while
+leafs of the tree are either hypotheses, or tautologies (i.e. conflicts returned by
+the theory).
+
+{!modules:
+Msat__Res
+Msat__Res_intf
+}
+
+Backends for exporting proofs to different formats:
+
+{!modules:
+Dot
+Coq
+Dedukti
+Backend_intf
+}
+
+{4 Internal modules}
+
+WARNING: for advanced users only ! These modules expose a lot of unsafe functions
+that must be used with care to not break the required invariants. Additionally, these
+interfaces are not part of the main API and so are subject to a lot more breaking changes
+than the safe modules above.
+
+{!modules:
+Dimacs
+Internal
+External
+Solver_types
+Solver_types_intf
+}
+
+{2 Index}
+
+{!indexlist}
--- a/src/sat/src/dune
+++ b/src/sat/src/dune
@ -0,0 +1,4 @@
+
+(documentation
+  (package msat)
+  (mld_files :standard))
--- a/src/sat/src/index.mld
+++ b/src/sat/src/index.mld
@ -0,0 +1,121 @@
+
+
+{1 mSAT: a Modular SAT Solver}
+
+(The entry point of this library is the module: {!module-Msat}.)
+
+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)
+
+{3 Sat Solver}
+
+A ready-to-use SAT solver is available in the {!Msat_sat} module
+using the [msat.sat] library (see {!module-Msat_sat}). It can be loaded
+as shown in the following code :
+
+{[
+# #require "msat";;
+# #require "msat.sat";;
+# #print_depth 0;; (* do not print details *)
+]}
+
+Then we can create a solver and create some boolean variables:
+
+{[
+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".
+
+{[
+# 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".
+
+{[
+# Sat.assume solver [[E.neg a]; [E.neg b]] () ;;
+- : unit = ()
+# let res = Sat.solve solver ;;
+val res : Sat.res = Sat.Unsat ...
+]}
+
+{3 Formulas API}
+
+Writing clauses by hand can be tedious and error-prone.
+The functor {!Msat_tseitin.Make} in the library [msat.tseitin] (see {!module-Msat_tseitin}).
+proposes a formula AST (parametrized by
+atoms) and a function to convert these formulas into clauses:
+
+{[
+# #require "msat.tseitin";;
+]}
+
+{[
+(* 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`:
+
+{[
+# Sat.assume solver (F.make_cnf r) ();;
+- : unit = ()
+# Sat.solve solver;;
+- : Sat.res = Sat.Sat ...
+]}
+
+{[
+# Sat.assume solver (F.make_cnf s) ();;
+- : unit = ()
+# Sat.solve solver ;;
+- : Sat.res = Sat.Unsat ...
+]}
+
+{3 Backtracking utils}
+
+The library {!module-Msat_backtrack} contains some backtrackable
+data structures that are useful for implementing theories.
+
+{3 Library msat.backend}
+
+This is used for proof backends:
+
+The entry point of this library is the module:
+{!module-Msat_backend}.
--- a/src/sat/src/main/Dimacs_lex.mll
+++ b/src/sat/src/main/Dimacs_lex.mll
@ -0,0 +1,20 @@
+{
+  open Dimacs_parse
+}
+
+let number = ['1' - '9'] ['0' - '9']*
+
+rule token = parse
+  | eof                     { EOF }
+  | "c"                     { comment lexbuf }
+  | [' ' '\t' '\r']         { token lexbuf }
+  | 'p'                     { P }
+  | "cnf"                   { CNF }
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | '0'                     { ZERO }
+  | '-'? number             { LIT (int_of_string (Lexing.lexeme lexbuf)) }
+  | _                       { failwith @@ Printf.sprintf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
+
+and comment = parse
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | [^'\n']                 { comment lexbuf }
--- a/src/sat/src/main/Dimacs_parse.mly
+++ b/src/sat/src/main/Dimacs_parse.mly
@ -0,0 +1,34 @@
+/*  Copyright 2005 INRIA  */
+
+%{
+  let lnum pos = pos.Lexing.pos_lnum
+  let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol
+  let pp_pos out (start,stop) =
+    Format.fprintf out "(at %d:%d - %d:%d)"
+      (lnum start) (cnum start) (lnum stop) (cnum stop)
+%}
+
+%token <int> LIT
+%token ZERO
+%token P CNF EOF
+
+%start file
+%type <int list list> file
+
+%%
+
+/* DIMACS syntax */
+
+prelude:
+  | P CNF LIT LIT { () }
+
+clauses:
+  | { [] }
+  | clause clauses { $1 :: $2 }
+
+file:
+  | prelude clauses EOF { $2 }
+
+clause:
+  | ZERO { [] }
+  | LIT clause { $1 :: $2 }
--- a/src/sat/src/main/dune
+++ b/src/sat/src/main/dune
@ -0,0 +1,14 @@
+
+; main binary
+(executable
+  (name main)
+  (public_name msat)
+  (package msat-bin)
+  (libraries containers camlzip msat msat.sat msat.backend)
+  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
+  (ocamlopt_flags :standard -O3 -color always
+                  -unbox-closures -unbox-closures-factor 20)
+  )
+
+(ocamlyacc (modules Dimacs_parse))
+(ocamllex (modules Dimacs_lex))
--- a/src/sat/src/main/main.ml
+++ b/src/sat/src/main/main.ml
@ -0,0 +1,186 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+exception Incorrect_model
+exception Out_of_time
+exception Out_of_space
+
+let file = ref ""
+let p_cnf = ref false
+let p_check = ref false
+let p_dot_proof = ref ""
+let p_proof_print = ref false
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
+let no_proof = ref false
+
+module S = Msat_sat
+
+module Process() = struct
+  module D = Msat_backend.Dot.Make(S)(Msat_backend.Dot.Default(S))
+
+  let hyps = ref []
+
+  let st = S.create ~store_proof:(not !no_proof) ~size:`Big ()
+
+  let check_model sat =
+    let check_clause c =
+      let l = List.map (function a ->
+          Log.debugf 99
+            (fun k -> k "Checking value of %a" S.Formula.pp a);
+          sat.Msat.eval a) c in
+      List.exists (fun x -> x) l
+    in
+    let l = List.map check_clause !hyps in
+    List.for_all (fun x -> x) l
+
+  let prove ~assumptions () =
+    let res = S.solve ~assumptions st in
+    let t = Sys.time () in
+    begin match res with
+      | S.Sat state ->
+        if !p_check then
+          if not (check_model state) then
+            raise Incorrect_model;
+        let t' = Sys.time () -. t in
+        Format.printf "Sat (%f/%f)@." t t'
+      | S.Unsat state ->
+        if !p_check then (
+          let p = state.Msat.get_proof () in
+          S.Proof.check_empty_conclusion p;
+          S.Proof.check p;
+          if !p_dot_proof <> "" then (
+            let oc = open_out !p_dot_proof in
+            let fmt = Format.formatter_of_out_channel oc in
+            Format.fprintf fmt "%a@?" D.pp p;
+            flush oc; close_out_noerr oc;
+          )
+        );
+        let t' = Sys.time () -. t in
+        Format.printf "Unsat (%f/%f)@." t t'
+    end
+
+  let conv_c c = List.rev_map S.Int_lit.make c
+
+  let add_clauses cs =
+    S.assume st (CCList.map conv_c cs) ()
+end[@@inline]
+
+let parse_file f =
+  let module L = Lexing in
+  CCIO.with_in f
+    (fun ic ->
+       let buf =
+         if CCString.suffix ~suf:".gz" f
+         then (
+           let gic = Gzip.open_in_chan ic in
+           L.from_function (fun bytes len -> Gzip.input gic bytes 0 len)
+         ) else L.from_channel ic
+       in
+       buf.L.lex_curr_p <- {buf.L.lex_curr_p with L.pos_fname=f;};
+       Dimacs_parse.file Dimacs_lex.token buf)
+
+let error_msg opt arg l =
+  Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
+    arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
+  Format.flush_str_formatter ()
+
+(* Arguments parsing *)
+let int_arg r arg =
+  let l = String.length arg in
+  let multiplier m =
+    let arg1 = String.sub arg 0 (l-1) in
+    r := m *. (float_of_string arg1)
+  in
+  if l = 0 then raise (Arg.Bad "bad numeric argument")
+  else
+    try
+      match arg.[l-1] with
+      | 'k' -> multiplier 1e3
+      | 'M' -> multiplier 1e6
+      | 'G' -> multiplier 1e9
+      | 'T' -> multiplier 1e12
+      | 's' -> multiplier 1.
+      | 'm' -> multiplier 60.
+      | 'h' -> multiplier 3600.
+      | 'd' -> multiplier 86400.
+      | '0'..'9' -> r := float_of_string arg
+      | _ -> raise (Arg.Bad "bad numeric argument")
+    with Failure _ -> raise (Arg.Bad "bad numeric argument")
+
+let setup_gc_stat () =
+  at_exit (fun () ->
+      Gc.print_stat stdout;
+    )
+
+let input_file = fun s -> file := s
+
+let usage = "Usage : main [options] <file>"
+let argspec = Arg.align [
+    "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true),
+    " Enable stack traces";
+    "-cnf", Arg.Set p_cnf,
+    " Prints the cnf used.";
+    "-check", Arg.Set p_check,
+    " Build, check and print the proof (if output is set), if unsat";
+    "-dot", Arg.Set_string p_dot_proof,
+    " If provided, print the dot proof in the given file";
+    "-gc", Arg.Unit setup_gc_stat,
+    " Outputs statistics about the GC";
+    "-size", Arg.String (int_arg size_limit),
+    "<s>[kMGT] Sets the size limit for the sat solver";
+    "-time", Arg.String (int_arg time_limit),
+    "<t>[smhd] Sets the time limit for the sat solver";
+    "-v", Arg.Int (fun i -> Log.set_debug i),
+    "<lvl> Sets the debug verbose level";
+    "-no-proof", Arg.Set no_proof, " disable proof logging";
+  ]
+
+(* Limits alarm *)
+let check () =
+  let t = Sys.time () in
+  let heap_size = (Gc.quick_stat ()).Gc.heap_words in
+  let s = float heap_size *. float Sys.word_size /. 8. in
+  if t > !time_limit then
+    raise Out_of_time
+  else if s > !size_limit then
+    raise Out_of_space
+
+let main () =
+  (* Administrative duties *)
+  Arg.parse argspec input_file usage;
+  if !file = "" then (
+    Arg.usage argspec usage;
+    exit 2
+  );
+  let al = Gc.create_alarm check in
+
+  let module P = Process() in
+
+  (* Interesting stuff happening *)
+  let clauses = parse_file !file in
+  P.add_clauses clauses;
+  P.prove ~assumptions:[] ();
+  Gc.delete_alarm al;
+  ()
+
+let () =
+  try
+    main ()
+  with
+  | Out_of_time ->
+    Format.printf "Timeout@.";
+    exit 2
+  | Out_of_space ->
+    Format.printf "Spaceout@.";
+    exit 3
+  | Incorrect_model ->
+    Format.printf "Internal error : incorrect *sat* model@.";
+    exit 4
+  | S.Proof.Resolution_error msg  ->
+    Format.printf "Internal error: incorrect *unsat* proof:\n%s@." msg;
+    exit 5
+
--- a/src/sat/src/sat/Int_lit.ml
+++ b/src/sat/src/sat/Int_lit.ml
@ -0,0 +1,66 @@
+
+exception Bad_atom
+(** Exception raised if an atom cannot be created *)
+
+type t = int
+(** Atoms are represented as integers. [-i] begin the negation of [i].
+    Additionally, since we nee dot be able to create fresh atoms, we
+    use even integers for user-created atoms, and odd integers for the
+    fresh atoms. *)
+
+let max_lit = max_int
+
+(* Counters *)
+let max_index = ref 0
+let max_fresh = ref (-1)
+
+(** Internal function for creating atoms.
+    Updates the internal counters *)
+let _make i =
+  if i <> 0 && (abs i) < max_lit then begin
+    max_index := max !max_index (abs i);
+    i
+  end else
+    raise Bad_atom
+
+let to_int i = i
+
+(** *)
+let neg a = - a
+
+let norm a =
+  abs a, if a < 0 then
+    Solver_intf.Negated
+  else
+    Solver_intf.Same_sign
+
+let abs = abs
+
+let sign i = i > 0
+
+let apply_sign b i = if b then i else neg i
+
+let set_sign b i = if b then abs i else neg (abs i)
+
+let hash (a:int) = a land max_int
+let equal (a:int) b = a=b
+let compare (a:int) b = compare a b
+
+let make i = _make (2 * i)
+
+let fresh () =
+  incr max_fresh;
+  _make (2 * !max_fresh + 1)
+
+(*
+let iter: (t -> unit) -> unit = fun f ->
+  for j = 1 to !max_index do
+    f j
+  done
+*)
+
+let pp fmt a =
+  Format.fprintf fmt "%s%s%d"
+    (if a < 0 then "~" else "")
+    (if a mod 2 = 0 then "v" else "f")
+    ((abs a) / 2)
--- a/src/sat/src/sat/Int_lit.mli
+++ b/src/sat/src/sat/Int_lit.mli
@ -0,0 +1,33 @@
+
+(** {1 The module defining formulas} *)
+
+(** SAT Formulas
+
+    This modules implements formuals adequate for use in a pure SAT Solver.
+    Atomic formuals are represented using integers, that should allow
+    near optimal efficiency (both in terms of space and time).
+*)
+
+include Solver_intf.FORMULA
+(** This modules implements the requirements for implementing an SAT Solver. *)
+
+val make : int -> t
+(** Make a proposition from an integer. *)
+
+val to_int : t -> int
+
+val fresh : unit -> t
+(** Make a fresh atom *)
+
+val compare : t -> t -> int
+(** Compare atoms *)
+
+val sign : t -> bool
+(** Is the given atom positive ? *)
+
+val apply_sign : bool -> t -> t
+(** [apply_sign b] is the identity if [b] is [true], and the negation
+    function if [b] is [false]. *)
+
+val set_sign : bool -> t -> t
+(** Return the atom with the sign set. *)
--- a/src/sat/src/sat/Msat_sat.ml
+++ b/src/sat/src/sat/Msat_sat.ml
@ -0,0 +1,11 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+*)
+
+module Int_lit = Int_lit
+include Msat.Make_pure_sat(struct
+    module Formula = Int_lit
+    type proof = unit
+  end)
+
--- a/src/sat/src/sat/Msat_sat.mli
+++ b/src/sat/src/sat/Msat_sat.mli
@ -0,0 +1,19 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+*)
+
+(** Sat solver
+
+    This modules instanciates a pure sat solver using integers to represent
+    atomic propositions.
+*)
+
+module Int_lit = Int_lit
+
+include Msat.S
+  with type Formula.t = Int_lit.t
+   and type theory = unit
+   and type lemma = unit
+(** A functor that can generate as many solvers as needed. *)
+
--- a/src/sat/src/sat/dune
+++ b/src/sat/src/sat/dune
@ -0,0 +1,11 @@
+
+(library
+  (name msat_sat)
+  (public_name msat.sat)
+  (synopsis "purely boolean interface to Msat")
+  (libraries msat)
+  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
+  (ocamlopt_flags :standard -O3 -color always
+                  -unbox-closures -unbox-closures-factor 20)
+  )
+
--- a/src/sat/src/sudoku/dune
+++ b/src/sat/src/sudoku/dune
@ -0,0 +1,9 @@
+
+(executable
+  (name sudoku_solve)
+  (modes native)
+  (libraries msat msat.backtrack iter containers)
+  (flags :standard -warn-error -a -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+)
--- a/src/sat/src/sudoku/sudoku_solve.ml
+++ b/src/sat/src/sudoku/sudoku_solve.ml
@ -0,0 +1,331 @@
+
+(** {1 simple sudoku solver} *)
+
+module Fmt = CCFormat
+module Log = Msat.Log
+module Vec = Msat.Vec
+
+let errorf msg = CCFormat.kasprintf failwith msg
+
+module Cell : sig
+  type t = private int
+  val equal : t -> t -> bool
+  val neq : t -> t -> bool
+  val hash : t -> int
+  val empty : t
+  val is_empty : t -> bool
+  val is_full : t -> bool
+  val make : int -> t
+  val pp : t Fmt.printer
+end = struct
+  type t = int
+  let empty = 0
+  let[@inline] make i = assert (i >= 0 && i <= 9); i
+  let[@inline] is_empty x = x = 0
+  let[@inline] is_full x = x > 0
+  let hash = CCHash.int
+  let[@inline] equal (a:t) b = a=b
+  let[@inline] neq (a:t) b = a<>b
+  let pp out i = if i=0 then Fmt.char out '.' else Fmt.int out i
+end
+
+module Grid : sig
+  type t
+
+  val get : t -> int -> int -> Cell.t
+  val set : t -> int -> int -> Cell.t -> t
+
+  (** A set of related cells *)
+  type set = (int*int*Cell.t) Iter.t
+
+  val rows : t -> set Iter.t
+  val cols : t -> set Iter.t
+  val squares : t -> set Iter.t
+
+  val all_cells : t -> (int*int*Cell.t) Iter.t
+
+  val parse : string -> t
+  val is_full : t -> bool
+  val is_valid : t -> bool
+  val matches : pat:t -> t -> bool
+  val pp : t Fmt.printer
+end = struct
+  type t = Cell.t array
+
+  let[@inline] get (s:t) i j = s.(i*9 + j)
+
+  let[@inline] set (s:t) i j n =
+    let s' = Array.copy s in
+    s'.(i*9 + j) <- n;
+    s'
+
+  (** A set of related cells *)
+  type set = (int*int*Cell.t) Iter.t
+
+  open Iter.Infix
+
+  let all_cells (g:t) =
+    0 -- 8 >>= fun i ->
+    0 -- 8 >|= fun j -> (i,j,get g i j)
+
+  let rows (g:t) =
+    0 -- 8 >|= fun i ->
+    ( 0 -- 8 >|= fun j -> (i,j,get g i j))
+
+  let cols g =
+    0 -- 8 >|= fun j ->
+    ( 0 -- 8 >|= fun i -> (i,j,get g i j))
+
+  let squares g =
+    0 -- 2 >>= fun sq_i ->
+    0 -- 2 >|= fun sq_j ->
+    ( 0 -- 2 >>= fun off_i ->
+      0 -- 2 >|= fun off_j ->
+      let i = 3*sq_i + off_i in
+      let j = 3*sq_j + off_j in
+      (i,j,get g i j))
+
+  let is_full g = Array.for_all Cell.is_full g
+
+  let is_valid g =
+    let all_distinct (s:set) =
+      (s >|= fun (_,_,c) -> c)
+      |> Iter.diagonal
+      |> Iter.for_all (fun (c1,c2) -> Cell.neq c1 c2)
+    in
+    Iter.for_all all_distinct @@ rows g &&
+    Iter.for_all all_distinct @@ cols g &&
+    Iter.for_all all_distinct @@ squares g
+
+  let matches ~pat:g1 g2 : bool =
+    all_cells g1
+    |> Iter.filter (fun (_,_,c) -> Cell.is_full c)
+    |> Iter.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y)
+
+  let pp out g =
+    Fmt.fprintf out "@[<v>";
+    Array.iteri
+      (fun i n ->
+         Cell.pp out n;
+         if i mod 9 = 8 then Fmt.fprintf out "@,")
+      g;
+    Fmt.fprintf out "@]"
+
+  let parse (s:string) : t =
+    if String.length s < 81 then (
+      errorf "line is too short, expected 81 chars, not %d" (String.length s);
+    );
+    let a = Array.make 81 Cell.empty in
+    for i = 0 to 80 do
+      let c = String.get s i in
+      let n = if c = '.' then 0 else Char.code c - Char.code '0' in
+      if n < 0 || n > 9 then errorf "invalid char %c" c;
+      a.(i) <- Cell.make n
+    done;
+    a
+end
+
+module B_ref = Msat_backtrack.Ref
+
+module Solver : sig
+  type t
+  val create : Grid.t -> t
+  val solve : t -> Grid.t option
+end = struct
+  open Msat.Solver_intf
+
+  (* formulas *)
+  module F = struct
+    type t = bool*int*int*Cell.t
+    let equal (sign1,x1,y1,c1)(sign2,x2,y2,c2) =
+      sign1=sign2 && x1=x2 && y1=y2 && Cell.equal c1 c2
+    let hash (sign,x,y,c) = CCHash.(combine4 (bool sign)(int x)(int y)(Cell.hash c))
+    let pp out (sign,x,y,c) =
+      Fmt.fprintf out "[@[(%d,%d) %s %a@]]" x y (if sign then "=" else "!=") Cell.pp c
+    let neg (sign,x,y,c) = (not sign,x,y,c)
+    let norm ((sign,_,_,_) as f) =
+      if sign then f, Same_sign else neg f, Negated
+
+    let make sign x y (c:Cell.t) : t = (sign,x,y,c)
+  end
+
+  module Theory = struct
+    type proof = unit
+    module Formula = F
+    type t = {
+      grid: Grid.t B_ref.t;
+    }
+
+    let create g : t = {grid=B_ref.create g}
+    let[@inline] grid self : Grid.t = B_ref.get self.grid
+    let[@inline] set_grid self g : unit = B_ref.set self.grid g
+
+    let push_level self = B_ref.push_level self.grid
+    let pop_levels self n = B_ref.pop_levels self.grid n
+
+    let pp_c_ = Fmt.(list ~sep:(return "@ ∨ ")) F.pp
+    let[@inline] logs_conflict kind c : unit =
+      Log.debugf 4 (fun k->k "(@[conflict.%s@ %a@])" kind pp_c_ c)
+
+    (* check that all cells are full *)
+    let check_full_ (self:t) acts : unit =
+      Grid.all_cells (grid self)
+        (fun (x,y,c) ->
+           if Cell.is_empty c then (
+             let c =
+               CCList.init 9
+                 (fun c -> F.make true x y (Cell.make (c+1)))
+             in
+             Log.debugf 4 (fun k->k "(@[add-clause@ %a@])" pp_c_ c);
+             acts.acts_add_clause ~keep:true c ();
+           ))
+
+    (* check constraints *)
+    let check_ (self:t) acts : unit =
+      Log.debugf 4 (fun k->k "(@[sudoku.check@ @[:g %a@]@])" Grid.pp (B_ref.get self.grid));
+      let[@inline] all_diff kind f =
+        let pairs =
+          f (grid self)
+          |> Iter.flat_map
+            (fun set ->
+               set
+               |> Iter.filter (fun (_,_,c) -> Cell.is_full c)
+               |> Iter.diagonal)
+        in
+        pairs
+          (fun ((x1,y1,c1),(x2,y2,c2)) ->
+             if Cell.equal c1 c2 then (
+               assert (x1<>x2 || y1<>y2);
+               let c = [F.make false x1 y1 c1; F.make false x2 y2 c2] in
+               logs_conflict ("all-diff." ^ kind) c;
+               acts.acts_raise_conflict c ()
+             ))
+      in
+      all_diff "rows" Grid.rows;
+      all_diff "cols" Grid.cols;
+      all_diff "squares" Grid.squares;
+      ()
+
+    let trail_ (acts:_ Msat.acts) =
+      acts.acts_iter_assumptions
+      |> Iter.map
+        (function
+          | Assign _ -> assert false
+          | Lit f -> f)
+
+    (* update current grid with the given slice *)
+    let add_slice (self:t) acts : unit =
+      trail_ acts
+        (function
+          | false,_,_,_ -> ()
+          | true,x,y,c ->
+            assert (Cell.is_full c);
+            let grid = grid self in
+            let c' = Grid.get grid x y in
+            if Cell.is_empty c' then (
+              set_grid self (Grid.set grid x y c);
+            ) else if Cell.neq c c' then (
+              (* conflict: at most one value *)
+              let c = [F.make false x y c; F.make false x y c'] in
+              logs_conflict "at-most-one" c;
+              acts.acts_raise_conflict c ()
+            )
+        )
+
+    let partial_check (self:t) acts : unit =
+      Log.debugf 4
+        (fun k->k "(@[sudoku.partial-check@ :trail [@[%a@]]@])"
+            (Fmt.list F.pp) (trail_ acts |> Iter.to_list));
+      add_slice self acts;
+      check_ self acts
+
+    let final_check (self:t) acts : unit =
+      Log.debugf 4 (fun k->k "(@[sudoku.final-check@])");
+      check_full_ self acts;
+      check_ self acts
+
+  end
+
+  module S = Msat.Make_cdcl_t(Theory)
+
+  type t = {
+    grid0: Grid.t;
+    solver: S.t;
+  }
+
+  let solve (self:t) : _ option =
+    let assumptions =
+      Grid.all_cells self.grid0
+      |> Iter.filter (fun (_,_,c) -> Cell.is_full c)
+      |> Iter.map (fun (x,y,c) -> F.make true x y c)
+      |> Iter.map (S.make_atom self.solver)
+      |> Iter.to_rev_list
+    in
+    Log.debugf 2
+      (fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions);
+    let r =
+      match S.solve self.solver ~assumptions with
+      | S.Sat _ -> Some (Theory.grid (S.theory self.solver))
+      | S.Unsat _ -> None
+    in
+    (* TODO: print some stats *)
+    r
+
+  let create g : t =
+    { solver=S.create ~store_proof:false (Theory.create g); grid0=g }
+end
+
+let solve_grid (g:Grid.t) : Grid.t option =
+  let s = Solver.create g in
+  Solver.solve s
+
+let solve_file file =
+  Format.printf "solve grids in file %S@." file;
+  let start = Sys.time() in
+  let grids =
+    CCIO.with_in file CCIO.read_lines_l
+    |> CCList.filter_map
+      (fun s ->
+         let s = String.trim s in
+         if s="" then None
+         else match Grid.parse s with
+           | g -> Some g
+           | exception e ->
+             errorf "cannot parse sudoku %S: %s@." s (Printexc.to_string e))
+  in
+  Format.printf "parsed %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start);
+  List.iter
+    (fun g ->
+       Format.printf "@[<v>@,#########################@,@[<2>solve grid:@ %a@]@]@." Grid.pp g;
+       let start=Sys.time() in
+       match solve_grid g with
+       | None -> Format.printf "no solution (in %.3fs)@." (Sys.time()-.start)
+       | Some g' when not @@ Grid.is_full g' ->
+         errorf "grid %a@ is not full" Grid.pp g'
+       | Some g' when not @@ Grid.is_valid g' ->
+         errorf "grid %a@ is not valid" Grid.pp g'
+       | Some g' when not @@ Grid.matches ~pat:g g' ->
+         errorf "grid %a@ @[<2>does not match original@ %a@]" Grid.pp g' Grid.pp g
+       | Some g' ->
+         Format.printf "@[<v>@[<2>solution (in %.3fs):@ %a@]@,###################@]@."
+           (Sys.time()-.start) Grid.pp g')
+    grids;
+  Format.printf "@.solved %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start);
+  ()
+
+let () =
+  Fmt.set_color_default true;
+  let files = ref [] in
+  let debug = ref 0 in
+  let opts = [
+    "--debug", Arg.Set_int debug, " debug";
+    "-d", Arg.Set_int debug, " debug";
+  ] |> Arg.align in
+  Arg.parse opts (fun f -> files := f :: !files) "sudoku_solve [options] <file>";
+  Msat.Log.set_debug !debug;
+  try
+    List.iter (fun f -> solve_file f) !files;
+  with
+  | Failure msg | Invalid_argument msg ->
+    Format.printf "@{<Red>Error@}:@.%s@." msg;
+    exit 1
--- a/src/sat/src/tseitin/Msat_tseitin.ml
+++ b/src/sat/src/tseitin/Msat_tseitin.ml
@ -0,0 +1,326 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                          Alt-Ergo Zero                                 *)
+(*                                                                        *)
+(*                  Sylvain Conchon and Alain Mebsout                     *)
+(*                      Universite Paris-Sud 11                           *)
+(*                                                                        *)
+(*  Copyright 2011. This file is distributed under the terms of the       *)
+(*  Apache Software License version 2.0                                   *)
+(*                                                                        *)
+(**************************************************************************)
+
+module type Arg = Tseitin_intf.Arg
+
+module type S = Tseitin_intf.S
+
+module Make (F : Tseitin_intf.Arg) = struct
+
+  exception Empty_Or
+  type combinator = And | Or | Imp | Not
+
+  type atom = F.t
+  type t =
+    | True
+    | Lit of atom
+    | Comb of combinator * t list
+
+  let rec pp fmt phi =
+    match phi with
+    | True -> Format.fprintf fmt "true"
+    | Lit a -> F.pp fmt a
+    | Comb (Not, [f]) ->
+      Format.fprintf fmt "not (%a)" pp f
+    | Comb (And, l) -> Format.fprintf fmt "(%a)" (pp_list "and") l
+    | Comb (Or, l) ->  Format.fprintf fmt "(%a)" (pp_list "or") l
+    | Comb (Imp, [f1; f2]) ->
+      Format.fprintf fmt "(%a => %a)" pp f1 pp f2
+    | _ -> assert false
+  and pp_list sep fmt = function
+    | [] -> ()
+    | [f] -> pp fmt f
+    | f::l -> Format.fprintf fmt "%a %s %a" pp f sep (pp_list sep) l
+
+  let make comb l = Comb (comb, l)
+
+  let make_atom p = Lit p
+
+  let f_true = True
+  let f_false = Comb(Not, [True])
+
+  let rec flatten comb acc = function
+    | [] -> acc
+    | (Comb (c, l)) :: r when c = comb ->
+      flatten comb (List.rev_append l acc) r
+    | a :: r ->
+      flatten comb (a :: acc) r
+
+  let rec opt_rev_map f acc = function
+    | [] -> acc
+    | a :: r -> begin match f a with
+        | None -> opt_rev_map f acc r
+        | Some b -> opt_rev_map f (b :: acc) r
+      end
+
+  let remove_true l =
+    let aux = function
+      | True -> None
+      | f -> Some f
+    in
+    opt_rev_map aux [] l
+
+  let remove_false l =
+    let aux = function
+      | Comb(Not, [True]) -> None
+      | f -> Some f
+    in
+    opt_rev_map aux [] l
+
+
+  let make_not f = make Not [f]
+
+  let make_and l =
+    let l' = remove_true (flatten And [] l) in
+    if List.exists ((=) f_false) l' then
+      f_false
+    else
+      make And l'
+
+  let make_or l =
+    let l' = remove_false (flatten Or [] l) in
+    if List.exists ((=) f_true) l' then
+      f_true
+    else match l' with
+      | [] -> raise Empty_Or
+      | [a] -> a
+      | _ -> Comb (Or, l')
+
+  let make_imply f1 f2 = make Imp [f1; f2]
+  let make_equiv f1 f2 = make_and [ make_imply f1 f2; make_imply f2 f1]
+  let make_xor f1 f2 = make_or [ make_and [ make_not f1; f2 ];
+                                 make_and [ f1; make_not f2 ] ]
+
+  (* simplify formula *)
+  let (%%) f g x = f (g x)
+
+  let rec sform f k = match f with
+    | True | Comb (Not, [True]) -> k f
+    | Comb (Not, [Lit a]) -> k (Lit (F.neg a))
+    | Comb (Not, [Comb (Not, [f])]) -> sform f k
+    | Comb (Not, [Comb (Or, l)]) -> sform_list_not [] l (k %% make_and)
+    | Comb (Not, [Comb (And, l)]) -> sform_list_not [] l (k %% make_or)
+    | Comb (And, l) -> sform_list [] l (k %% make_and)
+    | Comb (Or, l) -> sform_list [] l (k %% make_or)
+    | Comb (Imp, [f1; f2]) ->
+      sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2'])))
+    | Comb (Not, [Comb (Imp, [f1; f2])]) ->
+      sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2'])))
+    | Comb ((Imp | Not), _) -> assert false
+    | Lit _ -> k f
+  and sform_list acc l k = match l with
+    | [] -> k acc
+    | f :: tail ->
+      sform f (fun f' -> sform_list (f'::acc) tail k)
+  and sform_list_not acc l k = match l with
+    | [] -> k acc
+    | f :: tail ->
+      sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k)
+
+  let ( @@ ) l1 l2 = List.rev_append l1 l2
+  (* let ( @ ) = `Use_rev_append_instead   (* prevent use of non-tailrec append *) *)
+
+  (*
+  let distrib l_and l_or =
+    let l =
+      if l_or = [] then l_and
+      else
+        List.rev_map
+          (fun x ->
+             match x with
+             | Lit _ -> Comb (Or, x::l_or)
+             | Comb (Or, l) -> Comb (Or, l @@ l_or)
+             | _ -> assert false
+          ) l_and
+    in
+    Comb (And, l)
+
+  let rec flatten_or = function
+    | [] -> []
+    | Comb (Or, l)::r -> l @@ (flatten_or r)
+    | Lit a :: r -> (Lit a)::(flatten_or r)
+    | _ -> assert false
+
+  let rec flatten_and = function
+    | [] -> []
+    | Comb (And, l)::r -> l @@ (flatten_and r)
+    | a :: r -> a::(flatten_and r)
+
+
+  let rec cnf f =
+    match f with
+    | Comb (Or, l) ->
+      begin
+        let l = List.rev_map cnf l in
+        let l_and, l_or =
+          List.partition (function Comb(And,_) -> true | _ -> false) l in
+        match l_and with
+        | [ Comb(And, l_conj) ] ->
+          let u = flatten_or l_or in
+          distrib l_conj u
+
+        | Comb(And, l_conj) :: r ->
+          let u = flatten_or l_or in
+          cnf (Comb(Or, (distrib l_conj u)::r))
+
+        | _ ->
+          begin
+            match flatten_or l_or with
+            | [] -> assert false
+            | [r] -> r
+            | v -> Comb (Or, v)
+          end
+      end
+    | Comb (And, l) ->
+      Comb (And, List.rev_map cnf l)
+    | f -> f
+
+  let rec mk_cnf = function
+    | Comb (And, l) ->
+      List.fold_left (fun acc f ->  (mk_cnf f) @@ acc) [] l
+
+    | Comb (Or, [f1;f2]) ->
+      let ll1 = mk_cnf f1 in
+      let ll2 = mk_cnf f2 in
+      List.fold_left
+        (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
+
+    | Comb (Or, f1 :: l) ->
+      let ll1 = mk_cnf f1 in
+      let ll2 = mk_cnf (Comb (Or, l)) in
+      List.fold_left
+        (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1
+
+    | Lit a -> [[a]]
+    | Comb (Not, [Lit a]) -> [[F.neg a]]
+    | _ -> assert false
+
+
+  let rec unfold mono f =
+    match f with
+    | Lit a -> a::mono
+    | Comb (Not, [Lit a]) ->
+      (F.neg a)::mono
+    | Comb (Or, l) ->
+      List.fold_left unfold mono l
+    | _ -> assert false
+
+  let rec init monos f =
+    match f with
+    | Comb (And, l) ->
+      List.fold_left init monos l
+    | f -> (unfold [] f)::monos
+
+  let make_cnf f =
+    let sfnc = cnf (sform f) in
+    init [] sfnc
+  *)
+
+  let mk_proxy = F.fresh
+
+  let acc_or = ref []
+  let acc_and = ref []
+
+  (* build a clause by flattening (if sub-formulas have the
+     same combinator) and proxy-ing sub-formulas that have the
+     opposite operator. *)
+  let rec cnf f = match f with
+    | Lit a -> None, [a]
+    | Comb (Not, [Lit a]) -> None, [F.neg a]
+
+    | Comb (And, l) ->
+      List.fold_left
+        (fun (_, acc) f ->
+           match cnf f with
+           | _, [] -> assert false
+           | _cmb, [a] -> Some And, a :: acc
+           | Some And, l ->
+             Some And, l @@ acc
+           (* let proxy = mk_proxy () in *)
+           (* acc_and := (proxy, l) :: !acc_and; *)
+           (* proxy :: acc *)
+           | Some Or, l ->
+             let proxy = mk_proxy () in
+             acc_or := (proxy, l) :: !acc_or;
+             Some And, proxy :: acc
+           | None, l -> Some And, l @@ acc
+           | _ -> assert false
+        ) (None, []) l
+
+    | Comb (Or, l) ->
+      List.fold_left
+        (fun (_, acc) f ->
+           match cnf f with
+           | _, [] -> assert false
+           | _cmb, [a] -> Some Or, a :: acc
+           | Some Or, l ->
+             Some Or, l @@ acc
+           (* let proxy = mk_proxy () in *)
+           (* acc_or := (proxy, l) :: !acc_or; *)
+           (* proxy :: acc *)
+           | Some And, l ->
+             let proxy = mk_proxy () in
+             acc_and := (proxy, l) :: !acc_and;
+             Some Or, proxy :: acc
+           | None, l -> Some Or, l @@ acc
+           | _ -> assert false
+        ) (None, []) l
+    | _ -> assert false
+
+  let cnf f =
+    let acc = match f with
+      | True -> []
+      | Comb(Not, [True]) -> [[]]
+      | Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l
+      | _ -> [snd (cnf f)]
+    in
+    let proxies = ref [] in
+    (* encore clauses that make proxies in !acc_and equivalent to
+       their clause *)
+    let acc =
+      List.fold_left
+        (fun acc (p,l) ->
+           proxies := p :: !proxies;
+           let np = F.neg p in
+           (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]]
+              also add clauses [p => l1], [p => l2], etc. *)
+           let cl, acc =
+             List.fold_left
+               (fun (cl,acc) a -> (F.neg a :: cl), [np; a] :: acc)
+               ([p],acc) l in
+           cl :: acc
+        ) acc !acc_and
+    in
+    (* encore clauses that make proxies in !acc_or equivalent to
+       their clause *)
+    let acc =
+      List.fold_left
+        (fun acc (p,l) ->
+           proxies := p :: !proxies;
+           (* add clause [p => l1 | l2 | ... | ln], and add clauses
+              [l1 => p], [l2 => p], etc. *)
+           let acc = List.fold_left (fun acc a -> [p; F.neg a]::acc)
+               acc l in
+           (F.neg p :: l) :: acc
+        ) acc !acc_or
+    in
+    acc
+
+  let make_cnf f =
+    acc_or := [];
+    acc_and := [];
+    cnf (sform f (fun f' -> f'))
+
+  (* Naive CNF XXX remove???
+     let make_cnf f = mk_cnf (sform f)
+  *)
+end
--- a/src/sat/src/tseitin/Msat_tseitin.mli
+++ b/src/sat/src/tseitin/Msat_tseitin.mli
@ -0,0 +1,22 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Tseitin CNF conversion
+
+    This modules implements Tseitin's Conjunctive Normal Form conversion, i.e.
+    the ability to transform an arbitrary boolean formula into an equi-satisfiable
+    CNF, that can then be fed to a SAT/SMT/McSat solver.
+*)
+
+module type Arg = Tseitin_intf.Arg
+(** The implementation of formulas required to implement Tseitin's CNF conversion. *)
+
+module type S = Tseitin_intf.S
+(** The exposed interface of Tseitin's CNF conversion. *)
+
+module Make : functor (F : Arg) -> S with type atom = F.t
+(** This functor provides an implementation of Tseitin's CNF conversion. *)
+
--- a/src/sat/src/tseitin/Tseitin_intf.ml
+++ b/src/sat/src/tseitin/Tseitin_intf.ml
@ -0,0 +1,85 @@
+(**************************************************************************)
+(*                                                                        *)
+(*                          Alt-Ergo Zero                                 *)
+(*                                                                        *)
+(*                  Sylvain Conchon and Alain Mebsout                     *)
+(*                      Universite Paris-Sud 11                           *)
+(*                                                                        *)
+(*  Copyright 2011. This file is distributed under the terms of the       *)
+(*  Apache Software License version 2.0                                   *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Interfaces for Tseitin's CNF conversion *)
+
+module type Arg = sig
+  (** Formulas
+
+      This defines what is needed of formulas in order to implement
+      Tseitin's CNF conversion.
+  *)
+
+  type t
+  (** Type of atomic formulas. *)
+
+  val neg : t -> t
+  (** Negation of atomic formulas. *)
+
+  val fresh : unit -> t
+  (** Generate fresh formulas (that are different from any other). *)
+
+  val pp : Format.formatter -> t -> unit
+  (** Print the given formula. *)
+
+end
+
+module type S = sig
+  (** CNF conversion
+
+      This modules converts arbitrary boolean formulas into CNF.
+  *)
+
+  type atom
+  (** The type of atomic formulas. *)
+
+  type t
+  (** The type of arbitrary boolean formulas. Arbitrary boolean formulas
+      can be built using functions in this module, and then converted
+      to a CNF, which is a list of clauses that only use atomic formulas. *)
+
+  val f_true : t
+  (** The [true] formula, i.e a formula that is always satisfied. *)
+
+  val f_false : t
+  (** The [false] formula, i.e a formula that cannot be satisfied. *)
+
+  val make_atom : atom -> t
+  (** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *)
+
+  val make_not : t -> t
+  (** Creates the negation of a boolean formula. *)
+
+  val make_and : t list -> t
+  (** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *)
+
+  val make_or : t list -> t
+  (** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *)
+
+  val make_xor : t -> t -> t
+  (** [make_xor p q] creates the boolean formula "[p] xor [q]". *)
+
+  val make_imply : t -> t -> t
+  (** [make_imply p q] creates the boolean formula "[p] implies [q]". *)
+
+  val make_equiv : t -> t -> t
+  (** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *)
+
+  val make_cnf : t -> atom list list
+  (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a
+      list (which is a conjunction) of lists (which are disjunctions) of
+      atomic formulas. *)
+
+  val pp : Format.formatter -> t -> unit
+  (** [print fmt f] prints the formula on the formatter [fmt].*)
+
+end
--- a/src/sat/src/tseitin/dune
+++ b/src/sat/src/tseitin/dune
@ -0,0 +1,11 @@
+
+(library
+  (name msat_tseitin)
+  (public_name msat.tseitin)
+  (synopsis "Tseitin transformation for msat")
+  (libraries msat)
+  (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
+  (ocamlopt_flags :standard -O3 -bin-annot
+                  -unbox-closures -unbox-closures-factor 20)
+  )
+