From 444a0b9f8583ea9378a93a309b29ac58f502f39f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 1 Dec 2019 17:17:37 -0600 Subject: [PATCH] wip: theory of datatypes --- src/base-term/Base_types.ml | 111 +++++--------- src/base-term/Sidekick_base_term.ml | 1 - src/main/main.ml | 2 +- src/smtlib/Process.ml | 17 ++- src/smtlib/Typecheck.ml | 6 +- src/th-data/Sidekick_th_data.ml | 229 ++++++++++++++++++++-------- 6 files changed, 222 insertions(+), 144 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index e9ed2637..d1803cd5 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -63,17 +63,18 @@ and ty_view = | Ty_atomic of { def: ty_def; args: ty list; - card: ty_card lazy_t; + mutable finite: bool; } and ty_def = | Ty_uninterpreted of ID.t - | Ty_data of data + | Ty_data of { + data: data; + } | Ty_def of { id: ID.t; pp: ty Fmt.printer -> ty list Fmt.printer; default_val: value list -> value; (* default value of this type *) - card: ty list -> ty_card; } and data = { @@ -97,10 +98,6 @@ and select = { select_i: int; } -and ty_card = - | Finite - | Infinite - (** Semantic values, used for models (and possibly model-constructing calculi) *) and value = | V_bool of bool @@ -185,9 +182,9 @@ let rec pp_ty out t = match t.ty_view with | Ty_atomic {def=Ty_uninterpreted id; args; _} -> Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args | Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args - | Ty_atomic {def=Ty_data d; args=[];_} -> ID.pp out d.data_id + | Ty_atomic {def=Ty_data d; args=[];_} -> ID.pp out d.data.data_id | Ty_atomic {def=Ty_data d; args;_} -> - Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data_id (Util.pp_list pp_ty) args + Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data.data_id (Util.pp_list pp_ty) args let pp_term_view_gen ~pp_id ~pp_t out = function | Bool true -> Fmt.string out "true" @@ -212,40 +209,6 @@ let pp_term_top ~ids out t = let pp_term = pp_term_top ~ids:false let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term -module Ty_card : sig - type t = ty_card = Finite | Infinite - - val (+) : t -> t -> t - val ( * ) : t -> t -> t - val ( ^ ) : t -> t -> t - val finite : t - val infinite : t - - val sum : t list -> t - val product : t list -> t - - val equal : t -> t -> bool - val compare : t -> t -> int - val pp : t CCFormat.printer -end = struct - type t = ty_card = Finite | Infinite - - let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let finite = Finite - let infinite = Infinite - - let sum = List.fold_left (+) Finite - let product = List.fold_left ( * ) Finite - - let equal = (=) - let compare = Pervasives.compare - let pp out = function - | Finite -> CCFormat.string out "finite" - | Infinite -> CCFormat.string out "infinite" -end - module Ty : sig type t = ty type view = ty_view = @@ -253,17 +216,18 @@ module Ty : sig | Ty_atomic of { def: ty_def; args: ty list; - card: ty_card lazy_t; + mutable finite: bool; } type def = ty_def = | Ty_uninterpreted of ID.t - | Ty_data of data + | Ty_data of { + data: data; + } | Ty_def of { id: ID.t; pp: ty Fmt.printer -> ty list Fmt.printer; default_val: value list -> value; (* default value of this type *) - card: ty list -> ty_card; } val id : t -> int @@ -274,7 +238,8 @@ module Ty : sig val atomic_uninterpreted : ID.t -> t - val card : t -> ty_card + val finite : t -> bool + val set_finite : t -> bool -> unit val is_bool : t -> bool val is_uninterpreted : t -> bool @@ -305,16 +270,17 @@ end = struct | Ty_atomic of { def: ty_def; args: ty list; - card: ty_card lazy_t; + mutable finite: bool; } type def = ty_def = | Ty_uninterpreted of ID.t - | Ty_data of data + | Ty_data of { + data: data; + } | Ty_def of { id: ID.t; pp: ty Fmt.printer -> ty list Fmt.printer; default_val: value list -> value; (* default value of this type *) - card: ty list -> ty_card; } let[@inline] id t = t.ty_id @@ -327,7 +293,7 @@ end = struct let equal_def d1 d2 = match d1, d2 with | Ty_uninterpreted id1, Ty_uninterpreted id2 -> ID.equal id1 id2 | Ty_def d1, Ty_def d2 -> ID.equal d1.id d2.id - | Ty_data d1, Ty_data d2 -> ID.equal d1.data_id d2.data_id + | Ty_data d1, Ty_data d2 -> ID.equal d1.data.data_id d2.data.data_id | (Ty_uninterpreted _ | Ty_def _ | Ty_data _), _ -> false @@ -347,7 +313,7 @@ end = struct | Ty_atomic {def=Ty_def d; args; _} -> Hash.combine3 20 (ID.hash d.id) (Hash.list hash args) | Ty_atomic {def=Ty_data d; args; _} -> - Hash.combine3 30 (ID.hash d.data_id) (Hash.list hash args) + Hash.combine3 30 (ID.hash d.data.data_id) (Hash.list hash args) let set_id ty id = assert (ty.ty_id < 0); @@ -361,21 +327,18 @@ end = struct let ty = {ty_id= -1; ty_view=c; } in H.hashcons tbl ty - let card t = match view t with - | Ty_bool -> Finite - | Ty_atomic {card=lazy c; _} -> c + let finite t = match view t with + | Ty_bool -> true + | Ty_atomic {finite=f; _} -> f + + let set_finite t b = match view t with + | Ty_bool -> assert false + | Ty_atomic r -> r.finite <- b let bool = make_ Ty_bool let atomic def args : t = - let card = lazy ( - match def with - | Ty_uninterpreted _ -> - if List.for_all (fun sub -> card sub = Finite) args then Finite else Infinite - | Ty_def d -> d.card args - | Ty_data _ -> assert false (* TODO *) - ) in - make_ (Ty_atomic {def; args; card}) + make_ (Ty_atomic {def; args; finite=true;}) let atomic_uninterpreted id = atomic (Ty_uninterpreted id) [] @@ -968,6 +931,17 @@ module Data = struct let pp out d = ID.pp out d.data_id end +module Select = struct + type t = select = { + select_id: ID.t; + select_cstor: cstor; + select_ty: ty lazy_t; + select_i: int; + } + + let ty sel = Lazy.force sel.select_ty +end + module Cstor = struct type t = cstor = { cstor_id: ID.t; @@ -976,19 +950,12 @@ module Cstor = struct cstor_ty_as_data: data; cstor_ty: ty lazy_t; } + let ty_args c = + Lazy.force c.cstor_args |> Iter.of_list |> Iter.map Select.ty let equal = eq_cstor let pp out c = ID.pp out c.cstor_id end -module Select = struct - type t = select = { - select_id: ID.t; - select_cstor: cstor; - select_ty: ty lazy_t; - select_i: int; - } -end - module Proof = struct type t = Default let default = Default diff --git a/src/base-term/Sidekick_base_term.ml b/src/base-term/Sidekick_base_term.ml index cc936713..46477741 100644 --- a/src/base-term/Sidekick_base_term.ml +++ b/src/base-term/Sidekick_base_term.ml @@ -1,6 +1,5 @@ module Base_types = Base_types module ID = ID -module Ty_card = Base_types.Ty_card module Fun = Base_types.Fun module Stat = Stat module Model = Model diff --git a/src/main/main.ml b/src/main/main.ml index 5f4adf3d..12b57e49 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -192,7 +192,7 @@ let () = match main() with if Printexc.backtrace_status () then ( Format.fprintf Format.std_formatter "%s@." b ); - Pervasives.exit n + CCShims_.Stdlib.exit n in begin match e with | Error.Error msg -> diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 98c7890b..b07da7a6 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -266,15 +266,26 @@ module Th_data = Sidekick_th_data.Make(struct let as_datatype ty = match Ty.view ty with | Ty_atomic {def=Ty_data data;_} -> - Some (Lazy.force data.data_cstors |> ID.Map.values) - | _ -> None + Ty_data {cstors=Lazy.force data.data.data_cstors |> ID.Map.values} + | Ty_atomic {def=_;args;finite=_} -> + Ty_app{args=Iter.of_list args} + | Ty_bool -> Ty_app {args=Iter.empty} - (* TODO*) let view_as_data t = match Term.view t with | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args) + | Term.App_fun ({fun_view=Fun.Fun_select sel;_}, args) -> + assert (IArray.length args=1); + T_select (sel.select_cstor, sel.select_i, IArray.get args 0) + | Term.App_fun ({fun_view=Fun.Fun_is_a c;_}, args) -> + assert (IArray.length args=1); + T_is_a (c, IArray.get args 0) | _ -> T_other t let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args + let mk_is_a tst c u : Term.t = Term.app_fun tst (Fun.is_a c) (IArray.singleton u) + + let ty_is_finite = Ty.finite + let ty_set_is_finite = Ty.set_finite end) module Th_bool = Sidekick_th_bool_static.Make(struct diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index fa616caa..92887633 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -390,7 +390,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = let rec cstor = { Cstor. cstor_id; - cstor_is_a = ID.makef "is-a.%s" cstor_name; (* every fun needs a name *) + cstor_is_a = ID.makef "(is _ %s)" cstor_name; (* every fun needs a name *) cstor_args=lazy (mk_selectors cstor); cstor_ty_as_data=data; cstor_ty=data.data_as_ty; @@ -416,12 +416,12 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = data_id; data_cstors=lazy (cstors_of_data data cstors); data_as_ty=lazy ( - let def = Ty.Ty_data data in + let def = Ty.Ty_data { data; } in Ty.atomic def [] ); } in Ctx.add_id_ ctx data_name data_id - (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_data data))); + (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_data {data}))); data) l in diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 8e539fb8..1a5ce551 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -20,35 +20,12 @@ type ('c, 'ty) data_ty_view = args: 'ty Iter.t; } | Ty_data of { - cstors: 'c list; - } + cstors: 'c; + } | Ty_other let name = "th-data" -(** {2 Cardinality of types} *) - -module Ty_card = struct - type t = - | Finite - | Infinite - - let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let finite = Finite - let infinite = Infinite - - let sum = Iter.fold (+) Finite - let product = Iter.fold ( * ) Finite - - let equal : t -> t -> bool = (=) - let compare : t -> t -> int = Pervasives.compare - let pp out = function - | Finite -> Fmt.string out "finite" - | Infinite -> Fmt.string out "infinite" -end - (** An abtract representation of a datatype *) module type DATA_TY = sig type t @@ -56,6 +33,10 @@ module type DATA_TY = sig val equal : t -> t -> bool + val finite : t -> bool + + val set_finite : t -> bool -> unit + val view : t -> (cstor, t) data_ty_view val cstor_args : cstor -> t Iter.t @@ -64,40 +45,18 @@ module type DATA_TY = sig module Tbl : Hashtbl.S with type key = t end -(** Helper to compute the cardinality of types *) -module Compute_card(Ty : DATA_TY) : sig - type t - val create : unit -> t - val card : t -> Ty.t -> Ty_card.t -end = struct - module Card = Ty_card - type t = { - cards: Card.t Ty.Tbl.t; - } +(** {2 Cardinality of types} *) - let create() : t = { cards=Ty.Tbl.create 16} +module C = struct + type t = + | Finite + | Infinite - let card (self:t) (ty:Ty.t) : Card.t = - let rec aux (ty:Ty.t) : Card.t = - match Ty.Tbl.find self.cards ty with - | c -> c - | exception Not_found -> - Ty.Tbl.add self.cards ty Card.infinite; (* temp value, for fixpoint computation *) - let c = match Ty.view ty with - | Ty_other -> Card.finite - | Ty_app {args} -> Iter.map aux args |> Card.product - | Ty_arrow (args,ret) -> - Card.( (aux ret) ^ (Card.product @@ Iter.map aux args)) - | Ty_data { cstors; } -> - cstors - |> Iter.of_list - |> Iter.map (fun c -> Card.product (Iter.map aux @@ Ty.cstor_args c)) - |> Card.sum - in - Ty.Tbl.replace self.cards ty c; - c - in - aux ty + let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let sum = Iter.fold (+) Finite + let product = Iter.fold ( * ) Finite end module type ARG = sig @@ -105,12 +64,62 @@ module type ARG = sig module Cstor : sig type t + val ty_args : t -> S.T.Ty.t Iter.t val pp : t Fmt.printer val equal : t -> t -> bool end + + val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t - val as_datatype : S.T.Ty.t -> Cstor.t Iter.t option + val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t + val ty_is_finite : S.T.Ty.t -> bool + val ty_set_is_finite : S.T.Ty.t -> bool -> unit +end + +(** Helper to compute the cardinality of types *) +module Compute_card(A : ARG) : sig + type t + val create : unit -> t + val is_finite : t -> A.S.T.Ty.t -> bool +end = struct + module Ty = A.S.T.Ty + module Ty_tbl = CCHashtbl.Make(Ty) + type t = { + cards: C.t Ty_tbl.t; + } + + let create() : t = { cards=Ty_tbl.create 16} + + let card (self:t) (ty:Ty.t) : C.t = + let rec aux (ty:Ty.t) : C.t = + match Ty_tbl.find self.cards ty with + | c -> c + | exception Not_found -> + Ty_tbl.add self.cards ty C.Infinite; (* temp value, for fixpoint computation *) + let c = match A.as_datatype ty with + | Ty_other -> if A.ty_is_finite ty then C.Finite else C.Infinite + | Ty_app {args} -> Iter.map aux args |> C.product + | Ty_arrow (args,ret) -> + C.( (aux ret) ^ (C.product @@ Iter.map aux args)) + | Ty_data { cstors; } -> + let c = + cstors + |> Iter.map (fun c -> C.product (Iter.map aux @@ A.Cstor.ty_args c)) + |> C.sum + in + A.ty_set_is_finite ty (c=Finite); + c + in + Ty_tbl.replace self.cards ty c; + c + in + aux ty + + let is_finite self ty : bool = + match card self ty with + | C.Finite -> true + | C.Infinite -> false end module type S = sig @@ -123,9 +132,12 @@ module Make(A : ARG) : S with module A = A = struct module SI = A.S.Solver_internal module T = A.S.T.Term module N = SI.CC.N + module Ty = A.S.T.Ty module Fun = A.S.T.Fun module Expl = SI.CC.Expl + module Card = Compute_card(A) + type cstor_repr = { t: T.t; n: N.t; @@ -137,26 +149,71 @@ module Make(A : ARG) : S with module A = A = struct module N_tbl = Backtrackable_tbl.Make(N) type t = { + tst: T.state; cstors: cstor_repr N_tbl.t; (* repr -> cstor for the class *) + cards: Card.t; (* remember finiteness *) + to_decide: bool ref N_tbl.t; (* set of terms to decide. true means already clausified *) (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) + (* TODO: bitfield for types with less than 62 cstors, to quickly detect conflict? *) } + let push_level self = + N_tbl.push_level self.cstors; + N_tbl.push_level self.to_decide; + () + + let pop_levels self n = + N_tbl.pop_levels self.cstors n; + N_tbl.pop_levels self.to_decide n; + () + (* TODO: select/is-a, with exhaustivity rule *) (* TODO: acyclicity *) - let push_level self = N_tbl.push_level self.cstors - let pop_levels self n = N_tbl.pop_levels self.cstors n - (* attach data to constructor terms *) - let on_new_term self _solver n (t:T.t) = + let on_new_term_look_at_shape self n (t:T.t) = match A.view_as_data t with | T_cstor (cstor,args) -> Log.debugf 20 - (fun k->k "(@[th-cstor.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" - T.pp t A.Cstor.pp cstor (Util.pp_iarray T.pp) args); + (fun k->k "(@[%s.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" + name T.pp t A.Cstor.pp cstor (Util.pp_iarray T.pp) args); N_tbl.add self.cstors n {n; t; cstor; args}; + | T_select (cstor,i,u) -> + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.select[%d]@ %a@ :cstor %a@ :in %a@])" + name i T.pp t A.Cstor.pp cstor T.pp u); + (* TODO: remember that [u] must be decided *) + () + (* N_tbl.add self.cstors n {n; t; cstor; args}; *) + | T_is_a (cstor,u) -> + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.is-a@ %a@ :cstor %a@ :in %a@])" + name T.pp t A.Cstor.pp cstor T.pp u); + () + (* N_tbl.add self.cstors n {n; t; cstor; args}; *) + | T_other _ -> () + + (* remember terms of a datatype *) + let on_new_term_look_at_ty (self:t) n (t:T.t) : unit = + let ty = T.ty t in + match A.as_datatype ty with + | Ty_data _ -> + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.has-data-ty@ %a@ :ty %a@])" + name T.pp t Ty.pp ty); + if Card.is_finite self.cards ty && not (N_tbl.mem self.to_decide n) then ( + (* must decide this term *) + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.must-decide-finitey@ %a@])" name T.pp t); + N_tbl.add self.to_decide n (ref false); + ) | _ -> () + let on_new_term self _solver n t = + on_new_term_look_at_shape self n t; + on_new_term_look_at_ty self n t; + () + let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = begin match N_tbl.get self.cstors n1, N_tbl.get self.cstors n2 with | Some cr1, Some cr2 -> @@ -187,13 +244,57 @@ module Make(A : ARG) : S with module A = A = struct | None, None -> () end + let cstors_of_ty (ty:Ty.t) : A.Cstor.t Iter.t = + match A.as_datatype ty with + | Ty_data {cstors} -> cstors + | _ -> assert false + + let on_final_check (self:t) (solver:SI.t) (acts:SI.actions) _trail = + let remaining_to_decide = + N_tbl.to_iter self.to_decide + |> Iter.map (fun (n,r) -> SI.cc_find solver n, r) + |> Iter.filter (fun (n,r) -> not !r && not (N_tbl.mem self.cstors n)) + |> Iter.to_rev_list + in + begin match remaining_to_decide with + | [] -> () + | l -> + Log.debugf 10 + (fun k->k "(@[%s.must-decide@ %a@])" name + (Util.pp_list (Fmt.map fst N.pp)) l); + (* add clauses [∨_c is-c(t)] and [¬(is-a t) ∨ ¬(is-b t)] *) + List.iter + (fun (n,r) -> + assert (not !r); + let t = N.term n in + let c = + cstors_of_ty (T.ty t) + |> Iter.map (fun c -> A.mk_is_a self.tst c t) + |> Iter.map (SI.mk_lit solver acts) + |> Iter.to_rev_list + in + r := true; + SI.add_clause_permanent solver acts c; + Iter.diagonal_l c + (fun (c1,c2) -> + SI.add_clause_permanent solver acts + [SI.Lit.neg c1; SI.Lit.neg c2]); + ()) + l + end; + () + let create_and_setup (solver:SI.t) : t = let self = { + tst=SI.tst solver; cstors=N_tbl.create ~size:32 (); + to_decide=N_tbl.create ~size:16 (); + cards=Card.create(); } in Log.debugf 1 (fun k->k "(setup :%s)" name); SI.on_cc_new_term solver (on_new_term self); SI.on_cc_pre_merge solver (on_pre_merge self); + SI.on_final_check solver (on_final_check self); self let theory =