diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html index 35c49985..64c074a2 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html @@ -1,2 +1,2 @@ -
Base_types.FunFunction symbols
type view = fun_view = | Fun_undef of fun_ty | |||||||
| Fun_select of select | |||||||
| Fun_cstor of cstor | |||||||
| Fun_is_a of cstor | |||||||
| Fun_def of {
} | (* user defined function symbol. A good example can be found in |
Possible definitions for a function symbol
val hash : t -> intval is_undefined : t -> boolval do_cc : t -> boolval pp : t CCFormat.printerBase_types.FunFunction symbols
type view = fun_view = | Fun_undef of fun_ty | |||||||
| Fun_select of select | |||||||
| Fun_cstor of cstor | |||||||
| Fun_is_a of cstor | |||||||
| Fun_def of {
} | (* user defined function symbol. A good example can be found in |
Possible definitions for a function symbol
val hash : t -> intval is_undefined : t -> boolval do_cc : t -> boolval pp : t CCFormat.printerBase_types.TermTerm creation and manipulation
type 'a view = 'a term_view = | Bool of bool |
| App_fun of fun_ * 'a Sidekick_util.IArray.t |
| Eq of 'a * 'a |
| Not of 'a |
| Ite of 'a * 'a * 'a |
| LRA of 'a LRA_view.t |
| LIA of 'a LIA_view.t |
val id : t -> intval hash : t -> intval create : ?size:int -> unit -> storeval app_fun : store -> fun_ -> t Sidekick_util.IArray.t -> tapp_undefined store f ty args is app store (Fun.mk_undef f ty) args. It builds a function symbol and applies it into a term immediately
const_undefined store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.
val app_cstor : store -> cstor -> t Sidekick_util.IArray.t -> tval lra : store -> t LRA_view.t -> tval lia : store -> t LIA_view.t -> tmodule type ARITH_HELPER = sig ... endmodule LRA : ARITH_HELPER with type num := Q.tmodule LIA : ARITH_HELPER with type num := Z.tmodule Iter_dag : sig ... endval iter_dag_with : order:Iter_dag.order -> t -> t Iter.tval pp : t Fmt.printerval is_true : t -> boolval is_false : t -> boolval is_const : t -> boolval as_bool : t -> bool optionval store_size : store -> intBase_types.TermTerm creation and manipulation
type 'a view = 'a term_view = | Bool of bool |
| App_fun of fun_ * 'a array |
| Eq of 'a * 'a |
| Not of 'a |
| Ite of 'a * 'a * 'a |
| LRA of 'a LRA_view.t |
| LIA of 'a LIA_view.t |
val id : t -> intval hash : t -> intval create : ?size:int -> unit -> storeapp_undefined store f ty args is app store (Fun.mk_undef f ty) args. It builds a function symbol and applies it into a term immediately
const_undefined store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.
val lra : store -> t LRA_view.t -> tval lia : store -> t LIA_view.t -> tmodule type ARITH_HELPER = sig ... endmodule LRA : ARITH_HELPER with type num := Q.tmodule LIA : ARITH_HELPER with type num := Z.tmodule Iter_dag : sig ... endval iter_dag_with : order:Iter_dag.order -> t -> t Iter.tval pp : t Fmt.printerval is_true : t -> boolval is_false : t -> boolval is_const : t -> boolval as_bool : t -> bool optionval store_size : store -> intBase_types.Term_celltype 'a view = 'a term_view = | Bool of bool |
| App_fun of fun_ * 'a Sidekick_util.IArray.t |
| Eq of 'a * 'a |
| Not of 'a |
| Ite of 'a * 'a * 'a |
| LRA of 'a LRA_view.t |
| LIA of 'a LIA_view.t |
val hash : t -> intval true_ : tval false_ : tval app_fun : fun_ -> term Sidekick_util.IArray.t -> tval lra : term LRA_view.t -> tval lia : term LIA_view.t -> tval pp : t Fmt.printerval iter : ( 'a -> unit ) -> 'a view -> unitmodule type ARG = sig ... endBase_types.Term_celltype 'a view = 'a term_view = | Bool of bool |
| App_fun of fun_ * 'a array |
| Eq of 'a * 'a |
| Not of 'a |
| Ite of 'a * 'a * 'a |
| LRA of 'a LRA_view.t |
| LIA of 'a LIA_view.t |
val hash : t -> intval true_ : tval false_ : tval lra : term LRA_view.t -> tval lia : term LIA_view.t -> tval pp : t Fmt.printerval iter : ( 'a -> unit ) -> 'a view -> unitmodule type ARG = sig ... endSidekick_base.Base_typesBasic type definitions for Sidekick_base
module Vec = Sidekick_util.Vecmodule Log = Sidekick_util.Logmodule CC_view = Sidekick_core.CC_viewmodule Proof_ser = Sidekick_base_proof_trace.Proof_sermodule Storage = Sidekick_base_proof_trace.Storagemodule LRA_pred : sig ... endmodule LRA_op : sig ... endmodule LRA_view : sig ... endmodule LIA_pred = LRA_predmodule LIA_op = LRA_opmodule LIA_view : sig ... endTerm.
A term, with its own view, type, and a unique identifier. Do not create directly, see Term.
and 'a term_view = | Bool of bool |
| App_fun of fun_ * 'a Sidekick_util.IArray.t |
| Eq of 'a * 'a |
| Not of 'a |
| Ite of 'a * 'a * 'a |
| LRA of 'a LRA_view.t |
| LIA of 'a LIA_view.t |
Shallow structure of a term.
A term is a DAG (direct acyclic graph) of nodes, each of which has a term view.
and fun_view = | Fun_undef of fun_ty | |||||||
| Fun_select of select | |||||||
| Fun_cstor of cstor | |||||||
| Fun_is_a of cstor | |||||||
| Fun_def of {
} | (* Methods on the custom term view whose arguments are
|
Hashconsed type
and value = | V_bool of bool | |||||
| V_element of {
} | (* a named constant, distinct from any other constant *) | ||||
| V_cstor of {
} | |||||
| V_custom of {
} | (* Custom value *) | ||||
| V_real of Q.t |
Semantic values, used for models (and possibly model-constructing calculi)
type statement = | Stmt_set_logic of string |
| Stmt_set_option of string list |
| Stmt_set_info of string * string |
| Stmt_data of data list |
| Stmt_ty_decl of ID.t * int |
| Stmt_decl of ID.t * ty list * ty |
| Stmt_define of definition list |
| Stmt_assert of term |
| Stmt_assert_clause of term list |
| Stmt_check_sat of (bool * term) list |
| Stmt_get_model |
| Stmt_get_value of term list |
| Stmt_exit |
val term_hash_ : term -> intval pp_fun : CCFormat.t -> fun_ -> unitval hash_value : value Sidekick_util.Hash.tval pp_value : value Sidekick_util.Util.printerval pp_ty : ty Sidekick_util.Util.printerval pp_term_view_gen :
+Base_types (sidekick-base.Sidekick_base.Base_types) Module Sidekick_base.Base_types
Basic type definitions for Sidekick_base
module Vec = Sidekick_util.Vecmodule Log = Sidekick_util.Logmodule CC_view = Sidekick_core.CC_viewmodule Proof_ser = Sidekick_base_proof_trace.Proof_sermodule Storage = Sidekick_base_proof_trace.Storagemodule LRA_pred : sig ... endmodule LRA_op : sig ... endmodule LRA_view : sig ... endmodule LIA_pred = LRA_predmodule LIA_op = LRA_opmodule LIA_view : sig ... endTerm.
A term, with its own view, type, and a unique identifier. Do not create directly, see Term.
and 'a term_view = | Bool of bool| App_fun of fun_ * 'a array| Eq of 'a * 'a| Not of 'a| Ite of 'a * 'a * 'a| LRA of 'a LRA_view.t| LIA of 'a LIA_view.t
Shallow structure of a term.
A term is a DAG (direct acyclic graph) of nodes, each of which has a term view.
and fun_view = | Fun_undef of fun_ty| Fun_select of select| Fun_cstor of cstor| Fun_is_a of cstor| Fun_def of {pp : 'a. ( 'a Fmt.printer -> 'a array Fmt.printer ) option;abs : self:term -> term array -> term * bool;do_cc : bool;relevant : 'a. ID.t -> 'a array -> int -> bool;ty : ID.t -> term array -> ty;eval : value array -> value;
}(*Methods on the custom term view whose arguments are 'a. Terms must be printable, and provide some additional theory handles.
relevant must return a subset of args (possibly the same set). The terms it returns will be activated and evaluated whenever possible. Terms in args \ relevant args are considered for congruence but not for evaluation.
*)
Hashconsed type
and value = | V_bool of bool| V_element of {id : ID.t;ty : ty;
}(*a named constant, distinct from any other constant
*) | V_cstor of {c : cstor;args : value list;
}| V_custom of {view : value_custom_view;pp : value_custom_view Fmt.printer;eq : value_custom_view -> value_custom_view -> bool;hash : value_custom_view -> int;
}(*Custom value
*) | V_real of Q.t
Semantic values, used for models (and possibly model-constructing calculi)
type statement = | Stmt_set_logic of string| Stmt_set_option of string list| Stmt_set_info of string * string| Stmt_data of data list| Stmt_ty_decl of ID.t * int| Stmt_decl of ID.t * ty list * ty| Stmt_define of definition list| Stmt_assert of term| Stmt_assert_clause of term list| Stmt_check_sat of (bool * term) list| Stmt_get_model| Stmt_get_value of term list| Stmt_exit
val term_hash_ : term -> intval pp_fun : CCFormat.t -> fun_ -> unitval hash_value : value Sidekick_util.Hash.tval pp_value : value Sidekick_util.Util.printerval pp_ty : ty Sidekick_util.Util.printerval pp_term_view_gen :
pp_id:( Fmt.t -> ID.t -> unit ) ->
pp_t:'a Fmt.printer ->
Fmt.t ->
diff --git a/dev/sidekick-base/Sidekick_base/Form/Funs/index.html b/dev/sidekick-base/Sidekick_base/Form/Funs/index.html
index eef026a8..ef9c63db 100644
--- a/dev/sidekick-base/Sidekick_base/Form/Funs/index.html
+++ b/dev/sidekick-base/Sidekick_base/Form/Funs/index.html
@@ -1,2 +1,2 @@
-Funs (sidekick-base.Sidekick_base.Form.Funs) Module Form.Funs
val get_ty : 'a -> 'b -> Ty.tval eval : ID.t -> Value.t Sidekick_util.IArray.t -> Value.tval and_ : Fun.tval or_ : Fun.tval imply : Fun.t
\ No newline at end of file
+Funs (sidekick-base.Sidekick_base.Form.Funs) Module Form.Funs
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Form/index.html b/dev/sidekick-base/Sidekick_base/Form/index.html
index d781ff28..d5ee5c0b 100644
--- a/dev/sidekick-base/Sidekick_base/Form/index.html
+++ b/dev/sidekick-base/Sidekick_base/Form/index.html
@@ -1,10 +1,10 @@
Form (sidekick-base.Sidekick_base.Form) Module Sidekick_base.Form
Formulas (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.
module T = Base_types.Termmodule Ty = Base_types.Tymodule Fun = Base_types.Funmodule Value = Base_types.Valueval id_and : ID.tval id_or : ID.tval id_imply : ID.tval view_id :
ID.t ->
- 'a Sidekick_util.IArray.t ->
- ( 'a, 'a Sidekick_util.IArray.iter ) Sidekick_th_bool_static.bool_viewval view_as_bool :
+ 'a CCArray.t ->
+ ( 'a, 'a CCArray.iter ) Sidekick_th_bool_static.bool_viewval view_as_bool :
T.t ->
- ( T.t, T.t Sidekick_util.IArray.iter ) Sidekick_th_bool_static.bool_viewmodule Funs : sig ... endval as_id : ID.t -> T.t -> T.t Sidekick_util.IArray.t optionval and_a : T.store -> T.t Sidekick_util.IArray.t -> T.tval or_a : T.store -> T.t Sidekick_util.IArray.t -> T.tval imply_a : T.store -> T.t Sidekick_util.IArray.t -> T.t -> T.tval mk_bool :
+ ( T.t, T.t CCArray.iter ) Sidekick_th_bool_static.bool_viewmodule Funs : sig ... endval mk_bool :
T.store ->
- ( T.t, T.t Sidekick_util.IArray.t ) Sidekick_th_bool_static.bool_view ->
+ ( T.t, T.t array ) Sidekick_th_bool_static.bool_view ->
T.tmodule Gensym : sig ... end
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Proof/Step_vec/index.html b/dev/sidekick-base/Sidekick_base/Proof/Step_vec/index.html
index 98f2dfe0..fc7bb914 100644
--- a/dev/sidekick-base/Sidekick_base/Proof/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base/Proof/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base.Proof.Step_vec) Module Proof.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base.Proof.Step_vec) Module Proof.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Proof/index.html b/dev/sidekick-base/Sidekick_base/Proof/index.html
index bf518de4..32a8b81f 100644
--- a/dev/sidekick-base/Sidekick_base/Proof/index.html
+++ b/dev/sidekick-base/Sidekick_base/Proof/index.html
@@ -7,7 +7,7 @@
with type t := t
and type lit := lit
and type proof_step := proof_step
- and type proof_rule := proof_rulemodule Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
+ and type proof_rule := proof_rulemodule Step_vec : Sidekick_util.Vec_sig.BASE with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
proof_step ->
res:lit Iter.t ->
using:proof_step Iter.t ->
diff --git a/dev/sidekick-base/Sidekick_base/Proof_dummy/Step_vec/index.html b/dev/sidekick-base/Sidekick_base/Proof_dummy/Step_vec/index.html
index 5d4ddb95..b3dc2146 100644
--- a/dev/sidekick-base/Sidekick_base/Proof_dummy/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base/Proof_dummy/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base.Proof_dummy.Step_vec) Module Proof_dummy.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base.Proof_dummy.Step_vec) Module Proof_dummy.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html b/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html
index 4d116ac6..a14f133c 100644
--- a/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html
+++ b/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html
@@ -7,7 +7,7 @@
with type t := t
and type lit := lit
and type proof_step := proof_step
- and type proof_rule := t -> proof_stepmodule Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> t -> proof_stepEmit an input clause.
val emit_redundant_clause :
+ and type proof_rule := t -> proof_stepmodule Step_vec : Sidekick_util.Vec_sig.BASE with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> t -> proof_stepEmit an input clause.
val emit_redundant_clause :
lit Iter.t ->
hyps:proof_step Iter.t ->
t ->
diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/P/Step_vec/index.html
index 8e229b7e..c7c46e73 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Solver/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Solver/P/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base_solver.Solver.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = Solver_arg.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base_solver.Solver.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = Solver_arg.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/P/Step_vec/index.html
index 4a6b47d5..25e21f55 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/Actions/P/Step_vec/index.html
@@ -1,3 +1,3 @@
Step_vec (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.CC.Actions.P.Step_vec) Module P.Step_vec
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+ Sidekick_smt_solver.Make(Solver_arg).Solver_internal.CC.Actions.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/P/Step_vec/index.html
index 6b033925..a275d89b 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/CC/P/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.CC.P.Step_vec) Module P.Step_vec
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.CC.P.Step_vec) Module P.Step_vec
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/Step_vec/index.html
index 29b63c9d..96de6fad 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/index.html
index 2cefd49a..27bac1a2 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Solver/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Solver/index.html
@@ -13,7 +13,7 @@
T.Term.store ->
T.Ty.store ->
unit ->
- tval add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unitval add_clause_l : t -> lit list -> proof_step -> unittype res = Sidekick_smt_solver.Make(Solver_arg).res = | Sat of Model.t| Unsat of {unsat_core : unit -> lit Iter.t;unsat_proof_step : unit -> proof_step option;
}| Unknown of Unknown.t
val solve :
+ tval add_clause : t -> lit array -> proof_step -> unitval add_clause_l : t -> lit list -> proof_step -> unittype res = Sidekick_smt_solver.Make(Solver_arg).res = | Sat of Model.t| Unsat of {unsat_core : unit -> lit Iter.t;unsat_proof_step : unit -> proof_step option;
}| Unknown of Unknown.t
val solve :
?on_exit:( unit -> unit ) list ->
?check:bool ->
?on_progress:( t -> unit ) ->
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/Step_vec/index.html
index 7b7a5f38..6b10e910 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base_solver.Th_bool.A.S.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = Solver_arg.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base_solver.Th_bool.A.S.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = Solver_arg.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/P/Step_vec/index.html
index 378b2022..de0a8d5b 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/Actions/P/Step_vec/index.html
@@ -1,3 +1,3 @@
Step_vec (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.CC.Actions.P.Step_vec) Module P.Step_vec
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+ Sidekick_smt_solver.Make(Solver_arg).Solver_internal.CC.Actions.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/P/Step_vec/index.html
index b3f8b7c8..c8b67558 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/CC/P/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.CC.P.Step_vec) Module P.Step_vec
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.CC.P.Step_vec) Module P.Step_vec
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/Step_vec/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/Step_vec/index.html
index e02362a3..bd0e6857 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/Step_vec/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/Step_vec/index.html
@@ -1,2 +1,2 @@
-Step_vec (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
+Step_vec (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.P.Step_vec) Module P.Step_vec
type elt = proof_steptype t = P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html
index a5681066..22f674c7 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html
@@ -13,7 +13,7 @@
T.Term.store ->
T.Ty.store ->
unit ->
- tval add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unitval add_clause_l : t -> lit list -> proof_step -> unittype res = Sidekick_smt_solver.Make(Solver_arg).res = | Sat of Model.t| Unsat of {unsat_core : unit -> lit Iter.t;unsat_proof_step : unit -> proof_step option;
}| Unknown of Unknown.t
val solve :
+ tval add_clause : t -> lit array -> proof_step -> unitval add_clause_l : t -> lit list -> proof_step -> unittype res = Sidekick_smt_solver.Make(Solver_arg).res = | Sat of Model.t| Unsat of {unsat_core : unit -> lit Iter.t;unsat_proof_step : unit -> proof_step option;
}| Unknown of Unknown.t
val solve :
?on_exit:( unit -> unit ) list ->
?check:bool ->
?on_progress:( t -> unit ) ->
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/index.html
index 6b4d7cd0..cfce3e64 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/index.html
@@ -3,5 +3,5 @@
term ->
( term, term Iter.t ) Sidekick_th_bool_static.bool_viewval mk_bool :
S.T.Term.store ->
- ( term, term Sidekick_util.IArray.t ) Sidekick_th_bool_static.bool_view ->
+ ( term, term array ) Sidekick_th_bool_static.bool_view ->
termval lemma_bool_tauto : S.Lit.t Iter.t -> S.P.t -> S.P.proof_stepval lemma_bool_c : string -> S.T.Term.t list -> S.P.t -> S.P.proof_stepval lemma_bool_equiv : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_stepval lemma_ite_true : ite:S.T.Term.t -> S.P.t -> S.P.proof_stepval lemma_ite_false : ite:S.T.Term.t -> S.P.t -> S.P.proof_stepmodule Gensym : sig ... end