Module Ics
module Ics: sig end
raise Sys.Break exception upon
val init : int * bool * string * Pervasives.in_channel * Format.formatter -> unit
| Parameters: |
|
(n,pp,eot,inch,outch) |
: |
int * bool * string * Pervasives.in_channel * Format.formatter
|
|
raise Sys.Break exception upon
user interrupt.
val do_at_exit : unit -> unit
Channels.
type inchannel = Pervasives.in_channel
type outchannel = Format.formatter
val channel_stdin : unit -> Pervasives.in_channel
val channel_stdout : unit -> Format.formatter
val channel_stderr : unit -> Format.formatter
val inchannel_of_string : string -> Pervasives.in_channel
val outchannel_of_string : string -> Format.formatter
type name = Name.t
val name_of_string : string -> Name.t
val name_to_string : Name.t -> string
val name_eq : Name.t -> Name.t -> bool
Constrains.
type cnstrnt = Sign.t
val cnstrnt_pp : Sign.t -> unit
val cnstrnt_mk_zero : unit -> Sign.t
val cnstrnt_mk_pos : unit -> Sign.t
val cnstrnt_mk_neg : unit -> Sign.t
val cnstrnt_mk_nonneg : unit -> Sign.t
val cnstrnt_mk_nonpos : unit -> Sign.t
val cnstrnt_is_empty : Sign.t -> bool
val cnstrnt_is_pos : Sign.t -> bool
val cnstrnt_is_neg : Sign.t -> bool
val cnstrnt_is_nonneg : Sign.t -> bool
val cnstrnt_is_nonpos : Sign.t -> bool
val cnstrnt_eq : Sign.t -> Sign.t -> bool
val cnstrnt_sub : Sign.t -> Sign.t -> bool
val cnstrnt_disjoint : Sign.t -> Sign.t -> bool
val cnstrnt_inter : Sign.t -> Sign.t -> Sign.t
Theories.
type th = int
val th_to_string : int -> string
val th_of_string : string -> int
Function symbols. These are partitioned into uninterpreted
function symbols and function symbols interpreted in one of the
builtin theories. For each interpreted function symbol there is
a recognizer function is_xxx. Some values of type sym represent
families of function symbols. The corresponding indices can be obtained
using the destructor d_xxx functions (only after checking that is_xxx
holds.
type sym = Sym.t
val sym_eq : Sym.t -> Sym.t -> bool
val sym_cmp : Sym.t -> Sym.t -> int
val sym_theory_of : Sym.t -> int
val sym_is_uninterp : Sym.t -> bool
val sym_d_uninterp : Sym.t -> Name.t
val sym_mk_num : Mpa.Q.t -> Sym.t
val sym_is_num : Sym.t -> bool
val sym_d_num : Sym.t -> Mpa.Q.t
val sym_mk_multq : Mpa.Q.t -> Sym.t
val sym_is_multq : Sym.t -> bool
val sym_d_multq : Sym.t -> Mpa.Q.t
val sym_mk_add : unit -> Sym.t
val sym_is_add : Sym.t -> bool
val sym_mk_cons : unit -> Sym.t
val sym_is_cons : Sym.t -> bool
val sym_mk_car : unit -> Sym.t
val sym_is_car : Sym.t -> bool
val sym_mk_cdr : unit -> Sym.t
val sym_is_cdr : Sym.t -> bool
val sym_mk_inl : unit -> Sym.t
val sym_is_inl : Sym.t -> bool
val sym_mk_inr : unit -> Sym.t
val sym_is_inr : Sym.t -> bool
val sym_mk_outl : unit -> Sym.t
val sym_is_outl : Sym.t -> bool
val sym_mk_outr : unit -> Sym.t
val sym_is_outr : Sym.t -> bool
val sym_mk_bv_const : string -> Sym.t
val sym_is_bv_const : Sym.t -> bool
val sym_mk_bv_conc : int -> int -> Sym.t
val sym_is_bv_conc : Sym.t -> bool
val sym_d_bv_conc : Sym.t -> int * int
val sym_mk_bv_sub : int -> int -> int -> Sym.t
val sym_is_bv_sub : Sym.t -> bool
val sym_d_bv_sub : Sym.t -> int * int * int
val sym_mk_bv_bitwise : int -> Sym.t
val sym_is_bv_bitwise : Sym.t -> bool
val sym_d_bv_bitwise : Sym.t -> int
val sym_mk_mult : unit -> Sym.t
val sym_is_mult : Sym.t -> bool
val sym_mk_expt : int -> Sym.t
val sym_is_expt : Sym.t -> bool
val sym_d_expt : Sym.t -> int
val sym_mk_apply : 'a -> Sym.t
val sym_is_apply : Sym.t -> bool
val sym_d_apply : Sym.t -> 'a option
val sym_mk_abs : unit -> Sym.t
val sym_is_abs : Sym.t -> bool
val sym_mk_update : unit -> Sym.t
val sym_is_select : Sym.t -> bool
val sym_mk_select : unit -> Sym.t
val sym_is_update : Sym.t -> bool
val sym_mk_unsigned : unit -> Sym.t
val sym_is_unsigned : Sym.t -> bool
Variables.
type var = Var.t
val var_name_of : Var.t -> Name.t
val var_eq : Var.t -> Var.t -> bool
val var_cmp : Var.t -> Var.t -> int
val var_mk_external : Name.t -> Var.t
val var_mk_bound : int -> Var.t
val var_is_external : Var.t -> bool
val var_is_bound : Var.t -> bool
val var_d_bound : Var.t -> int
Terms ar either variables, uninterpreted applications,
or interpreted applications including boolean terms.
type term = Term.t
val term_of_string : string -> Term.t
val term_to_string : Term.t -> string
val term_input : Pervasives.in_channel -> Term.t
| Parameters: |
|
ch |
: |
Pervasives.in_channel
|
|
val term_output : Format.formatter -> Term.t -> unit
val term_pp : Term.t -> unit
Construct a variable.
val term_mk_var : string -> Term.t
Uninterpred function application and function update.
val term_mk_uninterp : string -> Term.t list -> Term.t
Constructing arithmetic expressions.
val term_mk_num : Mpa.Q.t -> Term.t
val term_mk_multq : Mpa.Q.t -> Term.t -> Term.t
val term_mk_add : Term.t -> Term.t -> Term.t
val term_mk_addl : Term.t list -> Term.t
val term_mk_sub : Term.t -> Term.t -> Term.t
val term_mk_unary_minus : Term.t -> Term.t
val term_is_arith : Term.t -> bool
Constructing tuples and projections.
val term_mk_tuple : Term.t list -> Term.t
val term_mk_proj : int -> Term.t -> Term.t
Bitvector terms.
val term_mk_bvconst : string -> Term.t
val term_mk_bvsub : int * int * int -> Term.t -> Term.t
| Parameters: |
|
(n,i,j) |
: |
int * int * int
|
|
val term_mk_bvconc : int * int -> Term.t -> Term.t -> Term.t
val term_mk_bwite : int -> Term.t * Term.t * Term.t -> Term.t
val term_mk_bwand : int -> Term.t -> Term.t -> Term.t
val term_mk_bwor : int -> Term.t -> Term.t -> Term.t
val term_mk_bwnot : int -> Term.t -> Term.t
Boolean terms.
val term_mk_true : unit -> Term.t
val term_mk_false : unit -> Term.t
Coproducts.
val term_mk_inj : int -> Term.t -> Term.t
val term_mk_out : int -> Term.t -> Term.t
Interpretation Domains
type dom = Dom.t
Atoms.
type atom = Atom.t
val atom_pp : Atom.t -> unit
val atom_of_string : string -> Atom.t
val atom_to_string : Atom.t -> string
val atom_mk_equal : Term.t -> Term.t -> Atom.t
val atom_mk_diseq : Term.t -> Term.t -> Atom.t
val atom_mk_true : unit -> Atom.t
val atom_mk_false : unit -> Atom.t
val atom_mk_in : Term.t -> Sign.t -> Atom.t
val atom_mk_lt : Term.t -> Term.t -> Atom.t
val atom_mk_le : Term.t -> Term.t -> Atom.t
val atom_mk_gt : Term.t -> Term.t -> Atom.t
val atom_mk_ge : Term.t -> Term.t -> Atom.t
val atom_is_negatable : Atom.t -> bool
val atom_negate : Atom.t -> Atom.t
type atoms = Atom.Set.t
val atoms_empty : unit -> Atom.Set.t
val atoms_add : Atom.Set.elt -> Atom.Set.t -> Atom.Set.t
val atoms_singleton : Atom.Set.elt -> Atom.Set.t
val atoms_to_list : Atom.Set.t -> Atom.Set.elt list
val term_is_true : Term.t -> bool
val term_is_false : Term.t -> bool
Propositions
type prop = Prop.t
val prop_mk_true : unit -> Prop.t
val prop_mk_false : unit -> Prop.t
val prop_mk_var : Name.t -> Prop.t
val prop_mk_poslit : Atom.t -> Prop.t
val prop_mk_neglit : Atom.t -> Prop.t
val prop_mk_ite : Prop.t -> Prop.t -> Prop.t -> Prop.t
val prop_mk_conj : Prop.t list -> Prop.t
val prop_mk_disj : Prop.t list -> Prop.t
val prop_mk_iff : Prop.t -> Prop.t -> Prop.t
val prop_mk_neg : Prop.t -> Prop.t
type assignment = Prop.Assignment.t
val prop_sat : Context.t -> Prop.t -> Prop.Assignment.t option
Nonlinear terms.
val term_mk_mult : Term.t -> Term.t -> Term.t
val term_mk_multl : Term.t list -> Term.t
val term_mk_expt : int -> Term.t -> Term.t
Builtin applications.
val term_mk_unsigned : Term.t -> Term.t
val term_mk_update : Term.t -> Term.t -> Term.t -> Term.t
val term_mk_select : Term.t -> Term.t -> Term.t
val term_mk_div : Term.t -> Term.t -> Term.t
val term_mk_apply : Term.t -> Term.t list -> Term.t
Set of terms.
type terms = Term.Set.t
val terms_to_list : Term.Set.t -> Term.Set.elt list
val terms_of_list : Term.Set.elt list -> Term.Set.t
type 'a map = 'a Term.Map.t
Equalities.
val term_eq : Term.t -> Term.t -> bool
val term_cmp : Term.t -> Term.t -> int
Trace level.
type trace_level = string
val trace_reset : unit -> unit
val trace_add : Trace.level -> unit
val trace_remove : Trace.level -> unit
val trace_get : unit -> Trace.level list
Solution sets.
type solution = Solution.t
val solution_to_list : Solution.t -> (Term.t * Term.t) list
States.
type context = Context.t
val context_eq : Context.t -> Context.t -> bool
val context_empty : unit -> Context.t
val context_ctxt_of : Context.t -> Atom.Set.t
val context_use : int -> Context.t -> Term.t -> Term.Set.t
val context_inv : int -> Context.t -> Term.t -> Term.t
val context_find : int -> Context.t -> Term.t -> Term.t
val context_apply : int -> Context.t -> Term.t -> Term.t
val context_mem : int -> Context.t -> Term.t -> bool
val context_solution_of : Context.t -> int -> Solution.t
val context_pp : Context.t -> unit
val context_ctxt_pp : Context.t -> unit
Processing of new equalities.
type status = Context.t Context.Status.t
val is_consistent : 'a Context.Status.t -> bool
val is_redundant : 'a Context.Status.t -> bool
val is_inconsistent : 'a Context.Status.t -> bool
val d_consistent : Context.t Context.Status.t -> Context.t
val process : Context.t -> Atom.t -> Context.t Context.Status.t
val split : Context.t -> Atom.Set.elt list
Normalization functions
val can : Context.t -> Term.t -> Term.t
val read_from_channel : Pervasives.in_channel -> Result.t
| Parameters: |
|
ch |
: |
Pervasives.in_channel
|
|
val read_from_string : string -> Result.t
val cmd_rep : unit -> unit
val cmd_batch : unit -> unit
val cmd_output : Format.formatter -> Result.t -> unit
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
result |
: |
Result.t
|
|
val cmd_error : Format.formatter -> string -> unit
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
str |
: |
string
|
|
val cmd_quit : int -> Format.formatter -> unit
| Parameters: |
|
n |
: |
int
|
|
fmt |
: |
Format.formatter
|
|
val cmd_endmarker : Format.formatter -> unit
Abstract sign interpretation.
val cnstrnt : Context.t -> Term.t -> Sign.t
Tools
val reset : unit -> unit
val gc : unit -> unit
val flush : unit -> unit
Lists.
val is_nil : 'a list -> bool
val cons : 'a -> 'a list -> 'a list
val head : 'a list -> 'a
val tail : 'a list -> 'a list
Pairs.
val pair : 'a -> 'b -> 'a * 'b
val fst : 'a * 'b -> 'a
val snd : 'a * 'b -> 'b
Triples.
val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c
val fst_of_triple : 'a * 'b * 'c -> 'a
val snd_of_triple : 'a * 'b * 'c -> 'b
val third_of_triple : 'a * 'b * 'c -> 'c
Quadruples.
val fst_of_quadruple : 'a * 'b * 'c * 'd -> 'a
| Parameters: |
|
(x1,(),(),()) |
: |
'a * 'b * 'c * 'd
|
|
val snd_of_quadruple : 'a * 'b * 'c * 'd -> 'b
| Parameters: |
|
((),x2,(),()) |
: |
'a * 'b * 'c * 'd
|
|
val third_of_quadruple : 'a * 'b * 'c * 'd -> 'c
| Parameters: |
|
((),(),x3,()) |
: |
'a * 'b * 'c * 'd
|
|
val fourth_of_quadruple : 'a * 'b * 'c * 'd -> 'd
| Parameters: |
|
((),(),(),x4) |
: |
'a * 'b * 'c * 'd
|
|
Options.
val is_some : 'a option -> bool
val is_none : 'a option -> bool
val value_of : 'a option -> 'a
Sleeping.
val sleep : int -> unit
Multi-precision arithmetic.
type q = Mpa.Q.t
val ints_of_num : Mpa.Q.t -> string * string
val num_of_int : int -> Mpa.Q.t
val num_of_ints : int -> int -> Mpa.Q.t
val string_of_num : Mpa.Q.t -> string
val num_of_string : string -> Mpa.Q.t