add LRA_term to base

src/base/Arith_types_.ml

@@ -14,6 +14,8 @@ module LRA_pred = struct
     | Gt -> ">"
     | Geq -> ">="
 
+  let equal : t -> t -> bool = ( = )
+  let hash : t -> int = Hashtbl.hash
   let pp out p = Fmt.string out (to_string p)
 end
 
@@ -24,63 +26,61 @@ module LRA_op = struct
     | Plus -> "+"
     | Minus -> "-"
 
+  let equal : t -> t -> bool = ( = )
+  let hash : t -> int = Hashtbl.hash
   let pp out p = Fmt.string out (to_string p)
 end
 
 module LRA_view = struct
-  type 'a t =
+  include Sidekick_th_lra
-    | Pred of LRA_pred.t * 'a * 'a
+
-    | Op of LRA_op.t * 'a * 'a
+  type 'a t = (Q.t, 'a) lra_view
-    | Mult of Q.t * 'a
-    | Const of Q.t
-    | Var of 'a
-    | To_real of 'a
 
   let map ~f_c f (l : _ t) : _ t =
     match l with
-    | Pred (p, a, b) -> Pred (p, f a, f b)
+    | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b)
-    | Op (p, a, b) -> Op (p, f a, f b)
+    | LRA_op (p, a, b) -> LRA_op (p, f a, f b)
-    | Mult (n, a) -> Mult (f_c n, f a)
+    | LRA_mult (n, a) -> LRA_mult (f_c n, f a)
-    | Const c -> Const (f_c c)
+    | LRA_const c -> LRA_const (f_c c)
-    | Var x -> Var (f x)
+    | LRA_other x -> LRA_other (f x)
-    | To_real x -> To_real (f x)
 
   let iter f l : unit =
     match l with
-    | Pred (_, a, b) | Op (_, a, b) ->
+    | LRA_pred (_, a, b) | LRA_op (_, a, b) ->
       f a;
       f b
-    | Mult (_, x) | Var x | To_real x -> f x
+    | LRA_mult (_, x) | LRA_other x -> f x
-    | Const _ -> ()
+    | LRA_const _ -> ()
 
   let pp ~pp_t out = function
-    | Pred (p, a, b) ->
+    | LRA_pred (p, a, b) ->
       Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_pred.to_string p) pp_t a pp_t b
-    | Op (p, a, b) ->
+    | LRA_op (p, a, b) ->
       Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_op.to_string p) pp_t a pp_t b
-    | Mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Q.pp_print n pp_t x
+    | LRA_mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Q.pp_print n pp_t x
-    | Const q -> Q.pp_print out q
+    | LRA_const q -> Q.pp_print out q
-    | Var x -> pp_t out x
+    | LRA_other x -> pp_t out x
-    | To_real x -> Fmt.fprintf out "(@[to_real@ %a@])" pp_t x
 
   let hash ~sub_hash = function
-    | Pred (p, a, b) -> Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
+    | LRA_pred (p, a, b) ->
-    | Op (p, a, b) -> Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
+      Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
-    | Mult (n, x) -> Hash.combine3 83 (hash_q n) (sub_hash x)
+    | LRA_op (p, a, b) ->
-    | Const q -> Hash.combine2 84 (hash_q q)
+      Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
-    | Var x -> sub_hash x
+    | LRA_mult (n, x) -> Hash.combine3 83 (hash_q n) (sub_hash x)
-    | To_real x -> Hash.combine2 85 (sub_hash x)
+    | LRA_const q -> Hash.combine2 84 (hash_q q)
+    | LRA_other x -> sub_hash x
 
   let equal ~sub_eq l1 l2 =
     match l1, l2 with
-    | Pred (p1, a1, b1), Pred (p2, a2, b2) ->
+    | LRA_pred (p1, a1, b1), LRA_pred (p2, a2, b2) ->
       p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
-    | Op (p1, a1, b1), Op (p2, a2, b2) ->
+    | LRA_op (p1, a1, b1), LRA_op (p2, a2, b2) ->
       p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
-    | Const a1, Const a2 -> Q.equal a1 a2
+    | LRA_const a1, LRA_const a2 -> Q.equal a1 a2
-    | Mult (n1, x1), Mult (n2, x2) -> Q.equal n1 n2 && sub_eq x1 x2
+    | LRA_mult (n1, x1), LRA_mult (n2, x2) -> Q.equal n1 n2 && sub_eq x1 x2
-    | Var x1, Var x2 | To_real x1, To_real x2 -> sub_eq x1 x2
+    | LRA_other x1, LRA_other x2 -> sub_eq x1 x2
-    | (Pred _ | Op _ | Const _ | Mult _ | Var _ | To_real _), _ -> false
+    | (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_other _), _ ->
+      false
 end
 
 module LIA_pred = LRA_pred
@@ -88,61 +88,64 @@ module LIA_op = LRA_op
 
 module LIA_view = struct
   type 'a t =
-    | Pred of LIA_pred.t * 'a * 'a
+    | LRA_pred of LIA_pred.t * 'a * 'a
-    | Op of LIA_op.t * 'a * 'a
+    | LRA_op of LIA_op.t * 'a * 'a
-    | Mult of Z.t * 'a
+    | LRA_mult of Z.t * 'a
-    | Const of Z.t
+    | LRA_const of Z.t
-    | Var of 'a
+    | LRA_other of 'a
 
   let map ~f_c f (l : _ t) : _ t =
     match l with
-    | Pred (p, a, b) -> Pred (p, f a, f b)
+    | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b)
-    | Op (p, a, b) -> Op (p, f a, f b)
+    | LRA_op (p, a, b) -> LRA_op (p, f a, f b)
-    | Mult (n, a) -> Mult (f_c n, f a)
+    | LRA_mult (n, a) -> LRA_mult (f_c n, f a)
-    | Const c -> Const (f_c c)
+    | LRA_const c -> LRA_const (f_c c)
-    | Var x -> Var (f x)
+    | LRA_other x -> LRA_other (f x)
 
   let iter f l : unit =
     match l with
-    | Pred (_, a, b) | Op (_, a, b) ->
+    | LRA_pred (_, a, b) | LRA_op (_, a, b) ->
       f a;
       f b
-    | Mult (_, x) | Var x -> f x
+    | LRA_mult (_, x) | LRA_other x -> f x
-    | Const _ -> ()
+    | LRA_const _ -> ()
 
   let pp ~pp_t out = function
-    | Pred (p, a, b) ->
+    | LRA_pred (p, a, b) ->
       Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_pred.to_string p) pp_t a pp_t b
-    | Op (p, a, b) ->
+    | LRA_op (p, a, b) ->
       Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_op.to_string p) pp_t a pp_t b
-    | Mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Z.pp_print n pp_t x
+    | LRA_mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Z.pp_print n pp_t x
-    | Const n -> Z.pp_print out n
+    | LRA_const n -> Z.pp_print out n
-    | Var x -> pp_t out x
+    | LRA_other x -> pp_t out x
 
   let hash ~sub_hash = function
-    | Pred (p, a, b) -> Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
+    | LRA_pred (p, a, b) ->
-    | Op (p, a, b) -> Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
+      Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
-    | Mult (n, x) -> Hash.combine3 83 (hash_z n) (sub_hash x)
+    | LRA_op (p, a, b) ->
-    | Const n -> Hash.combine2 84 (hash_z n)
+      Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
-    | Var x -> sub_hash x
+    | LRA_mult (n, x) -> Hash.combine3 83 (hash_z n) (sub_hash x)
+    | LRA_const n -> Hash.combine2 84 (hash_z n)
+    | LRA_other x -> sub_hash x
 
   let equal ~sub_eq l1 l2 =
     match l1, l2 with
-    | Pred (p1, a1, b1), Pred (p2, a2, b2) ->
+    | LRA_pred (p1, a1, b1), LRA_pred (p2, a2, b2) ->
       p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
-    | Op (p1, a1, b1), Op (p2, a2, b2) ->
+    | LRA_op (p1, a1, b1), LRA_op (p2, a2, b2) ->
       p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
-    | Const a1, Const a2 -> Z.equal a1 a2
+    | LRA_const a1, LRA_const a2 -> Z.equal a1 a2
-    | Mult (n1, x1), Mult (n2, x2) -> Z.equal n1 n2 && sub_eq x1 x2
+    | LRA_mult (n1, x1), LRA_mult (n2, x2) -> Z.equal n1 n2 && sub_eq x1 x2
-    | Var x1, Var x2 -> sub_eq x1 x2
+    | LRA_other x1, LRA_other x2 -> sub_eq x1 x2
-    | (Pred _ | Op _ | Const _ | Mult _ | Var _), _ -> false
+    | (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_other _), _ ->
+      false
 
   (* convert the whole structure to reals *)
   let to_lra f l : _ LRA_view.t =
     match l with
-    | Pred (p, a, b) -> LRA_view.Pred (p, f a, f b)
+    | LRA_pred (p, a, b) -> LRA_view.LRA_pred (p, f a, f b)
-    | Op (op, a, b) -> LRA_view.Op (op, f a, f b)
+    | LRA_op (op, a, b) -> LRA_view.LRA_op (op, f a, f b)
-    | Mult (c, x) -> LRA_view.Mult (Q.of_bigint c, f x)
+    | LRA_mult (c, x) -> LRA_view.LRA_mult (Q.of_bigint c, f x)
-    | Const x -> LRA_view.Const (Q.of_bigint x)
+    | LRA_const x -> LRA_view.LRA_const (Q.of_bigint x)
-    | Var v -> LRA_view.Var (f v)
+    | LRA_other v -> LRA_view.LRA_other (f v)
 end

src/base/LRA_term.ml

@@ -0,0 +1,63 @@
+open Sidekick_core
+module Pred = Arith_types_.LRA_pred
+module Op = Arith_types_.LRA_op
+module View = Arith_types_.LRA_view
+module T = Term
+
+type term = Term.t
+type ty = Term.t
+type Const.view += Const of Q.t | Pred of Pred.t | Op of Op.t | Mult_by of Q.t
+
+let ops : Const.ops =
+  (module struct
+    let pp out = function
+      | Const q -> Q.pp_print out q
+      | Pred p -> Pred.pp out p
+      | Op o -> Op.pp out o
+      | Mult_by q -> Fmt.fprintf out "(* %a)" Q.pp_print q
+      | _ -> assert false
+
+    let equal a b =
+      match a, b with
+      | Const a, Const b -> Q.equal a b
+      | Pred a, Pred b -> Pred.equal a b
+      | Op a, Op b -> Op.equal a b
+      | Mult_by a, Mult_by b -> Q.equal a b
+      | _ -> false
+
+    let hash = function
+      | Const q -> Sidekick_zarith.Rational.hash q
+      | Pred p -> Pred.hash p
+      | Op o -> Op.hash o
+      | Mult_by q -> Hash.(combine2 135 (Sidekick_zarith.Rational.hash q))
+      | _ -> assert false
+  end)
+
+let real tst = Ty.real tst
+
+let const tst q : term =
+  Term.const tst (Const.make (Const q) ops ~ty:(real tst))
+
+let mult_by tst q t : term =
+  let ty_c = Term.arrow tst (real tst) (real tst) in
+  let c = Term.const tst (Const.make (Mult_by q) ops ~ty:ty_c) in
+  Term.app tst c t
+
+let pred tst p t1 t2 : term =
+  let ty = Term.(arrow_l tst [ real tst; real tst ] (Term.bool tst)) in
+  let p = Term.const tst (Const.make (Pred p) ops ~ty) in
+  Term.app_l tst p [ t1; t2 ]
+
+let op tst op t1 t2 : term =
+  let ty = Term.(arrow_l tst [ real tst; real tst ] (real tst)) in
+  let p = Term.const tst (Const.make (Op op) ops ~ty) in
+  Term.app_l tst p [ t1; t2 ]
+
+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 = 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

src/base/LRA_term.mli

@@ -0,0 +1,16 @@
+open Sidekick_core
+module Pred = Arith_types_.LRA_pred
+module Op = Arith_types_.LRA_op
+module View = Arith_types_.LRA_view
+
+type term = Term.t
+type ty = Term.t
+
+val real : Term.store -> ty
+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
+val const : Term.store -> Q.t -> term
+
+val view : term -> term View.t
+(** View as LRA *)

src/base/Sidekick_base.ml

@@ -30,6 +30,7 @@ module Statement = Statement
 module Solver = Solver
 module Uconst = Uconst
 module Config = Config
+module LRA_term = LRA_term
 module Th_data = Th_data
 module Th_bool = Th_bool
 (* FIXME