mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
wip: theory of datatypes
This commit is contained in:
Simon Cruanes
parent
8c5e28da28
commit
444a0b9f85
6 changed files with 222 additions and 144 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 ->
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 =
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue