Module Sidekick_base.Types_

include module type of struct include Sidekick_core end
module Fmt = Sidekick_core.Fmt

Re-exports from core-logic

module Const = Sidekick_core.Const
module Str_const = Sidekick_core.Str_const
module Term = Sidekick_core.Term

view

module Bool_view = Sidekick_core.Bool_view
module CC_view = Sidekick_core.CC_view
module Default_cc_view = Sidekick_core.Default_cc_view

Main modules

module Bvar = Sidekick_core.Bvar
module Lit = Sidekick_core.Lit
module Subst = Sidekick_core.Subst
module Var = Sidekick_core.Var
module Box = Sidekick_core.Box
module Gensym = Sidekick_core.Gensym
exception Resource_exhausted

Const decoders for traces

val const_decoders : (string * Sidekick_core_logic.Const.Ops.t * (Sidekick_core_logic__.Types_.term Sidekick_util.Ser_decode.t -> Sidekick_core_logic.Const.view Sidekick_util.Ser_decode.t)) list
type term = Term.t
type ty = Term.t
type value = Term.t
type uconst = {
  1. uc_id : ID.t;
  2. uc_ty : ty;
}

Uninterpreted constant.

type ty_view =
  1. | Ty_int
  2. | Ty_real
  3. | Ty_uninterpreted of {
    1. id : ID.t;
    2. mutable finite : bool;
    }
and data = {
  1. data_id : ID.t;
  2. data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
  3. data_as_ty : ty lazy_t;
}
and cstor = {
  1. cstor_id : ID.t;
  2. cstor_is_a : ID.t;
  3. mutable cstor_arity : int;
  4. cstor_args : select list lazy_t;
  5. cstor_ty_as_data : data;
  6. cstor_ty : ty lazy_t;
}
and select = {
  1. select_id : ID.t;
  2. select_cstor : cstor;
  3. select_ty : ty lazy_t;
  4. select_i : int;
}
type definition = ID.t * ty * term
type statement =
  1. | Stmt_set_logic of string
  2. | Stmt_set_option of string list
  3. | Stmt_set_info of string * string
  4. | Stmt_data of data list
  5. | Stmt_ty_decl of {
    1. name : ID.t;
    2. arity : int;
    3. ty_const : ty;
    }
    (*

    new atomic cstor

    *)
  6. | Stmt_decl of {
    1. name : ID.t;
    2. ty_args : ty list;
    3. ty_ret : ty;
    4. const : term;
    }
  7. | Stmt_define of definition list
  8. | Stmt_assert of term
  9. | Stmt_assert_clause of term list
  10. | Stmt_check_sat of (bool * term) list
  11. | Stmt_get_model
  12. | Stmt_get_value of term list
  13. | Stmt_exit