From b2ab465cfff312b2e24056962d3f895c48da0936 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 13 Nov 2020 23:58:14 -0500
Subject: [PATCH 01/13] fix(LRA): track explanations properly when rewriting
 with an equality

---
 src/arith/lra/fourier_motzkin.ml | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/arith/lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml
index 7bd0f96a..24511862 100644
--- a/src/arith/lra/fourier_motzkin.ml
+++ b/src/arith/lra/fourier_motzkin.ml
@@ -315,8 +315,13 @@ module Make(A : ARG)
     let le = LE.remove x le in
     LE.( le + q * le1 )
 
-  let subst_constr x c ~by : Constr.t =
-    let c = {c with Constr.le=subst_le x ~by c.Constr.le} in
+  let subst_constr ~tag x c ~by : Constr.t =
+    let open Constr in
+    let c = {
+      c with
+      le=subst_le x ~by c.le;
+      tag=tag @ c.tag;
+    } in
     Constr.normalize c
 
   let rec solve_ (self:system) : res =
@@ -338,9 +343,9 @@ module Make(A : ARG)
 
           (* substitute using [c0] in the other constraints containing [v] *)
           assert (c0.pred = Eq);
-          let c0 = LE.normalize_wrt v c0.le in
+          let l0 = LE.normalize_wrt v c0.le in
           (* turn equation [c0] into [v = rhs] *)
-          let rhs = LE.neg @@ LE.remove v c0 in
+          let rhs = LE.neg @@ LE.remove v l0 in
           Log.debugf 50
             (fun k->k "(@[FM.subst-from-eq@ :v %a@ :rhs %a@])"
                 T.pp v LE.pp rhs);
@@ -354,7 +359,7 @@ module Make(A : ARG)
             [Iter.of_list ceq'; Iter.of_list occ_pos; Iter.of_list occ_neg]
             |> Iter.of_list
             |> Iter.flatten
-            |> Iter.map (subst_constr v ~by:rhs)
+            |> Iter.map (subst_constr v ~tag:c0.Constr.tag ~by:rhs)
             |> Iter.fold add_sys sys
           in
           solve_ new_sys

From 37089adb17640c1791b9ad0ee0b35697eeb235a7 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 14 Nov 2020 00:23:35 -0500
Subject: [PATCH 02/13] feat: add `-t` option to main

---
 src/main/main.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/main/main.ml b/src/main/main.ml
index 001d8330..fe36465a 100644
--- a/src/main/main.ml
+++ b/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";

From 103c3205775eea2a24f49d77f90e216a2478c39b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 14 Nov 2020 00:23:45 -0500
Subject: [PATCH 03/13] fix(lra): fixed case splitting on `a != b`

---
 src/arith/lra/Sidekick_arith_lra.ml | 49 ++++++++++++++++++++---------
 1 file changed, 34 insertions(+), 15 deletions(-)

diff --git a/src/arith/lra/Sidekick_arith_lra.ml b/src/arith/lra/Sidekick_arith_lra.ml
index 98d69326..85946fb4 100644
--- a/src/arith/lra/Sidekick_arith_lra.ml
+++ b/src/arith/lra/Sidekick_arith_lra.ml
@@ -82,7 +82,7 @@ module Make(A : ARG) : S with module A = A = struct
     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 *)
-    pred_defs: (pred * LE.t * LE.t) T.Tbl.t; (* predicate definitions *)
+    pred_defs: (pred * LE.t * LE.t * T.t * T.t) T.Tbl.t; (* predicate definitions *)
   }
 
   let create tst : state =
@@ -178,7 +178,7 @@ module Make(A : ARG) : S with module A = A = struct
       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
@@ -191,41 +191,59 @@ module Make(A : ARG) : S with module A = A = struct
       Some proxy
     | 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
-           | LRA_pred (Eq, a, b) when not (T.Tbl.mem self.neq_encoded t) ->
-             Some (lit, a,b)
-           | _ -> None)
+           Log.debugf 50 (fun k->k "@[lra: check lit %a@ :t %a@ :sign %B@]"
+                             Lit.pp lit T.pp t (Lit.sign lit));
+           begin match T.Tbl.find self.pred_defs t with
+             | (pred, _, _, ta, tb) ->
+               let pred = if Lit.sign lit then pred else FM.Pred.neg pred in
+               Log.debugf 50 (fun k->k "pred = `%s`" (FM.Pred.to_string pred));
+               if pred = Neq && not (T.Tbl.mem self.neq_encoded t) then (
+                 Some (lit, ta, tb)
+               ) else None
+             | exception Not_found ->
+               begin match A.view_as_lra t with
+                 | LRA_pred (Neq, a, b) when not (T.Tbl.mem self.neq_encoded t) ->
+                   Some (lit, 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
+
   let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
     Log.debug 5 "(th-lra.final-check)";
+    encode_neq self si acts trail;
     let fm = FM_A.create() in
     (* first, add definitions *)
     begin
       List.iter
         (fun (t,le) ->
            let open LE.Infix in
-           let le = le - LE.var t in
            let c = FM_A.Constr.mk ?tag:None Eq (LE.var t) le in
            FM_A.assert_c fm c)
         self.t_defs
@@ -239,7 +257,7 @@ module Make(A : ARG) : S with module A = A = struct
            let t = Lit.term lit in
            begin match T.Tbl.find self.pred_defs t with
              | exception Not_found -> ()
-             | (pred, a, b) ->
+             | (pred, a, b, _, _) ->
                let pred = if sign then pred else FM.Pred.neg pred in
                if pred = Neq then (
                  Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
@@ -259,7 +277,9 @@ module Make(A : ARG) : S with module A = A = struct
            unsat core translates directly into a conflict clause *)
         Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
                          (Fmt.Dump.list Lit.pp) lits);
-        let confl = List.rev_map Lit.neg lits in
+        let confl =
+          List.rev_map Lit.neg lits |> dedup_lits
+        in
         (* TODO: produce and store a proper LRA resolution proof *)
         SI.raise_conflict si acts confl SI.P.default
     end;
@@ -270,7 +290,6 @@ 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.add_preprocess si (cnf st); *)
     (* TODO: theory combination *)

From 77b33346f5620ad57f7b6e8ebe6d3f747a99b263 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 14 Nov 2020 13:17:23 -0500
Subject: [PATCH 04/13] fix(tycheck): handle proper unary minus

---
 src/smtlib/Typecheck.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index ce89c1d4..80337856 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -280,6 +280,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

From 883b27ccc923e9680cf01c4322fb0af7c954ab21 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 14 Nov 2020 16:59:19 -0500
Subject: [PATCH 05/13] add uflra to makefile targets

---
 Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Makefile b/Makefile
index be7fc5f6..aba219b0 100644
--- a/Makefile
+++ b/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

From 1b7d084a9c040367597e55abf2fe539275dded03 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Nov 2020 14:39:39 -0500
Subject: [PATCH 06/13] chore: allow smtlib-utils 0.2

---
 sidekick-bin.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sidekick-bin.opam b/sidekick-bin.opam
index 83de23dd..865f7c3b 100644
--- a/sidekick-bin.opam
+++ b/sidekick-bin.opam
@@ -15,7 +15,7 @@ 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" }

From db1c50f7ed4001913cbbf2dbd586d93f44962d4c Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Nov 2020 16:52:49 -0500
Subject: [PATCH 07/13] feat(LRA): expose model after fourier-motzkin returns
 "SAT"

---
 src/arith/lra/Sidekick_arith_lra.ml |  19 +++-
 src/arith/lra/fourier_motzkin.ml    | 147 +++++++++++++++++++++++++---
 src/smtlib/Process.ml               |   2 +
 3 files changed, 155 insertions(+), 13 deletions(-)

diff --git a/src/arith/lra/Sidekick_arith_lra.ml b/src/arith/lra/Sidekick_arith_lra.ml
index 85946fb4..a7971d28 100644
--- a/src/arith/lra/Sidekick_arith_lra.ml
+++ b/src/arith/lra/Sidekick_arith_lra.ml
@@ -38,6 +38,9 @@ module type ARG = sig
   val mk_lra : S.T.Term.state -> term lra_view -> term
   (** Make a term from the given theory view *)
 
+  val has_ty_real : term -> bool
+  (** Does this term have the type [Real] *)
+
   module Gensym : sig
     type t
 
@@ -81,6 +84,7 @@ module Make(A : ARG) : S with module A = A = struct
     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] *)
+    needs_th_combination: LE.t T.Tbl.t; (* terms that require theory combination *)
     mutable t_defs: (T.t * LE.t) list; (* term definitions *)
     pred_defs: (pred * LE.t * LE.t * T.t * T.t) T.Tbl.t; (* predicate definitions *)
   }
@@ -90,6 +94,7 @@ 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;
+      needs_th_combination=T.Tbl.create 8;
       t_defs=[];
       pred_defs=T.Tbl.create 16;
     }
@@ -170,7 +175,7 @@ module Make(A : ARG) : S with module A = A = struct
      *)
 
   (* 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
     match A.view_as_lra t with
@@ -184,11 +189,17 @@ module Make(A : ARG) : S with module A = A = struct
       Some proxy
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp ~f:recurse t in
+      (* TODO: reuse proxy if present? *)
       let proxy = fresh_term self ~pre:"_e_lra_" (T.ty t) in
       self.t_defs <- (proxy, le) :: self.t_defs;
+      T.Tbl.add self.needs_th_combination t 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.var t in
+      T.Tbl.replace self.needs_th_combination t le;
+      None
     | LRA_const _ | LRA_other _ -> None
 
   (* ensure that [a != b] triggers the clause
@@ -269,8 +280,12 @@ module Make(A : ARG) : S with module A = A = struct
     end;
     Log.debug 5 "lra: call arith solver";
     begin match FM_A.solve fm with
-      | FM_A.Sat ->
+      | FM_A.Sat model ->
         Log.debug 5 "lra: solver returns SAT";
+        Log.debugf 50
+          (fun k->k "(@[LRA.needs-th-combination:@ %a@])"
+              (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
+        Log.debugf 30 (fun k->k "(@[LRA.model@ %a@])" FM_A.pp_model model);
         () (* TODO: get a model + model combination *)
       | FM_A.Unsat lits ->
         (* we tagged assertions with their lit, so the certificate being an
diff --git a/src/arith/lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml
index 24511862..8a01995d 100644
--- a/src/arith/lra/fourier_motzkin.ml
+++ b/src/arith/lra/fourier_motzkin.ml
@@ -61,8 +61,6 @@ module type S = sig
     val find : term -> t -> Q.t option
     val mem : term -> t -> bool
 
-(*     val map : (term -> term) -> t -> t *)
-
     module Infix : sig
       val (+) : t -> t -> t
       val (-) : t -> t -> t
@@ -86,8 +84,13 @@ module type S = sig
 
   val assert_c : t -> Constr.t -> unit
 
+  type model
+
+  val get_model : model -> term -> Q.t
+  val pp_model : model Fmt.printer
+
   type res =
-    | Sat
+    | Sat of model
     | Unsat of A.tag list
 
   val solve : t -> res
@@ -237,8 +240,20 @@ module Make(A : ARG)
     occ_neg: Constr.t list;
   }
 
+  type pre_model_strict = Strict | NonStrict
+  type pre_model_constr =
+    | PM_eq of LE.t
+    | PM_bounds of {
+        lower: (pre_model_strict * LE.t) list;
+        upper: (pre_model_strict * LE.t) list;
+      }
+
+  type pre_model = pre_model_constr lazy_t T_map.t
+  type model = Q.t T_map.t lazy_t
+
   type system = {
     empties: Constr.t list; (* no variables, check first *)
+    pre_model: pre_model; (* for model construction *)
     idx: c_for_var T_map.t;
     (* map [t] to [cft] where [cft] are normalized constraints whose
        maximum term is [t], with positive sign for [cft.occ_pos]
@@ -250,7 +265,7 @@ module Make(A : ARG)
     mutable sys: system;
   }
 
-  let empty_sys : system = {empties=[]; idx=T_map.empty}
+  let empty_sys : system = {empties=[]; pre_model=T_map.empty; idx=T_map.empty}
   let empty_c_for_v : c_for_var =
     { occ_pos=[]; occ_neg=[]; occ_eq=[] }
 
@@ -294,7 +309,8 @@ module Make(A : ARG)
 
   let pp_system out (self:system) : unit =
     let pp_idxkv out (t,{occ_eq; occ_pos; occ_neg}) =
-      Fmt.fprintf out "(@[for-var %a@ :occ-eq %a@ :occ-pos %a@ :occ-neg %a@])"
+      Fmt.fprintf out
+        "(@[for-var %a@ @[:occ-eq %a@]@ @[:occ-pos %a@]@ @[:occ-neg %a@]@])"
         T.pp t
         (Fmt.Dump.list Constr.pp) occ_eq
         (Fmt.Dump.list Constr.pp) occ_pos
@@ -305,8 +321,82 @@ module Make(A : ARG)
       (Util.pp_iter pp_idxkv) (T_map.to_iter self.idx)
 
   (* TODO: be able to provide a model for SAT *)
+  let build_model_ (self:pre_model) : _ T_map.t =
+    let l = T_map.to_iter self |> Iter.to_rev_list in
+
+    (* how to evaluate a linexpr in the model *)
+    let eval_le (mv:Q.t T_map.t) (le:LE.t) : Q.t =
+      let find x = try T_map.find x mv with Not_found -> Q.zero in
+      T_map.to_iter le.LE.le
+      |> Iter.fold
+        (fun sum (t,coeff) -> Q.(sum + coeff * find t))
+        le.LE.const
+    in
+    let or_strict s1 s2 = match s1, s2 with
+      | Strict, _ | _, Strict -> Strict
+      | NonStrict, NonStrict -> NonStrict
+    in
+    let max_pair (s1,q1)(s2,q2) =
+      if Q.equal q1 q2 then or_strict s1 s2, q1
+      else if Q.gt q1 q2 then s1,q1
+      else s2,q2
+    and min_pair (s1,q1)(s2,q2) =
+      if Q.equal q1 q2 then or_strict s1 s2, q1
+      else if Q.lt q1 q2 then s1,q1
+      else s2,q2
+    in
+    let m =
+      List.fold_left
+        begin fun m (v,cs_v) ->
+          (* update [v] using its constraints [cs_v].
+             [m] is the model to update *)
+          let val_v =
+            match cs_v with
+            | lazy (PM_eq le) -> eval_le m le
+            | lazy (PM_bounds {lower; upper}) ->
+              let lower = List.map (fun (s,le) -> s, eval_le m le) lower in
+              let upper = List.map (fun (s,le) -> s, eval_le m le) upper in
+              let strict_low, lower = match lower with
+                | [] -> NonStrict, Q.minus_inf
+                | x :: l -> List.fold_left max_pair x l
+              and strict_up, upper = match upper with
+                | [] -> NonStrict, Q.inf
+                | x :: l -> List.fold_left min_pair x l
+              in
+              if Q.is_real lower && Q.is_real upper then (
+                if Q.equal lower upper then (
+                  assert (strict_low=NonStrict && strict_up=NonStrict); (* unsat otherwise *)
+                  lower
+                ) else (
+                  Q.((lower + upper) / of_int 2) (* middle *)
+                )
+              ) else if Q.is_real lower then (
+                if strict_low=Strict then Q.(lower + one) else lower
+              ) else if Q.is_real upper then (
+                if strict_up=Strict then Q.(upper - one) else upper
+              ) else (
+                Q.zero (* no bounds *)
+              )
+          in
+          T_map.add v val_v m
+        end
+        T_map.empty l
+    in
+    m
+
+  let get_model (m:model) (v:T.t) : Q.t =
+    let lazy m = m in
+    try T_map.find v m
+    with Not_found -> Q.zero
+
+  let pp_model out (m:model) : unit =
+    let lazy m = m in
+    let pp_pair out (v,q) = Fmt.fprintf out "(@[%a@ %a@])" T.pp v Q.pp_print q in
+    Fmt.fprintf out "(@[<hv1>model@ %a@])"
+      (Util.pp_iter pp_pair) (T_map.to_iter m)
+
   type res =
-    | Sat
+    | Sat of model
     | Unsat of A.tag list
 
   (* replace [x] with [by] inside [le] *)
@@ -324,6 +414,23 @@ module Make(A : ARG)
     } in
     Constr.normalize c
 
+  (* given an ineq constraint on [v], canonize it wrt [v]
+     (set the coeff of [v] to 1)
+     and return whether it's strict or not *)
+  let premod_of_constr (v:T.t) (c:Constr.t) : pre_model_strict * LE.t =
+    let strict =
+      match c.Constr.pred with
+      | Pred.Leq -> NonStrict | Pred.Lt -> Strict
+      | _ -> assert false
+    in
+    let coeff =
+      try LE.find_exn v c.Constr.le
+      with Not_found -> assert false
+    in
+    let le = LE.remove v c.Constr.le in
+    let le = LE.( Q.(one / coeff) * le) in
+    strict, le
+
   let rec solve_ (self:system) : res =
     Log.debugf 50
       (fun k->k "(@[FM.solve-rec@ :sys %a@])" pp_system self);
@@ -334,7 +441,9 @@ module Make(A : ARG)
       | exception Not_found ->
         (* need to process biggest variable first *)
         match T_map.max_binding_opt self.idx with
-        | None -> Sat
+        | None ->
+          let m = lazy (build_model_ self.pre_model) in
+          Sat m
         | Some (v, {occ_eq=c0 :: ceq'; occ_pos; occ_neg}) ->
           (* at least one equality constraint, use it as a substitution *)
 
@@ -362,6 +471,13 @@ module Make(A : ARG)
             |> Iter.map (subst_constr v ~tag:c0.Constr.tag ~by:rhs)
             |> Iter.fold add_sys sys
           in
+
+          let new_sys =
+            (* update pre-model, keeping only [v := rhs] *)
+            let pre_model = T_map.add v (Lazy.from_val (PM_eq rhs)) self.pre_model in
+            {new_sys with pre_model}
+          in
+
           solve_ new_sys
 
         | Some (v, {occ_eq=[]; occ_pos=l_pos; occ_neg=l_neg}) ->
@@ -373,10 +489,6 @@ module Make(A : ARG)
           (* remove [v] *)
           let sys = {self with idx=T_map.remove v self.idx} in
 
-          (* TODO: store all lower bound constraints for [v], so we can use
-             their max to build the model once we have values for lower
-             variables *)
-
           let new_sys =
             Iter.product (Iter.of_list l_pos) (Iter.of_list l_neg)
             |> Iter.map
@@ -402,6 +514,19 @@ module Make(A : ARG)
                 c)
             |> Iter.fold add_sys sys
           in
+
+          let new_sys =
+            let pre_model =
+              let pm_c = lazy (
+                let lower = List.rev_map (premod_of_constr v) l_neg in
+                let upper = List.rev_map (premod_of_constr v) l_pos in
+                PM_bounds {lower; upper}
+              ) in
+              T_map.add v pm_c self.pre_model
+            in
+            {new_sys with pre_model}
+          in
+
           solve_ new_sys
     end
 
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 3ae64420..305bacde 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -313,6 +313,8 @@ module Th_lra = Sidekick_arith_lra.Make(struct
     | T.Eq (a,b) when Ty.equal (T.ty a) Ty.real -> LRA_pred (Eq, a, b)
     | _ -> LRA_other t
 
+  let has_ty_real t = Ty.equal (T.ty t) Ty.real
+
   module Gensym = struct
     type t = {
       tst: T.state;

From 6a0731eeb13a45c4d1cddb1d78628126a1eb0e16 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Nov 2020 17:03:12 -0500
Subject: [PATCH 08/13] refactor: improve model production in FM

---
 src/arith/lra/fourier_motzkin.ml | 81 +++++++++++++++++---------------
 1 file changed, 43 insertions(+), 38 deletions(-)

diff --git a/src/arith/lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml
index 8a01995d..56d3cf4f 100644
--- a/src/arith/lra/fourier_motzkin.ml
+++ b/src/arith/lra/fourier_motzkin.ml
@@ -324,9 +324,15 @@ module Make(A : ARG)
   let build_model_ (self:pre_model) : _ T_map.t =
     let l = T_map.to_iter self |> Iter.to_rev_list in
 
+    let m = ref T_map.empty in
+
     (* how to evaluate a linexpr in the model *)
-    let eval_le (mv:Q.t T_map.t) (le:LE.t) : Q.t =
-      let find x = try T_map.find x mv with Not_found -> Q.zero in
+    let eval_le (le:LE.t) : Q.t =
+      let find x =
+        try T_map.find x !m
+        with Not_found ->
+          m := T_map.add x Q.zero !m; (* remember this choice *)
+          Q.zero in
       T_map.to_iter le.LE.le
       |> Iter.fold
         (fun sum (t,coeff) -> Q.(sum + coeff * find t))
@@ -345,44 +351,43 @@ module Make(A : ARG)
       else if Q.lt q1 q2 then s1,q1
       else s2,q2
     in
-    let m =
-      List.fold_left
-        begin fun m (v,cs_v) ->
-          (* update [v] using its constraints [cs_v].
-             [m] is the model to update *)
-          let val_v =
-            match cs_v with
-            | lazy (PM_eq le) -> eval_le m le
-            | lazy (PM_bounds {lower; upper}) ->
-              let lower = List.map (fun (s,le) -> s, eval_le m le) lower in
-              let upper = List.map (fun (s,le) -> s, eval_le m le) upper in
-              let strict_low, lower = match lower with
-                | [] -> NonStrict, Q.minus_inf
-                | x :: l -> List.fold_left max_pair x l
-              and strict_up, upper = match upper with
-                | [] -> NonStrict, Q.inf
-                | x :: l -> List.fold_left min_pair x l
-              in
-              if Q.is_real lower && Q.is_real upper then (
-                if Q.equal lower upper then (
-                  assert (strict_low=NonStrict && strict_up=NonStrict); (* unsat otherwise *)
-                  lower
-                ) else (
-                  Q.((lower + upper) / of_int 2) (* middle *)
-                )
-              ) else if Q.is_real lower then (
-                if strict_low=Strict then Q.(lower + one) else lower
-              ) else if Q.is_real upper then (
-                if strict_up=Strict then Q.(upper - one) else upper
+    List.iter
+      begin fun (v,cs_v) ->
+        (* update [v] using its constraints [cs_v].
+           [m] is the model to update *)
+        let val_v =
+          match cs_v with
+          | lazy (PM_eq le) -> eval_le le
+          | lazy (PM_bounds {lower; upper}) ->
+            let lower = List.map (fun (s,le) -> s, eval_le le) lower in
+            let upper = List.map (fun (s,le) -> s, eval_le le) upper in
+            let strict_low, lower = match lower with
+              | [] -> NonStrict, Q.minus_inf
+              | x :: l -> List.fold_left max_pair x l
+            and strict_up, upper = match upper with
+              | [] -> NonStrict, Q.inf
+              | x :: l -> List.fold_left min_pair x l
+            in
+            if Q.is_real lower && Q.is_real upper then (
+              if Q.equal lower upper then (
+                assert (strict_low=NonStrict && strict_up=NonStrict); (* unsat otherwise *)
+                lower
               ) else (
-                Q.zero (* no bounds *)
+                Q.((lower + upper) / of_int 2) (* middle *)
               )
-          in
-          T_map.add v val_v m
-        end
-        T_map.empty l
-    in
-    m
+            ) else if Q.is_real lower then (
+              if strict_low=Strict then Q.(lower + one) else lower
+            ) else if Q.is_real upper then (
+              if strict_up=Strict then Q.(upper - one) else upper
+            ) else (
+              Q.zero (* no bounds *)
+            )
+        in
+        assert (not (T_map.mem v !m)); (* by ordering *)
+        m := T_map.add v val_v !m;
+      end
+      l;
+    !m
 
   let get_model (m:model) (v:T.t) : Q.t =
     let lazy m = m in

From 60fe3506d5ad8fbee80f56a640f875292c5a757c Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Nov 2020 18:22:51 -0500
Subject: [PATCH 09/13] feat(core): add `CC.explain_eq` to explain why two
 nodes were merged

---
 src/cc/Sidekick_cc.ml     |  4 ++++
 src/core/Sidekick_core.ml | 10 ++++++++++
 2 files changed, 14 insertions(+)

diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 74de8767..9ae61c09 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -835,6 +835,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
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 127aa65d..d0953a42 100644
--- a/src/core/Sidekick_core.ml
+++ b/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,6 +394,9 @@ 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 *)
@@ -429,6 +436,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].

From 9839e5a36bc0327ce30856df436758b526869942 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Nov 2020 18:23:16 -0500
Subject: [PATCH 10/13] feat(core): add `push_decision`, for model-based th
 combination

---
 src/core/Sidekick_core.ml               |  6 ++++++
 src/msat-solver/Sidekick_msat_solver.ml | 10 +++++++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index d0953a42..7ef211bd 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -401,6 +401,12 @@ module type SOLVER_INTERNAL = sig
   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 *)
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index b5036682..3330099d 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/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
@@ -578,7 +586,7 @@ 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 add_clause_l self c = add_clause self (IArray.of_list c)

From 6417bbdd808b90b4dc9321c3ee0d703c2d0489cd Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Nov 2020 18:23:58 -0500
Subject: [PATCH 11/13] feat(util): add `Backtrack_stack.iter`

---
 src/util/Backtrack_stack.ml  | 2 ++
 src/util/Backtrack_stack.mli | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/src/util/Backtrack_stack.ml b/src/util/Backtrack_stack.ml
index a23056f1..890be02f 100644
--- a/src/util/Backtrack_stack.ml
+++ b/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
diff --git a/src/util/Backtrack_stack.mli b/src/util/Backtrack_stack.mli
index e7125138..901c63ce 100644
--- a/src/util/Backtrack_stack.mli
+++ b/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

From b3a7acf95bf378519699eedb0c19711e21456872 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Nov 2020 18:24:09 -0500
Subject: [PATCH 12/13] feat(LRA): handle congruence closure and theory
 combination in LRA

- merges in the CC are handled by adding corresponding equalities
  locally
- theory combination pushes the decision `a=b` into the SAT solver
  if a,b have the same model values and are not provably equal
  in the CC already.
- also, fix model construction
---
 src/arith/base-term/Base_types.ml   |   2 +
 src/arith/lra/Sidekick_arith_lra.ml | 166 ++++++++++++++++++++++------
 src/arith/lra/fourier_motzkin.ml    |  31 ++++--
 3 files changed, 159 insertions(+), 40 deletions(-)

diff --git a/src/arith/base-term/Base_types.ml b/src/arith/base-term/Base_types.ml
index ed7df0eb..660f19c1 100644
--- a/src/arith/base-term/Base_types.ml
+++ b/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
diff --git a/src/arith/lra/Sidekick_arith_lra.ml b/src/arith/lra/Sidekick_arith_lra.ml
index a7971d28..77e72195 100644
--- a/src/arith/lra/Sidekick_arith_lra.ml
+++ b/src/arith/lra/Sidekick_arith_lra.ml
@@ -67,17 +67,34 @@ 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 =
+      | Lit of Lit.t
+      | CC_eq of N.t * N.t
+
+    let pp out = function
+      | 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
+      | Lit l -> [l]
+      | CC_eq (n1,n2) ->
+        SI.CC.explain_eq (SI.cc si) n1 n2
+  end
 
   (* the fourier motzkin module *)
   module FM_A = FM.Make(struct
       module T = T
-      type tag = Lit.t
-      let pp_tag = Lit.pp
+      type tag = Tag.t
+      let pp_tag = Tag.pp
     end)
 
   (* linear expressions *)
   module LE = FM_A.LE
 
+  type proxy = T.t
   type state = {
     tst: T.state;
     simps: T.t T.Tbl.t; (* cache *)
@@ -85,8 +102,9 @@ module Make(A : ARG) : S with module A = A = struct
     neq_encoded: unit T.Tbl.t;
     (* if [a != b] asserted and not in this table, add clause [a = b \/ a<b \/ a>b] *)
     needs_th_combination: LE.t T.Tbl.t; (* terms that require theory combination *)
-    mutable t_defs: (T.t * LE.t) list; (* term 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 =
@@ -95,10 +113,19 @@ module Make(A : ARG) : S with module A = A = struct
       gensym=A.Gensym.create tst;
       neq_encoded=T.Tbl.create 16;
       needs_th_combination=T.Tbl.create 8;
-      t_defs=[];
+      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
@@ -170,6 +197,8 @@ module Make(A : ARG) : S with module A = A = struct
       LE.( n * t )
     | LRA_const q -> LE.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
      *)
@@ -177,8 +206,14 @@ module Make(A : ARG) : S with module A = A = struct
   (* preprocess linear expressions away *)
   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
@@ -189,10 +224,9 @@ module Make(A : ARG) : S with module A = A = struct
       Some proxy
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp ~f:recurse t in
-      (* TODO: reuse proxy if present? *)
       let proxy = fresh_term self ~pre:"_e_lra_" (T.ty t) in
-      self.t_defs <- (proxy, le) :: self.t_defs;
-      T.Tbl.add self.needs_th_combination t le;
+      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
@@ -213,17 +247,20 @@ module Make(A : ARG) : S with module A = A = struct
            let t = Lit.term lit in
            Log.debugf 50 (fun k->k "@[lra: check lit %a@ :t %a@ :sign %B@]"
                              Lit.pp lit T.pp t (Lit.sign lit));
+
+           let check_pred pred a b =
+             let pred = if Lit.sign lit then pred else FM.Pred.neg pred in
+             Log.debugf 50 (fun k->k "pred = `%s`" (FM.Pred.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) ->
-               let pred = if Lit.sign lit then pred else FM.Pred.neg pred in
-               Log.debugf 50 (fun k->k "pred = `%s`" (FM.Pred.to_string pred));
-               if pred = Neq && not (T.Tbl.mem self.neq_encoded t) then (
-                 Some (lit, ta, tb)
-               ) else None
+             | (pred, _, _, ta, tb) -> check_pred pred ta tb
              | exception Not_found ->
                begin match A.view_as_lra t with
-                 | LRA_pred (Neq, a, b) when not (T.Tbl.mem self.neq_encoded t) ->
-                   Some (lit, a, b)
+                 | LRA_pred (pred, a, b) -> check_pred pred a b
                  | _ -> None
                end
            end)
@@ -246,19 +283,28 @@ module Make(A : ARG) : S with module A = A = struct
     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)";
     encode_neq self si acts trail;
     let fm = FM_A.create() in
     (* first, add definitions *)
     begin
-      List.iter
-        (fun (t,le) ->
+      T.Tbl.iter
+        (fun t le ->
            let open LE.Infix in
            let c = FM_A.Constr.mk ?tag:None Eq (LE.var t) le in
            FM_A.assert_c fm c)
         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 = FM_A.Constr.mk ~tag:(Tag.CC_eq (n1,n2)) Eq t1 t2 in
+         FM_A.assert_c fm c);
     (* add trail *)
     begin
       trail
@@ -266,16 +312,25 @@ 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 FM.Pred.neg pred in
+             if pred = Neq then (
+               Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
+             ) else (
+               let c = FM_A.Constr.mk ~tag:(Tag.Lit lit) pred a b in
+               FM_A.assert_c fm c;
+             )
+           in
            begin match T.Tbl.find self.pred_defs t with
-             | exception Not_found -> ()
-             | (pred, a, b, _, _) ->
-               let pred = if sign then pred else FM.Pred.neg pred in
-               if pred = Neq then (
-                 Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
-               ) else (
-                 let c = FM_A.Constr.mk ~tag:lit pred a b in
-                 FM_A.assert_c fm c;
-               )
+             | (pred, a, b, _, _) -> assert_pred pred a b
+             | exception Not_found ->
+               begin match A.view_as_lra t with
+                 | LRA_pred (pred, a, b) ->
+                   let a = try T.Tbl.find self.t_defs a with _ -> as_linexp_id a in
+                   let b = try T.Tbl.find self.t_defs b with _ -> as_linexp_id b in
+                   assert_pred pred a b
+                 | _ -> ()
+               end
            end)
     end;
     Log.debug 5 "lra: call arith solver";
@@ -286,14 +341,56 @@ module Make(A : ARG) : S with module A = A = struct
           (fun k->k "(@[LRA.needs-th-combination:@ %a@])"
               (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
         Log.debugf 30 (fun k->k "(@[LRA.model@ %a@])" FM_A.pp_model model);
-        () (* TODO: get a model + model combination *)
-      | FM_A.Unsat lits ->
+
+        (* 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;
+        ()
+      | FM_A.Unsat tags ->
         (* we tagged assertions with their lit, so the certificate being an
            unsat core translates directly into a conflict clause *)
         Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
-                         (Fmt.Dump.list Lit.pp) lits);
+                         (Fmt.Dump.list Tag.pp) tags);
         let confl =
-          List.rev_map Lit.neg lits |> dedup_lits
+          tags
+          |> CCList.flat_map (fun t -> Tag.to_lits si t)
+          |> List.rev_map Lit.neg
+          |> dedup_lits
         in
         (* TODO: produce and store a proper LRA resolution proof *)
         SI.raise_conflict si acts confl SI.P.default
@@ -306,6 +403,11 @@ module Make(A : ARG) : S with module A = A = struct
     (* TODO    SI.add_simplifier si (simplify st); *)
     SI.add_preprocess si (preproc_lra 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
@@ -313,6 +415,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
diff --git a/src/arith/lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml
index 56d3cf4f..43707e48 100644
--- a/src/arith/lra/fourier_motzkin.ml
+++ b/src/arith/lra/fourier_motzkin.ml
@@ -87,6 +87,7 @@ module type S = sig
   type model
 
   val get_model : model -> term -> Q.t
+  val eval_model : model -> LE.t -> Q.t
   val pp_model : model Fmt.printer
 
   type res =
@@ -320,19 +321,23 @@ module Make(A : ARG)
       (Fmt.Dump.list Constr.pp) self.empties
       (Util.pp_iter pp_idxkv) (T_map.to_iter self.idx)
 
-  (* TODO: be able to provide a model for SAT *)
   let build_model_ (self:pre_model) : _ T_map.t =
-    let l = T_map.to_iter self |> Iter.to_rev_list in
+    (* order matters: we need to compute values for lowest variables first *)
+    let l = T_map.to_iter self |> Iter.to_list in
+    (* INVARIANT: assert (CCList.is_sorted ~cmp:(fun (a,_) (b,_) -> T.compare a b) l); *)
 
     let m = ref T_map.empty in
 
     (* how to evaluate a linexpr in the model *)
-    let eval_le (le:LE.t) : Q.t =
+    let eval_le ~for_v (le:LE.t) : Q.t =
       let find x =
+        assert (T.compare for_v x > 0);
         try T_map.find x !m
         with Not_found ->
+          Log.debugf 50 (fun k->k "LRA.model: add default value for %a" T.pp x);
           m := T_map.add x Q.zero !m; (* remember this choice *)
-          Q.zero in
+          Q.zero
+      in
       T_map.to_iter le.LE.le
       |> Iter.fold
         (fun sum (t,coeff) -> Q.(sum + coeff * find t))
@@ -355,12 +360,13 @@ module Make(A : ARG)
       begin fun (v,cs_v) ->
         (* update [v] using its constraints [cs_v].
            [m] is the model to update *)
+        Log.debugf 40 (fun k->k "LRA.model: compute value for %a" T.pp v);
         let val_v =
           match cs_v with
-          | lazy (PM_eq le) -> eval_le le
+          | lazy (PM_eq le) -> eval_le ~for_v:v le
           | lazy (PM_bounds {lower; upper}) ->
-            let lower = List.map (fun (s,le) -> s, eval_le le) lower in
-            let upper = List.map (fun (s,le) -> s, eval_le le) upper in
+            let lower = List.map (fun (s,le) -> s, eval_le ~for_v:v le) lower in
+            let upper = List.map (fun (s,le) -> s, eval_le ~for_v:v le) upper in
             let strict_low, lower = match lower with
               | [] -> NonStrict, Q.minus_inf
               | x :: l -> List.fold_left max_pair x l
@@ -383,7 +389,10 @@ module Make(A : ARG)
               Q.zero (* no bounds *)
             )
         in
-        assert (not (T_map.mem v !m)); (* by ordering *)
+        if T_map.mem v !m then (
+          (* error: by ordering [v] should not have been touched yet *)
+          Error.errorf "LRA.build-model: variable %a already has a value" T.pp v
+        );
         m := T_map.add v val_v !m;
       end
       l;
@@ -394,6 +403,12 @@ module Make(A : ARG)
     try T_map.find v m
     with Not_found -> Q.zero
 
+  let eval_model m (le:LE.t) : Q.t =
+    T_map.fold
+      (fun v coeff sum ->
+         Q.(sum + coeff * get_model m v))
+      le.LE.le le.LE.const
+
   let pp_model out (m:model) : unit =
     let lazy m = m in
     let pp_pair out (v,q) = Fmt.fprintf out "(@[%a@ %a@])" T.pp v Q.pp_print q in

From 9d579af235df7004a0586a8ee65b7adad8112283 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 21 Dec 2020 16:15:49 -0500
Subject: [PATCH 13/13] wip: make lazyness of model explicit

---
 src/arith/lra/Sidekick_arith_lra.ml |  1 +
 src/arith/lra/fourier_motzkin.ml    | 37 ++++++++++++++++++++++-------
 2 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/src/arith/lra/Sidekick_arith_lra.ml b/src/arith/lra/Sidekick_arith_lra.ml
index 77e72195..aae635f4 100644
--- a/src/arith/lra/Sidekick_arith_lra.ml
+++ b/src/arith/lra/Sidekick_arith_lra.ml
@@ -340,6 +340,7 @@ module Make(A : ARG) : S with module A = A = struct
         Log.debugf 50
           (fun k->k "(@[LRA.needs-th-combination:@ %a@])"
               (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
+        let lazy model = model in
         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]
diff --git a/src/arith/lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml
index 43707e48..ddf35768 100644
--- a/src/arith/lra/fourier_motzkin.ml
+++ b/src/arith/lra/fourier_motzkin.ml
@@ -91,7 +91,7 @@ module type S = sig
   val pp_model : model Fmt.printer
 
   type res =
-    | Sat of model
+    | Sat of model lazy_t
     | Unsat of A.tag list
 
   val solve : t -> res
@@ -183,7 +183,9 @@ module Make(A : ARG)
       let pp_sum out le =
         (Util.pp_iter ~sep:" + " pp_pair) out (M.to_iter le)
       in
-      if Q.sign self.const = 0 then (
+      if T_map.is_empty self.le then (
+        Q.pp_print out self.const
+      ) else if Q.sign self.const = 0 then (
         Fmt.fprintf out "(@[%a@])" pp_sum self.le
       ) else (
         Fmt.fprintf out "(@[%a@ + %a@])" Q.pp_print self.const pp_sum self.le
@@ -250,7 +252,7 @@ module Make(A : ARG)
       }
 
   type pre_model = pre_model_constr lazy_t T_map.t
-  type model = Q.t T_map.t lazy_t
+  type model = Q.t T_map.t
 
   type system = {
     empties: Constr.t list; (* no variables, check first *)
@@ -321,6 +323,23 @@ module Make(A : ARG)
       (Fmt.Dump.list Constr.pp) self.empties
       (Util.pp_iter pp_idxkv) (T_map.to_iter self.idx)
 
+  let pp_pre_model_strict out = function
+    | Strict -> Fmt.string out "strict"
+    | NonStrict -> Fmt.string out "non-strict"
+
+  let pp_pre_model_constr out (m:pre_model_constr) : unit =
+    match m with
+    | PM_eq le -> Fmt.fprintf out "(@[eq@ %a@])" LE.pp le
+    | PM_bounds {lower;upper} ->
+      Fmt.fprintf out "(@[bounds@ :lower %a@ :upper %a@])"
+        Fmt.Dump.(list @@ pair pp_pre_model_strict LE.pp) lower
+        Fmt.Dump.(list @@ pair pp_pre_model_strict LE.pp) upper
+
+  let pp_pre_model out (m:pre_model) : unit =
+    Fmt.fprintf out "(@[pre-model@ %a@])"
+      (Util.pp_iter @@ Fmt.Dump.pair T.pp (Fmt.map Lazy.force pp_pre_model_constr))
+      (T_map.to_iter m)
+
   let build_model_ (self:pre_model) : _ T_map.t =
     (* order matters: we need to compute values for lowest variables first *)
     let l = T_map.to_iter self |> Iter.to_list in
@@ -361,6 +380,7 @@ module Make(A : ARG)
         (* update [v] using its constraints [cs_v].
            [m] is the model to update *)
         Log.debugf 40 (fun k->k "LRA.model: compute value for %a" T.pp v);
+        Format.printf "(@[<2>pre-model@ :t %a@ :constr %a@])@." T.pp v pp_pre_model_constr (Lazy.force cs_v);
         let val_v =
           match cs_v with
           | lazy (PM_eq le) -> eval_le ~for_v:v le
@@ -374,6 +394,7 @@ module Make(A : ARG)
               | [] -> NonStrict, Q.inf
               | x :: l -> List.fold_left min_pair x l
             in
+            Format.printf "lower=%a, upper=%a@." Q.pp_print lower Q.pp_print upper;
             if Q.is_real lower && Q.is_real upper then (
               if Q.equal lower upper then (
                 assert (strict_low=NonStrict && strict_up=NonStrict); (* unsat otherwise *)
@@ -382,9 +403,9 @@ module Make(A : ARG)
                 Q.((lower + upper) / of_int 2) (* middle *)
               )
             ) else if Q.is_real lower then (
-              if strict_low=Strict then Q.(lower + one) else lower
+              if strict_low=Strict then Q.(lower + ~$ 1) else lower
             ) else if Q.is_real upper then (
-              if strict_up=Strict then Q.(upper - one) else upper
+              if strict_up=Strict then Q.(upper - ~$ 1) else upper
             ) else (
               Q.zero (* no bounds *)
             )
@@ -394,12 +415,12 @@ module Make(A : ARG)
           Error.errorf "LRA.build-model: variable %a already has a value" T.pp v
         );
         m := T_map.add v val_v !m;
+        Log.debugf 40 (fun k->k "LRA.model: value for %a is %a" T.pp v Q.pp_print val_v);
       end
       l;
     !m
 
   let get_model (m:model) (v:T.t) : Q.t =
-    let lazy m = m in
     try T_map.find v m
     with Not_found -> Q.zero
 
@@ -410,13 +431,12 @@ module Make(A : ARG)
       le.LE.le le.LE.const
 
   let pp_model out (m:model) : unit =
-    let lazy m = m in
     let pp_pair out (v,q) = Fmt.fprintf out "(@[%a@ %a@])" T.pp v Q.pp_print q in
     Fmt.fprintf out "(@[<hv1>model@ %a@])"
       (Util.pp_iter pp_pair) (T_map.to_iter m)
 
   type res =
-    | Sat of model
+    | Sat of model lazy_t
     | Unsat of A.tag list
 
   (* replace [x] with [by] inside [le] *)
@@ -489,6 +509,7 @@ module Make(A : ARG)
             |> Iter.of_list
             |> Iter.flatten
             |> Iter.map (subst_constr v ~tag:c0.Constr.tag ~by:rhs)
+            (* |> CCFun.tap (fun i -> Fmt.printf "@[<hv4>add constrs@ %a@]@." (Util.pp_iter Constr.pp) i) *)
             |> Iter.fold add_sys sys
           in