Module AltErgoLib.Parsed_interface

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

Declaration of optimization of objective functions.

val mk_optimize : Loc.t -> Parsed.lexpr -> bool -> 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_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

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_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_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 -> Parsed.lexpr -> string -> Parsed.lexpr