From b41a23e427b001f377988e1ee8e6736f4c694735 Mon Sep 17 00:00:00 2001 From: c-cube Date: Sun, 4 Jul 2021 05:30:10 +0000 Subject: [PATCH] deploy: 0368a29ada89c791946169624776389cfb6db32b --- dev/sidekick-base/Sidekick_base/Base_types/Fun/index.html | 2 +- dev/sidekick-base/Sidekick_base/Base_types/Term/index.html | 2 +- dev/sidekick-base/Sidekick_base/index.html | 2 +- dev/sidekick-base/Sidekick_base__/Base_types/Fun/index.html | 2 +- dev/sidekick-base/Sidekick_base__/Base_types/Term/index.html | 2 +- dev/sidekick-base/Sidekick_base__Base_types/Fun/index.html | 2 +- dev/sidekick-base/Sidekick_base__Base_types/Term/index.html | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) 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 9ee78438..089dd2f3 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

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

Possible definitions for a function symbol

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

A function symbol

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

Make a new uninterpreted function.

val mk_undef' : ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : ID.t -> Ty.t -> t

Make a new uninterpreted constant.

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

user defined function symbol. A good example can be found in Form for boolean connectives.

Possible definitions for a function symbol

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

A function symbol

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

Make a new uninterpreted function.

val mk_undef' : ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : ID.t -> Ty.t -> t

Make a new uninterpreted constant.

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/Term/index.html b/dev/sidekick-base/Sidekick_base/Base_types/Term/index.html index 6d6b30f9..25204471 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
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 +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 app_fun_l : store -> fun_ -> t list -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val app_undefined : store -> ID.t -> Ty.Fun.t -> t Sidekick_util.IArray.t -> t

app_undefined store f ty args is app store (Fun.mk_undef f ty) args. It builds a function symbol and applies it into a term immediately

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

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

val 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/index.html b/dev/sidekick-base/Sidekick_base/index.html index baf37ea8..fc43c844 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

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 Form : sig ... end

Formulas (boolean terms).

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.store = Term.store

Concrete implementation of Sidekick_core.TERM

\ 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 Form : sig ... end

Formulas (boolean terms).

module IArray = Sidekick_util.IArray
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.store = Term.store

Concrete implementation of Sidekick_core.TERM

\ 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 8f3aff8e..0259ac66 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

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

Possible definitions for a function symbol

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

A function symbol

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

Make a new uninterpreted function.

val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t

Make a new uninterpreted constant.

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

user defined function symbol. A good example can be found in Form for boolean connectives.

Possible definitions for a function symbol

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

A function symbol

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

Make a new uninterpreted function.

val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t

Make a new uninterpreted constant.

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/Term/index.html b/dev/sidekick-base/Sidekick_base__/Base_types/Term/index.html index 75e345f6..b1510f90 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
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 +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 app_fun_l : store -> fun_ -> t list -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val app_undefined : store -> Sidekick_base.ID.t -> Ty.Fun.t -> t Sidekick_util.IArray.t -> t

app_undefined store f ty args is app store (Fun.mk_undef f ty) args. It builds a function symbol and applies it into a term immediately

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

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

val 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/Fun/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Fun/index.html index f19f6d13..5c1bcb2c 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

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

Possible definitions for a function symbol

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

A function symbol

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

Make a new uninterpreted function.

val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t

Make a new uninterpreted constant.

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

user defined function symbol. A good example can be found in Form for boolean connectives.

Possible definitions for a function symbol

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

A function symbol

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

Make a new uninterpreted function.

val mk_undef' : Sidekick_base.ID.t -> Ty.t list -> Ty.t -> t
val mk_undef_const : Sidekick_base.ID.t -> Ty.t -> t

Make a new uninterpreted constant.

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/Term/index.html b/dev/sidekick-base/Sidekick_base__Base_types/Term/index.html index 892d8f43..11ccf27d 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
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 +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 app_fun_l : store -> fun_ -> t list -> t
val eq : store -> t -> t -> t
val not_ : store -> t -> t
val ite : store -> t -> t -> t -> t
val app_undefined : store -> Sidekick_base.ID.t -> Ty.Fun.t -> t Sidekick_util.IArray.t -> t

app_undefined store f ty args is app store (Fun.mk_undef f ty) args. It builds a function symbol and applies it into a term immediately

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

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

val 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