diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 66d4fe0..6d9d93c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -10,6 +10,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2
+        with:
+          submodules: recursive
       - name: Set up OCaml
         uses: ocaml/setup-ocaml@v1.1.11
         with:
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000..9c975c9
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "lib/minilib"]
+	path = lib/minilib
+	url = git@github.com:SolarLiner/minilib.git
diff --git a/bin/bench.ml b/bin/bench.ml
new file mode 100644
index 0000000..a204222
--- /dev/null
+++ b/bin/bench.ml
@@ -0,0 +1,30 @@
+open Modulus_lib
+open Strategy
+open Monadsat
+
+let () = Random.self_init ()
+
+let random_list () =
+  let len = Random.int 20 in
+  List.init len (fun _ -> 20 - Random.int 20)
+
+let random_cnf () =
+  let len = Random.int 50 in
+  List.init len (fun _ -> random_list ())
+
+let () =
+  let print_result = function
+    | Some m  -> Printf.printf "  \x1b[32mSAT\x1b[0m : %s\n" (string_of_clause m)
+    | None    -> Printf.printf "  \x1b[31mUNSAT\x1b[0m\n"
+  in
+  List.init 1000 (fun _ -> random_cnf ()) |>
+  List.iteri (fun i cnf ->
+    Printf.printf "testing unit [%d]\n" i;
+    let r1 = Runtime.time (fun () -> Sat.solve cnf) in
+    let r2 = Runtime.time (fun () -> run_opt solve cnf) in
+    assert (r1.result = r2.result);
+    Printf.printf "  (old) solver result [runtime : \x1b[33m%f\x1b[0m] : \n" r1.time;
+    print_result r1.result;
+    Printf.printf "  (new) solver result [runtime : \x1b[33m%f\x1b[0m] : \n" r2.time;
+    print_result r2.result;
+  )
\ No newline at end of file
diff --git a/bin/dune b/bin/dune
index dc39053..ebeacae 100644
--- a/bin/dune
+++ b/bin/dune
@@ -9,3 +9,9 @@
  (public_name test)
  (libraries modulus_lib)
  (modules test))
+
+(executable
+ (name bench)
+ (public_name bench)
+ (libraries modulus_lib)
+ (modules bench))
diff --git a/lib/minilib b/lib/minilib
new file mode 160000
index 0000000..f439454
--- /dev/null
+++ b/lib/minilib
@@ -0,0 +1 @@
+Subproject commit f4394545ade8ea0a705e05087697b3d488f884b5
diff --git a/src/benchmark/runtime.ml b/src/benchmark/runtime.ml
new file mode 100644
index 0000000..be2c73b
--- /dev/null
+++ b/src/benchmark/runtime.ml
@@ -0,0 +1,6 @@
+type 'a bench = { result : 'a; time : float }
+
+let time (f : unit -> 'a) : 'a bench =
+  let t = Sys.time () in
+  let r = f () in
+  { result = r; time = Sys.time () -. t }
\ No newline at end of file
diff --git a/src/dune b/src/dune
index 1856b71..36da497 100644
--- a/src/dune
+++ b/src/dune
@@ -2,4 +2,5 @@
 
 (library
  (public_name modulus.modulus_lib)
- (name modulus_lib))
+ (name modulus_lib)
+ (libraries minicat minicat_ext minilib))
diff --git a/src/sat/monadsat.ml b/src/sat/monadsat.ml
new file mode 100644
index 0000000..61dcf89
--- /dev/null
+++ b/src/sat/monadsat.ml
@@ -0,0 +1,37 @@
+type clause = int list
+
+type cnf = clause list
+
+module S = Strategy.Make(struct type t = cnf end)
+
+open Strategy
+open S
+open Minicat.Monad.Make(S)
+open Minicat.Alternative.Make(S)
+
+let string_of_clause c =
+  "{" ^ String.concat " " (List.map string_of_int c) ^ "}"
+
+let string_of_cnf c =
+  "{" ^ String.concat " " (List.map string_of_clause c) ^ "}"
+
+let remove_lit (l : int) = List.filter ((<>) l)
+
+let propagate l =
+  update @@ List.filter_map (fun c ->
+    if List.mem l c then None
+    else Some (remove_lit (-l) c)
+  )
+
+let add l = fun ls -> l::ls
+
+type 'a solver = 'a t
+
+let solve = ffix @@ fun recall cnf ->
+  match cnf with
+  | [] -> return []
+  | []::_ -> fail "unsat"
+  | (l::_)::_ ->
+    (propagate l <&> recall |> map (add l))
+    <|>
+    (propagate (-l) <&> recall |> map (add (-l)))
\ No newline at end of file
diff --git a/src/solver/core.ml b/src/solver/core.ml
index 3c7246f..1b30931 100644
--- a/src/solver/core.ml
+++ b/src/solver/core.ml
@@ -26,7 +26,7 @@ let dpllt f =
     th atoms
   in
   solve_all cnf
-  |> map (call_theory QfLia.solve)
+  |> map (call_theory MiniLia.solve)
   |> find_first_sat
   |> function
   | SAT m as res -> assert (check f m = Some true); res
diff --git a/src/solver/logic.ml b/src/solver/logic.ml
index b45aeb4..9be6948 100644
--- a/src/solver/logic.ml
+++ b/src/solver/logic.ml
@@ -19,6 +19,15 @@ type formula =
   | Neg of formula
   | Atom of atom
 
+let rec pp_term fmt = function
+  | Var x -> Format.fprintf fmt "%s" x
+  | Cst v -> Format.fprintf fmt "%d" v
+  | Add (t1, t2) -> Format.fprintf fmt "(%a + %a)" pp_term t1 pp_term t2
+
+let pp_atom fmt = function
+  | Eq (t1, t2) -> Format.fprintf fmt "%a = %a" pp_term t1 pp_term t2
+  | Ne (t1, t2) -> Format.fprintf fmt "%a ≠ %a" pp_term t1 pp_term t2
+
 module VSet = Set.Make (String)
 
 let neg_atom (a : atom) =
diff --git a/src/solver/loop.ml b/src/solver/loop.ml
index 983d476..1e541cf 100644
--- a/src/solver/loop.ml
+++ b/src/solver/loop.ml
@@ -108,7 +108,7 @@ let exec_one ctx sxp =
 
 let batch f =
   match Sexp.of_file f with
-  | Some (sxp, rem) when (Lazy.force rem = Nil) ->
+  | Ok sxp ->
     List.fold_left exec_one {
       tenv = Hashtbl.create 50;
       state = Start_mode;
@@ -116,19 +116,23 @@ let batch f =
       logic = ALL;
       model = UNKNOWN;
     } sxp
-  | _ -> Printf.eprintf "parse error\n"; exit 1
+  | Error (err, off) -> Printf.eprintf "%d: parse error: %s\n" off err; exit 1
 
 let repl () =
   let rec step ctx =
     flush stderr;
     Printf.printf "> ";
     match Sexp.of_string (read_line ()) with
-    | None | Some ([], _) | Some (_::_::_, _) ->
-      Printf.eprintf "(error \"this command is incorrect\")\n";
-      step ctx
-    | Some ([s], _) ->
+    | Ok [s] -> begin
       try step (exec_one ctx s)
       with Exit -> exit 0
+    end
+    | Ok _ ->
+      Printf.eprintf "(error \"This command is incorrect\")";
+      step ctx
+    | Error (err, off) ->
+      Printf.eprintf "(error %S)\n" (Printf.sprintf "Parse error: %d: %s" off err);
+      step ctx
   in
   step {
     tenv = Hashtbl.create 50;
diff --git a/src/solver/solver.ml b/src/solver/solver.ml
deleted file mode 100644
index d76e49c..0000000
--- a/src/solver/solver.ml
+++ /dev/null
@@ -1,266 +0,0 @@
-(**
-  This module provides utilities to define new resolution strategies.
-  We introduce a monad [Solver] to build customized solvers or generate
-  new ones given a domain (see {!Domain}).
-*)
-
-open Logic
-open Checker
-open Domain
-
-(**
-  !!! THIS MODULE IS A WORK IN PROGRESS !!!
-
-  A generic evaluator for ground terms (see {!Logic.term}).
-  This module is designed to assist the programmers willing to
-  extend modulus solver.
-
-  If you want add a solver for a specific theory (see {!Solver}),
-  this solver will require a custom evaluator.
-
-  An evaluation function [eval] is any function associating a value to
-  a term for a given model (see {!Model.t}).
-  If a custom evaluator is not intended to evaluate a specific expression [e],
-  then [eval e m] should return [None] for any model [m].
-*)
-module type Evaluator = sig
-  val eval : term -> Model.t -> int option
-end
-
-exception Contradiction of string
-exception Aborted
-
-module Make (D : Domain) : sig
-  type state = (term * D.t) list
-  (** Internal state of the solver *)
-
-  type 'a status
-  (**
-    Status of the solver after an update of the internal state.
-    The status is either:
-    {ul
-      {- A failure (reported if the search space becomes empty)}
-      {- A simple value (reported if the search space is not updated)}
-      {- An update notification (reported if the search space has been updated)}
-      {- An interuption of the resolution}
-    }
-  *)
-
-  val get : 'a status -> 'a
-  (**
-    Get the a [value] from a status report.
-    If the reported status is a failure or an interruption
-    this may raise either a [Contradiction] exception (in case of a failure)
-    or a [Aborted] exception (in case of an interruption).
-  *)
-
-  type 'a update
-  (** A monad to represent functions updating the solver state *)
-
-  val run : 'a update -> state -> 'a status
-  (**
-    Execute an update function on a given state
-  *)
-
-  val return : 'a -> 'a update
-  (**
-    [return v] is an update function ignoring the state
-    of the solver and returning the value [v]
-  *)
-
-  val update : term -> D.t -> D.t update
-  (**
-    [update t v] is an update function
-    which rebinds the value [v] to the term [t] in
-    the solver's state and return this new value.
-
-    If [t] is already bound, intersection as defined by [D.inter] is performed
-    to unify the domains. Such an operation may report a failure if
-    the intersection results in [D.bot] !
-  *)
-
-  val fail : string -> 'a update
-  (**
-    [fail msg] is an update function always resulting in a failure
-    with associated error message [msg].
-  *)
-
-  val leak : state update
-  (**
-    [leak] is an update functions providing the current state of the solver
-    as a return value.
-  *)
-
-  val (>>) : 'a update -> 'b update -> 'b update
-  (**
-    if [f] and [g] are 2 update functions, [f >> g] is the update
-    function performing first [f] and then [g].
-  *)
-
-  val (<|>) : 'a update -> 'a update -> 'a update
-  (**
-    if [f] and [g] are 2 update functions, [f <|> g] is an update function
-    trying first to apply [f] and fallbacks to [g] if [f] failed.
-  *)
-
-  (** TODO : fix operator *)
-  (* val fix : 'a update -> 'a update *)
-
-  val generic_solver : atom list -> Model.t update
-  (**
-    A generic solver generated using the [update] monad.
-  *)
-
-  val solve : atom list -> Model.answer
-  (**
-    Ready to be used version of [generic_solver].
-  *)
-end = struct
-
-type state = (term * D.t) list
-
-type 'a status =
-  | Value of 'a
-  | Update of state * 'a
-  | Fail of string
-  | Abort
-
-type 'a update = state -> 'a status
-
-let[@inline] run f s = f s
-
-let return (v : 'a) : 'a update = fun _ -> Value v
-
-let update (t : term) (v : 'a) : 'a update = fun s ->
-  match List.assoc_opt t s with
-  | Some v' ->
-    if v = v' then Value v' else
-    let d = D.inter v v' in
-    if D.is_empty d then
-      Fail (Format.asprintf "update failed %a ∩ %a = %a"
-        D.pp_print v D.pp_print v' D.pp_print d)
-    else Update ((t, d)::List.remove_assoc t s, d)
-  | None ->
-    Update ((t, v)::s, v)
-
-let get (s : 'a status) : 'a =
-  match s with
-  | Abort -> raise Aborted
-  | Fail l -> raise (Contradiction l)
-  | Value v -> v
-  | Update (_, v) -> v
-
-let leak : state update = fun s -> Value s
-
-let fail msg = fun _ -> Fail msg
-
-let abort = fun _ -> Abort
-
-let (let*) (m : 'a update) (f : 'a -> 'b update) : 'b update = fun s ->
-  match m s with
-  | Abort         -> Abort
-  | Fail _ as err -> err
-  | Value v       -> f v s
-  | Update (e, v) ->
-    match f v e with
-    | Value v -> Update (e, v)
-    | _ as ret -> ret
-
-let rec eval (x : term) : D.t update = fun s ->
-  match List.assoc_opt x s with
-  | Some v -> Value v
-  | None ->
-    match x with
-    | Var _ -> update x D.top s
-    | Cst v -> update x (D.singleton v) s
-    | Add (t1, t2) ->
-      begin
-        let* v1 = eval t1 in
-        let* v2 = eval t2 in
-        update x (D.add v1 v2)
-      end s
-
-let (>>) (f : 'a update) (g : 'b update) : 'b update =
-  let* _ = f in g
-
-let (<|>) (u1 : 'a update) (u2 : 'b update) : 'b update = fun s ->
-  match u1 s with
-  | Fail _ -> u2 s
-  | _ as r -> r
-
-let propagate_one (a : atom) : unit update =
-  match a with
-  | Eq (t1, t2) ->
-    let* d1 = eval t1 in
-    let* d2 = eval t2 in
-    let d = D.inter d1 d2 in
-    update t1 d >> update t2 d >> return ()
-  | Ne (t1, t2) ->
-    let* d1 = eval t1 in
-    let* d2 = eval t2 in
-    if d1 = d2 then
-      update t1 D.bot >> update t2 D.bot >> return ()
-    else
-      return ()
-
-let propagate_one_backward (a: atom) : unit update =
-  let rec step (t : term) (dt : D.t) : unit update =
-    match t with
-    | Cst _ | Var _ -> update t dt >> return ()
-    | Add (t1, t2) ->
-      let* d1 = eval t1 in
-      let* d2 = eval t2 in
-      let (d1', d2') = D.add_inv d1 d2 dt in
-      step t1 d1' >> step t2 d2' >> return ()
-  in
-  match a with
-  | Eq (t1, t2) ->
-    let* d1 = eval t1 in
-    let* d2 = eval t2 in
-    step t1 d1 >> step t2 d2
-  | Ne _ -> return ()
-
-let sequence (l : 'a list) (p : 'a -> unit update) : unit update =
-  List.fold_left (>>) (return ()) (List.map p l)
-
-let propagate l : unit update =
-  sequence l propagate_one
-  >> sequence l propagate_one_backward
-
-let extract_model (p : atom list) =
-  let rec step depth vlist (model : Model.t) : Model.t update =
-    if depth <= 0 then abort else
-    match vlist with
-    | [] ->
-      if check_list model p
-      then return model
-      else fail "extract model"
-    | x::xs ->
-      let* dx = eval (Var x) in
-      let decide x v = update (Var x) (D.singleton v) >> propagate p in
-      match D.split dx with
-      | Split (d1, d2) ->
-        let c1, c2 = D.peek d1, D.peek d2 in
-        (decide x c1 >> (step (depth - 1) xs ((x, c1)::model)))
-        <|>
-        (decide x c2 >> (step (depth - 1) xs ((x, c2)::model)))
-        <|>
-        (update (Var x) d1 >> propagate p >> step (depth - 1) vlist model)
-        <|>
-        (update (Var x) d2 >> propagate p >> step (depth - 1) vlist model)
-      | Single v ->
-        step (depth - 1) xs ((x, v)::model)
-    in
-    step 512 (lvars p) []
-
-let generic_solver (p : atom list) =
-  propagate p >> extract_model p
-
-let solve (p : atom list) =
-  let go = propagate p >> extract_model p in
-  try Model.SAT (get (go []))
-  with
-  | Aborted -> Model.UNKNOWN
-  | Contradiction _ -> Model.UNSAT
-
-end
\ No newline at end of file
diff --git a/src/solver/strategy.ml b/src/solver/strategy.ml
new file mode 100644
index 0000000..d8d5620
--- /dev/null
+++ b/src/solver/strategy.ml
@@ -0,0 +1,88 @@
+type ('env, 'res) status =
+  | Fail of string
+  | Abort
+  | Update of 'env
+  | UpdateValue of 'env * 'res
+  | Value of 'res
+
+type ('env, 'res) t = 'env -> ('env, 'res) status
+
+let[@inline] coerce_status : (('env, 'a) status -> ('env, 'b) status) =
+  function
+  | Value _ | UpdateValue _ -> assert false
+  | Fail _ as x -> x
+  | Abort as x -> x
+  | Update _ as x -> x
+
+let update up = fun env -> Update (up env)
+
+let update_ret v f = fun env -> UpdateValue (f env, v)
+
+let set env = fun _ -> Update env
+
+let abort = fun _ -> Abort
+
+let run f e = f e
+
+let run_opt f e =
+  match f e with
+  | Value v -> Some v
+  | _ -> None
+
+module Make(Env: sig type t end) : sig
+  include Minicat.Monad.MONAD with type 'a t = (Env.t -> (Env.t, 'a) status)
+  include Minicat.Alternative.ALTERNATIVE with type 'a t := 'a t
+
+  val ffix : ('a t -> Env.t -> 'a t) -> 'a t
+
+  val step : (Env.t -> 'a t) -> 'a t
+
+  val (<&>) : 'a t -> 'a t -> 'a t
+
+  val (<?>) : string -> 'a t -> 'a t
+end = struct
+
+  type 'res t = Env.t -> (Env.t, 'res) status
+
+  let empty = fun _ -> Abort
+
+  let fail msg = fun _ -> Fail msg
+
+  let pure v = fun _ -> Value v
+
+  let[@inline] bind m f = fun env ->
+    match m env with
+    | Value v -> f v env
+    | UpdateValue (e, v) -> f v e
+    | x -> coerce_status x
+
+  let[@inline] alt m1 m2 = fun (env : Env.t) ->
+    match m1 env with
+    | Fail _ | Abort -> m2 env
+    | _ as res -> res
+
+  let[@inline] (<&>) s1 s2 = fun env ->
+    match s1 env with
+    | Update e -> s2 e
+    | _ as ret -> ret
+
+  let map f m = bind m (fun r -> pure (f r))
+
+  let app fm xm = bind fm (fun f -> map f xm)
+
+  let ffix (step : 'a t -> Env.t -> 'a t) : 'a t =
+    let rec go env =
+      match step go env env with
+      | Update env -> go env
+      | _ as ret -> ret
+    in go
+
+  (* let rec fix s env =
+    match s env with
+    | Update env -> fix s env
+    | _ as ret -> ret *)
+
+  let step f = fun env -> f env env
+
+  let (<?>) msg m = fun env -> Printf.printf "%s\n" msg; m env
+end
\ No newline at end of file
diff --git a/src/solver/strategy.mli b/src/solver/strategy.mli
new file mode 100644
index 0000000..96cb8aa
--- /dev/null
+++ b/src/solver/strategy.mli
@@ -0,0 +1,91 @@
+(**
+  This module provides utilities to define new resolution strategies.
+  We introduce a monad [('env, 'res) Strategy.t] to build customized solvers.
+
+  Intuitively, a value of type [('env, 'res) Strategy.t] is a function from ['env -> 'res]
+  where ['env] is the type of resolution contexts and ['res] is the result of the strategy.
+
+  A strategy may or may not return a valid result. To modelize this situation, the stragegies results are
+  wrapped in the the [('env, 'res) status] type in order to give additional
+  information on strategies executions.
+
+  The call [run s e] executes the strategy [s] in context [e] and return a status information.
+*)
+
+type ('env, 'res) status =
+    Fail of string
+  | Abort
+  | Update of 'env
+  | UpdateValue of 'env * 'res
+  | Value of 'res
+(**
+  Status message reported by strategies.
+  The status is either:
+  {ul
+    {- A failure with a message }
+    {- A value indicating that the strategy successfully computed a result }
+    {- An update notification indicating that the strategy is not done }
+    {- An update notification together with an intermediate value.
+      This indicate that the strategy computed an intermediate value [v]
+      and updated the environment. It is especially useful to compose intermediate steps.
+    }
+    {- A forced interruption of the strategy }
+  }
+*)
+
+type ('env, 'a) t
+
+val update : ('env -> 'env) -> ('env, 'a) t
+(** [update f] updates the environment of the strategy monad by applying [f] on it, and saving the result. *)
+
+val update_ret : 'a -> ('env -> 'env) -> ('env, 'a) t
+(** [update_ret v f] updates the environment like [update f], but also combines it wdith a [pure v] as the return value. *)
+
+val set : 'env -> ('env, 'a) t
+(** [set env] replaces the current environment by the one provided in [env]. It is the equivalent of [update (Fun.const env)]. *)
+
+val abort : ('env, 'a) t
+(** Aborts computation immediately. *)
+
+
+val run : ('env, 'a) t -> 'env -> ('env, 'a) status
+(**
+  [run s e] executes strategy [s] in environnement [e]
+*)
+
+val run_opt : ('env, 'res) t -> 'env -> 'res option
+(**
+  [run_opt s e] is similar to [run s e] but convert the resulting [status]
+  message to an optional value. If [s] returns only a value [v] in context [e], [run_opt s e] is [Some v]
+  otherwise, [run_opt s e] is [None].
+*)
+
+(** Creates the strategy monad, passing in an instance of the environment type. *)
+module Make :
+  functor (Env : sig type t end) ->
+    sig
+      include Minicat.Monad.MONAD with type 'a t = (Env.t, 'a) t
+      include Minicat.Alternative.ALTERNATIVE with type 'a t := 'a t
+
+      val ffix : ('a t -> Env.t -> 'a t) -> 'a t
+      (**
+        [ffix] computes the fixpoint of a parametrized strategy.
+        If [step] is a function computing a strategy given a strategy [recall] and a context [env],
+        [fix step] computes a recursive strategy which is similar to [step] but where
+        every call to the strategy [recall] are recursive calls to the strategy [step] itself.
+        The recursion continues while [step] returns an update notification.
+        It may not terminates !
+      *)
+
+      val step : (Env.t -> 'a t) -> 'a t
+      (**
+        [step] is used to choose which strategy to apply given a current environment.
+        If [f] is a function from ['env] to [('env, 'res) t] (that is, a function computing a
+        strategy given an environment), then [step f] is the strategy which first apply [f] to 
+        its input environment, and then apply the resulting strategy.
+      *)
+
+      val (<&>) : 'a t -> 'a t -> 'a t
+
+      val (<?>) : string -> 'a t -> 'a t
+    end
diff --git a/src/theories/qf_lia/interval.ml b/src/theories/qf_lia/interval.ml
deleted file mode 100644
index e69de29..0000000
diff --git a/src/theories/qf_lia/qf_lia.ml b/src/theories/qf_lia/qf_lia.ml
index d83f608..fc016e3 100644
--- a/src/theories/qf_lia/qf_lia.ml
+++ b/src/theories/qf_lia/qf_lia.ml
@@ -1,12 +1,11 @@
 (**
   {1 Lia}
   
-  The Modulus internal solver for LIA
-
-  Disclaimer : this module is a "work in progress"
+  Modulus internal solver for QF_LIA
 *)
 
 open Domain
+open Strategy
 
 module Interval : Domain = struct
 
@@ -99,11 +98,181 @@ let peek = function
 
 end
 
-module QfLia = struct
-  module M = Solver.Make (Interval)
-  let solve p =
-    match M.solve p with
-    | Model.UNKNOWN ->
-      Last_effort.find_model p
-    | _ as r -> r 
+
+(** Alias for {!Format.asprintf} *)
+let info = Format.asprintf
+
+(**
+  A module describing the resolution environments
+*)
+module DomMap = struct
+module Typedef = struct
+  (** A context is a record including a mapping from terms to intervals,
+    a list of unbounded variables and a partial model.
+  *)
+  type t = { doms : (Logic.term * Interval.t) list; vlist : string list; model : Model.t }
+end
+
+include Typedef
+module S = Strategy.Make(Typedef)
+open Minicat.Monad.Make(S)
+
+let rec pp_print fmt = function
+  | [] -> ()
+  | (x, d)::next ->
+    Format.fprintf fmt "%a := %a, %a"
+      Logic.pp_term x
+      Interval.pp_print d
+      pp_print next
+
+(** [set_dom_aux x d] is a strategy which binds domain [d] to the term [x]
+    assuming [x] was unbound. This strategy returns [d] as return value.
+*)
+let set_dom x d =
+  let set_dom_aux x d env =
+    { env with doms = (x, d)::env.doms }
+  in update_ret d (set_dom_aux x d)
+
+(** [eval x] is a strategy which evaluates the term [x] in the current environment.
+    If [x] is not bound to a domain, [eval x] binds [x] to {!Interval.top} first.
+*)
+let rec eval (x : Logic.term) = S.step @@ fun env ->
+  (* info "evaluating %a in ctx [%a...]" Logic.pp_term x pp_print env.doms <?> *)
+  match List.assoc_opt x env.doms with
+  | Some v ->
+    (* info "find %a := %a" Logic.pp_term x Interval.pp_print v <?> *)
+    return v
+  | None ->
+    match x with
+    | Var _ ->
+      (* info "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.top) <?> *)
+      set_dom x Interval.top
+    | Cst v ->
+      (* info "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.singleton v) <?> *)
+      set_dom x (Interval.singleton v)
+    | Add (t1, t2) ->
+      let* v1 = eval t1 in
+      let* v2 = eval t2 in
+      (* info "set %a := %a" Logic.pp_term x Interval.pp_print (Interval.add v1 v2) <?> *)
+      set_dom x (Interval.add v1 v2)
+
+(** [update_dom x d] is a strategy which update the domain of [x] with domain [d].
+    If [x] is already bound to a domain [d'], the domain of [x] is set to be the intersection
+    [Interval.inter d d']. If the intersection is {!Interval.bot}, the strategy fails.
+*)
+let update_dom x d =
+  (* info "update %a := %a" Logic.pp_term x Interval.pp_print d <?> *)
+  let* dx = eval x in
+  let dx' = Interval.inter dx d in
+  if Interval.is_empty dx' then
+    S.fail "unsat"
+  else update @@ fun env ->
+    { env with doms = (x, d)::(List.remove_assoc x env.doms) }
+end
+
+(**
+  A mini monadic solver for QF_LIA
+*)
+module MiniLia = struct
+
+open DomMap
+open DomMap.S
+open Minicat.Monad.Make(DomMap.S)
+open Minicat.Alternative.Make(DomMap.S)
+
+(** A solver is a strategy which operates on environments of type {!DomMap.t} and
+  returns a {!Model.t}.
+*)
+type solver = Model.t t
+
+(** A strategy doing nothing *)
+let no_update = update (Fun.id)
+
+(** A strategy printing its current environment *)
+let debug = step @@ fun env ->
+  info "In ctx [%a...]" pp_print env.doms <?> no_update
+
+(** A strategy performing backward propagation.
+    [propagate_one_back t d] assumes that term [t] should evaluates to domain [d]
+    and consequently propagates this information to all subterms of [t].
+*)
+let rec propagate_one_back t d =
+  let open Logic in
+  (* info "propagating backward %a := %a" Logic.pp_term t Interval.pp_print d <?> *)
+  match t with
+  | Cst _ | Var _ -> update_dom t d
+  | Add (t1, t2) ->
+    let* d1 = eval t1 in
+    let* d2 = eval t2 in
+    let (d1', d2') = Interval.add_inv d1 d2 d in
+    propagate_one_back t1 d1' <&> propagate_one_back t2 d2'
+
+(** A strategy performing constraint propagation.
+    [propagate_one c] propagate the constraint [c] in the current
+    environment, thus restraining the domains.
+    It may fails if the constraints [c] is insatisfiable in the context.
+*)
+let propagate_one (a : Logic.atom) =
+  (* info "propagating %a" Logic.pp_atom a <?> *)
+  match a with
+  | Logic.Eq (t1, t2) ->
+    let* d1 = eval t1 in
+    let* d2 = eval t2 in
+    let d = Interval.inter d1 d2 in
+    propagate_one_back t1 d <&> propagate_one_back t2 d
+  | Logic.Ne (t1, t2) ->
+    let* d1 = eval t1 in
+    let* d2 = eval t2 in
+    if d1 = d2 then fail "unsat"
+    else no_update
+
+(** [propagate f] is a strategy
+*)
+let propagate (f : Logic.atom list) =
+  (* info "propagate" <?> *)
+  List.fold_left (<&>) no_update (List.map propagate_one f)
+
+let decide v = step (fun env ->
+  let x = List.hd env.vlist in
+  let xs = List.tl env.vlist in
+  let dx = Interval.singleton v in
+  (* info "decide %s := %d" x v <?> *)
+  set { doms = (Logic.Var x, dx)::List.remove_assoc (Logic.Var x) env.doms
+      ; model = (x, v)::env.model
+      ; vlist = xs
+      }
+)
+
+let rec extract_model (n : int) (f : Logic.atom list) = step @@ fun {vlist; model; _} ->
+  let next = extract_model (n/2) f in
+  let next_decision = extract_model (n - 1) f in
+  if n = 0 then abort
+  else match vlist with
+  | [] ->
+    if Checker.check_list model f then return model
+    else fail "extract model"
+  | x::_ ->
+    let* dx = eval (Var x) in
+    match Interval.split dx with
+    | Single v -> decide v <&> next
+    | Split (d1, d2) ->
+      let c1, c2 = Interval.peek d1, Interval.peek d2 in
+      choice [
+        decide c1 <&> next_decision;
+        decide c2 <&> next_decision;
+        update_dom (Var x) d1 <&> propagate f <&> next;
+        update_dom (Var x) d2 <&> propagate f <&> next
+      ]
+
+let generic_solver (p : Logic.atom list) =
+  propagate p <&> extract_model 16 p
+
+let solve p =
+  let vlist = Logic.lvars p in
+  let doms = [] in
+  let model = [] in
+  match run (generic_solver p) { doms; model; vlist } with
+  | Fail _ -> Model.UNSAT
+  | Value m -> Model.SAT m
+  | _ -> Last_effort.find_model p
 end
\ No newline at end of file
diff --git a/src/utils/parsing.ml b/src/utils/parsing.ml
deleted file mode 100644
index ab5001f..0000000
--- a/src/utils/parsing.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-open Lstream
-
-type ('i, 'o) presult = ('o * 'i t) option
-
-type ('i, 'o) parser = 'i t -> ('i, 'o) presult
-
-let zero _ = None
-
-let return x = fun i -> Some (x, i)
-
-let (>>=) p fp = fun i ->
-  match p i with
-  | None -> None
-  | Some (o, i') -> fp o i'
-
-let any : ('a, 'a) parser = fun inp ->
-  match Lazy.force inp with
-  | Nil -> None
-  | Cons (x, i) -> Some (x, i)
-
-let satisfy test =
-  any >>= (fun res -> if test res then return res else zero)
-
-let eof x = function
-  | Nil -> Some (x, Nil)
-  | Cons _ -> None
-
-let (=>) x f = x >>= fun r -> return (f r)
-
-let (>>) x y = x >>= fun _ -> y
-
-let (<<) x y = x >>= fun r -> y >>= fun _ -> return r
-
-let (<~>) x xs = x >>= fun r -> xs >>= fun rs -> return (r :: rs)
-
-let (<|>) p p' = fun i ->
-  match p i with
-  | None -> p' i
-  | Some _ as r -> r
-
-let option default x = x <|> return default
-
-let rec many p = option [] (p >>= fun r -> many p >>= fun rs -> return (r :: rs))
-
-let many1 p = p <~> many p
-
-let char (c : char) = satisfy ((=) c)
-
-let digit = satisfy (function '0'..'9' -> true | _ -> false)
-
-let implode x = String.concat "" @@ List.map (String.make 1) x
-
-let number = many1 digit => implode => int_of_string
-
-let alpha =
-  satisfy (function 'a'..'z' | 'A'..'Z' -> true | _ -> false)
-
-let spaces =
-  many (satisfy (function '\n' | '\t' | ' ' -> true | _ -> false))
-
-let (let*) = (>>=)
\ No newline at end of file
diff --git a/src/utils/sexp.ml b/src/utils/sexp.ml
index 2238227..b33fd02 100644
--- a/src/utils/sexp.ml
+++ b/src/utils/sexp.ml
@@ -1,5 +1,6 @@
-open Lstream
-open Parsing
+open Minilib.Parsing
+open Minicat.Monad.Make(Minilib.Parsing)
+open Minicat.Alternative.Make(Minilib.Parsing)
 
 type sexp =
   | Sym of string
@@ -7,41 +8,30 @@ type sexp =
   | Cons of sexp list
 
 let ident =
-  spaces >>
-    many1 (alpha <|> char '-') => (fun x -> Sym (implode x))
-  << spaces
+  let open Fold(Minicat_ext.Seq_ext) in (* < provides [many1] over [Seq.t] *)
+  let+ sym = token (many1 (alpha <|> char '-')) in
+  Sym (String.of_seq sym)
 
 let operator =
-  spaces >> (
-    char '+'
-    <|> char '-'
-    <|> char '/'
-    <|> char '*'
-    <|> char '='
-    <|> char '%'
-  ) << spaces => (fun x -> Sym (String.make 1 x))
-
+  let op' = ['+';'-';'/';'*';'=';'%'] |> List.map char |> choice in
+  let+ op = token op' in
+  Sym (String.make 1 op)
 let num =
-  spaces >>
-    number => (fun x -> Int x)
-  << spaces
+  let open Fold(Minicat_ext.Seq_ext) in
+  let+ chars = many1 digit in
+  let num = String.of_seq chars |> int_of_string in 
+  Int num
+
+let atom = token (ident <|> num <|> operator) <?> "atom"
 
-let atom = ident <|> num <|> operator
+let parens p = surround (token (char '(')) (token (char ')')) p <?> "parentheses"
 
-let parens p =
-  spaces >> char '(' >> p << char ')' << spaces
+let sexp =
+  let call sexp = let+ vals = many sexp in Cons vals in
+  fix (fun sexp -> (parens (call sexp) <|> atom) <?> "fix") <?> "sexp"
 
-let rec parse_sexp i =
-  begin
-    atom
-    <|>
-    parens (many parse_sexp => (fun r -> Cons r))
-  end i
+let parser = many sexp
 
-let of_string s =
-  Lstream.of_string s |> many1 parse_sexp
+let of_string s = parse_string parser s
 
-let of_file f =
-  open_in f
-  |> of_channel
-  |> many1 parse_sexp
\ No newline at end of file
+let of_file f = parse_file parser f