diff --git a/dev/sidekick-base/Sidekick_base/Config/Key/index.html b/dev/sidekick-base/Sidekick_base/Config/Key/index.html index 7f99c503..3976d0e7 100644 --- a/dev/sidekick-base/Sidekick_base/Config/Key/index.html +++ b/dev/sidekick-base/Sidekick_base/Config/Key/index.html @@ -1,2 +1,2 @@ -
Config.Keyval create : unit -> 'a tConfig.Keyval create : unit -> 'a tSidekick_base.ConfigConfiguration
Sidekick_base.ConfigConfiguration
Data_ty.Cstortype t = cstorinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerData_ty.Cstortype t = cstorinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerData_ty.Selecttype t = selectinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerData_ty.Selecttype t = selectinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerSidekick_base.Data_tytype select = Types_.select = {select_id : ID.t;select_cstor : Types_.cstor;select_ty : Types_.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 : Types_.data;cstor_ty : Types_.ty lazy_t;}type Sidekick_core.Const.view += | Data of Types_.data| Cstor of cstor| Select of select| Is_a of cstorinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printermodule Select : sig ... endmodule Cstor : sig ... endval data : Sidekick_core.Term.store -> t -> Sidekick_core.Term.tval cstor : Sidekick_core.Term.store -> cstor -> Sidekick_core.Term.tval select : Sidekick_core.Term.store -> select -> Sidekick_core.Term.tval is_a : Sidekick_core.Term.store -> cstor -> Sidekick_core.Term.tval as_data : Types_.ty -> Types_.data optionval as_select : Types_.term -> select optionval as_cstor : Types_.term -> cstor optionval as_is_a : Types_.term -> cstor optionSidekick_base.Data_tytype select = Types_.select = {select_id : ID.t;select_cstor : Types_.cstor;select_ty : Types_.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 : Types_.data;cstor_ty : Types_.ty lazy_t;}type Sidekick_core.Const.view += | Data of Types_.data| Cstor of cstor| Select of select| Is_a of cstorinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printermodule Select : sig ... endmodule Cstor : sig ... endval data : Sidekick_core.Term.store -> t -> Sidekick_core.Term.tval cstor : Sidekick_core.Term.store -> cstor -> Sidekick_core.Term.tval select : Sidekick_core.Term.store -> select -> Sidekick_core.Term.tval is_a : Sidekick_core.Term.store -> cstor -> Sidekick_core.Term.tval as_data : Types_.ty -> Types_.data optionval as_select : Types_.term -> select optionval as_cstor : Types_.term -> cstor optionval as_is_a : Types_.term -> cstor optionSidekick_base.FormFormulas (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.
type term = Sidekick_core.Term.ttype 'a view = 'a Sidekick_core.Bool_view.t = val bool : Sidekick_core.Term.store -> bool -> termval not_ : Sidekick_core.Term.store -> term -> termval and_ : Sidekick_core.Term.store -> term -> term -> termval or_ : Sidekick_core.Term.store -> term -> term -> termval eq : Sidekick_core.Term.store -> term -> term -> termval neq : Sidekick_core.Term.store -> term -> term -> termval imply : Sidekick_core.Term.store -> term -> term -> termval equiv : Sidekick_core.Term.store -> term -> term -> termval xor : Sidekick_core.Term.store -> term -> term -> termval ite : Sidekick_core.Term.store -> term -> term -> term -> termval distinct_l : Sidekick_core.Term.store -> term list -> termval const_decoders : Sidekick_core.Const.decodersval and_l : Sidekick_core.Term.store -> term list -> termval or_l : Sidekick_core.Term.store -> term list -> termval imply_l : Sidekick_core.Term.store -> term list -> term -> termval mk_of_view : Sidekick_core.Term.store -> term view -> termSidekick_base.FormFormulas (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.
type term = Sidekick_core.Term.ttype 'a view = 'a Sidekick_core.Bool_view.t = val bool : Sidekick_core.Term.store -> bool -> termval not_ : Sidekick_core.Term.store -> term -> termval and_ : Sidekick_core.Term.store -> term -> term -> termval or_ : Sidekick_core.Term.store -> term -> term -> termval eq : Sidekick_core.Term.store -> term -> term -> termval neq : Sidekick_core.Term.store -> term -> term -> termval imply : Sidekick_core.Term.store -> term -> term -> termval equiv : Sidekick_core.Term.store -> term -> term -> termval xor : Sidekick_core.Term.store -> term -> term -> termval ite : Sidekick_core.Term.store -> term -> term -> term -> termval distinct_l : Sidekick_core.Term.store -> term list -> termval const_decoders : Sidekick_core.Const.decodersval and_l : Sidekick_core.Term.store -> term list -> termval or_l : Sidekick_core.Term.store -> term list -> termval imply_l : Sidekick_core.Term.store -> term list -> term -> termval mk_of_view : Sidekick_core.Term.store -> term view -> termSidekick_base.IDUnique Identifiers
We use generative identifiers everywhere in Sidekick_base. Unlike strings, there are no risk of collision: during parsing, a new declaration or definition should create a fresh ID.t and associate it with the string name, and later references should look into some hashtable or map to get the ID corresponding to a string.
This allows us to handle definition shadowing or binder shadowing easily.
val make : string -> tmake s creates a new identifier with name s and some internal information. It is different than any other identifier created before or after, even with the same name.
val makef : ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 -> 'amakef "foo %d bar %b" 42 true is like make (Format.asprintf "foo %d bar %b" 42 true).
val id : t -> intUnique integer counter for this identifier.
val to_string : t -> stringPrint identifier.
val to_string_full : t -> stringPrinter name and unique counter for this ID.
val ser : t -> Sidekick_util.Ser_value.tval deser : t Sidekick_util.Ser_decode.tinclude Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.ORD with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerval pp_name : t CCFormat.printerval pp_full : t CCFormat.printerSidekick_base.IDUnique Identifiers
We use generative identifiers everywhere in Sidekick_base. Unlike strings, there are no risk of collision: during parsing, a new declaration or definition should create a fresh ID.t and associate it with the string name, and later references should look into some hashtable or map to get the ID corresponding to a string.
This allows us to handle definition shadowing or binder shadowing easily.
val make : string -> tmake s creates a new identifier with name s and some internal information. It is different than any other identifier created before or after, even with the same name.
val makef : ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 -> 'amakef "foo %d bar %b" 42 true is like make (Format.asprintf "foo %d bar %b" 42 true).
val id : t -> intUnique integer counter for this identifier.
val to_string : t -> stringPrint identifier.
val to_string_full : t -> stringPrinter name and unique counter for this ID.
val ser : t -> Sidekick_util.Ser_value.tval deser : t Sidekick_util.Ser_decode.tinclude Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.ORD with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerval pp_name : t CCFormat.printerval pp_full : t CCFormat.printerLRA_term.Opinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerLRA_term.Opinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerLRA_term.Predinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerLRA_term.Predinclude Sidekick_sigs.EQ_HASH_PRINT with type t := tinclude Sidekick_sigs.EQ with type t := tinclude Sidekick_sigs.HASH with type t := tval hash : t -> intinclude Sidekick_sigs.PRINT with type t := tval pp : t Sidekick_sigs.printerLRA_term.Viewtype ('num, 'a) lra_view = ('num, 'a) Sidekick_th_lra.lra_view = type 'a t = (Q.t, 'a) Sidekick_th_lra.lra_viewval iter : ('a -> unit) -> 'a t -> unitval pp : pp_t:'a Sidekick_core.Fmt.printer -> 'a t Sidekick_core.Fmt.printerval hash : sub_hash:('a -> int) -> 'a t -> intLRA_term.Viewtype ('num, 'a) lra_view = ('num, 'a) Sidekick_th_lra.lra_view = type 'a t = (Q.t, 'a) Sidekick_th_lra.lra_viewval iter : ('a -> unit) -> 'a t -> unitval pp : pp_t:'a Sidekick_core.Fmt.printer -> 'a t Sidekick_core.Fmt.printerval hash : sub_hash:('a -> int) -> 'a t -> intSidekick_base.LRA_termmodule Pred : sig ... endmodule Op : sig ... endval const_decoders : Sidekick_core.Const.decodersmodule View : sig ... endtype term = Sidekick_core.Term.ttype ty = Sidekick_core.Term.tval term_of_view : Sidekick_core.Term.store -> term View.t -> termval real : Sidekick_core.Term.store -> tyval has_ty_real : term -> boolval pred : Sidekick_core.Term.store -> Pred.t -> term -> term -> termval mult_by : Sidekick_core.Term.store -> Q.t -> term -> termval op : Sidekick_core.Term.store -> Op.t -> term -> term -> termval const : Sidekick_core.Term.store -> Q.t -> termval leq : Sidekick_core.Term.store -> term -> term -> termval lt : Sidekick_core.Term.store -> term -> term -> termval geq : Sidekick_core.Term.store -> term -> term -> termval gt : Sidekick_core.Term.store -> term -> term -> termval eq : Sidekick_core.Term.store -> term -> term -> termval neq : Sidekick_core.Term.store -> term -> term -> termval plus : Sidekick_core.Term.store -> term -> term -> termval minus : Sidekick_core.Term.store -> term -> term -> termSidekick_base.LRA_termmodule Pred : sig ... endmodule Op : sig ... endval const_decoders : Sidekick_core.Const.decodersmodule View : sig ... endtype term = Sidekick_core.Term.ttype ty = Sidekick_core.Term.tval term_of_view : Sidekick_core.Term.store -> term View.t -> termval real : Sidekick_core.Term.store -> tyval has_ty_real : term -> boolval pred : Sidekick_core.Term.store -> Pred.t -> term -> term -> termval mult_by : Sidekick_core.Term.store -> Q.t -> term -> termval op : Sidekick_core.Term.store -> Op.t -> term -> term -> termval const : Sidekick_core.Term.store -> Q.t -> termval leq : Sidekick_core.Term.store -> term -> term -> termval lt : Sidekick_core.Term.store -> term -> term -> termval geq : Sidekick_core.Term.store -> term -> term -> termval gt : Sidekick_core.Term.store -> term -> term -> termval eq : Sidekick_core.Term.store -> term -> term -> termval neq : Sidekick_core.Term.store -> term -> term -> termval plus : Sidekick_core.Term.store -> term -> term -> termval minus : Sidekick_core.Term.store -> term -> term -> termSidekick_base.Solverinclude module type of struct include Sidekick_smt_solver.Solver endmodule Check_res = Sidekick_smt_solver.Solver.Check_resmodule Unknown = Sidekick_smt_solver.Solver.Unknowntype t = Sidekick_smt_solver.Solver.tThe solver's state.
val registry : t -> Sidekick_smt_solver.Registry.tA solver contains a registry so that theories can share data
type theory = Sidekick_smt_solver.Theory.tval mk_theory :
+Solver (sidekick-base.Sidekick_base.Solver) Module Sidekick_base.Solver
include module type of struct include Sidekick_smt_solver.Solver end
module Check_res = Sidekick_smt_solver.Solver.Check_resmodule Unknown = Sidekick_smt_solver.Solver.Unknowntype t = Sidekick_smt_solver.Solver.tThe solver's state.
val registry : t -> Sidekick_smt_solver.Registry.tA solver contains a registry so that theories can share data
type theory = Sidekick_smt_solver.Theory.tval mk_theory :
name:string ->
create_and_setup:
(id:Sidekick_smt_solver.Theory_id.t ->
diff --git a/dev/sidekick-base/Sidekick_base/Statement/index.html b/dev/sidekick-base/Sidekick_base/Statement/index.html
index 8b26b56f..1793e54e 100644
--- a/dev/sidekick-base/Sidekick_base/Statement/index.html
+++ b/dev/sidekick-base/Sidekick_base/Statement/index.html
@@ -1,2 +1,2 @@
-Statement (sidekick-base.Sidekick_base.Statement) Module Sidekick_base.Statement
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.
type t = Types_.statement = | Stmt_set_logic of string| Stmt_set_option of string list| Stmt_set_info of string * string| Stmt_data of Types_.data list| Stmt_ty_decl of {}(*new atomic cstor
*)| Stmt_decl of {name : ID.t;ty_args : Types_.ty list;ty_ret : Types_.ty;const : Types_.term;
}| Stmt_define of Types_.definition list| Stmt_assert of Types_.term| Stmt_assert_clause of Types_.term list| Stmt_check_sat of (bool * Types_.term) list| Stmt_get_model| Stmt_get_value of Types_.term list| Stmt_exit
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
+Statement (sidekick-base.Sidekick_base.Statement) Module Sidekick_base.Statement
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.
type t = Types_.statement = | Stmt_set_logic of string| Stmt_set_option of string list| Stmt_set_info of string * string| Stmt_data of Types_.data list| Stmt_ty_decl of {}(*new atomic cstor
*)| Stmt_decl of {name : ID.t;ty_args : Types_.ty list;ty_ret : Types_.ty;const : Types_.term;
}| Stmt_define of Types_.definition list| Stmt_assert of Types_.term| Stmt_assert_clause of Types_.term list| Stmt_check_sat of (bool * Types_.term) list| Stmt_get_model| Stmt_get_value of Types_.term list| Stmt_exit
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
diff --git a/dev/sidekick-base/Sidekick_base/Term/index.html b/dev/sidekick-base/Sidekick_base/Term/index.html
index 2a9f6e68..8b422523 100644
--- a/dev/sidekick-base/Sidekick_base/Term/index.html
+++ b/dev/sidekick-base/Sidekick_base/Term/index.html
@@ -1,5 +1,5 @@
-Term (sidekick-base.Sidekick_base.Term) Module Sidekick_base.Term
include module type of struct include Sidekick_core.Term end
include module type of struct include Sidekick_core_logic.Term end
type var = Sidekick_core_logic.Var.ttype bvar = Sidekick_core_logic.Bvar.ttype store = Sidekick_core_logic.Term.storeThe store for terms.
The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).
include Sidekick_sigs.EQ_ORD_HASH with type t := t
include Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intval pp_debug : t Sidekick_util.Fmt.printerval pp_debug_with_ids : t Sidekick_util.Fmt.printerContainers
include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t
module Set = Sidekick_core.Term.Setmodule Map = Sidekick_core.Term.Mapmodule Tbl = Sidekick_core.Term.Tblinclude Sidekick_sigs.WITH_WEAK with type t := t
module Weak_set = Sidekick_core.Term.Weak_setmodule Weak_map = Sidekick_core.Term.Weak_mapUtils
val is_app : t -> boolval is_const : t -> boolval is_pi : t -> booliter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
+Term (sidekick-base.Sidekick_base.Term) Module Sidekick_base.Term
include module type of struct include Sidekick_core.Term end
include module type of struct include Sidekick_core_logic.Term end
type var = Sidekick_core_logic.Var.ttype bvar = Sidekick_core_logic.Bvar.ttype store = Sidekick_core_logic.Term.storeThe store for terms.
The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).
include Sidekick_sigs.EQ_ORD_HASH with type t := t
include Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intval pp_debug : t Sidekick_util.Fmt.printerval pp_debug_with_ids : t Sidekick_util.Fmt.printerContainers
include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t
module Set = Sidekick_core.Term.Setmodule Map = Sidekick_core.Term.Mapmodule Tbl = Sidekick_core.Term.Tblinclude Sidekick_sigs.WITH_WEAK with type t := t
module Weak_set = Sidekick_core.Term.Weak_setmodule Weak_map = Sidekick_core.Term.Weak_mapUtils
val is_app : t -> boolval is_const : t -> boolval is_pi : t -> booliter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
let y = f x x in
let z = g y x in
z = z
the DAG has the following nodes:
n1: 2
diff --git a/dev/sidekick-base/Sidekick_base/Th_bool/index.html b/dev/sidekick-base/Sidekick_base/Th_bool/index.html
index da64fac8..c62d450b 100644
--- a/dev/sidekick-base/Sidekick_base/Th_bool/index.html
+++ b/dev/sidekick-base/Sidekick_base/Th_bool/index.html
@@ -1,2 +1,2 @@
-Th_bool (sidekick-base.Sidekick_base.Th_bool) Module Sidekick_base.Th_bool
Reducing boolean formulas to clauses
val k_config : [ `Dyn | `Static ] Config.Key.tval theory_static : Solver.theoryval theory_dyn : Solver.theoryval theory : Config.t -> Solver.theory
+Th_bool (sidekick-base.Sidekick_base.Th_bool) Module Sidekick_base.Th_bool
Reducing boolean formulas to clauses
val k_config : [ `Dyn | `Static ] Config.Key.tval theory_static : Solver.theoryval theory_dyn : Solver.theoryval theory : Config.t -> Solver.theory
diff --git a/dev/sidekick-base/Sidekick_base/Th_data/index.html b/dev/sidekick-base/Sidekick_base/Th_data/index.html
index 95a30dc1..1e4b6ba9 100644
--- a/dev/sidekick-base/Sidekick_base/Th_data/index.html
+++ b/dev/sidekick-base/Sidekick_base/Th_data/index.html
@@ -1,2 +1,2 @@
-Th_data (sidekick-base.Sidekick_base.Th_data) Module Sidekick_base.Th_data
Theory of datatypes
val arg : (module Sidekick_th_data.ARG)val theory : Sidekick_th_data.SMT.theory
+Th_data (sidekick-base.Sidekick_base.Th_data) Module Sidekick_base.Th_data
Theory of datatypes
val arg : (module Sidekick_th_data.ARG)val theory : Sidekick_th_data.SMT.theory
diff --git a/dev/sidekick-base/Sidekick_base/Th_lra/index.html b/dev/sidekick-base/Sidekick_base/Th_lra/index.html
index 6209c0bc..668e2132 100644
--- a/dev/sidekick-base/Sidekick_base/Th_lra/index.html
+++ b/dev/sidekick-base/Sidekick_base/Th_lra/index.html
@@ -1,2 +1,2 @@
-Th_lra (sidekick-base.Sidekick_base.Th_lra) Module Sidekick_base.Th_lra
Theory of Linear Rational Arithmetic
module T = Sidekick_core.Termmodule Q = Sidekick_zarith.Rationalval mk_eq : Sidekick_core.Term.store -> Form.term -> Form.term -> Form.termval mk_bool : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval theory : Solver.theory
+Th_lra (sidekick-base.Sidekick_base.Th_lra) Module Sidekick_base.Th_lra
Theory of Linear Rational Arithmetic
module T = Sidekick_core.Termmodule Q = Sidekick_zarith.Rationalval mk_eq : Sidekick_core.Term.store -> Form.term -> Form.term -> Form.termval mk_bool : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval theory : Solver.theory
diff --git a/dev/sidekick-base/Sidekick_base/Th_ty_unin/index.html b/dev/sidekick-base/Sidekick_base/Th_ty_unin/index.html
index ade219c4..15bda96b 100644
--- a/dev/sidekick-base/Sidekick_base/Th_ty_unin/index.html
+++ b/dev/sidekick-base/Sidekick_base/Th_ty_unin/index.html
@@ -1,2 +1,2 @@
-Th_ty_unin (sidekick-base.Sidekick_base.Th_ty_unin) Module Sidekick_base.Th_ty_unin
val theory : Solver.theory
+Th_ty_unin (sidekick-base.Sidekick_base.Th_ty_unin) Module Sidekick_base.Th_ty_unin
val theory : Solver.theory
diff --git a/dev/sidekick-base/Sidekick_base/Ty/index.html b/dev/sidekick-base/Sidekick_base/Ty/index.html
index 03d76698..3dcc76d2 100644
--- a/dev/sidekick-base/Sidekick_base/Ty/index.html
+++ b/dev/sidekick-base/Sidekick_base/Ty/index.html
@@ -1,5 +1,5 @@
-Ty (sidekick-base.Sidekick_base.Ty) Module Sidekick_base.Ty
include module type of struct include Sidekick_core.Term end
include module type of struct include Sidekick_core_logic.Term end
type var = Sidekick_core_logic.Var.ttype bvar = Sidekick_core_logic.Bvar.ttype store = Sidekick_core_logic.Term.storeThe store for terms.
The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).
View.
A view is the shape of the root node of a term.
include Sidekick_sigs.EQ_ORD_HASH
+Ty (sidekick-base.Sidekick_base.Ty) Module Sidekick_base.Ty
include module type of struct include Sidekick_core.Term end
include module type of struct include Sidekick_core_logic.Term end
type var = Sidekick_core_logic.Var.ttype bvar = Sidekick_core_logic.Bvar.ttype store = Sidekick_core_logic.Term.storeThe store for terms.
The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).
View.
A view is the shape of the root node of a term.
include Sidekick_sigs.EQ_ORD_HASH
with type t := Sidekick_core_logic__.Types_.term
include Sidekick_sigs.EQ with type t := Sidekick_core_logic__.Types_.term
include Sidekick_sigs.ORD with type t := Sidekick_core_logic__.Types_.term
include Sidekick_sigs.HASH with type t := Sidekick_core_logic__.Types_.term
Containers
include Sidekick_sigs.WITH_SET_MAP_TBL
with type t := Sidekick_core_logic__.Types_.term
module Set = Sidekick_core.Term.Setmodule Map = Sidekick_core.Term.Mapmodule Tbl = Sidekick_core.Term.Tblinclude Sidekick_sigs.WITH_WEAK
diff --git a/dev/sidekick-base/Sidekick_base/Types_/index.html b/dev/sidekick-base/Sidekick_base/Types_/index.html
index 8ebe3580..854fd276 100644
--- a/dev/sidekick-base/Sidekick_base/Types_/index.html
+++ b/dev/sidekick-base/Sidekick_base/Types_/index.html
@@ -1,5 +1,5 @@
-Types_ (sidekick-base.Sidekick_base.Types_) Module Sidekick_base.Types_
include module type of struct include Sidekick_core end
module Fmt = Sidekick_core.FmtRe-exports from core-logic
module Const = Sidekick_core.Constmodule Str_const = Sidekick_core.Str_constmodule Term = Sidekick_core.Termview
module Bool_view = Sidekick_core.Bool_viewmodule CC_view = Sidekick_core.CC_viewmodule Default_cc_view = Sidekick_core.Default_cc_viewMain modules
module Bvar = Sidekick_core.Bvarmodule Lit = Sidekick_core.Litmodule Subst = Sidekick_core.Substmodule Var = Sidekick_core.Varmodule Box = Sidekick_core.Boxmodule Gensym = Sidekick_core.GensymConst decoders for traces
val const_decoders :
+Types_ (sidekick-base.Sidekick_base.Types_) Module Sidekick_base.Types_
include module type of struct include Sidekick_core end
module Fmt = Sidekick_core.FmtRe-exports from core-logic
module Const = Sidekick_core.Constmodule Str_const = Sidekick_core.Str_constmodule Term = Sidekick_core.Termview
module Bool_view = Sidekick_core.Bool_viewmodule CC_view = Sidekick_core.CC_viewmodule Default_cc_view = Sidekick_core.Default_cc_viewMain modules
module Bvar = Sidekick_core.Bvarmodule Lit = Sidekick_core.Litmodule Subst = Sidekick_core.Substmodule Var = Sidekick_core.Varmodule Box = Sidekick_core.Boxmodule Gensym = Sidekick_core.GensymConst decoders for traces
val const_decoders :
(string
* Sidekick_core_logic.Const.Ops.t
* (Sidekick_core_logic__.Types_.term Sidekick_util.Ser_decode.t ->
diff --git a/dev/sidekick-base/Sidekick_base/Uconst/index.html b/dev/sidekick-base/Sidekick_base/Uconst/index.html
index af7e1038..71e58f11 100644
--- a/dev/sidekick-base/Sidekick_base/Uconst/index.html
+++ b/dev/sidekick-base/Sidekick_base/Uconst/index.html
@@ -1,5 +1,5 @@
-Uconst (sidekick-base.Sidekick_base.Uconst) Module Sidekick_base.Uconst
Uninterpreted constants
type ty = Sidekick_core.Term.tinclude Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval const_decoders : Sidekick_core.Const.decodersval uconst : Sidekick_core.Term.store -> t -> Sidekick_core.Term.tval uconst_of_id :
+Uconst (sidekick-base.Sidekick_base.Uconst) Module Sidekick_base.Uconst
Uninterpreted constants
type ty = Sidekick_core.Term.tinclude Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval const_decoders : Sidekick_core.Const.decodersval uconst : Sidekick_core.Term.store -> t -> Sidekick_core.Term.tval uconst_of_id :
Sidekick_core.Term.store ->
ID.t ->
ty ->
diff --git a/dev/sidekick-base/Sidekick_base/index.html b/dev/sidekick-base/Sidekick_base/index.html
index 30be6915..abd90bdd 100644
--- a/dev/sidekick-base/Sidekick_base/index.html
+++ b/dev/sidekick-base/Sidekick_base/index.html
@@ -1,5 +1,5 @@
-Sidekick_base (sidekick-base.Sidekick_base) Module Sidekick_base
Sidekick base
This library is a starting point for writing concrete implementations of SMT solvers with Sidekick.
It provides a representation of terms, boolean formulas, linear arithmetic expressions, datatypes for the functors in Sidekick.
In addition, it has a notion of Statement. Statements are instructions for the SMT solver to do something, such as: define a new constant, declare a new constant, assert a formula as being true, set an option, check satisfiability of the set of statements added so far, 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 Types_ : sig ... endmodule Term : sig ... endmodule Const = Sidekick_core.Constmodule Ty : sig ... endmodule ID : sig ... endUnique Identifiers
module Form : sig ... endFormulas (boolean terms).
module Data_ty : sig ... endmodule Cstor = Data_ty.Cstormodule Select = Data_ty.Selectmodule Statement : sig ... endStatements.
module Solver : sig ... endmodule Uconst : sig ... endUninterpreted constants
module Config : sig ... endConfiguration
module LRA_term : sig ... endmodule Th_data : sig ... endTheory of datatypes
module Th_bool : sig ... endReducing boolean formulas to clauses
module Th_lra : sig ... endTheory of Linear Rational Arithmetic
module Th_ty_unin : sig ... endval k_th_bool_config : [ `Dyn | `Static ] Config.Key.tval th_bool : Config.t -> Solver.theoryval th_bool_dyn : Solver.theoryval th_bool_static : Solver.theoryval th_data : Solver.theoryval th_lra : Solver.theoryval th_ty_unin : Solver.theoryval const_decoders :
+Sidekick_base (sidekick-base.Sidekick_base) Module Sidekick_base
Sidekick base
This library is a starting point for writing concrete implementations of SMT solvers with Sidekick.
It provides a representation of terms, boolean formulas, linear arithmetic expressions, datatypes for the functors in Sidekick.
In addition, it has a notion of Statement. Statements are instructions for the SMT solver to do something, such as: define a new constant, declare a new constant, assert a formula as being true, set an option, check satisfiability of the set of statements added so far, 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 Types_ : sig ... endmodule Term : sig ... endmodule Const = Sidekick_core.Constmodule Ty : sig ... endmodule ID : sig ... endUnique Identifiers
module Form : sig ... endFormulas (boolean terms).
module Data_ty : sig ... endmodule Cstor = Data_ty.Cstormodule Select = Data_ty.Selectmodule Statement : sig ... endStatements.
module Solver : sig ... endmodule Uconst : sig ... endUninterpreted constants
module Config : sig ... endConfiguration
module LRA_term : sig ... endmodule Th_data : sig ... endTheory of datatypes
module Th_bool : sig ... endReducing boolean formulas to clauses
module Th_lra : sig ... endTheory of Linear Rational Arithmetic
module Th_ty_unin : sig ... endval k_th_bool_config : [ `Dyn | `Static ] Config.Key.tval th_bool : Config.t -> Solver.theoryval th_bool_dyn : Solver.theoryval th_bool_static : Solver.theoryval th_data : Solver.theoryval th_lra : Solver.theoryval th_ty_unin : Solver.theoryval const_decoders :
(string
* Sidekick_core.Const.Ops.t
* (Sidekick_core_logic__.Types_.term Sidekick_util.Ser_decode.t ->
diff --git a/dev/sidekick-base/Sidekick_smtlib/Check_cc/index.html b/dev/sidekick-base/Sidekick_smtlib/Check_cc/index.html
index eefa87ee..8afe0beb 100644
--- a/dev/sidekick-base/Sidekick_smtlib/Check_cc/index.html
+++ b/dev/sidekick-base/Sidekick_smtlib/Check_cc/index.html
@@ -1,2 +1,2 @@
-Check_cc (sidekick-base.Sidekick_smtlib.Check_cc) Module Sidekick_smtlib.Check_cc
val theory : Solver.cdcl_theorytheory that check validity of EUF conflicts, on the fly
+Check_cc (sidekick-base.Sidekick_smtlib.Check_cc) Module Sidekick_smtlib.Check_cc
val theory : Solver.cdcl_theorytheory that check validity of EUF conflicts, on the fly
diff --git a/dev/sidekick-base/Sidekick_smtlib/Driver/index.html b/dev/sidekick-base/Sidekick_smtlib/Driver/index.html
index 10a4e6ee..90bf19f8 100644
--- a/dev/sidekick-base/Sidekick_smtlib/Driver/index.html
+++ b/dev/sidekick-base/Sidekick_smtlib/Driver/index.html
@@ -1,5 +1,5 @@
-Driver (sidekick-base.Sidekick_smtlib.Driver) Module Sidekick_smtlib.Driver
Driver.
The driver is responsible for processing statements from a SMTLIB file, and interacting with the solver based on the statement (asserting formulas, calling "solve", etc.)
module Asolver = Sidekick_abstract_solver.Asolverval th_bool_dyn : Sidekick_base.Solver.theoryval th_bool_static : Sidekick_base.Solver.theoryval th_bool : Sidekick_base.Config.t -> Sidekick_base.Solver.theoryval th_data : Sidekick_base.Solver.theoryval th_lra : Sidekick_base.Solver.theoryval th_ty_unin : Sidekick_base.Solver.theoryval create :
+Driver (sidekick-base.Sidekick_smtlib.Driver) Module Sidekick_smtlib.Driver
Driver.
The driver is responsible for processing statements from a SMTLIB file, and interacting with the solver based on the statement (asserting formulas, calling "solve", etc.)
module Asolver = Sidekick_abstract_solver.Asolverval th_bool_dyn : Sidekick_base.Solver.theoryval th_bool_static : Sidekick_base.Solver.theoryval th_bool : Sidekick_base.Config.t -> Sidekick_base.Solver.theoryval th_data : Sidekick_base.Solver.theoryval th_lra : Sidekick_base.Solver.theoryval th_ty_unin : Sidekick_base.Solver.theoryval create :
?pp_cnf:bool ->
?proof_file:string ->
?pp_model:bool ->
diff --git a/dev/sidekick-base/Sidekick_smtlib/Model/index.html b/dev/sidekick-base/Sidekick_smtlib/Model/index.html
index 20954607..f93fd81b 100644
--- a/dev/sidekick-base/Sidekick_smtlib/Model/index.html
+++ b/dev/sidekick-base/Sidekick_smtlib/Model/index.html
@@ -1,2 +1,2 @@
-Model (sidekick-base.Sidekick_smtlib.Model) Module Sidekick_smtlib.Model
Models
A model can be produced when the solver is found to be in a satisfiable state after a call to solve.
type value = Sidekick_core.Term.ttype fun_ = Sidekick_core.Term.tval empty : tval is_empty : t -> boolval eval : Sidekick_core.Term.t -> t -> value optioninclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
+Model (sidekick-base.Sidekick_smtlib.Model) Module Sidekick_smtlib.Model
Models
A model can be produced when the solver is found to be in a satisfiable state after a call to solve.
type value = Sidekick_core.Term.ttype fun_ = Sidekick_core.Term.tval empty : tval is_empty : t -> boolval eval : Sidekick_core.Term.t -> t -> value optioninclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
diff --git a/dev/sidekick-base/Sidekick_smtlib/Solver/index.html b/dev/sidekick-base/Sidekick_smtlib/Solver/index.html
index 92989135..2aec5727 100644
--- a/dev/sidekick-base/Sidekick_smtlib/Solver/index.html
+++ b/dev/sidekick-base/Sidekick_smtlib/Solver/index.html
@@ -1,2 +1,2 @@
-Solver (sidekick-base.Sidekick_smtlib.Solver) Module Sidekick_smtlib.Solver
module Asolver = Sidekick_abstract_solver.Asolvermodule Smt_solver = Sidekick_smt_solvertype t = Asolver.ttype cdcl_theory = Smt_solver.theory
+Solver (sidekick-base.Sidekick_smtlib.Solver) Module Sidekick_smtlib.Solver
module Asolver = Sidekick_abstract_solver.Asolvermodule Smt_solver = Sidekick_smt_solvertype t = Asolver.ttype cdcl_theory = Smt_solver.theory
diff --git a/dev/sidekick-base/Sidekick_smtlib/index.html b/dev/sidekick-base/Sidekick_smtlib/index.html
index 4dedd8c9..c57e3ef5 100644
--- a/dev/sidekick-base/Sidekick_smtlib/index.html
+++ b/dev/sidekick-base/Sidekick_smtlib/index.html
@@ -1,2 +1,2 @@
-Sidekick_smtlib (sidekick-base.Sidekick_smtlib) Module Sidekick_smtlib
SMTLib-2.6 Driver
This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems.
module Term = Sidekick_base.Termmodule Stmt = Sidekick_base.Statementmodule Driver : sig ... endDriver.
module Solver : sig ... endmodule Check_cc : sig ... endmodule Model : sig ... endModels
val parse : Term.store -> string -> Stmt.t list or_errorval parse_stdin : Term.store -> Stmt.t list or_error
+Sidekick_smtlib (sidekick-base.Sidekick_smtlib) Module Sidekick_smtlib
SMTLib-2.6 Driver
This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems.
module Term = Sidekick_base.Termmodule Stmt = Sidekick_base.Statementmodule Driver : sig ... endDriver.
module Solver : sig ... endmodule Check_cc : sig ... endmodule Model : sig ... endModels
val parse : Term.store -> string -> Stmt.t list or_errorval parse_stdin : Term.store -> Stmt.t list or_error
diff --git a/dev/sidekick-base/index.html b/dev/sidekick-base/index.html
index 9e25a301..d0ca19f0 100644
--- a/dev/sidekick-base/index.html
+++ b/dev/sidekick-base/index.html
@@ -1,2 +1,2 @@
-index (sidekick-base.index) sidekick-base index
Library sidekick-base
The entry point of this library is the module: Sidekick_base.
Library sidekick-base.smtlib
The entry point of this library is the module: Sidekick_smtlib.
+index (sidekick-base.index) sidekick-base index
Library sidekick-base
The entry point of this library is the module: Sidekick_base.
Library sidekick-base.smtlib
The entry point of this library is the module: Sidekick_smtlib.
diff --git a/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_lexer/index.html b/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_lexer/index.html
index 5744af7d..5e4dcdc8 100644
--- a/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_lexer/index.html
+++ b/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_lexer/index.html
@@ -1,2 +1,2 @@
-Dimacs_lexer (sidekick-bin.Sidekick_bin_lib.Dimacs_lexer) Module Sidekick_bin_lib.Dimacs_lexer
val token : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_token_rec : Stdlib.Lexing.lexbuf -> int -> tokenval comment : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_comment_rec : Stdlib.Lexing.lexbuf -> int -> token
+Dimacs_lexer (sidekick-bin.Sidekick_bin_lib.Dimacs_lexer) Module Sidekick_bin_lib.Dimacs_lexer
val token : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_token_rec : Stdlib.Lexing.lexbuf -> int -> tokenval comment : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_comment_rec : Stdlib.Lexing.lexbuf -> int -> token
diff --git a/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_parser/index.html b/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_parser/index.html
index a7e482ef..f55b2f92 100644
--- a/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_parser/index.html
+++ b/dev/sidekick-bin/Sidekick_bin_lib/Dimacs_parser/index.html
@@ -1,2 +1,2 @@
-Dimacs_parser (sidekick-bin.Sidekick_bin_lib.Dimacs_parser) Module Sidekick_bin_lib.Dimacs_parser
DIMACS parser
val create : Stdlib.in_channel -> tval parse_header : t -> int * intval next_clause : t -> int list optionval iter : t -> int list Iter.t
+Dimacs_parser (sidekick-bin.Sidekick_bin_lib.Dimacs_parser) Module Sidekick_bin_lib.Dimacs_parser
DIMACS parser
val create : Stdlib.in_channel -> tval parse_header : t -> int * intval next_clause : t -> int list optionval iter : t -> int list Iter.t
diff --git a/dev/sidekick-bin/Sidekick_bin_lib/Drup_lexer/index.html b/dev/sidekick-bin/Sidekick_bin_lib/Drup_lexer/index.html
index 32645d93..9cb459d3 100644
--- a/dev/sidekick-bin/Sidekick_bin_lib/Drup_lexer/index.html
+++ b/dev/sidekick-bin/Sidekick_bin_lib/Drup_lexer/index.html
@@ -1,2 +1,2 @@
-Drup_lexer (sidekick-bin.Sidekick_bin_lib.Drup_lexer) Module Sidekick_bin_lib.Drup_lexer
val token : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_token_rec : Stdlib.Lexing.lexbuf -> int -> tokenval comment : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_comment_rec : Stdlib.Lexing.lexbuf -> int -> token
+Drup_lexer (sidekick-bin.Sidekick_bin_lib.Drup_lexer) Module Sidekick_bin_lib.Drup_lexer
val token : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_token_rec : Stdlib.Lexing.lexbuf -> int -> tokenval comment : Stdlib.Lexing.lexbuf -> tokenval __ocaml_lex_comment_rec : Stdlib.Lexing.lexbuf -> int -> token
diff --git a/dev/sidekick-bin/Sidekick_bin_lib/Drup_parser/index.html b/dev/sidekick-bin/Sidekick_bin_lib/Drup_parser/index.html
index 47312d8e..6efd6423 100644
--- a/dev/sidekick-bin/Sidekick_bin_lib/Drup_parser/index.html
+++ b/dev/sidekick-bin/Sidekick_bin_lib/Drup_parser/index.html
@@ -1,2 +1,2 @@
-Drup_parser (sidekick-bin.Sidekick_bin_lib.Drup_parser) Module Sidekick_bin_lib.Drup_parser
+Drup_parser (sidekick-bin.Sidekick_bin_lib.Drup_parser) Module Sidekick_bin_lib.Drup_parser
diff --git a/dev/sidekick-bin/Sidekick_bin_lib/Trace_setup/index.html b/dev/sidekick-bin/Sidekick_bin_lib/Trace_setup/index.html
index 8af0f865..5970dd4a 100644
--- a/dev/sidekick-bin/Sidekick_bin_lib/Trace_setup/index.html
+++ b/dev/sidekick-bin/Sidekick_bin_lib/Trace_setup/index.html
@@ -1,2 +1,2 @@
-Trace_setup (sidekick-bin.Sidekick_bin_lib.Trace_setup) Module Sidekick_bin_lib.Trace_setup
+Trace_setup (sidekick-bin.Sidekick_bin_lib.Trace_setup) Module Sidekick_bin_lib.Trace_setup
diff --git a/dev/sidekick-bin/Sidekick_bin_lib/index.html b/dev/sidekick-bin/Sidekick_bin_lib/index.html
index c9ca5de8..fa005dab 100644
--- a/dev/sidekick-bin/Sidekick_bin_lib/index.html
+++ b/dev/sidekick-bin/Sidekick_bin_lib/index.html
@@ -1,2 +1,2 @@
-Sidekick_bin_lib (sidekick-bin.Sidekick_bin_lib) Module Sidekick_bin_lib
Library for the Sidekick executables
module Dimacs_lexer : sig ... endmodule Dimacs_parser : sig ... endmodule Drup_lexer : sig ... endmodule Drup_parser : sig ... endmodule Trace_setup : sig ... end
+Sidekick_bin_lib (sidekick-bin.Sidekick_bin_lib) Module Sidekick_bin_lib
Library for the Sidekick executables
module Dimacs_lexer : sig ... endmodule Dimacs_parser : sig ... endmodule Drup_lexer : sig ... endmodule Drup_parser : sig ... endmodule Trace_setup : sig ... end
diff --git a/dev/sidekick-bin/index.html b/dev/sidekick-bin/index.html
index b0a5b974..d8c8e18f 100644
--- a/dev/sidekick-bin/index.html
+++ b/dev/sidekick-bin/index.html
@@ -1,2 +1,2 @@
-index (sidekick-bin.index) sidekick-bin index
Library sidekick-bin.lib
The entry point of this library is the module: Sidekick_bin_lib.
+index (sidekick-bin.index) sidekick-bin index
Library sidekick-bin.lib
The entry point of this library is the module: Sidekick_bin_lib.
diff --git a/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html
index ec635029..c2f5ac43 100644
--- a/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html
+++ b/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html
@@ -1,5 +1,5 @@
-t (sidekick.Sidekick_abstract_solver.Asolver.t) Class type Asolver.t
method assert_term : Sidekick_core.Term.t -> unitHelper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.
This uses Proof_sat.sat_input_clause to justify the assertion.
method assert_clause : Sidekick_core.Lit.t array -> Proof.Pterm.delayed -> unitadd_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.
method assert_clause_l : Sidekick_core.Lit.t list ->
+t (sidekick.Sidekick_abstract_solver.Asolver.t) Class type Asolver.t
method assert_term : Sidekick_core.Term.t -> unitHelper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.
This uses Proof_sat.sat_input_clause to justify the assertion.
method assert_clause : Sidekick_core.Lit.t array -> Proof.Pterm.delayed -> unitadd_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.
method assert_clause_l : Sidekick_core.Lit.t list ->
Proof.Pterm.delayed ->
unitAdd a clause to the solver, given as a list.
method add_ty : ty:Sidekick_core.Term.t -> unitAdd a new sort/atomic type.
method lit_of_term : ?sign:bool -> Sidekick_core.Term.t -> Sidekick_core.Lit.tConvert a term into a simplified literal.
method tst : Sidekick_core.Term.storemethod solve : ?on_exit:(unit -> unit) list ->
?on_progress:(unit -> unit) ->
diff --git a/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html
index 268f2273..3dc81b96 100644
--- a/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html
+++ b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html
@@ -1,5 +1,5 @@
-Asolver (sidekick.Sidekick_abstract_solver.Asolver) Module Sidekick_abstract_solver.Asolver
Abstract interface for a solver
module Unknown = Unknownmodule Check_res = Check_resmodule Proof = Sidekick_proofclass type t = object ... endval tst : t -> Sidekick_core.Term.storeval assert_term : t -> Sidekick_core.Term.t -> unitval assert_clause :
+Asolver (sidekick.Sidekick_abstract_solver.Asolver) Module Sidekick_abstract_solver.Asolver
Abstract interface for a solver
module Unknown = Unknownmodule Check_res = Check_resmodule Proof = Sidekick_proofclass type t = object ... endval tst : t -> Sidekick_core.Term.storeval assert_term : t -> Sidekick_core.Term.t -> unitval assert_clause :
t ->
Sidekick_core.Lit.t array ->
Proof.Pterm.delayed ->
diff --git a/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html b/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html
index ca1e4f38..bc360796 100644
--- a/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html
+++ b/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html
@@ -1,2 +1,2 @@
-Check_res (sidekick.Sidekick_abstract_solver.Check_res) Module Sidekick_abstract_solver.Check_res
Result of solving for the current set of clauses
type value = Sidekick_core.Term.ttype sat_result = {get_value : Sidekick_core.Term.t -> value option;(*Value for this term
*)iter_classes : (Sidekick_core.Term.t Iter.t * value) Iter.t;(*All equivalence classes in the congruence closure
*)eval_lit : Sidekick_core.Lit.t -> bool option;(*Evaluate literal
*)iter_true_lits : Sidekick_core.Lit.t Iter.t;(*Iterate on literals that are true in the trail
*)
}Satisfiable
type unsat_result = {unsat_core : unit -> Sidekick_core.Lit.t Iter.t;(*Unsat core (subset of assumptions), or empty
*)unsat_proof : unit -> Sidekick_proof.Step.id option;(*Proof step for the empty clause
*)
}Unsatisfiable
type t = | Sat of sat_result| Unsat of unsat_result| Unknown of Unknown.t(*Unknown, obtained after a timeout, memory limit, etc.
*)
Result of calling "check"
val pp : Sidekick_core.Fmt.t -> t -> unit
+Check_res (sidekick.Sidekick_abstract_solver.Check_res) Module Sidekick_abstract_solver.Check_res
Result of solving for the current set of clauses
type value = Sidekick_core.Term.ttype sat_result = {get_value : Sidekick_core.Term.t -> value option;(*Value for this term
*)iter_classes : (Sidekick_core.Term.t Iter.t * value) Iter.t;(*All equivalence classes in the congruence closure
*)eval_lit : Sidekick_core.Lit.t -> bool option;(*Evaluate literal
*)iter_true_lits : Sidekick_core.Lit.t Iter.t;(*Iterate on literals that are true in the trail
*)
}Satisfiable
type unsat_result = {unsat_core : unit -> Sidekick_core.Lit.t Iter.t;(*Unsat core (subset of assumptions), or empty
*)unsat_proof : unit -> Sidekick_proof.Step.id option;(*Proof step for the empty clause
*)
}Unsatisfiable
type t = | Sat of sat_result| Unsat of unsat_result| Unknown of Unknown.t(*Unknown, obtained after a timeout, memory limit, etc.
*)
Result of calling "check"
val pp : Sidekick_core.Fmt.t -> t -> unit
diff --git a/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html b/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html
index 8e3f00c0..74cef914 100644
--- a/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html
+++ b/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html
@@ -1,2 +1,2 @@
-Unknown (sidekick.Sidekick_abstract_solver.Unknown) Module Sidekick_abstract_solver.Unknown
val pp : t Sidekick_core.Fmt.printer
+Unknown (sidekick.Sidekick_abstract_solver.Unknown) Module Sidekick_abstract_solver.Unknown
val pp : t Sidekick_core.Fmt.printer
diff --git a/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html
index 093292f1..69f7d134 100644
--- a/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html
+++ b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html
@@ -1,5 +1,5 @@
-t (sidekick.Sidekick_abstract_solver.t) Class type Sidekick_abstract_solver.t
Main abstract solver type
method assert_term : Sidekick_core.Term.t -> unitHelper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.
This uses Proof_sat.sat_input_clause to justify the assertion.
method assert_clause : Sidekick_core.Lit.t array ->
+t (sidekick.Sidekick_abstract_solver.t) Class type Sidekick_abstract_solver.t
Main abstract solver type
method assert_term : Sidekick_core.Term.t -> unitHelper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.
This uses Proof_sat.sat_input_clause to justify the assertion.
method assert_clause : Sidekick_core.Lit.t array ->
Asolver.Proof.Pterm.delayed ->
unitadd_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.
method assert_clause_l : Sidekick_core.Lit.t list ->
Asolver.Proof.Pterm.delayed ->
diff --git a/dev/sidekick/Sidekick_abstract_solver/index.html b/dev/sidekick/Sidekick_abstract_solver/index.html
index c22b7d06..078f7f59 100644
--- a/dev/sidekick/Sidekick_abstract_solver/index.html
+++ b/dev/sidekick/Sidekick_abstract_solver/index.html
@@ -1,2 +1,2 @@
-Sidekick_abstract_solver (sidekick.Sidekick_abstract_solver) Module Sidekick_abstract_solver
Abstract interface for a solver
module Unknown : sig ... endmodule Check_res : sig ... endResult of solving for the current set of clauses
module Asolver : sig ... endAbstract interface for a solver
+Sidekick_abstract_solver (sidekick.Sidekick_abstract_solver) Module Sidekick_abstract_solver
Abstract interface for a solver
module Unknown : sig ... endmodule Check_res : sig ... endResult of solving for the current set of clauses
module Asolver : sig ... endAbstract interface for a solver
diff --git a/dev/sidekick/Sidekick_arith/index.html b/dev/sidekick/Sidekick_arith/index.html
index 62092457..86b113f4 100644
--- a/dev/sidekick/Sidekick_arith/index.html
+++ b/dev/sidekick/Sidekick_arith/index.html
@@ -1,2 +1,2 @@
-Sidekick_arith (sidekick.Sidekick_arith) Module Sidekick_arith
module type NUM = sig ... endmodule type INT = sig ... endmodule type RATIONAL = sig ... endmodule type INT_FULL = sig ... end
+Sidekick_arith (sidekick.Sidekick_arith) Module Sidekick_arith
module type NUM = sig ... endmodule type INT = sig ... endmodule type RATIONAL = sig ... endmodule type INT_FULL = sig ... end
diff --git a/dev/sidekick/Sidekick_arith/module-type-INT/index.html b/dev/sidekick/Sidekick_arith/module-type-INT/index.html
index 501f0f9e..a1ecd5cc 100644
--- a/dev/sidekick/Sidekick_arith/module-type-INT/index.html
+++ b/dev/sidekick/Sidekick_arith/module-type-INT/index.html
@@ -1,2 +1,2 @@
-INT (sidekick.Sidekick_arith.INT) Module type Sidekick_arith.INT
include NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
+INT (sidekick.Sidekick_arith.INT) Module type Sidekick_arith.INT
include NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
diff --git a/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html b/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html
index 5dfb1e75..0485510a 100644
--- a/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html
+++ b/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html
@@ -1,2 +1,2 @@
-INT_FULL (sidekick.Sidekick_arith.INT_FULL) Module type Sidekick_arith.INT_FULL
include INT
include NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval probab_prime : t -> bool
+INT_FULL (sidekick.Sidekick_arith.INT_FULL) Module type Sidekick_arith.INT_FULL
include INT
include NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval probab_prime : t -> bool
diff --git a/dev/sidekick/Sidekick_arith/module-type-NUM/index.html b/dev/sidekick/Sidekick_arith/module-type-NUM/index.html
index 590cfed6..f92ddc6f 100644
--- a/dev/sidekick/Sidekick_arith/module-type-NUM/index.html
+++ b/dev/sidekick/Sidekick_arith/module-type-NUM/index.html
@@ -1,2 +1,2 @@
-NUM (sidekick.Sidekick_arith.NUM) Module type Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
+NUM (sidekick.Sidekick_arith.NUM) Module type Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
diff --git a/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html b/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html
index 811f788b..8ed6c589 100644
--- a/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html
+++ b/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html
@@ -1,2 +1,2 @@
-RATIONAL (sidekick.Sidekick_arith.RATIONAL) Module type Sidekick_arith.RATIONAL
include NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
+RATIONAL (sidekick.Sidekick_arith.RATIONAL) Module type Sidekick_arith.RATIONAL
include NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval to_string : t -> stringval of_string : string -> t optioninclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
diff --git a/dev/sidekick/Sidekick_bencode/Decode/index.html b/dev/sidekick/Sidekick_bencode/Decode/index.html
index 82b4dc90..46634cb7 100644
--- a/dev/sidekick/Sidekick_bencode/Decode/index.html
+++ b/dev/sidekick/Sidekick_bencode/Decode/index.html
@@ -1,2 +1,2 @@
-Decode (sidekick.Sidekick_bencode.Decode) Module Sidekick_bencode.Decode
val of_string : ?idx:int -> string -> (int * t) optionDecode string, and also return how many bytes were consumed.
val of_string_exn : ?idx:int -> string -> int * tParse string.
+Decode (sidekick.Sidekick_bencode.Decode) Module Sidekick_bencode.Decode
val of_string : ?idx:int -> string -> (int * t) optionDecode string, and also return how many bytes were consumed.
val of_string_exn : ?idx:int -> string -> int * tParse string.
diff --git a/dev/sidekick/Sidekick_bencode/Encode/index.html b/dev/sidekick/Sidekick_bencode/Encode/index.html
index ecd85c2d..9ce5c004 100644
--- a/dev/sidekick/Sidekick_bencode/Encode/index.html
+++ b/dev/sidekick/Sidekick_bencode/Encode/index.html
@@ -1,2 +1,2 @@
-Encode (sidekick.Sidekick_bencode.Encode) Module Sidekick_bencode.Encode
+Encode (sidekick.Sidekick_bencode.Encode) Module Sidekick_bencode.Encode
diff --git a/dev/sidekick/Sidekick_bencode/index.html b/dev/sidekick/Sidekick_bencode/index.html
index eb2018c1..5e0d903f 100644
--- a/dev/sidekick/Sidekick_bencode/index.html
+++ b/dev/sidekick/Sidekick_bencode/index.html
@@ -1,2 +1,2 @@
-Sidekick_bencode (sidekick.Sidekick_bencode) Module Sidekick_bencode
+Sidekick_bencode (sidekick.Sidekick_bencode) Module Sidekick_bencode
diff --git a/dev/sidekick/Sidekick_cc/CC/Handler_action/index.html b/dev/sidekick/Sidekick_cc/CC/Handler_action/index.html
index 4a59c37c..78a96d0a 100644
--- a/dev/sidekick/Sidekick_cc/CC/Handler_action/index.html
+++ b/dev/sidekick/Sidekick_cc/CC/Handler_action/index.html
@@ -1,2 +1,2 @@
-Handler_action (sidekick.Sidekick_cc.CC.Handler_action) Module CC.Handler_action
Handler Actions
Actions that can be scheduled by event handlers.
type t = | Act_merge of E_node.t * E_node.t * Expl.t| Act_propagate of Sidekick_core.Lit.t * propagation_reason
+Handler_action (sidekick.Sidekick_cc.CC.Handler_action) Module CC.Handler_action
Handler Actions
Actions that can be scheduled by event handlers.
type t = | Act_merge of E_node.t * E_node.t * Expl.t| Act_propagate of Sidekick_core.Lit.t * propagation_reason
diff --git a/dev/sidekick/Sidekick_cc/CC/Make/argument-1-_/index.html b/dev/sidekick/Sidekick_cc/CC/Make/argument-1-_/index.html
index 1b2a7029..074ca373 100644
--- a/dev/sidekick/Sidekick_cc/CC/Make/argument-1-_/index.html
+++ b/dev/sidekick/Sidekick_cc/CC/Make/argument-1-_/index.html
@@ -1,2 +1,2 @@
-_ (sidekick.Sidekick_cc.CC.Make._) Parameter Make._
val view_as_cc : view_as_ccView the Term.t through the lens of the congruence closure
+_ (sidekick.Sidekick_cc.CC.Make._) Parameter Make._
val view_as_cc : view_as_ccView the Term.t through the lens of the congruence closure
diff --git a/dev/sidekick/Sidekick_cc/CC/Make/index.html b/dev/sidekick/Sidekick_cc/CC/Make/index.html
index 9424f7ee..5f1b2067 100644
--- a/dev/sidekick/Sidekick_cc/CC/Make/index.html
+++ b/dev/sidekick/Sidekick_cc/CC/Make/index.html
@@ -1,5 +1,5 @@
-Make (sidekick.Sidekick_cc.CC.Make) Module CC.Make
Parameters
Signature
val create :
+Make (sidekick.Sidekick_cc.CC.Make) Module CC.Make
Parameters
Signature
val create :
?stat:Sidekick_util.Stat.t ->
?size:[ `Small | `Big ] ->
Sidekick_core.Term.store ->
diff --git a/dev/sidekick/Sidekick_cc/CC/Result_action/index.html b/dev/sidekick/Sidekick_cc/CC/Result_action/index.html
index a0b4f9a3..bdeeec7d 100644
--- a/dev/sidekick/Sidekick_cc/CC/Result_action/index.html
+++ b/dev/sidekick/Sidekick_cc/CC/Result_action/index.html
@@ -1,2 +1,2 @@
-Result_action (sidekick.Sidekick_cc.CC.Result_action) Module CC.Result_action
Result Actions.
Actions returned by the congruence closure after calling check.
type t = | Act_propagate of {lit : Sidekick_core.Lit.t;reason : propagation_reason;
}(*propagate (Lit.t, reason) declares that reason() => Lit.t is a tautology.
reason() should return a list of literals that are currently true, as well as a proof.Lit.t should be a literal of interest (see S.set_as_lit).
This function might never be called, a congruence closure has the right to not propagate and only trigger conflicts.
*)
type conflict = | Conflict of Sidekick_core.Lit.t list * Sidekick_proof.Step.id(*raise_conflict (c,pr) declares that c is a tautology of the theory of congruence.
*)
+Result_action (sidekick.Sidekick_cc.CC.Result_action) Module CC.Result_action
Result Actions.
Actions returned by the congruence closure after calling check.
type t = | Act_propagate of {lit : Sidekick_core.Lit.t;reason : propagation_reason;
}(*propagate (Lit.t, reason) declares that reason() => Lit.t is a tautology.
reason() should return a list of literals that are currently true, as well as a proof.Lit.t should be a literal of interest (see S.set_as_lit).
This function might never be called, a congruence closure has the right to not propagate and only trigger conflicts.
*)
type conflict = | Conflict of Sidekick_core.Lit.t list * Sidekick_proof.Step.id(*raise_conflict (c,pr) declares that c is a tautology of the theory of congruence.
*)
diff --git a/dev/sidekick/Sidekick_cc/CC/index.html b/dev/sidekick/Sidekick_cc/CC/index.html
index c3c6a4a9..82ebe200 100644
--- a/dev/sidekick/Sidekick_cc/CC/index.html
+++ b/dev/sidekick/Sidekick_cc/CC/index.html
@@ -1,5 +1,5 @@
-CC (sidekick.Sidekick_cc.CC) Module Sidekick_cc.CC
Main congruence closure signature.
The congruence closure handles the theory QF_UF (uninterpreted function symbols). It is also responsible for theory combination, and provides a general framework for equality reasoning that other theories piggyback on.
For example, the theory of datatypes relies on the congruence closure to do most of the work, and "only" adds injectivity/disjointness/acyclicity lemmas when needed.
Similarly, a theory of arrays would hook into the congruence closure and assert (dis)equalities as needed.
type e_node = E_node.tA node of the congruence closure
type repr = E_node.tNode that is currently a representative.
type explanation = Expl.tA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
Accessors
val term_store : t -> Sidekick_core.Term.storeval proof_tracer : t -> Sidekick_proof.Tracer.tval stat : t -> Sidekick_util.Stat.tval add_term : t -> Sidekick_core.Term.t -> e_nodeAdd the Term.t to the congruence closure, if not present already. Will be backtracked.
val mem_term : t -> Sidekick_core.Term.t -> boolReturns true if the Term.t is explicitly present in the congruence closure
Allocate a new e_node field (see E_node.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each class_ individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor Term.t in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
Set the bitfield for the e_node. This will be backtracked. See E_node.bitfield.
type propagation_reason =
+CC (sidekick.Sidekick_cc.CC) Module Sidekick_cc.CC
Main congruence closure signature.
The congruence closure handles the theory QF_UF (uninterpreted function symbols). It is also responsible for theory combination, and provides a general framework for equality reasoning that other theories piggyback on.
For example, the theory of datatypes relies on the congruence closure to do most of the work, and "only" adds injectivity/disjointness/acyclicity lemmas when needed.
Similarly, a theory of arrays would hook into the congruence closure and assert (dis)equalities as needed.
type e_node = E_node.tA node of the congruence closure
type repr = E_node.tNode that is currently a representative.
type explanation = Expl.tA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
Accessors
val term_store : t -> Sidekick_core.Term.storeval proof_tracer : t -> Sidekick_proof.Tracer.tval stat : t -> Sidekick_util.Stat.tval add_term : t -> Sidekick_core.Term.t -> e_nodeAdd the Term.t to the congruence closure, if not present already. Will be backtracked.
val mem_term : t -> Sidekick_core.Term.t -> boolReturns true if the Term.t is explicitly present in the congruence closure
Allocate a new e_node field (see E_node.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each class_ individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor Term.t in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
Set the bitfield for the e_node. This will be backtracked. See E_node.bitfield.
type propagation_reason =
unit ->
Sidekick_core.Lit.t list * Sidekick_proof.Pterm.delayedmodule Handler_action : sig ... endHandler Actions
module Result_action : sig ... endResult Actions.
Events
Events triggered by the congruence closure, to which other plugins can subscribe.
val on_pre_merge :
t ->
diff --git a/dev/sidekick/Sidekick_cc/CC/module-type-ARG/index.html b/dev/sidekick/Sidekick_cc/CC/module-type-ARG/index.html
index 62ea3cbc..87d01379 100644
--- a/dev/sidekick/Sidekick_cc/CC/module-type-ARG/index.html
+++ b/dev/sidekick/Sidekick_cc/CC/module-type-ARG/index.html
@@ -1,2 +1,2 @@
-ARG (sidekick.Sidekick_cc.CC.ARG) Module type CC.ARG
Arguments to a congruence closure's implementation
val view_as_cc : view_as_ccView the Term.t through the lens of the congruence closure
+ARG (sidekick.Sidekick_cc.CC.ARG) Module type CC.ARG
Arguments to a congruence closure's implementation
val view_as_cc : view_as_ccView the Term.t through the lens of the congruence closure
diff --git a/dev/sidekick/Sidekick_cc/CC/module-type-BUILD/index.html b/dev/sidekick/Sidekick_cc/CC/module-type-BUILD/index.html
index 51914a5f..e1e0fec1 100644
--- a/dev/sidekick/Sidekick_cc/CC/module-type-BUILD/index.html
+++ b/dev/sidekick/Sidekick_cc/CC/module-type-BUILD/index.html
@@ -1,5 +1,5 @@
-BUILD (sidekick.Sidekick_cc.CC.BUILD) Module type CC.BUILD
val create :
+BUILD (sidekick.Sidekick_cc.CC.BUILD) Module type CC.BUILD
val create :
?stat:Sidekick_util.Stat.t ->
?size:[ `Small | `Big ] ->
Sidekick_core.Term.store ->
diff --git a/dev/sidekick/Sidekick_cc/E_node/Internal_/index.html b/dev/sidekick/Sidekick_cc/E_node/Internal_/index.html
index b4e9f2ed..e2928e17 100644
--- a/dev/sidekick/Sidekick_cc/E_node/Internal_/index.html
+++ b/dev/sidekick/Sidekick_cc/E_node/Internal_/index.html
@@ -1,2 +1,2 @@
-Internal_ (sidekick.Sidekick_cc.E_node.Internal_) Module E_node.Internal_
val make : Sidekick_core.Term.t -> t
+Internal_ (sidekick.Sidekick_cc.E_node.Internal_) Module E_node.Internal_
val make : Sidekick_core.Term.t -> t
diff --git a/dev/sidekick/Sidekick_cc/E_node/index.html b/dev/sidekick/Sidekick_cc/E_node/index.html
index eea6f705..65fdfc7d 100644
--- a/dev/sidekick/Sidekick_cc/E_node/index.html
+++ b/dev/sidekick/Sidekick_cc/E_node/index.html
@@ -1,2 +1,2 @@
-E_node (sidekick.Sidekick_cc.E_node) Module Sidekick_cc.E_node
E-node.
An e-node is a node in the congruence closure that is contained in some equivalence classe). An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in its representative's E_node.t.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
An E-node.
A value of type t points to a particular Term.t, but see find to get the representative of the class.
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval term : t -> Sidekick_core.Term.tTerm contained in this equivalence class. If is_root n, then Term.t n is the class' representative Term.t.
Are two classes physically equal? To check for logical equality, use CC.E_node.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this E_node.t.
val is_root : t -> boolIs the E_node.t a root (ie the representative of its class)? See find to get the root.
Traverse the congruence class. Precondition: is_root n (see find below)
Traverse the parents of the class. Precondition: is_root n (see find below)
val as_lit : t -> Sidekick_core.Lit.t optionSwap the next pointer of each node. If their classes were disjoint, they are now unioned.
module Internal_ : sig ... end
+E_node (sidekick.Sidekick_cc.E_node) Module Sidekick_cc.E_node
E-node.
An e-node is a node in the congruence closure that is contained in some equivalence classe). An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in its representative's E_node.t.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
An E-node.
A value of type t points to a particular Term.t, but see find to get the representative of the class.
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval term : t -> Sidekick_core.Term.tTerm contained in this equivalence class. If is_root n, then Term.t n is the class' representative Term.t.
Are two classes physically equal? To check for logical equality, use CC.E_node.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this E_node.t.
val is_root : t -> boolIs the E_node.t a root (ie the representative of its class)? See find to get the root.
Traverse the congruence class. Precondition: is_root n (see find below)
Traverse the parents of the class. Precondition: is_root n (see find below)
val as_lit : t -> Sidekick_core.Lit.t optionSwap the next pointer of each node. If their classes were disjoint, they are now unioned.
module Internal_ : sig ... end
diff --git a/dev/sidekick/Sidekick_cc/Expl/index.html b/dev/sidekick/Sidekick_cc/Expl/index.html
index bce7be4d..7c988280 100644
--- a/dev/sidekick/Sidekick_cc/Expl/index.html
+++ b/dev/sidekick/Sidekick_cc/Expl/index.html
@@ -1,5 +1,5 @@
-Expl (sidekick.Sidekick_cc.Expl) Module Sidekick_cc.Expl
Explanations
Explanations are specialized proofs, created by the congruence closure when asked to justify why two terms are equal.
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval mk_merge_t : Sidekick_core.Term.t -> Sidekick_core.Term.t -> tExplanation: the terms were explicitly merged
val mk_lit : Sidekick_core.Lit.t -> tExplanation: we merged t and u because of literal t=u, or we merged t and true because of literal t, or t and false because of literal ¬t
val mk_theory :
+Expl (sidekick.Sidekick_cc.Expl) Module Sidekick_cc.Expl
Explanations
Explanations are specialized proofs, created by the congruence closure when asked to justify why two terms are equal.
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval mk_merge_t : Sidekick_core.Term.t -> Sidekick_core.Term.t -> tExplanation: the terms were explicitly merged
val mk_lit : Sidekick_core.Lit.t -> tExplanation: we merged t and u because of literal t=u, or we merged t and true because of literal t, or t and false because of literal ¬t
val mk_theory :
Sidekick_core.Term.t ->
Sidekick_core.Term.t ->
(Sidekick_core.Term.t * Sidekick_core.Term.t * t list) list ->
diff --git a/dev/sidekick/Sidekick_cc/Plugin/Make/argument-1-M/index.html b/dev/sidekick/Sidekick_cc/Plugin/Make/argument-1-M/index.html
index bf321409..8bd6758f 100644
--- a/dev/sidekick/Sidekick_cc/Plugin/Make/argument-1-M/index.html
+++ b/dev/sidekick/Sidekick_cc/Plugin/Make/argument-1-M/index.html
@@ -1,5 +1,5 @@
-M (sidekick.Sidekick_cc.Plugin.Make.M) Parameter Make.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
+M (sidekick.Sidekick_cc.Plugin.Make.M) Parameter Make.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
CC.t ->
state ->
E_node.t ->
diff --git a/dev/sidekick/Sidekick_cc/Plugin/Make/index.html b/dev/sidekick/Sidekick_cc/Plugin/Make/index.html
index 7c264155..f070c105 100644
--- a/dev/sidekick/Sidekick_cc/Plugin/Make/index.html
+++ b/dev/sidekick/Sidekick_cc/Plugin/Make/index.html
@@ -1,2 +1,2 @@
-Make (sidekick.Sidekick_cc.Plugin.Make) Module Plugin.Make
Create a plugin builder from the given per-class monoid
Parameters
module M : sig ... endSignature
module M = Mmodule type DYN_PL_FOR_M = sig ... endtype t = (module DYN_PL_FOR_M)include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
+Make (sidekick.Sidekick_cc.Plugin.Make) Module Plugin.Make
Create a plugin builder from the given per-class monoid
Parameters
module M : sig ... endSignature
module M = Mmodule type DYN_PL_FOR_M = sig ... endtype t = (module DYN_PL_FOR_M)include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
diff --git a/dev/sidekick/Sidekick_cc/Plugin/Make/module-type-DYN_PL_FOR_M/index.html b/dev/sidekick/Sidekick_cc/Plugin/Make/module-type-DYN_PL_FOR_M/index.html
index a797cd8c..416d3e4c 100644
--- a/dev/sidekick/Sidekick_cc/Plugin/Make/module-type-DYN_PL_FOR_M/index.html
+++ b/dev/sidekick/Sidekick_cc/Plugin/Make/module-type-DYN_PL_FOR_M/index.html
@@ -1,2 +1,2 @@
-DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.Make.DYN_PL_FOR_M) Module type Make.DYN_PL_FOR_M
module M = Minclude Sidekick_sigs.DYN_BACKTRACKABLE
val mem : E_node.t -> boolDoes the CC E_node.t have a monoid value?
+DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.Make.DYN_PL_FOR_M) Module type Make.DYN_PL_FOR_M
module M = Minclude Sidekick_sigs.DYN_BACKTRACKABLE
val mem : E_node.t -> boolDoes the CC E_node.t have a monoid value?
diff --git a/dev/sidekick/Sidekick_cc/Plugin/index.html b/dev/sidekick/Sidekick_cc/Plugin/index.html
index d95932ee..6301e8e0 100644
--- a/dev/sidekick/Sidekick_cc/Plugin/index.html
+++ b/dev/sidekick/Sidekick_cc/Plugin/index.html
@@ -1,2 +1,2 @@
-Plugin (sidekick.Sidekick_cc.Plugin) Module Sidekick_cc.Plugin
Congruence Closure Plugin
module type EXTENDED_PLUGIN_BUILDER = sig ... endmodule Make (M : sig ... end) : EXTENDED_PLUGIN_BUILDER with module M = MCreate a plugin builder from the given per-class monoid
+Plugin (sidekick.Sidekick_cc.Plugin) Module Sidekick_cc.Plugin
Congruence Closure Plugin
module type EXTENDED_PLUGIN_BUILDER = sig ... endmodule Make (M : sig ... end) : EXTENDED_PLUGIN_BUILDER with module M = MCreate a plugin builder from the given per-class monoid
diff --git a/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/M/index.html b/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/M/index.html
index 944b5844..2832052d 100644
--- a/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/M/index.html
+++ b/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/M/index.html
@@ -1,5 +1,5 @@
-M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.M) Module EXTENDED_PLUGIN_BUILDER.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
+M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.M) Module EXTENDED_PLUGIN_BUILDER.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
CC.t ->
state ->
E_node.t ->
diff --git a/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/index.html b/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/index.html
index e16d81fe..aa75f261 100644
--- a/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/index.html
+++ b/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/index.html
@@ -1,2 +1,2 @@
-EXTENDED_PLUGIN_BUILDER (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER) Module type Plugin.EXTENDED_PLUGIN_BUILDER
module M : sig ... endmodule type DYN_PL_FOR_M = sig ... endtype t = (module DYN_PL_FOR_M)include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
+EXTENDED_PLUGIN_BUILDER (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER) Module type Plugin.EXTENDED_PLUGIN_BUILDER
module M : sig ... endmodule type DYN_PL_FOR_M = sig ... endtype t = (module DYN_PL_FOR_M)include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
diff --git a/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/module-type-DYN_PL_FOR_M/index.html b/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/module-type-DYN_PL_FOR_M/index.html
index a77aedcb..194b087b 100644
--- a/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/module-type-DYN_PL_FOR_M/index.html
+++ b/dev/sidekick/Sidekick_cc/Plugin/module-type-EXTENDED_PLUGIN_BUILDER/module-type-DYN_PL_FOR_M/index.html
@@ -1,2 +1,2 @@
-DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M) Module type EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M
module M = Minclude Sidekick_sigs.DYN_BACKTRACKABLE
val mem : E_node.t -> boolDoes the CC E_node.t have a monoid value?
+DYN_PL_FOR_M (sidekick.Sidekick_cc.Plugin.EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M) Module type EXTENDED_PLUGIN_BUILDER.DYN_PL_FOR_M
module M = Minclude Sidekick_sigs.DYN_BACKTRACKABLE
val mem : E_node.t -> boolDoes the CC E_node.t have a monoid value?
diff --git a/dev/sidekick/Sidekick_cc/Resolved_expl/index.html b/dev/sidekick/Sidekick_cc/Resolved_expl/index.html
index fc403590..febe6fad 100644
--- a/dev/sidekick/Sidekick_cc/Resolved_expl/index.html
+++ b/dev/sidekick/Sidekick_cc/Resolved_expl/index.html
@@ -1,2 +1,2 @@
-Resolved_expl (sidekick.Sidekick_cc.Resolved_expl) Module Sidekick_cc.Resolved_expl
Resolved explanations.
The congruence closure keeps explanations for why terms are in the same class. However these are represented in a compact, cheap form. To use these explanations we need to resolve them into a resolved explanation, typically a list of literals that are true in the current trail and are responsible for merges.
However, we can also have merged classes because they have the same value in the current model.
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
+Resolved_expl (sidekick.Sidekick_cc.Resolved_expl) Module Sidekick_cc.Resolved_expl
Resolved explanations.
The congruence closure keeps explanations for why terms are in the same class. However these are represented in a compact, cheap form. To use these explanations we need to resolve them into a resolved explanation, typically a list of literals that are true in the current trail and are responsible for merges.
However, we can also have merged classes because they have the same value in the current model.
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printer
diff --git a/dev/sidekick/Sidekick_cc/Signature/index.html b/dev/sidekick/Sidekick_cc/Signature/index.html
index 5bd77f45..f35974f1 100644
--- a/dev/sidekick/Sidekick_cc/Signature/index.html
+++ b/dev/sidekick/Sidekick_cc/Signature/index.html
@@ -1,5 +1,5 @@
-Signature (sidekick.Sidekick_cc.Signature) Module Sidekick_cc.Signature
A signature is a shallow term shape where immediate subterms are representative
type t =
+Signature (sidekick.Sidekick_cc.Signature) Module Sidekick_cc.Signature
A signature is a shallow term shape where immediate subterms are representative
type t =
(Sidekick_core.Const.t,
Sidekick_cc__.Types_.e_node,
Sidekick_cc__.Types_.e_node list)
diff --git a/dev/sidekick/Sidekick_cc/index.html b/dev/sidekick/Sidekick_cc/index.html
index 02a497c3..b2d3b403 100644
--- a/dev/sidekick/Sidekick_cc/index.html
+++ b/dev/sidekick/Sidekick_cc/index.html
@@ -1,5 +1,5 @@
-Sidekick_cc (sidekick.Sidekick_cc) Module Sidekick_cc
Congruence Closure Implementation
module type DYN_MONOID_PLUGIN = sig ... endmodule type MONOID_PLUGIN_ARG = sig ... endmodule type MONOID_PLUGIN_BUILDER = sig ... endmodule View = Sidekick_core.CC_viewmodule E_node : sig ... endE-node.
module Expl : sig ... endExplanations
module Signature : sig ... endA signature is a shallow term shape where immediate subterms are representative
module Resolved_expl : sig ... endResolved explanations.
module Plugin : sig ... endCongruence Closure Plugin
module CC : sig ... endMain congruence closure signature.
include module type of struct include CC end
type e_node = E_node.tA node of the congruence closure
type repr = E_node.tNode that is currently a representative.
type explanation = Expl.tA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
type t = CC.tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
Accessors
val term_store : t -> Sidekick_core.Term.storeval proof_tracer : t -> Sidekick_proof.Tracer.tval stat : t -> Sidekick_util.Stat.tval add_term : t -> Sidekick_core.Term.t -> e_nodeAdd the Term.t to the congruence closure, if not present already. Will be backtracked.
val mem_term : t -> Sidekick_core.Term.t -> boolReturns true if the Term.t is explicitly present in the congruence closure
Allocate a new e_node field (see E_node.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each class_ individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor Term.t in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
Set the bitfield for the e_node. This will be backtracked. See E_node.bitfield.
type propagation_reason =
+Sidekick_cc (sidekick.Sidekick_cc) Module Sidekick_cc
Congruence Closure Implementation
module type DYN_MONOID_PLUGIN = sig ... endmodule type MONOID_PLUGIN_ARG = sig ... endmodule type MONOID_PLUGIN_BUILDER = sig ... endmodule View = Sidekick_core.CC_viewmodule E_node : sig ... endE-node.
module Expl : sig ... endExplanations
module Signature : sig ... endA signature is a shallow term shape where immediate subterms are representative
module Resolved_expl : sig ... endResolved explanations.
module Plugin : sig ... endCongruence Closure Plugin
module CC : sig ... endMain congruence closure signature.
include module type of struct include CC end
type e_node = E_node.tA node of the congruence closure
type repr = E_node.tNode that is currently a representative.
type explanation = Expl.tA field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See allocate_bitfield.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
type t = CC.tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
Accessors
val term_store : t -> Sidekick_core.Term.storeval proof_tracer : t -> Sidekick_proof.Tracer.tval stat : t -> Sidekick_util.Stat.tval add_term : t -> Sidekick_core.Term.t -> e_nodeAdd the Term.t to the congruence closure, if not present already. Will be backtracked.
val mem_term : t -> Sidekick_core.Term.t -> boolReturns true if the Term.t is explicitly present in the congruence closure
Allocate a new e_node field (see E_node.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each class_ individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor Term.t in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
Set the bitfield for the e_node. This will be backtracked. See E_node.bitfield.
type propagation_reason =
unit ->
Sidekick_core.Lit.t list * Sidekick_proof.Pterm.delayedmodule Handler_action = CC.Handler_actionHandler Actions
module Result_action = CC.Result_actionResult Actions.
Events
Events triggered by the congruence closure, to which other plugins can subscribe.
val on_pre_merge :
t ->
diff --git a/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/M/index.html b/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/M/index.html
index 81881d35..4e5dfcce 100644
--- a/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/M/index.html
+++ b/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/M/index.html
@@ -1,5 +1,5 @@
-M (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN.M) Module DYN_MONOID_PLUGIN.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
+M (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN.M) Module DYN_MONOID_PLUGIN.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
CC.t ->
state ->
E_node.t ->
diff --git a/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/index.html b/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/index.html
index 2676798c..5d66dedf 100644
--- a/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/index.html
+++ b/dev/sidekick/Sidekick_cc/module-type-DYN_MONOID_PLUGIN/index.html
@@ -1,2 +1,2 @@
-DYN_MONOID_PLUGIN (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN) Module type Sidekick_cc.DYN_MONOID_PLUGIN
module M : sig ... endinclude Sidekick_sigs.DYN_BACKTRACKABLE
val mem : E_node.t -> boolDoes the CC E_node.t have a monoid value?
+DYN_MONOID_PLUGIN (sidekick.Sidekick_cc.DYN_MONOID_PLUGIN) Module type Sidekick_cc.DYN_MONOID_PLUGIN
module M : sig ... endinclude Sidekick_sigs.DYN_BACKTRACKABLE
val mem : E_node.t -> boolDoes the CC E_node.t have a monoid value?
diff --git a/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_ARG/index.html b/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_ARG/index.html
index 2a71ce38..d984e618 100644
--- a/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_ARG/index.html
+++ b/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_ARG/index.html
@@ -1,5 +1,5 @@
-MONOID_PLUGIN_ARG (sidekick.Sidekick_cc.MONOID_PLUGIN_ARG) Module type Sidekick_cc.MONOID_PLUGIN_ARG
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
+MONOID_PLUGIN_ARG (sidekick.Sidekick_cc.MONOID_PLUGIN_ARG) Module type Sidekick_cc.MONOID_PLUGIN_ARG
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
CC.t ->
state ->
E_node.t ->
diff --git a/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/M/index.html b/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/M/index.html
index 4ec3e7a4..e7079408 100644
--- a/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/M/index.html
+++ b/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/M/index.html
@@ -1,5 +1,5 @@
-M (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER.M) Module MONOID_PLUGIN_BUILDER.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
+M (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER.M) Module MONOID_PLUGIN_BUILDER.M
include Sidekick_sigs.PRINT with type t := t
val pp : t Sidekick_sigs.printerval of_term :
CC.t ->
state ->
E_node.t ->
diff --git a/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/index.html b/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/index.html
index 8eeb8b37..c09ee5eb 100644
--- a/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/index.html
+++ b/dev/sidekick/Sidekick_cc/module-type-MONOID_PLUGIN_BUILDER/index.html
@@ -1,2 +1,2 @@
-MONOID_PLUGIN_BUILDER (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER) Module type Sidekick_cc.MONOID_PLUGIN_BUILDER