wip: theory of datatypes

src/base-term/Base_types.ml

@@ -977,6 +977,7 @@ module Cstor = struct
     cstor_ty: ty lazy_t;
   }
   let equal = eq_cstor
+  let pp out c = ID.pp out c.cstor_id
 end
 
 module Select = struct

src/main/main.ml

@@ -143,7 +143,7 @@ let main () =
     let theories =
       if is_cnf then [] else [
         Process.th_bool ;
-        Process.th_cstor;
+        Process.th_data;
       ]
     in
     Process.Solver.create ~store_proof:!check ~theories tst ()

src/smtlib/Process.ml

@@ -262,11 +262,19 @@ module Th_data = Sidekick_th_data.Make(struct
     module S = Solver
     open Base_types
     open Sidekick_th_data
+    module Cstor = Cstor
+
+    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
 
     (* TODO*)
-    let view_as_cstor t = match Term.view t with
-      | Term.App_fun ({fun_view=Fun.Fun_cstor _;_} as f, args) -> T_cstor (f, args)
+    let view_as_data t = match Term.view t with
+      | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args)
       | _ -> T_other t
+
+    let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args
   end)
 
 module Th_bool = Sidekick_th_bool_static.Make(struct
@@ -276,4 +284,4 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
 end)
 
 let th_bool : Solver.theory = Th_bool.theory
-let th_cstor : Solver.theory = Th_cstor.theory
+let th_data : Solver.theory = Th_data.theory

src/smtlib/Process.mli

@@ -8,7 +8,7 @@ module Solver
                             and type T.Ty.t = Ty.t
 
 val th_bool : Solver.theory
-val th_cstor : Solver.theory
+val th_data : Solver.theory
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/dune

@@ -3,7 +3,7 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick.base-term sidekick.th-bool-static
-   sidekick.mini-cc sidekick.th-cstor msat.backend smtlib-utils)
+   sidekick.mini-cc sidekick.th-data msat.backend smtlib-utils)
  (flags :standard -warn-error -27-37 -open Sidekick_util))
 
 ; TODO: enable warn-error again

src/th-data/Sidekick_th_data.ml

@@ -102,9 +102,15 @@ end
 
 module type ARG = sig
   module S : Sidekick_core.SOLVER
-  val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view
-  val mk_cstor : S.T.Term.state -> S.T.Fun.t -> S.T.Term.t IArray.t -> S.T.Term.t
-  val as_datatype : S.T.Ty.t -> S.T.Fun.t list option
+
+  module Cstor : sig
+    type t
+    val pp : t Fmt.printer
+    val equal : t -> t -> bool
+  end
+  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
 end
 
 module type S = sig
@@ -123,7 +129,7 @@ module Make(A : ARG) : S with module A = A = struct
   type cstor_repr = {
     t: T.t;
     n: N.t;
-    cstor: Fun.t;
+    cstor: A.Cstor.t;
     args: T.t IArray.t;
   }
   (* associate to each class a unique constructor term in the class (if any) *)
@@ -135,16 +141,19 @@ module Make(A : ARG) : S with module A = A = struct
     (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *)
   }
 
+  (* 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) =
-    match A.view_as_cstor t with
+    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 Fun.pp cstor (Util.pp_iarray T.pp) args);
+            T.pp t A.Cstor.pp cstor (Util.pp_iarray T.pp) args);
       N_tbl.add self.cstors n {n; t; cstor; args};
     | _ -> ()
 
@@ -162,7 +171,7 @@ module Make(A : ARG) : S with module A = A = struct
             Expl.mk_merge n2 cr2.n;
           ]
         in
-        if Fun.equal cr1.cstor cr2.cstor then (
+        if A.Cstor.equal cr1.cstor cr2.cstor then (
           (* same function: injectivity *)
           assert (IArray.length cr1.args = IArray.length cr2.args);
           IArray.iter2
@@ -182,7 +191,7 @@ module Make(A : ARG) : S with module A = A = struct
     let self = {
       cstors=N_tbl.create ~size:32 ();
     } in
-    Log.debug 1 "(setup :th-cstor)";
+    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);
     self

src/th-data/types.ml

@@ -1,3 +1,4 @@
+(*
 
 and datatype = {
   data_cstors: data_cstor ID.Map.t lazy_t;
@@ -48,3 +49,4 @@ let cstor_proj cstor i t =
   let p = IArray.get (Lazy.force cstor.cstor_proj) i in
   app_cst p (IArray.singleton t)
 
+   *)