diff --git a/dev/sidekick-base/Sidekick_base/Data_ty/index.html b/dev/sidekick-base/Sidekick_base/Data_ty/index.html index 18eda63d..cd36cc29 100644 --- a/dev/sidekick-base/Sidekick_base/Data_ty/index.html +++ b/dev/sidekick-base/Sidekick_base/Data_ty/index.html @@ -1,2 +1,2 @@ -Data_ty (sidekick-base.Sidekick_base.Data_ty)

Module Sidekick_base.Data_ty

type select = Types_.select = {
select_id : ID.t;
select_cstor : Types_.cstor;
select_ty : Types_.ty lazy_t;
select_i : int;
}
type cstor = Types_.cstor = {
cstor_id : ID.t;
cstor_is_a : ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : Types_.data;
cstor_ty : Types_.ty lazy_t;
}
type t = Types_.data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : Types_.ty lazy_t;
}
type Types_.Const.view +=
| Data of Types_.data
| Cstor of cstor
| Select of select
| Is_a of cstor
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
module Select : sig ... end
module Cstor : sig ... end
val as_data : Types_.ty -> Types_.data option
val as_select : Types_.term -> select option
val as_cstor : Types_.term -> cstor option
val as_is_a : Types_.term -> cstor option
\ No newline at end of file +Data_ty (sidekick-base.Sidekick_base.Data_ty)

Module Sidekick_base.Data_ty

type select = Types_.select = {
select_id : ID.t;
select_cstor : Types_.cstor;
select_ty : Types_.ty lazy_t;
select_i : int;
}
type cstor = Types_.cstor = {
cstor_id : ID.t;
cstor_is_a : ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : Types_.data;
cstor_ty : Types_.ty lazy_t;
}
type t = Types_.data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : Types_.ty lazy_t;
}
type Types_.Const.view +=
| Data of Types_.data
| Cstor of cstor
| Select of select
| Is_a of cstor
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
module Select : sig ... end
module Cstor : sig ... end
val data_as_ty : t -> Types_.ty
val as_data : Types_.ty -> Types_.data option
val as_select : Types_.term -> select option
val as_cstor : Types_.term -> cstor option
val as_is_a : Types_.term -> cstor option
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Form/index.html b/dev/sidekick-base/Sidekick_base/Form/index.html index 72422e4e..aeb4f9d4 100644 --- a/dev/sidekick-base/Sidekick_base/Form/index.html +++ b/dev/sidekick-base/Sidekick_base/Form/index.html @@ -1,2 +1,2 @@ -Form (sidekick-base.Sidekick_base.Form)

Module Sidekick_base.Form

Formulas (boolean terms).

This module defines function symbols, constants, and views to manipulate boolean formulas in Sidekick_base. This is useful to have the ability to use boolean connectives instead of being limited to clauses; by using Sidekick_th_bool_static, the formulas are turned into clauses automatically for you.

type term = Types_.Term.t
type 'a 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
val view : term -> term view
val bool : Types_.Term.store -> bool -> term
val not_ : Types_.Term.store -> term -> term
val and_ : Types_.Term.store -> term -> term -> term
val or_ : Types_.Term.store -> term -> term -> term
val eq : Types_.Term.store -> term -> term -> term
val neq : Types_.Term.store -> term -> term -> term
val imply : Types_.Term.store -> term -> term -> term
val equiv : Types_.Term.store -> term -> term -> term
val xor : Types_.Term.store -> term -> term -> term
val ite : Types_.Term.store -> term -> term -> term -> term
val distinct_l : Types_.Term.store -> term list -> term
val and_l : Types_.Term.store -> term list -> term
val or_l : Types_.Term.store -> term list -> term
val imply_l : Types_.Term.store -> term list -> term -> term
val mk_of_view : Types_.Term.store -> term view -> term
\ No newline at end of file +Form (sidekick-base.Sidekick_base.Form)

Module Sidekick_base.Form

Formulas (boolean terms).

This module defines function symbols, constants, and views to manipulate boolean formulas in Sidekick_base. This is useful to have the ability to use boolean connectives instead of being limited to clauses; by using Sidekick_th_bool_static, the formulas are turned into clauses automatically for you.

type term = Types_.Term.t
type 'a 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
val view : term -> term view
val bool : Types_.Term.store -> bool -> term
val not_ : Types_.Term.store -> term -> term
val and_ : Types_.Term.store -> term -> term -> term
val or_ : Types_.Term.store -> term -> term -> term
val eq : Types_.Term.store -> term -> term -> term
val neq : Types_.Term.store -> term -> term -> term
val imply : Types_.Term.store -> term -> term -> term
val equiv : Types_.Term.store -> term -> term -> term
val xor : Types_.Term.store -> term -> term -> term
val ite : Types_.Term.store -> term -> term -> term -> term
val distinct_l : Types_.Term.store -> term list -> term
val const_decoders : Types_.Const.decoders
val and_l : Types_.Term.store -> term list -> term
val or_l : Types_.Term.store -> term list -> term
val imply_l : Types_.Term.store -> term list -> term -> term
val mk_of_view : Types_.Term.store -> term view -> term
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/ID/index.html b/dev/sidekick-base/Sidekick_base/ID/index.html index 5d4973ca..bebb775f 100644 --- a/dev/sidekick-base/Sidekick_base/ID/index.html +++ b/dev/sidekick-base/Sidekick_base/ID/index.html @@ -1,2 +1,2 @@ -ID (sidekick-base.Sidekick_base.ID)

Module Sidekick_base.ID

Unique Identifiers

We use generative identifiers everywhere in Sidekick_base. Unlike strings, there are no risk of collision: during parsing, a new declaration or definition should create a fresh ID.t and associate it with the string name, and later references should look into some hashtable or map to get the ID corresponding to a string.

This allows us to handle definition shadowing or binder shadowing easily.

type t

The opaque type of unique identifiers

val make : string -> t

make s creates a new identifier with name s and some internal information. It is different than any other identifier created before or after, even with the same name.

val makef : ( 'a, Stdlib.Format.formatter, unit, t ) Stdlib.format4 -> 'a

makef "foo %d bar %b" 42 true is like make (Format.asprintf "foo %d bar %b" 42 true).

val copy : t -> t

Fresh copy of the identifier, distinct from it, but with the same name.

val id : t -> int

Unique integer counter for this identifier.

val to_string : t -> string

Print identifier.

val to_string_full : t -> string

Printer name and unique counter for this ID.

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_name : t CCFormat.printer
val pp_full : t CCFormat.printer
module Map : CCMap.S with type key = t
module Set : CCSet.S with type elt = t
module Tbl : CCHashtbl.S with type key = t
\ No newline at end of file +ID (sidekick-base.Sidekick_base.ID)

Module Sidekick_base.ID

Unique Identifiers

We use generative identifiers everywhere in Sidekick_base. Unlike strings, there are no risk of collision: during parsing, a new declaration or definition should create a fresh ID.t and associate it with the string name, and later references should look into some hashtable or map to get the ID corresponding to a string.

This allows us to handle definition shadowing or binder shadowing easily.

type t

The opaque type of unique identifiers

val make : string -> t

make s creates a new identifier with name s and some internal information. It is different than any other identifier created before or after, even with the same name.

val makef : ( 'a, Stdlib.Format.formatter, unit, t ) Stdlib.format4 -> 'a

makef "foo %d bar %b" 42 true is like make (Format.asprintf "foo %d bar %b" 42 true).

val copy : t -> t

Fresh copy of the identifier, distinct from it, but with the same name.

val id : t -> int

Unique integer counter for this identifier.

val to_string : t -> string

Print identifier.

val to_string_full : t -> string

Printer name and unique counter for this ID.

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_name : t CCFormat.printer
val pp_full : t CCFormat.printer
module Map : CCMap.S with type key = t
module Set : CCSet.S with type elt = t
module Tbl : CCHashtbl.S with type key = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/LRA_term/index.html b/dev/sidekick-base/Sidekick_base/LRA_term/index.html index 08e13f6e..7dbbfba0 100644 --- a/dev/sidekick-base/Sidekick_base/LRA_term/index.html +++ b/dev/sidekick-base/Sidekick_base/LRA_term/index.html @@ -1,2 +1,2 @@ -LRA_term (sidekick-base.Sidekick_base.LRA_term)

Module Sidekick_base.LRA_term

module Pred : sig ... end
module Op : sig ... end
module View : sig ... end
val term_of_view : Sidekick_core.Term.store -> term View.t -> term
val has_ty_real : term -> bool
val mult_by : Sidekick_core.Term.store -> Q.t -> term -> term
val const : Sidekick_core.Term.store -> Q.t -> term

Helpers

val minus : Sidekick_core.Term.store -> term -> term -> term

View

val view : term -> term View.t

View as LRA

\ No newline at end of file +LRA_term (sidekick-base.Sidekick_base.LRA_term)

Module Sidekick_base.LRA_term

module Pred : sig ... end
module Op : sig ... end
val const_decoders : Sidekick_core.Const.decoders
module View : sig ... end
val term_of_view : Sidekick_core.Term.store -> term View.t -> term
val has_ty_real : term -> bool
val mult_by : Sidekick_core.Term.store -> Q.t -> term -> term
val const : Sidekick_core.Term.store -> Q.t -> term

Helpers

val minus : Sidekick_core.Term.store -> term -> term -> term

View

val view : term -> term View.t

View as LRA

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Solver/index.html b/dev/sidekick-base/Sidekick_base/Solver/index.html index 4e9a1c7c..28788237 100644 --- a/dev/sidekick-base/Sidekick_base/Solver/index.html +++ b/dev/sidekick-base/Sidekick_base/Solver/index.html @@ -12,6 +12,7 @@ (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 -> theories:Sidekick_smt_solver.Theory.t list -> Sidekick_smt_solver.Sigs.Term.store -> @@ -28,7 +29,7 @@ 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 the result to the solver as an 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

type res =
| Sat of Sidekick_smt_solver.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 : + 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 =
| 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 : ?on_exit:( unit -> unit ) list -> ?check:bool -> ?on_progress:( t -> unit ) -> @@ -41,6 +42,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 -> theories:Sidekick_smt_solver.Theory.t list -> Sidekick_smt_solver.Sigs.Term.store -> diff --git a/dev/sidekick-base/Sidekick_base/Term/index.html b/dev/sidekick-base/Sidekick_base/Term/index.html index 9cb9a25c..e994c650 100644 --- a/dev/sidekick-base/Sidekick_base/Term/index.html +++ b/dev/sidekick-base/Sidekick_base/Term/index.html @@ -1,5 +1,5 @@ -Term (sidekick-base.Sidekick_base.Term)

Module Sidekick_base.Term

include module type of struct include Sidekick_core.Term end
include module type of struct include Sidekick_core_logic.Term end
type nonrec var
type nonrec bvar
type t

A term, in the calculus of constructions

The store for terms.

The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).

type view =
| E_type of int
| E_var of var
| E_bound_var of bvar
| E_app of t * t
| E_lam of string * t * t
| E_pi of string * t * t

View.

A view is the shape of the root node of a term.

include Sidekick_sigs.EQ_ORD_HASH 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
val pp_debug : t Sidekick_util.Fmt.printer
val pp_debug_with_ids : t Sidekick_util.Fmt.printer

Containers

include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t

Utils

val view : t -> view
val unfold_app : t -> t * t list
val is_app : t -> bool
val is_const : t -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:( t -> unit ) -> t -> unit

iter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.

For example, in:

let x = 2 in
+Term (sidekick-base.Sidekick_base.Term)
Module Sidekick_base.Term
include module type of struct include Sidekick_core.Term end
include module type of struct include Sidekick_core_logic.Term end
type t
A term, in the calculus of constructions
The store for terms.
The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).
type view = 
| E_type of int
| E_var of var
| E_bound_var of bvar
| E_app of t * t
| E_lam of string * t * t
| E_pi of string * t * t
View.
A view is the shape of the root node of a term.
include Sidekick_sigs.EQ_ORD_HASH 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
val pp_debug : t Sidekick_util.Fmt.printer
val pp_debug_with_ids : t Sidekick_util.Fmt.printer
Containers
include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t
include Sidekick_sigs.WITH_WEAK with type t := t
module Weak_set = Sidekick_core.Term.Weak_set
module Weak_map = Sidekick_core.Term.Weak_map
Utils
val view : t -> view
val unfold_app : t -> t * t list
val is_app : t -> bool
val is_const : t -> bool
val is_pi : t -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:( t -> unit ) -> t -> unit
iter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
 let y = f x x in
 let z = g y x in
 z = z
the DAG has the following nodes:
n1: 2
@@ -11,7 +11,7 @@ n4: = n3 n3
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
val true_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
val false_ : Sidekick_core_logic.Term.store -> Sidekick_core_logic.Term.t
Sidekick_core_logic.Term.t

ite a b c is if a then b else c

val is_eq : Sidekick_core_logic.Term.t -> bool
val is_bool : Sidekick_core_logic.Term.t -> bool

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 : Sidekick_core_logic.Term.t -> bool option
type hook = + bool * Sidekick_core_logic.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 : Sidekick_core_logic.Term.t -> bool option

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

type hook = recurse: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

val view_as_cc : + 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 Trace_reader = Sidekick_core.Term.Trace_reader
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/Th_ty_unin/index.html b/dev/sidekick-base/Sidekick_base/Th_ty_unin/index.html new file mode 100644 index 00000000..cb47d406 --- /dev/null +++ b/dev/sidekick-base/Sidekick_base/Th_ty_unin/index.html @@ -0,0 +1,2 @@ + +Th_ty_unin (sidekick-base.Sidekick_base.Th_ty_unin)

Module Sidekick_base.Th_ty_unin

val theory : Solver.theory
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Th_uf/index.html b/dev/sidekick-base/Sidekick_base/Th_uf/index.html deleted file mode 100644 index 12bdf94e..00000000 --- a/dev/sidekick-base/Sidekick_base/Th_uf/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Th_uf (sidekick-base.Sidekick_base.Th_uf)

Module Sidekick_base.Th_uf

Theory of uninterpreted functions

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Ty/index.html b/dev/sidekick-base/Sidekick_base/Ty/index.html index 2f19b435..23e03ef6 100644 --- a/dev/sidekick-base/Sidekick_base/Ty/index.html +++ b/dev/sidekick-base/Sidekick_base/Ty/index.html @@ -1,10 +1,10 @@ -Ty (sidekick-base.Sidekick_base.Ty)

Module Sidekick_base.Ty

include module type of struct include Types_.Term end
include module type of struct include Sidekick_core_logic.Term end
type nonrec var
type nonrec bvar

The store for terms.

The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).

type view =
| E_type of int
| E_var of var
| E_bound_var of bvar

View.

A view is the shape of the root node of a term.

include Sidekick_sigs.EQ_ORD_HASH +Ty (sidekick-base.Sidekick_base.Ty)

Module Sidekick_base.Ty

include module type of struct include Types_.Term end
include module type of struct include Sidekick_core_logic.Term end

The store for terms.

The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).

type view =
| E_type of int
| E_var of var
| E_bound_var of bvar

View.

A view is the shape of the root node of a term.

include Sidekick_sigs.EQ_ORD_HASH with type t := Sidekick_core_logic__Types_.term
include Sidekick_sigs.EQ with type t := Sidekick_core_logic__Types_.term
include Sidekick_sigs.ORD with type t := Sidekick_core_logic__Types_.term
include Sidekick_sigs.HASH with type t := Sidekick_core_logic__Types_.term
val pp_debug : Sidekick_core_logic__Types_.term Sidekick_util.Fmt.printer
val pp_debug_with_ids : Sidekick_core_logic__Types_.term Sidekick_util.Fmt.printer

Containers

include Sidekick_sigs.WITH_SET_MAP_TBL - with type t := Sidekick_core_logic__Types_.term

Utils

val view : Sidekick_core_logic__Types_.term -> view
val unfold_app : + with type t := Sidekick_core_logic__Types_.term
include Sidekick_sigs.WITH_WEAK with type t := Sidekick_core_logic__Types_.term
module Weak_set = Sidekick_core.Term.Weak_set
module Weak_map = Sidekick_core.Term.Weak_map

Utils

val view : Sidekick_core_logic__Types_.term -> view
val unfold_app : Sidekick_core_logic__Types_.term -> - Sidekick_core_logic__Types_.term * Sidekick_core_logic__Types_.term list
val is_app : Sidekick_core_logic__Types_.term -> bool
val is_const : Sidekick_core_logic__Types_.term -> bool
val iter_dag : + Sidekick_core_logic__Types_.term * Sidekick_core_logic__Types_.term list
val is_app : Sidekick_core_logic__Types_.term -> bool
val is_const : Sidekick_core_logic__Types_.term -> bool
val is_pi : Sidekick_core_logic__Types_.term -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:( Sidekick_core_logic__Types_.term -> unit ) -> @@ -101,8 +101,10 @@ n4: = n3 n3
Sidekick_core_logic.Term.t

ite a b c is if a then b else c

val is_eq : Sidekick_core_logic.Term.t -> bool
val is_bool : Sidekick_core_logic.Term.t -> bool

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 : Sidekick_core_logic.Term.t -> bool option
type hook = + bool * Sidekick_core_logic.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 : Sidekick_core_logic.Term.t -> bool option

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

type hook = recurse: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

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

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 diff --git a/dev/sidekick-base/Sidekick_base/Types_/index.html b/dev/sidekick-base/Sidekick_base/Types_/index.html index 16e19b25..a69bcbb9 100644 --- a/dev/sidekick-base/Sidekick_base/Types_/index.html +++ b/dev/sidekick-base/Sidekick_base/Types_/index.html @@ -1,2 +1,2 @@ -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
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 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 diff --git a/dev/sidekick-base/Sidekick_base/Uconst/index.html b/dev/sidekick-base/Sidekick_base/Uconst/index.html index 75dffa6a..dcf27b3d 100644 --- a/dev/sidekick-base/Sidekick_base/Uconst/index.html +++ b/dev/sidekick-base/Sidekick_base/Uconst/index.html @@ -1,5 +1,5 @@ -Uconst (sidekick-base.Sidekick_base.Uconst)

Module Sidekick_base.Uconst

Uninterpreted constants

type ty = Types_.Term.t
type t = Types_.uconst = {
uc_id : ID.t;
uc_ty : ty;
}
val id : t -> ID.t
val ty : t -> ty
type Types_.Const.view +=
| Uconst of t
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 make : ID.t -> ty -> t

Make a new uninterpreted function.

val uconst : Types_.Term.store -> t -> Types_.Term.t
val uconst_of_id : Types_.Term.store -> ID.t -> ty -> Types_.Term.t
val uconst_of_id' : Types_.Term.store -> ID.t -> ty list -> ty -> Types_.Term.t
val uconst_of_str : +Uconst (sidekick-base.Sidekick_base.Uconst)

Module Sidekick_base.Uconst

Uninterpreted constants

type ty = Types_.Term.t
type t = Types_.uconst = {
uc_id : ID.t;
uc_ty : ty;
}
val id : t -> ID.t
val ty : t -> ty
type Types_.Const.view +=
| Uconst of t
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 make : ID.t -> ty -> t

Make a new uninterpreted function.

val uconst : Types_.Term.store -> t -> Types_.Term.t
val uconst_of_id : Types_.Term.store -> ID.t -> ty -> Types_.Term.t
val uconst_of_id' : Types_.Term.store -> ID.t -> ty list -> ty -> Types_.Term.t
val uconst_of_str : Types_.Term.store -> string -> ty list -> diff --git a/dev/sidekick-base/Sidekick_base/index.html b/dev/sidekick-base/Sidekick_base/index.html index ae1f8bc3..bc2afafb 100644 --- a/dev/sidekick-base/Sidekick_base/index.html +++ b/dev/sidekick-base/Sidekick_base/index.html @@ -1,2 +1,7 @@ -Sidekick_base (sidekick-base.Sidekick_base)

Module Sidekick_base

Sidekick base

This library is a starting point for writing concrete implementations of SMT solvers with Sidekick.

It provides a representation of terms, boolean formulas, linear arithmetic expressions, datatypes for the functors in Sidekick.

In addition, it has a notion of Statement. Statements are instructions for the SMT solver to do something, such as: define a new constant, declare a new constant, assert a formula as being true, set an option, check satisfiability of the set of statements added so far, etc. Logic formats such as SMT-LIB 2.6 are in fact based on a similar notion of statements, and a .smt2 files contains a list of statements.

module Types_ : sig ... end
module Term : sig ... end
module Const = Sidekick_core.Const
module Ty : sig ... end
module ID : sig ... end

Unique Identifiers

module Form : sig ... end

Formulas (boolean terms).

module Data_ty : sig ... end
module Cstor = Data_ty.Cstor
module Select = Data_ty.Select
module Statement : sig ... end

Statements.

module Solver : sig ... end
module Uconst : sig ... end

Uninterpreted constants

module Config : sig ... end

Configuration

module LRA_term : sig ... end
module Th_data : sig ... end

Theory of datatypes

module Th_bool : sig ... end

Reducing boolean formulas to clauses

module Th_lra : sig ... end

Theory of Linear Rational Arithmetic

module Th_uf : sig ... end

Theory of uninterpreted functions

val k_th_bool_config : [ `Dyn | `Static ] Config.Key.t
val th_bool : Config.t -> Solver.theory
val th_bool_dyn : Solver.theory
val th_bool_static : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
val th_uf : Solver.theory
\ No newline at end of file +Sidekick_base (sidekick-base.Sidekick_base)

Module Sidekick_base

Sidekick base

This library is a starting point for writing concrete implementations of SMT solvers with Sidekick.

It provides a representation of terms, boolean formulas, linear arithmetic expressions, datatypes for the functors in Sidekick.

In addition, it has a notion of Statement. Statements are instructions for the SMT solver to do something, such as: define a new constant, declare a new constant, assert a formula as being true, set an option, check satisfiability of the set of statements added so far, etc. Logic formats such as SMT-LIB 2.6 are in fact based on a similar notion of statements, and a .smt2 files contains a list of statements.

module Types_ : sig ... end
module Term : sig ... end
module Const = Sidekick_core.Const
module Ty : sig ... end
module ID : sig ... end

Unique Identifiers

module Form : sig ... end

Formulas (boolean terms).

module Data_ty : sig ... end
module Cstor = Data_ty.Cstor
module Select = Data_ty.Select
module Statement : sig ... end

Statements.

module Solver : sig ... end
module Uconst : sig ... end

Uninterpreted constants

module Config : sig ... end

Configuration

module LRA_term : sig ... end
module Th_data : sig ... end

Theory of datatypes

module Th_bool : sig ... end

Reducing boolean formulas to clauses

module Th_lra : sig ... end

Theory of Linear Rational Arithmetic

module Th_ty_unin : sig ... end
val k_th_bool_config : [ `Dyn | `Static ] Config.Key.t
val th_bool : Config.t -> Solver.theory
val th_bool_dyn : Solver.theory
val th_bool_static : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
val th_ty_unin : Solver.theory
val const_decoders : + (string + * Types_.Const.Ops.t + * ( Sidekick_core_logic__Types_.term Sidekick_util.Ser_decode.t -> + Types_.Const.view Sidekick_util.Ser_decode.t )) + list

All constant decoders

\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/index.html index b2a494fb..5c197c2b 100644 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib/Process/index.html @@ -1,5 +1,5 @@ -Process (sidekick-bin.Sidekick_smtlib.Process)

Module Sidekick_smtlib.Process

Process Statements

module Solver = Sidekick_base.Solver
val th_bool_dyn : Solver.theory
val th_bool_static : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
val th_uf : Solver.theory
type 'a or_error = ( 'a, string ) CCResult.t
module Check_cc : sig ... end
val process_stmt : +Process (sidekick-bin.Sidekick_smtlib.Process)

Module Sidekick_smtlib.Process

Process Statements

module Solver = Sidekick_base.Solver
val th_bool_dyn : Solver.theory
val th_bool_static : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
val th_ty_unin : Solver.theory
type 'a or_error = ( 'a, string ) CCResult.t
module Check_cc : sig ... end
val process_stmt : ?gc:bool -> ?restarts:bool -> ?pp_cnf:bool -> diff --git a/dev/sidekick/Sidekick_arith/module-type-INT/index.html b/dev/sidekick/Sidekick_arith/module-type-INT/index.html index 074c26c1..a2d0e3f1 100644 --- a/dev/sidekick/Sidekick_arith/module-type-INT/index.html +++ b/dev/sidekick/Sidekick_arith/module-type-INT/index.html @@ -1,2 +1,2 @@ -INT (sidekick.Sidekick_arith.INT)

Module type Sidekick_arith.INT

include NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file +INT (sidekick.Sidekick_arith.INT)

Module type Sidekick_arith.INT

include NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html b/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html index bd60e908..b715cfda 100644 --- a/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html +++ b/dev/sidekick/Sidekick_arith/module-type-INT_FULL/index.html @@ -1,2 +1,2 @@ -INT_FULL (sidekick.Sidekick_arith.INT_FULL)

Module type Sidekick_arith.INT_FULL

include INT
include NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
val sqrt : t -> t
val divexact : t -> t -> t
val (/) : t -> t -> t
val ediv : t -> t -> t

Euclidian division

val rem : t -> t -> t
val probab_prime : t -> bool
val pow : t -> int -> t
\ No newline at end of file +INT_FULL (sidekick.Sidekick_arith.INT_FULL)

Module type Sidekick_arith.INT_FULL

include INT
include NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
val sqrt : t -> t
val divexact : t -> t -> t
val (/) : t -> t -> t
val ediv : t -> t -> t

Euclidian division

val rem : t -> t -> t
val probab_prime : t -> bool
val pow : t -> int -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith/module-type-NUM/index.html b/dev/sidekick/Sidekick_arith/module-type-NUM/index.html index cce4c5f9..6d25d661 100644 --- a/dev/sidekick/Sidekick_arith/module-type-NUM/index.html +++ b/dev/sidekick/Sidekick_arith/module-type-NUM/index.html @@ -1,2 +1,2 @@ -NUM (sidekick.Sidekick_arith.NUM)

Module type Sidekick_arith.NUM

type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
\ No newline at end of file +NUM (sidekick.Sidekick_arith.NUM)

Module type Sidekick_arith.NUM

type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html b/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html index f0518623..56b31236 100644 --- a/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html +++ b/dev/sidekick/Sidekick_arith/module-type-RATIONAL/index.html @@ -1,2 +1,2 @@ -RATIONAL (sidekick.Sidekick_arith.RATIONAL)

Module type Sidekick_arith.RATIONAL

include NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file +RATIONAL (sidekick.Sidekick_arith.RATIONAL)

Module type Sidekick_arith.RATIONAL

include NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

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

Module Sidekick_bencode.Decode

val of_string : ?idx:int -> string -> (int * t) option

Decode string, and also return how many bytes were consumed.

  • parameter idx

    initial index (default 0)

val of_string_exn : ?idx:int -> string -> int * t

Parse string.

  • raises Error.Error

    if the string is not valid bencode.

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

Module Sidekick_bencode.Encode

val to_buffer : Stdlib.Buffer.t -> t -> unit
val to_string : t -> string
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_bencode/index.html b/dev/sidekick/Sidekick_bencode/index.html new file mode 100644 index 00000000..c5adde49 --- /dev/null +++ b/dev/sidekick/Sidekick_bencode/index.html @@ -0,0 +1,2 @@ + +Sidekick_bencode (sidekick.Sidekick_bencode)

Module Sidekick_bencode

module Encode : sig ... end
module Decode : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Box/index.html b/dev/sidekick/Sidekick_core/Box/index.html new file mode 100644 index 00000000..47b53ef0 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Box/index.html @@ -0,0 +1,5 @@ + +Box (sidekick.Sidekick_core.Box)

Module Sidekick_core.Box

box tst t makes a new constant that "boxes" t. This way it will be opaque.

val is_box : Sidekick_core_logic.Term.t -> bool
\ 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 new file mode 100644 index 00000000..6694d495 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Clause_tracer/class-dummy/index.html @@ -0,0 +1,2 @@ + +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 new file mode 100644 index 00000000..5683f316 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Clause_tracer/class-type-t/index.html @@ -0,0 +1,2 @@ + +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 new file mode 100644 index 00000000..09663846 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Clause_tracer/index.html @@ -0,0 +1,2 @@ + +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/Gensym/index.html b/dev/sidekick/Sidekick_core/Gensym/index.html index f388a636..4e4114d4 100644 --- a/dev/sidekick/Sidekick_core/Gensym/index.html +++ b/dev/sidekick/Sidekick_core/Gensym/index.html @@ -1,2 +1,2 @@ -Gensym (sidekick.Sidekick_core.Gensym)

Module Sidekick_core.Gensym

Fresh symbol generation

type t

Fresh symbol generator.

The theory needs to be able to create new terms with fresh names, to be used as placeholders for complex formulas during Tseitin encoding.

New (stateful) generator instance.

val fresh_term : ?opaque_to_cc:bool -> t -> pre:string -> ty -> term

Make a fresh term of the given type

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

Module Sidekick_core.Gensym

Fresh symbol generation

type t

Fresh symbol generator.

The theory needs to be able to create new terms with fresh names, to be used as placeholders for complex formulas during Tseitin encoding.

New (stateful) generator instance.

val fresh_term : t -> pre:string -> ty -> term

Make a fresh term of the given type

val reset : t -> unit

Reset to initial state

\ 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 new file mode 100644 index 00000000..40bdbd41 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Term/Trace_reader/index.html @@ -0,0 +1,13 @@ + +Trace_reader (sidekick.Sidekick_core.Term.Trace_reader)

Module Term.Trace_reader

module Tr = Sidekick_trace
type term_ref = Tr.entry_id
type t
val create : + ?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 -> + 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 diff --git a/dev/sidekick/Sidekick_core/Term/Tracer/class-concrete/index.html b/dev/sidekick/Sidekick_core/Term/Tracer/class-concrete/index.html new file mode 100644 index 00000000..20ee17a5 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Term/Tracer/class-concrete/index.html @@ -0,0 +1,2 @@ + +concrete (sidekick.Sidekick_core.Term.Tracer.concrete)

Class Tracer.concrete

Concrete implementation of t

method emit_term : Sidekick_core_logic.Term.t -> term_ref
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Term/Tracer/class-dummy/index.html b/dev/sidekick/Sidekick_core/Term/Tracer/class-dummy/index.html new file mode 100644 index 00000000..15a26c55 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Term/Tracer/class-dummy/index.html @@ -0,0 +1,2 @@ + +dummy (sidekick.Sidekick_core.Term.Tracer.dummy)

Class Tracer.dummy

Dummy implementation, returns Tr.Entry_id.dummy

inherit t
method emit_term : Sidekick_core_logic.Term.t -> term_ref
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Term/Tracer/class-type-t/index.html b/dev/sidekick/Sidekick_core/Term/Tracer/class-type-t/index.html new file mode 100644 index 00000000..d14090c8 --- /dev/null +++ b/dev/sidekick/Sidekick_core/Term/Tracer/class-type-t/index.html @@ -0,0 +1,2 @@ + +t (sidekick.Sidekick_core.Term.Tracer.t)

Class type Tracer.t

method emit_term : Sidekick_core_logic.Term.t -> term_ref
\ 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 new file mode 100644 index 00000000..2e5e575c --- /dev/null +++ b/dev/sidekick/Sidekick_core/Term/Tracer/index.html @@ -0,0 +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 diff --git a/dev/sidekick/Sidekick_core/Term/index.html b/dev/sidekick/Sidekick_core/Term/index.html index ec21831f..e9fb6674 100644 --- a/dev/sidekick/Sidekick_core/Term/index.html +++ b/dev/sidekick/Sidekick_core/Term/index.html @@ -1,5 +1,5 @@ -Term (sidekick.Sidekick_core.Term)

Module Sidekick_core.Term

include module type of struct include Sidekick_core_logic.Term end
type nonrec var
type nonrec bvar
type t

A term, in the calculus of constructions

type store

The store for terms.

The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).

type view =
| E_type of int
| E_var of var
| E_bound_var of bvar
| E_app of t * t
| E_lam of string * t * t
| E_pi of string * t * t

View.

A view is the shape of the root node of a term.

include Sidekick_sigs.EQ_ORD_HASH 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
val pp_debug : t Sidekick_util.Fmt.printer
val pp_debug_with_ids : t Sidekick_util.Fmt.printer

Containers

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

Utils

val view : t -> view
val unfold_app : t -> t * t list
val is_app : t -> bool
val is_const : t -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:( t -> unit ) -> t -> unit

iter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.

For example, in:

let x = 2 in
+Term (sidekick.Sidekick_core.Term)
Module Sidekick_core.Term
include module type of struct include Sidekick_core_logic.Term end
type t
A term, in the calculus of constructions
type store
The store for terms.
The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).
type view = 
| E_type of int
| E_var of var
| E_bound_var of bvar
| E_app of t * t
| E_lam of string * t * t
| E_pi of string * t * t
View.
A view is the shape of the root node of a term.
include Sidekick_sigs.EQ_ORD_HASH 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
val pp_debug : t Sidekick_util.Fmt.printer
val pp_debug_with_ids : t Sidekick_util.Fmt.printer
Containers
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
include Sidekick_sigs.WITH_WEAK with type t := t
module Weak_set : Stdlib.Weak.S with type data = t
module Weak_map : Stdlib.Ephemeron.S with type key = t
Utils
val view : t -> view
val unfold_app : t -> t * t list
val is_app : t -> bool
val is_const : t -> bool
val is_pi : t -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:( t -> unit ) -> t -> unit
iter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
 let y = f x x in
 let z = g y x in
 z = z
the DAG has the following nodes:
n1: 2
@@ -11,7 +11,7 @@ n4: = n3 n3
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
Sidekick_core_logic.Term.t

ite a b c is if a then b else c

val is_eq : Sidekick_core_logic.Term.t -> bool
val is_bool : Sidekick_core_logic.Term.t -> bool

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 : Sidekick_core_logic.Term.t -> bool option
type hook = + bool * Sidekick_core_logic.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 : Sidekick_core_logic.Term.t -> bool option

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

type hook = recurse: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

\ 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

module Tracer : sig ... end

Emit terms in traces.

module Trace_reader : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/index.html b/dev/sidekick/Sidekick_core/index.html index b55669f5..9d323b63 100644 --- a/dev/sidekick/Sidekick_core/index.html +++ b/dev/sidekick/Sidekick_core/index.html @@ -1,2 +1,2 @@ -Sidekick_core (sidekick.Sidekick_core)

Module Sidekick_core

Main Signatures.

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

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

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.

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:

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

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 diff --git a/dev/sidekick/Sidekick_core_logic/Bvar/index.html b/dev/sidekick/Sidekick_core_logic/Bvar/index.html index 95874fe0..e78f3055 100644 --- a/dev/sidekick/Sidekick_core_logic/Bvar/index.html +++ b/dev/sidekick/Sidekick_core_logic/Bvar/index.html @@ -1,2 +1,2 @@ -Bvar (sidekick.Sidekick_core_logic.Bvar)

Module Sidekick_core_logic.Bvar

Bound variable

type t = {
bv_idx : int;
bv_ty : Sidekick_core_logic__Types_.term;
}
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val make : int -> Sidekick_core_logic__Types_.term -> t
val ty : t -> Sidekick_core_logic__Types_.term
\ No newline at end of file +Bvar (sidekick.Sidekick_core_logic.Bvar)

Module Sidekick_core_logic.Bvar

Bound variable

type t = {
bv_idx : int;
bv_ty : Sidekick_core_logic__Types_.term;
}
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val make : int -> Sidekick_core_logic__Types_.term -> t
val idx : t -> int
val ty : t -> Sidekick_core_logic__Types_.term
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core_logic/Const/Ops/index.html b/dev/sidekick/Sidekick_core_logic/Const/Ops/index.html new file mode 100644 index 00000000..8b2c2d56 --- /dev/null +++ b/dev/sidekick/Sidekick_core_logic/Const/Ops/index.html @@ -0,0 +1,6 @@ + +Ops (sidekick.Sidekick_core_logic.Const.Ops)

Module Const.Ops

type t = {
pp : Sidekick_core_logic__Types_.const_view Sidekick_util.Fmt.printer;(*

Pretty-print constant

*)
equal : Sidekick_core_logic__Types_.const_view -> + Sidekick_core_logic__Types_.const_view -> + bool;(*

Equality of constant with any other constant

*)
hash : Sidekick_core_logic__Types_.const_view -> int;(*

Hash constant

*)
ser : ( Sidekick_core_logic__Types_.term -> Sidekick_util.Ser_value.t ) -> + Sidekick_core_logic__Types_.const_view -> + string * Sidekick_util.Ser_value.t;(*

Serialize a constant, along with a tag to recognize it.

*)
}
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core_logic/Const/index.html b/dev/sidekick/Sidekick_core_logic/Const/index.html index ba68c814..9c07f6c8 100644 --- a/dev/sidekick/Sidekick_core_logic/Const/index.html +++ b/dev/sidekick/Sidekick_core_logic/Const/index.html @@ -1,2 +1,10 @@ -Const (sidekick.Sidekick_core_logic.Const)

Module Sidekick_core_logic.Const

Constants.

Constants are logical symbols, defined by the user thanks to an open type

type view = ..
module type DYN_OPS = sig ... end
type ops = (module DYN_OPS)
type t = {
c_view : view;
c_ops : ops;
c_ty : Sidekick_core_logic__Types_.term;
}
val view : t -> view
val make : view -> ops -> ty:Sidekick_core_logic__Types_.term -> t
val ty : t -> Sidekick_core_logic__Types_.term
include Sidekick_sigs.EQ_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
\ No newline at end of file +Const (sidekick.Sidekick_core_logic.Const)

Module Sidekick_core_logic.Const

Constants.

Constants are logical symbols, defined by the user thanks to an open type

type view = ..
module Ops : sig ... end
type t = {
c_view : view;
c_ops : Ops.t;
c_ty : Sidekick_core_logic__Types_.term;
}
val view : t -> view
val make : view -> Ops.t -> ty:Sidekick_core_logic__Types_.term -> t
val ser : + ser_t:( Sidekick_core_logic__Types_.term -> Sidekick_util.Ser_value.t ) -> + t -> + string * Sidekick_util.Ser_value.t
val ty : t -> Sidekick_core_logic__Types_.term
type decoders = + (string + * Ops.t + * ( Sidekick_core_logic__Types_.term Sidekick_util.Ser_decode.t -> + view Sidekick_util.Ser_decode.t )) + list

Decoders for constants: given a term store, return a list of supported tags, and for each tag, a decoder for constants that have this particular tag.

include Sidekick_sigs.EQ_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core_logic/Const/module-type-DYN_OPS/index.html b/dev/sidekick/Sidekick_core_logic/Const/module-type-DYN_OPS/index.html deleted file mode 100644 index 5a7d6719..00000000 --- a/dev/sidekick/Sidekick_core_logic/Const/module-type-DYN_OPS/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -DYN_OPS (sidekick.Sidekick_core_logic.Const.DYN_OPS)

Module type Const.DYN_OPS

val pp : view Sidekick_util.Fmt.printer
val equal : view -> view -> bool
val hash : view -> int
val opaque_to_cc : view -> bool
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core_logic/Str_const/index.html b/dev/sidekick/Sidekick_core_logic/Str_const/index.html index 243ea602..51db6831 100644 --- a/dev/sidekick/Sidekick_core_logic/Str_const/index.html +++ b/dev/sidekick/Sidekick_core_logic/Str_const/index.html @@ -1,5 +1,5 @@ -Str_const (sidekick.Sidekick_core_logic.Str_const)

Module Sidekick_core_logic.Str_const

Basic string constants.

These constants are a string name, coupled with a type.

type Sidekick_core_logic__Types_.const_view +=
| Str of string
val make : +Str_const (sidekick.Sidekick_core_logic.Str_const)

Module Sidekick_core_logic.Str_const

Basic string constants.

These constants are a string name, coupled with a type.

type Sidekick_core_logic__Types_.const_view +=
| Str of string
val const_decoders : Const.decoders
val make : string -> ty:Sidekick_core_logic__Types_.term -> Sidekick_core_logic__Types_.const
\ 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 84578ba2..27223a03 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 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
\ 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
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 diff --git a/dev/sidekick/Sidekick_core_logic/Term/index.html b/dev/sidekick/Sidekick_core_logic/Term/index.html index e66b2a52..c335fe37 100644 --- a/dev/sidekick/Sidekick_core_logic/Term/index.html +++ b/dev/sidekick/Sidekick_core_logic/Term/index.html @@ -1,5 +1,5 @@ -Term (sidekick.Sidekick_core_logic.Term)

Module Sidekick_core_logic.Term

Core logic terms.

The core terms are expressions in the calculus of constructions, with no universe polymorphism nor cumulativity. It should be fast, with hashconsing; and simple enough (no inductives, no universe trickery).

It is intended to be the foundation for user-level terms and types and formulas.

type nonrec var
type nonrec bvar
type nonrec term
type t = term

A term, in the calculus of constructions

type store

The store for terms.

The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).

type view =
| E_type of int
| E_var of var
| E_bound_var of bvar
| E_app of t * t
| E_app_fold of {
f : term;(*

function to fold

*)
args : term list;(*

Arguments to the fold

*)
acc0 : term;(*

initial accumulator

*)
}
| E_lam of string * t * t
| E_pi of string * t * t

View.

A view is the shape of the root node of a term.

include Sidekick_sigs.EQ_ORD_HASH 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
val pp_debug : t Sidekick_util.Fmt.printer
val pp_debug_with_ids : t Sidekick_util.Fmt.printer

Containers

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

Utils

val view : t -> view
val unfold_app : t -> t * t list
val is_app : t -> bool
val is_const : t -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:( t -> unit ) -> t -> unit

iter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.

For example, in:

let x = 2 in
+Term (sidekick.Sidekick_core_logic.Term)
Module Sidekick_core_logic.Term
Core logic terms.
The core terms are expressions in the calculus of constructions, with no universe polymorphism nor cumulativity. It should be fast, with hashconsing; and simple enough (no inductives, no universe trickery).
It is intended to be the foundation for user-level terms and types and formulas.
type var = Var.t
type bvar = Bvar.t
type nonrec term
type t = term
A term, in the calculus of constructions
type store
The store for terms.
The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).
type view = 
| E_type of int
| E_var of var
| E_bound_var of bvar
| E_app of t * t
| E_app_fold of {
f : term;(*
function to fold
*)
args : term list;(*
Arguments to the fold
*)
acc0 : term;(*
initial accumulator
*)
}
| E_lam of string * t * t
| E_pi of string * t * t
View.
A view is the shape of the root node of a term.
include Sidekick_sigs.EQ_ORD_HASH 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
val pp_debug : t Sidekick_util.Fmt.printer
val pp_debug_with_ids : t Sidekick_util.Fmt.printer
Containers
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
include Sidekick_sigs.WITH_WEAK with type t := t
module Weak_set : Stdlib.Weak.S with type data = t
module Weak_map : Stdlib.Ephemeron.S with type key = t
Utils
val view : t -> view
val unfold_app : t -> t * t list
val is_app : t -> bool
val is_const : t -> bool
val is_pi : t -> bool
val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:( t -> unit ) -> t -> unit
iter_dag t ~f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
 let y = f x x in
 let z = g y x in
 z = z
the DAG has the following nodes:
n1: 2
diff --git a/dev/sidekick/Sidekick_core_logic/index.html b/dev/sidekick/Sidekick_core_logic/index.html
index 852e8763..e62ad73b 100644
--- a/dev/sidekick/Sidekick_core_logic/index.html
+++ b/dev/sidekick/Sidekick_core_logic/index.html
@@ -1,2 +1,2 @@
 
-Sidekick_core_logic (sidekick.Sidekick_core_logic)
Module Sidekick_core_logic
module Term : sig ... end
Core logic terms.
module Var : sig ... end
Free variable
module Bvar : sig ... end
Bound variable
module Const : sig ... end
Constants.
module Subst : sig ... end
Substitutions
module T_builtins : sig ... end
Core builtins
module Store = Term.Store
module Str_const : sig ... end
Basic string constants.

\ No newline at end of file
+Sidekick_core_logic (sidekick.Sidekick_core_logic)
Module Sidekick_core_logic
module Term : sig ... end
Core logic terms.
module Var : sig ... end
Free variable
module Bvar : sig ... end
Bound variable
module Const : sig ... end
Constants.
module Subst : sig ... end
Substitutions
module T_builtins : sig ... end
Core builtins
module Ser_sink = Sidekick_util.Ser_sink
module Store = Term.Store
module Str_const : sig ... end
Basic string constants.

\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_model/.dummy b/dev/sidekick/Sidekick_model/.dummy
new file mode 100644
index 00000000..e69de29b
diff --git a/dev/sidekick/Sidekick_model/index.html b/dev/sidekick/Sidekick_model/index.html
new file mode 100644
index 00000000..97dddfd6
--- /dev/null
+++ b/dev/sidekick/Sidekick_model/index.html
@@ -0,0 +1,2 @@
+
+Sidekick_model (sidekick.Sidekick_model)
Module Sidekick_model
Models
A model can be produced when the solver is found to be in a satisfiable state after a call to solve.
type t
val empty : t
val is_empty : t -> bool
val mem : t -> Sidekick_core.Term.t -> bool
val keys : t -> Sidekick_core.Term.t Iter.t
val to_iter : t -> (Sidekick_core.Term.t * Sidekick_core.Term.t) Iter.t
include Sidekick_sigs.PRINT with type t := t

\ 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 5e5e2be2..9216daab 100644
--- a/dev/sidekick/Sidekick_sat/Solver/index.html
+++ b/dev/sidekick/Sidekick_sat/Solver/index.html
@@ -25,11 +25,13 @@
   (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 ->
   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 ->
   unit ->
   t

\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat/index.html b/dev/sidekick/Sidekick_sat/index.html
index 7883e27d..51d31902 100644
--- a/dev/sidekick/Sidekick_sat/index.html
+++ b/dev/sidekick/Sidekick_sat/index.html
@@ -25,11 +25,13 @@
   (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 -> 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 -> unit -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sigs/index.html b/dev/sidekick/Sidekick_sigs/index.html index 301123f8..07ccdc10 100644 --- a/dev/sidekick/Sidekick_sigs/index.html +++ b/dev/sidekick/Sidekick_sigs/index.html @@ -1,2 +1,2 @@ -Sidekick_sigs (sidekick.Sidekick_sigs)

Module Sidekick_sigs

module type EQ = sig ... end
module type ORD = sig ... end
module type HASH = sig ... end
type 'a printer = Stdlib.Format.formatter -> 'a -> unit
module type PRINT = sig ... end
module type EQ_HASH_PRINT = sig ... end
module type EQ_ORD_HASH_PRINT = sig ... end
module type EQ_ORD_HASH = sig ... end
module type DYN_BACKTRACKABLE = sig ... end
module type BACKTRACKABLE0 = sig ... end
module type BACKTRACKABLE1 = sig ... end
module type BACKTRACKABLE1_CB = sig ... end
module type WITH_SET_MAP_TBL = sig ... end
\ No newline at end of file +Sidekick_sigs (sidekick.Sidekick_sigs)

Module Sidekick_sigs

module type EQ = sig ... end
module type ORD = sig ... end
module type HASH = sig ... end
type 'a printer = Stdlib.Format.formatter -> 'a -> unit
module type PRINT = sig ... end
module type EQ_HASH_PRINT = sig ... end
module type EQ_ORD_HASH_PRINT = sig ... end
module type EQ_ORD_HASH = sig ... end
module type DYN_BACKTRACKABLE = sig ... end
module type BACKTRACKABLE0 = sig ... end
module type BACKTRACKABLE1 = sig ... end
module type BACKTRACKABLE1_CB = sig ... end
module type WITH_SET_MAP_TBL = sig ... end
module type WITH_WEAK = sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sigs/module-type-WITH_WEAK/index.html b/dev/sidekick/Sidekick_sigs/module-type-WITH_WEAK/index.html new file mode 100644 index 00000000..f2354765 --- /dev/null +++ b/dev/sidekick/Sidekick_sigs/module-type-WITH_WEAK/index.html @@ -0,0 +1,2 @@ + +WITH_WEAK (sidekick.Sidekick_sigs.WITH_WEAK)

Module type Sidekick_sigs.WITH_WEAK

type t
module Weak_set : Stdlib.Weak.S with type data = t
module Weak_map : Stdlib.Ephemeron.S with type key = t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Comb/index.html b/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Comb/index.html index 5ca0aa54..70929231 100644 --- a/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Comb/index.html +++ b/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Comb/index.html @@ -1,2 +1,2 @@ -Comb (sidekick.Sidekick_simplex.Linear_expr.Make.Comb)

Module Make.Comb

Combinations.

This module defines linear combnations as mapping from variables to coefficients. This allows for very fast computations.

type t

The type of linear combinations.

val compare : t -> t -> int

Comparisons on linear combinations.

val pp : t Sidekick_util.Fmt.printer

Printer for linear combinations.

val is_empty : t -> bool

Is the given expression empty ?

Creation
val empty : t

The empty linear combination.

val monomial : C.t -> var -> t

monome n v creates the linear combination n * v

val monomial1 : var -> t

monome1 v creates the linear combination 1 * v

val as_singleton : t -> (C.t * var) option

as_singleton l returns Some (c,x) if l = c * x, None otherwise

val add : C.t -> var -> t -> t

add n v t adds the monome n * v to the combination t.

module Infix : sig ... end

Infix operations on combinations

Include the previous module.

include module type of Infix

Infix operations on combinations

This module defines usual operations on linear combinations, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between combinations.

val (-) : t -> t -> t

Substraction between combinations.

val (*) : C.t -> t -> t

Multiplication by a constant.

val iter : ( var -> C.t -> unit ) -> t -> unit
val of_list : (C.t * var) list -> t
val to_list : t -> (C.t * var) list

Converters to and from lists of monomes.

val of_map : C.t Var_map.t -> t
val to_map : t -> C.t Var_map.t
Semantics
val eval : subst -> t -> C.t

Evaluate a linear combination given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file +Comb (sidekick.Sidekick_simplex.Linear_expr.Make.Comb)

Module Make.Comb

Combinations.

This module defines linear combnations as mapping from variables to coefficients. This allows for very fast computations.

type t

The type of linear combinations.

val compare : t -> t -> int

Comparisons on linear combinations.

val pp : t Sidekick_util.Fmt.printer

Printer for linear combinations.

val is_empty : t -> bool

Is the given expression empty ?

Creation
val empty : t

The empty linear combination.

val monomial : C.t -> var -> t

monome n v creates the linear combination n * v

val monomial1 : var -> t

monome1 v creates the linear combination 1 * v

val as_singleton : t -> (C.t * var) option

as_singleton l returns Some (c,x) if l = c * x, None otherwise

val add : C.t -> var -> t -> t

add n v t adds the monome n * v to the combination t.

val map : f:( var -> var ) -> t -> t
module Infix : sig ... end

Infix operations on combinations

Include the previous module.

include module type of Infix

Infix operations on combinations

This module defines usual operations on linear combinations, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between combinations.

val (-) : t -> t -> t

Substraction between combinations.

val (*) : C.t -> t -> t

Multiplication by a constant.

val iter : ( var -> C.t -> unit ) -> t -> unit
val of_list : (C.t * var) list -> t
val to_list : t -> (C.t * var) list

Converters to and from lists of monomes.

val of_map : C.t Var_map.t -> t
val to_map : t -> C.t Var_map.t
Semantics
val eval : subst -> t -> C.t

Evaluate a linear combination given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Expr/index.html b/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Expr/index.html index 6b84b17f..977e0a9e 100644 --- a/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Expr/index.html +++ b/dev/sidekick/Sidekick_simplex/Linear_expr/Make/Expr/index.html @@ -1,2 +1,2 @@ -Expr (sidekick.Sidekick_simplex.Linear_expr.Make.Expr)

Module Make.Expr

Linear expressions represent linear arithmetic expressions as a linear combination and a constant.

type t

The type of linear expressions.

val comb : t -> Comb.t
val const : t -> C.t
val is_zero : t -> bool
val is_const : t -> bool
val compare : t -> t -> int

Standard comparison function on expressions.

val pp : t Sidekick_util.Fmt.printer

Standard printing function on expressions.

val zero : t

The expression 2.

val of_const : C.t -> t

The constant expression.

val of_comb : Comb.t -> t

Combination without constant

val of_list : C.t -> (C.t * Var.t) list -> t
val make : Comb.t -> C.t -> t

make c n makes the linear expression c + n.

val monomial : C.t -> var -> t
val monomial1 : var -> t
module Infix : sig ... end

Infix operations on expressions

Include the previous module.

include module type of Infix

Infix operations on expressions

This module defines usual operations on linear expressions, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between expressions.

val (-) : t -> t -> t

Substraction between expressions.

val (*) : C.t -> t -> t

Multiplication by a constant.

Semantics
val eval : subst -> t -> C.t

Evaluate a linear expression given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file +Expr (sidekick.Sidekick_simplex.Linear_expr.Make.Expr)

Module Make.Expr

Linear expressions represent linear arithmetic expressions as a linear combination and a constant.

type t

The type of linear expressions.

val comb : t -> Comb.t
val const : t -> C.t
val is_zero : t -> bool
val is_const : t -> bool
val compare : t -> t -> int

Standard comparison function on expressions.

val pp : t Sidekick_util.Fmt.printer

Standard printing function on expressions.

val zero : t

The expression 2.

val of_const : C.t -> t

The constant expression.

val of_comb : Comb.t -> t

Combination without constant

val of_list : C.t -> (C.t * Var.t) list -> t
val make : Comb.t -> C.t -> t

make c n makes the linear expression c + n.

val map : f:( var -> var ) -> t -> t
val monomial : C.t -> var -> t
val monomial1 : var -> t
module Infix : sig ... end

Infix operations on expressions

Include the previous module.

include module type of Infix

Infix operations on expressions

This module defines usual operations on linear expressions, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between expressions.

val (-) : t -> t -> t

Substraction between expressions.

val (*) : C.t -> t -> t

Multiplication by a constant.

Semantics
val eval : subst -> t -> C.t

Evaluate a linear expression given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Comb/index.html b/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Comb/index.html index 2825e690..d63f99d6 100644 --- a/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Comb/index.html +++ b/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Comb/index.html @@ -1,2 +1,2 @@ -Comb (sidekick.Sidekick_simplex.Linear_expr_intf.S.Comb)

Module S.Comb

Combinations.

This module defines linear combnations as mapping from variables to coefficients. This allows for very fast computations.

type t

The type of linear combinations.

val compare : t -> t -> int

Comparisons on linear combinations.

val pp : t Sidekick_util.Fmt.printer

Printer for linear combinations.

val is_empty : t -> bool

Is the given expression empty ?

Creation
val empty : t

The empty linear combination.

val monomial : C.t -> var -> t

monome n v creates the linear combination n * v

val monomial1 : var -> t

monome1 v creates the linear combination 1 * v

val as_singleton : t -> (C.t * var) option

as_singleton l returns Some (c,x) if l = c * x, None otherwise

val add : C.t -> var -> t -> t

add n v t adds the monome n * v to the combination t.

module Infix : sig ... end

Infix operations on combinations

Include the previous module.

include module type of Infix

Infix operations on combinations

This module defines usual operations on linear combinations, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between combinations.

val (-) : t -> t -> t

Substraction between combinations.

val (*) : C.t -> t -> t

Multiplication by a constant.

val iter : ( var -> C.t -> unit ) -> t -> unit
val of_list : (C.t * var) list -> t
val to_list : t -> (C.t * var) list

Converters to and from lists of monomes.

val of_map : C.t Var_map.t -> t
val to_map : t -> C.t Var_map.t
Semantics
val eval : subst -> t -> C.t

Evaluate a linear combination given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file +Comb (sidekick.Sidekick_simplex.Linear_expr_intf.S.Comb)

Module S.Comb

Combinations.

This module defines linear combnations as mapping from variables to coefficients. This allows for very fast computations.

type t

The type of linear combinations.

val compare : t -> t -> int

Comparisons on linear combinations.

val pp : t Sidekick_util.Fmt.printer

Printer for linear combinations.

val is_empty : t -> bool

Is the given expression empty ?

Creation
val empty : t

The empty linear combination.

val monomial : C.t -> var -> t

monome n v creates the linear combination n * v

val monomial1 : var -> t

monome1 v creates the linear combination 1 * v

val as_singleton : t -> (C.t * var) option

as_singleton l returns Some (c,x) if l = c * x, None otherwise

val add : C.t -> var -> t -> t

add n v t adds the monome n * v to the combination t.

val map : f:( var -> var ) -> t -> t
module Infix : sig ... end

Infix operations on combinations

Include the previous module.

include module type of Infix

Infix operations on combinations

This module defines usual operations on linear combinations, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between combinations.

val (-) : t -> t -> t

Substraction between combinations.

val (*) : C.t -> t -> t

Multiplication by a constant.

val iter : ( var -> C.t -> unit ) -> t -> unit
val of_list : (C.t * var) list -> t
val to_list : t -> (C.t * var) list

Converters to and from lists of monomes.

val of_map : C.t Var_map.t -> t
val to_map : t -> C.t Var_map.t
Semantics
val eval : subst -> t -> C.t

Evaluate a linear combination given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Expr/index.html b/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Expr/index.html index 3c45a4be..7561dbfe 100644 --- a/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Expr/index.html +++ b/dev/sidekick/Sidekick_simplex/Linear_expr_intf/module-type-S/Expr/index.html @@ -1,2 +1,2 @@ -Expr (sidekick.Sidekick_simplex.Linear_expr_intf.S.Expr)

Module S.Expr

Linear expressions represent linear arithmetic expressions as a linear combination and a constant.

type t

The type of linear expressions.

val comb : t -> Comb.t
val const : t -> C.t
val is_zero : t -> bool
val is_const : t -> bool
val compare : t -> t -> int

Standard comparison function on expressions.

val pp : t Sidekick_util.Fmt.printer

Standard printing function on expressions.

val zero : t

The expression 2.

val of_const : C.t -> t

The constant expression.

val of_comb : Comb.t -> t

Combination without constant

val of_list : C.t -> (C.t * Var.t) list -> t
val make : Comb.t -> C.t -> t

make c n makes the linear expression c + n.

val monomial : C.t -> var -> t
val monomial1 : var -> t
module Infix : sig ... end

Infix operations on expressions

Include the previous module.

include module type of Infix

Infix operations on expressions

This module defines usual operations on linear expressions, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between expressions.

val (-) : t -> t -> t

Substraction between expressions.

val (*) : C.t -> t -> t

Multiplication by a constant.

Semantics
val eval : subst -> t -> C.t

Evaluate a linear expression given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file +Expr (sidekick.Sidekick_simplex.Linear_expr_intf.S.Expr)

Module S.Expr

Linear expressions represent linear arithmetic expressions as a linear combination and a constant.

type t

The type of linear expressions.

val comb : t -> Comb.t
val const : t -> C.t
val is_zero : t -> bool
val is_const : t -> bool
val compare : t -> t -> int

Standard comparison function on expressions.

val pp : t Sidekick_util.Fmt.printer

Standard printing function on expressions.

val zero : t

The expression 2.

val of_const : C.t -> t

The constant expression.

val of_comb : Comb.t -> t

Combination without constant

val of_list : C.t -> (C.t * Var.t) list -> t
val make : Comb.t -> C.t -> t

make c n makes the linear expression c + n.

val map : f:( var -> var ) -> t -> t
val monomial : C.t -> var -> t
val monomial1 : var -> t
module Infix : sig ... end

Infix operations on expressions

Include the previous module.

include module type of Infix

Infix operations on expressions

This module defines usual operations on linear expressions, as infix operators to ease reading of complex computations.

val (+) : t -> t -> t

Addition between expressions.

val (-) : t -> t -> t

Substraction between expressions.

val (*) : C.t -> t -> t

Multiplication by a constant.

Semantics
val eval : subst -> t -> C.t

Evaluate a linear expression given a substitution for its variables. TODO: document potential exceptions raised ?

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Q/index.html b/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Q/index.html index 5ec35cfd..08871508 100644 --- a/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Q/index.html +++ b/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Q/index.html @@ -1,2 +1,2 @@ -Q (sidekick.Sidekick_simplex.Make.1-Arg.Q)

Module 1-Arg.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file +Q (sidekick.Sidekick_simplex.Make.1-Arg.Q)

Module 1-Arg.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Z/index.html b/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Z/index.html index 6e302d1b..a7d66ec9 100644 --- a/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Z/index.html +++ b/dev/sidekick/Sidekick_simplex/Make/argument-1-Arg/Z/index.html @@ -1,2 +1,2 @@ -Z (sidekick.Sidekick_simplex.Make.1-Arg.Z)

Module 1-Arg.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file +Z (sidekick.Sidekick_simplex.Make.1-Arg.Z)

Module 1-Arg.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/module-type-ARG/Q/index.html b/dev/sidekick/Sidekick_simplex/module-type-ARG/Q/index.html index ad6c3767..2b5740bc 100644 --- a/dev/sidekick/Sidekick_simplex/module-type-ARG/Q/index.html +++ b/dev/sidekick/Sidekick_simplex/module-type-ARG/Q/index.html @@ -1,2 +1,2 @@ -Q (sidekick.Sidekick_simplex.ARG.Q)

Module ARG.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file +Q (sidekick.Sidekick_simplex.ARG.Q)

Module ARG.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/module-type-ARG/Z/index.html b/dev/sidekick/Sidekick_simplex/module-type-ARG/Z/index.html index 7159a046..bc6f0670 100644 --- a/dev/sidekick/Sidekick_simplex/module-type-ARG/Z/index.html +++ b/dev/sidekick/Sidekick_simplex/module-type-ARG/Z/index.html @@ -1,2 +1,2 @@ -Z (sidekick.Sidekick_simplex.ARG.Z)

Module ARG.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file +Z (sidekick.Sidekick_simplex.ARG.Z)

Module ARG.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/module-type-S/Q/index.html b/dev/sidekick/Sidekick_simplex/module-type-S/Q/index.html index 31f54798..af9c64c0 100644 --- a/dev/sidekick/Sidekick_simplex/module-type-S/Q/index.html +++ b/dev/sidekick/Sidekick_simplex/module-type-S/Q/index.html @@ -1,2 +1,2 @@ -Q (sidekick.Sidekick_simplex.S.Q)

Module S.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file +Q (sidekick.Sidekick_simplex.S.Q)

Module S.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_simplex/module-type-S/Z/index.html b/dev/sidekick/Sidekick_simplex/module-type-S/Z/index.html index 6e63e709..e51be9d3 100644 --- a/dev/sidekick/Sidekick_simplex/module-type-S/Z/index.html +++ b/dev/sidekick/Sidekick_simplex/module-type-S/Z/index.html @@ -1,2 +1,2 @@ -Z (sidekick.Sidekick_simplex.S.Z)

Module S.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file +Z (sidekick.Sidekick_simplex.S.Z)

Module S.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Find_foreign/index.html b/dev/sidekick/Sidekick_smt_solver/Find_foreign/index.html new file mode 100644 index 00000000..d444e268 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Find_foreign/index.html @@ -0,0 +1,2 @@ + +Find_foreign (sidekick.Sidekick_smt_solver.Find_foreign)

Module Sidekick_smt_solver.Find_foreign

Find foreign variables.

This module is a modular discoverer of foreign variables (and boolean terms). It should run after preprocessing of terms.

module type ACTIONS = sig ... end
type actions = (module ACTIONS)
type t
type hook = actions -> is_sub:bool -> Sidekick_core.Term.t -> unit
val create : unit -> t
val add_hook : t -> hook -> unit

Register a hook to detect foreign subterms

val traverse_term : t -> actions -> Sidekick_core.Term.t -> unit

Traverse subterms of this term to detect foreign variables and boolean subterms.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Find_foreign/module-type-ACTIONS/index.html b/dev/sidekick/Sidekick_smt_solver/Find_foreign/module-type-ACTIONS/index.html new file mode 100644 index 00000000..a34c98b9 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Find_foreign/module-type-ACTIONS/index.html @@ -0,0 +1,2 @@ + +ACTIONS (sidekick.Sidekick_smt_solver.Find_foreign.ACTIONS)

Module type Find_foreign.ACTIONS

val declare_need_th_combination : Sidekick_core.Term.t -> unit

Declare that this term is a foreign variable in some other subterm.

val add_lit_for_bool_term : ?default_pol:bool -> Sidekick_core.Term.t -> unit

Add the (boolean) term to the SAT solver

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Model/Internal_/index.html b/dev/sidekick/Sidekick_smt_solver/Model/Internal_/index.html deleted file mode 100644 index 298445e0..00000000 --- a/dev/sidekick/Sidekick_smt_solver/Model/Internal_/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Internal_ (sidekick.Sidekick_smt_solver.Model.Internal_)

Module Model.Internal_

val of_tbl : Sigs.term Sidekick_smt_solver__.Sigs.Term.Tbl.t -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Model/index.html b/dev/sidekick/Sidekick_smt_solver/Model/index.html deleted file mode 100644 index de2a1abf..00000000 --- a/dev/sidekick/Sidekick_smt_solver/Model/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Model (sidekick.Sidekick_smt_solver.Model)

Module Sidekick_smt_solver.Model

Models

A model can be produced when the solver is found to be in a satisfiable state after a call to solve.

type t
val empty : t
val mem : t -> Sigs.term -> bool
val find : t -> Sigs.term -> Sigs.term option
val eval : t -> Sigs.term -> Sigs.term option
val pp : t Sidekick_smt_solver__.Sigs.Fmt.printer
module Internal_ : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html b/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html index 7369e8f5..1ae90707 100644 --- a/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html @@ -1,2 +1,2 @@ -Model_builder (sidekick.Sidekick_smt_solver.Model_builder)

Module Sidekick_smt_solver.Model_builder

Model Builder.

This contains a partial model, in construction. It is accessible to every theory, so they can contribute partial values.

TODO: seen values?

type t
include Sidekick_sigs.PRINT with type t := t
val create : Sigs.Term.store -> t
val mem : t -> Sigs.Term.t -> bool
val require_eval : t -> Sigs.Term.t -> unit

Require that this term gets a value.

val add : t -> ?subs:Sigs.Term.t list -> Sigs.Term.t -> Sigs.value -> unit

Add a value to the model.

  • parameter subs

    if provided, these terms will be passed to require_eval to ensure they map to a value.

val gensym : t -> pre:string -> ty:Sigs.Term.t -> Sigs.Term.t

New fresh constant

type eval_cache = Sidekick_smt_solver__.Sigs.Term.Internal_.cache
val eval : ?cache:eval_cache -> t -> Sigs.Term.t -> Sigs.value
val pop_required : t -> Sigs.Term.t option

gives the next subterm that is required but has no value yet

val to_model : t -> Model.t
\ No newline at end of file +Model_builder (sidekick.Sidekick_smt_solver.Model_builder)

Module Sidekick_smt_solver.Model_builder

Model Builder.

This contains a partial model, in construction. It is accessible to every theory, so they can contribute partial values.

TODO: seen values?

type t
include Sidekick_sigs.PRINT with type t := t
val create : Sigs.Term.store -> t
val mem : t -> Sigs.Term.t -> bool
val require_eval : t -> Sigs.Term.t -> unit

Require that this term gets a value.

val add : t -> ?subs:Sigs.Term.t list -> Sigs.Term.t -> Sigs.value -> unit

Add a value to the model.

  • parameter subs

    if provided, these terms will be passed to require_eval to ensure they map to a value.

val gensym : t -> pre:string -> ty:Sigs.Term.t -> Sigs.Term.t

New fresh constant

type eval_cache = Sidekick_smt_solver__.Sigs.Term.Internal_.cache
val eval : ?cache:eval_cache -> t -> Sigs.Term.t -> Sigs.value
val pop_required : t -> Sigs.Term.t option

gives the next subterm that is required but has no value yet

val to_model : t -> Sigs.Model.t
\ 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 new file mode 100644 index 00000000..fe1dde3e --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Preprocess/index.html @@ -0,0 +1,28 @@ + +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 -> + cc:Sigs.CC.t -> + simplify:Sigs.Simplify.t -> + Sigs.Term.store -> + t
module type PREPROCESS_ACTS = sig ... end

Actions given to preprocessor hooks

type preprocess_actions = (module PREPROCESS_ACTS)

Actions available to the preprocessor

type preprocess_hook = + t -> + is_sub:bool -> + recurse:( Sigs.term -> Sigs.term ) -> + preprocess_actions -> + Sigs.term -> + Sigs.term option

Given a term, preprocess it.

The idea is to add literals and clauses to help define the meaning of the term, if needed. For example for boolean formulas, clauses for their Tseitin encoding can be added, with the formula acting as its own proxy symbol; or a new symbol might be added.

  • parameter preprocess_actions

    actions available during preprocessing.

val on_preprocess : t -> preprocess_hook -> unit

Add a hook that will be called when terms are preprocessed

val simplify_and_preproc_lit : + t -> + preprocess_actions -> + Sigs.lit -> + Sigs.lit * Sigs.step_id option
val preprocess_clause : + t -> + preprocess_actions -> + Sigs.lit list -> + Sigs.step_id -> + Sigs.lit list * Sigs.step_id
val preprocess_clause_array : + t -> + preprocess_actions -> + Sigs.lit array -> + Sigs.step_id -> + Sigs.lit array * Sigs.step_id
val cc : t -> Sigs.CC.t
\ No newline at end of file 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 new file mode 100644 index 00000000..4452f939 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Preprocess/module-type-PREPROCESS_ACTS/index.html @@ -0,0 +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 diff --git a/dev/sidekick/Sidekick_smt_solver/Sigs/index.html b/dev/sidekick/Sidekick_smt_solver/Sigs/index.html index b348de75..5b50d9a9 100644 --- a/dev/sidekick/Sidekick_smt_solver/Sigs/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Sigs/index.html @@ -1,2 +1,2 @@ -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
exception Resource_exhausted
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 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 diff --git a/dev/sidekick/Sidekick_smt_solver/Sigs/module-type-ARG/index.html b/dev/sidekick/Sidekick_smt_solver/Sigs/module-type-ARG/index.html index 0b5bcaae..7f27a4e0 100644 --- a/dev/sidekick/Sidekick_smt_solver/Sigs/module-type-ARG/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Sigs/module-type-ARG/index.html @@ -1,2 +1,2 @@ -ARG (sidekick.Sidekick_smt_solver.Sigs.ARG)

Module type Sigs.ARG

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

val view_as_cc : Sidekick_cc.view_as_cc
val is_valid_literal : Term.t -> bool

Is this a valid boolean literal? (e.g. is it a closed term, not inside a quantifier)

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

Module type Sigs.ARG

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

val view_as_cc : Sidekick_cc.view_as_cc
\ 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 cee58b14..e6995bcc 100644 --- a/dev/sidekick/Sidekick_smt_solver/Solver/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Solver/index.html @@ -9,6 +9,7 @@ (module Sigs.ARG) -> ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> + ?tracer:Tracer.t -> proof:Sigs.proof_trace -> theories:Theory.t list -> Sigs.Term.store -> @@ -16,11 +17,12 @@ 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 -> 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 the result to the solver as an 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

type res =
| Sat of 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.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 =
| 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 : ?on_exit:( unit -> unit ) list -> ?check:bool -> ?on_progress:( t -> unit ) -> diff --git a/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html b/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html index da945e1c..bc755548 100644 --- a/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html @@ -1,5 +1,11 @@ -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 = sig ... end
type preprocess_actions = (module PREPROCESS_ACTS)

Actions available to the preprocessor

type preprocess_hook = t -> preprocess_actions -> Sigs.term -> unit

Given a term, preprocess it.

The idea is to add literals and clauses to help define the meaning of the term, if needed. For example for boolean formulas, clauses for their Tseitin encoding can be added, with the formula acting as its own proxy symbol.

  • parameter preprocess_actions

    actions available during preprocessing.

val on_preprocess : t -> preprocess_hook -> unit

Add a hook that will be called when terms are preprocessed

val preprocess_clause : +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 = + Preprocess.t -> + is_sub:bool -> + recurse:( Sigs.term -> Sigs.term ) -> + preprocess_actions -> + Sigs.term -> + Sigs.term option

Given a term, preprocess it.

The idea is to add literals and clauses to help define the meaning of the term, if needed. For example for boolean formulas, clauses for their Tseitin encoding can be added, with the formula acting as its own proxy symbol.

  • parameter preprocess_actions

    actions available during preprocessing.

val preprocess : t -> Preprocess.t
val on_preprocess : t -> preprocess_hook -> unit

Add a hook that will be called when terms are preprocessed

val preprocess_clause : t -> Sigs.lit list -> Sigs.step_id -> @@ -7,7 +13,7 @@ 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

val claim_term : t -> th_id:Theory_id.t -> Sigs.term -> unit

Claim a term, for a theory that might decide or merge it with another term. This is useful for theory combination.

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.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 : t -> theory_actions -> Sigs.lit -> @@ -28,7 +34,7 @@ theory_actions -> Sigs.lit list -> Sigs.step_id -> - unit

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

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 : + 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 : t -> ( (Sigs.CC.t * Sigs.E_node.t * Sigs.E_node.t * Sigs.CC_expl.t) -> Sigs.CC.Handler_action.or_conflict ) -> @@ -46,7 +52,7 @@ t -> ( (Sigs.CC.t * Sigs.lit * ( unit -> Sigs.lit list * Sigs.step_id )) -> Sigs.CC.Handler_action.t list ) -> - unit

Callback called on every CC propagation

val on_partial_check : + 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 -> ( t -> theory_actions -> Sigs.lit Iter.t -> unit ) -> unit

Register callbacked to be called with the slice of literals newly added on the trail.

This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.

val on_final_check : @@ -63,7 +69,7 @@ ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> - unit

Add model production/completion hooks.

val on_progress : t -> ( unit, unit ) Sidekick_util.Event.t
val is_complete : t -> bool

Are we still in a complete logic fragment?

val last_model : t -> Model.t option

Delayed actions

module type PERFORM_ACTS = sig ... end
module Perform_delayed (A : PERFORM_ACTS) : sig ... end
val add_theory_state : + unit

Add model production/completion hooks.

val on_progress : t -> ( unit, unit ) Sidekick_util.Event.t
val is_complete : t -> bool

Are we still in a complete logic fragment?

val last_model : t -> Sigs.Model.t option

Delayed actions

module type PERFORM_ACTS = sig ... end
module Perform_delayed (A : PERFORM_ACTS) : sig ... end
val add_theory_state : st:'a -> push_level:( 'a -> unit ) -> pop_levels:( 'a -> int -> unit ) -> @@ -71,6 +77,7 @@ unit
val create : (module Sigs.ARG) -> stat:Sidekick_util.Stat.t -> + tracer:Tracer.t -> proof:Sigs.Proof_trace.t -> Sigs.Term.store -> unit -> diff --git a/dev/sidekick/Sidekick_smt_solver/Solver_internal/module-type-PREPROCESS_ACTS/index.html b/dev/sidekick/Sidekick_smt_solver/Solver_internal/module-type-PREPROCESS_ACTS/index.html deleted file mode 100644 index 84c6cc2a..00000000 --- a/dev/sidekick/Sidekick_smt_solver/Solver_internal/module-type-PREPROCESS_ACTS/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -PREPROCESS_ACTS (sidekick.Sidekick_smt_solver.Solver_internal.PREPROCESS_ACTS)

Module type Solver_internal.PREPROCESS_ACTS

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 diff --git a/dev/sidekick/Sidekick_smt_solver/Trace_reader/index.html b/dev/sidekick/Sidekick_smt_solver/Trace_reader/index.html new file mode 100644 index 00000000..d6634eb4 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Trace_reader/index.html @@ -0,0 +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 : + ?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 diff --git a/dev/sidekick/Sidekick_smt_solver/Tracer/class-concrete/index.html b/dev/sidekick/Sidekick_smt_solver/Tracer/class-concrete/index.html new file mode 100644 index 00000000..270712b6 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/class-concrete/index.html @@ -0,0 +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 diff --git a/dev/sidekick/Sidekick_smt_solver/Tracer/class-dummy/index.html b/dev/sidekick/Sidekick_smt_solver/Tracer/class-dummy/index.html new file mode 100644 index 00000000..d98f1b5a --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/class-dummy/index.html @@ -0,0 +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 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 new file mode 100644 index 00000000..d0c144a0 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/class-type-t/index.html @@ -0,0 +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 diff --git a/dev/sidekick/Sidekick_smt_solver/Tracer/index.html b/dev/sidekick/Sidekick_smt_solver/Tracer/index.html new file mode 100644 index 00000000..b028e115 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Tracer/index.html @@ -0,0 +1,2 @@ + +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 diff --git a/dev/sidekick/Sidekick_smt_solver/index.html b/dev/sidekick/Sidekick_smt_solver/index.html index ae32114b..a641d4b3 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 : sig ... end

Models

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
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
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_lra/Intf/module-type-ARG/Q/index.html b/dev/sidekick/Sidekick_th_lra/Intf/module-type-ARG/Q/index.html index 1409f7be..b6cd1523 100644 --- a/dev/sidekick/Sidekick_th_lra/Intf/module-type-ARG/Q/index.html +++ b/dev/sidekick/Sidekick_th_lra/Intf/module-type-ARG/Q/index.html @@ -1,2 +1,2 @@ -Q (sidekick.Sidekick_th_lra.Intf.ARG.Q)

Module ARG.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file +Q (sidekick.Sidekick_th_lra.Intf.ARG.Q)

Module ARG.Q

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_lra/Intf/module-type-ARG/Z/index.html b/dev/sidekick/Sidekick_th_lra/Intf/module-type-ARG/Z/index.html index e8580fa1..a08e5612 100644 --- a/dev/sidekick/Sidekick_th_lra/Intf/module-type-ARG/Z/index.html +++ b/dev/sidekick/Sidekick_th_lra/Intf/module-type-ARG/Z/index.html @@ -1,2 +1,2 @@ -Z (sidekick.Sidekick_th_lra.Intf.ARG.Z)

Module ARG.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file +Z (sidekick.Sidekick_th_lra.Intf.ARG.Z)

Module ARG.Z

include Sidekick_arith.NUM
type t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_ty_unin/.dummy b/dev/sidekick/Sidekick_th_ty_unin/.dummy new file mode 100644 index 00000000..e69de29b diff --git a/dev/sidekick/Sidekick_th_ty_unin/index.html b/dev/sidekick/Sidekick_th_ty_unin/index.html new file mode 100644 index 00000000..b728c4b2 --- /dev/null +++ b/dev/sidekick/Sidekick_th_ty_unin/index.html @@ -0,0 +1,2 @@ + +Sidekick_th_ty_unin (sidekick.Sidekick_th_ty_unin)

Module Sidekick_th_ty_unin

module type ARG = sig ... end
val theory : (module ARG) -> Sidekick_smt_solver.Theory.t

Theory of uninterpreted types

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_ty_unin/module-type-ARG/index.html b/dev/sidekick/Sidekick_th_ty_unin/module-type-ARG/index.html new file mode 100644 index 00000000..12f3161e --- /dev/null +++ b/dev/sidekick/Sidekick_th_ty_unin/module-type-ARG/index.html @@ -0,0 +1,2 @@ + +ARG (sidekick.Sidekick_th_ty_unin.ARG)

Module type Sidekick_th_ty_unin.ARG

val ty_is_unin : ty -> bool
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/.dummy b/dev/sidekick/Sidekick_trace/.dummy new file mode 100644 index 00000000..e69de29b diff --git a/dev/sidekick/Sidekick_trace/Entry_id/index.html b/dev/sidekick/Sidekick_trace/Entry_id/index.html new file mode 100644 index 00000000..4165c54b --- /dev/null +++ b/dev/sidekick/Sidekick_trace/Entry_id/index.html @@ -0,0 +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 diff --git a/dev/sidekick/Sidekick_trace/Entry_view/index.html b/dev/sidekick/Sidekick_trace/Entry_view/index.html new file mode 100644 index 00000000..5f3d54c1 --- /dev/null +++ b/dev/sidekick/Sidekick_trace/Entry_view/index.html @@ -0,0 +1,2 @@ + +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/Sink/index.html b/dev/sidekick/Sidekick_trace/Sink/index.html new file mode 100644 index 00000000..81b3c92d --- /dev/null +++ b/dev/sidekick/Sidekick_trace/Sink/index.html @@ -0,0 +1,2 @@ + +Sink (sidekick.Sidekick_trace.Sink)

Module Sidekick_trace.Sink

An IO sink for serialization/tracing

A trace is emitted on the fly into a sink. The sink collects or writes entries that are emitted into it.

type tag = string
module type S = sig ... end
type t = (module S)

Trace sink

val emit : t -> tag:tag -> Sidekick_util.Ser_value.t -> Entry_id.t
val emit' : t -> tag:tag -> Sidekick_util.Ser_value.t -> unit
val null : t

Sink that writes nowhere, just eats bytes.

val of_out_channel_using_bencode : Stdlib.out_channel -> t

A sink that emits entries using Bencode into the given channel

val of_buffer_using_bencode : Stdlib.Buffer.t -> t

Emit entries into the given buffer, in Bencode.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/Sink/module-type-S/index.html b/dev/sidekick/Sidekick_trace/Sink/module-type-S/index.html new file mode 100644 index 00000000..f1a2bccc --- /dev/null +++ b/dev/sidekick/Sidekick_trace/Sink/module-type-S/index.html @@ -0,0 +1,2 @@ + +S (sidekick.Sidekick_trace.Sink.S)

Module type Sink.S

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/Source/index.html b/dev/sidekick/Sidekick_trace/Source/index.html new file mode 100644 index 00000000..33e3d430 --- /dev/null +++ b/dev/sidekick/Sidekick_trace/Source/index.html @@ -0,0 +1,5 @@ + +Source (sidekick.Sidekick_trace.Source)

Module Sidekick_trace.Source

Source to read a trace.

A source is an IO input source that allows the read of individual entries of the trace, by providing their entry ID. It also allows to iterate on entries in chronological order.

type tag = string
module type S = sig ... end
type t = (module S)
val get_entry : t -> Entry_id.t -> (tag * Sidekick_util.Ser_value.t) option
val get_entry_exn : t -> Entry_id.t -> tag * Sidekick_util.Ser_value.t
val iter_all : + t -> + ( Entry_id.t -> tag:tag -> Sidekick_util.Ser_value.t -> unit ) -> + unit
val of_string_using_bencode : string -> t

Decode string, where entries are offsets

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/Source/module-type-S/index.html b/dev/sidekick/Sidekick_trace/Source/module-type-S/index.html new file mode 100644 index 00000000..e6180cb5 --- /dev/null +++ b/dev/sidekick/Sidekick_trace/Source/module-type-S/index.html @@ -0,0 +1,4 @@ + +S (sidekick.Sidekick_trace.Source.S)

Module type Source.S

val get_entry : Entry_id.t -> tag * Sidekick_util.Ser_value.t
  • raises Not_found

    if there is no such entry

val iter_all : + ( Entry_id.t -> tag:tag -> Sidekick_util.Ser_value.t -> unit ) -> + unit

Iterate on all entries

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_trace/index.html b/dev/sidekick/Sidekick_trace/index.html new file mode 100644 index 00000000..b5d4bfd4 --- /dev/null +++ b/dev/sidekick/Sidekick_trace/index.html @@ -0,0 +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 diff --git a/dev/sidekick/Sidekick_util/Error/index.html b/dev/sidekick/Sidekick_util/Error/index.html index 9c7f6c86..f830be61 100644 --- a/dev/sidekick/Sidekick_util/Error/index.html +++ b/dev/sidekick/Sidekick_util/Error/index.html @@ -1,2 +1,2 @@ -Error (sidekick.Sidekick_util.Error)

Module Sidekick_util.Error

exception Error of string
val errorf : ( 'a, Stdlib.Format.formatter, unit, 'b ) Stdlib.format4 -> 'a
  • raises Error

    when called

\ No newline at end of file +Error (sidekick.Sidekick_util.Error)

Module Sidekick_util.Error

exception Error of string
val errorf : ( 'a, Stdlib.Format.formatter, unit, 'b ) Stdlib.format4 -> 'a
  • raises Error

    when called

type nonrec 'a result = ( 'a, string ) Stdlib.result
val try_ : ( unit -> 'a ) -> 'a result
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Event/index.html b/dev/sidekick/Sidekick_util/Event/index.html index caee63c7..5de74f85 100644 --- a/dev/sidekick/Sidekick_util/Event/index.html +++ b/dev/sidekick/Sidekick_util/Event/index.html @@ -1,2 +1,2 @@ -Event (sidekick.Sidekick_util.Event)

Module Sidekick_util.Event

type ('a, 'b) t

An event emitting values of type 'a, where subscribers return values of type 'b.

module Emitter : sig ... end
val on : ( 'a, 'b ) t -> f:( 'a -> 'b ) -> unit
val of_emitter : ( 'a, 'b ) Emitter.t -> ( 'a, 'b ) t
val emit : ( 'a, unit ) Emitter.t -> 'a -> unit
val emit_collect : ( 'a, 'b ) Emitter.t -> 'a -> 'b list
val emit_iter : ( 'a, 'b ) Emitter.t -> 'a -> f:( 'b -> unit ) -> unit
\ No newline at end of file +Event (sidekick.Sidekick_util.Event)

Module Sidekick_util.Event

Event pattern.

This provides a basic observer pattern, where events are emitted from some source (with an attached value), and callbacks that were registered will receive this value.

type ('a, 'b) t

An event emitting values of type 'a, where subscribers return values of type 'b.

module Emitter : sig ... end
val on : ( 'a, 'b ) t -> f:( 'a -> 'b ) -> unit
val of_emitter : ( 'a, 'b ) Emitter.t -> ( 'a, 'b ) t
val emit : ( 'a, unit ) Emitter.t -> 'a -> unit
val emit_collect : ( 'a, 'b ) Emitter.t -> 'a -> 'b list
val emit_iter : ( 'a, 'b ) Emitter.t -> 'a -> f:( 'b -> unit ) -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Ser_decode/Error/index.html b/dev/sidekick/Sidekick_util/Ser_decode/Error/index.html new file mode 100644 index 00000000..80d4f1b9 --- /dev/null +++ b/dev/sidekick/Sidekick_util/Ser_decode/Error/index.html @@ -0,0 +1,2 @@ + +Error (sidekick.Sidekick_util.Ser_decode.Error)

Module Ser_decode.Error

Errors

type t
include Sidekick_sigs.PRINT with type t := t
val to_string : t -> string
val of_string : string -> Ser_value.t -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Ser_decode/Infix/index.html b/dev/sidekick/Sidekick_util/Ser_decode/Infix/index.html new file mode 100644 index 00000000..883c9dce --- /dev/null +++ b/dev/sidekick/Sidekick_util/Ser_decode/Infix/index.html @@ -0,0 +1,2 @@ + +Infix (sidekick.Sidekick_util.Ser_decode.Infix)

Module Ser_decode.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
\ 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 new file mode 100644 index 00000000..7f7eb22a --- /dev/null +++ b/dev/sidekick/Sidekick_util/Ser_decode/index.html @@ -0,0 +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 diff --git a/dev/sidekick/Sidekick_util/Ser_value/index.html b/dev/sidekick/Sidekick_util/Ser_value/index.html new file mode 100644 index 00000000..e24d4c54 --- /dev/null +++ b/dev/sidekick/Sidekick_util/Ser_value/index.html @@ -0,0 +1,2 @@ + +Ser_value (sidekick.Sidekick_util.Ser_value)

Module Sidekick_util.Ser_value

Serialization representation.

A Ser_value.t describes how to serialized some structured data into bytes. It reflects the shape of the structured data but does not commit to a particular serialization format.

type t = private
| Null
| Bool of bool
| Str of string
| Bytes of string
| Int of int
| List of t list
| Dict of t Sidekick_util__.Util.Str_map.t
val null : t
val bool : bool -> t
val int : int -> t
val string : string -> t
val bytes : string -> t
val list : t list -> t
val dict : t Sidekick_util__.Util.Str_map.t -> t
val dict_of_list : (string * t) list -> t
val is_null : t -> bool
include Sidekick_sigs.PRINT with type t := t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/Util/index.html b/dev/sidekick/Sidekick_util/Util/index.html index a1fe043c..819bd5ab 100644 --- a/dev/sidekick/Sidekick_util/Util/index.html +++ b/dev/sidekick/Sidekick_util/Util/index.html @@ -3,4 +3,4 @@ f:( int -> 'a -> 'b -> unit ) -> 'a array -> 'b array -> - unit
val setup_gc : unit -> unit

Change parameters of the GC

module Int_set : CCSet.S with type elt = int
module Int_map : CCMap.S with type key = int
module Int_tbl : CCHashtbl.S with type key = int
module Str_tbl : CCHashtbl.S with type key = string
\ No newline at end of file + unit
val setup_gc : unit -> unit

Change parameters of the GC

module Int_set : CCSet.S with type elt = int
module Int_map : CCMap.S with type key = int
module Int_tbl : CCHashtbl.S with type key = int
module Str_tbl : CCHashtbl.S with type key = string
module Str_map : CCMap.S with type key = string
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_util/index.html b/dev/sidekick/Sidekick_util/index.html index b74ab294..eb879294 100644 --- a/dev/sidekick/Sidekick_util/index.html +++ b/dev/sidekick/Sidekick_util/index.html @@ -1,2 +1,2 @@ -Sidekick_util (sidekick.Sidekick_util)

Module Sidekick_util

module Fmt = CCFormat
module Util : sig ... end
module Vec : sig ... end

Vectors

module Veci : sig ... end

Vectors of int32 integers

module Vec_float : sig ... end

Vectors of floats

module Vec_sig : sig ... end
module Bitvec : sig ... end

Bitvector.

module Int_id : sig ... end

Integer-based identifiers.

module Int_tbl = Util.Int_tbl
module Int_set = Util.Int_set
module Int_map = Util.Int_map
module Event : sig ... end
module Backtrack_stack : sig ... end
module Backtrackable_tbl : sig ... end
module Backtrackable_ref : sig ... end
module Log : sig ... end

Logging function, for debugging

module Error : sig ... end
module Bag : sig ... end
module Stat : sig ... end
module Hash : sig ... end
module Profile : sig ... end

Profiling probes.

module Chunk_stack : sig ... end

Manage a list of chunks.

val let@ : ( 'a -> 'b ) -> 'a -> 'b
\ No newline at end of file +Sidekick_util (sidekick.Sidekick_util)

Module Sidekick_util

module Fmt = CCFormat
module Util : sig ... end
module Vec : sig ... end

Vectors

module Veci : sig ... end

Vectors of int32 integers

module Vec_float : sig ... end

Vectors of floats

module Vec_sig : sig ... end
module Bitvec : sig ... end

Bitvector.

module Int_id : sig ... end

Integer-based identifiers.

module Int_tbl = Util.Int_tbl
module Int_set = Util.Int_set
module Int_map = Util.Int_map
module Event : sig ... end

Event pattern.

module Backtrack_stack : sig ... end
module Backtrackable_tbl : sig ... end
module Backtrackable_ref : sig ... end
module Log : sig ... end

Logging function, for debugging

module Error : sig ... end
module Bag : sig ... end
module Stat : sig ... end
module Hash : sig ... end
module Profile : sig ... end

Profiling probes.

module Chunk_stack : sig ... end

Manage a list of chunks.

module Ser_value : sig ... end

Serialization representation.

module Ser_decode : sig ... end

Decoders for Ser_value.

module Ser_sink = Ser_sink
val let@ : ( 'a -> 'b ) -> 'a -> 'b
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_zarith/Int/index.html b/dev/sidekick/Sidekick_zarith/Int/index.html index 7394006b..ecf1a185 100644 --- a/dev/sidekick/Sidekick_zarith/Int/index.html +++ b/dev/sidekick/Sidekick_zarith/Int/index.html @@ -1,2 +1,2 @@ -Int (sidekick.Sidekick_zarith.Int)

Module Sidekick_zarith.Int

include Sidekick_arith.INT with type t = Z.t
include Sidekick_arith.NUM with type t = Z.t
type t = Z.t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
val sqrt : t -> t
val divexact : t -> t -> t
val (/) : t -> t -> t
val ediv : t -> t -> t

Euclidian division

val rem : t -> t -> t
val probab_prime : t -> bool
val pow : t -> int -> t
\ No newline at end of file +Int (sidekick.Sidekick_zarith.Int)

Module Sidekick_zarith.Int

include Sidekick_arith.INT with type t = Z.t
include Sidekick_arith.NUM with type t = Z.t
type t = Z.t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val succ : t -> t
val pred : t -> t
val gcd : t -> t -> t
val sqrt : t -> t
val divexact : t -> t -> t
val (/) : t -> t -> t
val ediv : t -> t -> t

Euclidian division

val rem : t -> t -> t
val probab_prime : t -> bool
val pow : t -> int -> t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_zarith/Rational/index.html b/dev/sidekick/Sidekick_zarith/Rational/index.html index d0004f7c..250ad55d 100644 --- a/dev/sidekick/Sidekick_zarith/Rational/index.html +++ b/dev/sidekick/Sidekick_zarith/Rational/index.html @@ -1,2 +1,2 @@ -Rational (sidekick.Sidekick_zarith.Rational)

Module Sidekick_zarith.Rational

include Sidekick_arith.NUM with type t = Q.t
type t = Q.t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> 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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file +Rational (sidekick.Sidekick_zarith.Rational)

Module Sidekick_zarith.Rational

include Sidekick_arith.NUM with type t = Q.t
type t = Q.t
val zero : t
val one : t
val minus_one : t
val abs : t -> t
val sign : t -> int
val of_int : int -> t
val to_string : t -> string
val of_string : string -> t option
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 (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
val (~-) : t -> t
val neg : t -> t
val min : t -> t -> t
val max : t -> t -> t
val (=) : t -> t -> bool
val (<>) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
type bigint = Z.t
val (/) : t -> t -> t
val num : t -> bigint
val denum : t -> bigint
val infinity : t

+infinity

val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool

A proper real, not nan/infinity

val is_int : t -> bool

Is this a proper integer?

val as_int : t -> bigint option

Convert to an integer if it's one, return None otherwise

val floor : t -> bigint

Integer equal or below

val ceil : t -> bigint

Integer equal or above

val pp_approx : int -> Stdlib.Format.formatter -> t -> unit

Pretty print rational with given amount of precision (for example as a floating point number)

\ No newline at end of file diff --git a/dev/sidekick/index.html b/dev/sidekick/index.html index 353921b8..9bcd3ef2 100644 --- a/dev/sidekick/index.html +++ b/dev/sidekick/index.html @@ -1,2 +1,2 @@ -index (sidekick.index)

sidekick index

Library sidekick.arith

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

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