Module `AltErgoLib.Parsed_interface`Source

Declaration of types *

Sourceval 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

Source

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

Source

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

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

Declaration of symbols, functions, predicates, and goals

Source

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

Source

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

Source

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

Source

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

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

Declaration of theories, generic axioms and rewriting rules *

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

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

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

Declaration of theory axioms and case-splits *

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

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

Making pure and logic types

Sourceval int_type : Parsed.ppure_type

Sourceval bool_type : Parsed.ppure_type

Sourceval real_type : Parsed.ppure_type

Sourceval unit_type : Parsed.ppure_type

Sourceval mk_bitv_type : string -> Parsed.ppure_type

Source

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

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

Source

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

Making arithmetic expressions and predicates *

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

Sourceval mk_real_const : Loc.t -> Num.num -> Parsed.lexpr

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

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

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

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

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

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

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

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

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

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

Making Record expressions *

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

Source

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

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

Making Array expressions *

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

Source

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

Making Bit-vector expressions *

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

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

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

Making Boolean / Propositional expressions *

Sourceval mk_true_const : Loc.t -> Parsed.lexpr

Sourceval mk_false_const : Loc.t -> Parsed.lexpr

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

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

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

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

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

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

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

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

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

Making quantified formulas *

Source

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

Source

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 *

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

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

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

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

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

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

Source

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

Source

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

Sourceval mk_void : Loc.t -> Parsed.lexpr

Making particular expression used in semantic triggers *

Source

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

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

Making cuts and checks *

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

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

Source

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

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

Source

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

package alt-ergo-lib

Module AltErgoLib.Parsed_interfaceSource

Module `AltErgoLib.Parsed_interface`Source