diff --git a/dev/sidekick/Sidekick_smt_solver/Theory/index.html b/dev/sidekick/Sidekick_smt_solver/Theory/index.html index d0f6d88f..3771a346 100644 --- a/dev/sidekick/Sidekick_smt_solver/Theory/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Theory/index.html @@ -2,7 +2,7 @@ Theory (sidekick.Sidekick_smt_solver.Theory)

Module Sidekick_smt_solver.Theory

Signatures for theory plugins

module type S = sig ... end

A theory

type t = (module S)

A theory that can be used for this particular solver.

type 'a p = (module S with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val name : t -> string

Name of the theory

val make : name:string -> create_and_setup:(id:Theory_id.t -> Solver_internal.t -> 'st) -> - ?push_level:('st -> unit) -> - ?pop_levels:('st -> int -> unit) -> + ?push_level:('st0 -> unit) -> + ?pop_levels:('st1 -> int -> unit) -> unit -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_lra/Intf/index.html b/dev/sidekick/Sidekick_th_lra/Intf/index.html index fc959ac1..9f75974a 100644 --- a/dev/sidekick/Sidekick_th_lra/Intf/index.html +++ b/dev/sidekick/Sidekick_th_lra/Intf/index.html @@ -1,2 +1,2 @@ -Intf (sidekick.Sidekick_th_lra.Intf)

Module Sidekick_th_lra.Intf

module SMT = Sidekick_smt_solver
module Proof = Sidekick_proof
module Predicate = Sidekick_simplex.Predicate
module Linear_expr = Sidekick_simplex.Linear_expr
module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf
module type INT = Sidekick_arith.INT
module type RATIONAL = Sidekick_arith.RATIONAL
module S_op = Sidekick_simplex.Op
type pred = Linear_expr_intf.bool_op =
  1. | Leq
  2. | Geq
  3. | Lt
  4. | Gt
  5. | Eq
  6. | Neq
type op = Linear_expr_intf.op =
  1. | Plus
  2. | Minus
type ('num, 'a) lra_view =
  1. | LRA_pred of pred * 'a * 'a
  2. | LRA_op of op * 'a * 'a
  3. | LRA_mult of 'num * 'a
  4. | LRA_const of 'num
  5. | LRA_other of 'a
val map_view : ('a -> 'b) -> ('c, 'a) lra_view -> ('c, 'b) lra_view
module type ARG = sig ... end
\ No newline at end of file +Intf (sidekick.Sidekick_th_lra.Intf)

Module Sidekick_th_lra.Intf

module SMT = Sidekick_smt_solver
module Proof = Sidekick_proof
module Predicate = Sidekick_simplex.Predicate
module Linear_expr = Sidekick_simplex.Linear_expr
module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf
module type INT = Sidekick_arith.INT
module type RATIONAL = Sidekick_arith.RATIONAL
module S_op = Sidekick_simplex.Op
type pred = Linear_expr_intf.bool_op =
  1. | Leq
  2. | Geq
  3. | Lt
  4. | Gt
  5. | Eq
  6. | Neq
type op = Linear_expr_intf.op =
  1. | Plus
  2. | Minus
type ('num, 'a) lra_view =
  1. | LRA_pred of pred * 'a * 'a
  2. | LRA_op of op * 'a * 'a
  3. | LRA_mult of 'num * 'a
  4. | LRA_const of 'num
  5. | LRA_other of 'a
val map_view : ('a -> 'b) -> ('c, 'd) lra_view -> ('e, 'f) lra_view
module type ARG = sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Int_id/Make/index.html b/dev/sidekick/Sidekick_util/Int_id/Make/index.html index 275ff70e..ba241d14 100644 --- a/dev/sidekick/Sidekick_util/Int_id/Make/index.html +++ b/dev/sidekick/Sidekick_util/Int_id/Make/index.html @@ -1,2 +1,2 @@ -Make (sidekick.Sidekick_util.Int_id.Make)

Module Int_id.Make

Generate a new type for integer identifiers

Parameters

Signature

type t = int
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : int CCHash.t
val pp : int CCFormat.printer
val to_int : 'a -> 'a
val of_int_unsafe : int -> t
\ No newline at end of file +Make (sidekick.Sidekick_util.Int_id.Make)

Module Int_id.Make

Generate a new type for integer identifiers

Parameters

Signature

type t = int
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : int CCHash.t
val pp : int CCFormat.printer
val to_int : 'a -> 'b
val of_int_unsafe : int -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/index.html b/dev/sidekick/Sidekick_util/index.html index 1574d0f0..dcc164c6 100644 --- a/dev/sidekick/Sidekick_util/index.html +++ b/dev/sidekick/Sidekick_util/index.html @@ -1,2 +1,2 @@ -Sidekick_util (sidekick.Sidekick_util)

Module Sidekick_util

module Fmt = CCFormat
module Util : sig ... end
module Vec : sig ... end

Vectors

module Veci : sig ... end

Vectors of int32 integers

module Vec_float : sig ... end

Vectors of floats

module Vec_sig : sig ... end
module Bitvec : sig ... end

Bitvector.

module Int_id : sig ... end

Integer-based identifiers.

module Int_tbl = Util.Int_tbl
module Int_set = Util.Int_set
module Int_map = Util.Int_map
module Event : sig ... end

Event pattern.

module Backtrack_stack : sig ... end
module Backtrackable_tbl : sig ... end
module Backtrackable_ref : sig ... end
module Log : sig ... end

Logging function, for debugging

module Error : sig ... end
module Bag : sig ... end
module Stat : sig ... end
module Hash : sig ... end
module Profile : sig ... end

Profiling probes.

module Chunk_stack : sig ... end

Manage a list of chunks.

module Ser_value : sig ... end

Serialization representation.

module Ser_decode : sig ... end

Decoders for Ser_value.

val let@ : ('a -> 'b) -> 'a -> 'b
\ No newline at end of file +Sidekick_util (sidekick.Sidekick_util)

Module Sidekick_util

module Fmt = CCFormat
module Util : sig ... end
module Vec : sig ... end

Vectors

module Veci : sig ... end

Vectors of int32 integers

module Vec_float : sig ... end

Vectors of floats

module Vec_sig : sig ... end
module Bitvec : sig ... end

Bitvector.

module Int_id : sig ... end

Integer-based identifiers.

module Int_tbl = Util.Int_tbl
module Int_set = Util.Int_set
module Int_map = Util.Int_map
module Event : sig ... end

Event pattern.

module Backtrack_stack : sig ... end
module Backtrackable_tbl : sig ... end
module Backtrackable_ref : sig ... end
module Log : sig ... end

Logging function, for debugging

module Error : sig ... end
module Bag : sig ... end
module Stat : sig ... end
module Hash : sig ... end
module Profile : sig ... end

Profiling probes.

module Chunk_stack : sig ... end

Manage a list of chunks.

module Ser_value : sig ... end

Serialization representation.

module Ser_decode : sig ... end

Decoders for Ser_value.

val let@ : ('a -> 'b) -> 'c -> 'd
\ No newline at end of file