Module `AltErgoLib.Symbols`

type builtin =

| LE
| LT
| IsConstr of Hstring.t

type operator =

| Plus
| Minus
| Mult
| Div
| Modulo
| Concat
| Extract
| Get
| Set
| Fixed
| Float
| Reach
| Access of Hstring.t
| Record
| Sqrt_real
| Abs_int
| Abs_real
| Real_of_int
| Int_floor
| Int_ceil
| Sqrt_real_default
| Sqrt_real_excess
| Min_real
| Min_int
| Max_real
| Max_int
| Integer_log2
| Pow
| Integer_round
| Constr of Hstring.t
| Destruct of Hstring.t * bool
| Tite

type lit =

| L_eq
| L_built of builtin
| L_neg_eq
| L_neg_built of builtin
| L_neg_pred

type form =

| F_Unit of bool
| F_Clause of bool
| F_Iff
| F_Xor
| F_Lemma
| F_Skolem

type name_kind =

| Ac
| Other

type bound_kind =

| VarBnd of Var.t
| ValBnd of Numbers.Q.t

type bound = private {

kind : bound_kind;
sort : Ty.t;
is_open : bool;
is_lower : bool;

}

type t =

| True
| False
| Void
| Name of Hstring.t * name_kind
| Int of Hstring.t
| Real of Hstring.t
| Bitv of string
| Op of operator
| Lit of lit
| Form of form
| Var of Var.t
| In of bound * bound
| MapsTo of Var.t
| Let

val name : ?kind:name_kind -> string -> t

val var : Var.t -> t

val underscore : t

val int : string -> t

val real : string -> t

val constr : string -> t

val destruct : guarded:bool -> string -> t

val mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound

val mk_in : bound -> bound -> t

val mk_maps_to : Var.t -> t

val is_ac : t -> bool

val equal : t -> t -> bool

val compare : t -> t -> int

val compare_bounds : bound -> bound -> int

val hash : t -> int

val to_string : t -> string

val print : Format.formatter -> t -> unit

val to_string_clean : t -> string

val print_clean : Format.formatter -> t -> unit

val fresh : ?is_var:bool -> string -> t

val is_get : t -> bool

val is_set : t -> bool

val fake_eq : t

val fake_neq : t

val fake_lt : t

val fake_le : t

val add_label : Hstring.t -> t -> unit

val label : t -> Hstring.t

val print_bound : Format.formatter -> bound -> unit

val string_of_bound : bound -> string

module Set : Set.S with type elt = t

module Map : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alt-ergo-lib/AltErgoLib/Symbols/index.html

Module `AltErgoLib.Symbols`

package alt-ergo-lib

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alt-ergo-lib/AltErgoLib/Symbols/index.html

Module AltErgoLib.Symbols

Module `AltErgoLib.Symbols`