diff --git a/dev/sidekick-base/Sidekick_base/Solver/index.html b/dev/sidekick-base/Sidekick_base/Solver/index.html index a2f7ffda..36ea3665 100644 --- a/dev/sidekick-base/Sidekick_base/Solver/index.html +++ b/dev/sidekick-base/Sidekick_base/Solver/index.html @@ -8,12 +8,11 @@ ?push_level:( 'th -> unit ) -> ?pop_levels:( 'th -> int -> unit ) -> unit -> - Sidekick_smt_solver.Theory.t

Helper to create a theory.

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> Sidekick_smt_solver.Sigs.Term.store
val proof : t -> Sidekick_smt_solver.Sigs.proof_trace
val create : + Sidekick_smt_solver.Theory.t

Helper to create a theory.

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> Sidekick_smt_solver.Sigs.Term.store
val tracer : t -> Sidekick_smt_solver.Tracer.t
val create : (module Sidekick_smt_solver.Sigs.ARG) -> ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> - ?tracer:Sidekick_smt_solver.Tracer.t -> - proof:Sidekick_smt_solver.Sigs.proof_trace -> + tracer:Sidekick_smt_solver.Tracer.t -> theories:Sidekick_smt_solver.Theory.t list -> Sidekick_smt_solver.Sigs.Term.store -> unit -> @@ -24,12 +23,12 @@ Sidekick_smt_solver.Sigs.lit

mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.

The proof of |- lit = lit' is directly added to the solver's proof.

val add_clause : t -> Sidekick_smt_solver.Sigs.lit array -> - Sidekick_smt_solver.Sigs.step_id -> + Sidekick_smt_solver.Sigs.Proof.Pterm.delayed -> unit

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

val add_clause_l : t -> Sidekick_smt_solver.Sigs.lit list -> - Sidekick_smt_solver.Sigs.step_id -> - unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sidekick_smt_solver.Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sidekick_smt_solver.Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sidekick_smt_solver.Sigs.ty -> unit
type res = Check_res.t =
| Sat of Sidekick_smt_solver.Sigs.Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sidekick_smt_solver.Sigs.lit Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_step_id : unit -> Sidekick_smt_solver.Sigs.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : + Sidekick_smt_solver.Sigs.Proof.Pterm.delayed -> + unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sidekick_smt_solver.Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sidekick_smt_solver.Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sidekick_smt_solver.Sigs.ty -> unit
type res = Check_res.t =
| Sat of Sidekick_smt_solver.Sigs.Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sidekick_smt_solver.Sigs.lit Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sidekick_smt_solver.Sigs.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> @@ -41,8 +40,7 @@ propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

val default_arg : (module Sidekick_smt_solver.Sigs.ARG)
val create_default : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Small | `Tiny ] -> - ?tracer:Sidekick_smt_solver.Tracer.t -> - proof:Sidekick_smt_solver.Sigs.proof_trace -> + tracer:Sidekick_smt_solver.Tracer.t -> theories:Sidekick_smt_solver.Theory.t list -> Sidekick_smt_solver.Sigs.Term.store -> t
\ 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 e994c650..3d324b9d 100644 --- a/dev/sidekick-base/Sidekick_base/Term/index.html +++ b/dev/sidekick-base/Sidekick_base/Term/index.html @@ -8,7 +8,7 @@ n3: g n2 n1 n4: = n3 n3
val iter_shallow : f:( bool -> t -> unit ) -> t -> unit

iter_shallow f e iterates on immediate subterms of e, calling f trdb e' for each subterm e', with trdb = true iff e' is directly under a binder.

val map_shallow : store -> f:( bool -> t -> t ) -> t -> t
val exists_shallow : f:( bool -> t -> bool ) -> t -> bool
val for_all_shallow : f:( bool -> t -> bool ) -> t -> bool
val contains : t -> sub:t -> bool
val free_vars_iter : t -> var Iter.t
val free_vars : ?init:Sidekick_core_logic__.Var.Set.t -> t -> - Sidekick_core_logic__.Var.Set.t
val is_type : t -> bool

is_type t is true iff view t is Type _

val is_a_type : t -> bool

is_a_type t is true if is_ty (ty t)

val is_closed : t -> bool

Is the term closed (all bound variables are paired with a binder)? time: O(1)

val has_fvars : t -> bool

Does the term contain free variables? time: O(1)

val ty : t -> t

Return the type of this term.

Creation

module Store = Sidekick_core.Term.Store
val type_ : store -> t
val type_of_univ : store -> int -> t
val var : store -> var -> t
val var_str : store -> string -> ty:t -> t
val bvar : store -> bvar -> t
val bvar_i : store -> int -> ty:t -> t
val const : store -> Sidekick_core_logic__Types_.const -> t
val app : store -> t -> t -> t
val app_l : store -> t -> t list -> t
val app_fold : store -> f:t -> acc0:t -> t list -> t
val lam : store -> var -> t -> t
val pi : store -> var -> t -> t
val arrow : store -> t -> t -> t
val arrow_l : store -> t list -> t -> t
val open_lambda : store -> t -> (var * t) option
val open_lambda_exn : store -> t -> var * t
module DB = Sidekick_core.Term.DB

De bruijn indices

include module type of struct include Sidekick_core_logic.T_builtins end
type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val bool_val : + Sidekick_core_logic__.Var.Set.t
val is_type : t -> bool

is_type t is true iff view t is Type _

val is_a_type : t -> bool

is_a_type t is true if is_ty (ty t)

val is_closed : t -> bool

Is the term closed (all bound variables are paired with a binder)? time: O(1)

val has_fvars : t -> bool

Does the term contain free variables? time: O(1)

val ty : t -> t

Return the type of this term.

Creation

val type_ : store -> t
val type_of_univ : store -> int -> t
val var : store -> var -> t
val var_str : store -> string -> ty:t -> t
val bvar : store -> bvar -> t
val bvar_i : store -> int -> ty:t -> t
val const : store -> Sidekick_core_logic__Types_.const -> t
val app : store -> t -> t -> t
val app_l : store -> t -> t list -> t
val app_fold : store -> f:t -> acc0:t -> t list -> t
val lam : store -> var -> t -> t
val pi : store -> var -> t -> t
val arrow : store -> t -> t -> t
val arrow_l : store -> t list -> t -> t
val open_lambda : store -> t -> (var * t) option
val open_lambda_exn : store -> t -> var * t

De bruijn indices

include module type of struct include Sidekick_core_logic.T_builtins end
type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
| C_proof
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val eq : @@ -32,7 +32,7 @@ n4: = n3 n3
term Sidekick_util.Fmt.printer -> Sidekick_util.Fmt.t -> term -> - bool

Printing hook, responsible for printing certain subterms

val default_hooks : Hooks.t Stdlib.ref
val pp_with : Hooks.t -> term Sidekick_util.Fmt.printer

Print using the hooks

val pp : term Sidekick_util.Fmt.printer

Print using default_hooks

module Tracer = Sidekick_core.Term.Tracer
module Trace_reader = Sidekick_core.Term.Trace_reader
val view_as_cc : + bool

Printing hook, responsible for printing certain subterms

module Hooks = Sidekick_core.Term.Hooks
val default_hooks : Hooks.t Stdlib.ref
val pp_with : Hooks.t -> term Sidekick_util.Fmt.printer

Print using the hooks

val pp : term Sidekick_util.Fmt.printer

Print using default_hooks

val pp_limit : max_depth:int -> max_nodes:int -> term Sidekick_util.Fmt.printer

Print with a limit on the number of nodes printed. An ellipsis is displayed otherwise.

module Tracer = Sidekick_core.Term.Tracer
module Trace_reader = Sidekick_core.Term.Trace_reader
module Ref = Sidekick_core.Term.Ref
val view_as_cc : Sidekick_core_logic.Term.t -> ( Sidekick_core_logic.Const.t, Sidekick_core_logic.Term.t, diff --git a/dev/sidekick-base/Sidekick_base/Ty/index.html b/dev/sidekick-base/Sidekick_base/Ty/index.html index 23e03ef6..2c1f93d1 100644 --- a/dev/sidekick-base/Sidekick_base/Ty/index.html +++ b/dev/sidekick-base/Sidekick_base/Ty/index.html @@ -83,7 +83,7 @@ n4: = n3 n3
var * Sidekick_core_logic__Types_.term) option
val open_lambda_exn : store -> Sidekick_core_logic__Types_.term -> - var * Sidekick_core_logic__Types_.term
module DB = Sidekick_core.Term.DB

De bruijn indices

include module type of struct include Sidekick_core_logic.T_builtins end
type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val bool_val : + var * Sidekick_core_logic__Types_.term

De bruijn indices

include module type of struct include Sidekick_core_logic.T_builtins end
type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
| C_proof
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val eq : @@ -107,4 +107,4 @@ n4: = n3 n3
term Sidekick_util.Fmt.printer -> Sidekick_util.Fmt.t -> term -> - bool

Printing hook, responsible for printing certain subterms

val default_hooks : Hooks.t Stdlib.ref
val pp_with : Hooks.t -> term Sidekick_util.Fmt.printer

Print using the hooks

module Tracer = Sidekick_core.Term.Tracer
module Trace_reader = Sidekick_core.Term.Trace_reader
type t = Types_.ty
type data = Types_.data
include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.ORD with type t := t
val compare : t -> t -> int
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val const_decoders : Types_.Const.decoders
val bool : store -> t
val real : store -> t
val int : store -> t
val uninterpreted : store -> ID.t -> t
val uninterpreted_str : store -> string -> t
val is_uninterpreted : t -> bool
val is_real : t -> bool
val is_int : t -> bool
\ No newline at end of file + bool

Printing hook, responsible for printing certain subterms

module Hooks = Sidekick_core.Term.Hooks
val default_hooks : Hooks.t Stdlib.ref
val pp_with : Hooks.t -> term Sidekick_util.Fmt.printer

Print using the hooks

val pp_limit : max_depth:int -> max_nodes:int -> term Sidekick_util.Fmt.printer

Print with a limit on the number of nodes printed. An ellipsis is displayed otherwise.

module Tracer = Sidekick_core.Term.Tracer
module Trace_reader = Sidekick_core.Term.Trace_reader
module Ref = Sidekick_core.Term.Ref
type t = Types_.ty
type data = Types_.data
include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.ORD with type t := t
val compare : t -> t -> int
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val const_decoders : Types_.Const.decoders
val bool : store -> t
val real : store -> t
val int : store -> t
val uninterpreted : store -> ID.t -> t
val uninterpreted_str : store -> string -> t
val is_uninterpreted : t -> bool
val is_real : t -> bool
val is_int : t -> bool
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Types_/index.html b/dev/sidekick-base/Sidekick_base/Types_/index.html index a69bcbb9..dda6913c 100644 --- a/dev/sidekick-base/Sidekick_base/Types_/index.html +++ b/dev/sidekick-base/Sidekick_base/Types_/index.html @@ -1,2 +1,7 @@ -Types_ (sidekick-base.Sidekick_base.Types_)

Module Sidekick_base.Types_

include module type of struct include Sidekick_core end
module Fmt = Sidekick_core.Fmt

Re-exports from core-logic

module Const = Sidekick_core.Const
module Term = Sidekick_core.Term
module Gensym = Sidekick_core.Gensym

view

module Bool_view = Sidekick_core.Bool_view
module CC_view = Sidekick_core.CC_view
module Default_cc_view = Sidekick_core.Default_cc_view

Main modules

module Bvar = Sidekick_core.Bvar
module Lit = Sidekick_core.Lit
module Proof_step = Sidekick_core.Proof_step
module Proof_core = Sidekick_core.Proof_core
module Proof_sat = Sidekick_core.Proof_sat
module Proof_trace = Sidekick_core.Proof_trace
module Proof_term = Sidekick_core.Proof_term
module Subst = Sidekick_core.Subst
module Var = Sidekick_core.Var
module Box = Sidekick_core.Box
module Clause_tracer = Sidekick_core.Clause_tracer
exception Resource_exhausted
type term = Term.t
type ty = Term.t
type value = Term.t
type uconst = {
uc_id : ID.t;
uc_ty : ty;
}

Uninterpreted constant.

type ty_view =
| Ty_int
| Ty_real
| Ty_uninterpreted of {
id : ID.t;
mutable finite : bool;
}
and data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : ID.t;
cstor_is_a : ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
and select = {
select_id : ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
type definition = ID.t * ty * term
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
\ No newline at end of file +Types_ (sidekick-base.Sidekick_base.Types_)

Module Sidekick_base.Types_

include module type of struct include Sidekick_core end
module Fmt = Sidekick_core.Fmt

Re-exports from core-logic

module Const = Sidekick_core.Const
module Str_const = Sidekick_core.Str_const
module Term = Sidekick_core.Term

view

module Bool_view = Sidekick_core.Bool_view
module CC_view = Sidekick_core.CC_view
module Default_cc_view = Sidekick_core.Default_cc_view

Main modules

module Bvar = Sidekick_core.Bvar
module Lit = Sidekick_core.Lit
module Subst = Sidekick_core.Subst
module Var = Sidekick_core.Var
module Box = Sidekick_core.Box
module Gensym = Sidekick_core.Gensym
exception Resource_exhausted

Const decoders for traces

val const_decoders : + (string + * Sidekick_core_logic.Const.Ops.t + * ( Sidekick_core_logic__Types_.term Sidekick_util.Ser_decode.t -> + Sidekick_core_logic.Const.view Sidekick_util.Ser_decode.t )) + list
type term = Term.t
type ty = Term.t
type value = Term.t
type uconst = {
uc_id : ID.t;
uc_ty : ty;
}

Uninterpreted constant.

type ty_view =
| Ty_int
| Ty_real
| Ty_uninterpreted of {
id : ID.t;
mutable finite : bool;
}
and data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : ID.t;
cstor_is_a : ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
and select = {
select_id : ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
type definition = ID.t * ty * term
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
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Decode/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Decode/index.html deleted file mode 100644 index ea8cb993..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Decode/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Decode (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.Decode)

Module Bare.Decode

type t = input
val of_input : input -> t
val of_bytes : ?off:int -> ?len:int -> bytes -> t
val of_string : ?off:int -> ?len:int -> string -> t
type 'a dec = t -> 'a
val uint : t -> int64
val int : t -> int64
val i8 : t -> char
val u8 : t -> char
val i16 : t -> int
val u16 : t -> int
val i32 : t -> int32
val u32 : t -> int32
val i64 : t -> int64
val u64 : t -> int64
val bool : t -> bool
val f32 : t -> float
val f64 : t -> float
val data_of : size:int -> t -> bytes
val data : t -> bytes
val string : t -> string
val optional : ( t -> 'a ) -> t -> 'a option
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Encode/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Encode/index.html deleted file mode 100644 index f0b04df9..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Encode/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Encode (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.Encode)

Module Bare.Encode

type t = output
val of_output : output -> t
val of_buffer : Stdlib.Buffer.t -> t
type 'a enc = t -> 'a -> unit
val unsafe_chr : int -> char
val uint : t -> int64 -> unit
val int : t -> int64 -> unit
val i8 : t -> char -> unit
val u8 : t -> char -> unit
val i16 : t -> int -> unit
val u16 : t -> int -> unit
val i32 : t -> int32 -> unit
val u32 : t -> int32 -> unit
val i64 : t -> int64 -> unit
val u64 : t -> int64 -> unit
val bool : t -> bool -> unit
val f64 : t -> float -> unit
val data_of : size:int -> t -> bytes -> unit
val data : t -> bytes -> unit
val string : t -> string -> unit
val optional : ( t -> 'a -> unit ) -> t -> 'a option -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Pp/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Pp/index.html deleted file mode 100644 index 94a6eef9..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/Pp/index.html +++ /dev/null @@ -1,18 +0,0 @@ - -Pp (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.Pp)

Module Bare.Pp

type 'a t = Stdlib.Format.formatter -> 'a -> unit
type 'a iter = ( 'a -> unit ) -> unit
val unit : Stdlib.Format.formatter -> unit -> unit
val int8 : Stdlib.Format.formatter -> char -> unit
val int : Stdlib.Format.formatter -> int -> unit
val int32 : Stdlib.Format.formatter -> int32 -> unit
val int64 : Stdlib.Format.formatter -> int64 -> unit
val float : Stdlib.Format.formatter -> float -> unit
val bool : Stdlib.Format.formatter -> bool -> unit
val string : Stdlib.Format.formatter -> string -> unit
val data : Stdlib.Format.formatter -> bytes -> unit
val option : - ( Stdlib.Format.formatter -> 'a -> unit ) -> - Stdlib.Format.formatter -> - 'a option -> - unit
val array : - ( Stdlib.Format.formatter -> 'a -> unit ) -> - Stdlib.Format.formatter -> - 'a array -> - unit
val iter : - ( Stdlib.Format.formatter -> 'a -> 'b ) -> - Stdlib.Format.formatter -> - ( ( 'a -> 'b ) -> unit ) -> - unit
val list : - ( Stdlib.Format.formatter -> 'a -> unit ) -> - Stdlib.Format.formatter -> - 'a list -> - unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/String_map/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/String_map/index.html deleted file mode 100644 index dfaa8d8f..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/String_map/index.html +++ /dev/null @@ -1,6 +0,0 @@ - -String_map (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.String_map)

Module Bare.String_map

type key = Stdlib.String.t
type !'a t = 'a Stdlib__map.Make(Stdlib.String).t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val update : key -> ( 'a option -> 'a option ) -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge : - ( key -> 'a option -> 'b option -> 'c option ) -> - 'a t -> - 'b t -> - 'c t
val union : ( key -> 'a -> 'a -> 'a option ) -> 'a t -> 'a t -> 'a t
val compare : ( 'a -> 'a -> int ) -> 'a t -> 'a t -> int
val equal : ( 'a -> 'a -> bool ) -> 'a t -> 'a t -> bool
val iter : ( key -> 'a -> unit ) -> 'a t -> unit
val fold : ( key -> 'a -> 'b -> 'b ) -> 'a t -> 'b -> 'b
val for_all : ( key -> 'a -> bool ) -> 'a t -> bool
val exists : ( key -> 'a -> bool ) -> 'a t -> bool
val filter : ( key -> 'a -> bool ) -> 'a t -> 'a t
val filter_map : ( key -> 'a -> 'b option ) -> 'a t -> 'b t
val partition : ( key -> 'a -> bool ) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val min_binding_opt : 'a t -> (key * 'a) option
val max_binding : 'a t -> key * 'a
val max_binding_opt : 'a t -> (key * 'a) option
val choose : 'a t -> key * 'a
val choose_opt : 'a t -> (key * 'a) option
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val find_opt : key -> 'a t -> 'a option
val find_first : ( key -> bool ) -> 'a t -> key * 'a
val find_first_opt : ( key -> bool ) -> 'a t -> (key * 'a) option
val find_last : ( key -> bool ) -> 'a t -> key * 'a
val find_last_opt : ( key -> bool ) -> 'a t -> (key * 'a) option
val map : ( 'a -> 'b ) -> 'a t -> 'b t
val mapi : ( key -> 'a -> 'b ) -> 'a t -> 'b t
val to_seq : 'a t -> (key * 'a) Stdlib.Seq.t
val to_rev_seq : 'a t -> (key * 'a) Stdlib.Seq.t
val to_seq_from : key -> 'a t -> (key * 'a) Stdlib.Seq.t
val add_seq : (key * 'a) Stdlib.Seq.t -> 'a t -> 'a t
val of_seq : (key * 'a) Stdlib.Seq.t -> 'a t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/index.html deleted file mode 100644 index bba5942c..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/index.html +++ /dev/null @@ -1,12 +0,0 @@ - -Bare (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare)

Module Proof_ser.Bare

module String_map : sig ... end
module type INPUT = sig ... end
type input = (module INPUT)
val input_of_bytes : ?off:int -> ?len:int -> bytes -> input
module Decode : sig ... end
module type OUTPUT = sig ... end
type output = (module OUTPUT)
val output_of_buffer : Stdlib.Buffer.t -> output
module Encode : sig ... end
module Pp : sig ... end
val to_string : 'a Encode.enc -> 'a -> string
val of_bytes_exn : ?off:int -> ?len:int -> ( Decode.t -> 'a ) -> bytes -> 'a
val of_bytes : - ?off:int -> - ?len:int -> - ( Decode.t -> 'a ) -> - bytes -> - ( 'a, string ) Stdlib.result
val of_string_exn : ?off:int -> ?len:int -> ( Decode.t -> 'a ) -> string -> 'a
val of_string : - ?off:int -> - ?len:int -> - ( Decode.t -> 'a ) -> - string -> - ( 'a, string ) Stdlib.result
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-INPUT/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-INPUT/index.html deleted file mode 100644 index 1c5873c8..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-INPUT/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -INPUT (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.INPUT)

Module type Bare.INPUT

val read_byte : unit -> char
val read_i16 : unit -> int
val read_i32 : unit -> int32
val read_i64 : unit -> int64
val read_exact : bytes -> int -> int -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-OUTPUT/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-OUTPUT/index.html deleted file mode 100644 index 62654e89..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Bare/module-type-OUTPUT/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -OUTPUT (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Bare.OUTPUT)

Module type Bare.OUTPUT

val write_byte : char -> unit
val write_i16 : int -> unit
val write_i32 : int32 -> unit
val write_i64 : int64 -> unit
val write_exact : bytes -> int -> int -> unit
val flush : unit -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Clause/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Clause/index.html deleted file mode 100644 index d906fb6f..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Clause/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Clause (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Clause)

Module Proof_ser.Clause

type t = {
lits : Lit.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_app/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_app/index.html deleted file mode 100644 index 23844231..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_app/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Expr_app (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_app)

Module Proof_ser.Expr_app

type t = {
f : ID.t;
args : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_bool/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_bool/index.html deleted file mode 100644 index 52ee4a09..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_bool/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Expr_bool (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_bool)

Module Proof_ser.Expr_bool

type t = {
b : bool;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_def/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_def/index.html deleted file mode 100644 index 6f0a16a5..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_def/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Expr_def (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_def)

Module Proof_ser.Expr_def

type t = {
c : ID.t;
rhs : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_eq/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_eq/index.html deleted file mode 100644 index 46eebe14..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_eq/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Expr_eq (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_eq)

Module Proof_ser.Expr_eq

type t = {
lhs : ID.t;
rhs : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_if/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_if/index.html deleted file mode 100644 index d4381d18..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_if/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Expr_if (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_if)

Module Proof_ser.Expr_if

type t = {
cond : ID.t;
then_ : ID.t;
else_ : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html deleted file mode 100644 index 02fc6d10..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_isa/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Expr_isa (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_isa)

Module Proof_ser.Expr_isa

type t = {
c : ID.t;
arg : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_not/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_not/index.html deleted file mode 100644 index cd50f536..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Expr_not/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Expr_not (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Expr_not)

Module Proof_ser.Expr_not

type t = {
f : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Fun_decl/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Fun_decl/index.html deleted file mode 100644 index a9f9e0b6..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Fun_decl/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Fun_decl (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Fun_decl)

Module Proof_ser.Fun_decl

type t = {
f : string;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/ID/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/ID/index.html deleted file mode 100644 index 4a6ded27..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/ID/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -ID (sidekick-base.Sidekick_base_proof_trace.Proof_ser.ID)

Module Proof_ser.ID

type t = int32
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Lit/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Lit/index.html deleted file mode 100644 index 093edee4..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Lit/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Lit (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Lit)

Module Proof_ser.Lit

type t = ID.t
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step/index.html deleted file mode 100644 index 8f8b8b9c..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step)

Module Proof_ser.Step

type t = {
id : ID.t;
view : Step_view.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_c/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_c/index.html deleted file mode 100644 index e8ca4753..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_c/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_bool_c (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bool_c)

Module Proof_ser.Step_bool_c

type t = {
rule : string;
exprs : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_tauto/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_tauto/index.html deleted file mode 100644 index 3ff2f1eb..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bool_tauto/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_bool_tauto (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bool_tauto)

Module Proof_ser.Step_bool_tauto

type t = {
lits : Lit.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bridge_lit_expr/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bridge_lit_expr/index.html deleted file mode 100644 index 570d441e..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_bridge_lit_expr/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_bridge_lit_expr (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_bridge_lit_expr)

Module Proof_ser.Step_bridge_lit_expr

type t = {
lit : Lit.t;
expr : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_cc/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_cc/index.html deleted file mode 100644 index e1ca30db..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_cc/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_cc (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_cc)

Module Proof_ser.Step_cc

type t = {
eqns : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_clause_rw/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_clause_rw/index.html deleted file mode 100644 index dbb239ed..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_clause_rw/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_clause_rw (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_clause_rw)

Module Proof_ser.Step_clause_rw

type t = {
c : ID.t;
res : Clause.t;
using : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_input/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_input/index.html deleted file mode 100644 index 02ddc4ba..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_input/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_input (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_input)

Module Proof_ser.Step_input

type t = {
c : Clause.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_preprocess/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_preprocess/index.html deleted file mode 100644 index 708e3ba9..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_preprocess/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_preprocess (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_preprocess)

Module Proof_ser.Step_preprocess

type t = {
t : ID.t;
u : ID.t;
using : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_p1/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_p1/index.html deleted file mode 100644 index 8d97f9e8..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_p1/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_proof_p1 (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_p1)

Module Proof_ser.Step_proof_p1

type t = {
rw_with : ID.t;
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html deleted file mode 100644 index a3a1adc9..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_proof_r1 (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_r1)

Module Proof_ser.Step_proof_r1

type t = {
unit : ID.t;
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_res/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_res/index.html deleted file mode 100644 index 64c2b8d0..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_res/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_proof_res (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_res)

Module Proof_ser.Step_proof_res

type t = {
pivot : ID.t;
c1 : ID.t;
c2 : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_rup/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_rup/index.html deleted file mode 100644 index 02d2782b..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_rup/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_rup (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_rup)

Module Proof_ser.Step_rup

type t = {
res : Clause.t;
hyps : ID.t array;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_true/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_true/index.html deleted file mode 100644 index 59d8b7be..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_true/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_true (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_true)

Module Proof_ser.Step_true

type t = {
true_ : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_unsat/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_unsat/index.html deleted file mode 100644 index 9452c96c..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_unsat/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_unsat (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_unsat)

Module Proof_ser.Step_unsat

type t = {
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html deleted file mode 100644 index 535c25aa..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_view (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_view)

Module Proof_ser.Step_view

type t =
| Step_input of Step_input.t
| Step_unsat of Step_unsat.t
| Step_rup of Step_rup.t
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Step_clause_rw of Step_clause_rw.t
| Step_bool_tauto of Step_bool_tauto.t
| Step_bool_c of Step_bool_c.t
| Step_proof_p1 of Step_proof_p1.t
| Step_proof_r1 of Step_proof_r1.t
| Step_proof_res of Step_proof_res.t
| Step_true of Step_true.t
| Fun_decl of Fun_decl.t
| Expr_def of Expr_def.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
| Expr_isa of Expr_isa.t
| Expr_eq of Expr_eq.t
| Expr_app of Expr_app.t
val decode : Bare.Decode.t -> t
  • raises Invalid_argument

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html deleted file mode 100644 index b222aa9e..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Proof_ser (sidekick-base.Sidekick_base_proof_trace.Proof_ser)

Module Sidekick_base_proof_trace.Proof_ser

module Bare : sig ... end
module ID : sig ... end
module Lit : sig ... end
module Clause : sig ... end
module Step_input : sig ... end
module Step_rup : sig ... end
module Step_bridge_lit_expr : sig ... end
module Step_cc : sig ... end
module Step_preprocess : sig ... end
module Step_clause_rw : sig ... end
module Step_unsat : sig ... end
module Step_proof_p1 : sig ... end
module Step_proof_r1 : sig ... end
module Step_proof_res : sig ... end
module Step_bool_tauto : sig ... end
module Step_bool_c : sig ... end
module Step_true : sig ... end
module Fun_decl : sig ... end
module Expr_def : sig ... end
module Expr_bool : sig ... end
module Expr_if : sig ... end
module Expr_not : sig ... end
module Expr_eq : sig ... end
module Expr_app : sig ... end
module Expr_isa : sig ... end
module Step_view : sig ... end
module Step : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Storage/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Storage/index.html deleted file mode 100644 index 9db80b2d..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Storage/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Storage (sidekick-base.Sidekick_base_proof_trace.Storage)

Module Sidekick_base_proof_trace.Storage

type t =
| No_store
| In_memory of Sidekick_util.Chunk_stack.Buf.t
| On_disk of string * Stdlib.out_channel
val pp : Stdlib.Format.formatter -> t -> unit
val iter_steps_backward : t -> Proof_ser.Step.t Iter.t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/index.html deleted file mode 100644 index cb49e134..00000000 --- a/dev/sidekick-base/Sidekick_base_proof_trace/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Sidekick_base_proof_trace (sidekick-base.Sidekick_base_proof_trace)

Module Sidekick_base_proof_trace

Proof trace with serialization

This library is useful to serialize a series of reasoning steps in memory or into a file, to be able to reconstruct a proper proof later.

module Proof_ser : sig ... end
module Storage : sig ... end
val iter_steps_backward : Storage.t -> Proof_ser.Step.t Iter.t
\ 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 ee291fe1..ef84c85d 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.

type 'a or_error = ( 'a, string ) CCResult.t
module Term = Sidekick_base.Term
module Driver : sig ... end

Driver.

module Solver : sig ... end
module Proof_trace = Sidekick_core.Proof_trace
module Check_cc : sig ... end
val parse : Term.store -> string -> Stmt.t list or_error
val 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.

type 'a or_error = ( 'a, string ) CCResult.t
module Term = Sidekick_base.Term
module Driver : sig ... end

Driver.

module Solver : sig ... end
module Check_cc : sig ... end
val parse : Term.store -> string -> Stmt.t list or_error
val 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 cb51efa1..e14e6922 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.proof-trace

The entry point of this library is the module: Sidekick_base_proof_trace.

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/Sidekick_abstract_solver/Asolver/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html index adf78554..5ffefa8f 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,11 +1,9 @@ -t (sidekick.Sidekick_abstract_solver.Asolver.t)

Class type Asolver.t

method assert_term : Sidekick_core.Term.t -> unit

Helper 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 -> - Sidekick_core.Proof_step.id -> - unit

add_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 -> - Sidekick_core.Proof_step.id -> +t (sidekick.Sidekick_abstract_solver.Asolver.t)

Class type Asolver.t

method assert_term : Sidekick_core.Term.t -> unit

Helper 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 -> unit

add_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 -> unit

Add a clause to the solver, given as a list.

method add_ty : ty:Sidekick_core.Term.t -> unit

Add a new sort/atomic type.

method lit_of_term : ?sign:bool -> Sidekick_core.Term.t -> Sidekick_core.Lit.t

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> assumptions:Sidekick_core.Lit.t list -> unit -> - Check_res.t

Checks the satisfiability of the clauses added so far to the solver.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_progress

    called regularly during solving.

  • parameter should_stop

    a callback regularly called from within the solver. It is given a number of "steps" done since last call. The exact notion of step is not defined, but is guaranteed to increase regularly. The function should return true if it judges solving must stop (returning Unknown), false if solving can proceed.

  • parameter on_exit

    functions to be run before this returns

method last_res : Check_res.t option

Returns the result of the last call to solve, if the logic statee has not changed (mostly by asserting new clauses).

TODO: remove, use Tracer instead

\ No newline at end of file + Check_res.t

Checks the satisfiability of the clauses added so far to the solver.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_progress

    called regularly during solving.

  • parameter should_stop

    a callback regularly called from within the solver. It is given a number of "steps" done since last call. The exact notion of step is not defined, but is guaranteed to increase regularly. The function should return true if it judges solving must stop (returning Unknown), false if solving can proceed.

  • parameter on_exit

    functions to be run before this returns

method last_res : Check_res.t option

Returns the result of the last call to solve, if the logic statee has not changed (mostly by asserting new clauses).

method proof_tracer : Proof.Tracer.t

TODO: remove, use Tracer instead

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html index 408bddec..51b556fc 100644 --- a/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html +++ b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html @@ -1,12 +1,12 @@ -Asolver (sidekick.Sidekick_abstract_solver.Asolver)

Module Sidekick_abstract_solver.Asolver

Abstract interface for a solver

module Unknown = Unknown
module Check_res = Check_res
class type t = object ... end
val assert_term : t -> Sidekick_core.Term.t -> unit
val assert_clause : +Asolver (sidekick.Sidekick_abstract_solver.Asolver)

Module Sidekick_abstract_solver.Asolver

Abstract interface for a solver

module Unknown = Unknown
module Check_res = Check_res
module Proof = Sidekick_proof
class type t = object ... end
val assert_term : t -> Sidekick_core.Term.t -> unit
val assert_clause : t -> Sidekick_core.Lit.t array -> - Sidekick_core.Proof_step.id -> + Proof.Pterm.delayed -> unit
val assert_clause_l : t -> Sidekick_core.Lit.t list -> - Sidekick_core.Proof_step.id -> + Proof.Pterm.delayed -> unit
val add_ty : t -> ty:Sidekick_core.Term.t -> unit
val lit_of_term : t -> ?sign:bool -> @@ -18,4 +18,4 @@ ?should_stop:( int -> bool ) -> assumptions:Sidekick_core.Lit.t list -> unit -> - Check_res.t
val last_res : t -> Check_res.t option
\ No newline at end of file + Check_res.t
val last_res : t -> Check_res.t option
val proof : t -> Proof.Tracer.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html b/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html index 445e990e..37f7a5d2 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

module Model = Sidekick_model
type t =
| Sat of Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sidekick_core.Lit.t Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_step_id : unit -> Sidekick_core.Proof_trace.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| 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

module Model = Sidekick_model
type t =
| Sat of Model.t(*

Satisfiable

*)
| Unsat of {
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

*)
| 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/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html index e4b37f32..88dc667f 100644 --- a/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html +++ b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html @@ -1,11 +1,11 @@ t (sidekick.Sidekick_abstract_solver.t)

Class type Sidekick_abstract_solver.t

Main abstract solver type

method assert_term : Sidekick_core.Term.t -> unit

Helper 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 -> - Sidekick_core.Proof_step.id -> + Asolver.Proof.Pterm.delayed -> unit

add_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 -> - Sidekick_core.Proof_step.id -> + Asolver.Proof.Pterm.delayed -> unit

Add a clause to the solver, given as a list.

method add_ty : ty:Sidekick_core.Term.t -> unit

Add a new sort/atomic type.

method lit_of_term : ?sign:bool -> Sidekick_core.Term.t -> Sidekick_core.Lit.t

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> assumptions:Sidekick_core.Lit.t list -> unit -> - Asolver.Check_res.t

Checks the satisfiability of the clauses added so far to the solver.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_progress

    called regularly during solving.

  • parameter should_stop

    a callback regularly called from within the solver. It is given a number of "steps" done since last call. The exact notion of step is not defined, but is guaranteed to increase regularly. The function should return true if it judges solving must stop (returning Unknown), false if solving can proceed.

  • parameter on_exit

    functions to be run before this returns

method last_res : Asolver.Check_res.t option

Returns the result of the last call to solve, if the logic statee has not changed (mostly by asserting new clauses).

TODO: remove, use Tracer instead

\ No newline at end of file + Asolver.Check_res.t

Checks the satisfiability of the clauses added so far to the solver.

method last_res : Asolver.Check_res.t option

Returns the result of the last call to solve, if the logic statee has not changed (mostly by asserting new clauses).

method proof_tracer : Asolver.Proof.Tracer.t

TODO: remove, use Tracer instead

\ 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 cac58ab2..c5083e34 100644 --- a/dev/sidekick/Sidekick_cc/CC/Make/index.html +++ b/dev/sidekick/Sidekick_cc/CC/Make/index.html @@ -3,5 +3,5 @@ ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Create a new congruence closure.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/CC/Result_action/index.html b/dev/sidekick/Sidekick_cc/CC/Result_action/index.html index 316fbaf0..d39bf5ad 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_core.Proof_term.step_id(*

raise_conflict (c,pr) declares that c is a tautology of the theory of congruence.

  • parameter pr

    the proof of c being a tautology

*)
type or_conflict = ( t list, conflict ) Stdlib.result
\ 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.

  • parameter pr

    the proof of c being a tautology

*)
type or_conflict = ( t list, conflict ) Stdlib.result
\ 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 8ea6d942..1b5ba63a 100644 --- a/dev/sidekick/Sidekick_cc/CC/index.html +++ b/dev/sidekick/Sidekick_cc/CC/index.html @@ -1,7 +1,7 @@ -CC (sidekick.Sidekick_cc.CC)

Module Sidekick_cc.CC

Main congruence closure type.

type e_node = E_node.t

A node of the congruence closure

type repr = E_node.t

Node that is currently a representative.

type explanation = Expl.t
type bitfield

A 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.

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 t

The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.

Accessors

val term_store : t -> Sidekick_core.Term.store
val stat : t -> Sidekick_util.Stat.t
val find : t -> e_node -> repr

Current representative

val add_term : t -> Sidekick_core.Term.t -> e_node

Add the Term.t to the congruence closure, if not present already. Will be backtracked.

val mem_term : t -> Sidekick_core.Term.t -> bool

Returns true if the Term.t is explicitly present in the congruence closure

val allocate_bitfield : t -> descr:string -> bitfield

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).

val get_bitfield : t -> bitfield -> E_node.t -> bool

Access the bit field of the given e_node

val set_bitfield : t -> bitfield -> bool -> E_node.t -> unit

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.t

A node of the congruence closure

type repr = E_node.t

Node that is currently a representative.

type explanation = Expl.t
type bitfield

A 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

The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.

Accessors

val term_store : t -> Sidekick_core.Term.store
val proof_tracer : t -> Sidekick_proof.Tracer.t
val stat : t -> Sidekick_util.Stat.t
val find : t -> e_node -> repr

Current representative

val add_term : t -> Sidekick_core.Term.t -> e_node

Add the Term.t to the congruence closure, if not present already. Will be backtracked.

val mem_term : t -> Sidekick_core.Term.t -> bool

Returns true if the Term.t is explicitly present in the congruence closure

val allocate_bitfield : t -> descr:string -> bitfield

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).

val get_bitfield : t -> bitfield -> E_node.t -> bool

Access the bit field of the given e_node

val set_bitfield : t -> bitfield -> bool -> E_node.t -> unit

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_core.Proof_term.step_id
module Handler_action : sig ... end

Handler Actions

module Result_action : sig ... end

Result Actions.

Events

Events triggered by the congruence closure, to which other plugins can subscribe.

module Handler_action : sig ... end

Handler Actions

module Result_action : sig ... end

Result Actions.

Events

Events triggered by the congruence closure, to which other plugins can subscribe.

Events emitted by the congruence closure when something changes.

Ev_on_pre_merge acts n1 n2 expl is emitted right before n1 and n2 are merged with explanation expl.

val on_pre_merge2 : @@ -14,11 +14,7 @@ ( t * E_node.t * Sidekick_core.Term.t, Handler_action.t list ) Sidekick_util.Event.t

ev_on_new_term n t is emitted whenever a new Term.t t is added to the congruence closure. Its E_node.t is n.

type ev_on_conflict = {
cc : t;
th : bool;
c : Sidekick_core.Lit.t list;
}

Event emitted when a conflict occurs in the CC.

th is true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.

val on_conflict : t -> ( ev_on_conflict, unit ) Sidekick_util.Event.t

ev_on_conflict {th; c} is emitted when the congruence closure triggers a conflict by asserting the tautology c.

ev_on_propagate Lit.t reason is emitted whenever reason() => Lit.t is a propagated lemma. See CC_ACTIONS.propagate.

val on_is_subterm : t -> ( t * E_node.t * Sidekick_core.Term.t, Handler_action.t list ) @@ -40,10 +36,10 @@ ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Create a new congruence closure.

  • parameter term_store

    used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.

val create_default : ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Same as create but with the default CC view

\ 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 bc4e06cb..33282461 100644 --- a/dev/sidekick/Sidekick_cc/CC/module-type-BUILD/index.html +++ b/dev/sidekick/Sidekick_cc/CC/module-type-BUILD/index.html @@ -3,5 +3,5 @@ ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Create a new congruence closure.

  • parameter term_store

    used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.

\ 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 652572b9..2c8952ff 100644 --- a/dev/sidekick/Sidekick_cc/Expl/index.html +++ b/dev/sidekick/Sidekick_cc/Expl/index.html @@ -3,5 +3,5 @@ Sidekick_core.Term.t -> Sidekick_core.Term.t -> (Sidekick_core.Term.t * Sidekick_core.Term.t * t list) list -> - Sidekick_core.Proof_term.step_id -> + Sidekick_proof.Pterm.delayed -> t

mk_theory t u expl_sets pr builds a theory explanation for why |- t=u. It depends on sub-explanations expl_sets which are tuples (t_i, u_i, expls_i) where expls_i are explanations that justify t_i = u_i in the current congruence closure.

The proof pr is the theory lemma, of the form (t_i = u_i)_i |- t=u . It is resolved against each expls_i |- t_i=u_i obtained from expl_sets, on pivot t_i=u_i, to obtain a proof of Gamma |- t=u where Gamma is a subset of the literals asserted into the congruence closure.

For example for the lemma a=b deduced by injectivity from Some a=Some b in the theory of datatypes, the arguments would be a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr where pr is the injectivity lemma Some a=Some b |- a=b.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/Make/index.html b/dev/sidekick/Sidekick_cc/Make/index.html index c21e7cde..655e12d5 100644 --- a/dev/sidekick/Sidekick_cc/Make/index.html +++ b/dev/sidekick/Sidekick_cc/Make/index.html @@ -3,5 +3,5 @@ ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Create a new congruence closure.

\ 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 eb566171..eb6016ad 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
\ 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
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/Result_action/index.html b/dev/sidekick/Sidekick_cc/Result_action/index.html index 4fa1b20d..10ec1614 100644 --- a/dev/sidekick/Sidekick_cc/Result_action/index.html +++ b/dev/sidekick/Sidekick_cc/Result_action/index.html @@ -1,2 +1,2 @@ -Result_action (sidekick.Sidekick_cc.Result_action)

Module Sidekick_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_core.Proof_term.step_id(*

raise_conflict (c,pr) declares that c is a tautology of the theory of congruence.

  • parameter pr

    the proof of c being a tautology

*)
type or_conflict = ( t list, conflict ) Stdlib.result
\ No newline at end of file +Result_action (sidekick.Sidekick_cc.Result_action)

Module Sidekick_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.

  • parameter pr

    the proof of c being a tautology

*)
type or_conflict = ( t list, conflict ) Stdlib.result
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/index.html b/dev/sidekick/Sidekick_cc/index.html index 25b1c45a..318823ca 100644 --- a/dev/sidekick/Sidekick_cc/index.html +++ b/dev/sidekick/Sidekick_cc/index.html @@ -1,7 +1,7 @@ -Sidekick_cc (sidekick.Sidekick_cc)

Module Sidekick_cc

Congruence Closure Implementation

module type DYN_MONOID_PLUGIN = sig ... end
module type MONOID_PLUGIN_ARG = sig ... end
module type MONOID_PLUGIN_BUILDER = sig ... end
module View = Sidekick_core.CC_view
module E_node : sig ... end

E-node.

module Expl : sig ... end

Explanations

module Signature : sig ... end

A signature is a shallow term shape where immediate subterms are representative

module Resolved_expl : sig ... end

Resolved explanations.

module Plugin : sig ... end

Congruence Closure Plugin

module CC : sig ... end

Main congruence closure type.

include module type of struct include CC end
type e_node = E_node.t

A node of the congruence closure

type repr = E_node.t

Node that is currently a representative.

type explanation = Expl.t
type bitfield

A 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.

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 t

The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.

Accessors

val term_store : t -> Sidekick_core.Term.store
val stat : t -> Sidekick_util.Stat.t
val find : t -> e_node -> repr

Current representative

val add_term : t -> Sidekick_core.Term.t -> e_node

Add the Term.t to the congruence closure, if not present already. Will be backtracked.

val mem_term : t -> Sidekick_core.Term.t -> bool

Returns true if the Term.t is explicitly present in the congruence closure

val allocate_bitfield : t -> descr:string -> bitfield

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).

val get_bitfield : t -> bitfield -> E_node.t -> bool

Access the bit field of the given e_node

val set_bitfield : t -> bitfield -> bool -> E_node.t -> unit

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 ... end
module type MONOID_PLUGIN_ARG = sig ... end
module type MONOID_PLUGIN_BUILDER = sig ... end
module View = Sidekick_core.CC_view
module E_node : sig ... end

E-node.

module Expl : sig ... end

Explanations

module Signature : sig ... end

A signature is a shallow term shape where immediate subterms are representative

module Resolved_expl : sig ... end

Resolved explanations.

module Plugin : sig ... end

Congruence Closure Plugin

module CC : sig ... end

Main congruence closure signature.

include module type of struct include CC end
type e_node = E_node.t

A node of the congruence closure

type repr = E_node.t

Node that is currently a representative.

type explanation = Expl.t
type bitfield

A 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

The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.

Accessors

val term_store : t -> Sidekick_core.Term.store
val proof_tracer : t -> Sidekick_proof.Tracer.t
val stat : t -> Sidekick_util.Stat.t
val find : t -> e_node -> repr

Current representative

val add_term : t -> Sidekick_core.Term.t -> e_node

Add the Term.t to the congruence closure, if not present already. Will be backtracked.

val mem_term : t -> Sidekick_core.Term.t -> bool

Returns true if the Term.t is explicitly present in the congruence closure

val allocate_bitfield : t -> descr:string -> bitfield

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).

val get_bitfield : t -> bitfield -> E_node.t -> bool

Access the bit field of the given e_node

val set_bitfield : t -> bitfield -> bool -> E_node.t -> unit

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_core.Proof_term.step_id
module Handler_action : sig ... end

Handler Actions

module Result_action : sig ... end

Result Actions.

Events

Events triggered by the congruence closure, to which other plugins can subscribe.

module Handler_action : sig ... end

Handler Actions

module Result_action : sig ... end

Result Actions.

Events

Events triggered by the congruence closure, to which other plugins can subscribe.

Events emitted by the congruence closure when something changes.

Ev_on_pre_merge acts n1 n2 expl is emitted right before n1 and n2 are merged with explanation expl.

val on_pre_merge2 : @@ -14,11 +14,7 @@ ( t * E_node.t * Sidekick_core.Term.t, Handler_action.t list ) Sidekick_util.Event.t

ev_on_new_term n t is emitted whenever a new Term.t t is added to the congruence closure. Its E_node.t is n.

type ev_on_conflict = {
cc : t;
th : bool;
c : Sidekick_core.Lit.t list;
}

Event emitted when a conflict occurs in the CC.

th is true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.

val on_conflict : t -> ( ev_on_conflict, unit ) Sidekick_util.Event.t

ev_on_conflict {th; c} is emitted when the congruence closure triggers a conflict by asserting the tautology c.

ev_on_propagate Lit.t reason is emitted whenever reason() => Lit.t is a propagated lemma. See CC_ACTIONS.propagate.

val on_is_subterm : t -> ( t * E_node.t * Sidekick_core.Term.t, Handler_action.t list ) @@ -40,10 +36,10 @@ ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Create a new congruence closure.

  • parameter term_store

    used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.

val create_default : ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Same as create but with the default CC view

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/module-type-BUILD/index.html b/dev/sidekick/Sidekick_cc/module-type-BUILD/index.html index a28e7471..be06180f 100644 --- a/dev/sidekick/Sidekick_cc/module-type-BUILD/index.html +++ b/dev/sidekick/Sidekick_cc/module-type-BUILD/index.html @@ -3,5 +3,5 @@ ?stat:Sidekick_util.Stat.t -> ?size:[ `Small | `Big ] -> Sidekick_core.Term.store -> - Sidekick_core.Proof_trace.t -> + Sidekick_proof.Tracer.t -> t

Create a new congruence closure.

  • parameter term_store

    used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Clause_tracer/class-dummy/index.html b/dev/sidekick/Sidekick_core/Clause_tracer/class-dummy/index.html deleted file mode 100644 index 6694d495..00000000 --- a/dev/sidekick/Sidekick_core/Clause_tracer/class-dummy/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -dummy (sidekick.Sidekick_core.Clause_tracer.dummy)

Class Clause_tracer.dummy

method assert_clause : id:int -> Sidekick_core__Lit.t Iter.t -> Tr.Entry_id.t
method delete_clause : id:int -> Sidekick_core__Lit.t Iter.t -> unit
method unsat_clause : id:int -> Tr.Entry_id.t
method encode_lit : Sidekick_core__Lit.t -> Sidekick_util.Ser_value.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Clause_tracer/class-type-t/index.html b/dev/sidekick/Sidekick_core/Clause_tracer/class-type-t/index.html deleted file mode 100644 index 5683f316..00000000 --- a/dev/sidekick/Sidekick_core/Clause_tracer/class-type-t/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -t (sidekick.Sidekick_core.Clause_tracer.t)

Class type Clause_tracer.t

Tracer for clauses.

method assert_clause : id:int -> Sidekick_core__Lit.t Iter.t -> Tr.Entry_id.t
method delete_clause : id:int -> Sidekick_core__Lit.t Iter.t -> unit
method unsat_clause : id:int -> Tr.Entry_id.t
method encode_lit : Sidekick_core__Lit.t -> Sidekick_util.Ser_value.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Clause_tracer/index.html b/dev/sidekick/Sidekick_core/Clause_tracer/index.html deleted file mode 100644 index 09663846..00000000 --- a/dev/sidekick/Sidekick_core/Clause_tracer/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Clause_tracer (sidekick.Sidekick_core.Clause_tracer)

Module Sidekick_core.Clause_tracer

Tracer for clauses and literals

module Tr = Sidekick_trace
class type t = object ... end

Tracer for clauses.

class dummy : t
val dummy : t

Dummy tracer, recording nothing.

val assert_clause : t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t
val assert_clause' : t -> id:int -> Lit.t Iter.t -> unit
val delete_clause : t -> id:int -> Lit.t Iter.t -> unit
val unsat_clause : t -> id:int -> Tr.Entry_id.t
val unsat_clause' : t -> id:int -> unit
val encode_lit : t -> Lit.t -> Sidekick_util.Ser_value.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Lit/index.html b/dev/sidekick/Sidekick_core/Lit/index.html index 08409ff7..771f520e 100644 --- a/dev/sidekick/Sidekick_core/Lit/index.html +++ b/dev/sidekick/Sidekick_core/Lit/index.html @@ -1,2 +1,2 @@ -Lit (sidekick.Sidekick_core.Lit)

Module Sidekick_core.Lit

Literals

Literals are a pair of a boolean-sorted term, and a sign. Positive literals are the same as their term, and negative literals are the negation of their term.

The SAT solver deals only in literals and clauses (sets of literals). Everything else belongs in the SMT solver.

type t

A literal

include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.ORD with type t := t
val compare : t -> t -> int
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val term : t -> term

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> term * bool

Return the atom and the sign

val atom : ?sign:bool -> Sidekick_core_logic.Term.store -> term -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

  • parameter sign

    if provided, and sign=false, negate the resulting lit.

val make_eq : ?sign:bool -> Sidekick_core_logic.Term.store -> term -> term -> t
val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t
module Set : CCSet.S with type elt = t
module Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t
\ No newline at end of file +Lit (sidekick.Sidekick_core.Lit)

Module Sidekick_core.Lit

Literals

Literals are a pair of a boolean-sorted term, and a sign. Positive literals are the same as their term, and negative literals are the negation of their term.

The SAT solver deals only in literals and clauses (sets of literals). Everything else belongs in the SMT solver.

type t

A literal

include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.ORD with type t := t
val compare : t -> t -> int
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val pp_limit : max_depth:int -> max_nodes:int -> t Sidekick_util.Fmt.printer
val term : t -> term

Get the (positive) term

val sign : t -> bool

Get the sign. A negated literal has sign false.

val neg : t -> t

Take negation of literal. sign (neg lit) = not (sign lit).

val abs : t -> t

abs lit is like lit but always positive, i.e. sign (abs lit) = true

val signed_term : t -> term * bool

Return the atom and the sign

val atom : ?sign:bool -> Sidekick_core_logic.Term.store -> term -> t

atom store t makes a literal out of a term, possibly normalizing its sign in the process.

  • parameter sign

    if provided, and sign=false, negate the resulting lit.

val make_eq : ?sign:bool -> Sidekick_core_logic.Term.store -> term -> term -> t
val norm_sign : t -> t * bool

norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.

include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t
module Set : CCSet.S with type elt = t
module Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Proof_core/index.html b/dev/sidekick/Sidekick_core/Proof_core/index.html deleted file mode 100644 index a52a47a1..00000000 --- a/dev/sidekick/Sidekick_core/Proof_core/index.html +++ /dev/null @@ -1,17 +0,0 @@ - -Proof_core (sidekick.Sidekick_core.Proof_core)

Module Sidekick_core.Proof_core

Core proofs for SMT and congruence closure.

type lit = Lit.t
val lemma_cc : lit list -> Proof_term.t

lemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.

define_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u

proof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the Proof_term.t that produces C \/ u, i.e unit paramodulation.

proof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the Proof_term.t that produces C \/ u, i.e unit resolution.

proof_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 Proof_term.t that produces C \/ D, i.e boolean resolution.

with_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.

lemma_true (true) p asserts the clause (true)

lemma_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.

  • returns

    a Proof_term.t ID for the clause (t=u).

val lemma_rw_clause : - Proof_term.step_id -> - res:lit list -> - using:Proof_term.step_id list -> - Proof_term.t

lemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Proof_sat/index.html b/dev/sidekick/Sidekick_core/Proof_sat/index.html deleted file mode 100644 index 3aa8e524..00000000 --- a/dev/sidekick/Sidekick_core/Proof_sat/index.html +++ /dev/null @@ -1,5 +0,0 @@ - -Proof_sat (sidekick.Sidekick_core.Proof_sat)

Module Sidekick_core.Proof_sat

SAT-solver proof emission.

type lit = Lit.t
val sat_input_clause : lit list -> Proof_term.t

Emit an input clause.

val sat_redundant_clause : - lit list -> - hyps:Proof_term.step_id Iter.t -> - Proof_term.t

Emit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.

val sat_unsat_core : lit list -> Proof_term.t

TODO: is this relevant here?

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Proof_step/index.html b/dev/sidekick/Sidekick_core/Proof_step/index.html deleted file mode 100644 index 15a599f6..00000000 --- a/dev/sidekick/Sidekick_core/Proof_step/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Proof_step (sidekick.Sidekick_core.Proof_step)

Module Sidekick_core.Proof_step

type id = int32
val pp : int32 Sidekick_util.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Proof_term/index.html b/dev/sidekick/Sidekick_core/Proof_term/index.html deleted file mode 100644 index 4e09fb3c..00000000 --- a/dev/sidekick/Sidekick_core/Proof_term/index.html +++ /dev/null @@ -1,9 +0,0 @@ - -Proof_term (sidekick.Sidekick_core.Proof_term)

Module Sidekick_core.Proof_term

Proof terms.

A proof term is the description of a reasoning step, that yields a clause.

type step_id = Proof_step.id
type local_ref = int
type lit = Lit.t
type rule_apply = {
rule_name : string;
lit_args : lit list;
term_args : Sidekick_core_logic.Term.t list;
subst_args : Sidekick_core_logic.Subst.t list;
premises : step_id list;
indices : int list;
}
type t =
| P_ref of step_id
| P_local of local_ref(*

Local reference, in a let

*)
| P_let of (local_ref * t) list * t
| P_apply of rule_apply
type delayed = unit -> t
include Sidekick_sigs.PRINT with type t := t
val ref_ : step_id -> t
val local_ref : local_ref -> t
val let_ : (local_ref * t) list -> t -> t
val apply_rule : - ?lits:lit list -> - ?terms:Sidekick_core_logic.Term.t list -> - ?substs:Sidekick_core_logic.Subst.t list -> - ?premises:step_id list -> - ?indices:int list -> - string -> - t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Proof_trace/Step_vec/index.html b/dev/sidekick/Sidekick_core/Proof_trace/Step_vec/index.html deleted file mode 100644 index 14247d37..00000000 --- a/dev/sidekick/Sidekick_core/Proof_trace/Step_vec/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Step_vec (sidekick.Sidekick_core.Proof_trace.Step_vec)

Module Proof_trace.Step_vec

A vector indexed by steps.

include Sidekick_util.Vec_sig.BASE_RO with type elt = step_id
type elt = step_id
type t
val size : t -> int
val get : t -> int -> elt
val iter : f:( elt -> unit ) -> t -> unit
val iteri : f:( int -> elt -> unit ) -> t -> unit
val to_iter : t -> elt Iter.t
val create : ?cap:int -> unit -> t
val clear : t -> unit
val copy : t -> t
val is_empty : t -> bool
val push : t -> elt -> unit
val fast_remove : t -> int -> unit

Remove element at index i without preserving order (swap with last element)

val filter_in_place : ( elt -> bool ) -> t -> unit
val ensure_size : t -> int -> unit
val pop : t -> elt
val set : t -> int -> elt -> unit
val shrink : t -> int -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Proof_trace/index.html b/dev/sidekick/Sidekick_core/Proof_trace/index.html deleted file mode 100644 index 49e06835..00000000 --- a/dev/sidekick/Sidekick_core/Proof_trace/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Proof_trace (sidekick.Sidekick_core.Proof_trace)

Module Sidekick_core.Proof_trace

Proof traces.

A proof trace is a log of all the deductive reasoning steps made by the SMT solver and other reasoning components. It essentially stores a DAG of all these steps, where each step points (via step_id) to its premises.

type lit = Lit.t
type step_id = Proof_step.id

Identifier for a tracing step (like a unique ID for a clause previously added/proved)

A vector indexed by steps.

Traces

type t

The proof trace itself.

A proof trace is a log of all deductive steps taken by the solver, so we can later reconstruct a certificate for proof-checking.

Each step in the proof trace should be a valid lemma (of its theory) or a valid consequence of previous steps.

val enabled : t -> bool

Is proof tracing enabled?

val add_step : t -> Proof_term.delayed -> step_id

Create a new step in the trace.

val add_unsat : t -> step_id -> unit

Signal "unsat" result at the given proof

val delete : t -> step_id -> unit

Forget a step that won't be used in the rest of the trace. Only useful for performance/memory considerations.

val close : t -> unit

close p closes the proof, and can dispose of underlying resources

Dummy backend

val dummy_step_id : step_id
val dummy : t

Dummy proof trace, logs nothing.

Dynamic interface

module type DYN = sig ... end
val make : (module DYN) -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Proof_trace/module-type-DYN/index.html b/dev/sidekick/Sidekick_core/Proof_trace/module-type-DYN/index.html deleted file mode 100644 index 41085a71..00000000 --- a/dev/sidekick/Sidekick_core/Proof_trace/module-type-DYN/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -DYN (sidekick.Sidekick_core.Proof_trace.DYN)

Module type Proof_trace.DYN

val enabled : unit -> bool
val add_step : Proof_term.delayed -> step_id
val add_unsat : step_id -> unit
val delete : step_id -> unit
val close : unit -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Term/Ref/index.html b/dev/sidekick/Sidekick_core/Term/Ref/index.html new file mode 100644 index 00000000..5426b6d1 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Term/Ref/index.html @@ -0,0 +1,6 @@ + +Ref (sidekick.Sidekick_core.Term.Ref)

Module Term.Ref

Term reference

Reference to another term, by a unique ID in a trace.

This allows a trace to contain terms with explicit references to other terms, but where these references have to be followed explicitly. Thus, each term can be deserialized separately.

For example, a proof term for a given lemma might use references to previous lemmas, instead of their direct proof terms; this allows a checker or proof GUI to only read this particular lemma's proof into a term.

ref tst id ~ty is the reference to entry id in a trace, which must be a term of type ty.

val as_ref : Sidekick_core_logic.Term.t -> t option

as_ref (ref tst id ~ty) is Some id.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Term/Trace_reader/index.html b/dev/sidekick/Sidekick_core/Term/Trace_reader/index.html index 40bdbd41..7c3e4b11 100644 --- a/dev/sidekick/Sidekick_core/Term/Trace_reader/index.html +++ b/dev/sidekick/Sidekick_core/Term/Trace_reader/index.html @@ -3,11 +3,11 @@ ?const_decoders:const_decoders list -> source:Tr.Source.t -> Sidekick_core_logic.Term.store -> - t
val add_const_decoders : t -> const_decoders -> unit
val read_term : + t
val store : t -> Sidekick_core_logic.Term.store
val add_const_decoders : t -> const_decoders -> unit
val read_term : t -> term_ref -> ( Sidekick_core_logic.Term.t, string ) Stdlib.result
val read_term_err : t -> term_ref -> ( Sidekick_core_logic.Term.t, Sidekick_util.Ser_decode.Error.t ) - Stdlib.result
\ No newline at end of file + Stdlib.result
val read_term_exn : t -> term_ref -> Sidekick_core_logic.Term.t
val deref_term : t -> Sidekick_core_logic.Term.t -> Sidekick_core_logic.Term.t

deref_term reader t dereferences the root node of t. If t is Ref id, this returns the term at id instead.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Term/Tracer/index.html b/dev/sidekick/Sidekick_core/Term/Tracer/index.html index 2e5e575c..a4f8795e 100644 --- a/dev/sidekick/Sidekick_core/Term/Tracer/index.html +++ b/dev/sidekick/Sidekick_core/Term/Tracer/index.html @@ -1,2 +1,2 @@ -Tracer (sidekick.Sidekick_core.Term.Tracer)

Module Term.Tracer

Emit terms in traces.

Traces will contains terms, encoded as a DAG. Each subterm is its own event, and gets a term identifier used in other subsequent entries to refer to it.

module Tr = Sidekick_trace
type term_ref = Tr.entry_id
type Tr.entry_view +=
| T_ty of int
| T_app of term_ref * term_ref
| T_var of string * term_ref
| T_bvar of int * term_ref
| T_const of {
c : Sidekick_core_logic.Const.view;
c_ops : Sidekick_core_logic.Const.Ops.t;
ty : term_ref;
}
| T_lam of {
v_name : string;
v_ty : term_ref;
body : term_ref;
}
| T_pi of {
v_name : string;
v_ty : term_ref;
body : term_ref;
}
class type t = object ... end
class dummy : object ... end

Dummy implementation, returns Tr.Entry_id.dummy

class concrete : sink:Tr.Sink.t -> t

Concrete implementation of t

val create : sink:Tr.Sink.t -> unit -> t

create ~sink () makes a tracer that will write terms into the given sink.

val emit' : t -> Sidekick_core_logic.Term.t -> unit
\ No newline at end of file +Tracer (sidekick.Sidekick_core.Term.Tracer)

Module Term.Tracer

Emit terms in traces.

Traces will contains terms, encoded as a DAG. Each subterm is its own event, and gets a term identifier used in other subsequent entries to refer to it.

module Tr = Sidekick_trace
type term_ref = Sidekick_trace.entry_id
class type t = object ... end
class dummy : object ... end

Dummy implementation, returns Tr.Entry_id.dummy

class concrete : sink:Tr.Sink.t -> t

Concrete implementation of t

val create : sink:Tr.Sink.t -> unit -> t

create ~sink () makes a tracer that will write terms into the given sink.

val emit' : t -> Sidekick_core_logic.Term.t -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Term/index.html b/dev/sidekick/Sidekick_core/Term/index.html index e9fb6674..6e5d6d99 100644 --- a/dev/sidekick/Sidekick_core/Term/index.html +++ b/dev/sidekick/Sidekick_core/Term/index.html @@ -8,7 +8,7 @@ n3: g n2 n1 n4: = n3 n3
val iter_shallow : f:( bool -> t -> unit ) -> t -> unit

iter_shallow f e iterates on immediate subterms of e, calling f trdb e' for each subterm e', with trdb = true iff e' is directly under a binder.

val map_shallow : store -> f:( bool -> t -> t ) -> t -> t
val exists_shallow : f:( bool -> t -> bool ) -> t -> bool
val for_all_shallow : f:( bool -> t -> bool ) -> t -> bool
val contains : t -> sub:t -> bool
val free_vars_iter : t -> var Iter.t
val free_vars : ?init:Sidekick_core_logic__.Var.Set.t -> t -> - Sidekick_core_logic__.Var.Set.t
val is_type : t -> bool

is_type t is true iff view t is Type _

val is_a_type : t -> bool

is_a_type t is true if is_ty (ty t)

val is_closed : t -> bool

Is the term closed (all bound variables are paired with a binder)? time: O(1)

val has_fvars : t -> bool

Does the term contain free variables? time: O(1)

val ty : t -> t

Return the type of this term.

Creation

module Store : sig ... end
val type_ : store -> t
val type_of_univ : store -> int -> t
val var : store -> var -> t
val var_str : store -> string -> ty:t -> t
val bvar : store -> bvar -> t
val bvar_i : store -> int -> ty:t -> t
val const : store -> Sidekick_core_logic__Types_.const -> t
val app : store -> t -> t -> t
val app_l : store -> t -> t list -> t
val app_fold : store -> f:t -> acc0:t -> t list -> t
val lam : store -> var -> t -> t
val pi : store -> var -> t -> t
val arrow : store -> t -> t -> t
val arrow_l : store -> t list -> t -> t
val open_lambda : store -> t -> (var * t) option
val open_lambda_exn : store -> t -> var * t
module DB : sig ... end

De bruijn indices

include module type of struct include Sidekick_core_logic.T_builtins end
type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val bool_val : + Sidekick_core_logic__.Var.Set.t
val is_type : t -> bool

is_type t is true iff view t is Type _

val is_a_type : t -> bool

is_a_type t is true if is_ty (ty t)

val is_closed : t -> bool

Is the term closed (all bound variables are paired with a binder)? time: O(1)

val has_fvars : t -> bool

Does the term contain free variables? time: O(1)

val ty : t -> t

Return the type of this term.

Creation

module Store : sig ... end
val type_ : store -> t
val type_of_univ : store -> int -> t
val var : store -> var -> t
val var_str : store -> string -> ty:t -> t
val bvar : store -> bvar -> t
val bvar_i : store -> int -> ty:t -> t
val const : store -> Sidekick_core_logic__Types_.const -> t
val app : store -> t -> t -> t
val app_l : store -> t -> t list -> t
val app_fold : store -> f:t -> acc0:t -> t list -> t
val lam : store -> var -> t -> t
val pi : store -> var -> t -> t
val arrow : store -> t -> t -> t
val arrow_l : store -> t list -> t -> t
val open_lambda : store -> t -> (var * t) option
val open_lambda_exn : store -> t -> var * t
module DB : sig ... end

De bruijn indices

include module type of struct include Sidekick_core_logic.T_builtins end
type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
| C_proof
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val eq : @@ -32,4 +32,4 @@ n4: = n3 n3
term Sidekick_util.Fmt.printer -> Sidekick_util.Fmt.t -> term -> - bool

Printing hook, responsible for printing certain subterms

module Hooks : sig ... end
val default_hooks : Hooks.t Stdlib.ref
val pp_with : Hooks.t -> term Sidekick_util.Fmt.printer

Print using the hooks

val pp : term Sidekick_util.Fmt.printer

Print using default_hooks

module Tracer : sig ... end

Emit terms in traces.

module Trace_reader : sig ... end
\ No newline at end of file + bool

Printing hook, responsible for printing certain subterms

module Hooks : sig ... end
val default_hooks : Hooks.t Stdlib.ref
val pp_with : Hooks.t -> term Sidekick_util.Fmt.printer

Print using the hooks

val pp : term Sidekick_util.Fmt.printer

Print using default_hooks

val pp_limit : max_depth:int -> max_nodes:int -> term Sidekick_util.Fmt.printer

Print with a limit on the number of nodes printed. An ellipsis is displayed otherwise.

module Tracer : sig ... end

Emit terms in traces.

module Trace_reader : sig ... end
module Ref : sig ... end

Term reference

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/index.html b/dev/sidekick/Sidekick_core/index.html index 9d323b63..16dd9cbc 100644 --- a/dev/sidekick/Sidekick_core/index.html +++ b/dev/sidekick/Sidekick_core/index.html @@ -1,2 +1,7 @@ -Sidekick_core (sidekick.Sidekick_core)

Module Sidekick_core

Main Signatures.

Theories and concrete solvers rely on an environment that defines several important types:

In this module we define most of the main signatures used throughout Sidekick.

module Fmt = CCFormat

Re-exports from core-logic

module Term : sig ... end
module Gensym : sig ... end

Fresh symbol generation

view

module Bool_view : sig ... end

Boolean-oriented view of terms

module CC_view : sig ... end

View terms through the lens of a Congruence Closure

module Default_cc_view : sig ... end

Main modules

module Lit : sig ... end

Literals

module Proof_step : sig ... end
module Proof_core : sig ... end

Core proofs for SMT and congruence closure.

module Proof_sat : sig ... end

SAT-solver proof emission.

module Proof_trace : sig ... end

Proof traces.

module Proof_term : sig ... end

Proof terms.

module Box : sig ... end
module Clause_tracer : sig ... end

Tracer for clauses and literals

exception Resource_exhausted
\ No newline at end of file +Sidekick_core (sidekick.Sidekick_core)

Module Sidekick_core

Main Signatures.

Theories and concrete solvers rely on an environment that defines several important types:

In this module we define most of the main signatures used throughout Sidekick.

module Fmt = CCFormat

Re-exports from core-logic

module Term : sig ... end

view

module Bool_view : sig ... end

Boolean-oriented view of terms

module CC_view : sig ... end

View terms through the lens of a Congruence Closure

module Default_cc_view : sig ... end

Main modules

module Lit : sig ... end

Literals

module Box : sig ... end
module Gensym : sig ... end

Fresh symbol generation

exception Resource_exhausted

Const decoders for traces

val const_decoders : + (string + * Sidekick_core_logic.Const.Ops.t + * ( Sidekick_core_logic__Types_.term Sidekick_util.Ser_decode.t -> + Sidekick_core_logic.Const.view Sidekick_util.Ser_decode.t )) + list
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core_logic/T_builtins/index.html b/dev/sidekick/Sidekick_core_logic/T_builtins/index.html index 27223a03..8bcad848 100644 --- a/dev/sidekick/Sidekick_core_logic/T_builtins/index.html +++ b/dev/sidekick/Sidekick_core_logic/T_builtins/index.html @@ -1,2 +1,2 @@ -T_builtins (sidekick.Sidekick_core_logic.T_builtins)

Module Sidekick_core_logic.T_builtins

Core builtins

type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
val bool : Term.store -> Term.t
val c_not : Term.store -> Term.t
val c_eq : Term.store -> Term.t
val c_ite : Term.store -> Term.t
val true_ : Term.store -> Term.t
val false_ : Term.store -> Term.t
val bool_val : Term.store -> bool -> Term.t
val const_decoders : Const.decoders
val eq : Term.store -> Term.t -> Term.t -> Term.t

eq a b is a = b

val not : Term.store -> Term.t -> Term.t
val ite : Term.store -> Term.t -> Term.t -> Term.t -> Term.t

ite a b c is if a then b else c

val is_eq : Term.t -> bool
val is_bool : Term.t -> bool
val abs : Term.store -> Term.t -> bool * Term.t

abs t returns an "absolute value" for the term, along with the sign of t.

The idea is that we want to turn not a into (false, a), or (a != b) into (false, a=b). For terms without a negation this should return (true, t).

val as_bool_val : Term.t -> bool option
val open_eq : Term.t -> (Term.t * Term.t) option

open_eq (a=b) returns Some (a,b), None for other terms.

\ No newline at end of file +T_builtins (sidekick.Sidekick_core_logic.T_builtins)

Module Sidekick_core_logic.T_builtins

Core builtins

type Sidekick_core_logic__Types_.const_view +=
| C_bool
| C_eq
| C_ite
| C_not
| C_true
| C_false
| C_proof
val bool : Term.store -> Term.t
val proof : Term.store -> Term.t
val c_not : Term.store -> Term.t
val c_eq : Term.store -> Term.t
val c_ite : Term.store -> Term.t
val true_ : Term.store -> Term.t
val false_ : Term.store -> Term.t
val bool_val : Term.store -> bool -> Term.t
val const_decoders : Const.decoders
val eq : Term.store -> Term.t -> Term.t -> Term.t

eq a b is a = b

val not : Term.store -> Term.t -> Term.t
val ite : Term.store -> Term.t -> Term.t -> Term.t -> Term.t

ite a b c is if a then b else c

val is_eq : Term.t -> bool
val is_bool : Term.t -> bool
val abs : Term.store -> Term.t -> bool * Term.t

abs t returns an "absolute value" for the term, along with the sign of t.

The idea is that we want to turn not a into (false, a), or (a != b) into (false, a=b). For terms without a negation this should return (true, t).

val as_bool_val : Term.t -> bool option
val open_eq : Term.t -> (Term.t * Term.t) option

open_eq (a=b) returns Some (a,b), None for other terms.

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/.dummy b/dev/sidekick/Sidekick_proof/.dummy similarity index 100% rename from dev/sidekick-base/Sidekick_base_proof_trace/.dummy rename to dev/sidekick/Sidekick_proof/.dummy diff --git a/dev/sidekick/Sidekick_proof/Core_rules/index.html b/dev/sidekick/Sidekick_proof/Core_rules/index.html new file mode 100644 index 00000000..a7bdae62 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Core_rules/index.html @@ -0,0 +1,17 @@ + +Core_rules (sidekick.Sidekick_proof.Core_rules)

Module Sidekick_proof.Core_rules

Core proofs for SMT and congruence closure.

val lemma_cc : lit list -> Pterm.t

lemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.

define_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 : Pterm.step_id -> Pterm.step_id -> Pterm.t

proof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the Pterm.t that produces C \/ u, i.e unit paramodulation.

val proof_r1 : Pterm.step_id -> Pterm.step_id -> Pterm.t

proof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the Pterm.t that produces C \/ u, i.e unit resolution.

val proof_res : + pivot:Sidekick_core_logic.Term.t -> + Pterm.step_id -> + Pterm.step_id -> + Pterm.t

proof_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 Pterm.t that produces C \/ D, i.e boolean resolution.

val with_defs : Pterm.step_id -> Pterm.step_id list -> Pterm.t

with_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.

lemma_true (true) p asserts the clause (true)

val lemma_preprocess : + Sidekick_core_logic.Term.t -> + Sidekick_core_logic.Term.t -> + using:Pterm.step_id list -> + Pterm.t

lemma_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.

  • returns

    a Pterm.t ID for the clause (t=u).

val lemma_rw_clause : + Pterm.step_id -> + res:lit list -> + using:Pterm.step_id list -> + Pterm.t

lemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Pterm/index.html b/dev/sidekick/Sidekick_proof/Pterm/index.html new file mode 100644 index 00000000..967e81ff --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Pterm/index.html @@ -0,0 +1,9 @@ + +Pterm (sidekick.Sidekick_proof.Pterm)

Module Sidekick_proof.Pterm

Proof terms.

A proof term is the description of a reasoning step, that yields a clause.

type step_id = Step.id
type local_ref = Step.id

A local reference is a step id that is only valid in the scope of a P_let. Typically one can use negative integers to avoid accidental shadowing.

type rule_apply = {
rule_name : string;
lit_args : lit list;
term_args : Sidekick_core.Term.t list;
subst_args : Sidekick_core.Subst.t list;
premises : step_id list;
indices : int list;
}
type t =
| P_ref of step_id
| P_local of local_ref(*

Local reference, in a let

*)
| P_let of (local_ref * t) list * t
| P_apply of rule_apply
type delayed = unit -> t
include Sidekick_sigs.PRINT with type t := t
val ref : step_id -> t
val local_ref : local_ref -> t
val let_ : (local_ref * t) list -> t -> t
val delay : ( unit -> t ) -> delayed
val dummy : t

Reference to the dummy step

val apply_rule : + ?lits:lit list -> + ?terms:Sidekick_core.Term.t list -> + ?substs:Sidekick_core.Subst.t list -> + ?premises:step_id list -> + ?indices:int list -> + string -> + t

Serialize

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Sat_rules/index.html b/dev/sidekick/Sidekick_proof/Sat_rules/index.html new file mode 100644 index 00000000..33c19d21 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Sat_rules/index.html @@ -0,0 +1,2 @@ + +Sat_rules (sidekick.Sidekick_proof.Sat_rules)

Module Sidekick_proof.Sat_rules

SAT-solver proof emission.

val sat_input_clause : lit list -> Pterm.t

Emit an input clause.

val sat_redundant_clause : lit list -> hyps:Step.id Iter.t -> Pterm.t

Emit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.

val sat_unsat_core : lit list -> Pterm.t

TODO: is this relevant here?

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Step/index.html b/dev/sidekick/Sidekick_proof/Step/index.html new file mode 100644 index 00000000..31f8edb2 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Step/index.html @@ -0,0 +1,2 @@ + +Step (sidekick.Sidekick_proof.Step)

Module Sidekick_proof.Step

val equal : id -> id -> bool
val dummy : id
val pp : id Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Step_vec/index.html b/dev/sidekick/Sidekick_proof/Step_vec/index.html new file mode 100644 index 00000000..1fc0a780 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Step_vec/index.html @@ -0,0 +1,2 @@ + +Step_vec (sidekick.Sidekick_proof.Step_vec)

Module Sidekick_proof.Step_vec

A vector indexed by steps.

include Sidekick_util.Vec_sig.BASE with type elt = Step.id
include Sidekick_util.Vec_sig.BASE_RO with type elt = Step.id
type elt = Step.id
type t
val size : t -> int
val get : t -> int -> elt
val iter : f:( elt -> unit ) -> t -> unit
val iteri : f:( int -> elt -> unit ) -> t -> unit
val to_iter : t -> elt Iter.t
val create : ?cap:int -> unit -> t
val clear : t -> unit
val copy : t -> t
val is_empty : t -> bool
val push : t -> elt -> unit
val fast_remove : t -> int -> unit

Remove element at index i without preserving order (swap with last element)

val filter_in_place : ( elt -> bool ) -> t -> unit
val ensure_size : t -> int -> unit
val pop : t -> elt
val set : t -> int -> elt -> unit
val shrink : t -> int -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Trace_reader/index.html b/dev/sidekick/Sidekick_proof/Trace_reader/index.html new file mode 100644 index 00000000..5ac706d1 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Trace_reader/index.html @@ -0,0 +1,6 @@ + +Trace_reader (sidekick.Sidekick_proof.Trace_reader)

Module Sidekick_proof.Trace_reader

module Tr = Sidekick_trace
type step_id = Step.id
type t
val read_step : + ?fix:bool -> + t -> + step_id -> + ( Pterm.t, Dec.Error.t ) Stdlib.result

Read a step from the source at the given step id, using the trace reader.

  • parameter fix

    if true, dereferences in a loop so the returned proof term is not a Ref.

val dec_step_id : ?fix:bool -> t -> Pterm.t Dec.t

Reads an integer, decodes the corresponding entry

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Tracer/class-concrete/index.html b/dev/sidekick/Sidekick_proof/Tracer/class-concrete/index.html new file mode 100644 index 00000000..d270f99d --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Tracer/class-concrete/index.html @@ -0,0 +1,2 @@ + +concrete (sidekick.Sidekick_proof.Tracer.concrete)

Class Tracer.concrete

Concrete implementation of t

inherit Sidekick_core.Term.Tracer.t
method proof_enabled : bool

If proof tracing enabled?

method proof_enable : bool -> unit

Enable/disable proof tracing, if supported

method emit_proof_step : Sidekick_proof__Pterm.delayed -> step_id

Create a new step in the trace.

method emit_proof_delete : step_id -> unit

Forget a step that won't be used in the rest of the trace. Only useful for performance/memory considerations.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Tracer/class-dummy/index.html b/dev/sidekick/Sidekick_proof/Tracer/class-dummy/index.html new file mode 100644 index 00000000..1c3beff8 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Tracer/class-dummy/index.html @@ -0,0 +1,2 @@ + +dummy (sidekick.Sidekick_proof.Tracer.dummy)

Class Tracer.dummy

Dummy proof trace, logs nothing.

inherit Sidekick_core.Term.Tracer.t
method proof_enabled : bool

If proof tracing enabled?

method proof_enable : bool -> unit

Enable/disable proof tracing, if supported

method emit_proof_step : Sidekick_proof__Pterm.delayed -> step_id

Create a new step in the trace.

method emit_proof_delete : step_id -> unit

Forget a step that won't be used in the rest of the trace. Only useful for performance/memory considerations.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Tracer/class-type-t/index.html b/dev/sidekick/Sidekick_proof/Tracer/class-type-t/index.html new file mode 100644 index 00000000..1ad381da --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Tracer/class-type-t/index.html @@ -0,0 +1,2 @@ + +t (sidekick.Sidekick_proof.Tracer.t)

Class type Tracer.t

A proof tracer.

A proof tracer builds a log of all deductive steps taken by the solver, so we can later reconstruct a certificate for proof-checking.

Each step in the proof trace should be a valid lemma (of its theory) or a valid consequence of previous steps.

inherit Sidekick_core.Term.Tracer.t
method proof_enabled : bool

If proof tracing enabled?

method proof_enable : bool -> unit

Enable/disable proof tracing, if supported

method emit_proof_step : Sidekick_proof__Pterm.delayed -> step_id

Create a new step in the trace.

method emit_proof_delete : step_id -> unit

Forget a step that won't be used in the rest of the trace. Only useful for performance/memory considerations.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/Tracer/index.html b/dev/sidekick/Sidekick_proof/Tracer/index.html new file mode 100644 index 00000000..6dd51494 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/Tracer/index.html @@ -0,0 +1,2 @@ + +Tracer (sidekick.Sidekick_proof.Tracer)

Module Sidekick_proof.Tracer

Proof traces.

A proof trace is a log of all the deductive reasoning steps made by the SMT solver and other reasoning components. It essentially stores a DAG of all these steps, where each step points (via step_id) to its premises.

type step_id = Step.id

Identifier for a tracing step (like a unique ID for a clause previously added/proved)

class type t = object ... end

A proof tracer.

val enabled : t -> bool

Is proof tracing enabled?

val enable : t -> bool -> unit

Enable proof tracing

val add_step : t -> Pterm.delayed -> step_id

Create a new step in the trace.

val delete : t -> step_id -> unit

Forget a step that won't be used in the rest of the trace. Only useful for performance/memory considerations.

class dummy : t

Dummy proof trace, logs nothing.

val dummy : t

Concrete implementation of t

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_proof/index.html b/dev/sidekick/Sidekick_proof/index.html new file mode 100644 index 00000000..c6136147 --- /dev/null +++ b/dev/sidekick/Sidekick_proof/index.html @@ -0,0 +1,2 @@ + +Sidekick_proof (sidekick.Sidekick_proof)

Module Sidekick_proof

module Step : sig ... end
module Step_vec : sig ... end

A vector indexed by steps.

module Sat_rules : sig ... end

SAT-solver proof emission.

module Core_rules : sig ... end

Core proofs for SMT and congruence closure.

module Pterm : sig ... end

Proof terms.

module Tracer : sig ... end

Proof traces.

module Trace_reader : sig ... end
module Arg = Stdlib.Arg
type term = Pterm.t
type term_ref = Step.id
type step_id = Step.id
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Solver/index.html b/dev/sidekick/Sidekick_sat/Solver/index.html index 9216daab..bd303421 100644 --- a/dev/sidekick/Sidekick_sat/Solver/index.html +++ b/dev/sidekick/Sidekick_sat/Solver/index.html @@ -1,12 +1,12 @@ -Solver (sidekick.Sidekick_sat.Solver)

Module Sidekick_sat.Solver

The external interface implemented by SAT solvers.

type clause
type plugin = (module Sidekick_sat__Sigs.PLUGIN)
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end

Main Solver Type

type t = solver

Main solver type, containing all state for solving.

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

Access the inner proof

val on_conflict : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_decision : t -> ( Sidekick_core.Lit.t, unit ) Sidekick_util.Event.t
val on_learnt : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_gc : t -> ( Sidekick_core.Lit.t array, unit ) Sidekick_util.Event.t

Types

type res =
| Sat of (module Sidekick_sat__Sigs.SAT_STATE)(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (module Sidekick_sat__Sigs.UNSAT_STATE with type clause = clause)(*

Returned when the solver reaches UNSAT, with a proof

*)

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : t -> Sidekick_core.Lit.t list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val add_clause : +Solver (sidekick.Sidekick_sat.Solver)

Module Sidekick_sat.Solver

The external interface implemented by SAT solvers.

type clause
type plugin = (module Sidekick_sat__Sigs.PLUGIN)
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end

Main Solver Type

type t = solver

Main solver type, containing all state for solving.

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val tracer : t -> Tracer.t

Access the inner proof

val on_conflict : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_decision : t -> ( Sidekick_core.Lit.t, unit ) Sidekick_util.Event.t
val on_learnt : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_gc : t -> ( Sidekick_core.Lit.t array, unit ) Sidekick_util.Event.t

Types

type res =
| Sat of (module Sidekick_sat__Sigs.SAT_STATE)(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (module Sidekick_sat__Sigs.UNSAT_STATE with type clause = clause)(*

Returned when the solver reaches UNSAT, with a proof

*)

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : t -> Sidekick_core.Lit.t list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

Lower level addition of clauses

Lower level addition of clauses

val add_input_clause : t -> Sidekick_core.Lit.t list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> Sidekick_core.Lit.t array -> unit

Like add_clause_a but with justification of being an input clause

Solving

val solve : ?on_progress:( unit -> unit ) -> ?assumptions:Sidekick_core.Lit.t list -> @@ -25,13 +25,11 @@ (module Sidekick_sat__Sigs.PLUGIN)

Create a plugin

  • parameter push_level

    create a new backtrack level

  • parameter pop_levels

    Pop n levels of the plugin

  • parameter partial_check

    Assume the lits in the slice, possibly using the slice to push new lits to be propagated or to raising a conflict or to add new lemmas.

  • parameter final_check

    Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; if a conflict clause is added, search backtracks and then resumes.

val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> - ?tracer:Sidekick_core.Clause_tracer.t -> - proof:Sidekick_core.Proof_trace.t -> + tracer:Tracer.t -> plugin -> t

Create new solver

  • parameter theory

    the theory

  • parameter the

    proof

  • parameter size

    the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses.

val plugin_pure_sat : plugin
val create_pure_sat : ?stat:Sidekick_util.Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> - ?tracer:Sidekick_core.Clause_tracer.t -> - proof:Sidekick_core.Proof_trace.t -> + tracer:Tracer.t -> unit -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Tracer/class-dummy/index.html b/dev/sidekick/Sidekick_sat/Tracer/class-dummy/index.html new file mode 100644 index 00000000..dad33fe1 --- /dev/null +++ b/dev/sidekick/Sidekick_sat/Tracer/class-dummy/index.html @@ -0,0 +1,5 @@ + +dummy (sidekick.Sidekick_sat.Tracer.dummy)

Class Tracer.dummy

inherit Proof.Tracer.t
method sat_assert_clause : id:int -> + Sidekick_core.Lit.t Iter.t -> + Proof.Step.id -> + Tr.Entry_id.t
method sat_delete_clause : id:int -> Sidekick_core.Lit.t Iter.t -> unit
method sat_unsat_clause : id:int -> Tr.Entry_id.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Tracer/class-type-t/index.html b/dev/sidekick/Sidekick_sat/Tracer/class-type-t/index.html new file mode 100644 index 00000000..6bddbec5 --- /dev/null +++ b/dev/sidekick/Sidekick_sat/Tracer/class-type-t/index.html @@ -0,0 +1,5 @@ + +t (sidekick.Sidekick_sat.Tracer.t)

Class type Tracer.t

Tracer for the SAT solver.

inherit Proof.Tracer.t
method sat_assert_clause : id:int -> + Sidekick_core.Lit.t Iter.t -> + Proof.Step.id -> + Tr.Entry_id.t
method sat_delete_clause : id:int -> Sidekick_core.Lit.t Iter.t -> unit
method sat_unsat_clause : id:int -> Tr.Entry_id.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Tracer/index.html b/dev/sidekick/Sidekick_sat/Tracer/index.html new file mode 100644 index 00000000..35d58e12 --- /dev/null +++ b/dev/sidekick/Sidekick_sat/Tracer/index.html @@ -0,0 +1,12 @@ + +Tracer (sidekick.Sidekick_sat.Tracer)

Module Sidekick_sat.Tracer

Tracer for clauses and literals

module Tr = Sidekick_trace
module Proof = Sidekick_proof
class type t = object ... end

Tracer for the SAT solver.

class dummy : t
val dummy : t

Dummy tracer, recording nothing.

val assert_clause : + t -> + id:int -> + Sidekick_core.Lit.t Iter.t -> + Proof.Step.id -> + Tr.Entry_id.t
val assert_clause' : + t -> + id:int -> + Sidekick_core.Lit.t Iter.t -> + Proof.Step.id -> + unit
val delete_clause : t -> id:int -> Sidekick_core.Lit.t Iter.t -> unit
val unsat_clause : t -> id:int -> Tr.Entry_id.t
val unsat_clause' : t -> id:int -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/index.html b/dev/sidekick/Sidekick_sat/index.html index 51d31902..90f0811e 100644 --- a/dev/sidekick/Sidekick_sat/index.html +++ b/dev/sidekick/Sidekick_sat/index.html @@ -1,12 +1,12 @@ -Sidekick_sat (sidekick.Sidekick_sat)

Module Sidekick_sat

Main API

module type SAT_STATE = sig ... end

Solver in a "SATISFIABLE" state

type sat_state = (module SAT_STATE)

The type of values returned when the solver reaches a SAT state.

module type UNSAT_STATE = sig ... end

Solver in an "UNSATISFIABLE" state

type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause)

The type of values returned when the solver reaches an UNSAT state.

type same_sign = bool

This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.

type reason =
| Consequence of unit -> Sidekick_core.Lit.t list * Sidekick_core.Proof_step.id

The type of reasons for propagations of a lit f.

Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".

invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.

note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.

type lbool =
| L_true
| L_false
| L_undefined(*

Valuation of an atom

*)
val pp_lbool : Sidekick_core.Fmt.t -> lbool -> unit
module type ACTS = sig ... end

Actions available to the Plugin.

type acts = (module ACTS)

The type for a slice of assertions to assume/propagate in the theory.

module type THEORY_CDCL_T = sig ... end

Signature for theories to be given to the CDCL(T) solver

module type PLUGIN = sig ... end
module Solver : sig ... end

The external interface implemented by SAT solvers.

include module type of struct include Solver end
type clause
type plugin = (module Sidekick_sat__Sigs.PLUGIN)
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end

Main Solver Type

type t = solver

Main solver type, containing all state for solving.

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

Access the inner proof

val on_conflict : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_decision : t -> ( Sidekick_core.Lit.t, unit ) Sidekick_util.Event.t
val on_learnt : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_gc : t -> ( Sidekick_core.Lit.t array, unit ) Sidekick_util.Event.t

Types

type res =
| Sat of (module Sidekick_sat__Sigs.SAT_STATE)(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (module Sidekick_sat__Sigs.UNSAT_STATE with type clause = clause)(*

Returned when the solver reaches UNSAT, with a proof

*)

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : t -> Sidekick_core.Lit.t list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val add_clause : +Sidekick_sat (sidekick.Sidekick_sat)

Module Sidekick_sat

Main API

module Proof = Sidekick_proof
module type SAT_STATE = sig ... end

Solver in a "SATISFIABLE" state

type sat_state = (module SAT_STATE)

The type of values returned when the solver reaches a SAT state.

module type UNSAT_STATE = sig ... end

Solver in an "UNSATISFIABLE" state

type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause)

The type of values returned when the solver reaches an UNSAT state.

type same_sign = bool

This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.

type reason =
| Consequence of unit -> Sidekick_core.Lit.t list * Sidekick_proof.Pterm.delayed

The type of reasons for propagations of a lit f.

Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".

invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.

note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.

type lbool =
| L_true
| L_false
| L_undefined(*

Valuation of an atom

*)
val pp_lbool : Sidekick_core.Fmt.t -> lbool -> unit
module type ACTS = sig ... end

Actions available to the Plugin.

type acts = (module ACTS)

The type for a slice of assertions to assume/propagate in the theory.

module type THEORY_CDCL_T = sig ... end

Signature for theories to be given to the CDCL(T) solver

module type PLUGIN = sig ... end
module Solver : sig ... end

The external interface implemented by SAT solvers.

module Tracer : sig ... end

Tracer for clauses and literals

include module type of struct include Solver end
type clause
type plugin = (module Sidekick_sat__Sigs.PLUGIN)
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end

Main Solver Type

type t = solver

Main solver type, containing all state for solving.

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val tracer : t -> Tracer.t

Access the inner proof

val on_conflict : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_decision : t -> ( Sidekick_core.Lit.t, unit ) Sidekick_util.Event.t
val on_learnt : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_gc : t -> ( Sidekick_core.Lit.t array, unit ) Sidekick_util.Event.t

Types

type res =
| Sat of (module Sidekick_sat__Sigs.SAT_STATE)(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (module Sidekick_sat__Sigs.UNSAT_STATE with type clause = clause)(*

Returned when the solver reaches UNSAT, with a proof

*)

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : t -> Sidekick_core.Lit.t list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

Lower level addition of clauses

Lower level addition of clauses

val add_input_clause : t -> Sidekick_core.Lit.t list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> Sidekick_core.Lit.t array -> unit

Like add_clause_a but with justification of being an input clause

Solving

val solve : ?on_progress:( unit -> unit ) -> ?assumptions:Sidekick_core.Lit.t list -> @@ -25,13 +25,11 @@ (module Sidekick_sat__Sigs.PLUGIN)

Create a plugin

  • parameter push_level

    create a new backtrack level

  • parameter pop_levels

    Pop n levels of the plugin

  • parameter partial_check

    Assume the lits in the slice, possibly using the slice to push new lits to be propagated or to raising a conflict or to add new lemmas.

  • parameter final_check

    Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; if a conflict clause is added, search backtracks and then resumes.

val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> - ?tracer:Sidekick_core.Clause_tracer.t -> - proof:Sidekick_core.Proof_trace.t -> + tracer:Tracer.t -> plugin -> t

Create new solver

  • parameter theory

    the theory

  • parameter the

    proof

  • parameter size

    the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses.

val plugin_pure_sat : plugin
val create_pure_sat : ?stat:Sidekick_util.Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> - ?tracer:Sidekick_core.Clause_tracer.t -> - proof:Sidekick_core.Proof_trace.t -> + tracer:Tracer.t -> unit -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html b/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html index 3b87d502..a0ac3a1e 100644 --- a/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html +++ b/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html @@ -1,9 +1,9 @@ -ACTS (sidekick.Sidekick_sat.ACTS)

Module type Sidekick_sat.ACTS

Actions available to the Plugin.

The plugin provides callbacks for the SAT solver to use. These callbacks are provided with a (module ACTS) so they can modify the SAT solver by adding new lemmas, raise conflicts, etc.

val iter_assumptions : ( Sidekick_core.Lit.t -> unit ) -> unit

Traverse the new assumptions on the boolean trail.

val eval_lit : Sidekick_core.Lit.t -> lbool

Obtain current value of the given literal

val add_lit : ?default_pol:bool -> Sidekick_core.Lit.t -> unit

Map the given lit to an internal atom, which will be decided by the SAT solver.

val add_clause : +ACTS (sidekick.Sidekick_sat.ACTS)

Module type Sidekick_sat.ACTS

Actions available to the Plugin.

The plugin provides callbacks for the SAT solver to use. These callbacks are provided with a (module ACTS) so they can modify the SAT solver by adding new lemmas, raise conflicts, etc.

val proof_tracer : Sidekick_proof.Tracer.t
val iter_assumptions : ( Sidekick_core.Lit.t -> unit ) -> unit

Traverse the new assumptions on the boolean trail.

val eval_lit : Sidekick_core.Lit.t -> lbool

Obtain current value of the given literal

val add_lit : ?default_pol:bool -> Sidekick_core.Lit.t -> unit

Map the given lit to an internal atom, which will be decided by the SAT solver.

val add_clause : ?keep:bool -> Sidekick_core.Lit.t list -> - Sidekick_core.Proof_step.id -> + Sidekick_proof.Pterm.delayed -> unit

Add a clause to the solver.

  • parameter keep

    if true, the clause will be kept by the solver. Otherwise the solver is allowed to GC the clause and propose this partial model again.

    • C_use_allocator alloc puts the clause in the given allocator.

Raise a conflict, yielding control back to the solver. The list of atoms must be a valid theory lemma that is false in the current trail.

val propagate : Sidekick_core.Lit.t -> reason -> unit

Propagate a lit, i.e. the theory can evaluate the lit to be true (see the definition of eval_res

val add_decision_lit : Sidekick_core.Lit.t -> bool -> unit

Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/module-type-UNSAT_STATE/index.html b/dev/sidekick/Sidekick_sat/module-type-UNSAT_STATE/index.html index ce745a32..52a772cd 100644 --- a/dev/sidekick/Sidekick_sat/module-type-UNSAT_STATE/index.html +++ b/dev/sidekick/Sidekick_sat/module-type-UNSAT_STATE/index.html @@ -1,2 +1,2 @@ -UNSAT_STATE (sidekick.Sidekick_sat.UNSAT_STATE)

Module type Sidekick_sat.UNSAT_STATE

Solver in an "UNSATISFIABLE" state

type clause
val unsat_conflict : unit -> clause

Returns the unsat clause found at the toplevel

val unsat_assumptions : unit -> Sidekick_core.Lit.t Iter.t

Subset of assumptions responsible for "unsat"

val unsat_proof : unit -> Sidekick_core.Proof_term.step_id
\ No newline at end of file +UNSAT_STATE (sidekick.Sidekick_sat.UNSAT_STATE)

Module type Sidekick_sat.UNSAT_STATE

Solver in an "UNSATISFIABLE" state

type clause
val unsat_conflict : unit -> clause

Returns the unsat clause found at the toplevel

val unsat_assumptions : unit -> Sidekick_core.Lit.t Iter.t

Subset of assumptions responsible for "unsat"

val unsat_proof : unit -> Sidekick_proof.Step.id
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplify/index.html b/dev/sidekick/Sidekick_simplify/index.html index 4653e911..8411d0ec 100644 --- a/dev/sidekick/Sidekick_simplify/index.html +++ b/dev/sidekick/Sidekick_simplify/index.html @@ -1,11 +1,11 @@ -Sidekick_simplify (sidekick.Sidekick_simplify)

Module Sidekick_simplify

Term simplifier

type t

Create a simplifier

val clear : t -> unit

Reset internal cache, etc.

Access proof

type hook = +Sidekick_simplify (sidekick.Sidekick_simplify)

Module Sidekick_simplify

Term simplifier

type t

Create a simplifier

val clear : t -> unit

Reset internal cache, etc.

val proof : t -> Sidekick_proof.Tracer.t

Access proof

Given a Term.t, try to simplify it. Return None if it didn't change.

A simple example could be a hook that takes a Term.t t, and if t is app "+" (const x) (const y) where x and y are number, returns Some (const (x+y)), and None otherwise.

The simplifier will take care of simplifying the resulting Term.t further, caching (so that work is not duplicated in subterms), etc.

val add_hook : t -> hook -> unit
val normalize : + (Sidekick_core.Term.t * Sidekick_proof.Step.id Iter.t) option

Given a Term.t, try to simplify it. Return None if it didn't change.

A simple example could be a hook that takes a Term.t t, and if t is app "+" (const x) (const y) where x and y are number, returns Some (const (x+y)), and None otherwise.

The simplifier will take care of simplifying the resulting Term.t further, caching (so that work is not duplicated in subterms), etc.

val add_hook : t -> hook -> unit

Normalize a Term.t using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the Term.t.

val normalize_t : + (Sidekick_core.Term.t * Sidekick_proof.Step.id) option

Normalize a Term.t using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the Term.t.

Normalize a Term.t using all the hooks, along with a proof that the simplification is correct. returns t, ø if no simplification occurred.

\ No newline at end of file + Sidekick_core.Term.t * Sidekick_proof.Step.id option

Normalize a Term.t using all the hooks, along with a proof that the simplification is correct. returns t, ø if no simplification occurred.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Preprocess/index.html b/dev/sidekick/Sidekick_smt_solver/Preprocess/index.html index fe1dde3e..dc46d136 100644 --- a/dev/sidekick/Sidekick_smt_solver/Preprocess/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Preprocess/index.html @@ -1,7 +1,7 @@ Preprocess (sidekick.Sidekick_smt_solver.Preprocess)

Module Sidekick_smt_solver.Preprocess

Preprocessor

The preprocessor turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Every literal undergoes preprocessing. Typically some clauses are also added to the solver on the side, and some subterms are found to be foreign variables.

type t

Preprocessor

val create : ?stat:Sidekick_util.Stat.t -> - proof:Sigs.proof_trace -> + proof:Sigs.Proof.Tracer.t -> cc:Sigs.CC.t -> simplify:Sigs.Simplify.t -> Sigs.Term.store -> diff --git a/dev/sidekick/Sidekick_smt_solver/Preprocess/module-type-PREPROCESS_ACTS/index.html b/dev/sidekick/Sidekick_smt_solver/Preprocess/module-type-PREPROCESS_ACTS/index.html index 4452f939..278821e2 100644 --- a/dev/sidekick/Sidekick_smt_solver/Preprocess/module-type-PREPROCESS_ACTS/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Preprocess/module-type-PREPROCESS_ACTS/index.html @@ -1,2 +1,2 @@ -PREPROCESS_ACTS (sidekick.Sidekick_smt_solver.Preprocess.PREPROCESS_ACTS)

Module type Preprocess.PREPROCESS_ACTS

Actions given to preprocessor hooks

val proof : Sigs.proof_trace
val mk_lit : ?sign:bool -> Sigs.term -> Sigs.lit

mk_lit t creates a new literal for a boolean term t.

val add_clause : Sigs.lit list -> Sigs.step_id -> unit

pushes a new clause into the SAT solver.

val add_lit : ?default_pol:bool -> Sigs.lit -> unit

Ensure the literal will be decided/handled by the SAT solver.

\ No newline at end of file +PREPROCESS_ACTS (sidekick.Sidekick_smt_solver.Preprocess.PREPROCESS_ACTS)

Module type Preprocess.PREPROCESS_ACTS

Actions given to preprocessor hooks

val proof_tracer : Sigs.Proof.Tracer.t
val mk_lit : ?sign:bool -> Sigs.term -> Sigs.lit

mk_lit t creates a new literal for a boolean term t.

val add_clause : Sigs.lit list -> Sigs.step_id -> unit

pushes a new clause into the SAT solver.

val add_lit : ?default_pol:bool -> Sigs.lit -> unit

Ensure the literal will be decided/handled by the SAT solver.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Sigs/index.html b/dev/sidekick/Sidekick_smt_solver/Sigs/index.html index 5b50d9a9..bec6b3a4 100644 --- a/dev/sidekick/Sidekick_smt_solver/Sigs/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Sigs/index.html @@ -1,2 +1,7 @@ -Sigs (sidekick.Sidekick_smt_solver.Sigs)

Module Sidekick_smt_solver.Sigs

Signature for the main SMT solver types.

Theories and concrete solvers rely on an environment that defines several important types:

  • sorts
  • terms (to represent logic expressions and formulas)
  • a congruence closure instance
  • a bridge to some SAT solver

In this module we collect signatures defined elsewhere and define the module types for the main SMT solver.

include module type of struct include Sidekick_core end
module Fmt = Sidekick_core.Fmt

Re-exports from core-logic

module Const = Sidekick_core.Const
module Term = Sidekick_core.Term
module Gensym = Sidekick_core.Gensym

view

module Bool_view = Sidekick_core.Bool_view
module CC_view = Sidekick_core.CC_view
module Default_cc_view = Sidekick_core.Default_cc_view

Main modules

module Bvar = Sidekick_core.Bvar
module Lit = Sidekick_core.Lit
module Proof_step = Sidekick_core.Proof_step
module Proof_core = Sidekick_core.Proof_core
module Proof_sat = Sidekick_core.Proof_sat
module Proof_trace = Sidekick_core.Proof_trace
module Proof_term = Sidekick_core.Proof_term
module Subst = Sidekick_core.Subst
module Var = Sidekick_core.Var
module Box = Sidekick_core.Box
module Clause_tracer = Sidekick_core.Clause_tracer
exception Resource_exhausted
module Model = Sidekick_model
module Simplify = Sidekick_simplify
module CC = Sidekick_cc.CC
module E_node = Sidekick_cc.E_node
module CC_expl = Sidekick_cc.Expl
type term = Term.t
type ty = term
type value = Term.t
type lit = Lit.t
type term_store = Term.store
type proof_trace = Proof_trace.t
type step_id = Proof_step.id
type sat_acts = Sidekick_sat.acts
type th_combination_conflict = {
lits : lit list;
semantic : (bool * term * term) list;
}

Conflict obtained during theory combination. It involves equalities merged because of the current model so it's not a "true" conflict and doesn't need to kill the current trail.

module type ARG = sig ... end

Argument to pass to the functor Make in order to create a new Msat-based SMT solver.

\ No newline at end of file +Sigs (sidekick.Sidekick_smt_solver.Sigs)

Module Sidekick_smt_solver.Sigs

Signature for the main SMT solver types.

Theories and concrete solvers rely on an environment that defines several important types:

  • sorts
  • terms (to represent logic expressions and formulas)
  • a congruence closure instance
  • a bridge to some SAT solver

In this module we collect signatures defined elsewhere and define the module types for the main SMT solver.

include module type of struct include Sidekick_core end
module Fmt = Sidekick_core.Fmt

Re-exports from core-logic

module Const = Sidekick_core.Const
module Str_const = Sidekick_core.Str_const
module Term = Sidekick_core.Term

view

module Bool_view = Sidekick_core.Bool_view
module CC_view = Sidekick_core.CC_view
module Default_cc_view = Sidekick_core.Default_cc_view

Main modules

module Bvar = Sidekick_core.Bvar
module Lit = Sidekick_core.Lit
module Subst = Sidekick_core.Subst
module Var = Sidekick_core.Var
module Box = Sidekick_core.Box
module Gensym = Sidekick_core.Gensym
exception Resource_exhausted

Const decoders for traces

val const_decoders : + (string + * Sidekick_core_logic.Const.Ops.t + * ( Sidekick_core_logic__Types_.term Sidekick_util.Ser_decode.t -> + Sidekick_core_logic.Const.view Sidekick_util.Ser_decode.t )) + list
module Model = Sidekick_model
module Simplify = Sidekick_simplify
module CC = Sidekick_cc.CC
module E_node = Sidekick_cc.E_node
module CC_expl = Sidekick_cc.Expl
module Proof = Sidekick_proof
type term = Term.t
type ty = term
type value = Term.t
type lit = Lit.t
type term_store = Term.store
type step_id = Sidekick_proof.Step.id
type sat_acts = Sidekick_sat.acts
type th_combination_conflict = {
lits : lit list;
semantic : (bool * term * term) list;
}

Conflict obtained during theory combination. It involves equalities merged because of the current model so it's not a "true" conflict and doesn't need to kill the current trail.

module type ARG = sig ... end

Argument to pass to the functor Make in order to create a new Msat-based SMT solver.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Solver/index.html b/dev/sidekick/Sidekick_smt_solver/Solver/index.html index 1eeba185..76760d6d 100644 --- a/dev/sidekick/Sidekick_smt_solver/Solver/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Solver/index.html @@ -5,24 +5,22 @@ ?push_level:( 'th -> unit ) -> ?pop_levels:( 'th -> int -> unit ) -> unit -> - Theory.t

Helper to create a theory.

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> Sigs.Term.store
val proof : t -> Sigs.proof_trace
val create : + Theory.t

Helper to create a theory.

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> Sigs.Term.store
val tracer : t -> Tracer.t
val create : (module Sigs.ARG) -> ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> - ?tracer:Tracer.t -> - proof:Sigs.proof_trace -> + tracer:Tracer.t -> theories:Theory.t list -> Sigs.Term.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val create_default : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> - ?tracer:Tracer.t -> - proof:Sigs.proof_trace -> + tracer:Tracer.t -> theories:Theory.t list -> Sigs.Term.store -> unit -> - t

Create a new solver with the default CC view, and where all boolean subterms are mapped to boolean atoms.

val add_theory : t -> Theory.t -> unit

Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).

val add_theory_p : t -> 'a Theory.p -> 'a

Add the given theory and obtain its state

val add_theory_l : t -> Theory.t list -> unit
val mk_lit_t : t -> ?sign:bool -> Sigs.term -> Sigs.lit

mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.

The proof of |- lit = lit' is directly added to the solver's proof.

val add_clause : t -> Sigs.lit array -> Sigs.step_id -> unit

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

val add_clause_l : t -> Sigs.lit list -> Sigs.step_id -> unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sigs.ty -> unit
type res = Check_res.t =
| Sat of Sigs.Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sigs.lit Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_step_id : unit -> Sigs.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : + t

Create a new solver with the default CC view, and where all boolean subterms are mapped to boolean atoms.

val add_theory : t -> Theory.t -> unit

Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).

val add_theory_p : t -> 'a Theory.p -> 'a

Add the given theory and obtain its state

val add_theory_l : t -> Theory.t list -> unit
val mk_lit_t : t -> ?sign:bool -> Sigs.term -> Sigs.lit

mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.

The proof of |- lit = lit' is directly added to the solver's proof.

val add_clause : t -> Sigs.lit array -> Sigs.Proof.Pterm.delayed -> unit

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

val add_clause_l : t -> Sigs.lit list -> Sigs.Proof.Pterm.delayed -> unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sigs.ty -> unit
type res = Check_res.t =
| Sat of Sigs.Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sigs.lit Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sigs.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> diff --git a/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html b/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html index bc755548..8013fa83 100644 --- a/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html @@ -1,5 +1,5 @@ -Solver_internal (sidekick.Sidekick_smt_solver.Solver_internal)

Module Sidekick_smt_solver.Solver_internal

A view of the solver from a theory's point of view.

Theories should interact with the solver via this module, to assert new lemmas, propagate literals, access the congruence closure, etc.

type t

Main type for the SMT solver

type solver = t
val tst : t -> Sigs.term_store
val stats : t -> Sidekick_util.Stat.t
val proof : t -> Sigs.proof_trace

Access the proof object

val registry : t -> Registry.t

A solver contains a registry so that theories can share data

Actions for the theories

type theory_actions

Handle that the theories can use to perform actions.

Congruence Closure

val cc : t -> Sigs.CC.t

Congruence closure for this solver

Backtracking

include Sidekick_sigs.BACKTRACKABLE0 with type t := t
val n_levels : t -> int

Number of levels

val push_level : t -> unit

Push a backtracking point

val pop_levels : t -> int -> unit

pop_levels st n removes n levels

Interface to SAT

val to_sat_plugin : t -> (module Sidekick_sat.PLUGIN)

Simplifiers

type simplify_hook = Sigs.Simplify.hook
val simplifier : t -> Sigs.Simplify.t
val add_simplifier : t -> Sigs.Simplify.hook -> unit

Add a simplifier hook for preprocessing.

val simplify_t : t -> Sigs.term -> (Sigs.term * Sigs.step_id) option

Simplify input term, returns Some u if some simplification occurred.

val simp_t : t -> Sigs.term -> Sigs.term * Sigs.step_id option

simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)

Preprocessors

These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.

module type PREPROCESS_ACTS = Preprocess.PREPROCESS_ACTS
type preprocess_actions = (module PREPROCESS_ACTS)

Actions available to the preprocessor

type preprocess_hook = +Solver_internal (sidekick.Sidekick_smt_solver.Solver_internal)

Module Sidekick_smt_solver.Solver_internal

A view of the solver from a theory's point of view.

Theories should interact with the solver via this module, to assert new lemmas, propagate literals, access the congruence closure, etc.

type t

Main type for the SMT solver

type solver = t
val tst : t -> Sigs.term_store
val stats : t -> Sidekick_util.Stat.t
val tracer : t -> Tracer.t

Access the tracer object

val registry : t -> Registry.t

A solver contains a registry so that theories can share data

Actions for the theories

type theory_actions

Handle that the theories can use to perform actions.

Congruence Closure

val cc : t -> Sigs.CC.t

Congruence closure for this solver

Backtracking

include Sidekick_sigs.BACKTRACKABLE0 with type t := t
val n_levels : t -> int

Number of levels

val push_level : t -> unit

Push a backtracking point

val pop_levels : t -> int -> unit

pop_levels st n removes n levels

Interface to SAT

val to_sat_plugin : t -> (module Sidekick_sat.PLUGIN)

Simplifiers

type simplify_hook = Sigs.Simplify.hook
val simplifier : t -> Sigs.Simplify.t
val add_simplifier : t -> Sigs.Simplify.hook -> unit

Add a simplifier hook for preprocessing.

val simplify_t : t -> Sigs.term -> (Sigs.term * Sigs.step_id) option

Simplify input term, returns Some u if some simplification occurred.

val simp_t : t -> Sigs.term -> Sigs.term * Sigs.step_id option

simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)

Preprocessors

These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.

module type PREPROCESS_ACTS = Preprocess.PREPROCESS_ACTS
type preprocess_actions = (module PREPROCESS_ACTS)

Actions available to the preprocessor

type preprocess_hook = Preprocess.t -> is_sub:bool -> recurse:( Sigs.term -> Sigs.term ) -> @@ -13,28 +13,36 @@ t -> Sigs.lit array -> Sigs.step_id -> - Sigs.lit array * Sigs.step_id
val simplify_and_preproc_lit : t -> Sigs.lit -> Sigs.lit * Sigs.step_id option

Simplify literal then preprocess it

Finding foreign variables

val find_foreign : t -> Find_foreign.t
val on_find_foreign : t -> Find_foreign.hook -> unit

Add a hook for finding foreign variables

hooks for the theory

val raise_conflict : t -> theory_actions -> Sigs.lit list -> Sigs.step_id -> 'a

Give a conflict clause to the solver

val push_decision : t -> theory_actions -> Sigs.lit -> unit

Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.

val propagate : + Sigs.lit array * Sigs.step_id
val simplify_and_preproc_lit : t -> Sigs.lit -> Sigs.lit * Sigs.step_id option

Simplify literal then preprocess it

Finding foreign variables

val find_foreign : t -> Find_foreign.t
val on_find_foreign : t -> Find_foreign.hook -> unit

Add a hook for finding foreign variables

hooks for the theory

val raise_conflict : + t -> + theory_actions -> + Sigs.lit list -> + Sigs.Proof.Pterm.delayed -> + 'a

Give a conflict clause to the solver

val push_decision : t -> theory_actions -> Sigs.lit -> unit

Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.

val propagate : t -> theory_actions -> Sigs.lit -> - reason:( unit -> Sigs.lit list * Sigs.step_id ) -> + reason:( unit -> Sigs.lit list * Sigs.Proof.Pterm.delayed ) -> unit

Propagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology

val propagate_l : t -> theory_actions -> Sigs.lit -> Sigs.lit list -> - Sigs.step_id -> + Sigs.Proof.Pterm.delayed -> unit

Propagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology

val add_clause_temp : t -> theory_actions -> Sigs.lit list -> - Sigs.step_id -> + Sigs.Proof.Pterm.delayed -> unit

Add local clause to the SAT solver. This clause will be removed when the solver backtracks.

val add_clause_permanent : t -> theory_actions -> Sigs.lit list -> - Sigs.step_id -> - unit

Add toplevel clause to the SAT solver. This clause will not be backtracked.

val add_ty : t -> ty:Sigs.term -> unit

Declare a sort for the SMT solver

val mk_lit : t -> ?sign:bool -> Sigs.term -> Sigs.lit

Create a literal. This automatically preprocesses the term.

val add_lit : t -> theory_actions -> ?default_pol:bool -> Sigs.lit -> unit

Add the given literal to the SAT solver, so it gets assigned a boolean value.

  • parameter default_pol

    default polarity for the corresponding atom

val add_lit_t : t -> theory_actions -> ?sign:bool -> Sigs.term -> unit

Add the given (signed) bool term to the SAT solver, so it gets assigned a boolean value

val cc_find : t -> Sigs.E_node.t -> Sigs.E_node.t

Find representative of the node

val cc_are_equal : t -> Sigs.term -> Sigs.term -> bool

Are these two terms equal in the congruence closure?

val cc_resolve_expl : t -> Sigs.CC_expl.t -> Sigs.lit list * Sigs.step_id
val cc_add_term : t -> Sigs.term -> Sigs.E_node.t

Add/retrieve congruence closure node for this term. To be used in theories

val cc_mem_term : t -> Sigs.term -> bool

Return true if the term is explicitly in the congruence closure. To be used in theories

val on_cc_pre_merge : + Sigs.Proof.Pterm.delayed -> + unit

Add toplevel clause to the SAT solver. This clause will not be backtracked.

val add_ty : t -> ty:Sigs.term -> unit

Declare a sort for the SMT solver

val mk_lit : t -> ?sign:bool -> Sigs.term -> Sigs.lit

Create a literal. This automatically preprocesses the term.

val add_lit : t -> theory_actions -> ?default_pol:bool -> Sigs.lit -> unit

Add the given literal to the SAT solver, so it gets assigned a boolean value.

  • parameter default_pol

    default polarity for the corresponding atom

val add_lit_t : t -> theory_actions -> ?sign:bool -> Sigs.term -> unit

Add the given (signed) bool term to the SAT solver, so it gets assigned a boolean value

val cc_find : t -> Sigs.E_node.t -> Sigs.E_node.t

Find representative of the node

val cc_are_equal : t -> Sigs.term -> Sigs.term -> bool

Are these two terms equal in the congruence closure?

val cc_resolve_expl : + t -> + Sigs.CC_expl.t -> + Sigs.lit list * Sigs.Proof.Pterm.delayed
val cc_add_term : t -> Sigs.term -> Sigs.E_node.t

Add/retrieve congruence closure node for this term. To be used in theories

val cc_mem_term : t -> Sigs.term -> bool

Return true if the term is explicitly in the congruence closure. To be used in theories

val on_cc_pre_merge : t -> ( (Sigs.CC.t * Sigs.E_node.t * Sigs.E_node.t * Sigs.CC_expl.t) -> Sigs.CC.Handler_action.or_conflict ) -> @@ -50,7 +58,10 @@ ( (Sigs.CC.t * Sigs.E_node.t * Sigs.term) -> Sigs.CC.Handler_action.t list ) -> unit

Callback for when a term is a subterm of another term in the congruence closure

val on_cc_conflict : t -> ( Sigs.CC.ev_on_conflict -> unit ) -> unit

Callback called on every CC conflict

val on_cc_propagate : t -> - ( (Sigs.CC.t * Sigs.lit * ( unit -> Sigs.lit list * Sigs.step_id )) -> + ( (Sigs.CC.t + * Sigs.lit + * ( unit -> + Sigs.lit list * Sigs.Proof.Pterm.delayed )) -> Sigs.CC.Handler_action.t list ) -> unit

Callback called on every CC propagation

val on_new_ty : t -> ( Sigs.ty, unit ) Sidekick_util.Event.t

Add a callback for when new types are added via add_ty

val on_partial_check : t -> @@ -78,7 +89,6 @@ (module Sigs.ARG) -> stat:Sidekick_util.Stat.t -> tracer:Tracer.t -> - proof:Sigs.Proof_trace.t -> Sigs.Term.store -> unit -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Trace_reader/index.html b/dev/sidekick/Sidekick_smt_solver/Trace_reader/index.html index d6634eb4..c80f2b3d 100644 --- a/dev/sidekick/Sidekick_smt_solver/Trace_reader/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Trace_reader/index.html @@ -1,6 +1,6 @@ -Trace_reader (sidekick.Sidekick_smt_solver.Trace_reader)

Module Sidekick_smt_solver.Trace_reader

Read trace

module Tr = Sidekick_trace
type entry =
| Assert of Sidekick_core.Term.t
| Assert_clause of {
id : int;
c : Sidekick_core.Lit.t list;
}
val pp_entry : entry Sidekick_core.Fmt.printer
type t
val create : +Trace_reader (sidekick.Sidekick_smt_solver.Trace_reader)

Module Sidekick_smt_solver.Trace_reader

Read trace

module Proof = Sidekick_proof
module Tr = Sidekick_trace
type entry =
| Assert of Sidekick_core.Term.t
| Assert_clause of {
id : int;
c : Sidekick_core.Lit.t list;
p : Proof.Pterm.t option;
}
val pp_entry : entry Sidekick_core.Fmt.printer
type t
val create : ?const_decoders:Sidekick_core.Const.decoders list -> Sidekick_core.Term.store -> Tr.Source.t -> - t
val add_const_decoders : t -> Sidekick_core.Const.decoders -> unit
val decode : t -> tag:string -> Sidekick_util.Ser_value.t -> entry option
val decode_entry : t -> Tr.Entry_id.t -> entry option
\ No newline at end of file + t
val add_const_decoders : t -> Sidekick_core.Const.decoders -> unit
val term_trace_reader : t -> Sidekick_core.Term.Trace_reader.t
val decode : t -> tag:string -> Sidekick_util.Ser_value.t -> entry option
val decode_entry : t -> Tr.Entry_id.t -> entry option
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Tracer/class-concrete/index.html b/dev/sidekick/Sidekick_smt_solver/Tracer/class-concrete/index.html index 270712b6..4b0997be 100644 --- a/dev/sidekick/Sidekick_smt_solver/Tracer/class-concrete/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/class-concrete/index.html @@ -1,2 +1,2 @@ -concrete (sidekick.Sidekick_smt_solver.Tracer.concrete)

Class Tracer.concrete

Tracer emitting to a sink

inherit Sidekick_core.Term.Tracer.t
inherit Sidekick_core.Clause_tracer.t
method emit_assert_term : Sidekick_core.Term.t -> Tr.Entry_id.t

Emit an assertion

\ No newline at end of file +concrete (sidekick.Sidekick_smt_solver.Tracer.concrete)

Class Tracer.concrete

Tracer emitting to a sink

inherit Sidekick_core.Term.Tracer.t
inherit Sidekick_sat.Tracer.t
inherit Sidekick_proof.Tracer.t
method emit_assert_term : Sidekick_core.Term.t -> Tr.Entry_id.t

Emit an assertion

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Tracer/class-dummy/index.html b/dev/sidekick/Sidekick_smt_solver/Tracer/class-dummy/index.html index d98f1b5a..a2e522ad 100644 --- a/dev/sidekick/Sidekick_smt_solver/Tracer/class-dummy/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/class-dummy/index.html @@ -1,2 +1,2 @@ -dummy (sidekick.Sidekick_smt_solver.Tracer.dummy)

Class Tracer.dummy

Dummy tracer

inherit Sidekick_core.Term.Tracer.t
inherit Sidekick_core.Clause_tracer.t
method emit_assert_term : Sidekick_core.Term.t -> Tr.Entry_id.t

Emit an assertion

\ No newline at end of file +dummy (sidekick.Sidekick_smt_solver.Tracer.dummy)

Class Tracer.dummy

Dummy tracer

inherit Sidekick_core.Term.Tracer.t
inherit Sidekick_sat.Tracer.t
inherit Sidekick_proof.Tracer.t
method emit_assert_term : Sidekick_core.Term.t -> Tr.Entry_id.t

Emit an assertion

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Tracer/class-type-t/index.html b/dev/sidekick/Sidekick_smt_solver/Tracer/class-type-t/index.html index d0c144a0..9f7ed211 100644 --- a/dev/sidekick/Sidekick_smt_solver/Tracer/class-type-t/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/class-type-t/index.html @@ -1,2 +1,2 @@ -t (sidekick.Sidekick_smt_solver.Tracer.t)

Class type Tracer.t

inherit Sidekick_core.Term.Tracer.t
inherit Sidekick_core.Clause_tracer.t
method emit_assert_term : Sidekick_core.Term.t -> Tr.Entry_id.t

Emit an assertion

\ No newline at end of file +t (sidekick.Sidekick_smt_solver.Tracer.t)

Class type Tracer.t

inherit Sidekick_core.Term.Tracer.t
inherit Sidekick_sat.Tracer.t
inherit Sidekick_proof.Tracer.t
method emit_assert_term : Sidekick_core.Term.t -> Tr.Entry_id.t

Emit an assertion

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Tracer/index.html b/dev/sidekick/Sidekick_smt_solver/Tracer/index.html index b028e115..e589a027 100644 --- a/dev/sidekick/Sidekick_smt_solver/Tracer/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/index.html @@ -1,2 +1,12 @@ -Tracer (sidekick.Sidekick_smt_solver.Tracer)

Module Sidekick_smt_solver.Tracer

module Tr = Sidekick_trace
class type t = object ... end
class dummy : t

Dummy tracer

class concrete : Tr.Sink.t -> t

Tracer emitting to a sink

val dummy : t
val make : sink:Tr.Sink.t -> unit -> t
val assert_term : t -> Sidekick_core.Term.t -> Tr.Entry_id.t
val assert_term' : t -> Sidekick_core.Term.t -> unit
val assert_clause : t -> id:int -> Sidekick_core.Lit.t Iter.t -> Tr.Entry_id.t
val assert_clause' : t -> id:int -> Sidekick_core.Lit.t Iter.t -> unit
val delete_clause : t -> id:int -> Sidekick_core.Lit.t Iter.t -> unit
val unsat_clause : t -> id:int -> Tr.Entry_id.t
val unsat_clause' : t -> id:int -> unit
\ No newline at end of file +Tracer (sidekick.Sidekick_smt_solver.Tracer)

Module Sidekick_smt_solver.Tracer

Tracer for SMT solvers.

The tracer is used to track clauses and terms used or deduced during proof search.

module Tr = Sidekick_trace
module Proof = Sidekick_proof
class type t = object ... end
class dummy : t

Dummy tracer

class concrete : Tr.Sink.t -> t

Tracer emitting to a sink

val dummy : t
val make : sink:Tr.Sink.t -> unit -> t
val assert_term : t -> Sidekick_core.Term.t -> Tr.Entry_id.t
val assert_term' : t -> Sidekick_core.Term.t -> unit
val assert_clause : + t -> + id:int -> + Sidekick_core.Lit.t Iter.t -> + Proof.Step.id -> + Tr.Entry_id.t
val assert_clause' : + t -> + id:int -> + Sidekick_core.Lit.t Iter.t -> + Proof.Step.id -> + unit
val delete_clause : t -> id:int -> Sidekick_core.Lit.t Iter.t -> unit
val unsat_clause : t -> id:int -> Tr.Entry_id.t
val unsat_clause' : t -> id:int -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/index.html b/dev/sidekick/Sidekick_smt_solver/index.html index a641d4b3..bdca990b 100644 --- a/dev/sidekick/Sidekick_smt_solver/index.html +++ b/dev/sidekick/Sidekick_smt_solver/index.html @@ -1,2 +1,2 @@ -Sidekick_smt_solver (sidekick.Sidekick_smt_solver)

Module Sidekick_smt_solver

Core of the SMT solver using Sidekick_sat

Sidekick_sat (in src/sat/) is a modular SAT solver in pure OCaml.

This builds a SMT solver on top of it.

module Sigs : sig ... end

Signature for the main SMT solver types.

module Model = Sidekick_model
module Model_builder : sig ... end

Model Builder.

module Registry : sig ... end

Registry to extract values

module Solver_internal : sig ... end

A view of the solver from a theory's point of view.

module Solver : sig ... end

Main solver type, user facing.

module Theory : sig ... end

Signatures for theory plugins

module Theory_id : sig ... end
module Preprocess : sig ... end

Preprocessor

module Find_foreign : sig ... end

Find foreign variables.

module Tracer : sig ... end
module Trace_reader : sig ... end

Read trace

type theory = Theory.t
type solver = Solver.t
\ No newline at end of file +Sidekick_smt_solver (sidekick.Sidekick_smt_solver)

Module Sidekick_smt_solver

Core of the SMT solver using Sidekick_sat

Sidekick_sat (in src/sat/) is a modular SAT solver in pure OCaml.

This builds a SMT solver on top of it.

module Sigs : sig ... end

Signature for the main SMT solver types.

module Model = Sidekick_model
module Model_builder : sig ... end

Model Builder.

module Registry : sig ... end

Registry to extract values

module Solver_internal : sig ... end

A view of the solver from a theory's point of view.

module Solver : sig ... end

Main solver type, user facing.

module Theory : sig ... end

Signatures for theory plugins

module Theory_id : sig ... end
module Preprocess : sig ... end

Preprocessor

module Find_foreign : sig ... end

Find foreign variables.

module Tracer : sig ... end

Tracer for SMT solvers.

module Trace_reader : sig ... end

Read trace

type theory = Theory.t
type solver = Solver.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_dyn/Intf/index.html b/dev/sidekick/Sidekick_th_bool_dyn/Intf/index.html index 6c43b79d..4809eaf5 100644 --- a/dev/sidekick/Sidekick_th_bool_dyn/Intf/index.html +++ b/dev/sidekick/Sidekick_th_bool_dyn/Intf/index.html @@ -1,2 +1,2 @@ -Intf (sidekick.Sidekick_th_bool_dyn.Intf)

Module Sidekick_th_bool_dyn.Intf

module SMT = Sidekick_smt_solver
module Simplify = Sidekick_simplify
type 'a bool_view = 'a Sidekick_core.Bool_view.t =
| B_bool of bool
| B_not of 'a
| B_and of 'a list
| B_or of 'a list
| B_imply of 'a * 'a
| B_equiv of 'a * 'a
| B_xor of 'a * 'a
| B_eq of 'a * 'a
| B_neq of 'a * 'a
| B_ite of 'a * 'a * 'a
| B_atom of 'a

Boolean-oriented view of terms

module type ARG = sig ... end

Argument to the theory

\ No newline at end of file +Intf (sidekick.Sidekick_th_bool_dyn.Intf)

Module Sidekick_th_bool_dyn.Intf

module Proof = Sidekick_proof
module SMT = Sidekick_smt_solver
module Simplify = Sidekick_simplify
type 'a bool_view = 'a Sidekick_core.Bool_view.t =
| B_bool of bool
| B_not of 'a
| B_and of 'a list
| B_or of 'a list
| B_imply of 'a * 'a
| B_equiv of 'a * 'a
| B_xor of 'a * 'a
| B_eq of 'a * 'a
| B_neq of 'a * 'a
| B_ite of 'a * 'a * 'a
| B_atom of 'a

Boolean-oriented view of terms

module type ARG = sig ... end

Argument to the theory

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_dyn/Proof_rules/index.html b/dev/sidekick/Sidekick_th_bool_dyn/Proof_rules/index.html index 81d43f2d..cb45464d 100644 --- a/dev/sidekick/Sidekick_th_bool_dyn/Proof_rules/index.html +++ b/dev/sidekick/Sidekick_th_bool_dyn/Proof_rules/index.html @@ -1,2 +1,2 @@ -Proof_rules (sidekick.Sidekick_th_bool_dyn.Proof_rules)

Module Sidekick_th_bool_dyn.Proof_rules

val lemma_bool_tauto : lit list -> Sidekick_core.Proof_term.t

Boolean tautology lemma (clause)

val lemma_bool_c : string -> term list -> Sidekick_core.Proof_term.t

Basic boolean logic lemma for a clause |- c. proof_bool_c b name cs is the Proof_term.t designated by name.

val lemma_bool_equiv : term -> term -> Sidekick_core.Proof_term.t

Boolean tautology lemma (equivalence)

val lemma_ite_true : ite:term -> Sidekick_core.Proof_term.t

lemma a ==> ite a b c = b

val lemma_ite_false : ite:term -> Sidekick_core.Proof_term.t

lemma ¬a ==> ite a b c = c

\ No newline at end of file +Proof_rules (sidekick.Sidekick_th_bool_dyn.Proof_rules)

Module Sidekick_th_bool_dyn.Proof_rules

module Proof = Sidekick_proof
val lemma_bool_tauto : lit list -> Proof.Pterm.t

Boolean tautology lemma (clause)

val lemma_bool_c : string -> term list -> Proof.Pterm.t

Basic boolean logic lemma for a clause |- c. proof_bool_c b name cs is the Proof.Pterm.t designated by name.

val lemma_bool_equiv : term -> term -> Proof.Pterm.t

Boolean tautology lemma (equivalence)

val lemma_ite_true : ite:term -> Proof.Pterm.t

lemma a ==> ite a b c = b

val lemma_ite_false : ite:term -> Proof.Pterm.t

lemma ¬a ==> ite a b c = c

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Intf/index.html b/dev/sidekick/Sidekick_th_bool_static/Intf/index.html index 49e8de7d..ee8bfd5b 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Intf/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Intf/index.html @@ -1,2 +1,2 @@ -Intf (sidekick.Sidekick_th_bool_static.Intf)

Module Sidekick_th_bool_static.Intf

module SMT = Sidekick_smt_solver
module Simplify = Sidekick_simplify
type 'a bool_view = 'a Sidekick_core.Bool_view.t =
| B_bool of bool
| B_not of 'a
| B_and of 'a list
| B_or of 'a list
| B_imply of 'a * 'a
| B_equiv of 'a * 'a
| B_xor of 'a * 'a
| B_eq of 'a * 'a
| B_neq of 'a * 'a
| B_ite of 'a * 'a * 'a
| B_atom of 'a

Boolean-oriented view of terms

module type ARG = sig ... end

Argument to the theory

\ No newline at end of file +Intf (sidekick.Sidekick_th_bool_static.Intf)

Module Sidekick_th_bool_static.Intf

module Proof = Sidekick_proof
module SMT = Sidekick_smt_solver
module Simplify = Sidekick_simplify
type 'a bool_view = 'a Sidekick_core.Bool_view.t =
| B_bool of bool
| B_not of 'a
| B_and of 'a list
| B_or of 'a list
| B_imply of 'a * 'a
| B_equiv of 'a * 'a
| B_xor of 'a * 'a
| B_eq of 'a * 'a
| B_neq of 'a * 'a
| B_ite of 'a * 'a * 'a
| B_atom of 'a

Boolean-oriented view of terms

module type ARG = sig ... end

Argument to the theory

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Proof_rules/index.html b/dev/sidekick/Sidekick_th_bool_static/Proof_rules/index.html index ae0f3c8a..8bdf7890 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Proof_rules/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Proof_rules/index.html @@ -1,2 +1,2 @@ -Proof_rules (sidekick.Sidekick_th_bool_static.Proof_rules)

Module Sidekick_th_bool_static.Proof_rules

val lemma_bool_tauto : lit list -> Sidekick_core.Proof_term.t

Boolean tautology lemma (clause)

val lemma_bool_c : string -> term list -> Sidekick_core.Proof_term.t

Basic boolean logic lemma for a clause |- c. proof_bool_c b name cs is the Proof_term.t designated by name.

val lemma_bool_equiv : term -> term -> Sidekick_core.Proof_term.t

Boolean tautology lemma (equivalence)

val lemma_ite_true : ite:term -> Sidekick_core.Proof_term.t

lemma a ==> ite a b c = b

val lemma_ite_false : ite:term -> Sidekick_core.Proof_term.t

lemma ¬a ==> ite a b c = c

\ No newline at end of file +Proof_rules (sidekick.Sidekick_th_bool_static.Proof_rules)

Module Sidekick_th_bool_static.Proof_rules

module Proof = Sidekick_proof
val lemma_bool_tauto : lit list -> Proof.Pterm.t

Boolean tautology lemma (clause)

val lemma_bool_c : string -> term list -> Proof.Pterm.t

Basic boolean logic lemma for a clause |- c. proof_bool_c b name cs is the Proof_term.t designated by name.

val lemma_bool_equiv : term -> term -> Proof.Pterm.t

Boolean tautology lemma (equivalence)

val lemma_ite_true : ite:term -> Proof.Pterm.t

lemma a ==> ite a b c = b

val lemma_ite_false : ite:term -> Proof.Pterm.t

lemma ¬a ==> ite a b c = c

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/index.html index 42917499..54f436d7 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/index.html @@ -1,4 +1,4 @@ ARG (sidekick.Sidekick_th_cstor.ARG)

Module type Sidekick_th_cstor.ARG

\ No newline at end of file + ( Sidekick_core.Const.t, Sidekick_core.Term.t ) cstor_view
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_lra/Intf/index.html b/dev/sidekick/Sidekick_th_lra/Intf/index.html index 80f29d65..66fc668f 100644 --- a/dev/sidekick/Sidekick_th_lra/Intf/index.html +++ b/dev/sidekick/Sidekick_th_lra/Intf/index.html @@ -1,2 +1,2 @@ -Intf (sidekick.Sidekick_th_lra.Intf)

Module Sidekick_th_lra.Intf

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

Module Sidekick_th_lra.Intf

module SMT = Sidekick_smt_solver
module Proof = Sidekick_proof
module Predicate = Sidekick_simplex.Predicate
module Linear_expr = Sidekick_simplex.Linear_expr
module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf
module type INT = Sidekick_arith.INT
module type RATIONAL = Sidekick_arith.RATIONAL
module S_op = Sidekick_simplex.Op
type pred = Linear_expr_intf.bool_op =
| Leq
| Geq
| Lt
| Gt
| Eq
| Neq
type op = Linear_expr_intf.op =
| Plus
| Minus
type ('num, 'a) lra_view =
| LRA_pred of pred * 'a * 'a
| LRA_op of op * 'a * 'a
| LRA_mult of 'num * 'a
| LRA_const of 'num
| LRA_other of 'a
val map_view : ( 'a -> 'b ) -> ( 'c, 'a ) lra_view -> ( 'c, 'b ) lra_view
module type ARG = sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/Entry_id/index.html b/dev/sidekick/Sidekick_trace/Entry_id/index.html index 4165c54b..9538f8ec 100644 --- a/dev/sidekick/Sidekick_trace/Entry_id/index.html +++ b/dev/sidekick/Sidekick_trace/Entry_id/index.html @@ -1,2 +1,2 @@ -Entry_id (sidekick.Sidekick_trace.Entry_id)

Module Sidekick_trace.Entry_id

Entry in the sink.

This integer tag represent a single entry in a trace, for example a line if we serialized using line-separate json values. In general each entry has its own unique ID that is monotonically increasing with time.

type t = int
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : int CCHash.t
val to_int : 'a -> 'a
val of_int_unsafe : int -> t
val dummy : t

Dummy id

\ No newline at end of file +Entry_id (sidekick.Sidekick_trace.Entry_id)

Module Sidekick_trace.Entry_id

Entry in the sink.

This integer tag represent a single entry in a trace, for example a line if we serialized using line-separate json values. In general each entry has its own unique ID that is monotonically increasing with time.

type t = int
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : int CCHash.t
val pp : int CCFormat.printer
val to_int : 'a -> 'a
val of_int_unsafe : int -> t
val dummy : t

Dummy id

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/Entry_view/index.html b/dev/sidekick/Sidekick_trace/Entry_view/index.html deleted file mode 100644 index 5f3d54c1..00000000 --- a/dev/sidekick/Sidekick_trace/Entry_view/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Entry_view (sidekick.Sidekick_trace.Entry_view)

Module Sidekick_trace.Entry_view

type t = ..

Extensible type, each entry uses its own.

See Entry.t.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/index.html b/dev/sidekick/Sidekick_trace/index.html index b5d4bfd4..03a859ee 100644 --- a/dev/sidekick/Sidekick_trace/index.html +++ b/dev/sidekick/Sidekick_trace/index.html @@ -1,2 +1,2 @@ -Sidekick_trace (sidekick.Sidekick_trace)

Module Sidekick_trace

Tracing.

Sidekick should be able to emit traces of some or all of the events happening inside its components (SAT solver, SMT solver, theories, etc.).

Traces can be written to disk and read back later from another process.

The two initial intended use cases are:

  • proof production (trace all inferences; reconstruct a proof from them starting from the inference of false)
  • debugging (trace some inferences/internal states/partial models; double check them later)

Exports

module Entry_view : sig ... end
module Sink : sig ... end

An IO sink for serialization/tracing

module Source : sig ... end

Source to read a trace.

module Entry_id : sig ... end

Entry in the sink.

type entry_id = Entry_id.t
type entry_view = Entry_view.t = ..
\ No newline at end of file +Sidekick_trace (sidekick.Sidekick_trace)

Module Sidekick_trace

Tracing.

Sidekick should be able to emit traces of some or all of the events happening inside its components (SAT solver, SMT solver, theories, etc.).

Traces can be written to disk and read back later from another process.

The two initial intended use cases are:

  • proof production (trace all inferences; reconstruct a proof from them starting from the inference of false)
  • debugging (trace some inferences/internal states/partial models; double check them later)

Exports

module Sink : sig ... end

An IO sink for serialization/tracing

module Source : sig ... end

Source to read a trace.

module Entry_id : sig ... end

Entry in the sink.

type entry_id = Entry_id.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Int_id/Make/index.html b/dev/sidekick/Sidekick_util/Int_id/Make/index.html index 5581334d..7bec931a 100644 --- a/dev/sidekick/Sidekick_util/Int_id/Make/index.html +++ b/dev/sidekick/Sidekick_util/Int_id/Make/index.html @@ -1,2 +1,2 @@ -Make (sidekick.Sidekick_util.Int_id.Make)

Module Int_id.Make

Generate a new type for integer identifiers

Parameters

Signature

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

Module Int_id.Make

Generate a new type for integer identifiers

Parameters

Signature

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

Module type Int_id.S

type t = private int
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val to_int : t -> int
val of_int_unsafe : int -> t
\ No newline at end of file +S (sidekick.Sidekick_util.Int_id.S)

Module type Int_id.S

type t = private int
include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.ORD with type t := t
val compare : t -> t -> int
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val to_int : t -> int
val of_int_unsafe : int -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Ser_decode/index.html b/dev/sidekick/Sidekick_util/Ser_decode/index.html index 7f7eb22a..ac3147fc 100644 --- a/dev/sidekick/Sidekick_util/Ser_decode/index.html +++ b/dev/sidekick/Sidekick_util/Ser_decode/index.html @@ -1,2 +1,2 @@ -Ser_decode (sidekick.Sidekick_util.Ser_decode)

Module Sidekick_util.Ser_decode

Decoders for Ser_value.

Combinators to decode values.

module Error : sig ... end

Errors

Main combinators

type +'a t

Decode a value of type 'a

val int : int t
val bool : bool t
val string : string t
val return : 'a -> 'a t
val return_result : ( 'a, string ) Stdlib.result -> 'a t
val return_result_err : ( 'a, Error.t ) Stdlib.result -> 'a t
val fail : string -> 'a t
val failf : ( 'a, unit, string, 'b t ) Stdlib.format4 -> 'a
val fail_err : Error.t -> 'a t
val unwrap_opt : string -> 'a option -> 'a t

Unwrap option, or fail

val any : Ser_value.t t

Unwrap option, or fail

val list : 'a t -> 'a list t
val tup2 : 'a t -> 'b t -> ('a * 'b) t
val tup3 : 'a t -> 'b t -> 'c t -> ('a * 'b * 'c) t
val tup4 : 'a t -> 'b t -> 'c t -> 'd t -> ('a * 'b * 'c * 'd) t
val dict_field : string -> 'a t -> 'a t
val dict_field_opt : string -> 'a t -> 'a option t
val both : 'a t -> 'b t -> ('a * 'b) t
val reflect : 'a t -> Ser_value.t -> ( 'a, Error.t ) Stdlib.result t

reflect dec v returns the result of decoding v with dec

val reflect_or_fail : 'a t -> Ser_value.t -> 'a t
val try_l : 'a t list -> 'a t

try_l fs tries each f in fs turn by turn, until one succeeds

module Infix : sig ... end
include module type of Infix
val (>|=) : 'a t -> ( 'a -> 'b ) -> 'b t
val (>>=) : 'a t -> ( 'a -> 'b t ) -> 'b t
val let+ : 'a t -> ( 'a -> 'b ) -> 'b t
val and+ : 'a t -> 'b t -> ('a * 'b) t
val let* : 'a t -> ( 'a -> 'b t ) -> 'b t
val and* : 'a t -> 'b t -> ('a * 'b) t

Deserializing

val run : 'a t -> Ser_value.t -> ( 'a, Error.t ) Stdlib.result
val run_exn : 'a t -> Ser_value.t -> 'a
  • raises Error.Error

    in case of failure

\ No newline at end of file +Ser_decode (sidekick.Sidekick_util.Ser_decode)

Module Sidekick_util.Ser_decode

Decoders for Ser_value.

Combinators to decode values.

module Error : sig ... end

Errors

Main combinators

type +'a t

Decode a value of type 'a

val int : int t
val bool : bool t
val string : string t
val return : 'a -> 'a t
val return_result : ( 'a, string ) Stdlib.result -> 'a t
val return_result_err : ( 'a, Error.t ) Stdlib.result -> 'a t
val delay : ( unit -> 'a t ) -> 'a t
val fail : string -> 'a t
val failf : ( 'a, Stdlib.Format.formatter, unit, 'b t ) Stdlib.format4 -> 'a
val fail_err : Error.t -> 'a t
val unwrap_opt : string -> 'a option -> 'a t

Unwrap option, or fail

val any : Ser_value.t t
val list : 'a t -> 'a list t
val tup2 : 'a t -> 'b t -> ('a * 'b) t
val tup3 : 'a t -> 'b t -> 'c t -> ('a * 'b * 'c) t
val tup4 : 'a t -> 'b t -> 'c t -> 'd t -> ('a * 'b * 'c * 'd) t
val dict_field : string -> 'a t -> 'a t
val dict_field_opt : string -> 'a t -> 'a option t
val dict_field_or : 'a -> string -> 'a t -> 'a t
val both : 'a t -> 'b t -> ('a * 'b) t
val reflect : 'a t -> Ser_value.t -> ( 'a, Error.t ) Stdlib.result t

reflect dec v returns the result of decoding v with dec

val reflect_or_fail : 'a t -> Ser_value.t -> 'a t
val try_l : 'a t list -> 'a t

try_l fs tries each f in fs turn by turn, until one succeeds

module Infix : sig ... end
include module type of Infix
val (>|=) : 'a t -> ( 'a -> 'b ) -> 'b t
val (>>=) : 'a t -> ( 'a -> 'b t ) -> 'b t
val let+ : 'a t -> ( 'a -> 'b ) -> 'b t
val and+ : 'a t -> 'b t -> ('a * 'b) t
val let* : 'a t -> ( 'a -> 'b t ) -> 'b t
val and* : 'a t -> 'b t -> ('a * 'b) t

Deserializing

val run : 'a t -> Ser_value.t -> ( 'a, Error.t ) Stdlib.result
val run_exn : 'a t -> Ser_value.t -> 'a
  • raises Error.Error

    in case of failure

\ No newline at end of file diff --git a/dev/sidekick/index.html b/dev/sidekick/index.html index a10b30d4..eeaffcff 100644 --- a/dev/sidekick/index.html +++ b/dev/sidekick/index.html @@ -1,2 +1,2 @@ -index (sidekick.index)

sidekick index

Library sidekick.abstract-solver

The entry point of this library is the module: Sidekick_abstract_solver.

Library sidekick.arith

The entry point of this library is the module: Sidekick_arith.

Library sidekick.bencode

The entry point of this library is the module: Sidekick_bencode.

Library sidekick.cc

The entry point of this library is the module: Sidekick_cc.

Library sidekick.cc.plugin

The entry point of this library is the module: Sidekick_cc_plugin.

Library sidekick.core

The entry point of this library is the module: Sidekick_core.

Library sidekick.core-logic

The entry point of this library is the module: Sidekick_core_logic.

Library sidekick.drup

The entry point of this library is the module: Sidekick_drup.

Library sidekick.memtrace

The entry point of this library is the module: Sidekick_memtrace.

Library sidekick.mini-cc

The entry point of this library is the module: Sidekick_mini_cc.

Library sidekick.model

The entry point of this library is the module: Sidekick_model.

Library sidekick.quip

The entry point of this library is the module: Sidekick_quip.

Library sidekick.sat

The entry point of this library is the module: Sidekick_sat.

Library sidekick.sigs

The entry point of this library is the module: Sidekick_sigs.

Library sidekick.simplex

The entry point of this library is the module: Sidekick_simplex.

Library sidekick.simplify

The entry point of this library is the module: Sidekick_simplify.

Library sidekick.smt-solver

The entry point of this library is the module: Sidekick_smt_solver.

Library sidekick.tef

The entry point of this library is the module: Sidekick_tef.

Library sidekick.th-bool-dyn

The entry point of this library is the module: Sidekick_th_bool_dyn.

Library sidekick.th-bool-static

The entry point of this library is the module: Sidekick_th_bool_static.

Library sidekick.th-cstor

The entry point of this library is the module: Sidekick_th_cstor.

Library sidekick.th-data

The entry point of this library is the module: Sidekick_th_data.

Library sidekick.th-lra

The entry point of this library is the module: Sidekick_th_lra.

Library sidekick.th-ty-unin

The entry point of this library is the module: Sidekick_th_ty_unin.

Library sidekick.trace

The entry point of this library is the module: Sidekick_trace.

Library sidekick.util

The entry point of this library is the module: Sidekick_util.

Library sidekick.zarith

The entry point of this library is the module: Sidekick_zarith.

\ No newline at end of file +index (sidekick.index)

sidekick index

Library sidekick.abstract-solver

The entry point of this library is the module: Sidekick_abstract_solver.

Library sidekick.arith

The entry point of this library is the module: Sidekick_arith.

Library sidekick.bencode

The entry point of this library is the module: Sidekick_bencode.

Library sidekick.cc

The entry point of this library is the module: Sidekick_cc.

Library sidekick.cc.plugin

The entry point of this library is the module: Sidekick_cc_plugin.

Library sidekick.core

The entry point of this library is the module: Sidekick_core.

Library sidekick.core-logic

The entry point of this library is the module: Sidekick_core_logic.

Library sidekick.drup

The entry point of this library is the module: Sidekick_drup.

Library sidekick.memtrace

The entry point of this library is the module: Sidekick_memtrace.

Library sidekick.mini-cc

The entry point of this library is the module: Sidekick_mini_cc.

Library sidekick.model

The entry point of this library is the module: Sidekick_model.

Library sidekick.proof

The entry point of this library is the module: Sidekick_proof.

Library sidekick.quip

The entry point of this library is the module: Sidekick_quip.

Library sidekick.sat

The entry point of this library is the module: Sidekick_sat.

Library sidekick.sigs

The entry point of this library is the module: Sidekick_sigs.

Library sidekick.simplex

The entry point of this library is the module: Sidekick_simplex.

Library sidekick.simplify

The entry point of this library is the module: Sidekick_simplify.

Library sidekick.smt-solver

The entry point of this library is the module: Sidekick_smt_solver.

Library sidekick.tef

The entry point of this library is the module: Sidekick_tef.

Library sidekick.th-bool-dyn

The entry point of this library is the module: Sidekick_th_bool_dyn.

Library sidekick.th-bool-static

The entry point of this library is the module: Sidekick_th_bool_static.

Library sidekick.th-cstor

The entry point of this library is the module: Sidekick_th_cstor.

Library sidekick.th-data

The entry point of this library is the module: Sidekick_th_data.

Library sidekick.th-lra

The entry point of this library is the module: Sidekick_th_lra.

Library sidekick.th-ty-unin

The entry point of this library is the module: Sidekick_th_ty_unin.

Library sidekick.trace

The entry point of this library is the module: Sidekick_trace.

Library sidekick.util

The entry point of this library is the module: Sidekick_util.

Library sidekick.zarith

The entry point of this library is the module: Sidekick_zarith.

\ No newline at end of file