diff --git a/dev/index.html b/dev/index.html index be3070b0..97e784ed 100644 --- a/dev/index.html +++ b/dev/index.html @@ -2,7 +2,7 @@
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 db4b4acf..d14194d3 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Term/index.html b/dev/sidekick-base/Sidekick_base/Term/index.html
index fdde6f45..21a4ded2 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 e90e410b..5e65ebd4 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Th_data/index.html b/dev/sidekick-base/Sidekick_base/Th_data/index.html
index 2a8ce0c3..a4cc439a 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Th_lra/index.html b/dev/sidekick-base/Sidekick_base/Th_lra/index.html
index 6047cbe6..f300761b 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
\ No newline at end of file
+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
\ No newline at end of file
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 b2d4faa9..faa7882a 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
\ No newline at end of file
+Th_ty_unin (sidekick-base.Sidekick_base.Th_ty_unin) Module Sidekick_base.Th_ty_unin
val theory : Solver.theory
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Ty/index.html b/dev/sidekick-base/Sidekick_base/Ty/index.html
index e9922978..e7ab43f0 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 8ccde852..8de96190 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 5d2e97c1..64f98194 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 20b3e85f..f3250861 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 fe997a8b..3991590b 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_smtlib/Driver/index.html b/dev/sidekick-base/Sidekick_smtlib/Driver/index.html
index 3e200341..7cf1fec7 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 ec5e6f0f..1dd1b0f6 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_smtlib/Solver/index.html b/dev/sidekick-base/Sidekick_smtlib/Solver/index.html
index 40f1d053..d8b59a1d 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_smtlib/index.html b/dev/sidekick-base/Sidekick_smtlib/index.html
index e7535023..1700e51a 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick-base/index.html b/dev/sidekick-base/index.html
index 747826c9..4f6fdfab 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.
\ No newline at end of file
+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.
\ No newline at end of file
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 6e728c1f..7c881b0e 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
\ No newline at end of file
+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
\ No newline at end of file
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 885a1b11..527f6ab7 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
\ No newline at end of file
+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
\ No newline at end of file
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 f10dc2b3..52192863 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
\ No newline at end of file
+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
\ No newline at end of file
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 af20a8af..f1dba79d 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
\ No newline at end of file
+Drup_parser (sidekick-bin.Sidekick_bin_lib.Drup_parser) Module Sidekick_bin_lib.Drup_parser
\ No newline at end of file
diff --git a/dev/sidekick-bin/Sidekick_bin_lib/index.html b/dev/sidekick-bin/Sidekick_bin_lib/index.html
index 09f4e133..dbdd8120 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 ... end
\ No newline at end of file
+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 ... end
\ No newline at end of file
diff --git a/dev/sidekick-bin/index.html b/dev/sidekick-bin/index.html
index e6ef7e01..61387f16 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.
\ No newline at end of file
+index (sidekick-bin.index) sidekick-bin index
Library sidekick-bin.lib
The entry point of this library is the module: Sidekick_bin_lib.
\ No newline at end of file
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 85bfdc6f..49a2a3d1 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 4a2b7126..1c6b57ad 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 8129a4cc..549f5dda 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html b/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html
index f2ccb2bf..78d06c7e 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
\ No newline at end of file
+Unknown (sidekick.Sidekick_abstract_solver.Unknown) Module Sidekick_abstract_solver.Unknown
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
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 4bc28d47..0ce834c9 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 63c3b793..c831d306 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith/index.html b/dev/sidekick/Sidekick_arith/index.html
index 3d549dda..91e1a7d6 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith/module-type-INT/index.html b/dev/sidekick/Sidekick_arith/module-type-INT/index.html
index 9ab619f3..47054685 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
\ No newline at end of file
+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
\ No newline at end of file
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 fddfde97..10d85b96 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith/module-type-NUM/index.html b/dev/sidekick/Sidekick_arith/module-type-NUM/index.html
index bb2b186e..2770c780 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html b/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html
index 84f73ec1..a627c87d 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)
\ No newline at end of file
+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)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_bencode/Decode/index.html b/dev/sidekick/Sidekick_bencode/Decode/index.html
index 56b4c2ee..273e217b 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.
\ No newline at end of file
+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.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_bencode/Encode/index.html b/dev/sidekick/Sidekick_bencode/Encode/index.html
index 42cd83ab..2639fd6a 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
\ No newline at end of file
+Encode (sidekick.Sidekick_bencode.Encode) Module Sidekick_bencode.Encode
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_bencode/index.html b/dev/sidekick/Sidekick_bencode/index.html
index 32d8bbdb..5b50a008 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
\ No newline at end of file
+Sidekick_bencode (sidekick.Sidekick_bencode) Module Sidekick_bencode
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/CC/Handler_action/index.html b/dev/sidekick/Sidekick_cc/CC/Handler_action/index.html
index b07b3f18..a1efe3f7 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
\ No newline at end of file
+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
\ No newline at end of file
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 7c7b0888..d60520e5 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
\ No newline at end of file
+_ (sidekick.Sidekick_cc.CC.Make._) Parameter Make._
val view_as_cc : view_as_ccView the Term.t through the lens of the congruence closure
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/CC/Make/index.html b/dev/sidekick/Sidekick_cc/CC/Make/index.html
index aefe1b20..d25655ad 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 820a0e19..ba575089 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.
*)
\ No newline at end of file
+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.
*)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/CC/index.html b/dev/sidekick/Sidekick_cc/CC/index.html
index f693d52f..6a011342 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 2fd0d957..71b76781 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
\ No newline at end of file
+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
\ No newline at end of file
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 4d59a289..71b0b331 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 551ca521..d77a3864 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
\ No newline at end of file
+Internal_ (sidekick.Sidekick_cc.E_node.Internal_) Module E_node.Internal_
val make : Sidekick_core.Term.t -> t
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/E_node/index.html b/dev/sidekick/Sidekick_cc/E_node/index.html
index 78900fb5..50cf97d1 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/Expl/index.html b/dev/sidekick/Sidekick_cc/Expl/index.html
index 8217d064..a8531803 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 54a15d8c..61e4d0ce 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 1bc4ab98..8fe5ad2d 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
\ No newline at end of file
+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
\ No newline at end of file
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 6702a0ad..9ea1dbf1 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?
\ No newline at end of file
+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?
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/Plugin/index.html b/dev/sidekick/Sidekick_cc/Plugin/index.html
index b5e3d085..4c930dd4 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
\ No newline at end of file
+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
\ No newline at end of file
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 9a375e52..d6e6d020 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 2de88be2..95d28273 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
\ No newline at end of file
+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
\ No newline at end of file
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 2f19a600..e5c2ea7b 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?
\ No newline at end of file
+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?
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/Resolved_expl/index.html b/dev/sidekick/Sidekick_cc/Resolved_expl/index.html
index 6b341117..96eabaa8 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
\ No newline at end of file
+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
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_cc/Signature/index.html b/dev/sidekick/Sidekick_cc/Signature/index.html
index 7869de1f..59e8e2e4 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 20cadf50..02b6231d 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 8420f9bc..19005ae7 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 715d965b..b75d7a92 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?
\ No newline at end of file
+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?
\ No newline at end of file
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 2b040cfa..1fe50279 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 ae08decc..fe7032f2 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 e6276e60..0ab26e67 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