diff --git a/dev/sidekick-base/Sidekick_base/Base_types/Term/LRA/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Term/LRA/index.html new file mode 100644 index 00000000..77ba7300 --- /dev/null +++ b/dev/sidekick-base/Sidekick_base/Base_types/Term/LRA/index.html @@ -0,0 +1,2 @@ + +LRA (sidekick-base.Sidekick_base.Base_types.Term.LRA)

Module Term.LRA

Helpers for LRA

val plus : store -> t -> t -> t
val minus : store -> t -> t -> t
val mult : store -> Q.t -> t -> t
val const : store -> Q.t -> t
val leq : store -> t -> t -> t
val lt : store -> t -> t -> t
val geq : store -> t -> t -> t
val gt : store -> t -> t -> t
val eq : store -> t -> t -> t
val neq : store -> t -> t -> t
\ 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 bc8422f3..6d6b30f9 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

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 store
val create : ?⁠size:int -> unit -> store
val make : store -> t view -> t
val true_ : store -> t
val false_ : store -> t
val bool : store -> bool -> t
val const : store -> fun_ -> t
val app_fun : store -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val const_undefined_fun : store -> ID.t -> Ty.Fun.t -> t

const_undefined_fun store f ty is const store (Fun.mk_undef f ty). It builds a function symbol and turns it into a term immediately

val const_undefined_const : store -> ID.t -> Ty.t -> t

const_undefined_const store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.

val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : store -> cstor -> t -> t
val lra : store -> (Q.t, t) lra_view -> t
val abs : store -> 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 : store -> (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

Store

val store_size : store -> int
val store_iter : store -> term Iter.t

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 store
val create : ?⁠size:int -> unit -> store
val make : store -> t view -> t
val true_ : store -> t
val false_ : store -> t
val bool : store -> bool -> t
val const : store -> fun_ -> t
val app_fun : store -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val const_undefined_fun : store -> ID.t -> Ty.Fun.t -> t

const_undefined_fun store f ty is const store (Fun.mk_undef f ty). It builds a function symbol and turns it into a term immediately

val const_undefined_const : store -> ID.t -> Ty.t -> t

const_undefined_const store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.

val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : store -> cstor -> t -> t
val lra : store -> (Q.t, t) lra_view -> t
module LRA : sig ... end

Helpers for LRA

val abs : store -> 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 : store -> (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

Store

val store_size : store -> int
val store_iter : store -> term Iter.t

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/Term/LRA/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Term/LRA/index.html new file mode 100644 index 00000000..bc8713b0 --- /dev/null +++ b/dev/sidekick-base/Sidekick_base__/Base_types/Term/LRA/index.html @@ -0,0 +1,2 @@ + +LRA (sidekick-base.Sidekick_base__.Base_types.Term.LRA)

Module Term.LRA

Helpers for LRA

val plus : store -> t -> t -> t
val minus : store -> t -> t -> t
val mult : store -> Q.t -> t -> t
val const : store -> Q.t -> t
val leq : store -> t -> t -> t
val lt : store -> t -> t -> t
val geq : store -> t -> t -> t
val gt : store -> t -> t -> t
val eq : store -> t -> t -> t
val neq : store -> t -> t -> t
\ 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 4b586607..75e345f6 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

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 store
val create : ?⁠size:int -> unit -> store
val make : store -> t view -> t
val true_ : store -> t
val false_ : store -> t
val bool : store -> bool -> t
val const : store -> fun_ -> t
val app_fun : store -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val const_undefined_fun : store -> Sidekick_base.ID.t -> Ty.Fun.t -> t

const_undefined_fun store f ty is const store (Fun.mk_undef f ty). It builds a function symbol and turns it into a term immediately

val const_undefined_const : store -> Sidekick_base.ID.t -> Ty.t -> t

const_undefined_const store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.

val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : store -> cstor -> t -> t
val lra : store -> (Q.t, t) lra_view -> t
val abs : store -> 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 : store -> (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

Store

val store_size : store -> int
val store_iter : store -> term Iter.t

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 store
val create : ?⁠size:int -> unit -> store
val make : store -> t view -> t
val true_ : store -> t
val false_ : store -> t
val bool : store -> bool -> t
val const : store -> fun_ -> t
val app_fun : store -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val const_undefined_fun : store -> Sidekick_base.ID.t -> Ty.Fun.t -> t

const_undefined_fun store f ty is const store (Fun.mk_undef f ty). It builds a function symbol and turns it into a term immediately

val const_undefined_const : store -> Sidekick_base.ID.t -> Ty.t -> t

const_undefined_const store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.

val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : store -> cstor -> t -> t
val lra : store -> (Q.t, t) lra_view -> t
module LRA : sig ... end

Helpers for LRA

val abs : store -> 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 : store -> (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

Store

val store_size : store -> int
val store_iter : store -> term Iter.t

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/Term/LRA/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Term/LRA/index.html new file mode 100644 index 00000000..501b3442 --- /dev/null +++ b/dev/sidekick-base/Sidekick_base__Base_types/Term/LRA/index.html @@ -0,0 +1,2 @@ + +LRA (sidekick-base.Sidekick_base__Base_types.Term.LRA)

Module Term.LRA

Helpers for LRA

val plus : store -> t -> t -> t
val minus : store -> t -> t -> t
val mult : store -> Q.t -> t -> t
val const : store -> Q.t -> t
val leq : store -> t -> t -> t
val lt : store -> t -> t -> t
val geq : store -> t -> t -> t
val gt : store -> t -> t -> t
val eq : store -> t -> t -> t
val neq : store -> t -> t -> t
\ 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 22e0c81d..892d8f43 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

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 store
val create : ?⁠size:int -> unit -> store
val make : store -> t view -> t
val true_ : store -> t
val false_ : store -> t
val bool : store -> bool -> t
val const : store -> fun_ -> t
val app_fun : store -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val const_undefined_fun : store -> Sidekick_base.ID.t -> Ty.Fun.t -> t

const_undefined_fun store f ty is const store (Fun.mk_undef f ty). It builds a function symbol and turns it into a term immediately

val const_undefined_const : store -> Sidekick_base.ID.t -> Ty.t -> t

const_undefined_const store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.

val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : store -> cstor -> t -> t
val lra : store -> (Q.t, t) lra_view -> t
val abs : store -> 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 : store -> (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

Store

val store_size : store -> int
val store_iter : store -> term Iter.t

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 store
val create : ?⁠size:int -> unit -> store
val make : store -> t view -> t
val true_ : store -> t
val false_ : store -> t
val bool : store -> bool -> t
val const : store -> fun_ -> t
val app_fun : store -> fun_ -> t Sidekick_util.IArray.t -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val const_undefined_fun : store -> Sidekick_base.ID.t -> Ty.Fun.t -> t

const_undefined_fun store f ty is const store (Fun.mk_undef f ty). It builds a function symbol and turns it into a term immediately

val const_undefined_const : store -> Sidekick_base.ID.t -> Ty.t -> t

const_undefined_const store f ty is const store (Fun.mk_undef_const f ty). It builds a constant function symbol and makes it into a term immediately.

val select : store -> select -> t -> t
val app_cstor : store -> cstor -> t Sidekick_util.IArray.t -> t
val is_a : store -> cstor -> t -> t
val lra : store -> (Q.t, t) lra_view -> t
module LRA : sig ... end

Helpers for LRA

val abs : store -> 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 : store -> (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

Store

val store_size : store -> int
val store_iter : store -> term Iter.t

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