From 943efad2060d83ca0ec64bc6f79a39cf7f9b4cac Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 3 Oct 2020 23:46:45 -0400 Subject: [PATCH] feat: add AST for LRA --- src/base-term/Base_types.ml | 79 ++++++++++++++++++++++++++++++++++++- src/base-term/Model.ml | 12 +++++- src/base-term/dune | 2 +- src/smtlib/Process.ml | 1 - src/th-lra/Sidekick_lra.ml | 8 ++++ 5 files changed, 97 insertions(+), 5 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index 2918e277..5e720d2e 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -4,6 +4,15 @@ module Fmt = CCFormat module CC_view = Sidekick_core.CC_view +type lra_pred = Sidekick_lra.pred = Lt | Leq | Eq | Neq | Geq | Gt +type lra_op = Sidekick_lra.op = Plus | Minus + +type 'a lra_view = 'a Sidekick_lra.lra_view = + | LRA_pred of lra_pred * 'a * 'a + | LRA_op of lra_op * 'a * 'a + | LRA_const of Q.t + | LRA_other of 'a + (* main term cell. *) type term = { mutable term_id: int; (* unique ID *) @@ -18,6 +27,7 @@ and 'a term_view = | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a + | LRA of 'a lra_view and fun_ = { fun_id: ID.t; @@ -193,6 +203,20 @@ let rec pp_ty out t = match t.ty_view with | Ty_atomic {def=Ty_data d; args;_} -> Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data.data_id (Util.pp_list pp_ty) args +let string_of_lra_pred = function + | Lt -> "<" + | Leq -> "<=" + | Neq -> "!=" + | Eq -> "=" + | Gt-> ">" + | Geq -> ">=" +let pp_pred out p = Fmt.string out (string_of_lra_pred p) + +let string_of_lra_op = function + | Plus -> "+" + | Minus -> "-" +let pp_lra_op out p = Fmt.string out (string_of_lra_op p) + let pp_term_view_gen ~pp_id ~pp_t out = function | Bool true -> Fmt.string out "true" | Bool false -> Fmt.string out "false" @@ -204,6 +228,15 @@ let pp_term_view_gen ~pp_id ~pp_t out = function | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp_t a pp_t b | Not u -> Fmt.fprintf out "(@[not@ %a@])" pp_t u | Ite (a,b,c) -> Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" pp_t a pp_t b pp_t c + | LRA l -> + begin match l with + | LRA_pred (p, a, b) -> + Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_pred p) pp_t a pp_t b + | LRA_op (p, a, b) -> + Fmt.fprintf out "(@[%s@ %a@ %a@])" (string_of_lra_op p) pp_t a pp_t b + | LRA_const q -> Q.pp_print out q + | LRA_other x -> pp_t out x + end let pp_term_top ~ids out t = let rec pp out t = @@ -499,6 +532,7 @@ module Term_cell : sig | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a + | LRA of 'a lra_view type t = term view @@ -512,6 +546,7 @@ module Term_cell : sig val eq : term -> term -> t val not_ : term -> t val ite : term -> term -> term -> t + val lra : term lra_view -> t val ty : t -> Ty.t (** Compute the type of this term cell. Not totally free *) @@ -540,6 +575,7 @@ end = struct | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a + | LRA of 'a lra_view type t = term view @@ -561,6 +597,15 @@ end = struct | Eq (a,b) -> Hash.combine3 12 (sub_hash a) (sub_hash b) | Not u -> Hash.combine2 70 (sub_hash u) | Ite (a,b,c) -> Hash.combine4 80 (sub_hash a)(sub_hash b)(sub_hash c) + | LRA l -> + begin match l with + | 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_const q -> Hash.combine2 83 (Hash.string @@ Q.to_string q) + | LRA_other x -> sub_hash x + end (* equality that relies on physical equality of subterms *) let equal (a:A.t view) b : bool = match a, b with @@ -571,7 +616,17 @@ end = struct | Not a, Not b -> sub_eq a b | Ite (a1,b1,c1), Ite (a2,b2,c2) -> sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 c2 - | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _), _ + | LRA l1, LRA l2 -> + begin match l1, l2 with + | LRA_pred (p1,a1,b1), LRA_pred (p2,a2,b2) -> + p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2 + | LRA_op(p1,a1,b1), LRA_op (p2,a2,b2) -> + p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2 + | LRA_const a1, LRA_const a2 -> Q.equal a1 a2 + | LRA_other x1, LRA_other x2 -> sub_eq x1 x2 + | (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_other _), _ -> false + end + | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _ | LRA _), _ -> false let pp = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:A.pp @@ -605,6 +660,7 @@ end = struct | _ -> Not t let ite a b c = Ite (a,b,c) + let lra l : t = LRA l let ty (t:t): Ty.t = match t with | Bool _ | Eq _ | Not _ -> Ty.bool @@ -635,6 +691,12 @@ end = struct | Fun_select s -> Lazy.force s.select_ty | Fun_cstor c -> Lazy.force c.cstor_ty end + | LRA l -> + begin match l with + | LRA_pred _ -> Ty.bool + | LRA_op _ | LRA_const _ -> Ty.real + | LRA_other x -> x.term_ty + end let iter f view = match view with @@ -643,6 +705,12 @@ end = struct | Not u -> f u | Eq (a,b) -> f a; f b | Ite (a,b,c) -> f a; f b; f c + | LRA l -> + begin match l with + | LRA_pred (_, a, b)|LRA_op (_, a, b) -> f a; f b + | LRA_const _ -> () + | LRA_other x -> f x + end let map f view = match view with @@ -651,6 +719,7 @@ end = struct | Not u -> Not (f u) | Eq (a,b) -> Eq (f a, f b) | Ite (a,b,c) -> Ite (f a, f b, f c) + | LRA l -> LRA (Sidekick_lra.map_view f l) module Tbl = CCHashtbl.Make(struct type t = term view @@ -672,6 +741,7 @@ module Term : sig | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a + | LRA of 'a lra_view val id : t -> int val view : t -> term view @@ -697,6 +767,7 @@ module Term : sig val select : state -> select -> t -> t val app_cstor : state -> cstor -> t IArray.t -> t val is_a : state -> cstor -> t -> t + val lra : state -> t lra_view -> t (** Obtain unsigned version of [t], + the sign as a boolean *) val abs : state -> t -> t * bool @@ -743,6 +814,7 @@ end = struct | Eq of 'a * 'a | Not of 'a | Ite of 'a * 'a * 'a + | LRA of 'a lra_view let[@inline] id t = t.term_id let[@inline] ty t = t.term_ty @@ -804,6 +876,9 @@ end = struct let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t) let app_cstor st c args : t = app_fun st (Fun.cstor c) args + let[@inline] lra (st:state) (l:t lra_view) : t = + make st (Term_cell.lra l) + (* might need to tranfer the negation from [t] to [sign] *) let abs tst t : t * bool = match view t with | Bool false -> true_ tst, false @@ -828,6 +903,7 @@ end = struct | Eq (a,b) -> C.Eq (a, b) | Not u -> C.Not u | Ite (a,b,c) -> C.If (a,b,c) + | LRA _ -> C.Opaque t (* no congruence here *) module As_key = struct type t = term @@ -877,6 +953,7 @@ end = struct | Not u -> not_ tst (f u) | Eq (a,b) -> eq tst (f a) (f b) | Ite (a,b,c) -> ite tst (f a) (f b) (f c) + | LRA l -> lra tst (Sidekick_lra.map_view f l) end module Value : sig diff --git a/src/base-term/Model.ml b/src/base-term/Model.ml index e3d399fa..220785c6 100644 --- a/src/base-term/Model.ml +++ b/src/base-term/Model.ml @@ -153,6 +153,14 @@ let eval (m:t) (t:Term.t) : Value.t option = let a = aux a in let b = aux b in if Value.equal a b then Value.true_ else Value.false_ + | LRA _l -> + assert false + (* TODO: evaluation + begin match l with + | LRA_pred (p, a, b) -> + | LRA_op (_, _, _)|LRA_const _|LRA_other _ -> assert false + end + *) | App_fun (c, args) -> match Fun.view c, (args :_ IArray.t:> _ array) with | Fun_def udef, _ -> @@ -180,7 +188,7 @@ let eval (m:t) (t:Term.t) : Value.t option = | Fun_is_a _, _ -> Error.errorf "bad is-a term %a" Term.pp t | Fun_undef _, _ -> - try Term.Map.find t m.values + (try Term.Map.find t m.values with Not_found -> begin match Fun.Map.find c m.funs with | fi -> @@ -191,7 +199,7 @@ let eval (m:t) (t:Term.t) : Value.t option = end | exception Not_found -> raise No_value (* no particular interpretation *) - end + end) in try Some (aux t) with No_value -> None diff --git a/src/base-term/dune b/src/base-term/dune index 0fc8293b..c056f5ae 100644 --- a/src/base-term/dune +++ b/src/base-term/dune @@ -2,5 +2,5 @@ (name sidekick_base_term) (public_name sidekick.base-term) (synopsis "Basic term definitions for the standalone SMT solver") - (libraries containers sidekick.core sidekick.util zarith) + (libraries containers sidekick.core sidekick.util sidekick.th-lra zarith) (flags :standard -w -32 -open Sidekick_util)) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index c7029119..98ca0f5f 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -304,7 +304,6 @@ end) module Th_lra = Sidekick_lra.Make(struct module S = Solver - module T = S.T.Term type term = S.T.Term.t include Lra diff --git a/src/th-lra/Sidekick_lra.ml b/src/th-lra/Sidekick_lra.ml index 8b3de28b..fd03bd2e 100644 --- a/src/th-lra/Sidekick_lra.ml +++ b/src/th-lra/Sidekick_lra.ml @@ -15,6 +15,14 @@ type 'a lra_view = | LRA_const of Q.t | LRA_other of 'a +let map_view f (l:_ lra_view) : _ lra_view = + begin match l with + | 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_const q -> LRA_const q + | LRA_other x -> LRA_other (f x) + end + module type ARG = sig module S : Sidekick_core.SOLVER