[sledge] Refactor: Expose constructors for record Terms

Summary: McCarthy-style select/update terms for records.

Reviewed By: jvillard

Differential Revision: D22401038

fbshipit-source-id: 9c9b8e0a1
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent d39dd1fee2
commit 48833cc63b

@ -88,6 +88,10 @@ module rec Term : sig
val extract : seq:t -> off:t -> len:t -> t val extract : seq:t -> off:t -> len:t -> t
val concat : t array -> t val concat : t array -> t
(* records *)
val select : rcd:t -> idx:int -> t
val update : rcd:t -> idx:int -> elt:t -> t
(* if-then-else *) (* if-then-else *)
val ite : cnd:Formula.t -> thn:t -> els:t -> t val ite : cnd:Formula.t -> thn:t -> els:t -> t

Loading…
Cancel
Save