feat: reinstate LRA theory and terms

src/base/Form.ml

@@ -1,8 +1,6 @@
-open Types_
 open Sidekick_core
 module T = Term
 
-type ty = Term.t
 type term = Term.t
 
 type 'a view = 'a Sidekick_core.Bool_view.t =
@@ -42,8 +40,6 @@ let ops : Const.ops =
 
 (* ### view *)
 
-exception Not_a_th_term
-
 let view (t : T.t) : T.t view =
   let hd, args = T.unfold_app t in
   match T.view hd, args with

src/base/LRA_term.ml

@@ -34,6 +34,7 @@ let ops : Const.ops =
   end)
 
 let real tst = Ty.real tst
+let has_ty_real t = Ty.is_real (T.ty t)
 
 let const tst q : term =
   Term.const tst (Const.make (Const q) ops ~ty:(real tst))
@@ -56,8 +57,17 @@ let op tst op t1 t2 : term =
 let view (t : term) : _ View.t =
   let f, args = Term.unfold_app t in
   match T.view f, args with
+  | T.E_const { Const.c_view = T.C_eq; _ }, [ _; a; b ] when has_ty_real a ->
+    View.LRA_pred (Pred.Eq, a, b)
   | T.E_const { Const.c_view = Const q; _ }, [] -> View.LRA_const q
   | T.E_const { Const.c_view = Pred p; _ }, [ a; b ] -> View.LRA_pred (p, a, b)
   | T.E_const { Const.c_view = Op op; _ }, [ a; b ] -> View.LRA_op (op, a, b)
   | T.E_const { Const.c_view = Mult_by q; _ }, [ a ] -> View.LRA_mult (q, a)
   | _ -> View.LRA_other t
+
+let term_of_view store = function
+  | View.LRA_const q -> const store q
+  | View.LRA_mult (n, t) -> mult_by store n t
+  | View.LRA_pred (p, a, b) -> pred store p a b
+  | View.LRA_op (o, a, b) -> op store o a b
+  | View.LRA_other x -> x

src/base/LRA_term.mli

@@ -7,6 +7,7 @@ type term = Term.t
 type ty = Term.t
 
 val real : Term.store -> ty
+val has_ty_real : term -> bool
 val pred : Term.store -> Pred.t -> term -> term -> term
 val mult_by : Term.store -> Q.t -> term -> term
 val op : Term.store -> Op.t -> term -> term -> term
@@ -14,3 +15,5 @@ val const : Term.store -> Q.t -> term
 
 val view : term -> term View.t
 (** View as LRA *)
+
+val term_of_view : Term.store -> term View.t -> term

src/base/Sidekick_base.ml

@@ -33,35 +33,11 @@ module Config = Config
 module LRA_term = LRA_term
 module Th_data = Th_data
 module Th_bool = Th_bool
-(* FIXME
+module Th_lra = Th_lra
-   module Th_lra = Th_lra
-*)
 
 let k_th_bool_config = Th_bool.k_config
 let th_bool = Th_bool.theory
 let th_bool_dyn : Solver.theory = Th_bool.theory_dyn
 let th_bool_static : Solver.theory = Th_bool.theory_static
 let th_data : Solver.theory = Th_data.theory
-
+let th_lra : Solver.theory = Th_lra.theory
-(* FIXME
-   let th_lra : Solver.theory = Th_lra.theory
-*)
-
-(* TODO
-
-   module Value = Value
-   module Statement = Statement
-   module Data = Data
-   module Select = Select
-
-      module LRA_view = Types_.LRA_view
-      module LRA_pred = Base_types.LRA_pred
-      module LRA_op = Base_types.LRA_op
-      module LIA_view = Base_types.LIA_view
-      module LIA_pred = Base_types.LIA_pred
-      module LIA_op = Base_types.LIA_op
-*)
-
-(*
-module Proof_quip = Proof_quip
-*)

src/base/th_lra.ml

@@ -1,48 +1,21 @@
-(* TODO
+(** Theory of Linear Rational Arithmetic *)
 
+open Sidekick_core
+module T = Term
+module Q = Sidekick_zarith.Rational
+open LRA_term
 
-   (** Theory of Linear Rational Arithmetic *)
+let mk_eq = Form.eq
-   module Th_lra = Sidekick_arith_lra.Make (struct
+let mk_bool = T.bool
-     module S = Solver
-     module T = Term
-     module Z = Sidekick_zarith.Int
-     module Q = Sidekick_zarith.Rational
 
-     type term = S.T.Term.t
+let theory : Solver.theory =
-     type ty = S.T.Ty.t
+  Sidekick_th_lra.theory
+    (module struct
+      module Z = Sidekick_zarith.Int
+      module Q = Sidekick_zarith.Rational
 
-     module LRA = Sidekick_arith_lra
+      let ty_real = LRA_term.real
-
+      let has_ty_real = LRA_term.has_ty_real
-     let mk_eq = Form.eq
+      let view_as_lra = LRA_term.view
-
+      let mk_lra = LRA_term.term_of_view
-     let mk_lra store l =
+    end : Sidekick_th_lra.ARG)
-       match l with
-       | LRA.LRA_other x -> x
-       | LRA.LRA_pred (p, x, y) -> T.lra store (Pred (p, x, y))
-       | LRA.LRA_op (op, x, y) -> T.lra store (Op (op, x, y))
-       | LRA.LRA_const c -> T.lra store (Const c)
-       | LRA.LRA_mult (c, x) -> T.lra store (Mult (c, x))
-
-     let mk_bool = T.bool
-
-     let rec view_as_lra t =
-       match T.view t with
-       | T.LRA l ->
-         let module LRA = Sidekick_arith_lra in
-         (match l with
-         | Const c -> LRA.LRA_const c
-         | Pred (p, a, b) -> LRA.LRA_pred (p, a, b)
-         | Op (op, a, b) -> LRA.LRA_op (op, a, b)
-         | Mult (c, x) -> LRA.LRA_mult (c, x)
-         | To_real x -> view_as_lra x
-         | Var x -> LRA.LRA_other x)
-       | T.Eq (a, b) when Ty.equal (T.ty a) (Ty.real ()) -> LRA.LRA_pred (Eq, a, b)
-       | _ -> LRA.LRA_other t
-
-     let ty_lra _st = Ty.real ()
-     let has_ty_real t = Ty.equal (T.ty t) (Ty.real ())
-     let lemma_lra = Proof.lemma_lra
-
-     module Gensym = Gensym
-   end)
-*)

src/main/main.ml

@@ -178,8 +178,7 @@ let main_smt ~config () : _ result =
       Log.debugf 1 (fun k ->
           k "(@[main.th-bool.pick@ %S@])"
             (Sidekick_smt_solver.Theory.name th_bool));
-      Sidekick_smt_solver.Theory.
+      Sidekick_smt_solver.Theory.[ th_bool; Process.th_data; Process.th_lra ]
-        [ th_bool; Process.th_data (* FIXME Process.th_lra *) ]
     in
     Process.Solver.create_default ~proof ~theories tst
   in

src/smtlib/Process.ml

@@ -338,14 +338,10 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model
 
 module Th_data = Sidekick_base.Th_data
 module Th_bool = Sidekick_base.Th_bool
-(* FIXME
+module Th_lra = Sidekick_base.Th_lra
-   module Th_lra = Sidekick_base.Th_lra
-*)
 
 let th_bool = Th_bool.theory
 let th_bool_dyn : Solver.theory = Th_bool.theory_dyn
 let th_bool_static : Solver.theory = Th_bool.theory_static
 let th_data : Solver.theory = Th_data.theory
-(* FIXME
+let th_lra : Solver.theory = Th_lra.theory
-   let th_lra : Solver.theory = Th_lra.theory
-*)

src/smtlib/Process.mli

@@ -7,9 +7,7 @@ val th_bool_dyn : Solver.theory
 val th_bool_static : Solver.theory
 val th_bool : Config.t -> Solver.theory
 val th_data : Solver.theory
-(* FIXME
+val th_lra : Solver.theory
-   val th_lra : Solver.theory
-*)
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/Typecheck.ml

@@ -113,59 +113,84 @@ let string_as_q (s : string) : Q.t option =
     Some x
   with _ -> None
 
-(* TODO
+let t_as_q t =
-   let t_as_q t =
+  match LRA_term.view t with
-     match Term.view t with
+  | LRA_term.View.LRA_const n -> Some n
-     | T.LRA (Const n) -> Some n
+  (*
-     | T.LIA (Const n) -> Some (Q.of_bigint n)
+   | T.LIA (Const n) -> Some (Q.of_bigint n)
-     | _ -> None
+   *)
+  | _ -> None
 
+(* TODO
    let t_as_z t =
      match Term.view t with
      | T.LIA (Const n) -> Some n
      | _ -> None
+*)
 
-   let is_real = Ty.is_real
+let is_real = Ty.is_real
 
-   (* convert [t] to a real term *)
+(* convert [t] to a real term *)
-   let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t =
+let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t =
-     let rec conv t =
+  let conv t =
-       match T.view t with
+    match T.view t with
-       | T.LRA _ -> t
+    | _ when Ty.is_real (T.ty t) -> t
-       | _ when Ty.equal (T.ty t) (Ty.real ()) -> t
+    (* FIXME
        | T.LIA (Const n) -> T.lra ctx.tst (Const (Q.of_bigint n))
        | T.LIA l ->
          (* convert the whole structure to reals *)
          let l = LIA_view.to_lra conv l in
          T.lra ctx.tst l
        | T.Ite (a, b, c) -> T.ite ctx.tst a (conv b) (conv c)
-       | _ -> errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t
+    *)
-     in
+    | _ -> errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t
-     conv t
+  in
+  conv t
 
-   let conv_arith_op (ctx : Ctx.t) t (op : PA.arith_op) (l : T.t list) : T.t =
+let conv_arith_op (ctx : Ctx.t) (t : PA.term) (op : PA.arith_op) (l : T.t list)
-     let tst = ctx.Ctx.tst in
+    : T.t =
+  let tst = ctx.Ctx.tst in
 
-     let mk_pred p a b =
+  let mk_pred p a b =
+    LRA_term.pred tst p (cast_to_real ctx a) (cast_to_real ctx b)
+  (* TODO
+     if is_real a || is_real b then
+       LRA_term.pred tst p (cast_to_real ctx a) (cast_to_real ctx b)
+     else
+       Error.errorf "cannot handle LIA term %a" PA.pp_term t
+      T.lia tst (Pred (p, a, b))
+  *)
+  and mk_op o a b =
+    LRA_term.op tst o (cast_to_real ctx a) (cast_to_real ctx b)
+    (* TODO
        if is_real a || is_real b then
-         T.lra tst (Pred (p, cast_to_real ctx a, cast_to_real ctx b))
+         LRA_term.op tst o (cast_to_real ctx a) (cast_to_real ctx b)
        else
-         T.lia tst (Pred (p, a, b))
+         Error.errorf "cannot handle LIA term %a" PA.pp_term t
-     and mk_op o a b =
+          T.lia tst (Op (o, a, b))
-       if is_real a || is_real b then
+    *)
-         T.lra tst (Op (o, cast_to_real ctx a, cast_to_real ctx b))
+  in
-       else
-         T.lia tst (Op (o, a, b))
-     in
 
-     match op, l with
+  match op, l with
-     | PA.Leq, [ a; b ] -> mk_pred Leq a b
+  | PA.Leq, [ a; b ] -> mk_pred Leq a b
-     | PA.Lt, [ a; b ] -> mk_pred Lt a b
+  | PA.Lt, [ a; b ] -> mk_pred Lt a b
-     | PA.Geq, [ a; b ] -> mk_pred Geq a b
+  | PA.Geq, [ a; b ] -> mk_pred Geq a b
-     | PA.Gt, [ a; b ] -> mk_pred Gt a b
+  | PA.Gt, [ a; b ] -> mk_pred Gt a b
-     | PA.Add, [ a; b ] -> mk_op Plus a b
+  | PA.Add, [ a; b ] -> mk_op Plus a b
-     | PA.Add, a :: l -> List.fold_left (fun a b -> mk_op Plus a b) a l
+  | PA.Add, a :: l -> List.fold_left (fun a b -> mk_op Plus a b) a l
-     | PA.Minus, [ a ] ->
+  | PA.Minus, [ a ] ->
+    (match t_as_q a with
+    | Some q -> LRA_term.const tst (Q.neg q)
+    | None ->
+      let zero =
+        if is_real a then
+          LRA_term.const tst Q.zero
+        else
+          Error.errorf "cannot handle non-rat %a" PA.pp_term t
+        (* T.lia tst (Const Z.zero) *)
+      in
+      mk_op Minus zero a)
+    (*
        (match t_as_q a, t_as_z a with
        | _, Some n -> T.lia tst (Const (Z.neg n))
        | Some q, None -> T.lra tst (Const (Q.neg q))
@@ -176,57 +201,52 @@ let string_as_q (s : string) : Q.t option =
            else
              T.lia tst (Const Z.zero)
          in
-
          mk_op Minus zero a)
-     | PA.Minus, [ a; b ] -> mk_op Minus a b
+         *)
-     | PA.Minus, a :: l -> List.fold_left (fun a b -> mk_op Minus a b) a l
+  | PA.Minus, [ a; b ] -> mk_op Minus a b
-     | PA.Mult, [ a; b ] when is_real a || is_real b ->
+  | PA.Minus, a :: l -> List.fold_left (fun a b -> mk_op Minus a b) a l
-       (match t_as_q a, t_as_q b with
+  | PA.Mult, [ a; b ] ->
-       | Some a, Some b -> T.lra tst (Const (Q.mul a b))
+    (match t_as_q a, t_as_q b with
-       | Some a, _ -> T.lra tst (Mult (a, b))
+    | Some a, Some b -> LRA_term.const tst (Q.mul a b)
-       | _, Some b -> T.lra tst (Mult (b, a))
+    | Some a, _ -> LRA_term.mult_by tst a b
-       | None, None ->
+    | _, Some b -> LRA_term.mult_by tst b a
-         errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t)
+    | None, None ->
-     | PA.Mult, [ a; b ] ->
+      errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t)
-       (match t_as_z a, t_as_z b with
+    (* TODO
-       | Some a, Some b -> T.lia tst (Const (Z.mul a b))
+          | PA.Mult, [ _a; _b ] ->
-       | Some a, _ -> T.lia tst (Mult (a, b))
+               (match t_as_z a, t_as_z b with
-       | _, Some b -> T.lia tst (Mult (b, a))
+               | Some a, Some b -> T.lia tst (Const (Z.mul a b))
-       | None, None ->
+               | Some a, _ -> T.lia tst (Mult (a, b))
-         errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t)
+               | _, Some b -> T.lia tst (Mult (b, a))
-     | PA.Div, [ a; b ] when is_real a || is_real b ->
+               | None, None ->
-       (match t_as_q a, t_as_q b with
+                 errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t)
-       | Some a, Some b -> T.lra tst (Const (Q.div a b))
+       errorf_ctx ctx "cannot handle non-linear mult %a" PA.pp_term t
-       | _, Some b -> T.lra tst (Mult (Q.inv b, a))
+    *)
-       | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t)
+  | PA.Div, [ a; b ] ->
-     | PA.Div, [ a; b ] ->
+    (match t_as_q a, t_as_q b with
-       (* becomes a real *)
+    | Some a, Some b -> LRA_term.const tst (Q.div a b)
-       (match t_as_q a, t_as_q b with
+    | _, Some b ->
-       | Some a, Some b -> T.lra tst (Const (Q.div a b))
+      let a = cast_to_real ctx a in
-       | _, Some b ->
+      LRA_term.mult_by tst (Q.inv b) a
-         let a = cast_to_real ctx a in
+    | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t)
-         T.lra tst (Mult (Q.inv b, a))
+  | _ -> errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t
-       | _, None -> errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t)
-     | _ -> errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t
-*)
 
 (* conversion of terms *)
 let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t =
   let tst = ctx.Ctx.tst in
   match t with
   | PA.True -> T.true_ tst
-  | PA.False ->
+  | PA.False -> T.false_ tst
-    T.false_ tst
+  | PA.Const s when is_num s ->
-    (* FIXME
+    (match string_as_z s, ctx.default_num with
-       | PA.Const s when is_num s ->
+    | Some n, `Real -> LRA_term.const tst (Q.of_bigint n)
-         (match string_as_z s, ctx.default_num with
+    | Some n, `Int ->
-         | Some n, `Int -> T.lia tst (Const n)
+      Error.errorf "cannot handle integer constant %a yet" Z.pp_print n
-         | Some n, `Real -> T.lra tst (Const (Q.of_bigint n))
+      (* TODO T.lia tst (Const n) *)
-         | None, _ ->
+    | None, _ ->
-           (match string_as_q s with
+      (match string_as_q s with
-           | Some n -> T.lra tst (Const n)
+      | Some n -> LRA_term.const tst n
-           | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t))
+      | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t))
-    *)
   | PA.Const f | PA.App (f, []) ->
     (* lookup in `let` table, then in type defs *)
     (match StrTbl.find ctx.Ctx.lets f with
@@ -276,12 +296,12 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t =
   | PA.Eq (a, b) ->
     let a = conv_term ctx a in
     let b = conv_term ctx b in
-    (* FIXME
+    if is_real a || is_real b then
-       if is_real a || is_real b then
+      (* Form.eq tst (cast_to_real ctx a) (cast_to_real ctx b) *)
-         Form.eq tst (cast_to_real ctx a) (cast_to_real ctx b)
+      LRA_term.pred tst LRA_term.Pred.Eq (cast_to_real ctx a)
-       else
+        (cast_to_real ctx b)
-    *)
+    else
-    Form.eq tst a b
+      Form.eq tst a b
   | PA.Imply (a, b) ->
     let a = conv_term ctx a in
     let b = conv_term ctx b in
@@ -371,12 +391,9 @@ let rec conv_term (ctx : Ctx.t) (t : PA.term) : T.t =
         in
         A.match_ lhs cases
     *)
-
+  | PA.Arith (op, l) ->
-    (* FIXME
+    let l = List.map (conv_term ctx) l in
-       | PA.Arith (op, l) ->
+    conv_arith_op ctx t op l
-         let l = List.map (conv_term ctx) l in
-         conv_arith_op ctx t op l
-    *)
   | PA.Cast (t, ty_expect) ->
     let t = conv_term ctx t in
     let ty_expect = conv_ty ctx ty_expect in

src/th-lra/intf.ml

@@ -39,21 +39,9 @@ module type ARG = sig
   val mk_lra : Term.store -> (Q.t, Term.t) lra_view -> Term.t
   (** Make a Term.t from the given theory view *)
 
-  val ty_lra : Term.store -> ty
+  val ty_real : Term.store -> ty
+  (** Build the type Q *)
 
   val has_ty_real : Term.t -> bool
   (** Does this term have the type [Real] *)
-
-  val lemma_lra : Lit.t list -> Proof_term.t
-
-  module Gensym : sig
-    type t
-
-    val create : Term.store -> t
-    val tst : t -> Term.store
-    val copy : t -> t
-
-    val fresh_term : t -> pre:string -> ty -> term
-    (** Make a fresh term of the given type *)
-  end
 end

src/th-lra/proof_rules.ml

@@ -0,0 +1,3 @@
+open Sidekick_core
+
+let lemma_lra lits : Proof_term.t = Proof_term.apply_rule "lra.lemma" ~lits

src/th-lra/proof_rules.mli

@@ -0,0 +1,5 @@
+open Sidekick_core
+
+val lemma_lra : Lit.t list -> Proof_term.t
+(** List of literals [l1…ln] where [¬l1 /\ … /\ ¬ln] is LRA-unsat *)
+

src/th-lra/sidekick_th_lra.ml

@@ -126,7 +126,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
   type state = {
     tst: Term.store;
     proof: Proof_trace.t;
-    gensym: A.Gensym.t;
+    gensym: Gensym.t;
     in_model: unit Term.Tbl.t; (* terms to add to model *)
     encoded_eqs: unit Term.Tbl.t;
     (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
@@ -140,6 +140,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     mutable encoded_le: Term.t Comb_map.t; (* [le] -> var encoding [le] *)
     simplex: SimpSolver.t;
     mutable last_res: SimpSolver.result option;
+    n_propagate: int Stat.counter;
+    n_conflict: int Stat.counter;
   }
 
   let create (si : SI.t) : state =
@@ -151,7 +153,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       proof;
       in_model = Term.Tbl.create 8;
       st_exprs = ST_exprs.create_and_setup (SI.cc si);
-      gensym = A.Gensym.create tst;
+      gensym = Gensym.create tst;
       simp_preds = Term.Tbl.create 32;
       simp_defined = Term.Tbl.create 16;
       encoded_eqs = Term.Tbl.create 8;
@@ -159,6 +161,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       encoded_le = Comb_map.empty;
       simplex = SimpSolver.create ~stat ();
       last_res = None;
+      n_propagate = Stat.mk_int stat "th.lra.propagate";
+      n_conflict = Stat.mk_int stat "th.lra.conflicts";
     }
 
   let[@inline] reset_res_ (self : state) : unit = self.last_res <- None
@@ -175,7 +179,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     SimpSolver.pop_levels self.simplex n;
     ()
 
-  let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
+  let fresh_term self ~pre ty = Gensym.fresh_term self.gensym ~pre ty
 
   let fresh_lit (self : state) ~mk_lit ~pre : Lit.t =
     let t = fresh_term ~pre self (Term.bool self.tst) in
@@ -239,7 +243,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       | x -> x (* already encoded that *)
       | exception Not_found ->
         (* new variable to represent [le_comb] *)
-        let proxy = fresh_term self ~pre (A.ty_lra self.tst) in
+        let proxy = fresh_term self ~pre (A.ty_real self.tst) in
         (* TODO: define proxy *)
         self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le;
         Log.debugf 50 (fun k ->
@@ -251,7 +255,9 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         proxy)
 
   let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits =
-    let pr = Proof_trace.add_step PA.proof @@ fun () -> A.lemma_lra lits in
+    let pr =
+      Proof_trace.add_step PA.proof @@ fun () -> Proof_rules.lemma_lra lits
+    in
     let pr =
       match using with
       | None -> pr
@@ -281,7 +287,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       (match Comb_map.get le_comb self.encoded_le with
       | Some x -> x, A.Q.one (* already encoded that *)
       | None ->
-        let proxy = fresh_term self ~pre:"_le_comb" (A.ty_lra self.tst) in
+        let proxy = fresh_term self ~pre:"_le_comb" (A.ty_real self.tst) in
 
         self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le;
         LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
@@ -400,11 +406,11 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       (Term.t * Proof_step.id Iter.t) option =
     let proof_eq t u =
       Proof_trace.add_step self.proof @@ fun () ->
-      A.lemma_lra [ Lit.atom self.tst (Term.eq self.tst t u) ]
+      Proof_rules.lemma_lra [ Lit.atom self.tst (Term.eq self.tst t u) ]
     in
     let proof_bool t ~sign:b =
       let lit = Lit.atom ~sign:b self.tst t in
-      Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
+      Proof_trace.add_step self.proof @@ fun () -> Proof_rules.lemma_lra [ lit ]
     in
 
     match A.view_as_lra t with
@@ -462,7 +468,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     | _ -> None
 
   (* raise conflict from certificate *)
-  let fail_with_cert si acts cert : 'a =
+  let fail_with_cert (self : state) si acts cert : 'a =
     Profile.with1 "lra.simplex.check-cert" SimpSolver._check_cert cert;
     let confl =
       SimpSolver.Unsat_cert.lits cert
@@ -470,19 +476,22 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       |> List.rev_map Lit.neg
     in
     let pr =
-      Proof_trace.add_step (SI.proof si) @@ fun () -> A.lemma_lra confl
+      Proof_trace.add_step (SI.proof si) @@ fun () ->
+      Proof_rules.lemma_lra confl
     in
+    Stat.incr self.n_conflict;
     SI.raise_conflict si acts confl pr
 
-  let on_propagate_ si acts lit ~reason =
+  let on_propagate_ self si acts lit ~reason =
     match lit with
     | Tag.Lit lit ->
       (* TODO: more detailed proof certificate *)
+      Stat.incr self.n_propagate;
       SI.propagate si acts lit ~reason:(fun () ->
           let lits = CCList.flat_map (Tag.to_lits si) reason in
           let pr =
             Proof_trace.add_step (SI.proof si) @@ fun () ->
-            A.lemma_lra (lit :: lits)
+            Proof_rules.lemma_lra (lit :: lits)
           in
           CCList.flat_map (Tag.to_lits si) reason, pr)
     | _ -> ()
@@ -495,7 +504,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
           (SimpSolver.n_rows self.simplex));
     let res =
       Profile.with_ "lra.simplex.solve" @@ fun () ->
-      SimpSolver.check self.simplex ~on_propagate:(on_propagate_ si acts)
+      SimpSolver.check self.simplex ~on_propagate:(on_propagate_ self si acts)
     in
     Log.debug 5 "(lra.check-simplex.done)";
     self.last_res <- Some res;
@@ -504,7 +513,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     | SimpSolver.Unsat cert ->
       Log.debugf 10 (fun k ->
           k "(@[lra.check.unsat@ :cert %a@])" SimpSolver.Unsat_cert.pp cert);
-      fail_with_cert si acts cert
+      fail_with_cert self si acts cert
 
   (* TODO: trivial propagations *)
 
@@ -528,7 +537,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         (* [c=0] when [c] is not 0 *)
         let lit = Lit.atom ~sign:false self.tst @@ Term.eq self.tst t1 t2 in
         let pr =
-          Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
+          Proof_trace.add_step self.proof @@ fun () ->
+          Proof_rules.lemma_lra [ lit ]
         in
         SI.add_clause_permanent si acts [ lit ] pr
       )
@@ -537,11 +547,11 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       try
         let c1 = SimpSolver.Constraint.geq v le_const in
         SimpSolver.add_constraint self.simplex c1 tag
-          ~on_propagate:(on_propagate_ si acts);
+          ~on_propagate:(on_propagate_ self si acts);
         let c2 = SimpSolver.Constraint.leq v le_const in
         SimpSolver.add_constraint self.simplex c2 tag
-          ~on_propagate:(on_propagate_ si acts)
+          ~on_propagate:(on_propagate_ self si acts)
-      with SimpSolver.E_unsat cert -> fail_with_cert si acts cert
+      with SimpSolver.E_unsat cert -> fail_with_cert self si acts cert
     )
 
   let add_local_eq (self : state) si acts n1 n2 : unit =
@@ -627,12 +637,12 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         (try
            SimpSolver.add_var self.simplex v;
            SimpSolver.add_constraint self.simplex constr (Tag.Lit lit)
-             ~on_propagate:(on_propagate_ si acts)
+             ~on_propagate:(on_propagate_ self si acts)
          with SimpSolver.E_unsat cert ->
            Log.debugf 10 (fun k ->
                k "(@[lra.partial-check.unsat@ :cert %a@])"
                  SimpSolver.Unsat_cert.pp cert);
-           fail_with_cert si acts cert)
+           fail_with_cert self si acts cert)
       | None, LRA_pred (Eq, t1, t2) when sign ->
         add_local_eq_t self si acts t1 t2 ~tag:(Tag.Lit lit)
       | None, LRA_pred (Neq, t1, t2) when not sign ->

src/th-lra/sidekick_th_lra.mli

@@ -1,10 +1,30 @@
 (** Linear Rational Arithmetic *)
 
+open Sidekick_core
 module Intf = Intf
+module Predicate = Intf.Predicate
+module SMT = Sidekick_smt_solver
 
-include module type of struct
+module type INT = Intf.INT
-  include Intf
+module type RATIONAL = Intf.RATIONAL
-end
+
+module S_op = Sidekick_simplex.Op
+
+type term = Term.t
+type ty = Term.t
+type pred = Intf.pred = Leq | Geq | Lt | Gt | Eq | Neq
+type op = Intf.op = Plus | Minus
+
+type ('num, 'a) lra_view = ('num, 'a) Intf.lra_view =
+  | LRA_pred of pred * 'a * 'a
+  | LRA_op of op * 'a * 'a
+  | LRA_mult of 'num * 'a
+  | LRA_const of 'num
+  | LRA_other of 'a
+
+val map_view : ('a -> 'b) -> ('c, 'a) lra_view -> ('c, 'b) lra_view
+
+module type ARG = Intf.ARG
 
 (* TODO
    type state