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 += private | 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 1793e54e..94da641c 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 8b422523..fd8d9afd 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
@@ -8,7 +8,7 @@ n3: g n2 n1
n4: = n3 n3
iter_shallow f e iterates on immediate subterms of e, calling f trdb e' for each subterm e', with trdb = true iff e' is directly under a binder.
val free_vars :
?init:Sidekick_core_logic__.Var.Set.t ->
t ->
- Sidekick_core_logic__.Var.Set.tval is_type : t -> boolis_type t is true iff view t is Type _
val is_a_type : t -> boolis_a_type t is true if is_ty (ty t)
val is_closed : t -> boolIs the term closed (all bound variables are paired with a binder)? time: O(1)
val has_fvars : t -> boolDoes the term contain free variables? time: O(1)
Creation
module Store = Sidekick_core.Term.Storemodule DB = Sidekick_core.Term.DBDe bruijn indices
include module type of struct include Sidekick_core_logic.T_builtins end
val bool : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval proof : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_not : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_eq : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_ite : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval is_type : t -> boolis_type t is true iff view t is Type _
val is_a_type : t -> boolis_a_type t is true if is_ty (ty t)
val is_closed : t -> boolIs the term closed (all bound variables are paired with a binder)? time: O(1)
val has_fvars : t -> boolDoes the term contain free variables? time: O(1)
Creation
module Store = Sidekick_core.Term.Storemodule DB = Sidekick_core.Term.DBDe bruijn indices
include module type of struct include Sidekick_core_logic.T_builtins end
val bool : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval proof : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_not : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_eq : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_ite : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval bool_val :
Sidekick_core_logic.Term.store ->
bool ->
Sidekick_core_logic.Term.tval const_decoders : Sidekick_core_logic.Const.decodersval eq :
diff --git a/dev/sidekick-base/Sidekick_base/Th_bool/index.html b/dev/sidekick-base/Sidekick_base/Th_bool/index.html
index c62d450b..22f885dc 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 1e4b6ba9..ad44ed16 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 668e2132..1bc81638 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 15bda96b..866b26b0 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 3dcc76d2..2ec45584 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
@@ -84,7 +84,7 @@ n4: = n3 n3
var * Sidekick_core_logic__.Types_.term) optionmodule DB = Sidekick_core.Term.DBDe bruijn indices
include module type of struct include Sidekick_core_logic.T_builtins end
val proof : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_not : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_eq : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_ite : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval bool_val :
+ var * Sidekick_core_logic__.Types_.termmodule DB = Sidekick_core.Term.DBDe bruijn indices
include module type of struct include Sidekick_core_logic.T_builtins end
val proof : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_not : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_eq : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval c_ite : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.tval bool_val :
Sidekick_core_logic.Term.store ->
bool ->
Sidekick_core_logic.Term.tval eq :
diff --git a/dev/sidekick-base/Sidekick_base/Types_/index.html b/dev/sidekick-base/Sidekick_base/Types_/index.html
index 854fd276..512a9939 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 71e58f11..f16cf66c 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 abd90bdd..e93c7452 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 8afe0beb..724870a7 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 90bf19f8..dc8398a3 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 f93fd81b..32073fda 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 2aec5727..c8af1434 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 c57e3ef5..79a0b887 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 d0ca19f0..0439e320 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 5e4dcdc8..d7abeb9f 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 f55b2f92..3ff9af4b 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 9cb459d3..9dabc960 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 6efd6423..b6fd78f1 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
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
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 d8c8e18f..57d0c710 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 c2f5ac43..4bf5585a 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 3dc81b96..68e625d8 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 bc360796..6396826f 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 74cef914..ec9f72ed 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 69f7d134..036eae37 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 078f7f59..9e88c89d 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 86b113f4..06c36d48 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 a1ecd5cc..2757a54b 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 0485510a..b48fb8df 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 f92ddc6f..60822d0c 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 8ed6c589..c02639eb 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 46634cb7..068b70bb 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 9ce5c004..d8c98b05 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
Sidekick_bencode (sidekick.Sidekick_bencode) Module Sidekick_bencode
Sidekick_bencode (sidekick.Sidekick_bencode) Module Sidekick_bencode
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 074ca373..2d336eb4 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 5f1b2067..1a1ca2f2 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 bdeeec7d..9dec829c 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 82ebe200..4ecf5987 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 87d01379..a605f825 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 e1e0fec1..aaba922f 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 e2928e17..69a65f2d 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 65fdfc7d..d6015752 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 7c988280..41a952eb 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 8bd6758f..5c478f1e 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 f070c105..6cc434b1 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 416d3e4c..38f5fb22 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 6301e8e0..006c9015 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 2832052d..5d450f4c 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 aa75f261..8a1de634 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 194b087b..627cc90e 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 febe6fad..43cc041b 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 f35974f1..00053601 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 b2d3b403..4823882f 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 4e5dfcce..79486ddf 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 5d66dedf..56d6cb46 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 d984e618..4eebb505 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 e7079408..8a6a15a4 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 c09ee5eb..ad81b5ea 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
MONOID_PLUGIN_BUILDER (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER) Module type Sidekick_cc.MONOID_PLUGIN_BUILDER
DYN_PL_FOR_M (sidekick.Sidekick_cc.MONOID_PLUGIN_BUILDER.DYN_PL_FOR_M) Module type MONOID_PLUGIN_BUILDER.DYN_PL_FOR_M
module M = Minclude Sidekick_sigs.DYN_BACKTRACKABLE