Merge pull request #6 from c-cube/wip-lra-simplex-unsat-core

Add unsat core explanations to the simplex

.github/workflows/main.yml

@@ -13,8 +13,16 @@ jobs:
     - uses: avsm/setup-ocaml@master
       with:
         ocaml-version: ${{ matrix.ocaml-version }}
+    - name: cache opam
+      id: cache-opam
+      uses: actions/cache@v2
+      with:
+        path: _opam
+        key: opam-${{matrix.operating-system}}-${{matrix.ocaml-version}}
     - run: opam pin -n .
     - run: opam depext -yt sidekick-bin
+      if: steps.cache-opam.outputs.cache-hit != 'true'
     - run: opam install -t . --deps-only
+      if: steps.cache-opam.outputs.cache-hit != 'true'
     - run: opam exec -- dune build
     - run: opam exec -- dune runtest

Makefile

@@ -44,6 +44,9 @@ $(TESTTOOL)-smt-QF_DT: snapshots
 $(TESTTOOL)-smt-QF_LRA: snapshots
 	$(TESTTOOL) run $(TESTOPTS) \
 	  --csv snapshots/smt-QF_LRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_LRA
+$(TESTTOOL)-smt-QF_UFLRA: snapshots
+	$(TESTTOOL) run $(TESTOPTS) \
+	  --csv snapshots/smt-QF_UFLRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_UFLRA
 
 install: build-install
 	@dune install

dune-project

@@ -1,3 +1,2 @@
 (lang dune 1.6)
 (using menhir 1.0)
-(using fmt 1.1)

sidekick-bin.opam

@@ -15,10 +15,10 @@ depends: [
   "containers" { >= "3.0" & < "4.0" }
   "iter"
   "zarith"
-  "smtlib-utils" { >= "0.1" & < "0.2" }
+  "smtlib-utils" { >= "0.1" & < "0.3" }
   "sidekick" { = version }
   "menhir"
-  "msat" { >= "0.8" < "0.9" }
+  "mtime"
   "ocaml" { >= "4.03" }
 ]
 tags: [ "sat" "smt" ]

sidekick.opam

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

src/arith/base-term/Base_types.ml

@@ -914,6 +914,8 @@ end = struct
     | Eq (a,b) -> C.Eq (a, b)
     | Not u -> C.Not u
     | Ite (a,b,c) -> C.If (a,b,c)
+    | LRA (LRA_pred (Eq, a, b)) ->
+      C.Eq (a,b) (* need congruence closure on this one, for theory combination *)
     | LRA _ -> C.Opaque t (* no congruence here *)
 
   module As_key = struct

src/arith/lra/linear_expr_intf.ml

@@ -134,7 +134,7 @@ module type S = sig
       to coefficients. This allows for very fast computations.
   *)
   module Comb : sig
-    type t = private C.t Var_map.t
+    type t
     (** The type of linear combinations. *)
 
     val compare : t -> t -> int

src/arith/lra/sidekick_arith_lra.ml

@@ -43,6 +43,9 @@ module type ARG = sig
 
   val ty_lra : S.T.Term.state -> ty
 
+  val has_ty_real : term -> bool
+  (** Does this term have the type [Real] *)
+
   module Gensym : sig
     type t
 
@@ -73,18 +76,37 @@ module Make(A : ARG) : S with module A = A = struct
   module T = A.S.T.Term
   module Lit = A.S.Solver_internal.Lit
   module SI = A.S.Solver_internal
+  module N = A.S.Solver_internal.CC.N
+
+  module Tag = struct
+    type t =
+      | By_def
+      | Lit of Lit.t
+      | CC_eq of N.t * N.t
+
+    let pp out = function
+      | By_def -> Fmt.string out "<bydef>"
+      | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l
+      | CC_eq (n1,n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2
+
+    let to_lits si = function
+      | By_def -> []
+      | Lit l -> [l]
+      | CC_eq (n1,n2) ->
+        SI.CC.explain_eq (SI.cc si) n1 n2
+  end
 
   module SimpVar
     : Linear_expr.VAR_GEN
       with type t = A.term
        and type Fresh.t = A.Gensym.t
-       and type lit = Lit.t
+       and type lit = Tag.t
   = struct
     type t = A.term
     let pp = A.S.T.Term.pp
     let compare = A.S.T.Term.compare
-    type lit = Lit.t
+    type lit = Tag.t
-    let pp_lit = Lit.pp
+    let pp_lit = Tag.pp
     module Fresh = struct
       type t = A.Gensym.t
       let copy = A.Gensym.copy
@@ -101,14 +123,17 @@ module Make(A : ARG) : S with module A = A = struct
   module LE = SimpSolver.L.Expr
   module LConstr = SimpSolver.L.Constr
 
+  type proxy = T.t
   type state = {
     tst: T.state;
     simps: T.t T.Tbl.t; (* cache *)
     gensym: A.Gensym.t;
     neq_encoded: unit T.Tbl.t;
     (* if [a != b] asserted and not in this table, add clause [a = b \/ a<b \/ a>b] *)
-    mutable t_defs: (T.t * LE.t) list; (* term definitions *)
+    needs_th_combination: LE.t T.Tbl.t; (* terms that require theory combination *)
-    pred_defs: (pred * LE.t * LE.t) T.Tbl.t; (* predicate definitions *)
+    t_defs: LE.t T.Tbl.t; (* term definitions *)
+    pred_defs: (pred * LE.t * LE.t * T.t * T.t) T.Tbl.t; (* predicate definitions *)
+    local_eqs: (N.t * N.t) Backtrack_stack.t; (* inferred by the congruence closure *)
   }
 
   let create tst : state =
@@ -116,10 +141,20 @@ module Make(A : ARG) : S with module A = A = struct
       simps=T.Tbl.create 128;
       gensym=A.Gensym.create tst;
       neq_encoded=T.Tbl.create 16;
-      t_defs=[];
+      needs_th_combination=T.Tbl.create 8;
+      t_defs=T.Tbl.create 8;
       pred_defs=T.Tbl.create 16;
+      local_eqs = Backtrack_stack.create();
     }
 
+  let push_level self =
+    Backtrack_stack.push_level self.local_eqs;
+    ()
+
+  let pop_levels self n =
+    Backtrack_stack.pop_levels self.local_eqs n ~f:(fun _ -> ());
+    ()
+
   (* FIXME
   let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
     let tst = self.tst in
@@ -191,71 +226,119 @@ module Make(A : ARG) : S with module A = A = struct
       LE.( n * t )
     | LRA_const q -> LE.of_const q
 
+  let as_linexp_id = as_linexp ~f:CCFun.id
+
   (* TODO: keep the linexps until they're asserted;
      TODO: but use simplification in preprocess
      *)
 
   (* preprocess linear expressions away *)
-  let preproc_lra self si ~recurse ~mk_lit:_ ~add_clause:_ (t:T.t) : T.t option =
+  let preproc_lra (self:state) si ~recurse ~mk_lit:_ ~add_clause:_ (t:T.t) : T.t option =
     Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
-    let _tst = SI.tst si in
+    let tst = SI.tst si in
     match A.view_as_lra t with
+    | LRA_pred ((Eq|Neq) as pred, t1, t2) ->
+      (* keep equality as is, needed for congruence closure *)
+      let t1 = recurse t1 in
+      let t2 = recurse t2 in
+      let u = A.mk_lra tst (LRA_pred (pred, t1, t2)) in
+      if T.equal t u then None else Some u
     | LRA_pred (pred, t1, t2) ->
       let l1 = as_linexp ~f:recurse t1 in
       let l2 = as_linexp ~f:recurse t2 in
       let proxy = fresh_term self ~pre:"_pred_lra_" Ty.bool in
-      T.Tbl.add self.pred_defs proxy (pred, l1, l2);
+      T.Tbl.add self.pred_defs proxy (pred, l1, l2, t1, t2);
       Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
                        T.pp t T.pp proxy pp_pred_def (pred,l1,l2));
       Some proxy
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp ~f:recurse t in
       let proxy = fresh_term self ~pre:"_e_lra_" (T.ty t) in
-      self.t_defs <- (proxy, le) :: self.t_defs;
+      T.Tbl.add self.t_defs proxy le;
+      T.Tbl.add self.needs_th_combination proxy le;
       Log.debugf 5 (fun k->k"@[<hv2>lra.preprocess.step %a@ :into %a@ :def %a@]"
                        T.pp t T.pp proxy LE.pp le);
       Some proxy
+    | LRA_other t when A.has_ty_real t ->
+      let le = LE.monomial1 t in
+      T.Tbl.replace self.needs_th_combination t le;
+      None
     | LRA_const _ | LRA_other _ -> None
 
-  (* partial check: just ensure [a != b] triggers the clause
+  (* ensure that [a != b] triggers the clause
      [a=b \/ a<b \/ a>b] *)
-  let partial_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
+  let encode_neq self si acts trail : unit =
     let tst = self.tst in
     begin
       trail
-      |> Iter.filter (fun lit -> not (Lit.sign lit))
       |> Iter.filter_map
         (fun lit ->
            let t = Lit.term lit in
-           match A.view_as_lra t with
+           Log.debugf 50 (fun k->k "@[lra: check lit %a@ :t %a@ :sign %B@]"
-           | LRA_pred (Eq, a, b) when not (T.Tbl.mem self.neq_encoded t) ->
+                             Lit.pp lit T.pp t (Lit.sign lit));
-             Some (lit, a,b)
+
-           | _ -> None)
+           let check_pred pred a b =
+             let pred = if Lit.sign lit then pred else Predicate.neg pred in
+             Log.debugf 50 (fun k->k "pred = `%s`" (Predicate.to_string pred));
+             if pred = Neq && not (T.Tbl.mem self.neq_encoded t) then (
+               Some (lit, a, b)
+             ) else None
+           in
+
+           begin match T.Tbl.find self.pred_defs t with
+             | (pred, _, _, ta, tb) -> check_pred pred ta tb
+             | exception Not_found ->
+               begin match A.view_as_lra t with
+                 | LRA_pred (pred, a, b) -> check_pred pred a b
+                 | _ -> None
+               end
+           end)
       |> Iter.iter
         (fun (lit,a,b) ->
+           Log.debugf 50 (fun k->k "encode neq in %a" Lit.pp lit);
            let c = [
-             Lit.abs lit;
+             Lit.neg lit;
              SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, a, b)));
              SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, b, a)));
            ] in
            SI.add_clause_permanent si acts c;
-           T.Tbl.add self.neq_encoded (Lit.term lit) ();
+           T.Tbl.add self.neq_encoded (Lit.term (Lit.abs lit)) ();
         )
     end
 
+  let dedup_lits lits : _ list =
+    let module LTbl = CCHashtbl.Make(Lit) in
+    let tbl = LTbl.create 16 in
+    List.iter (fun l -> LTbl.replace tbl l ()) lits;
+    LTbl.keys_list tbl
+
+  module Q_map = CCMap.Make(Q)
+
   let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
     Log.debug 5 "(th-lra.final-check)";
+    Profile.with_ "lra.final-check" @@ fun () ->
     let simplex = SimpSolver.create self.gensym in
+    encode_neq self si acts trail;
     (* first, add definitions *)
     begin
-      List.iter
+      T.Tbl.iter
-        (fun (t,le) ->
+        (fun t le ->
            let open LE.Infix in
            let le = le - LE.monomial1 t in
            let c = LConstr.eq0 le in
-           SimpSolver.add_constr simplex c)
+           let lit = Tag.By_def in
+           SimpSolver.add_constr simplex c lit
+        )
         self.t_defs
     end;
+    (* add congruence closure equalities *)
+    Backtrack_stack.iter self.local_eqs
+      ~f:(fun (n1,n2) ->
+         let t1 = N.term n1 |> as_linexp_id in
+         let t2 = N.term n2 |> as_linexp_id in
+         let c = LConstr.eq0 LE.(t1 -  t2) in
+         let lit = Tag.CC_eq (n1,n2) in
+         SimpSolver.add_constr simplex c lit);
     (* add trail *)
     begin
       trail
@@ -263,37 +346,96 @@ module Make(A : ARG) : S with module A = A = struct
         (fun lit ->
            let sign = Lit.sign lit in
            let t = Lit.term lit in
+           let assert_pred pred a b =
+             let pred = if sign then pred else Predicate.neg pred in
+             if pred = Neq then (
+               Log.debugf 50 (fun k->k "(@[LRA.skip-neq@ :in %a@])" T.pp t);
+             ) else (
+               let c = LConstr.of_expr LE.(a-b) pred in
+               SimpSolver.add_constr simplex c (Tag.Lit lit);
+             )
+           in
            begin match T.Tbl.find self.pred_defs t with
-             | exception Not_found -> ()
+             | (pred, a, b, _, _) -> assert_pred pred a b
-             | (pred, a, b) ->
+             | exception Not_found ->
-               (* FIXME: generic negation+printer in Linear_expr_intf;
+               begin match A.view_as_lra t with
-                  actually move predicates to their own module *)
+                 | LRA_pred (pred, a, b) ->
-               let pred = if sign then pred else Predicate.neg pred in
+                   let a = try T.Tbl.find self.t_defs a with _ -> as_linexp_id a in
-               if pred = Neq then (
+                   let b = try T.Tbl.find self.t_defs b with _ -> as_linexp_id b in
-                 Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
+                   assert_pred pred a b
-               ) else (
+                 | _ -> ()
-                 (* TODO: tag *)
+               end
-                 let c = LConstr.of_expr LE.(a-b) pred in
-                 SimpSolver.add_constr simplex c;
-               )
            end)
     end;
     Log.debug 5 "lra: call arith solver";
-    begin match SimpSolver.solve simplex with
+    let res = Profile.with1 "simplex.solve" SimpSolver.solve simplex in
+    begin match res with
       | SimpSolver.Solution _m ->
         Log.debug 5 "lra: solver returns SAT";
-        () (* TODO: get a model + model combination *)
+        Log.debugf 50
-      | SimpSolver.Unsatisfiable _cert ->
+          (fun k->k "(@[LRA.needs-th-combination:@ %a@])"
-        (* we tagged assertions with their lit, so the certificate being an
+              (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
-           unsat core translates directly into a conflict clause *)
+        (* FIXME: theory combination
-        assert false
+        let lazy model = model in
-          (* TODO
+        Log.debugf 30 (fun k->k "(@[LRA.model@ %a@])" FM_A.pp_model model);
+
+        (* theory combination: for [t1,t2] terms in [self.needs_th_combination]
+           that have same value, but are not provably equal, push
+           decision [t1=t2] into the SAT solver. *)
+        begin
+          let by_val: T.t list Q_map.t =
+            T.Tbl.to_iter self.needs_th_combination
+            |> Iter.map (fun (t,le) -> FM_A.eval_model model le, t)
+            |> Iter.fold
+              (fun m (q,t) ->
+                 let l = Q_map.get_or ~default:[] q m in
+                 Q_map.add q (t::l) m)
+              Q_map.empty
+          in
+          Q_map.iter
+            (fun _q ts ->
+               begin match ts with
+                 | [] | [_] -> ()
+                 | ts ->
+                   (* several terms! see if they are already equal *)
+                   CCList.diagonal ts
+                   |> List.iter
+                     (fun (t1,t2) ->
+                        Log.debugf 50
+                          (fun k->k "(@[LRA.th-comb.check-pair[val=%a]@ %a@ %a@])"
+                              Q.pp_print _q T.pp t1 T.pp t2);
+                        (* FIXME: we need these equalities to be considered
+                           by the congruence closure *)
+                        if not (SI.cc_are_equal si t1 t2) then (
+                          Log.debug 50 "LRA.th-comb.must-decide-equal";
+                          let t = A.mk_lra (SI.tst si) (LRA_pred (Eq, t1, t2)) in
+                          let lit = SI.mk_lit si acts t in
+                          SI.push_decision si acts lit
+                        )
+                     )
+               end)
+            by_val;
+          ()
+        end;
+           *)
+        ()
+      | SimpSolver.Unsatisfiable cert ->
+        let unsat_core =
+          match SimpSolver.check_cert simplex cert with
+          | `Ok unsat_core -> unsat_core (* TODO *)
+          | _ -> assert false (* some kind of fatal error ? *)
+        in
         Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
-                         (Fmt.Dump.list Lit.pp) lits);
+                         (Fmt.Dump.list Tag.pp) unsat_core);
-        let confl = List.rev_map Lit.neg lits in
         (* TODO: produce and store a proper LRA resolution proof *)
+        let confl =
+          unsat_core
+          |> Iter.of_list
+          |> Iter.flat_map_l (fun tag -> Tag.to_lits si tag)
+          |> Iter.map Lit.neg
+          |> Iter.to_rev_list
+        in
         SI.raise_conflict si acts confl SI.P.default
-             *)
     end;
     ()
 
@@ -302,8 +444,12 @@ module Make(A : ARG) : S with module A = A = struct
     let st = create (SI.tst si) in
     (* TODO    SI.add_simplifier si (simplify st); *)
     SI.add_preprocess si (preproc_lra st);
-    SI.on_partial_check si (partial_check_ st);
     SI.on_final_check si (final_check_ st);
+    SI.on_cc_post_merge si
+      (fun _ _ n1 n2 ->
+         if A.has_ty_real (N.term n1) then (
+           Backtrack_stack.push st.local_eqs (n1, n2)
+         ));
     (*     SI.add_preprocess si (cnf st); *)
     (* TODO: theory combination *)
     st
@@ -311,6 +457,6 @@ module Make(A : ARG) : S with module A = A = struct
   let theory =
     A.S.mk_theory
       ~name:"th-lra"
-      ~create_and_setup
+      ~create_and_setup ~push_level ~pop_levels
       ()
 end

src/arith/lra/simplex.ml

@@ -122,13 +122,18 @@ module Make_inner
   let str_of_erat = Format.to_string Erat.pp
   let str_of_q = Format.to_string Q.pp_print
 
+  type bound = {
+    value : Erat.t;
+    reason : lit option;
+  }
+
   type t = {
     param: param;
     tab : Q.t Matrix.t; (* the matrix of coefficients *)
     basic : basic_var Vec.vector; (* basic variables *)
     nbasic : nbasic_var Vec.vector; (* non basic variables *)
     mutable assign : Erat.t M.t; (* assignments *)
-    mutable bounds : (Erat.t * Erat.t) M.t; (* (lower, upper) bounds for variables *)
+    mutable bounds : (bound * bound) M.t; (* (lower, upper) bounds for variables *)
     mutable idx_basic : int M.t; (* basic var -> its index in [basic] *)
     mutable idx_nbasic : int M.t; (* non basic var -> its index in [nbasic] *)
   }
@@ -136,7 +141,6 @@ module Make_inner
   type cert = {
     cert_var: var;
     cert_expr: (Q.t * var) list;
-    cert_core: lit list;
   }
 
   type res =
@@ -239,17 +243,23 @@ module Make_inner
     with Not_found -> value_basic t x
 
   (* trivial bounds *)
-  let empty_bounds : Erat.t * Erat.t = Q.(Erat.make minus_inf zero, Erat.make inf zero)
+  let empty_bounds : bound * bound =
+    { value = Erat.make Q.minus_inf Q.zero; reason = None; },
+    { value = Erat.make Q.inf Q.zero; reason = None; }
 
   (* find bounds of [x] *)
-  let[@inline] get_bounds (t:t) (x:var) : Erat.t * Erat.t =
+  let[@inline] get_bounds (t:t) (x:var) : bound * bound =
     try M.find x t.bounds
     with Not_found -> empty_bounds
 
+  let[@inline] get_bounds_values (t:t) (x:var) : Erat.t * Erat.t =
+    let l, u = get_bounds t x in
+    l.value, u.value
+
   (* is [value x] within the bounds for [x]? *)
   let is_within_bounds (t:t) (x:var) : bool * Erat.t =
     let v = value t x in
-    let low, upp = get_bounds t x in
+    let low, upp = get_bounds_values t x in
     if Erat.compare v low < 0 then
       false, low
     else if Erat.compare v upp > 0 then
@@ -313,15 +323,21 @@ module Make_inner
     ()
 
   (* add bounds to [x] in [t] *)
-  let add_bound_aux (t:t) (x:var) (low:Erat.t) (upp:Erat.t) : unit =
+  let add_bound_aux (t:t) (x:var)
+      (low:Erat.t) (low_reason:lit option)
+      (upp:Erat.t) (upp_reason:lit option) : unit =
     add_vars t [x];
     let l, u = get_bounds t x in
-    t.bounds <- M.add x (Erat.max l low, Erat.min u upp) t.bounds
+    let l' = if Erat.lt low l.value then l else { value = low; reason = low_reason; } in
+    let u' = if Erat.gt upp u.value then u else { value = upp; reason = upp_reason; } in
+    t.bounds <- M.add x (l', u') t.bounds
 
-  let add_bounds (t:t) ?strict_lower:(slow=false) ?strict_upper:(supp=false) (x, l, u) : unit =
+  let add_bounds (t:t)
+      ?strict_lower:(slow=false) ?strict_upper:(supp=false)
+      ?lower_reason ?upper_reason (x, l, u) : unit =
     let e1 = if slow then Q.one else Q.zero in
     let e2 = if supp then Q.neg Q.one else Q.zero in
-    add_bound_aux t x (Erat.make l e1) (Erat.make u e2);
+    add_bound_aux t x (Erat.make l e1) lower_reason (Erat.make u e2) upper_reason;
     if mem_nbasic t x then (
       let b, v = is_within_bounds t x in
       if not b then (
@@ -329,8 +345,11 @@ module Make_inner
       )
     )
 
-  let add_lower_bound t ?strict x l = add_bounds t ?strict_lower:strict (x,l,Q.inf)
+  let add_lower_bound t ?strict ~reason x l =
-  let add_upper_bound t ?strict x u = add_bounds t ?strict_upper:strict (x,Q.minus_inf,u)
+    add_bounds t ?strict_lower:strict ~lower_reason:reason (x,l,Q.inf)
+
+  let add_upper_bound t ?strict ~reason x u =
+    add_bounds t ?strict_upper:strict ~upper_reason:reason (x,Q.minus_inf,u)
 
   (* full assignment *)
   let full_assign (t:t) : (var * Erat.t) Iter.t =
@@ -352,7 +371,8 @@ module Make_inner
   let solve_epsilon (t:t) : Q.t =
     let emax =
       M.fold
-        (fun x ({base=low;eps_factor=e_low}, {base=upp;eps_factor=e_upp}) emax ->
+        (fun x ({ value = {base=low;eps_factor=e_low}; _},
+                { value = {base=upp;eps_factor=e_upp}; _}) emax ->
            let {base=v; eps_factor=e_v} = value t x in
            (* lower bound *)
            let emax =
@@ -396,7 +416,7 @@ module Make_inner
     let test (y:nbasic_var) (a:Q.t) : bool =
       assert (mem_nbasic t y);
       let v = value t y in
-      let low, upp = get_bounds t y in
+      let low, upp = get_bounds_values t y in
       if b then (
         (Erat.lt v upp && Q.compare a Q.zero > 0) ||
         (Erat.gt v low && Q.compare a Q.zero < 0)
@@ -489,7 +509,7 @@ module Make_inner
 
   (* check bounds *)
   let check_bounds (t:t) : unit =
-    M.iter (fun x (l, u) -> if Erat.gt l u then raise (AbsurdBounds x)) t.bounds
+    M.iter (fun x (l, u) -> if Erat.gt l.value u.value then raise (AbsurdBounds x)) t.bounds
 
   (* actual solving algorithm *)
   let solve_aux (t:t) : unit =
@@ -534,9 +554,9 @@ module Make_inner
             (Vec.to_list (find_expr_basic t x))
             (Vec.to_list t.nbasic)
         in
-        Unsatisfiable { cert_var=x; cert_expr; cert_core=[]; } (* FIXME *)
+        Unsatisfiable { cert_var=x; cert_expr; } (* FIXME *)
       | AbsurdBounds x ->
-        Unsatisfiable { cert_var=x; cert_expr=[]; cert_core=[]; }
+        Unsatisfiable { cert_var=x; cert_expr=[]; }
 
   (* add [c·x] to [m] *)
   let add_expr_ (x:var) (c:Q.t) (m:Q.t M.t) =
@@ -557,38 +577,54 @@ module Make_inner
       !m
 
   (* maybe invert bounds, if [c < 0] *)
-  let scale_bounds c (l,u) : erat * erat =
+  let scale_bounds c (l,u) : bound * bound =
     match Q.compare c Q.zero with
-      | 0 -> Erat.zero, Erat.zero
+      | 0 ->
-      | n when n<0 -> Erat.mul c u, Erat.mul c l
+        let b = { value = Erat.zero; reason = None; } in
-      | _ -> Erat.mul c l, Erat.mul c u
+        b, b
+      | n when n<0 ->
+        { u with value = Erat.mul c u.value; },
+        { l with value = Erat.mul c l.value; }
+      | _ ->
+        { l with value = Erat.mul c l.value; },
+        { u with value = Erat.mul c u.value; }
+
+  let add_to_unsat_core acc = function
+    | None -> acc
+    | Some reason -> reason :: acc
 
   let check_cert (t:t) (c:cert) =
     let x = c.cert_var in
-    let low_x, up_x = get_bounds t x in
+    let { value = low_x; reason = low_x_reason; },
+        { value = up_x; reason = upp_x_reason; } = get_bounds t x in
     begin match c.cert_expr with
       | [] ->
-        if Erat.compare low_x up_x > 0 then `Ok
+        if Erat.compare low_x up_x > 0
+        then `Ok (add_to_unsat_core (add_to_unsat_core [] low_x_reason) upp_x_reason)
         else `Bad_bounds (str_of_erat low_x, str_of_erat up_x)
       | expr ->
         let e0 = deref_var_ t x (Q.neg Q.one) M.empty in
         (* compute bounds for the expression [c.cert_expr],
            and also compute [c.cert_expr - x] to check if it's 0] *)
-        let low, up, expr_minus_x =
+        let low, low_unsat_core, up, up_unsat_core, expr_minus_x =
           List.fold_left
-            (fun (l,u,expr_minus_x) (c, y) ->
+            (fun (l, luc, u, uuc, expr_minus_x) (c, y) ->
                let ly, uy = scale_bounds c (get_bounds t y) in
-               assert (Erat.compare ly uy <= 0);
+               assert (Erat.compare ly.value uy.value <= 0);
                let expr_minus_x = deref_var_ t y c expr_minus_x in
-               Erat.sum l ly, Erat.sum u uy, expr_minus_x)
+               let luc = add_to_unsat_core luc ly.reason in
-              (Erat.zero, Erat.zero, e0)
+               let uuc = add_to_unsat_core uuc uy.reason in
+               Erat.sum l ly.value, luc, Erat.sum u uy.value, uuc, expr_minus_x)
+            (Erat.zero, [], Erat.zero, [], e0)
               expr
         in
         (* check that the expanded expression is [x], and that
            one of the bounds on [x] is incompatible with bounds of [c.cert_expr] *)
         if M.is_empty expr_minus_x then (
-          if Erat.compare low_x up > 0 || Erat.compare up_x low < 0
+          if Erat.compare low_x up > 0
-          then `Ok
+          then `Ok (add_to_unsat_core up_unsat_core low_x_reason)
+          else if Erat.compare up_x low < 0
+          then `Ok (add_to_unsat_core low_unsat_core upp_x_reason)
           else `Bad_bounds (str_of_erat low, str_of_erat up)
         ) else `Diff_not_0 expr_minus_x
     end
@@ -631,14 +667,14 @@ module Make_inner
     let pp_pair =
       within "(" ")" @@ hvbox @@ pair ~sep:(return "@ := ") Var.pp Erat.pp
     in
-    map Var_map.to_seq @@ within "(" ")" @@ hvbox @@ seq pp_pair
+    map Var_map.to_iter @@ within "(" ")" @@ hvbox @@ iter pp_pair
 
   let pp_bounds =
     let open Format in
     let pp_pairs out (x,(l,u)) =
-      fprintf out "(@[%a =< %a =< %a@])" Erat.pp l Var.pp x Erat.pp u
+      fprintf out "(@[%a =< %a =< %a@])" Erat.pp l.value Var.pp x Erat.pp u.value
     in
-    map Var_map.to_seq @@ within "(" ")" @@ hvbox @@ seq pp_pairs
+    map Var_map.to_iter @@ within "(" ")" @@ hvbox @@ iter pp_pairs
 
   let pp_full_state out (t:t) : unit =
     (* print main matrix *)
@@ -659,6 +695,13 @@ module Make_full_for_expr(V : VAR_GEN)
      with type Var.t = V.t
       and type C.t = Q.t
       and type Var.lit = V.lit)
+  : S_FULL with type var = V.t
+            and type lit = V.lit
+            and module L = L
+            and module Var_map = L.Var_map
+            and type L.var = V.t
+            and type L.Comb.t = L.Comb.t
+            and type param = V.Fresh.t
 = struct
   include Make_inner(V)(L.Var_map)(V.Fresh)
   module L = L
@@ -668,19 +711,25 @@ module Make_full_for_expr(V : VAR_GEN)
   type constr = L.Constr.t
 
   (* add a constraint *)
-  let add_constr (t:t) (c:constr) : unit =
+  let add_constr (t:t) (c:constr) (reason:lit) : unit =
     let (x:var) = V.Fresh.fresh t.param in
     let e, op, q = L.Constr.split c in
     add_eq t (x, L.Comb.to_list e);
     begin match op with
-      | Leq -> add_upper_bound t ~strict:false x q
+      | Leq -> add_upper_bound t ~strict:false ~reason x q
-      | Geq -> add_lower_bound t ~strict:false x q
+      | Geq -> add_lower_bound t ~strict:false ~reason x q
-      | Lt -> add_upper_bound t ~strict:true x q
+      | Lt -> add_upper_bound t ~strict:true ~reason x q
-      | Gt -> add_lower_bound t ~strict:true x q
+      | Gt -> add_lower_bound t ~strict:true ~reason x q
-      | Eq -> add_bounds t ~strict_lower:false ~strict_upper:false (x,q,q)
+      | Eq -> add_bounds t (x,q,q)
+                ~strict_lower:false ~strict_upper:false
+                ~lower_reason:reason ~upper_reason:reason
       | Neq -> assert false
     end
 end
 
 module Make_full(V : VAR_GEN)
+  : S_FULL with type var = V.t
+            and type lit = V.lit
+            and type L.var = V.t
+            and type param = V.Fresh.t
   = Make_full_for_expr(V)(Linear_expr.Make(struct include Q let pp = pp_print end)(V))

src/arith/lra/simplex.mli

@@ -22,6 +22,8 @@ module Make_full_for_expr(V : VAR_GEN)
             and type lit = V.lit
             and module L = L
             and module Var_map = L.Var_map
+            and type L.var = V.t
+            and type L.Comb.t = L.Comb.t
             and type param = V.Fresh.t
 
 module Make_full(V : VAR_GEN)

src/arith/lra/simplex_intf.ml

@@ -35,7 +35,6 @@ module type S = sig
   type cert = {
     cert_var: var;
     cert_expr: (Q.t * var) list;
-    cert_core: lit list;
   }
 
   (** Generic type returned when solving the simplex. A solution is a list of
@@ -66,11 +65,14 @@ module type S = sig
       [Q.inf].
       Optional parameters allow to make the the bounds strict. Defaults to false,
       so that bounds are large by default. *)
-  val add_bounds : t -> ?strict_lower:bool -> ?strict_upper:bool -> var * Q.t * Q.t -> unit
+  val add_bounds : t ->
+    ?strict_lower:bool -> ?strict_upper:bool ->
+    ?lower_reason:lit -> ?upper_reason:lit ->
+    var * Q.t * Q.t -> unit
 
-  val add_lower_bound : t -> ?strict:bool -> var -> Q.t -> unit
+  val add_lower_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
 
-  val add_upper_bound : t -> ?strict:bool -> var -> Q.t -> unit
+  val add_upper_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
 
   (** {3 Simplex solving} *)
 
@@ -85,10 +87,10 @@ module type S = sig
   val check_cert :
     t ->
     cert ->
-    [`Ok | `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t]
+    [`Ok of lit list | `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t]
   (** checks that the certificat indeed yields to a contradiction
       in the current state of the simplex.
-      @return [`Ok] if the certificate is valid. *)
+      @return [`Ok unsat_core] if the certificate is valid. *)
 
   (* TODO: push/pop? at least on bounds *)
 
@@ -119,6 +121,6 @@ module type S_FULL = sig
 
   type constr = L.Constr.t
 
-  val add_constr : t -> constr -> unit
+  val add_constr : t -> constr -> lit -> unit
   (** Add a constraint to a simplex state. *)
 end

src/arith/tests/run_tests.ml

@@ -1,6 +1,4 @@
 
-open OUnit
-
 let props =
   List.flatten
     [ Test_simplex.props;

src/arith/tests/test_simplex.ml

@@ -107,11 +107,13 @@ module Problem = struct
     QC.list_of_size QC.Gen.(m -- n) @@ Constr.rand 10
 end
 
-let add_problem (t:Spl.t) (pb:Problem.t) : unit = List.iter (Spl.add_constr t) pb
+let add_problem (t:Spl.t) (pb:Problem.t) : unit =
+  let lit = 0 in
+  List.iter (fun constr -> Spl.add_constr t constr lit) pb
 
 let pp_subst : subst Fmt.printer =
-  Fmt.(map Spl.L.Var_map.to_seq @@
+  Fmt.(map Spl.L.Var_map.to_iter @@
-    within "{" "}" @@ hvbox @@ seq ~sep:(return ",@ ") @@
+    within "{" "}" @@ hvbox @@ iter ~sep:(return ",@ ") @@
     pair ~sep:(return "@ @<1>→ ") Var.pp Q.pp_print
   )
 
@@ -150,7 +152,7 @@ let check_sound =
         )
       | Spl.Unsatisfiable cert ->
         begin match Spl.check_cert simplex cert with
-          | `Ok -> true
+          | `Ok _ -> true
           | `Bad_bounds (low, up) ->
             QC.Test.fail_reportf
               "(@[<hv>bad-certificat@ :problem %a@ :cert %a@ :low %s :up %s@ :simplex-after  %a@ :simplex-before %a@])"

src/cc/Sidekick_cc.ml

@@ -373,6 +373,7 @@ module Make (A: CC_ARG)
     end
 
   let raise_conflict (cc:t) ~th (acts:actions) (e:lit list) : _ =
+    Profile.instant "cc.conflict";
     (* clear tasks queue *)
     Vec.clear cc.pending;
     Vec.clear cc.combine;
@@ -835,6 +836,10 @@ module Make (A: CC_ARG)
   let[@inline] merge_t cc t1 t2 expl =
     merge cc (add_term cc t1) (add_term cc t2) expl
 
+  let explain_eq cc n1 n2 : lit list =
+    let th = ref true in
+    explain_pair cc ~th [] n1 n2
+
   let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
   let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge
   let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term

src/core/Sidekick_core.ml

@@ -280,6 +280,10 @@ module type CC_S = sig
   val assert_lits : t -> lit Iter.t -> unit
   (** Addition of many literals *)
 
+  val explain_eq : t -> N.t -> N.t -> lit list
+  (** Explain why the two nodes are equal.
+      Fails if they are not, in an unspecified way *)
+
   val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
   (** Raise a conflict with the given explanation
       it must be a theory tautology that [expl ==> absurd].
@@ -390,10 +394,19 @@ module type SOLVER_INTERNAL = sig
   (** {3 hooks for the theory} *)
 
   val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit
+  (** Propagate a literal for a reason. This is similar to asserting
+      the clause [reason => lit], but more lightweight, and in a way
+      that is backtrackable. *)
 
   val raise_conflict : t -> actions -> lit list -> proof -> 'a
   (** Give a conflict clause to the solver *)
 
+  val push_decision : t -> actions -> lit -> unit
+  (** Ask the SAT solver to decide the given literal in an extension of the
+      current trail. This is useful for theory combination.
+      If the SAT solver backtracks, this (potential) decision is removed
+      and forgotten. *)
+
   val propagate: t -> actions -> lit -> (unit -> lit list) -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
@@ -429,6 +442,9 @@ module type SOLVER_INTERNAL = sig
   val cc_find : t -> CC.N.t -> CC.N.t
   (** Find representative of the node *)
 
+  val cc_are_equal : t -> term -> term -> bool
+  (** Are these two terms equal in the congruence closure? *)
+
   val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
   (** Merge these two nodes in the congruence closure, given this explanation.
       It must be a theory tautology that [expl ==> n1 = n2].

src/main/dune

@@ -5,7 +5,7 @@
  (public_name sidekick)
  (package sidekick-bin)
  (libraries containers iter result msat sidekick.core sidekick-arith.base-term
-   sidekick.msat-solver sidekick-bin.smtlib)
+   sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (rule

src/main/main.ml

@@ -78,6 +78,7 @@ let argspec = Arg.align [
     "--no-p", Arg.Clear p_progress, " no progress bar";
     "--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";
+    "-t", Arg.String (int_arg time_limit), " short for --time";
     "--version", Arg.Unit (fun () -> Printf.printf "version: %s\n%!" Sidekick_version.version; exit 0), " show version and exit";
     "-d", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
     "--debug", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
@@ -126,6 +127,8 @@ let check_limits () =
     raise Out_of_space
 
 let main () =
+  Sidekick_tef.setup();
+  at_exit Sidekick_tef.teardown;
   CCFormat.set_color_default true;
   (* Administrative duties *)
   Arg.parse argspec input_file usage;

src/mini-cc/Sidekick_mini_cc.ml

@@ -147,13 +147,14 @@ module Make(A: ARG) = struct
     self
 
   let clear (self:t) : unit =
+    let {ok=_; tbl; sig_tbl; pending=_; combine=_; true_; false_} = self in
     self.ok <- true;
-    T_tbl.clear self.tbl;
-    Sig_tbl.clear self.sig_tbl;
     self.pending <- [];
     self.combine <- [];
-    T_tbl.add self.tbl self.true_.n_t self.true_;
+    T_tbl.clear tbl;
-    T_tbl.add self.tbl self.false_.n_t self.false_;
+    Sig_tbl.clear sig_tbl;
+    T_tbl.add tbl true_.n_t true_;
+    T_tbl.add tbl false_.n_t false_;
     ()
 
   let sub_ t k : unit =
@@ -317,5 +318,4 @@ module Make(A: ARG) = struct
     |> Iter.filter Node.is_root
     |> Iter.map
       (fun n -> Node.iter_cls n |> Iter.map Node.term)
-    
 end

src/msat-solver/Sidekick_msat_solver.ml

@@ -202,6 +202,10 @@ module Make(A : ARG)
 
     let add_preprocess self f = self.preprocess <- f :: self.preprocess
 
+    let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
+      let sign = Lit.sign lit in
+      acts.Msat.acts_add_decision_lit (Lit.abs lit) sign
+
     let[@inline] raise_conflict self acts c : 'a =
       Stat.incr self.count_conflict;
       acts.Msat.acts_raise_conflict c P.default
@@ -279,6 +283,10 @@ module Make(A : ARG)
 
     let cc_add_term self t = CC.add_term (cc self) t
     let cc_find self n = CC.find (cc self) n
+    let cc_are_equal self t1 t2 =
+      let n1 = cc_add_term self t1 in
+      let n2 = cc_add_term self t2 in
+      N.equal (cc_find self n1) (cc_find self n2)
     let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e
     let cc_merge_t self acts t1 t2 e =
       cc_merge self acts (cc_add_term self t1) (cc_add_term self t2) e
@@ -345,10 +353,12 @@ module Make(A : ARG)
 
     (* propagation from the bool solver *)
     let check_ ~final (self:t) (acts: msat_acts) =
+      let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
       let iter = iter_atoms_ acts in
       Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
       self.on_progress();
-      assert_lits_ ~final self acts iter
+      assert_lits_ ~final self acts iter;
+      Profile.exit pb
 
     (* propagation from the bool solver *)
     let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
@@ -578,13 +588,16 @@ module Make(A : ARG)
 
   let add_clause (self:t) (c:Atom.t IArray.t) : unit =
     Stat.incr self.count_clause;
-    Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c);
+    Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c);
-    Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default
+    let pb = Profile.begin_ "add-clause" in
+    Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default;
+    Profile.exit pb
 
   let add_clause_l self c = add_clause self (IArray.of_list c)
 
   let mk_model (self:t) (lits:lit Iter.t) : Model.t =
     Log.debug 1 "(smt.solver.mk-model)";
+    Profile.with_ "msat-solver.mk-model" @@ fun () ->
     let module M = Term.Tbl in
     let m = M.create 128 in
     let tst = self.si.tst in
@@ -606,6 +619,7 @@ module Make(A : ARG)
 
   let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
       ~assumptions (self:t) : res =
+    Profile.with_ "msat-solver.solve" @@ fun () ->
     let do_on_exit () =
       List.iter (fun f->f()) on_exit;
     in

src/smtlib/Form.ml

@@ -134,6 +134,7 @@ let imply_l st xs y = match xs with
   | _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs)
 
 let imply st a b = imply_a st (IArray.singleton a) b
+let xor st a b = not_ st (equiv st a b)
 
 let distinct_l tst l =
   match l with

src/smtlib/Process.ml

@@ -1,6 +1,7 @@
 (** {2 Conversion into {!Term.t}} *)
 
 module BT = Sidekick_base_term
+module Profile = Sidekick_util.Profile
 open Sidekick_base_term
 
 [@@@ocaml.warning "-32"]
@@ -153,8 +154,10 @@ let solve
   let on_progress =
     if progress then Some (mk_progress()) else None in
   let res =
-    Solver.solve ~assumptions ?on_progress s
+    Profile.with_ "solve" begin fun () ->
+      Solver.solve ~assumptions ?on_progress s
     (* ?gc ?restarts ?time ?memory ?progress *)
+    end
   in
   let t2 = Sys.time () in
   Printf.printf "\r"; flush stdout;
@@ -176,11 +179,12 @@ let solve
       Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
     | Solver.Unsat {proof=Some p;_} ->
       if check then (
-        Solver.Proof.check p;
+        Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
       );
       begin match dot_proof with
         | None ->  ()
         | Some file ->
+          Profile.with_ "dot.proof" @@ fun () ->
           CCIO.with_out file
             (fun oc ->
                Log.debugf 1 (fun k->k "write proof into `%s`" file);
@@ -315,6 +319,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
     | _ -> LRA_other t
 
   let ty_lra _st = Ty.real
+  let has_ty_real t = Ty.equal (T.ty t) Ty.real
 
   module Gensym = struct
     type t = {

src/smtlib/Typecheck.ml

@@ -144,6 +144,10 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
             errorf_ctx ctx "expected term, not type; got `%s`" f
         end
     end
+  | PA.App ("xor", [a;b]) ->
+    let a = conv_term ctx a in
+    let b = conv_term ctx b in
+    Form.xor ctx.tst a b
   | PA.App (f, args) ->
     let args = List.map (conv_term ctx) args in
     begin match find_id_ ctx f with
@@ -280,6 +284,12 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
       | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b))
       | PA.Add, (a::l) ->
         List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l
+      | PA.Minus, [a] ->
+        begin match t_as_q a with
+          | Some a -> T.lra ctx.tst (LRA_const (Q.neg a))
+          | None ->
+            T.lra ctx.tst (LRA_op (Minus, T.lra ctx.tst (LRA_const Q.zero), a))
+        end
       | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b))
       | PA.Minus, (a::l) ->
         List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l

src/smtlib/dune

@@ -3,5 +3,6 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick-arith.base-term sidekick.th-bool-static
-   sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils)
+   sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils
+   sidekick.tef)
  (flags :standard -warn-error -a+8 -open Sidekick_util))

src/tef/Sidekick_tef.ml

@@ -0,0 +1,74 @@
+
+module P = Sidekick_util.Profile
+
+let active = lazy (
+  match Sys.getenv "TEF" with
+  | "1"|"true" -> true | _ -> false
+  | exception Not_found -> false
+)
+
+let program_start = Mtime_clock.now()
+
+module Make()
+  : P.BACKEND
+= struct
+  let first_ = ref true
+  let closed_ = ref false
+
+  let teardown_ oc =
+    if not !closed_ then (
+      closed_ := true;
+      output_char oc ']'; (* close array *)
+      flush oc;
+      close_out_noerr oc
+    )
+
+  (* connection to subprocess writing into the file *)
+  let oc =
+    let oc = Unix.open_process_out "gzip - --stdout > trace.json.gz" in
+    output_char oc '[';
+    at_exit (fun () -> teardown_ oc);
+    oc
+
+  let get_ts () : float =
+    let now = Mtime_clock.now() in
+    Mtime.Span.to_us (Mtime.span program_start now)
+
+  let emit_sep_ () =
+    if !first_ then (
+      first_ := false;
+    ) else (
+      output_string oc ",\n";
+    )
+
+  let emit_duration_event ~name ~start ~end_ () : unit =
+    let dur = end_ -. start in
+    let ts = start in
+    let pid = Unix.getpid() in
+    let tid = Thread.id (Thread.self()) in
+    emit_sep_();
+    Printf.fprintf oc
+      {json|{"pid": %d,"cat":"","tid": %d,"dur": %.2f,"ts": %.2f,"name":"%s","ph":"X"}|json}
+      pid tid dur ts name;
+    ()
+
+  let emit_instant_event ~name ~ts () : unit =
+    let pid = Unix.getpid() in
+    let tid = Thread.id (Thread.self()) in
+    emit_sep_();
+    Printf.fprintf oc
+      {json|{"pid": %d,"cat":"","tid": %d,"ts": %.2f,"name":"%s","ph":"I"}|json}
+      pid tid ts name;
+    ()
+
+  let teardown () = teardown_ oc
+end
+
+let setup_ = lazy (
+  let lazy active = active in
+  let b = if active then Some (module Make() : P.BACKEND) else None in
+  P.Control.setup b
+)
+
+let setup () = Lazy.force setup_
+let teardown = P.Control.teardown

src/tef/Sidekick_tef.mli

@@ -0,0 +1,10 @@
+
+(** {1 Tracing Event Format}
+
+    A nice profiling format based on json, useful for visualizing what goes on.
+    See https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/
+*)
+
+val setup : unit -> unit
+
+val teardown : unit -> unit

src/tef/dune

@@ -0,0 +1,8 @@
+
+(library
+  (name sidekick_tef)
+  (public_name sidekick.tef)
+  (synopsis "profiling backend based on TEF")
+  (optional)
+  (flags :standard -warn-error -a+8)
+  (libraries sidekick.util unix threads mtime mtime.clock.os))

src/util/Backtrack_stack.ml

@@ -34,3 +34,5 @@ let pop_levels (self:_ t) (n:int) ~f : unit =
     done;
     Vec.shrink self.lvls new_lvl
   )
+
+let iter ~f self = Vec.iter f self.vec

src/util/Backtrack_stack.mli

@@ -19,3 +19,5 @@ val push_level : _ t -> unit
 
 val pop_levels : 'a t -> int -> f:('a -> unit) -> unit
 (** [pop_levels st n ~f] removes [n] levels, calling [f] on every removed item *)
+
+val iter : f:('a -> unit) -> 'a t -> unit

src/util/Profile.ml

@@ -0,0 +1,102 @@
+
+module type BACKEND = sig
+  val get_ts : unit -> float
+
+  val emit_duration_event :
+    name : string ->
+    start : float ->
+    end_ : float ->
+    unit ->
+    unit
+
+  val emit_instant_event :
+    name : string ->
+    ts : float ->
+    unit ->
+    unit
+
+  val teardown : unit -> unit
+end
+
+type backend = (module BACKEND)
+
+type probe =
+  | No_probe
+  | Probe of {
+    name: string;
+    start: float;
+  }
+
+let null_probe = No_probe
+
+(* where to print events *)
+let out_ : backend option ref = ref None
+
+let begin_with_ (module B:BACKEND) name : probe =
+  Probe {name; start=B.get_ts ()}
+
+let[@inline] begin_ name : probe =
+  match !out_ with
+  | None -> No_probe
+  | Some b -> begin_with_ b name
+
+let[@inline] instant name =
+  match !out_ with
+  | None -> ()
+  | Some (module B) ->
+    let now = B.get_ts() in
+    B.emit_instant_event ~name ~ts:now ()
+
+(* slow path *)
+let exit_full_ (module B : BACKEND) name start =
+  let now = B.get_ts() in
+  B.emit_duration_event ~name ~start ~end_:now ()
+
+let exit_with_ b pb =
+  match pb with
+  | No_probe -> ()
+  | Probe {name; start} -> exit_full_ b name start
+
+let[@inline] exit pb =
+  match pb, !out_ with
+  | Probe {name;start}, Some b -> exit_full_ b name start
+  | _ -> ()
+
+let[@inline] with_ name f =
+  match !out_ with
+  | None -> f()
+  | Some b ->
+    let pb = begin_with_ b name in
+    try
+      let x = f() in
+      exit_with_ b pb;
+      x
+    with e ->
+      exit_with_ b pb;
+      raise e
+
+let[@inline] with1 name f x =
+  match !out_ with
+  | None -> f x
+  | Some b ->
+    let pb = begin_with_ b name in
+    try
+      let res = f x in
+      exit_with_ b pb;
+      res
+    with e ->
+      exit_with_ b pb;
+      raise e
+
+module Control = struct
+  let setup b =
+    assert (!out_ = None);
+    out_ := b
+
+  let teardown () =
+    match !out_ with
+    | None -> ()
+    | Some (module B) ->
+      out_ := None;
+      B.teardown()
+end

src/util/Profile.mli

@@ -0,0 +1,43 @@
+
+(** {1 Profiling probes} *)
+
+type probe
+
+val null_probe : probe
+
+val instant : string -> unit
+
+val begin_ : string -> probe
+
+val exit : probe -> unit
+
+val with_ : string -> (unit -> 'a) -> 'a
+
+val with1 : string -> ('a -> 'b) -> 'a -> 'b
+
+module type BACKEND = sig
+  val get_ts : unit -> float
+
+  val emit_duration_event :
+    name : string ->
+    start : float ->
+    end_ : float ->
+    unit ->
+    unit
+
+  val emit_instant_event :
+    name : string ->
+    ts : float ->
+    unit ->
+    unit
+
+  val teardown : unit -> unit
+end
+
+type backend = (module BACKEND)
+
+module Control : sig
+  val setup : backend option -> unit
+
+  val teardown : unit -> unit
+end

src/util/Sidekick_util.ml

@@ -12,3 +12,4 @@ module Intf = Intf
 module Bag = Bag
 module Stat = Stat
 module Hash = Hash
+module Profile = Profile

tests/unsat/reg_lra_fm1.smt2

@@ -0,0 +1,36 @@
+
+; expect: unsat
+; intermediate problem in tests/unsat/clocksynchro_2clocks.worst_case_skew.base.smt2
+
+(set-logic QF_LRA)
+(declare-fun x_0 () Real)
+(declare-fun x_1 () Real)
+(declare-fun x_2 () Real)
+(declare-fun x_3 () Real)
+(declare-fun x_4 () Real)
+(declare-fun x_5 () Real)
+(declare-fun x_6 () Real)
+(declare-fun x_7 () Real)
+
+(assert (< (+ (/ 2335 666) x_5 x_6 (* (/ 2 999) x_7) (* (/ 2 999) x_4)) 0))
+(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_2) 0))
+(assert (<= (+ (/ 999 1000) x_0 (* -1 x_2)) 0))
+(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_1) 0))
+(assert (<= (+ (/ 999 1000) x_0 (- 0 x_1)) 0))
+(assert (= x_0 0))
+(assert
+  (<= (+
+    (/ 1502501 999000)
+    (* (/ 1001 999) x_5)
+    (* (/ 1001 999) x_6)
+    (* -1 x_7)
+    (* (/ 1001 999) x_3))
+    0))
+
+(assert (< (+ (/ 1001 2) (* (/ 999 2) x_6) x_7 (* (/ -999 2) x_4)) 0))
+(assert (<= (+ (/ 1001 999) x_5 (* -1 x_6) (* (/ 1001 1998) x_4)) 0))
+(assert (< (* -1 x_5) 0))
+(assert (< (* -1 x_4) 0))
+(assert (< (* -1 x_3) 0))
+
+(check-sat)

tests/unsat/smtlib.624916.smt2

@@ -0,0 +1,16 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFLRA)
+(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-sort S1 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (Real) Real)
+(declare-fun f4 () Real)
+(declare-fun f5 () Real)
+(assert (not (= f1 f2)))
+(assert (= (f3 f4) (- 1)))
+(assert (not (=> (= f5 f4) (not (= (f3 f5) 1.0)))))
+(check-sat)
+(exit)