From e03e5e77a929caa92ac55b1d0472a116cf2a7e29 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 25 Aug 2022 23:03:12 -0400 Subject: [PATCH] add LRA_term to base --- src/base/Arith_types_.ml | 139 +++++++++++++++++++------------------- src/base/LRA_term.ml | 63 +++++++++++++++++ src/base/LRA_term.mli | 16 +++++ src/base/Sidekick_base.ml | 1 + 4 files changed, 151 insertions(+), 68 deletions(-) create mode 100644 src/base/LRA_term.ml create mode 100644 src/base/LRA_term.mli diff --git a/src/base/Arith_types_.ml b/src/base/Arith_types_.ml index e244d13d..5691be2c 100644 --- a/src/base/Arith_types_.ml +++ b/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 = - | Pred of LRA_pred.t * 'a * 'a - | Op of LRA_op.t * 'a * 'a - | Mult of Q.t * 'a - | Const of Q.t - | Var of 'a - | To_real of 'a + include Sidekick_th_lra + + type 'a t = (Q.t, 'a) lra_view let map ~f_c f (l : _ t) : _ t = match l with - | Pred (p, a, b) -> Pred (p, f a, f b) - | Op (p, a, b) -> Op (p, f a, f b) - | Mult (n, a) -> Mult (f_c n, f a) - | Const c -> Const (f_c c) - | Var x -> Var (f x) - | To_real x -> To_real (f x) + | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b) + | LRA_op (p, a, b) -> LRA_op (p, f a, f b) + | LRA_mult (n, a) -> LRA_mult (f_c n, f a) + | LRA_const c -> LRA_const (f_c c) + | 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 | To_real x -> f x - | Const _ -> () + | LRA_mult (_, x) | LRA_other x -> f x + | 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 - | Const q -> Q.pp_print out q - | Var x -> pp_t out x - | To_real x -> Fmt.fprintf out "(@[to_real@ %a@])" pp_t x + | LRA_mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Q.pp_print n pp_t x + | LRA_const q -> Q.pp_print out q + | 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) - | Op (p, a, b) -> Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b) - | Mult (n, x) -> Hash.combine3 83 (hash_q n) (sub_hash x) - | Const q -> Hash.combine2 84 (hash_q q) - | Var x -> sub_hash x - | To_real x -> Hash.combine2 85 (sub_hash x) + | LRA_pred (p, a, b) -> + Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b) + | LRA_op (p, a, b) -> + Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b) + | LRA_mult (n, x) -> Hash.combine3 83 (hash_q n) (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 - | Mult (n1, x1), 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 - | (Pred _ | Op _ | Const _ | Mult _ | Var _ | To_real _), _ -> false + | LRA_const a1, LRA_const a2 -> Q.equal a1 a2 + | LRA_mult (n1, x1), LRA_mult (n2, x2) -> Q.equal n1 n2 && sub_eq x1 x2 + | LRA_other x1, LRA_other x2 -> sub_eq x1 x2 + | (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 - | Op of LIA_op.t * 'a * 'a - | Mult of Z.t * 'a - | Const of Z.t - | Var of 'a + | LRA_pred of LIA_pred.t * 'a * 'a + | LRA_op of LIA_op.t * 'a * 'a + | LRA_mult of Z.t * 'a + | LRA_const of Z.t + | 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) - | Op (p, a, b) -> Op (p, f a, f b) - | Mult (n, a) -> Mult (f_c n, f a) - | Const c -> Const (f_c c) - | Var x -> Var (f x) + | LRA_pred (p, a, b) -> LRA_pred (p, f a, f b) + | LRA_op (p, a, b) -> LRA_op (p, f a, f b) + | LRA_mult (n, a) -> LRA_mult (f_c n, f a) + | LRA_const c -> LRA_const (f_c c) + | 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 - | Const _ -> () + | LRA_mult (_, x) | LRA_other x -> f x + | 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 - | Const n -> Z.pp_print out n - | Var x -> pp_t out x + | LRA_mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Z.pp_print n pp_t x + | LRA_const n -> Z.pp_print out n + | 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) - | Op (p, a, b) -> Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b) - | Mult (n, x) -> Hash.combine3 83 (hash_z n) (sub_hash x) - | Const n -> Hash.combine2 84 (hash_z n) - | Var x -> sub_hash x + | LRA_pred (p, a, b) -> + Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b) + | LRA_op (p, a, b) -> + Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b) + | 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 - | Mult (n1, x1), Mult (n2, x2) -> Z.equal n1 n2 && sub_eq x1 x2 - | Var x1, Var x2 -> sub_eq x1 x2 - | (Pred _ | Op _ | Const _ | Mult _ | Var _), _ -> false + | LRA_const a1, LRA_const a2 -> Z.equal a1 a2 + | LRA_mult (n1, x1), LRA_mult (n2, x2) -> Z.equal n1 n2 && sub_eq x1 x2 + | LRA_other x1, LRA_other x2 -> sub_eq x1 x2 + | (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) - | Op (op, a, b) -> LRA_view.Op (op, f a, f b) - | Mult (c, x) -> LRA_view.Mult (Q.of_bigint c, f x) - | Const x -> LRA_view.Const (Q.of_bigint x) - | Var v -> LRA_view.Var (f v) + | LRA_pred (p, a, b) -> LRA_view.LRA_pred (p, f a, f b) + | LRA_op (op, a, b) -> LRA_view.LRA_op (op, f a, f b) + | LRA_mult (c, x) -> LRA_view.LRA_mult (Q.of_bigint c, f x) + | LRA_const x -> LRA_view.LRA_const (Q.of_bigint x) + | LRA_other v -> LRA_view.LRA_other (f v) end diff --git a/src/base/LRA_term.ml b/src/base/LRA_term.ml new file mode 100644 index 00000000..eea25db2 --- /dev/null +++ b/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 diff --git a/src/base/LRA_term.mli b/src/base/LRA_term.mli new file mode 100644 index 00000000..396f3b8c --- /dev/null +++ b/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 *) diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml index e13f4026..d0b03630 100644 --- a/src/base/Sidekick_base.ml +++ b/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