package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install

Dune Dependency

alt-ergo.ocamlpro.com Readme LicenseRef-OCamlPro-Non-Commercial-Purpose-License-Version-1 License Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. A
    Alt-Ergo developers

Sources

2.4.1.tar.gz
md5=35d6c6f3fa43bcd10fe7f524b1eb59ca
sha512=c3eee41d3c588ca89c2a1eebe9f10914ef647743b58fb562b682172cf6b6bdeb0920ebbba8a850820c0cb53bad0260f11b82fe71f00830ea9b33f5bb5d4fd048

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

Module AltErgoLib.Parsed_interfaceSource

Declaration of types *

Sourceval mk_abstract_type_decl : Loc.t -> string list -> string -> Parsed.decl
Sourceval mk_enum_type_decl : Loc.t -> string list -> string -> string list -> Parsed.decl
Sourceval mk_algebraic_type_decl : Loc.t -> string list -> string -> (string * (string * Parsed.ppure_type) list) list -> Parsed.decl
Sourceval 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

Sourceval mk_logic : Loc.t -> Symbols.name_kind -> (string * string) list -> Parsed.plogic_type -> Parsed.decl
Sourceval mk_function_def : Loc.t -> (string * string) -> (Loc.t * string * Parsed.ppure_type) list -> Parsed.ppure_type -> Parsed.lexpr -> Parsed.decl
Sourceval mk_ground_predicate_def : Loc.t -> (string * string) -> Parsed.lexpr -> Parsed.decl
Sourceval 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

Declaration of stack assertions commands

Sourceval mk_push : Loc.t -> int -> Parsed.decl
Sourceval mk_pop : Loc.t -> int -> Parsed.decl

Making pure and logic types

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
Sourceval mk_external_type : Loc.t -> Parsed.ppure_type list -> string -> Parsed.ppure_type
Sourceval mk_var_type : Loc.t -> string -> Parsed.ppure_type
Sourceval 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

Making Record expressions *

Sourceval mk_record : Loc.t -> (string * Parsed.lexpr) list -> Parsed.lexpr
Sourceval 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 *

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_distinct : Loc.t -> Parsed.lexpr list -> Parsed.lexpr
Sourceval mk_pred_not_eq : Loc.t -> Parsed.lexpr -> Parsed.lexpr -> Parsed.lexpr

Making quantified formulas *

Sourceval mk_forall : Loc.t -> (string * string * Parsed.ppure_type) list -> (Parsed.lexpr list * bool) list -> Parsed.lexpr list -> Parsed.lexpr -> Parsed.lexpr
Sourceval 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_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
Sourceval 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 *

Sourceval 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_algebraic_test : Loc.t -> Parsed.lexpr -> string -> Parsed.lexpr
Sourceval mk_algebraic_project : Loc.t -> guarded:bool -> Parsed.lexpr -> string -> Parsed.lexpr
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct