simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

tiny helper

Browse source
This commit is contained in:
Simon Cruanes 2022-09-01 22:32:24 -04:00
parent 8db63dbdc4
commit 0797ff0409
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 3 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/base/Data_ty.ml
View file

@ -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)

1
src/base/Data_ty.mli
View file

@ -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 *)

24
src/base/th_uf.ml
View file

@ -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);
())
()