package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

alt-ergo-lib
- AltErgoLib
  - Ac
    
    Make
    
    X
    
    S
  - Adt
    
    ALIEN
    
    Shostak
    
    X
  - Adt_rel
  - Arith
    
    Shostak
    
    P
    
    X
    
    Type
    
    X
  - Arrays
    
    ALIEN
    
    Shostak
    
    X
  - Arrays_rel
  - Bitv
    
    ALIEN
    
    Shostak
    
    X
  - Bitv_rel
  - Ccx
    
    Main
    
    S
  - Cnf
  - Commands
  - Compat
    
    Seq
    
    String
  - D_cnf
  - D_loop
    
    Header
    
    Parser
    
    Pipeline
    
    Typer
    
    Typer_Pipe
  - Emap
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Enum
    
    ALIEN
    
    Shostak
    
    X
  - Enum_rel
  - Errors
  - Explanation
  - Expr
    
    BV
    
    Core
    
    Ints
  - Fpa_rounding
  - Frontend
    
    Make
    
    SAT
    
    S
  - Fun_sat
    
    Make
    
    Th
  - Gc_debug
  - Hconsing
    
    HASHED
    
    Make
    
    H
    
    S
  - Hstring
  - Iheap
  - Inequalities
    
    Container_SIG
    
    Make
    
    MINEQS
    
    P
    
    FM
    
    MINEQS
    
    P
    
    S
    
    MINEQS
    
    P
  - Input
    
    S
  - Instances
    
    Make
    
    X
    
    S
  - IntervalCalculus
  - Intervals
  - Ite
    
    ALIEN
    
    Shostak
    
    X
  - Ite_rel
  - Lists
  - Loc
  - Matching
    
    Arg
    
    Make
    
    X
    
    S
  - Matching_types
  - ModelMap
  - Models
  - MyUnix
  - My_zip
  - Numbers
    
    Q
    
    Z
  - Options
    
    Output
    
    Time
  - Parsed
  - Parsed_interface
  - Polynome
    
    EXTENDED_Polynome
    
    Make
    
    X
    
    S
    
    T
  - Printer
  - Profiling
  - Records
    
    ALIEN
    
    Shostak
    
    X
  - Records_rel
  - Relation
  - Sat_solver
  - Sat_solver_sig
    
    S
    
    SatContainer
    
    Make
    
    Th
  - Satml
    
    Make
    
    Th
    
    SAT_ML
  - Satml_frontend
    
    Make
    
    Th
  - Satml_frontend_hybrid
    
    Make
    
    Th
  - Satml_types
    
    ATOM
    
    Atom
    
    FLAT_FORMULA
    
    Flat_Formula
    
    Proxy_formula
  - Shostak
    
    Ac
    
    Adt
    
    Arith
    
    Arrays
    
    Bitv
    
    Combine
    
    Enum
    
    Ite
    
    Polynome
    
    Records
  - Sig
    
    SHOSTAK
    
    X
  - Sig_rel
    
    RELATION
  - Steps
  - Symbols
    
    Map
  - Th_util
  - Theories
  - Theory
    
    Main_Default
    
    Main_Empty
    
    S
  - Timers
  - Ty
  - Typechecker
  - Typed
  - Uf
    
    LX
  - Use
  - Util
  - Var
  - Vec
  - Version
  - Xliteral
    
    Make
    
    X
    
    OrderedType
    
    S

Legend:
Library
Module
Module type
Parameter
Class
Class type

Declaration of types *

val mk_abstract_type_decl : Loc.t -> string list -> string -> Parsed.decl

val mk_enum_type_decl : 
  Loc.t ->
  string list ->
  string ->
  string list ->
  Parsed.decl

val mk_algebraic_type_decl : 
  Loc.t ->
  string list ->
  string ->
  (string * (string * Parsed.ppure_type) list) list ->
  Parsed.decl

val mk_record_type_decl : 
  Loc.t ->
  string list ->
  string ->
  ?constr:string ->
  (string * Parsed.ppure_type) list ->
  Parsed.decl

val mk_rec_type_decl : Parsed.type_decl list -> Parsed.decl

Declaration of symbols, functions, predicates, and goals

val mk_logic : 
  Loc.t ->
  Symbols.name_kind ->
  (string * string) list ->
  Parsed.plogic_type ->
  Parsed.decl

val mk_function_def : 
  Loc.t ->
  (string * string) ->
  (Loc.t * string * Parsed.ppure_type) list ->
  Parsed.ppure_type ->
  Parsed.lexpr ->
  Parsed.decl

val mk_ground_predicate_def : 
  Loc.t ->
  (string * string) ->
  Parsed.lexpr ->
  Parsed.decl

val mk_non_ground_predicate_def : 
  Loc.t ->
  (string * string) ->
  (Loc.t * string * Parsed.ppure_type) list ->
  Parsed.lexpr ->
  Parsed.decl

val mk_mut_rec_def : 
  (Loc.t
   * (string * string)
   * (Loc.t * string * Parsed.ppure_type) list
   * Parsed.ppure_type option
   * Parsed.lexpr)
    list ->
  Parsed.decl

val mk_goal : Loc.t -> string -> Parsed.lexpr -> Parsed.decl

val mk_check_sat : Loc.t -> string -> Parsed.lexpr -> Parsed.decl

Declaration of theories, generic axioms and rewriting rules *

val mk_theory : Loc.t -> string -> string -> Parsed.decl list -> Parsed.decl

val mk_generic_axiom : Loc.t -> string -> Parsed.lexpr -> Parsed.decl

val mk_rewriting : Loc.t -> string -> Parsed.lexpr list -> Parsed.decl

Declaration of theory axioms and case-splits *

val mk_theory_axiom : Loc.t -> string -> Parsed.lexpr -> Parsed.decl

val mk_theory_case_split : Loc.t -> string -> Parsed.lexpr -> Parsed.decl

Declaration of stack assertions commands

val mk_push : Loc.t -> int -> Parsed.decl

val mk_pop : Loc.t -> int -> Parsed.decl

Making pure and logic types

val int_type : Parsed.ppure_type

val bool_type : Parsed.ppure_type

val real_type : Parsed.ppure_type

val unit_type : Parsed.ppure_type

val mk_bitv_type : string -> Parsed.ppure_type

val mk_external_type : 
  Loc.t ->
  Parsed.ppure_type list ->
  string ->
  Parsed.ppure_type

val mk_var_type : Loc.t -> string -> Parsed.ppure_type

val mk_logic_type : 
  Parsed.ppure_type list ->
  Parsed.ppure_type option ->
  Parsed.plogic_type

Making arithmetic expressions and predicates *

val mk_int_const : Loc.t -> string -> Parsed.lexpr

val mk_real_const : Loc.t -> Numbers.Q.t -> Parsed.lexpr

val mk_add : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_sub : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_mul : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_div : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_mod : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_pow_int : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_pow_real : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_minus : Loc.t -> Parsed.lexpr -> Parsed.lexpr

val mk_pred_lt : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_pred_le : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_pred_gt : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_pred_ge : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

Making Record expressions *

val mk_record : Loc.t -> (string * Parsed.lexpr) list -> Parsed.lexpr

val mk_with_record : 
  Loc.t ->
  Parsed.lexpr ->
  (string * Parsed.lexpr) list ->
  Parsed.lexpr

val mk_dot_record : Loc.t -> Parsed.lexpr -> string -> Parsed.lexpr

Making Array expressions *

val mk_array_get : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_array_set : 
  Loc.t ->
  Parsed.lexpr ->
  Parsed.lexpr ->
  Parsed.lexpr ->
  Parsed.lexpr

Making Bit-vector expressions *

val mk_bitv_const : Loc.t -> string -> Parsed.lexpr

val mk_bitv_extract : Loc.t -> Parsed.lexpr -> string -> string -> Parsed.lexpr

val mk_bitv_concat : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

Making Boolean / Propositional expressions *

val mk_true_const : Loc.t -> Parsed.lexpr

val mk_false_const : Loc.t -> Parsed.lexpr

val mk_and : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_or : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_xor : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_iff : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_implies : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_not : Loc.t -> Parsed.lexpr -> Parsed.lexpr

val mk_distinct : Loc.t -> Parsed.lexpr list -> Parsed.lexpr

val mk_pred_eq : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

val mk_pred_not_eq : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

Making quantified formulas *

val mk_forall : 
  Loc.t ->
  (string * string * Parsed.ppure_type) list ->
  (Parsed.lexpr list * bool) list ->
  Parsed.lexpr list ->
  Parsed.lexpr ->
  Parsed.lexpr

val mk_exists : 
  Loc.t ->
  (string * string * Parsed.ppure_type) list ->
  (Parsed.lexpr list * bool) list ->
  Parsed.lexpr list ->
  Parsed.lexpr ->
  Parsed.lexpr

Naming and casting types of expressions *

val mk_type_cast : Loc.t -> Parsed.lexpr -> Parsed.ppure_type -> Parsed.lexpr

val mk_named : Loc.t -> string -> Parsed.lexpr -> Parsed.lexpr

Making vars, applications, if-then-else, and let expressions *

val mk_var : Loc.t -> string -> Parsed.lexpr

val mk_application : Loc.t -> string -> Parsed.lexpr list -> Parsed.lexpr

val mk_pattern : Loc.t -> string -> string list -> Parsed.pattern

val mk_ite : 
  Loc.t ->
  Parsed.lexpr ->
  Parsed.lexpr ->
  Parsed.lexpr ->
  Parsed.lexpr

val mk_let : 
  Loc.t ->
  (string * Parsed.lexpr) list ->
  Parsed.lexpr ->
  Parsed.lexpr

val mk_void : Loc.t -> Parsed.lexpr

Making particular expression used in semantic triggers *

val mk_in_interval : 
  Loc.t ->
  Parsed.lexpr ->
  bool ->
  Parsed.lexpr ->
  Parsed.lexpr ->
  bool ->
  Parsed.lexpr

val mk_maps_to : Loc.t -> string -> Parsed.lexpr -> Parsed.lexpr

Making cuts and checks *

val mk_check : Loc.t -> Parsed.lexpr -> Parsed.lexpr

val mk_cut : Loc.t -> Parsed.lexpr -> Parsed.lexpr

val mk_match : 
  Loc.t ->
  Parsed.lexpr ->
  (Parsed.pattern * Parsed.lexpr) list ->
  Parsed.lexpr

val mk_algebraic_test : Loc.t -> Parsed.lexpr -> string -> Parsed.lexpr

val mk_algebraic_project : 
  Loc.t ->
  guarded:bool ->
  Parsed.lexpr ->
  string ->
  Parsed.lexpr