package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type
val symbol_of_svar : Smtlib.sorted_var -> Smtlib.symbol

Extracts the symbol part out of the declaration of a sorted variable.

val sort_of_svar : Smtlib.sorted_var -> Smtlib.sort

Extracts the sort part out of the declaration of a sorted variable.

val symbol_of_vbinding : Smtlib.var_binding -> Smtlib.symbol

Extracts the newly defined symbol part out of a variable binding.

val symbols_of_sort : Smtlib.sort -> Smtlib.symbol list
val string_of_symbol : Smtlib.symbol -> string
val get_logic : Smtlib.script -> string

Extracts the logic name from a SMT script

id_from_qid qid extracts the id part of a qualified identifier

val is_constant_term : Smtlib.term -> bool

is_constant t checks if the term t is a constant or not. * A real constant might be hidden under an annotated term.

val is_variable_term : Smtlib.term -> bool

is_variable t checks if the term t is possibly a variable or not.

Creation functions

val mk_symbol : string -> Smtlib.symbol

mk_symbol name creates a dummy symbol for name

val mk_localized_symbol : string -> Location.t -> Smtlib.symbol
val mk_idx_num : int -> Smtlib.index
val mk_id_symbol : Smtlib.symbol -> Smtlib.identifier
val mk_id_underscore : Smtlib.symbol -> Smtlib.indexes -> Smtlib.identifier
val mk_qual_identifier_identifier : Smtlib.identifier -> Smtlib.qual_identifier
val mk_sorted_var : Smtlib.symbol -> Smtlib.sort -> Smtlib.sorted_var
val mk_var_binding : Smtlib.symbol -> Smtlib.term -> Smtlib.var_binding
val mk_sort_identifier : Smtlib.symbol -> Smtlib.sort
val mk_sort_fun : Smtlib.symbol -> Smtlib.sorts -> Smtlib.sort
val mk_term_spec_constant : Smtlib.constant -> Smtlib.term
val mk_term_qual_identifier : Smtlib.qual_identifier -> Smtlib.term
val mk_term_qual_identifier_terms : Smtlib.qual_identifier -> Smtlib.terms -> Smtlib.term
val mk_term_let_term : Smtlib.var_bindings -> Smtlib.term -> Smtlib.term
val mk_term_forall_term : Smtlib.sorted_vars -> Smtlib.term -> Smtlib.term
val mk_term_exists_term : Smtlib.sorted_vars -> Smtlib.term -> Smtlib.term
val mk_cmd_declare_fun : Smtlib.symbol -> Smtlib.sorts -> Smtlib.sort -> Smtlib.command
val mk_cmd_define_fun : Smtlib.fun_def -> Smtlib.command

mk_command cmd_des creates a command with a dummy location

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