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

refactor: remove Value, just use terms in the model

Browse source
This commit is contained in:
Simon Cruanes 2021-03-22 12:53:38 -04:00
parent b6713fb833
commit be97938e12
2 changed files with 4 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/core/Sidekick_core.ml
View file

@ -626,17 +626,6 @@ module type SOLVER = sig
val sign : t -> bool
end
(* FIXME: just use terms instead? *)
(** {3 Semantic values} *)
module Value : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val ty : t -> ty
val pp : t Fmt.printer
end
module Model : sig
type t
@ -644,9 +633,9 @@ module type SOLVER = sig
val mem : t -> term -> bool
val find : t -> term -> Value.t option
val find : t -> term -> term option
val eval : t -> term -> Value.t option
val eval : t -> term -> term option
val pp : t Fmt.printer
end

7
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -561,13 +561,10 @@ module Make(A : ARG)
| U_incomplete -> Fmt.string out "incomplete fragment"
end [@@ocaml.warning "-37"]
(* just use terms as values *)
module Value = Term
module Model = struct
type t =
| Empty
| Map of Value.t Term.Tbl.t
| Map of term Term.Tbl.t
let empty = Empty
let mem = function
| Empty -> fun _ -> false
@ -580,7 +577,7 @@ module Make(A : ARG)
| Empty -> Fmt.string out "(model)"
| Map tbl ->
let pp_pair out (t,v) =
Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Value.pp v
Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Term.pp v
in
Fmt.fprintf out "(@[<hv>model@ %a@])"
(Util.pp_iter pp_pair) (Term.Tbl.to_iter tbl)