diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Cstor/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Cstor/index.html index ee1c6fb0..3a8f38dc 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Cstor/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Cstor/index.html @@ -1,2 +1,2 @@ -Cstor (sidekick-base.Sidekick_base.Base_types.Cstor)

Module Base_types.Cstor

type t = 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;
}
val id : t -> ID.t
val ty_args : t -> ty Iter.t
val equal : cstor -> cstor -> bool
val pp : CCFormat.t -> t -> unit
\ No newline at end of file +Cstor (sidekick-base.Sidekick_base.Base_types.Cstor)

Module Base_types.Cstor

Datatype constructors.

A datatype has one or more constructors, each of which is a special kind of function symbol. Constructors are injective and pairwise distinct.

type t = 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;
}
val id : t -> ID.t
val ty_args : t -> ty Iter.t
val equal : cstor -> cstor -> bool
val pp : CCFormat.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Data/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Data/index.html index 89544223..374b45f6 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Data/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Data/index.html @@ -1,2 +1,2 @@ -Data (sidekick-base.Sidekick_base.Base_types.Data)

Module Base_types.Data

type t = data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
val pp : CCFormat.t -> t -> unit
\ No newline at end of file +Data (sidekick-base.Sidekick_base.Base_types.Data)

Module Base_types.Data

Datatypes

type t = data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
val pp : CCFormat.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html index ac915316..41827146 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html @@ -1,2 +1,2 @@ -Fun (sidekick-base.Sidekick_base.Base_types.Fun)

Module Base_types.Fun

type view = fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}
type t = fun_ = {
fun_id : ID.t;
fun_view : fun_view;
}
val id : t -> ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val select : select -> t
val select_idx : cstor -> int -> t
val cstor : cstor -> t
val is_a : cstor -> t
val do_cc : t -> bool
val mk_undef : ID.t -> Ty.Fun.t -> t
val mk_undef' : ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : ID.t -> Ty.t -> t
val pp : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file +Fun (sidekick-base.Sidekick_base.Base_types.Fun)

Module Base_types.Fun

Function symbols

type view = fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}
type t = fun_ = {
fun_id : ID.t;
fun_view : fun_view;
}
val id : t -> ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val select : select -> t
val select_idx : cstor -> int -> t
val cstor : cstor -> t
val is_a : cstor -> t
val do_cc : t -> bool
val mk_undef : ID.t -> Ty.Fun.t -> t
val mk_undef' : ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : ID.t -> Ty.t -> t
val pp : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Select/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Select/index.html index 3cf4fb03..613f5db4 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Select/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Select/index.html @@ -1,2 +1,2 @@ -Select (sidekick-base.Sidekick_base.Base_types.Select)

Module Base_types.Select

type t = select = {
select_id : ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
val ty : t -> ty
\ No newline at end of file +Select (sidekick-base.Sidekick_base.Base_types.Select)

Module Base_types.Select

Datatype selectors.

A selector is a kind of function that allows to obtain an argument of a given constructor.

type t = select = {
select_id : ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
val ty : t -> ty
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Statement/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Statement/index.html index a54e9183..41b1bd6e 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Statement/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Statement/index.html @@ -1,2 +1,2 @@ -Statement (sidekick-base.Sidekick_base.Base_types.Statement)

Module Base_types.Statement

type t = 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_exit
val pp : Fmt.t -> t -> unit
\ No newline at end of file +Statement (sidekick-base.Sidekick_base.Base_types.Statement)

Module Base_types.Statement

Statements.

A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.

type t = 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_exit
val pp : Fmt.t -> t -> unit

Pretty print a statement

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Term/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Term/index.html index 870694c7..e51e4d62 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Term/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Term/index.html @@ -1,2 +1,2 @@ -Term (sidekick-base.Sidekick_base.Base_types.Term)

Module Base_types.Term

type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?⁠size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> fun_ -> t
val app_fun : state -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : state -> t -> t -> t
val not_ : state -> t -> t
val ite : state -> t -> t -> t -> t
val select : state -> select -> t -> t
val app_cstor : state -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : state -> cstor -> t -> t
val lra : state -> (Q.t, t) lra_view -> t
val abs : state -> t -> t * bool

Obtain unsigned version of t, + the sign as a boolean

module Iter_dag : sig ... end
val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t
val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t
val pp : t Fmt.printer

Views

val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (fun_, t, t Iter.t) CC_view.t
val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
val as_bool : t -> bool option

Containers

module Tbl : CCHashtbl.S with type Tbl.key = t
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
\ No newline at end of file +Term (sidekick-base.Sidekick_base.Base_types.Term)

Module Base_types.Term

Term creation and manipulation

type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?⁠size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> fun_ -> t
val app_fun : state -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : state -> t -> t -> t
val not_ : state -> t -> t
val ite : state -> t -> t -> t -> t
val select : state -> select -> t -> t
val app_cstor : state -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : state -> cstor -> t -> t
val lra : state -> (Q.t, t) lra_view -> t
val abs : state -> t -> t * bool

Obtain unsigned version of t, + the sign as a boolean

module Iter_dag : sig ... end
val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t
val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t
val pp : t Fmt.printer

Views

val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (fun_, t, t Iter.t) CC_view.t
val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
val as_bool : t -> bool option

Containers

module Tbl : CCHashtbl.S with type Tbl.key = t
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Ty/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Ty/index.html index 05f1072a..67795050 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Ty/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Ty/index.html @@ -1,2 +1,2 @@ -Ty (sidekick-base.Sidekick_base.Base_types.Ty)

Module Base_types.Ty

type t = ty
type state = unit
type view = ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
type def = ty_def =
| Ty_uninterpreted of ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
val id : t -> int
val view : t -> view
val bool : state -> t
val real : state -> t
val atomic : def -> t list -> t
val id_of_def : def -> ID.t
val atomic_uninterpreted : ID.t -> t
val finite : t -> bool
val set_finite : t -> bool -> unit
val is_bool : t -> bool
val is_uninterpreted : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t CCFormat.printer
module Tbl : CCHashtbl.S with type Tbl.key = t
module Fun : sig ... end
\ No newline at end of file +Ty (sidekick-base.Sidekick_base.Base_types.Ty)

Module Base_types.Ty

Types

type t = ty
type state = unit
type view = ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
type def = ty_def =
| Ty_uninterpreted of ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
val id : t -> int
val view : t -> view
val bool : state -> t
val real : state -> t
val atomic : def -> t list -> t
val id_of_def : def -> ID.t
val atomic_uninterpreted : ID.t -> t
val finite : t -> bool
val set_finite : t -> bool -> unit
val is_bool : t -> bool
val is_uninterpreted : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t CCFormat.printer
module Tbl : CCHashtbl.S with type Tbl.key = t
module Fun : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Value/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Value/index.html index ef529fb9..3c1957ee 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/Value/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/Value/index.html @@ -1,2 +1,2 @@ -Value (sidekick-base.Sidekick_base.Base_types.Value)

Module Base_types.Value

type t = value =
| V_bool of bool
| V_element of {
id : ID.t;
ty : ty;
}
| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}
| V_real of Q.t
val true_ : t
val false_ : t
val bool : bool -> t
val real : Q.t -> t
val real_of_string : string -> t
val mk_elt : ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val cstor_app : cstor -> t list -> t
val fresh : Term.t -> t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
\ No newline at end of file +Value (sidekick-base.Sidekick_base.Base_types.Value)

Module Base_types.Value

Values (used in models)

type t = value =
| V_bool of bool
| V_element of {
id : ID.t;
ty : ty;
}
| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}
| V_real of Q.t
val true_ : t
val false_ : t
val bool : bool -> t
val real : Q.t -> t
val real_of_string : string -> t
val mk_elt : ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val cstor_app : cstor -> t list -> t
val fresh : Term.t -> t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Base_types/index.html b/dev/sidekick-base/Sidekick_base/Base_types/index.html index 115a3925..7f2245bc 100644 --- a/dev/sidekick-base/Sidekick_base/Base_types/index.html +++ b/dev/sidekick-base/Sidekick_base/Base_types/index.html @@ -1,2 +1,2 @@ -Base_types (sidekick-base.Sidekick_base.Base_types)

Module Sidekick_base.Base_types

module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
type lra_pred = Sidekick_arith_lra.Predicate.t =
| Leq
| Geq
| Lt
| Gt
| Eq
| Neq
type lra_op = Sidekick_arith_lra.op =
| Plus
| Minus
type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
| LRA_pred of lra_pred * 'a * 'a
| LRA_op of lra_op * 'a * 'a
| LRA_mult of 'num * 'a
| LRA_const of 'num
| LRA_simplex_var of 'a
| LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
| LRA_other of 'a
type term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : term term_view;
}
and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
and fun_ = {
fun_id : ID.t;
fun_view : fun_view;
}
and fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}

Methods on the custom term view whose arguments are 'a. Terms must be printable, and provide some additional theory handles.

  • relevant must return a subset of args (possibly the same set). The terms it returns will be activated and evaluated whenever possible. Terms in args \ relevant args are considered for congruence but not for evaluation.
and fun_ty = {
fun_ty_args : ty list;
fun_ty_ret : ty;
}

Function type

and ty = {
mutable ty_id : int;
ty_view : ty_view;
}

Hashconsed type

and ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
and ty_def =
| Ty_uninterpreted of ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
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;
}
and value =
| V_bool of bool
| V_element of {
id : ID.t;
ty : ty;
}

a named constant, distinct from any other constant

| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}

Custom value

| V_real of Q.t

Semantic values, used for models (and possibly model-constructing calculi)

and value_custom_view = ..
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_exit
val term_equal_ : term -> term -> bool
val term_hash_ : term -> int
val term_cmp_ : term -> term -> int
val fun_compare : fun_ -> fun_ -> int
val pp_fun : CCFormat.t -> fun_ -> unit
val id_of_fun : fun_ -> ID.t
val eq_ty : ty -> ty -> bool
val eq_cstor : cstor -> cstor -> bool
val eq_value : value -> value -> bool
val hash_value : value Sidekick_util.Hash.t
val pp_value : value Sidekick_util.Util.printer
val pp_db : Stdlib.Format.formatter -> (int * 'a) -> unit
val pp_ty : ty Sidekick_util.Util.printer
val string_of_lra_pred : lra_pred -> string
val pp_pred : Fmt.t -> lra_pred -> unit
val string_of_lra_op : lra_op -> string
val pp_lra_op : Fmt.t -> lra_op -> unit
val pp_term_view_gen : pp_id:(Fmt.t -> ID.t -> unit) -> pp_t:'a Fmt.printer -> Fmt.t -> 'a term_view -> unit
val pp_term_top : ids:bool -> Fmt.t -> term -> unit
val pp_term : Fmt.t -> term -> unit
val pp_term_view : Fmt.t -> term term_view -> unit
module Ty : sig ... end
module Fun : sig ... end
module Term_cell : sig ... end
module Term : sig ... end
module Value : sig ... end
module Data : sig ... end
module Select : sig ... end
module Cstor : sig ... end
module Statement : sig ... end
\ No newline at end of file +Base_types (sidekick-base.Sidekick_base.Base_types)

Module Sidekick_base.Base_types

Basic type definitions for Sidekick_base

module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
type lra_pred = Sidekick_arith_lra.Predicate.t =
| Leq
| Geq
| Lt
| Gt
| Eq
| Neq
type lra_op = Sidekick_arith_lra.op =
| Plus
| Minus
type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
| LRA_pred of lra_pred * 'a * 'a
| LRA_op of lra_op * 'a * 'a
| LRA_mult of 'num * 'a
| LRA_const of 'num
| LRA_simplex_var of 'a
| LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
| LRA_other of 'a
type term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : term term_view;
}

Term.

A term, with its own view, type, and a unique identifier. Do not create directly, see Term.

and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view

Shallow structure of a term.

A term is a DAG (direct acyclic graph) of nodes, each of which has a term view.

and fun_ = {
fun_id : ID.t;
fun_view : fun_view;
}

type of function symbols

and fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}

Methods on the custom term view whose arguments are 'a. Terms must be printable, and provide some additional theory handles.

  • relevant must return a subset of args (possibly the same set). The terms it returns will be activated and evaluated whenever possible. Terms in args \ relevant args are considered for congruence but not for evaluation.
and fun_ty = {
fun_ty_args : ty list;
fun_ty_ret : ty;
}

Function type

and ty = {
mutable ty_id : int;
ty_view : ty_view;
}

Hashconsed type

and ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
and ty_def =
| Ty_uninterpreted of ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
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;
}
and value =
| V_bool of bool
| V_element of {
id : ID.t;
ty : ty;
}

a named constant, distinct from any other constant

| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}

Custom value

| V_real of Q.t

Semantic values, used for models (and possibly model-constructing calculi)

and value_custom_view = ..
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_exit
val term_equal_ : term -> term -> bool
val term_hash_ : term -> int
val term_cmp_ : term -> term -> int
val fun_compare : fun_ -> fun_ -> int
val pp_fun : CCFormat.t -> fun_ -> unit
val id_of_fun : fun_ -> ID.t
val eq_ty : ty -> ty -> bool
val eq_cstor : cstor -> cstor -> bool
val eq_value : value -> value -> bool
val hash_value : value Sidekick_util.Hash.t
val pp_value : value Sidekick_util.Util.printer
val pp_db : Stdlib.Format.formatter -> (int * 'a) -> unit
val pp_ty : ty Sidekick_util.Util.printer
val string_of_lra_pred : lra_pred -> string
val pp_pred : Fmt.t -> lra_pred -> unit
val string_of_lra_op : lra_op -> string
val pp_lra_op : Fmt.t -> lra_op -> unit
val pp_term_view_gen : pp_id:(Fmt.t -> ID.t -> unit) -> pp_t:'a Fmt.printer -> Fmt.t -> 'a term_view -> unit
val pp_term_top : ids:bool -> Fmt.t -> term -> unit
val pp_term : Fmt.t -> term -> unit
val pp_term_view : Fmt.t -> term term_view -> unit
module Ty : sig ... end

Types

module Fun : sig ... end

Function symbols

module Term_cell : sig ... end
module Term : sig ... end

Term creation and manipulation

module Value : sig ... end

Values (used in models)

module Data : sig ... end

Datatypes

module Select : sig ... end

Datatype selectors.

module Cstor : sig ... end

Datatype constructors.

module Statement : sig ... end

Statements.

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/ID/B/index.html b/dev/sidekick-base/Sidekick_base/ID/B/index.html deleted file mode 100644 index 67eb647b..00000000 --- a/dev/sidekick-base/Sidekick_base/ID/B/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -B (sidekick-base.Sidekick_base.ID.B)

Module ID.B

val rat : t
val int : t
\ 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 4ab25a99..9cbf3095 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

type t
val make : string -> t
val makef : ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 -> 'a
val copy : t -> t
val id : t -> int
val to_string : t -> string
val to_string_full : t -> string
include Sidekick_util.Intf.EQ with type t := t
type t
val equal : t -> t -> bool
include Sidekick_util.Intf.ORD with type t := t
type t
val compare : t -> t -> int
include Sidekick_util.Intf.HASH with type t := t
type t
val hash : t -> int
include Sidekick_util.Intf.PRINT with type t := t
type t
val pp : t CCFormat.printer
val pp_name : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
module Tbl : CCHashtbl.S with type Tbl.key = t
module B : sig ... end
\ No newline at end of file +ID (sidekick-base.Sidekick_base.ID)

Module Sidekick_base.ID

Unique Identifiers

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_util.Intf.EQ with type t := t
type t
val equal : t -> t -> bool
include Sidekick_util.Intf.ORD with type t := t
type t
val compare : t -> t -> int
include Sidekick_util.Intf.HASH with type t := t
type t
val hash : t -> int
include Sidekick_util.Intf.PRINT with type t := t
type t
val pp : t CCFormat.printer
val pp_name : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Model/Fun_interpretation/index.html b/dev/sidekick-base/Sidekick_base/Model/Fun_interpretation/index.html index 37ea47af..6ab04adf 100644 --- a/dev/sidekick-base/Sidekick_base/Model/Fun_interpretation/index.html +++ b/dev/sidekick-base/Sidekick_base/Model/Fun_interpretation/index.html @@ -1,2 +1,2 @@ -Fun_interpretation (sidekick-base.Sidekick_base.Model.Fun_interpretation)

Module Model.Fun_interpretation

type t = {
cases : Base_types.Value.t Val_map.t;
default : Base_types.Value.t;
}
val default : t -> Base_types.Value.t
val cases_list : t -> (Base_types.Value.t list * Base_types.Value.t) list
val make : default:Base_types.Value.t -> (Base_types.Value.t list * Base_types.Value.t) list -> t
\ No newline at end of file +Fun_interpretation (sidekick-base.Sidekick_base.Model.Fun_interpretation)

Module Model.Fun_interpretation

Model for function symbols.

Function models are a finite map from argument tuples to values, accompanied with a default value that every other argument tuples map to. In other words, it's of the form:

lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault

type t = {
cases : Base_types.Value.t Val_map.t;
default : Base_types.Value.t;
}
val default : t -> Base_types.Value.t
val cases_list : t -> (Base_types.Value.t list * Base_types.Value.t) list
val make : default:Base_types.Value.t -> (Base_types.Value.t list * Base_types.Value.t) list -> t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Model/index.html b/dev/sidekick-base/Sidekick_base/Model/index.html index 47d48969..1f2db5a1 100644 --- a/dev/sidekick-base/Sidekick_base/Model/index.html +++ b/dev/sidekick-base/Sidekick_base/Model/index.html @@ -1,2 +1,2 @@ -Model (sidekick-base.Sidekick_base.Model)

Module Sidekick_base.Model

Model

module Val_map : sig ... end
module Fun_interpretation : sig ... end
type t = {
values : Base_types.Value.t Sidekick_base__.Base_types.Term.Map.t;
funs : Fun_interpretation.t Sidekick_base__.Base_types.Fun.Map.t;
}
val empty : t
val add : Base_types.Term.t -> Base_types.Value.t -> t -> t
val mem : Base_types.Term.t -> t -> bool
val find : Base_types.Term.t -> t -> Base_types.Value.t option
val merge : t -> t -> t
val pp : t CCFormat.printer
val eval : t -> Base_types.Term.t -> Base_types.Value.t option
\ No newline at end of file +Model (sidekick-base.Sidekick_base.Model)

Module Sidekick_base.Model

Models

A model is a solution to the satisfiability question, created by the SMT solver when it proves the formula to be satisfiable.

A model gives a value to each term of the original formula(s), in such a way that the formula(s) is true when the term is replaced by its value.

module Val_map : sig ... end
module Fun_interpretation : sig ... end

Model for function symbols.

type t = {
values : Base_types.Value.t Sidekick_base__.Base_types.Term.Map.t;
funs : Fun_interpretation.t Sidekick_base__.Base_types.Fun.Map.t;
}

Model

val empty : t

Empty model

val add : Base_types.Term.t -> Base_types.Value.t -> t -> t
val mem : Base_types.Term.t -> t -> bool
val find : Base_types.Term.t -> t -> Base_types.Value.t option
val merge : t -> t -> t
val pp : t CCFormat.printer
val eval : t -> Base_types.Term.t -> Base_types.Value.t option

eval m t tries to evaluate term t in the model. If it succeeds, the value is returned, otherwise None is.

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Proof/index.html b/dev/sidekick-base/Sidekick_base/Proof/index.html index 691e25fe..35c36bd9 100644 --- a/dev/sidekick-base/Sidekick_base/Proof/index.html +++ b/dev/sidekick-base/Sidekick_base/Proof/index.html @@ -1,2 +1,2 @@ -Proof (sidekick-base.Sidekick_base.Proof)

Module Sidekick_base.Proof

include Sidekick_core.PROOF with type term = Base_types.Term.t and type ty = Base_types.Ty.t
type term = Base_types.Term.t
type ty = Base_types.Ty.t
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
val isa_split : ty -> term Iter.t -> t
val isa_disj : ty -> term -> term -> t
val cstor_inj : Base_types.Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : string -> term list -> t
val ite_true : term -> t
val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t
\ No newline at end of file +Proof (sidekick-base.Sidekick_base.Proof)

Module Sidekick_base.Proof

Proofs of unsatisfiability

Proofs are used in sidekick when the problem is found unsatisfiable. A proof collects inferences made by the solver into a list of steps, each with its own kind of justification (e.g. "by congruence"), and outputs it in some kind of format.

Currently we target Quip as an experimental proof backend.

include Sidekick_core.PROOF with type term = Base_types.Term.t and type ty = Base_types.Ty.t
type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = Base_types.Term.t
type ty = Base_types.Ty.t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
val isa_split : ty -> term Iter.t -> t
val isa_disj : ty -> term -> term -> t
val cstor_inj : Base_types.Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : string -> term list -> t
val ite_true : term -> t
val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/index.html b/dev/sidekick-base/Sidekick_base/index.html index 9ce512d3..b4036a0d 100644 --- a/dev/sidekick-base/Sidekick_base/index.html +++ b/dev/sidekick-base/Sidekick_base/index.html @@ -1,2 +1,2 @@ -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 Base_types : sig ... end
module ID : sig ... end
module Fun = Base_types.Fun
module Stat = Sidekick_util.Stat
module Model : sig ... end
module Term = Base_types.Term
module Value = Base_types.Value
module Term_cell = Base_types.Term_cell
module Ty = Base_types.Ty
module Statement = Base_types.Statement
module Data = Base_types.Data
module Select = Base_types.Select
module Proof : sig ... end
module Arg : Sidekick_core.TERM with type Term.t = Term.t and type Fun.t = Fun.t and type Ty.t = Ty.t and type Term.state = Term.state
\ 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 Base_types : sig ... end

Basic type definitions for Sidekick_base

module ID : sig ... end

Unique Identifiers

module Fun = Base_types.Fun
module Stat = Sidekick_util.Stat
module Model : sig ... end

Models

module Term = Base_types.Term
module Value = Base_types.Value
module Term_cell = Base_types.Term_cell
module Ty = Base_types.Ty
module Statement = Base_types.Statement
module Data = Base_types.Data
module Select = Base_types.Select
module Proof : sig ... end

Proofs of unsatisfiability

module Arg : Sidekick_core.TERM with type Term.t = Term.t and type Fun.t = Fun.t and type Ty.t = Ty.t and type Term.state = Term.state
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Cstor/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Cstor/index.html index 98a2b957..c6067a5c 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Cstor/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Cstor/index.html @@ -1,2 +1,2 @@ -Cstor (sidekick-base.Sidekick_base__.Base_types.Cstor)

Module Base_types.Cstor

type t = cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
val id : t -> Sidekick_base.ID.t
val ty_args : t -> ty Iter.t
val equal : cstor -> cstor -> bool
val pp : CCFormat.t -> t -> unit
\ No newline at end of file +Cstor (sidekick-base.Sidekick_base__.Base_types.Cstor)

Module Base_types.Cstor

Datatype constructors.

A datatype has one or more constructors, each of which is a special kind of function symbol. Constructors are injective and pairwise distinct.

type t = cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
val id : t -> Sidekick_base.ID.t
val ty_args : t -> ty Iter.t
val equal : cstor -> cstor -> bool
val pp : CCFormat.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Data/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Data/index.html index 07d50057..1233e517 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Data/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Data/index.html @@ -1,2 +1,2 @@ -Data (sidekick-base.Sidekick_base__.Base_types.Data)

Module Base_types.Data

type t = data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
val pp : CCFormat.t -> t -> unit
\ No newline at end of file +Data (sidekick-base.Sidekick_base__.Base_types.Data)

Module Base_types.Data

Datatypes

type t = data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
val pp : CCFormat.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Fun/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Fun/index.html index 21871ac5..28fc9c26 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Fun/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Fun/index.html @@ -1,2 +1,2 @@ -Fun (sidekick-base.Sidekick_base__.Base_types.Fun)

Module Base_types.Fun

type view = fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}
type t = fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}
val id : t -> Sidekick_base.ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val select : select -> t
val select_idx : cstor -> int -> t
val cstor : cstor -> t
val is_a : cstor -> t
val do_cc : t -> bool
val mk_undef : Sidekick_base.ID.t -> Ty.Fun.t -> t
val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t
val pp : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file +Fun (sidekick-base.Sidekick_base__.Base_types.Fun)

Module Base_types.Fun

Function symbols

type view = fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}
type t = fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}
val id : t -> Sidekick_base.ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val select : select -> t
val select_idx : cstor -> int -> t
val cstor : cstor -> t
val is_a : cstor -> t
val do_cc : t -> bool
val mk_undef : Sidekick_base.ID.t -> Ty.Fun.t -> t
val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t
val pp : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Select/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Select/index.html index f24b153b..c42b53bb 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Select/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Select/index.html @@ -1,2 +1,2 @@ -Select (sidekick-base.Sidekick_base__.Base_types.Select)

Module Base_types.Select

type t = select = {
select_id : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
val ty : t -> ty
\ No newline at end of file +Select (sidekick-base.Sidekick_base__.Base_types.Select)

Module Base_types.Select

Datatype selectors.

A selector is a kind of function that allows to obtain an argument of a given constructor.

type t = select = {
select_id : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
val ty : t -> ty
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Statement/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Statement/index.html index 521b0e8e..bea3c4c6 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Statement/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Statement/index.html @@ -1,2 +1,2 @@ -Statement (sidekick-base.Sidekick_base__.Base_types.Statement)

Module Base_types.Statement

type t = 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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val pp : Fmt.t -> t -> unit
\ No newline at end of file +Statement (sidekick-base.Sidekick_base__.Base_types.Statement)

Module Base_types.Statement

Statements.

A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.

type t = 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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val pp : Fmt.t -> t -> unit

Pretty print a statement

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Term/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Term/index.html index 3a54dba7..b72c390e 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Term/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Term/index.html @@ -1,2 +1,2 @@ -Term (sidekick-base.Sidekick_base__.Base_types.Term)

Module Base_types.Term

type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?⁠size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> fun_ -> t
val app_fun : state -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : state -> t -> t -> t
val not_ : state -> t -> t
val ite : state -> t -> t -> t -> t
val select : state -> select -> t -> t
val app_cstor : state -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : state -> cstor -> t -> t
val lra : state -> (Q.t, t) lra_view -> t
val abs : state -> t -> t * bool

Obtain unsigned version of t, + the sign as a boolean

module Iter_dag : sig ... end
val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t
val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t
val pp : t Fmt.printer

Views

val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (fun_, t, t Iter.t) CC_view.t
val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
val as_bool : t -> bool option

Containers

module Tbl : CCHashtbl.S with type Tbl.key = t
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
\ No newline at end of file +Term (sidekick-base.Sidekick_base__.Base_types.Term)

Module Base_types.Term

Term creation and manipulation

type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?⁠size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> fun_ -> t
val app_fun : state -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : state -> t -> t -> t
val not_ : state -> t -> t
val ite : state -> t -> t -> t -> t
val select : state -> select -> t -> t
val app_cstor : state -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : state -> cstor -> t -> t
val lra : state -> (Q.t, t) lra_view -> t
val abs : state -> t -> t * bool

Obtain unsigned version of t, + the sign as a boolean

module Iter_dag : sig ... end
val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t
val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t
val pp : t Fmt.printer

Views

val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (fun_, t, t Iter.t) CC_view.t
val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
val as_bool : t -> bool option

Containers

module Tbl : CCHashtbl.S with type Tbl.key = t
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Ty/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Ty/index.html index 6abbfba6..ca529d12 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Ty/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Ty/index.html @@ -1,2 +1,2 @@ -Ty (sidekick-base.Sidekick_base__.Base_types.Ty)

Module Base_types.Ty

type t = ty
type state = unit
type view = ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
type def = ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
val id : t -> int
val view : t -> view
val bool : state -> t
val real : state -> t
val atomic : def -> t list -> t
val id_of_def : def -> Sidekick_base.ID.t
val atomic_uninterpreted : Sidekick_base.ID.t -> t
val finite : t -> bool
val set_finite : t -> bool -> unit
val is_bool : t -> bool
val is_uninterpreted : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t CCFormat.printer
module Tbl : CCHashtbl.S with type Tbl.key = t
module Fun : sig ... end
\ No newline at end of file +Ty (sidekick-base.Sidekick_base__.Base_types.Ty)

Module Base_types.Ty

Types

type t = ty
type state = unit
type view = ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
type def = ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
val id : t -> int
val view : t -> view
val bool : state -> t
val real : state -> t
val atomic : def -> t list -> t
val id_of_def : def -> Sidekick_base.ID.t
val atomic_uninterpreted : Sidekick_base.ID.t -> t
val finite : t -> bool
val set_finite : t -> bool -> unit
val is_bool : t -> bool
val is_uninterpreted : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t CCFormat.printer
module Tbl : CCHashtbl.S with type Tbl.key = t
module Fun : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/Value/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Value/index.html index ff6444b5..58050d61 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/Value/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Value/index.html @@ -1,2 +1,2 @@ -Value (sidekick-base.Sidekick_base__.Base_types.Value)

Module Base_types.Value

type t = value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}
| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}
| V_real of Q.t
val true_ : t
val false_ : t
val bool : bool -> t
val real : Q.t -> t
val real_of_string : string -> t
val mk_elt : Sidekick_base.ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val cstor_app : cstor -> t list -> t
val fresh : Term.t -> t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
\ No newline at end of file +Value (sidekick-base.Sidekick_base__.Base_types.Value)

Module Base_types.Value

Values (used in models)

type t = value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}
| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}
| V_real of Q.t
val true_ : t
val false_ : t
val bool : bool -> t
val real : Q.t -> t
val real_of_string : string -> t
val mk_elt : Sidekick_base.ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val cstor_app : cstor -> t list -> t
val fresh : Term.t -> t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Base_types/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/index.html index a763837b..ed1ab6d8 100644 --- a/dev/sidekick-base/Sidekick_base__/Base_types/index.html +++ b/dev/sidekick-base/Sidekick_base__/Base_types/index.html @@ -1,2 +1,2 @@ -Base_types (sidekick-base.Sidekick_base__.Base_types)

Module Sidekick_base__.Base_types

module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
type lra_pred = Sidekick_arith_lra.Predicate.t =
| Leq
| Geq
| Lt
| Gt
| Eq
| Neq
type lra_op = Sidekick_arith_lra.op =
| Plus
| Minus
type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
| LRA_pred of lra_pred * 'a * 'a
| LRA_op of lra_op * 'a * 'a
| LRA_mult of 'num * 'a
| LRA_const of 'num
| LRA_simplex_var of 'a
| LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
| LRA_other of 'a
type term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : term term_view;
}
and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
and fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}
and fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}

Methods on the custom term view whose arguments are 'a. Terms must be printable, and provide some additional theory handles.

  • relevant must return a subset of args (possibly the same set). The terms it returns will be activated and evaluated whenever possible. Terms in args \ relevant args are considered for congruence but not for evaluation.
and fun_ty = {
fun_ty_args : ty list;
fun_ty_ret : ty;
}

Function type

and ty = {
mutable ty_id : int;
ty_view : ty_view;
}

Hashconsed type

and ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
and ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
and data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.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 : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
and value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}

a named constant, distinct from any other constant

| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}

Custom value

| V_real of Q.t

Semantic values, used for models (and possibly model-constructing calculi)

and value_custom_view = ..
type definition = Sidekick_base.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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val term_equal_ : term -> term -> bool
val term_hash_ : term -> int
val term_cmp_ : term -> term -> int
val fun_compare : fun_ -> fun_ -> int
val pp_fun : CCFormat.t -> fun_ -> unit
val id_of_fun : fun_ -> Sidekick_base.ID.t
val eq_ty : ty -> ty -> bool
val eq_cstor : cstor -> cstor -> bool
val eq_value : value -> value -> bool
val hash_value : value Sidekick_util.Hash.t
val pp_value : value Sidekick_util.Util.printer
val pp_db : Stdlib.Format.formatter -> (int * 'a) -> unit
val pp_ty : ty Sidekick_util.Util.printer
val string_of_lra_pred : lra_pred -> string
val pp_pred : Fmt.t -> lra_pred -> unit
val string_of_lra_op : lra_op -> string
val pp_lra_op : Fmt.t -> lra_op -> unit
val pp_term_view_gen : pp_id:(Fmt.t -> Sidekick_base.ID.t -> unit) -> pp_t:'a Fmt.printer -> Fmt.t -> 'a term_view -> unit
val pp_term_top : ids:bool -> Fmt.t -> term -> unit
val pp_term : Fmt.t -> term -> unit
val pp_term_view : Fmt.t -> term term_view -> unit
module Ty : sig ... end
module Fun : sig ... end
module Term_cell : sig ... end
module Term : sig ... end
module Value : sig ... end
module Data : sig ... end
module Select : sig ... end
module Cstor : sig ... end
module Statement : sig ... end
\ No newline at end of file +Base_types (sidekick-base.Sidekick_base__.Base_types)

Module Sidekick_base__.Base_types

module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
type lra_pred = Sidekick_arith_lra.Predicate.t =
| Leq
| Geq
| Lt
| Gt
| Eq
| Neq
type lra_op = Sidekick_arith_lra.op =
| Plus
| Minus
type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
| LRA_pred of lra_pred * 'a * 'a
| LRA_op of lra_op * 'a * 'a
| LRA_mult of 'num * 'a
| LRA_const of 'num
| LRA_simplex_var of 'a
| LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
| LRA_other of 'a
type term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : term term_view;
}

Term.

A term, with its own view, type, and a unique identifier. Do not create directly, see Term.

and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view

Shallow structure of a term.

A term is a DAG (direct acyclic graph) of nodes, each of which has a term view.

and fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}

type of function symbols

and fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}

Methods on the custom term view whose arguments are 'a. Terms must be printable, and provide some additional theory handles.

  • relevant must return a subset of args (possibly the same set). The terms it returns will be activated and evaluated whenever possible. Terms in args \ relevant args are considered for congruence but not for evaluation.
and fun_ty = {
fun_ty_args : ty list;
fun_ty_ret : ty;
}

Function type

and ty = {
mutable ty_id : int;
ty_view : ty_view;
}

Hashconsed type

and ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
and ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
and data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.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 : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
and value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}

a named constant, distinct from any other constant

| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}

Custom value

| V_real of Q.t

Semantic values, used for models (and possibly model-constructing calculi)

and value_custom_view = ..
type definition = Sidekick_base.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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val term_equal_ : term -> term -> bool
val term_hash_ : term -> int
val term_cmp_ : term -> term -> int
val fun_compare : fun_ -> fun_ -> int
val pp_fun : CCFormat.t -> fun_ -> unit
val id_of_fun : fun_ -> Sidekick_base.ID.t
val eq_ty : ty -> ty -> bool
val eq_cstor : cstor -> cstor -> bool
val eq_value : value -> value -> bool
val hash_value : value Sidekick_util.Hash.t
val pp_value : value Sidekick_util.Util.printer
val pp_db : Stdlib.Format.formatter -> (int * 'a) -> unit
val pp_ty : ty Sidekick_util.Util.printer
val string_of_lra_pred : lra_pred -> string
val pp_pred : Fmt.t -> lra_pred -> unit
val string_of_lra_op : lra_op -> string
val pp_lra_op : Fmt.t -> lra_op -> unit
val pp_term_view_gen : pp_id:(Fmt.t -> Sidekick_base.ID.t -> unit) -> pp_t:'a Fmt.printer -> Fmt.t -> 'a term_view -> unit
val pp_term_top : ids:bool -> Fmt.t -> term -> unit
val pp_term : Fmt.t -> term -> unit
val pp_term_view : Fmt.t -> term term_view -> unit
module Ty : sig ... end

Types

module Fun : sig ... end

Function symbols

module Term_cell : sig ... end
module Term : sig ... end

Term creation and manipulation

module Value : sig ... end

Values (used in models)

module Data : sig ... end

Datatypes

module Select : sig ... end

Datatype selectors.

module Cstor : sig ... end

Datatype constructors.

module Statement : sig ... end

Statements.

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/ID/B/index.html b/dev/sidekick-base/Sidekick_base__/ID/B/index.html deleted file mode 100644 index d9bae380..00000000 --- a/dev/sidekick-base/Sidekick_base__/ID/B/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -B (sidekick-base.Sidekick_base__.ID.B)

Module ID.B

val rat : t
val int : t
\ 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 6b64eed7..75c114e3 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

type t
val make : string -> t
val makef : ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 -> 'a
val copy : t -> t
val id : t -> int
val to_string : t -> string
val to_string_full : t -> string
include Sidekick_util.Intf.EQ with type t := t
type t
val equal : t -> t -> bool
include Sidekick_util.Intf.ORD with type t := t
type t
val compare : t -> t -> int
include Sidekick_util.Intf.HASH with type t := t
type t
val hash : t -> int
include Sidekick_util.Intf.PRINT with type t := t
type t
val pp : t CCFormat.printer
val pp_name : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
module Tbl : CCHashtbl.S with type Tbl.key = t
module B : sig ... end
\ No newline at end of file +ID (sidekick-base.Sidekick_base__.ID)

Module Sidekick_base__.ID

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_util.Intf.EQ with type t := t
type t
val equal : t -> t -> bool
include Sidekick_util.Intf.ORD with type t := t
type t
val compare : t -> t -> int
include Sidekick_util.Intf.HASH with type t := t
type t
val hash : t -> int
include Sidekick_util.Intf.PRINT with type t := t
type t
val pp : t CCFormat.printer
val pp_name : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Model/Fun_interpretation/index.html b/dev/sidekick-base/Sidekick_base__/Model/Fun_interpretation/index.html index d58677a5..8e4cd0b8 100644 --- a/dev/sidekick-base/Sidekick_base__/Model/Fun_interpretation/index.html +++ b/dev/sidekick-base/Sidekick_base__/Model/Fun_interpretation/index.html @@ -1,2 +1,2 @@ -Fun_interpretation (sidekick-base.Sidekick_base__.Model.Fun_interpretation)

Module Model.Fun_interpretation

type t = {
cases : Sidekick_base.Base_types.Value.t Val_map.t;
default : Sidekick_base.Base_types.Value.t;
}
val default : t -> Sidekick_base.Base_types.Value.t
val cases_list : t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list
val make : default:Sidekick_base.Base_types.Value.t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list -> t
\ No newline at end of file +Fun_interpretation (sidekick-base.Sidekick_base__.Model.Fun_interpretation)

Module Model.Fun_interpretation

Model for function symbols.

Function models are a finite map from argument tuples to values, accompanied with a default value that every other argument tuples map to. In other words, it's of the form:

lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault

type t = {
cases : Sidekick_base.Base_types.Value.t Val_map.t;
default : Sidekick_base.Base_types.Value.t;
}
val default : t -> Sidekick_base.Base_types.Value.t
val cases_list : t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list
val make : default:Sidekick_base.Base_types.Value.t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list -> t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Model/index.html b/dev/sidekick-base/Sidekick_base__/Model/index.html index 98a9f546..919ac29d 100644 --- a/dev/sidekick-base/Sidekick_base__/Model/index.html +++ b/dev/sidekick-base/Sidekick_base__/Model/index.html @@ -1,2 +1,2 @@ -Model (sidekick-base.Sidekick_base__.Model)

Module Sidekick_base__.Model

Model

module Val_map : sig ... end
module Fun_interpretation : sig ... end
type t = {
values : Sidekick_base.Base_types.Value.t Sidekick_base__.Base_types.Term.Map.t;
funs : Fun_interpretation.t Sidekick_base__.Base_types.Fun.Map.t;
}
val empty : t
val add : Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t -> t -> t
val mem : Sidekick_base.Base_types.Term.t -> t -> bool
val find : Sidekick_base.Base_types.Term.t -> t -> Sidekick_base.Base_types.Value.t option
val merge : t -> t -> t
val pp : t CCFormat.printer
val eval : t -> Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t option
\ No newline at end of file +Model (sidekick-base.Sidekick_base__.Model)

Module Sidekick_base__.Model

module Val_map : sig ... end
module Fun_interpretation : sig ... end

Model for function symbols.

type t = {
values : Sidekick_base.Base_types.Value.t Sidekick_base__.Base_types.Term.Map.t;
funs : Fun_interpretation.t Sidekick_base__.Base_types.Fun.Map.t;
}

Model

val empty : t

Empty model

val add : Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t -> t -> t
val mem : Sidekick_base.Base_types.Term.t -> t -> bool
val find : Sidekick_base.Base_types.Term.t -> t -> Sidekick_base.Base_types.Value.t option
val merge : t -> t -> t
val pp : t CCFormat.printer
val eval : t -> Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t option

eval m t tries to evaluate term t in the model. If it succeeds, the value is returned, otherwise None is.

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__/Proof/index.html b/dev/sidekick-base/Sidekick_base__/Proof/index.html index c558cfe6..4107056c 100644 --- a/dev/sidekick-base/Sidekick_base__/Proof/index.html +++ b/dev/sidekick-base/Sidekick_base__/Proof/index.html @@ -1,2 +1,2 @@ -Proof (sidekick-base.Sidekick_base__.Proof)

Module Sidekick_base__.Proof

include Sidekick_core.PROOF with type term = Sidekick_base.Base_types.Term.t and type ty = Sidekick_base.Base_types.Ty.t
type term = Sidekick_base.Base_types.Term.t
type ty = Sidekick_base.Base_types.Ty.t
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
val isa_split : ty -> term Iter.t -> t
val isa_disj : ty -> term -> term -> t
val cstor_inj : Sidekick_base.Base_types.Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : string -> term list -> t
val ite_true : term -> t
val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t
\ No newline at end of file +Proof (sidekick-base.Sidekick_base__.Proof)

Module Sidekick_base__.Proof

include Sidekick_core.PROOF with type term = Sidekick_base.Base_types.Term.t and type ty = Sidekick_base.Base_types.Ty.t
type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = Sidekick_base.Base_types.Term.t
type ty = Sidekick_base.Base_types.Ty.t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
val isa_split : ty -> term Iter.t -> t
val isa_disj : ty -> term -> term -> t
val cstor_inj : Sidekick_base.Base_types.Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : string -> term list -> t
val ite_true : term -> t
val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Cstor/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Cstor/index.html index ed988f86..6156c352 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Cstor/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Cstor/index.html @@ -1,2 +1,2 @@ -Cstor (sidekick-base.Sidekick_base__Base_types.Cstor)

Module Sidekick_base__Base_types.Cstor

type t = cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
val id : t -> Sidekick_base.ID.t
val ty_args : t -> ty Iter.t
val equal : cstor -> cstor -> bool
val pp : CCFormat.t -> t -> unit
\ No newline at end of file +Cstor (sidekick-base.Sidekick_base__Base_types.Cstor)

Module Sidekick_base__Base_types.Cstor

Datatype constructors.

A datatype has one or more constructors, each of which is a special kind of function symbol. Constructors are injective and pairwise distinct.

type t = cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
val id : t -> Sidekick_base.ID.t
val ty_args : t -> ty Iter.t
val equal : cstor -> cstor -> bool
val pp : CCFormat.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Data/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Data/index.html index 43483e9d..09cda25e 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Data/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Data/index.html @@ -1,2 +1,2 @@ -Data (sidekick-base.Sidekick_base__Base_types.Data)

Module Sidekick_base__Base_types.Data

type t = data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
val pp : CCFormat.t -> t -> unit
\ No newline at end of file +Data (sidekick-base.Sidekick_base__Base_types.Data)

Module Sidekick_base__Base_types.Data

Datatypes

type t = data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
val pp : CCFormat.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Fun/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Fun/index.html index 59f2a4ef..9e43e23e 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Fun/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Fun/index.html @@ -1,2 +1,2 @@ -Fun (sidekick-base.Sidekick_base__Base_types.Fun)

Module Sidekick_base__Base_types.Fun

type view = fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}
type t = fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}
val id : t -> Sidekick_base.ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val select : select -> t
val select_idx : cstor -> int -> t
val cstor : cstor -> t
val is_a : cstor -> t
val do_cc : t -> bool
val mk_undef : Sidekick_base.ID.t -> Ty.Fun.t -> t
val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t
val pp : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file +Fun (sidekick-base.Sidekick_base__Base_types.Fun)

Module Sidekick_base__Base_types.Fun

Function symbols

type view = fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}
type t = fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}
val id : t -> Sidekick_base.ID.t
val view : t -> view
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val as_undefined : t -> (t * Ty.Fun.t) option
val as_undefined_exn : t -> t * Ty.Fun.t
val is_undefined : t -> bool
val select : select -> t
val select_idx : cstor -> int -> t
val cstor : cstor -> t
val is_a : cstor -> t
val do_cc : t -> bool
val mk_undef : Sidekick_base.ID.t -> Ty.Fun.t -> t
val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t
val pp : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Select/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Select/index.html index 2dd2f07b..9861d9f7 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Select/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Select/index.html @@ -1,2 +1,2 @@ -Select (sidekick-base.Sidekick_base__Base_types.Select)

Module Sidekick_base__Base_types.Select

type t = select = {
select_id : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
val ty : t -> ty
\ No newline at end of file +Select (sidekick-base.Sidekick_base__Base_types.Select)

Module Sidekick_base__Base_types.Select

Datatype selectors.

A selector is a kind of function that allows to obtain an argument of a given constructor.

type t = select = {
select_id : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
val ty : t -> ty
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Statement/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Statement/index.html index be8a522b..2432ff39 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Statement/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Statement/index.html @@ -1,2 +1,2 @@ -Statement (sidekick-base.Sidekick_base__Base_types.Statement)

Module Sidekick_base__Base_types.Statement

type t = 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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val pp : Fmt.t -> t -> unit
\ No newline at end of file +Statement (sidekick-base.Sidekick_base__Base_types.Statement)

Module Sidekick_base__Base_types.Statement

Statements.

A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.

type t = 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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val pp : Fmt.t -> t -> unit

Pretty print a statement

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Term/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Term/index.html index 51691135..05d8be02 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Term/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Term/index.html @@ -1,2 +1,2 @@ -Term (sidekick-base.Sidekick_base__Base_types.Term)

Module Sidekick_base__Base_types.Term

type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?⁠size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> fun_ -> t
val app_fun : state -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : state -> t -> t -> t
val not_ : state -> t -> t
val ite : state -> t -> t -> t -> t
val select : state -> select -> t -> t
val app_cstor : state -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : state -> cstor -> t -> t
val lra : state -> (Q.t, t) lra_view -> t
val abs : state -> t -> t * bool

Obtain unsigned version of t, + the sign as a boolean

module Iter_dag : sig ... end
val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t
val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t
val pp : t Fmt.printer

Views

val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (fun_, t, t Iter.t) CC_view.t
val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
val as_bool : t -> bool option

Containers

module Tbl : CCHashtbl.S with type Tbl.key = t
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
\ No newline at end of file +Term (sidekick-base.Sidekick_base__Base_types.Term)

Module Sidekick_base__Base_types.Term

Term creation and manipulation

type t = term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : t term_view;
}
type 'a view = 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
val id : t -> int
val view : t -> term view
val ty : t -> Ty.t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
type state
val create : ?⁠size:int -> unit -> state
val make : state -> t view -> t
val true_ : state -> t
val false_ : state -> t
val bool : state -> bool -> t
val const : state -> fun_ -> t
val app_fun : state -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : state -> t -> t -> t
val not_ : state -> t -> t
val ite : state -> t -> t -> t -> t
val select : state -> select -> t -> t
val app_cstor : state -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : state -> cstor -> t -> t
val lra : state -> (Q.t, t) lra_view -> t
val abs : state -> t -> t * bool

Obtain unsigned version of t, + the sign as a boolean

module Iter_dag : sig ... end
val iter_dag_with : order:Iter_dag.order -> t -> t Iter.t
val iter_dag : t -> t Iter.t
val map_shallow : state -> (t -> t) -> t -> t
val pp : t Fmt.printer

Views

val is_true : t -> bool
val is_false : t -> bool
val is_const : t -> bool
val cc_view : t -> (fun_, t, t Iter.t) CC_view.t
val as_fun_undef : t -> (fun_ * Ty.Fun.t) option
val as_bool : t -> bool option

Containers

module Tbl : CCHashtbl.S with type Tbl.key = t
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Ty/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Ty/index.html index 0dd1230b..3444603e 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Ty/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Ty/index.html @@ -1,2 +1,2 @@ -Ty (sidekick-base.Sidekick_base__Base_types.Ty)

Module Sidekick_base__Base_types.Ty

type t = ty
type state = unit
type view = ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
type def = ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
val id : t -> int
val view : t -> view
val bool : state -> t
val real : state -> t
val atomic : def -> t list -> t
val id_of_def : def -> Sidekick_base.ID.t
val atomic_uninterpreted : Sidekick_base.ID.t -> t
val finite : t -> bool
val set_finite : t -> bool -> unit
val is_bool : t -> bool
val is_uninterpreted : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t CCFormat.printer
module Tbl : CCHashtbl.S with type Tbl.key = t
module Fun : sig ... end
\ No newline at end of file +Ty (sidekick-base.Sidekick_base__Base_types.Ty)

Module Sidekick_base__Base_types.Ty

Types

type t = ty
type state = unit
type view = ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
type def = ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
val id : t -> int
val view : t -> view
val bool : state -> t
val real : state -> t
val atomic : def -> t list -> t
val id_of_def : def -> Sidekick_base.ID.t
val atomic_uninterpreted : Sidekick_base.ID.t -> t
val finite : t -> bool
val set_finite : t -> bool -> unit
val is_bool : t -> bool
val is_uninterpreted : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp : t CCFormat.printer
module Tbl : CCHashtbl.S with type Tbl.key = t
module Fun : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/Value/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Value/index.html index 23d57206..67ad8d0a 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/Value/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/Value/index.html @@ -1,2 +1,2 @@ -Value (sidekick-base.Sidekick_base__Base_types.Value)

Module Sidekick_base__Base_types.Value

type t = value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}
| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}
| V_real of Q.t
val true_ : t
val false_ : t
val bool : bool -> t
val real : Q.t -> t
val real_of_string : string -> t
val mk_elt : Sidekick_base.ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val cstor_app : cstor -> t list -> t
val fresh : Term.t -> t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
\ No newline at end of file +Value (sidekick-base.Sidekick_base__Base_types.Value)

Module Sidekick_base__Base_types.Value

Values (used in models)

type t = value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}
| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}
| V_real of Q.t
val true_ : t
val false_ : t
val bool : bool -> t
val real : Q.t -> t
val real_of_string : string -> t
val mk_elt : Sidekick_base.ID.t -> Ty.t -> t
val is_bool : t -> bool
val is_true : t -> bool
val is_false : t -> bool
val cstor_app : cstor -> t list -> t
val fresh : Term.t -> t
val hash : t -> int
val equal : t -> t -> bool
val pp : t Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Base_types/index.html b/dev/sidekick-base/Sidekick_base__Base_types/index.html index bd18d812..d4a9c01c 100644 --- a/dev/sidekick-base/Sidekick_base__Base_types/index.html +++ b/dev/sidekick-base/Sidekick_base__Base_types/index.html @@ -1,2 +1,2 @@ -Sidekick_base__Base_types (sidekick-base.Sidekick_base__Base_types)

Module Sidekick_base__Base_types

module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
type lra_pred = Sidekick_arith_lra.Predicate.t =
| Leq
| Geq
| Lt
| Gt
| Eq
| Neq
type lra_op = Sidekick_arith_lra.op =
| Plus
| Minus
type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
| LRA_pred of lra_pred * 'a * 'a
| LRA_op of lra_op * 'a * 'a
| LRA_mult of 'num * 'a
| LRA_const of 'num
| LRA_simplex_var of 'a
| LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
| LRA_other of 'a
type term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : term term_view;
}
and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view
and fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}
and fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}

Methods on the custom term view whose arguments are 'a. Terms must be printable, and provide some additional theory handles.

  • relevant must return a subset of args (possibly the same set). The terms it returns will be activated and evaluated whenever possible. Terms in args \ relevant args are considered for congruence but not for evaluation.
and fun_ty = {
fun_ty_args : ty list;
fun_ty_ret : ty;
}

Function type

and ty = {
mutable ty_id : int;
ty_view : ty_view;
}

Hashconsed type

and ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
and ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
and data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.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 : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
and value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}

a named constant, distinct from any other constant

| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}

Custom value

| V_real of Q.t

Semantic values, used for models (and possibly model-constructing calculi)

and value_custom_view = ..
type definition = Sidekick_base.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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val term_equal_ : term -> term -> bool
val term_hash_ : term -> int
val term_cmp_ : term -> term -> int
val fun_compare : fun_ -> fun_ -> int
val pp_fun : CCFormat.t -> fun_ -> unit
val id_of_fun : fun_ -> Sidekick_base.ID.t
val eq_ty : ty -> ty -> bool
val eq_cstor : cstor -> cstor -> bool
val eq_value : value -> value -> bool
val hash_value : value Sidekick_util.Hash.t
val pp_value : value Sidekick_util.Util.printer
val pp_db : Stdlib.Format.formatter -> (int * 'a) -> unit
val pp_ty : ty Sidekick_util.Util.printer
val string_of_lra_pred : lra_pred -> string
val pp_pred : Fmt.t -> lra_pred -> unit
val string_of_lra_op : lra_op -> string
val pp_lra_op : Fmt.t -> lra_op -> unit
val pp_term_view_gen : pp_id:(Fmt.t -> Sidekick_base.ID.t -> unit) -> pp_t:'a Fmt.printer -> Fmt.t -> 'a term_view -> unit
val pp_term_top : ids:bool -> Fmt.t -> term -> unit
val pp_term : Fmt.t -> term -> unit
val pp_term_view : Fmt.t -> term term_view -> unit
module Ty : sig ... end
module Fun : sig ... end
module Term_cell : sig ... end
module Term : sig ... end
module Value : sig ... end
module Data : sig ... end
module Select : sig ... end
module Cstor : sig ... end
module Statement : sig ... end
\ No newline at end of file +Sidekick_base__Base_types (sidekick-base.Sidekick_base__Base_types)

Module Sidekick_base__Base_types

Basic type definitions for Sidekick_base

module Vec = Msat.Vec
module Log = Msat.Log
module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
type lra_pred = Sidekick_arith_lra.Predicate.t =
| Leq
| Geq
| Lt
| Gt
| Eq
| Neq
type lra_op = Sidekick_arith_lra.op =
| Plus
| Minus
type ('num, 'a) lra_view = ('num, 'a) Sidekick_arith_lra.lra_view =
| LRA_pred of lra_pred * 'a * 'a
| LRA_op of lra_op * 'a * 'a
| LRA_mult of 'num * 'a
| LRA_const of 'num
| LRA_simplex_var of 'a
| LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
| LRA_other of 'a
type term = {
mutable term_id : int;
mutable term_ty : ty;
term_view : term term_view;
}

Term.

A term, with its own view, type, and a unique identifier. Do not create directly, see Term.

and 'a term_view =
| Bool of bool
| App_fun of fun_ * 'a Sidekick_util.IArray.t
| Eq of 'a * 'a
| Not of 'a
| Ite of 'a * 'a * 'a
| LRA of (Q.t, 'a) lra_view

Shallow structure of a term.

A term is a DAG (direct acyclic graph) of nodes, each of which has a term view.

and fun_ = {
fun_id : Sidekick_base.ID.t;
fun_view : fun_view;
}

type of function symbols

and fun_view =
| Fun_undef of fun_ty
| Fun_select of select
| Fun_cstor of cstor
| Fun_is_a of cstor
| Fun_def of {
pp : a. ('a Fmt.printer -> 'a Sidekick_util.IArray.t Fmt.printer) option;
abs : self:term -> term Sidekick_util.IArray.t -> term * bool;
do_cc : bool;
relevant : a. Sidekick_base.ID.t -> 'a Sidekick_util.IArray.t -> int -> bool;
ty : Sidekick_base.ID.t -> term Sidekick_util.IArray.t -> ty;
eval : value Sidekick_util.IArray.t -> value;
}

Methods on the custom term view whose arguments are 'a. Terms must be printable, and provide some additional theory handles.

  • relevant must return a subset of args (possibly the same set). The terms it returns will be activated and evaluated whenever possible. Terms in args \ relevant args are considered for congruence but not for evaluation.
and fun_ty = {
fun_ty_args : ty list;
fun_ty_ret : ty;
}

Function type

and ty = {
mutable ty_id : int;
ty_view : ty_view;
}

Hashconsed type

and ty_view =
| Ty_bool
| Ty_real
| Ty_atomic of {
def : ty_def;
args : ty list;
mutable finite : bool;
}
and ty_def =
| Ty_uninterpreted of Sidekick_base.ID.t
| Ty_data of {
data : data;
}
| Ty_def of {
id : Sidekick_base.ID.t;
pp : ty Fmt.printer -> ty list Fmt.printer;
default_val : value list -> value;
}
and data = {
data_id : Sidekick_base.ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : Sidekick_base.ID.t;
cstor_is_a : Sidekick_base.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 : Sidekick_base.ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
and value =
| V_bool of bool
| V_element of {
id : Sidekick_base.ID.t;
ty : ty;
}

a named constant, distinct from any other constant

| V_cstor of {
c : cstor;
args : value list;
}
| V_custom of {
view : value_custom_view;
pp : value_custom_view Fmt.printer;
eq : value_custom_view -> value_custom_view -> bool;
hash : value_custom_view -> int;
}

Custom value

| V_real of Q.t

Semantic values, used for models (and possibly model-constructing calculi)

and value_custom_view = ..
type definition = Sidekick_base.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 Sidekick_base.ID.t * int
| Stmt_decl of Sidekick_base.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_exit
val term_equal_ : term -> term -> bool
val term_hash_ : term -> int
val term_cmp_ : term -> term -> int
val fun_compare : fun_ -> fun_ -> int
val pp_fun : CCFormat.t -> fun_ -> unit
val id_of_fun : fun_ -> Sidekick_base.ID.t
val eq_ty : ty -> ty -> bool
val eq_cstor : cstor -> cstor -> bool
val eq_value : value -> value -> bool
val hash_value : value Sidekick_util.Hash.t
val pp_value : value Sidekick_util.Util.printer
val pp_db : Stdlib.Format.formatter -> (int * 'a) -> unit
val pp_ty : ty Sidekick_util.Util.printer
val string_of_lra_pred : lra_pred -> string
val pp_pred : Fmt.t -> lra_pred -> unit
val string_of_lra_op : lra_op -> string
val pp_lra_op : Fmt.t -> lra_op -> unit
val pp_term_view_gen : pp_id:(Fmt.t -> Sidekick_base.ID.t -> unit) -> pp_t:'a Fmt.printer -> Fmt.t -> 'a term_view -> unit
val pp_term_top : ids:bool -> Fmt.t -> term -> unit
val pp_term : Fmt.t -> term -> unit
val pp_term_view : Fmt.t -> term term_view -> unit
module Ty : sig ... end

Types

module Fun : sig ... end

Function symbols

module Term_cell : sig ... end
module Term : sig ... end

Term creation and manipulation

module Value : sig ... end

Values (used in models)

module Data : sig ... end

Datatypes

module Select : sig ... end

Datatype selectors.

module Cstor : sig ... end

Datatype constructors.

module Statement : sig ... end

Statements.

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

Module Sidekick_base__ID.B

val rat : t
val int : t
\ 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 f44afd12..b606d18b 100644 --- a/dev/sidekick-base/Sidekick_base__ID/index.html +++ b/dev/sidekick-base/Sidekick_base__ID/index.html @@ -1,2 +1,2 @@ -Sidekick_base__ID (sidekick-base.Sidekick_base__ID)

Module Sidekick_base__ID

Unique Identifiers

type t
val make : string -> t
val makef : ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 -> 'a
val copy : t -> t
val id : t -> int
val to_string : t -> string
val to_string_full : t -> string
include Sidekick_util.Intf.EQ with type t := t
type t
val equal : t -> t -> bool
include Sidekick_util.Intf.ORD with type t := t
type t
val compare : t -> t -> int
include Sidekick_util.Intf.HASH with type t := t
type t
val hash : t -> int
include Sidekick_util.Intf.PRINT with type t := t
type t
val pp : t CCFormat.printer
val pp_name : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
module Tbl : CCHashtbl.S with type Tbl.key = t
module B : sig ... end
\ No newline at end of file +Sidekick_base__ID (sidekick-base.Sidekick_base__ID)

Module Sidekick_base__ID

Unique Identifiers

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_util.Intf.EQ with type t := t
type t
val equal : t -> t -> bool
include Sidekick_util.Intf.ORD with type t := t
type t
val compare : t -> t -> int
include Sidekick_util.Intf.HASH with type t := t
type t
val hash : t -> int
include Sidekick_util.Intf.PRINT with type t := t
type t
val pp : t CCFormat.printer
val pp_name : t CCFormat.printer
module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
module Tbl : CCHashtbl.S with type Tbl.key = t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Model/Fun_interpretation/index.html b/dev/sidekick-base/Sidekick_base__Model/Fun_interpretation/index.html index 041dbd9c..cd912390 100644 --- a/dev/sidekick-base/Sidekick_base__Model/Fun_interpretation/index.html +++ b/dev/sidekick-base/Sidekick_base__Model/Fun_interpretation/index.html @@ -1,2 +1,2 @@ -Fun_interpretation (sidekick-base.Sidekick_base__Model.Fun_interpretation)

Module Sidekick_base__Model.Fun_interpretation

type t = {
cases : Sidekick_base.Base_types.Value.t Val_map.t;
default : Sidekick_base.Base_types.Value.t;
}
val default : t -> Sidekick_base.Base_types.Value.t
val cases_list : t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list
val make : default:Sidekick_base.Base_types.Value.t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list -> t
\ No newline at end of file +Fun_interpretation (sidekick-base.Sidekick_base__Model.Fun_interpretation)

Module Sidekick_base__Model.Fun_interpretation

Model for function symbols.

Function models are a finite map from argument tuples to values, accompanied with a default value that every other argument tuples map to. In other words, it's of the form:

lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault

type t = {
cases : Sidekick_base.Base_types.Value.t Val_map.t;
default : Sidekick_base.Base_types.Value.t;
}
val default : t -> Sidekick_base.Base_types.Value.t
val cases_list : t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list
val make : default:Sidekick_base.Base_types.Value.t -> (Sidekick_base.Base_types.Value.t list * Sidekick_base.Base_types.Value.t) list -> t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Model/index.html b/dev/sidekick-base/Sidekick_base__Model/index.html index 5b12b4a2..5e05e85d 100644 --- a/dev/sidekick-base/Sidekick_base__Model/index.html +++ b/dev/sidekick-base/Sidekick_base__Model/index.html @@ -1,2 +1,2 @@ -Sidekick_base__Model (sidekick-base.Sidekick_base__Model)

Module Sidekick_base__Model

Model

module Val_map : sig ... end
module Fun_interpretation : sig ... end
type t = {
values : Sidekick_base.Base_types.Value.t Sidekick_base__.Base_types.Term.Map.t;
funs : Fun_interpretation.t Sidekick_base__.Base_types.Fun.Map.t;
}
val empty : t
val add : Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t -> t -> t
val mem : Sidekick_base.Base_types.Term.t -> t -> bool
val find : Sidekick_base.Base_types.Term.t -> t -> Sidekick_base.Base_types.Value.t option
val merge : t -> t -> t
val pp : t CCFormat.printer
val eval : t -> Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t option
\ No newline at end of file +Sidekick_base__Model (sidekick-base.Sidekick_base__Model)

Module Sidekick_base__Model

Models

A model is a solution to the satisfiability question, created by the SMT solver when it proves the formula to be satisfiable.

A model gives a value to each term of the original formula(s), in such a way that the formula(s) is true when the term is replaced by its value.

module Val_map : sig ... end
module Fun_interpretation : sig ... end

Model for function symbols.

type t = {
values : Sidekick_base.Base_types.Value.t Sidekick_base__.Base_types.Term.Map.t;
funs : Fun_interpretation.t Sidekick_base__.Base_types.Fun.Map.t;
}

Model

val empty : t

Empty model

val add : Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t -> t -> t
val mem : Sidekick_base.Base_types.Term.t -> t -> bool
val find : Sidekick_base.Base_types.Term.t -> t -> Sidekick_base.Base_types.Value.t option
val merge : t -> t -> t
val pp : t CCFormat.printer
val eval : t -> Sidekick_base.Base_types.Term.t -> Sidekick_base.Base_types.Value.t option

eval m t tries to evaluate term t in the model. If it succeeds, the value is returned, otherwise None is.

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base__Proof/index.html b/dev/sidekick-base/Sidekick_base__Proof/index.html index f9dbbaa4..ba0cbff0 100644 --- a/dev/sidekick-base/Sidekick_base__Proof/index.html +++ b/dev/sidekick-base/Sidekick_base__Proof/index.html @@ -1,2 +1,2 @@ -Sidekick_base__Proof (sidekick-base.Sidekick_base__Proof)

Module Sidekick_base__Proof

include Sidekick_core.PROOF with type term = Sidekick_base.Base_types.Term.t and type ty = Sidekick_base.Base_types.Ty.t
type term = Sidekick_base.Base_types.Term.t
type ty = Sidekick_base.Base_types.Ty.t
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
val isa_split : ty -> term Iter.t -> t
val isa_disj : ty -> term -> term -> t
val cstor_inj : Sidekick_base.Base_types.Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : string -> term list -> t
val ite_true : term -> t
val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t
\ No newline at end of file +Sidekick_base__Proof (sidekick-base.Sidekick_base__Proof)

Module Sidekick_base__Proof

Proofs of unsatisfiability

Proofs are used in sidekick when the problem is found unsatisfiable. A proof collects inferences made by the solver into a list of steps, each with its own kind of justification (e.g. "by congruence"), and outputs it in some kind of format.

Currently we target Quip as an experimental proof backend.

include Sidekick_core.PROOF with type term = Sidekick_base.Base_types.Term.t and type ty = Sidekick_base.Base_types.Ty.t
type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = Sidekick_base.Base_types.Term.t
type ty = Sidekick_base.Base_types.Ty.t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
val isa_split : ty -> term Iter.t -> t
val isa_disj : ty -> term -> term -> t
val cstor_inj : Sidekick_base.Base_types.Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : string -> term list -> t
val ite_true : term -> t
val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html index d0e3d0cc..4cc0efcf 100644 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-bin.Sidekick_smtlib.Process.Solver.P)

Module Solver.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick-bin.Sidekick_smtlib.Process.Solver.P)

Module Solver.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/P/index.html b/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/P/index.html index 0fb1fe98..9475f75e 100644 --- a/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/P/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-bin.Sidekick_smtlib__.Process.Solver.P)

Module Solver.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick-bin.Sidekick_smtlib__.Process.Solver.P)

Module Solver.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/P/index.html b/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/P/index.html index e07888ae..69381f76 100644 --- a/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/P/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-bin.Sidekick_smtlib__Process.Solver.P)

Module Solver.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick-bin.Sidekick_smtlib__Process.Solver.P)

Module Solver.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html index d939d561..bbafae09 100644 --- a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_arith_lra.Make.1-A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_arith_lra.Make.1-A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html index b29f97ac..77364ccc 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_arith_lra.ARG.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_arith_lra.ARG.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html index 614babc1..c90a4962 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_arith_lra.S.A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_arith_lra.S.A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/Make/argument-1-A/P/index.html b/dev/sidekick/Sidekick_cc/Make/argument-1-A/P/index.html index 4feead72..61864a0c 100644 --- a/dev/sidekick/Sidekick_cc/Make/argument-1-A/P/index.html +++ b/dev/sidekick/Sidekick_cc/Make/argument-1-A/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_cc.Make.1-A.P)

Module 1-A.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_cc.Make.1-A.P)

Module 1-A.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_cc/module-type-S/P/index.html b/dev/sidekick/Sidekick_cc/module-type-S/P/index.html index 6070c51e..7f236537 100644 --- a/dev/sidekick/Sidekick_cc/module-type-S/P/index.html +++ b/dev/sidekick/Sidekick_cc/module-type-S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_cc.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_cc.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html index ac77577e..7d5fde75 100644 --- a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html +++ b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.Monoid_of_repr.1-M.SI.P)

Module SI.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_core.Monoid_of_repr.1-M.SI.P)

Module SI.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : 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 f536239f..03dc282c 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:

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

module Fmt = CCFormat
module CC_view : sig ... end

View terms through the lens of the Congruence Closure

module type TERM = sig ... end

Main representation of Terms and Types

module type PROOF = sig ... end
module type LIT = sig ... end

Literals

module type CC_ACTIONS = sig ... end

Actions provided to the congruence closure.

module type CC_ARG = sig ... end

Arguments to a congruence closure's implementation

module type CC_S = sig ... end

Signature of the congruence closure

module type SOLVER_INTERNAL = sig ... end

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

module type SOLVER = sig ... end

User facing view of the solver

module type MONOID_ARG = sig ... end

Helper for the congruence closure

module Monoid_of_repr : functor (M : MONOID_ARG) -> sig ... end

State for a per-equivalence-class monoid.

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

Module Sidekick_core

Main Signatures

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

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

module Fmt = CCFormat
module CC_view : sig ... end

View terms through the lens of the Congruence Closure

module type TERM = sig ... end

Main representation of Terms and Types

module type PROOF = sig ... end

Proofs of unsatisfiability

module type LIT = sig ... end

Literals

module type CC_ACTIONS = sig ... end

Actions provided to the congruence closure.

module type CC_ARG = sig ... end

Arguments to a congruence closure's implementation

module type CC_S = sig ... end

Signature of the congruence closure

module type SOLVER_INTERNAL = sig ... end

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

module type SOLVER = sig ... end

User facing view of the solver

module type MONOID_ARG = sig ... end

Helper for the congruence closure

module Monoid_of_repr : functor (M : MONOID_ARG) -> sig ... end

State for a per-equivalence-class monoid.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/P/index.html b/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/P/index.html index 5a7a6d5c..0d9cf1d7 100644 --- a/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-CC_ACTIONS/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.CC_ACTIONS.P)

Module CC_ACTIONS.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_core.CC_ACTIONS.P)

Module CC_ACTIONS.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-CC_ARG/P/index.html b/dev/sidekick/Sidekick_core/module-type-CC_ARG/P/index.html index 9441160f..58d8a8bb 100644 --- a/dev/sidekick/Sidekick_core/module-type-CC_ARG/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-CC_ARG/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.CC_ARG.P)

Module CC_ARG.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_core.CC_ARG.P)

Module CC_ARG.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-CC_S/P/index.html b/dev/sidekick/Sidekick_core/module-type-CC_S/P/index.html index 1b168762..f18bc77c 100644 --- a/dev/sidekick/Sidekick_core/module-type-CC_S/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-CC_S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.CC_S.P)

Module CC_S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_core.CC_S.P)

Module CC_S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html index 9f69e926..36874c95 100644 --- a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.MONOID_ARG.SI.P)

Module SI.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_core.MONOID_ARG.SI.P)

Module SI.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-PROOF/index.html b/dev/sidekick/Sidekick_core/module-type-PROOF/index.html index bca500ec..ea545aa7 100644 --- a/dev/sidekick/Sidekick_core/module-type-PROOF/index.html +++ b/dev/sidekick/Sidekick_core/module-type-PROOF/index.html @@ -1,2 +1,2 @@ -PROOF (sidekick.Sidekick_core.PROOF)

Module type Sidekick_core.PROOF

type term
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +PROOF (sidekick.Sidekick_core.PROOF)

Module type Sidekick_core.PROOF

Proofs of unsatisfiability

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html index 76298c7e..316f0f0b 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.SOLVER.P)

Module SOLVER.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_core.SOLVER.P)

Module SOLVER.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html index 51dd2084..6d23b507 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.SOLVER_INTERNAL.P)

Module SOLVER_INTERNAL.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_core.SOLVER_INTERNAL.P)

Module SOLVER_INTERNAL.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_msat_solver/Make/argument-1-A/P/index.html b/dev/sidekick/Sidekick_msat_solver/Make/argument-1-A/P/index.html index 94c174fc..c478583f 100644 --- a/dev/sidekick/Sidekick_msat_solver/Make/argument-1-A/P/index.html +++ b/dev/sidekick/Sidekick_msat_solver/Make/argument-1-A/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_msat_solver.Make.1-A.P)

Module 1-A.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_msat_solver.Make.1-A.P)

Module 1-A.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_msat_solver/module-type-ARG/P/index.html b/dev/sidekick/Sidekick_msat_solver/module-type-ARG/P/index.html index 247949f5..127de243 100644 --- a/dev/sidekick/Sidekick_msat_solver/module-type-ARG/P/index.html +++ b/dev/sidekick/Sidekick_msat_solver/module-type-ARG/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_msat_solver.ARG.P)

Module ARG.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_msat_solver.ARG.P)

Module ARG.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_msat_solver/module-type-S/P/index.html b/dev/sidekick/Sidekick_msat_solver/module-type-S/P/index.html index 7c3a03cf..110a3949 100644 --- a/dev/sidekick/Sidekick_msat_solver/module-type-S/P/index.html +++ b/dev/sidekick/Sidekick_msat_solver/module-type-S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_msat_solver.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_msat_solver.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html index a336ce10..9a349065 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_bool_static.Make.1-A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_bool_static.Make.1-A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html index a985113b..20a41f01 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_bool_static.ARG.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_bool_static.ARG.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html index 40962730..73a6c8f0 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_bool_static.S.A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_bool_static.S.A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html index 73c6bc18..308d7a9a 100644 --- a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_cstor.Make.1-A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_cstor.Make.1-A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html index 81f512da..89e76dc1 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_cstor.ARG.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_cstor.ARG.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html index cc99f7a5..f71b6cf8 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_cstor.S.A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_cstor.S.A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html index 81376a72..9ac5fce3 100644 --- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_data.Make.1-A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_data.Make.1-A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html index 50f824ed..c576932b 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_data.ARG.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_data.ARG.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html index 9b8c0f37..c333bb88 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_data.S.A.S.P)

Module S.P

type term = T.Term.t
type ty
type t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file +P (sidekick.Sidekick_th_data.S.A.S.P)

Module S.P

type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type ty
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
\ No newline at end of file