diff --git a/src/arith/base-term/Base_types.ml b/src/arith/base-term/Base_types.ml index 8d32a736..6895a84c 100644 --- a/src/arith/base-term/Base_types.ml +++ b/src/arith/base-term/Base_types.ml @@ -260,6 +260,7 @@ let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term module Ty : sig type t = ty + type state = unit type view = ty_view = | Ty_bool | Ty_real @@ -283,8 +284,8 @@ module Ty : sig val id : t -> int val view : t -> view - val bool : t - val real : t + val bool : state -> t + val real : state -> t val atomic : def -> t list -> t val atomic_uninterpreted : ID.t -> t @@ -316,6 +317,7 @@ module Ty : sig end end = struct type t = ty + type state = unit type view = ty_view = | Ty_bool | Ty_real @@ -390,8 +392,8 @@ end = struct | Ty_bool | Ty_real -> assert false | Ty_atomic r -> r.finite <- b - let bool = make_ Ty_bool - let real = make_ Ty_real + let bool () = make_ Ty_bool + let real () = make_ Ty_real let atomic def args : t = make_ (Ty_atomic {def; args; finite=true;}) @@ -684,7 +686,7 @@ end = struct let[@inline] lra l : t = LRA l let ty (t:t): Ty.t = match t with - | Bool _ | Eq _ | Not _ -> Ty.bool + | Bool _ | Eq _ | Not _ -> Ty.bool () | Ite (_, b, _) -> b.term_ty | App_fun (f, args) -> begin match Fun.view f with @@ -707,15 +709,15 @@ end = struct )) ty_args; ty_ret - | Fun_is_a _ -> Ty.bool + | Fun_is_a _ -> Ty.bool () | Fun_def def -> def.ty f.fun_id args | Fun_select s -> Lazy.force s.select_ty | Fun_cstor c -> Lazy.force c.cstor_ty end | LRA l -> begin match l with - | LRA_pred _ | LRA_simplex_pred _ -> Ty.bool - | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_simplex_var _ -> Ty.real + | LRA_pred _ | LRA_simplex_pred _ -> Ty.bool () + | LRA_op _ | LRA_const _ | LRA_mult _ | LRA_simplex_var _ -> Ty.real () | LRA_other x -> x.term_ty end @@ -864,7 +866,7 @@ end = struct } let[@inline] make st (c:t term_view) : t = - let t = {term_id= -1; term_ty=Ty.bool; term_view=c} in + let t = {term_id= -1; term_ty=Ty.bool(); term_view=c} in let t' = H.hashcons st.tbl t in if t == t' then ( t'.term_ty <- Term_cell.ty c; diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml index f25440b1..14625334 100644 --- a/src/arith/lra/sidekick_arith_lra.ml +++ b/src/arith/lra/sidekick_arith_lra.ml @@ -76,7 +76,10 @@ module type S = sig type state - val create : ?stat:Stat.t -> A.S.T.Term.state -> state + val create : ?stat:Stat.t -> + A.S.T.Term.state -> + A.S.T.Ty.state -> + state val theory : A.S.theory end @@ -129,6 +132,7 @@ module Make(A : ARG) : S with module A = A = struct type state = { tst: T.state; + ty_st: Ty.state; simps: T.t T.Tbl.t; (* cache *) gensym: A.Gensym.t; encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *) @@ -139,8 +143,8 @@ module Make(A : ARG) : S with module A = A = struct stat_th_comb: int Stat.counter; } - let create ?(stat=Stat.create()) tst : state = - { tst; + let create ?(stat=Stat.create()) tst ty_st : state = + { tst; ty_st; simps=T.Tbl.create 128; gensym=A.Gensym.create tst; encoded_eqs=T.Tbl.create 8; @@ -163,7 +167,7 @@ module Make(A : ARG) : S with module A = A = struct let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty let fresh_lit (self:state) ~mk_lit ~pre : Lit.t = - let t = fresh_term ~pre self Ty.bool in + let t = fresh_term ~pre self (Ty.bool self.ty_st) in mk_lit t let pp_pred_def out (p,l1,l2) : unit = @@ -542,7 +546,7 @@ module Make(A : ARG) : S with module A = A = struct let create_and_setup si = Log.debug 2 "(th-lra.setup)"; let stat = SI.stats si in - let st = create ~stat (SI.tst si) in + let st = create ~stat (SI.tst si) (SI.ty_st si) in SI.add_simplifier si (simplify st); SI.add_preprocess si (preproc_lra st); SI.on_final_check si (final_check_ st); diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 434ac895..a01f18a1 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -56,7 +56,9 @@ module type TERM = sig val hash : t -> int val pp : t Fmt.printer - val bool : t + type state + + val bool : state -> t val is_bool : t -> bool end @@ -341,6 +343,7 @@ module type SOLVER_INTERNAL = sig type ty = T.Ty.t type term = T.Term.t type term_state = T.Term.state + type ty_state = T.Ty.state type proof = P.t (** {3 Main type for a solver} *) @@ -348,6 +351,7 @@ module type SOLVER_INTERNAL = sig type solver = t val tst : t -> term_state + val ty_st : t -> ty_state val stats : t -> Stat.t (** {3 Actions for the theories} *) @@ -380,6 +384,7 @@ module type SOLVER_INTERNAL = sig type t val tst : t -> term_state + val ty_st : t -> ty_state val clear : t -> unit (** Reset internal cache, etc. *) @@ -662,6 +667,7 @@ module type SOLVER = sig ?store_proof:bool -> theories:theory list -> T.Term.state -> + T.Ty.state -> unit -> t (** Create a new solver. diff --git a/src/main/main.ml b/src/main/main.ml index 5c1cf236..1eaf4a6c 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -95,7 +95,8 @@ module Dimacs = struct match Util.Int_tbl.find atoms (abs i) with | x -> Term.const tst x | exception Not_found -> - let f = Sidekick_base_term.Fun.mk_undef_const (ID.makef "%d" (abs i)) Ty.bool in + let f = Sidekick_base_term.Fun.mk_undef_const + (ID.makef "%d" (abs i)) (Ty.bool()) in Util.Int_tbl.add atoms (abs i) f; Term.const tst f in @@ -145,12 +146,12 @@ let main () = let solver = let theories = if is_cnf then [] else [ - Process.th_bool ; + Process.th_bool; Process.th_data; Process.th_lra; ] in - Process.Solver.create ~store_proof:!check ~theories tst () + Process.Solver.create ~store_proof:!check ~theories tst () () in if !check then ( (* might have to check conflicts *) diff --git a/src/mini-cc/tests/tests.ml b/src/mini-cc/tests/tests.ml index c9307a63..a55aa20a 100644 --- a/src/mini-cc/tests/tests.ml +++ b/src/mini-cc/tests/tests.ml @@ -12,7 +12,7 @@ module Setup() = struct let tst = Term.create() let (@->) l ret = Ty.Fun.mk l ret let ty_i = Ty.atomic_uninterpreted (ID.make "$i") - let ty_bool = Ty.bool + let ty_bool = Ty.bool () let fun_f = Fun.mk_undef (ID.make "f") ([ty_i] @-> ty_i) let fun_g = Fun.mk_undef (ID.make "g") ([ty_i; ty_i] @-> ty_i) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index fc401464..d9675bc6 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -105,6 +105,7 @@ module Make(A : ARG) type ty = Ty.t type lit = Lit.t type term_state = Term.state + type ty_state = Ty.state type th_states = | Ths_nil @@ -120,13 +121,16 @@ module Make(A : ARG) module Simplify = struct type t = { tst: term_state; + ty_st: ty_state; mutable hooks: hook list; cache: Term.t Term.Tbl.t; } and hook = t -> term -> term option - let create tst : t = {tst; hooks=[]; cache=Term.Tbl.create 32;} + let create tst ty_st : t = + {tst; ty_st; hooks=[]; cache=Term.Tbl.create 32;} let[@inline] tst self = self.tst + let[@inline] ty_st self = self.ty_st let add_hook self f = self.hooks <- f :: self.hooks let clear self = Term.Tbl.clear self.cache @@ -156,6 +160,7 @@ module Make(A : ARG) type t = { tst: Term.state; (** state for managing terms *) + ty_st: Ty.state; cc: CC.t lazy_t; (** congruence closure *) stat: Stat.t; count_axiom: int Stat.counter; @@ -194,6 +199,7 @@ module Make(A : ARG) let[@inline] cc (t:t) = Lazy.force t.cc let[@inline] tst t = t.tst + let[@inline] ty_st t = t.ty_st let stats t = t.stat let simplifier self = self.simp @@ -381,16 +387,17 @@ module Make(A : ARG) CC.mk_model (cc self) m *) - let create ~stat (tst:Term.state) () : t = + let create ~stat (tst:Term.state) (ty_st:Ty.state) () : t = let rec self = { tst; + ty_st; cc = lazy ( (* lazily tie the knot *) CC.create ~size:`Big self.tst; ); th_states=Ths_nil; stat; - simp=Simplify.create tst; + simp=Simplify.create tst ty_st; on_progress=(fun () -> ()); preprocess=[]; preprocess_cache=Term.Tbl.create 32; @@ -467,9 +474,9 @@ module Make(A : ARG) let add_theory_l self = List.iter (add_theory self) (* create a new solver *) - let create ?(stat=Stat.global) ?size ?store_proof ~theories tst () : t = + let create ?(stat=Stat.global) ?size ?store_proof ~theories tst ty_st () : t = Log.debug 5 "msat-solver.create"; - let si = Solver_internal.create ~stat tst () in + let si = Solver_internal.create ~stat tst ty_st () in let self = { si; solver=Sat_solver.create ?store_proof ?size si; diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml index 2dc21cfc..60b8bebf 100644 --- a/src/smtlib/Form.ml +++ b/src/smtlib/Form.ml @@ -32,7 +32,7 @@ let view_as_bool (t:T.t) : T.t bool_view = | _ -> B_atom t module Funs = struct - let get_ty _ _ = Ty.bool + let get_ty _ _ = Ty.bool() let abs ~self _a = match T.view self with diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 489ee2cb..5ccbfc4e 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -320,11 +320,11 @@ module Th_lra = Sidekick_arith_lra.Make(struct let mk_bool = T.bool let view_as_lra t = match T.view t with | T.LRA l -> l - | T.Eq (a,b) when Ty.equal (T.ty a) Ty.real -> LRA_pred (Eq, a, b) + | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> LRA_pred (Eq, a, b) | _ -> LRA_other t - let ty_lra _st = Ty.real - let has_ty_real t = Ty.equal (T.ty t) Ty.real + let ty_lra _st = Ty.real() + let has_ty_real t = Ty.equal (T.ty t) (Ty.real()) module Gensym = struct type t = { diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 2ffb0392..03bec7e2 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -6,6 +6,7 @@ module Solver : Sidekick_msat_solver.S with type T.Term.t = Term.t and type T.Term.state = Term.state and type T.Ty.t = Ty.t + and type T.Ty.state = Ty.state val th_bool : Solver.theory val th_data : Solver.theory diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 17df956b..4a9b6c74 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -77,7 +77,7 @@ let ill_typed ctx fmt = errorf_ctx ctx ("ill-typed: " ^^ fmt) let check_bool_ ctx t = - if not (Ty.equal (T.ty t) Ty.bool) then ( + if not (Ty.equal (T.ty t) (Ty.bool())) then ( ill_typed ctx "expected bool, got `@[%a : %a@]`" T.pp t Ty.pp (T.ty t) ) @@ -87,8 +87,8 @@ let find_id_ ctx (s:string): ID.t * Ctx.kind = (* parse a type *) let rec conv_ty ctx (t:PA.ty) : Ty.t = match t with - | PA.Ty_bool -> Ty.bool - | PA.Ty_real -> Ty.real + | PA.Ty_bool -> Ty.bool() + | PA.Ty_real -> Ty.real() | PA.Ty_app ("Int",[]) -> ill_typed ctx "cannot handle ints for now" (* TODO: A.Ty.int , Ctx.K_ty Ctx.K_other *) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index bedf0033..861a1326 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -44,7 +44,7 @@ module type S = sig type state - val create : A.S.T.Term.state -> state + val create : A.S.T.Term.state -> A.S.T.Ty.state -> state val simplify : state -> A.S.Solver_internal.simplify_hook (** Simplify given term *) @@ -64,13 +64,14 @@ module Make(A : ARG) : S with module A = A = struct type state = { tst: T.state; + ty_st: Ty.state; simps: T.t T.Tbl.t; (* cache *) cnf: Lit.t T.Tbl.t; (* tseitin CNF *) gensym: A.Gensym.t; } - let create tst : state = - { tst; simps=T.Tbl.create 128; + let create tst ty_st : state = + { tst; ty_st; simps=T.Tbl.create 128; cnf=T.Tbl.create 128; gensym=A.Gensym.create tst; } @@ -129,7 +130,7 @@ module Make(A : ARG) : S with module A = A = struct let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty let fresh_lit (self:state) ~mk_lit ~pre : Lit.t = - let t = fresh_term ~pre self Ty.bool in + let t = fresh_term ~pre self (Ty.bool self.ty_st) in mk_lit t (* preprocess "ite" away *) @@ -243,7 +244,7 @@ module Make(A : ARG) : S with module A = A = struct let create_and_setup si = Log.debug 2 "(th-bool.setup)"; - let st = create (SI.tst si) in + let st = create (SI.tst si) (SI.ty_st si) in SI.add_simplifier si (simplify st); SI.add_preprocess si (preproc_ite st); SI.add_preprocess si (cnf st);