From 0797ff0409ec46f9ac506c767c596965249c9469 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 1 Sep 2022 22:32:24 -0400 Subject: [PATCH] tiny helper --- src/base/Data_ty.ml | 2 ++ src/base/Data_ty.mli | 1 + src/base/th_uf.ml | 24 ------------------------ 3 files changed, 3 insertions(+), 24 deletions(-) delete mode 100644 src/base/th_uf.ml diff --git a/src/base/Data_ty.ml b/src/base/Data_ty.ml index 26e87dd8..59839eba 100644 --- a/src/base/Data_ty.ml +++ b/src/base/Data_ty.ml @@ -107,6 +107,8 @@ let ops = let opaque_to_cc _ = false end : Const.DYN_OPS) +let data_as_ty (d : data) = Lazy.force d.data_as_ty + let data tst d : Term.t = Term.const tst @@ Const.make (Data d) ops ~ty:(Term.type_ tst) diff --git a/src/base/Data_ty.mli b/src/base/Data_ty.mli index 749bc22a..e53b9150 100644 --- a/src/base/Data_ty.mli +++ b/src/base/Data_ty.mli @@ -50,6 +50,7 @@ val data : Term.store -> t -> Term.t val cstor : Term.store -> cstor -> Term.t val select : Term.store -> select -> Term.t val is_a : Term.store -> cstor -> Term.t +val data_as_ty : t -> ty (* TODO: select_ : store -> cstor -> int -> term *) diff --git a/src/base/th_uf.ml b/src/base/th_uf.ml deleted file mode 100644 index efb40ee9..00000000 --- a/src/base/th_uf.ml +++ /dev/null @@ -1,24 +0,0 @@ -(** Theory of uninterpreted functions *) - -open Sidekick_core -open Sidekick_smt_solver - -open struct - module SI = Solver_internal - - let on_is_subterm ~th_id (solver : SI.t) (_, _, t) : _ list = - let f, args = Term.unfold_app t in - (match Term.view f, args with - | Term.E_const { Const.c_view = Uconst.Uconst _; _ }, _ :: _ -> - SI.claim_term solver ~th_id t - | _ -> ()); - - [] -end - -let theory : Theory.t = - Theory.make ~name:"uf" - ~create_and_setup:(fun ~id:th_id solver -> - SI.on_cc_is_subterm solver (on_is_subterm ~th_id solver); - ()) - ()