From 4916aee050246ad56d8ac2354f853e53e5f59d6e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 13 Nov 2020 07:32:43 -0800 Subject: [PATCH] [sledge] Revise Context.classify to detect more atomic terms Summary: Treating atomic terms as uninterpreted is correct, but slower. Reviewed By: jvillard Differential Revision: D24934117 fbshipit-source-id: d9bdf5c8d --- sledge/src/fol/context.ml | 7 +++---- sledge/src/fol/trm.ml | 3 +++ sledge/src/fol/trm.mli | 2 ++ 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index afd5d824d..0724ba7fd 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -14,16 +14,15 @@ open Exp type kind = Interpreted | Atomic | Uninterpreted [@@deriving compare, equal] -let rec classify e = +let classify e = match (e : Trm.t) with + | Var _ | Z _ | Q _ | Concat [||] | Apply (_, [||]) -> Atomic | Arith a -> ( match Trm.Arith.classify a with - | Trm t -> classify t - | Const _ -> Atomic + | Trm _ | Const _ -> violates Trm.invariant e | Interpreted -> Interpreted | Uninterpreted -> Uninterpreted ) | Splat _ | Sized _ | Extract _ | Concat _ -> Interpreted - | Var _ | Z _ | Q _ -> Atomic | Apply _ -> Uninterpreted let interpreted e = equal_kind (classify e) Interpreted diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 3336387b0..18886f9c2 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -88,6 +88,9 @@ and Trm : sig val ppx : Var.strength -> t pp val pp : t pp + + include Invariant.S with type t := t + val _Var : int -> string -> t val _Z : Z.t -> t val _Q : Q.t -> t diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli index d2d05d002..eb76a33c2 100644 --- a/sledge/src/fol/trm.mli +++ b/sledge/src/fol/trm.mli @@ -47,6 +47,8 @@ val ppx : Var.strength -> t pp val pp : t pp val pp_diff : (t * t) pp +include Invariant.S with type t := t + (** Construct *) (* variables *)