wip: refactor(base): split into several views, all based on Const

src/base/Arith_types_.ml

@@ -1,5 +1,7 @@
-let hash_z = Z.hash
-let[@inline] hash_q q = CCHash.combine2 (hash_z (Q.num q)) (hash_z (Q.den q))
+open struct
+  let hash_z = Z.hash
+  let[@inline] hash_q q = CCHash.combine2 (hash_z (Q.num q)) (hash_z (Q.den q))
+end
 
 module LRA_pred = struct
   type t = Sidekick_th_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq

src/base/Data_ty.ml

@@ -0,0 +1,113 @@
+open Types_
+
+type select = Types_.select = {
+  select_id: ID.t;
+  select_cstor: cstor;
+  select_ty: ty lazy_t;
+  select_i: int;
+}
+
+type cstor = Types_.cstor = {
+  cstor_id: ID.t;
+  cstor_is_a: ID.t;
+  mutable cstor_arity: int;
+  cstor_args: select list lazy_t;
+  cstor_ty_as_data: data;
+  cstor_ty: ty lazy_t;
+}
+
+type t = data = {
+  data_id: ID.t;
+  data_cstors: cstor ID.Map.t lazy_t;
+  data_as_ty: ty lazy_t;
+}
+
+let pp out d = ID.pp out d.data_id
+let equal a b = ID.equal a.data_id b.data_id
+let hash a = ID.hash a.data_id
+
+(** Datatype selectors.
+
+    A selector is a kind of function that allows to obtain an argument
+    of a given constructor. *)
+module Select = struct
+  type t = Types_.select = {
+    select_id: ID.t;
+    select_cstor: cstor;
+    select_ty: ty lazy_t;
+    select_i: int;
+  }
+
+  let ty sel = Lazy.force sel.select_ty
+
+  let equal a b =
+    ID.equal a.select_id b.select_id
+    && ID.equal a.select_cstor.cstor_id b.select_cstor.cstor_id
+    && a.select_i = b.select_i
+
+  let hash a =
+    Hash.combine4 1952 (ID.hash a.select_id)
+      (ID.hash a.select_cstor.cstor_id)
+      (Hash.int a.select_i)
+
+  let pp out self =
+    Fmt.fprintf out "select.%a[%d]" ID.pp self.select_cstor.cstor_id
+      self.select_i
+end
+
+(** Datatype constructors.
+
+    A datatype has one or more constructors, each of which is a special
+    kind of function symbol. Constructors are injective and pairwise distinct. *)
+module Cstor = struct
+  type t = cstor
+
+  let id c = c.cstor_id
+  let hash c = ID.hash c.cstor_id
+  let ty_args c = Lazy.force c.cstor_args |> Iter.of_list |> Iter.map Select.ty
+  let equal a b = ID.equal a.cstor_id b.cstor_id
+  let pp out c = ID.pp out c.cstor_id
+end
+
+type Const.view +=
+  | Data of data
+  | Cstor of cstor
+  | Select of select
+  | Is_a of cstor
+
+let ops =
+  (module struct
+    let pp out = function
+      | Data d -> pp out d
+      | Cstor c -> Cstor.pp out c
+      | Select s -> Select.pp out s
+      | Is_a c -> Fmt.fprintf out "(_ is %a)" Cstor.pp c
+      | _ -> assert false
+
+    let equal a b =
+      match a, b with
+      | Data a, Data b -> equal a b
+      | Cstor a, Cstor b -> Cstor.equal a b
+      | Select a, Select b -> Select.equal a b
+      | Is_a a, Is_a b -> Cstor.equal a b
+      | _ -> false
+
+    let hash = function
+      | Data d -> Hash.combine2 592 (hash d)
+      | Cstor c -> Hash.combine2 593 (Cstor.hash c)
+      | Select s -> Hash.combine2 594 (Select.hash s)
+      | Is_a c -> Hash.combine2 595 (Cstor.hash c)
+      | _ -> assert false
+  end : Const.DYN_OPS)
+
+let data tst d : Term.t =
+  Term.const tst @@ Const.make (Data d) ops ~ty:(Term.type_ tst)
+
+let cstor tst c : Term.t =
+  Term.const tst @@ Const.make (Cstor c) ops ~ty:(Lazy.force c.cstor_ty)
+
+let select tst s : Term.t =
+  Term.const tst @@ Const.make (Select s) ops ~ty:(Lazy.force s.select_ty)
+
+let is_a tst c : Term.t =
+  Term.const tst @@ Const.make (Is_a c) ops ~ty:(Term.bool tst)

src/base/Data_ty.mli

@@ -0,0 +1,51 @@
+open Types_
+
+type select = Types_.select = {
+  select_id: ID.t;
+  select_cstor: cstor;
+  select_ty: ty lazy_t;
+  select_i: int;
+}
+
+type cstor = Types_.cstor = {
+  cstor_id: ID.t;
+  cstor_is_a: ID.t;
+  mutable cstor_arity: int;
+  cstor_args: select list lazy_t;
+  cstor_ty_as_data: data;
+  cstor_ty: ty lazy_t;
+}
+
+type t = data = {
+  data_id: ID.t;
+  data_cstors: cstor ID.Map.t lazy_t;
+  data_as_ty: ty lazy_t;
+}
+
+type Const.view +=
+  private
+  | Data of data
+  | Cstor of cstor
+  | Select of select
+  | Is_a of cstor
+
+include Sidekick_sigs.EQ_HASH_PRINT with type t := t
+
+module Select : sig
+  type t = select
+
+  include Sidekick_sigs.EQ_HASH_PRINT with type t := t
+end
+
+module Cstor : sig
+  type t = cstor
+
+  include Sidekick_sigs.EQ_HASH_PRINT with type t := t
+end
+
+val data : Term.store -> t -> Term.t
+val cstor : Term.store -> cstor -> Term.t
+val select : Term.store -> select -> Term.t
+val is_a : Term.store -> cstor -> Term.t
+
+(* TODO: select_ : store -> cstor -> int -> term *)

src/base/Form.ml

@@ -1,14 +1,164 @@
-(*
+open Types_
+open Sidekick_core
+module T = Term
 
-(** Formulas (boolean terms).
+type ty = Term.t
+type term = Term.t
 
-    This module defines function symbols, constants, and views
-    to manipulate boolean formulas in {!Sidekick_base}.
-    This is useful to have the ability to use boolean connectives instead
-    of being limited to clauses; by using {!Sidekick_th_bool_static},
-    the formulas are turned into clauses automatically for you.
+type ('a, 'args) view = ('a, 'args) Sidekick_core.Bool_view.t =
+  | B_bool of bool
+  | B_not of 'a
+  | B_and of 'args
+  | B_or of 'args
+  | B_imply of 'args * 'a
+  | B_equiv of 'a * 'a
+  | B_xor of 'a * 'a
+  | B_eq of 'a * 'a
+  | B_neq of 'a * 'a
+  | B_ite of 'a * 'a * 'a
+  | B_atom of 'a
+
+(* ### allocate special IDs for connectors *)
+
+let id_and = ID.make "and"
+let id_or = ID.make "or"
+let id_imply = ID.make "=>"
+
+(* ### view *)
+
+exception Not_a_th_term
+
+let view_id_ fid args =
+  if ID.equal fid id_and then
+    B_and args
+  else if ID.equal fid id_or then
+    B_or args
+  else if ID.equal fid id_imply then (
+    match args with
+    | [ arg; concl ] -> B_imply ([ arg ], concl)
+    | _ -> raise_notrace Not_a_th_term
+  ) else
+    raise_notrace Not_a_th_term
+
+let view (t : T.t) : (T.t, _) view =
+  let hd, args = T.unfold_app t in
+  match T.view hd, args with
+  | E_const { Const.c_view = T.C_true; _ }, [] -> B_bool true
+  | E_const { Const.c_view = T.C_false; _ }, [] -> B_bool false
+  | E_const { Const.c_view = T.C_not; _ }, [ a ] -> B_not a
+  | E_const { Const.c_view = T.C_eq; _ }, [ _ty; a; b ] -> B_eq (a, b)
+  | E_const { Const.c_view = T.C_ite; _ }, [ _ty; a; b; c ] -> B_ite (a, b, c)
+  | E_const { Const.c_view = Uconst.Uconst { uc_id; _ }; _ }, _ ->
+    (try view_id_ uc_id args with Not_a_th_term -> B_atom t)
+  | _ -> B_atom t
+
+(* TODO
+   let and_l st l =
+     match flatten_id id_and true l with
+     | [] -> T.true_ st
+     | l when List.exists T.is_false l -> T.false_ st
+     | [ x ] -> x
+     | args -> T.app_fun st Funs.and_ (CCArray.of_list args)
+
+   let or_l st l =
+     match flatten_id id_or false l with
+     | [] -> T.false_ st
+     | l when List.exists T.is_true l -> T.true_ st
+     | [ x ] -> x
+     | args -> T.app_fun st Funs.or_ (CCArray.of_list args)
 *)
 
+let c_and tst : Term.t =
+  let bool = Term.bool tst in
+  Uconst.uconst_of_id' tst id_and [ bool; bool ] bool
+
+let c_or tst : Term.t =
+  let bool = Term.bool tst in
+  Uconst.uconst_of_id' tst id_or [ bool; bool ] bool
+
+let c_imply tst : Term.t =
+  let bool = Term.bool tst in
+  Uconst.uconst_of_id' tst id_imply [ bool; bool ] bool
+
+let bool = Term.bool_val
+let and_ tst a b = Term.app_l tst (c_and tst) [ a; b ]
+let or_ tst a b = Term.app_l tst (c_or tst) [ a; b ]
+let imply tst a b = Term.app_l tst (c_imply tst) [ a; b ]
+let eq = T.eq
+let not_ = T.not
+let ite = T.ite
+let neq st a b = not_ st @@ eq st a b
+let imply_l tst xs y = List.fold_right (imply tst) xs y
+
+let equiv tst a b =
+  if (not (T.is_bool (T.ty a))) || not (T.is_bool (T.ty b)) then
+    failwith "Form.equiv: takes boolean arguments";
+  T.eq tst a b
+
+let xor tst a b = not_ tst (equiv tst a b)
+
+let and_l tst = function
+  | [] -> T.true_ tst
+  | [ x ] -> x
+  | x :: tl -> List.fold_left (and_ tst) x tl
+
+let or_l tst = function
+  | [] -> T.false_ tst
+  | [ x ] -> x
+  | x :: tl -> List.fold_left (or_ tst) x tl
+
+let distinct_l tst l =
+  match l with
+  | [] | [ _ ] -> T.true_ tst
+  | l ->
+    (* turn into [and_{i<j} t_i != t_j] *)
+    let cs = CCList.diagonal l |> List.map (fun (a, b) -> neq tst a b) in
+    and_l tst cs
+
+let mk_of_view tst = function
+  | B_bool b -> T.bool_val tst b
+  | B_atom t -> t
+  | B_and l -> and_l tst l
+  | B_or l -> or_l tst l
+  | B_imply (a, b) -> imply_l tst a b
+  | B_ite (a, b, c) -> ite tst a b c
+  | B_equiv (a, b) -> equiv tst a b
+  | B_xor (a, b) -> not_ tst (equiv tst a b)
+  | B_eq (a, b) -> T.eq tst a b
+  | B_neq (a, b) -> not_ tst (T.eq tst a b)
+  | B_not t -> not_ tst t
+
+(*
+  let eval id args =
+    let open Value in
+    match view_id id args with
+    | B_bool b -> Value.bool b
+    | B_not (V_bool b) -> Value.bool (not b)
+    | B_and a when Iter.for_all Value.is_true a -> Value.true_
+    | B_and a when Iter.exists Value.is_false a -> Value.false_
+    | B_or a when Iter.exists Value.is_true a -> Value.true_
+    | B_or a when Iter.for_all Value.is_false a -> Value.false_
+    | B_imply (_, V_bool true) -> Value.true_
+    | B_imply (a, _) when Iter.exists Value.is_false a -> Value.true_
+    | B_imply (a, b) when Iter.for_all Value.is_true a && Value.is_false b ->
+      Value.false_
+    | B_ite (a, b, c) ->
+      if Value.is_true a then
+        b
+      else if Value.is_false a then
+        c
+      else
+        Error.errorf "non boolean value %a in ite" Value.pp a
+    | B_equiv (a, b) | B_eq (a, b) -> Value.bool (Value.equal a b)
+    | B_xor (a, b) | B_neq (a, b) -> Value.bool (not (Value.equal a b))
+    | B_atom v -> v
+    | B_opaque_bool t -> Error.errorf "cannot evaluate opaque bool %a" pp t
+    | B_not _ | B_and _ | B_or _ | B_imply _ ->
+      Error.errorf "non boolean value in boolean connective"
+      *)
+
+(*
+
 module T = Base_types.Term
 module Ty = Base_types.Ty
 module Fun = Base_types.Fun

src/base/Form.mli

@@ -0,0 +1,48 @@
+(** Formulas (boolean terms).
+
+    This module defines function symbols, constants, and views
+    to manipulate boolean formulas in {!Sidekick_base}.
+    This is useful to have the ability to use boolean connectives instead
+    of being limited to clauses; by using {!Sidekick_th_bool_static},
+    the formulas are turned into clauses automatically for you.
+*)
+
+open Types_
+
+type term = Term.t
+
+type ('a, 'args) view = ('a, 'args) Sidekick_core.Bool_view.t =
+  | B_bool of bool
+  | B_not of 'a
+  | B_and of 'args
+  | B_or of 'args
+  | B_imply of 'args * 'a
+  | B_equiv of 'a * 'a
+  | B_xor of 'a * 'a
+  | B_eq of 'a * 'a
+  | B_neq of 'a * 'a
+  | B_ite of 'a * 'a * 'a
+  | B_atom of 'a
+
+val view : term -> (term, term list) view
+val bool : Term.store -> bool -> term
+val not_ : Term.store -> term -> term
+val and_ : Term.store -> term -> term -> term
+val or_ : Term.store -> term -> term -> term
+val eq : Term.store -> term -> term -> term
+val neq : Term.store -> term -> term -> term
+val imply : Term.store -> term -> term -> term
+val equiv : Term.store -> term -> term -> term
+val xor : Term.store -> term -> term -> term
+val ite : Term.store -> term -> term -> term
+
+(* *)
+
+val and_l : Term.store -> term list -> term
+val or_l : Term.store -> term list -> term
+val imply_l : Term.store -> term list -> term -> term
+val mk_of_view : Term.store -> (term, term list) view -> term
+
+(* TODO?
+   val make : Term.store -> (term, term list) view -> term
+*)

src/base/Sidekick_base.ml

@@ -1,4 +1,4 @@
-(** {1 Sidekick base}
+(** Sidekick base
 
     This library is a starting point for writing concrete implementations
     of SMT solvers with Sidekick.
@@ -14,26 +14,35 @@
     etc. Logic formats such as SMT-LIB 2.6 are in fact based on a similar
     notion of statements, and a [.smt2] files contains a list of statements.
 
-    *)
+*)
 
-module Term = Sidekick_core.Term
-module Base_types = Base_types
-module ID = ID
-module Stat = Stat
-module Value = Base_types.Value
-module Term_cell = Base_types.Term_cell
-module Statement = Base_types.Statement
-module Data = Base_types.Data
-module Select = Base_types.Select
-module Form = Form
-module LRA_view = Base_types.LRA_view
-module LRA_pred = Base_types.LRA_pred
-module LRA_op = Base_types.LRA_op
-module LIA_view = Base_types.LIA_view
-module LIA_pred = Base_types.LIA_pred
-module LIA_op = Base_types.LIA_op
-module Solver_arg = Solver_arg
-module Lit = Lit
-module Proof = Proof
-module Proof_quip = Proof_quip
 module Types_ = Types_
+module Term = Sidekick_core.Term
+module Ty = Ty
+module ID = ID
+module Form = Form
+include Arith_types_
+module Data_ty = Data_ty
+module Cstor = Data_ty.Cstor
+module Select = Data_ty.Select
+module Statement = Statement
+module Uconst = Uconst
+
+(* TODO
+
+   module Value = Value
+   module Statement = Statement
+   module Data = Data
+   module Select = Select
+
+      module LRA_view = Types_.LRA_view
+      module LRA_pred = Base_types.LRA_pred
+      module LRA_op = Base_types.LRA_op
+      module LIA_view = Base_types.LIA_view
+      module LIA_pred = Base_types.LIA_pred
+      module LIA_op = Base_types.LIA_op
+*)
+
+(*
+module Proof_quip = Proof_quip
+*)

src/base/Solver_arg.ml

@@ -1,4 +0,0 @@
-open! Base_types
-module Term = Term
-module Fun = Fun
-module Ty = Ty

src/base/Solver_arg.mli

@@ -1,15 +0,0 @@
-(** Concrete implementation of {!Sidekick_core.TERM}
-
-    this module gathers most definitions above in a form
-    that is compatible with what Sidekick expects for terms, functions, etc.
-*)
-
-open Base_types
-
-include
-  Sidekick_core.TERM
-    with type Term.t = Term.t
-     and type Fun.t = Fun.t
-     and type Ty.t = Ty.t
-     and type Term.store = Term.store
-     and type Ty.store = Ty.store

src/base/Statement.ml

@@ -0,0 +1,48 @@
+open Sidekick_core
+open Types_
+
+type t = statement =
+  | Stmt_set_logic of string
+  | Stmt_set_option of string list
+  | Stmt_set_info of string * string
+  | Stmt_data of data list
+  | Stmt_ty_decl of ID.t * int (* new atomic cstor *)
+  | Stmt_decl of ID.t * ty list * ty
+  | Stmt_define of definition list
+  | Stmt_assert of term
+  | Stmt_assert_clause of term list
+  | Stmt_check_sat of (bool * term) list
+  | Stmt_get_model
+  | Stmt_get_value of term list
+  | Stmt_exit
+
+(** Pretty print a statement *)
+let pp out = function
+  | Stmt_set_logic s -> Fmt.fprintf out "(set-logic %s)" s
+  | Stmt_set_option l ->
+    Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l
+  | Stmt_set_info (a, b) -> Fmt.fprintf out "(@[set-info@ %s@ %s@])" a b
+  | Stmt_check_sat [] -> Fmt.string out "(check-sat)"
+  | Stmt_check_sat l ->
+    let pp_pair out (b, t) =
+      if b then
+        Term.pp_debug out t
+      else
+        Fmt.fprintf out "(@[not %a@])" Term.pp_debug t
+    in
+    Fmt.fprintf out "(@[check-sat-assuming@ (@[%a@])@])" (Fmt.list pp_pair) l
+  | Stmt_ty_decl (s, n) -> Fmt.fprintf out "(@[declare-sort@ %a %d@])" ID.pp s n
+  | Stmt_decl (id, args, ret) ->
+    Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])" ID.pp id
+      (Util.pp_list Ty.pp) args Ty.pp ret
+  | Stmt_assert t -> Fmt.fprintf out "(@[assert@ %a@])" Term.pp_debug t
+  | Stmt_assert_clause c ->
+    Fmt.fprintf out "(@[assert-clause@ %a@])" (Util.pp_list Term.pp_debug) c
+  | Stmt_exit -> Fmt.string out "(exit)"
+  | Stmt_data l ->
+    Fmt.fprintf out "(@[declare-datatypes@ %a@])" (Util.pp_list Data_ty.pp) l
+  | Stmt_get_model -> Fmt.string out "(get-model)"
+  | Stmt_get_value l ->
+    Fmt.fprintf out "(@[get-value@ (@[%a@])@])" (Util.pp_list Term.pp_debug) l
+  | Stmt_define _ -> assert false
+(* TODO *)

src/base/Statement.mli

@@ -0,0 +1,24 @@
+(** Statements.
+
+    A statement is an instruction for the SMT solver to do something,
+    like asserting that a formula is true, declaring a new constant,
+    or checking satisfiabilty of the current set of assertions. *)
+
+open Types_
+
+type t = statement =
+  | Stmt_set_logic of string
+  | Stmt_set_option of string list
+  | Stmt_set_info of string * string
+  | Stmt_data of data list
+  | Stmt_ty_decl of ID.t * int (* new atomic cstor *)
+  | Stmt_decl of ID.t * ty list * ty
+  | Stmt_define of definition list
+  | Stmt_assert of term
+  | Stmt_assert_clause of term list
+  | Stmt_check_sat of (bool * term) list
+  | Stmt_get_model
+  | Stmt_get_value of term list
+  | Stmt_exit
+
+include Sidekick_sigs.PRINT with type t := t

src/base/Ty.ml

@@ -4,6 +4,8 @@ open Sidekick_core
 include Sidekick_core.Term
 open Types_
 
+let pp = pp_debug
+
 type Const.view += Ty of ty_view
 type data = Types_.data
 
@@ -14,8 +16,7 @@ let ops_ty : Const.ops =
         (match ty with
         | Ty_real -> Fmt.string out "Real"
         | Ty_int -> Fmt.string out "Int"
-        | Ty_uninterpreted { id; _ } -> ID.pp out id
-        | Ty_data d -> ID.pp out d.data.data_id)
+        | Ty_uninterpreted { id; _ } -> ID.pp out id)
       | _ -> ()
 
     let equal a b =
@@ -24,8 +25,7 @@ let ops_ty : Const.ops =
         (match a, b with
         | Ty_int, Ty_int | Ty_real, Ty_real -> true
         | Ty_uninterpreted u1, Ty_uninterpreted u2 -> ID.equal u1.id u2.id
-        | Ty_data d1, Ty_data d2 -> ID.equal d1.data.data_id d2.data.data_id
-        | (Ty_real | Ty_int | Ty_uninterpreted _ | Ty_data _), _ -> false)
+        | (Ty_real | Ty_int | Ty_uninterpreted _), _ -> false)
       | _ -> false
 
     let hash = function
@@ -33,8 +33,7 @@ let ops_ty : Const.ops =
         (match a with
         | Ty_real -> Hash.int 2
         | Ty_int -> Hash.int 3
-        | Ty_uninterpreted u -> Hash.combine2 10 (ID.hash u.id)
-        | Ty_data d -> Hash.combine2 30 (ID.hash d.data.data_id))
+        | Ty_uninterpreted u -> Hash.combine2 10 (ID.hash u.id))
       | _ -> assert false
   end)
 
@@ -51,8 +50,6 @@ let real tst : ty = mk_ty0 tst Ty_real
 let uninterpreted tst id : t =
   mk_ty0 tst (Ty_uninterpreted { id; finite = false })
 
-let data tst data : t = mk_ty0 tst (Ty_data { data })
-
 let is_uninterpreted (self : t) =
   match view self with
   | E_const { Const.c_view = Ty (Ty_uninterpreted _); _ } -> true

src/base/Ty.mli

@@ -7,11 +7,12 @@ end
 type t = ty
 type data = Types_.data
 
+include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
+
 val bool : store -> t
 val real : store -> t
 val int : store -> t
 val uninterpreted : store -> ID.t -> t
-val data : store -> data -> t
 val is_uninterpreted : t -> bool
 
 (* TODO: separate functor?

src/base/Uconst.ml

@@ -0,0 +1,51 @@
+open Types_
+
+type ty = Term.t
+type t = Types_.uconst = { uc_id: ID.t; uc_ty: ty }
+
+let[@inline] id self = self.uc_id
+let[@inline] ty self = self.uc_ty
+let equal a b = ID.equal a.uc_id b.uc_id
+let compare a b = ID.compare a.uc_id b.uc_id
+let hash a = ID.hash a.uc_id
+let pp out c = ID.pp out c.uc_id
+
+type Const.view += Uconst of t
+
+let ops =
+  (module struct
+    let pp out = function
+      | Uconst c -> pp out c
+      | _ -> assert false
+
+    let equal a b =
+      match a, b with
+      | Uconst a, Uconst b -> equal a b
+      | _ -> false
+
+    let hash = function
+      | Uconst c -> Hash.combine2 522660 (hash c)
+      | _ -> assert false
+  end : Const.DYN_OPS)
+
+let[@inline] make uc_id uc_ty : t = { uc_id; uc_ty }
+
+let uconst tst (self : t) : Term.t =
+  Term.const tst @@ Const.make (Uconst self) ops ~ty:self.uc_ty
+
+let uconst_of_id tst id ty = uconst tst @@ make id ty
+
+let uconst_of_id' tst id args ret =
+  let ty = Term.arrow_l tst args ret in
+  uconst_of_id tst id ty
+
+module As_key = struct
+  type nonrec t = t
+
+  let compare = compare
+  let equal = equal
+  let hash = hash
+end
+
+module Map = CCMap.Make (As_key)
+module Tbl = CCHashtbl.Make (As_key)

src/base/Uconst.mli

@@ -0,0 +1,23 @@
+(** Uninterpreted constants *)
+
+open Types_
+
+type ty = Term.t
+type t = Types_.uconst = { uc_id: ID.t; uc_ty: ty }
+
+val id : t -> ID.t
+val ty : t -> ty
+
+type Const.view += private Uconst of t
+
+include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
+
+val make : ID.t -> ty -> t
+(** Make a new uninterpreted function. *)
+
+val uconst : Term.store -> t -> Term.t
+val uconst_of_id : Term.store -> ID.t -> ty -> Term.t
+val uconst_of_id' : Term.store -> ID.t -> ty list -> ty -> Term.t
+
+module Map : CCMap.S with type key = t
+module Tbl : CCHashtbl.S with type key = t

src/base/solver/dune

@@ -1,9 +0,0 @@
-(library
- (name sidekick_base_solver)
- (public_name sidekick-base.solver)
- (synopsis "Instantiation of solver and theories for Sidekick_base")
- (libraries sidekick-base sidekick.core sidekick.smt-solver
-   sidekick.th-bool-static sidekick.mini-cc sidekick.th-data sidekick.th-lra
-   sidekick.zarith)
- (flags :standard -warn-error -a+8 -safe-string -color always -open
-   Sidekick_util))

src/base/solver/sidekick_base_solver.ml

@@ -1,142 +0,0 @@
-(** SMT Solver and Theories for [Sidekick_base].
-
-    This contains instances of the SMT solver, and theories,
-    from {!Sidekick_core}, using data structures from
-    {!Sidekick_base}. *)
-
-open! Sidekick_base
-
-(** Argument to the SMT solver *)
-module Solver_arg = struct
-  module T = Sidekick_base.Solver_arg
-  module Lit = Sidekick_base.Lit
-
-  let view_as_cc = Term.cc_view
-  let mk_eq = Term.eq
-  let is_valid_literal _ = true
-
-  module Proof_trace = Sidekick_base.Proof.Proof_trace
-  module Rule_core = Sidekick_base.Proof.Rule_core
-  module Rule_sat = Sidekick_base.Proof.Rule_sat
-
-  type step_id = Proof_trace.A.step_id
-  type rule = Proof_trace.A.rule
-end
-
-module Solver = Sidekick_smt_solver.Make (Solver_arg)
-(** SMT solver, obtained from {!Sidekick_smt_solver} *)
-
-(** Theory of datatypes *)
-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; _ } ->
-      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_real | Ty_int -> Ty_app { args = Iter.empty }
-
-  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 (CCArray.length args = 1);
-      T_select (sel.select_cstor, sel.select_i, CCArray.get args 0)
-    | Term.App_fun ({ fun_view = Fun.Fun_is_a c; _ }, args) ->
-      assert (CCArray.length args = 1);
-      T_is_a (c, CCArray.get args 0)
-    | _ -> T_other t
-
-  let mk_eq = Term.eq
-  let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args
-  let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) [| u |]
-
-  let mk_is_a tst c u : Term.t =
-    if c.cstor_arity = 0 then
-      Term.eq tst u (Term.const tst (Fun.cstor c))
-    else
-      Term.app_fun tst (Fun.is_a c) [| u |]
-
-  let ty_is_finite = Ty.finite
-  let ty_set_is_finite = Ty.set_finite
-
-  module P = Proof.Rule_data
-end)
-
-(** Reducing boolean formulas to clauses *)
-module Th_bool = Sidekick_th_bool_static.Make (struct
-  module S = Solver
-
-  type term = S.T.Term.t
-
-  include Form
-  module P = Proof.Rule_bool
-end)
-
-module Gensym = struct
-  type t = { tst: Term.store; mutable fresh: int }
-
-  let create tst : t = { tst; fresh = 0 }
-  let tst self = self.tst
-  let copy s = { s with tst = s.tst }
-
-  let fresh_term (self : t) ~pre (ty : Ty.t) : Term.t =
-    let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in
-    self.fresh <- 1 + self.fresh;
-    let id = ID.make name in
-    Term.const self.tst @@ Fun.mk_undef_const id ty
-end
-
-(** Theory of Linear Rational Arithmetic *)
-module Th_lra = Sidekick_arith_lra.Make (struct
-  module S = Solver
-  module T = Term
-  module Z = Sidekick_zarith.Int
-  module Q = Sidekick_zarith.Rational
-
-  type term = S.T.Term.t
-  type ty = S.T.Ty.t
-
-  module LRA = Sidekick_arith_lra
-
-  let mk_eq = Form.eq
-
-  let mk_lra store l =
-    match l with
-    | LRA.LRA_other x -> x
-    | LRA.LRA_pred (p, x, y) -> T.lra store (Pred (p, x, y))
-    | LRA.LRA_op (op, x, y) -> T.lra store (Op (op, x, y))
-    | LRA.LRA_const c -> T.lra store (Const c)
-    | LRA.LRA_mult (c, x) -> T.lra store (Mult (c, x))
-
-  let mk_bool = T.bool
-
-  let rec view_as_lra t =
-    match T.view t with
-    | T.LRA l ->
-      let module LRA = Sidekick_arith_lra in
-      (match l with
-      | Const c -> LRA.LRA_const c
-      | Pred (p, a, b) -> LRA.LRA_pred (p, a, b)
-      | Op (op, a, b) -> LRA.LRA_op (op, a, b)
-      | Mult (c, x) -> LRA.LRA_mult (c, x)
-      | To_real x -> view_as_lra x
-      | Var x -> LRA.LRA_other x)
-    | T.Eq (a, b) when Ty.equal (T.ty a) (Ty.real ()) -> LRA.LRA_pred (Eq, a, b)
-    | _ -> LRA.LRA_other t
-
-  let ty_lra _st = Ty.real ()
-  let has_ty_real t = Ty.equal (T.ty t) (Ty.real ())
-  let lemma_lra = Proof.lemma_lra
-
-  module Gensym = Gensym
-end)
-
-let th_bool : Solver.theory = Th_bool.theory
-let th_data : Solver.theory = Th_data.theory
-let th_lra : Solver.theory = Th_lra.theory

src/base/types_.ml

@@ -9,33 +9,16 @@ type term = Term.t
 type ty = Term.t
 type value = Term.t
 
-type fun_view =
-  | Fun_undef of ty (* simple undefined constant *)
-  | Fun_select of select
-  | Fun_cstor of cstor
-  | Fun_is_a of cstor
-  | Fun_def of {
-      pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
-      abs: self:term -> term array -> term * bool; (* remove the sign? *)
-      do_cc: bool; (* participate in congruence closure? *)
-      relevant: 'a. ID.t -> 'a array -> int -> bool; (* relevant argument? *)
-      ty: ID.t -> term array -> ty; (* compute type *)
-      eval: value array -> value; (* evaluate term *)
-    }
-      (** Methods on the custom term view whose arguments are ['a].
-    Terms must be printable, and provide some additional theory handles.
+type uconst = { uc_id: ID.t; uc_ty: ty }
+(** Uninterpreted constant. *)
 
-    - [relevant] must return a subset of [args] (possibly the same set).
-      The terms it returns will be activated and evaluated whenever possible.
-      Terms in [args \ relevant args] are considered for
-      congruence but not for evaluation.
-*)
-
-and ty_view =
+type ty_view =
   | Ty_int
   | Ty_real
   | Ty_uninterpreted of { id: ID.t; mutable finite: bool }
-  | Ty_data of { data: data }
+(* TODO: remove (lives in Data_ty now)
+   | Ty_data of { data: data }
+*)
 
 and data = {
   data_id: ID.t;