package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type

Definition of abstract representation for logical formulas (based on SMTLIB's syntax and semantics)

type status =
  1. | SAT
  2. | UNSAT
  3. | TIMEOUT
  4. | UNKNOWN
val status_to_exit_code : status -> int
type bl_unop =
  1. | BlNot
type bl_bnop =
  1. | BlImply
  2. | BlAnd
  3. | BlOr
  4. | BlXor
type bl_comp =
  1. | BlEqual
  2. | BlDistinct
type bv_unop =
  1. | BvNot
  2. | BvNeg
  3. | BvRepeat of int
  4. | BvZeroExtend of int
    (*

    result has size: `size_of(bv) + int` *

    *)
  5. | BvSignExtend of int
  6. | BvRotateLeft of int
  7. | BvRotateRight of int
  8. | BvExtract of int Interval.t
type bv_bnop =
  1. | BvConcat
  2. | BvAnd
  3. | BvNand
  4. | BvOr
  5. | BvNor
  6. | BvXor
  7. | BvXnor
  8. | BvCmp
  9. | BvAdd
  10. | BvSub
  11. | BvMul
  12. | BvUdiv
  13. | BvSdiv
  14. | BvUrem
  15. | BvSrem
  16. | BvSmod
  17. | BvShl
  18. | BvAshr
  19. | BvLshr
type bv_comp =
  1. | BvEqual
  2. | BvDistinct
  3. | BvUlt
  4. | BvUle
  5. | BvUgt
  6. | BvUge
  7. | BvSlt
  8. | BvSle
  9. | BvSgt
  10. | BvSge
type ax_comp =
  1. | AxEqual
  2. | AxDistinct
type sort =
  1. | BlSort
  2. | BvSort of int
  3. | AxSort of int * int
type bl_var = private {
  1. bl_hash : int;
  2. bl_name : string;
}
type bv_var = private {
  1. bv_hash : int;
  2. bv_name : string;
  3. bv_size : int;
}
type ax_var = private {
  1. ax_hash : int;
  2. ax_name : string;
  3. idx_size : int;
  4. elt_size : int;
}
type var =
  1. | BlVar of bl_var
  2. | BvVar of bv_var
  3. | AxVar of ax_var
type term_desc =
  1. | BlTerm of bl_term
  2. | BvTerm of bv_term
  3. | AxTerm of ax_term
and term = private {
  1. term_hash : int;
  2. term_desc : term_desc;
}
and bl_term_desc =
  1. | BlTrue
  2. | BlFalse
  3. | BlFun of bl_var * term list
  4. | BlLet of def list * bl_term
  5. | BlUnop of bl_unop * bl_term
  6. | BlBnop of bl_bnop * bl_term * bl_term
  7. | BlComp of bl_comp * bl_term * bl_term
  8. | BvComp of bv_comp * bv_term * bv_term
  9. | AxComp of ax_comp * ax_term * ax_term
  10. | BlIte of bl_term * bl_term * bl_term
and bl_term = private {
  1. bl_term_hash : int;
  2. bl_term_desc : bl_term_desc;
}
and bv_term_desc =
  1. | BvCst of Bitvector.t
  2. | BvFun of bv_var * term list
  3. | BvLet of def list * bv_term
  4. | BvUnop of bv_unop * bv_term
  5. | BvBnop of bv_bnop * bv_term * bv_term
  6. | BvIte of bl_term * bv_term * bv_term
  7. | Select of int * ax_term * bv_term
and bv_term = private {
  1. bv_term_hash : int;
  2. bv_term_desc : bv_term_desc;
  3. bv_term_size : int;
}
and ax_term_desc =
  1. | AxFun of ax_var * term list
  2. | AxLet of def list * ax_term
  3. | AxIte of bl_term * ax_term * ax_term
  4. | Store of int * ax_term * bv_term * bv_term
and ax_term = private {
  1. ax_term_hash : int;
  2. ax_term_desc : ax_term_desc;
  3. idx_term_size : int;
  4. elt_term_size : int;
}
and def_desc =
  1. | BlDef of bl_var * decl list * bl_term
  2. | BvDef of bv_var * decl list * bv_term
  3. | AxDef of ax_var * decl list * ax_term
and def = private {
  1. def_hash : int;
  2. def_desc : def_desc;
}
and decl_desc =
  1. | BlDecl of bl_var * sort list
  2. | BvDecl of bv_var * sort list
  3. | AxDecl of ax_var * sort list
and decl = private {
  1. decl_hash : int;
  2. decl_desc : decl_desc;
}
type entry_desc =
  1. | Declare of decl
  2. | Define of def
  3. | Assert of bl_term
  4. | Assume of bl_term
  5. | Comment of string
type entry = private {
  1. entry_hash : int;
  2. entry_desc : entry_desc;
}
type formula = private {
  1. entries : entry Sequence.t;
}
val empty : formula
val length : formula -> int
val append : formula -> formula -> formula
val push_front : entry -> formula -> formula
val push_back : entry -> formula -> formula
val peek_front : formula -> entry option
val peek_back : formula -> entry option
val pop_front : formula -> formula option
val pop_back : formula -> formula option
val map_forward : (entry -> entry) -> formula -> formula
val map_backward : (entry -> entry) -> formula -> formula
val iter_forward : (entry -> unit) -> formula -> unit
val iter_backward : (entry -> unit) -> formula -> unit
val fold_forward : (entry -> 'a -> 'a) -> formula -> 'a -> 'a
val fold_backward : (entry -> 'a -> 'a) -> formula -> 'a -> 'a
val push_front_declare : decl -> formula -> formula
val push_front_define : def -> formula -> formula
val push_front_assert : bl_term -> formula -> formula
val push_front_assume : bl_term -> formula -> formula
val push_front_comment : string -> formula -> formula
val push_back_declare : decl -> formula -> formula
val push_back_define : def -> formula -> formula
val push_back_assert : bl_term -> formula -> formula
val push_back_assume : bl_term -> formula -> formula
val push_back_comment : string -> formula -> formula
module Printing : sig ... end

Basic printing of formulas

val equal_bl_term : bl_term -> bl_term -> bool
val equal_bv_term : bv_term -> bv_term -> bool
val equal_ax_term : ax_term -> ax_term -> bool
val bl_sort : sort
val bv_sort : int -> sort
val ax_sort : int -> int -> sort
val bl_var : string -> bl_var
val bv_var : string -> int -> bv_var
val ax_var : string -> int -> int -> ax_var
val term : term_desc -> term
val bl_term : bl_term_desc -> bl_term
val bv_term : bv_term_desc -> bv_term
val ax_term : ax_term_desc -> ax_term
val def : def_desc -> def
val decl : decl_desc -> decl
val entry : entry_desc -> entry
val mk_bl_term : bl_term -> term
val mk_bv_term : bv_term -> term
val mk_ax_term : ax_term -> term
val mk_bl_true : bl_term
val mk_bl_false : bl_term
val mk_bl_var : bl_var -> bl_term
val mk_bl_fun : bl_var -> term list -> bl_term
val mk_bl_let : def list -> bl_term -> bl_term
val mk_bl_unop : bl_unop -> bl_term -> bl_term
val mk_bl_bnop : bl_bnop -> bl_term -> bl_term -> bl_term
val mk_bl_comp : bl_comp -> bl_term -> bl_term -> bl_term
val mk_bv_comp : bv_comp -> bv_term -> bv_term -> bl_term
val mk_ax_comp : ax_comp -> ax_term -> ax_term -> bl_term
val mk_bl_ite : bl_term -> bl_term -> bl_term -> bl_term
val mk_bv_cst : Bitvector.t -> bv_term
val mk_bv_var : bv_var -> bv_term
val mk_bv_fun : bv_var -> term list -> bv_term
val mk_bv_let : def list -> bv_term -> bv_term
val mk_bv_unop : bv_unop -> bv_term -> bv_term
val mk_bv_bnop : bv_bnop -> bv_term -> bv_term -> bv_term
val mk_bv_ite : bl_term -> bv_term -> bv_term -> bv_term
val mk_select : int -> ax_term -> bv_term -> bv_term
val mk_ax_var : ax_var -> ax_term
val mk_ax_fun : ax_var -> term list -> ax_term
val mk_ax_let : def list -> ax_term -> ax_term
val mk_ax_ite : bl_term -> ax_term -> ax_term -> ax_term
val mk_store : int -> ax_term -> bv_term -> bv_term -> ax_term
val mk_bl_def : bl_var -> decl list -> bl_term -> def
val mk_bv_def : bv_var -> decl list -> bv_term -> def
val mk_ax_def : ax_var -> decl list -> ax_term -> def
val mk_bl_decl : bl_var -> sort list -> decl
val mk_bv_decl : bv_var -> sort list -> decl
val mk_ax_decl : ax_var -> sort list -> decl
val mk_declare : decl -> entry
val mk_define : def -> entry
val mk_assert : bl_term -> entry
val mk_assume : bl_term -> entry
val mk_comment : string -> entry
val mk_bl_not : bl_term -> bl_term
val mk_bv_not : bv_term -> bv_term
val mk_bv_neg : bv_term -> bv_term
val mk_bv_repeat : int -> bv_term -> bv_term
val mk_bv_zero_extend : int -> bv_term -> bv_term
val mk_bv_sign_extend : int -> bv_term -> bv_term
val mk_bv_rotate_left : int -> bv_term -> bv_term
val mk_bv_rotate_right : int -> bv_term -> bv_term
val mk_bv_extract : int Interval.t -> bv_term -> bv_term
val mk_bl_imply : bl_term -> bl_term -> bl_term
val mk_bl_and : bl_term -> bl_term -> bl_term
val mk_bl_or : bl_term -> bl_term -> bl_term
val mk_bl_xor : bl_term -> bl_term -> bl_term
val mk_bv_concat : bv_term -> bv_term -> bv_term
val mk_bv_and : bv_term -> bv_term -> bv_term
val mk_bv_nand : bv_term -> bv_term -> bv_term
val mk_bv_or : bv_term -> bv_term -> bv_term
val mk_bv_nor : bv_term -> bv_term -> bv_term
val mk_bv_xor : bv_term -> bv_term -> bv_term
val mk_bv_xnor : bv_term -> bv_term -> bv_term
val mk_bv_cmp : bv_term -> bv_term -> bv_term
val mk_bv_add : bv_term -> bv_term -> bv_term
val mk_bv_sub : bv_term -> bv_term -> bv_term
val mk_bv_mul : bv_term -> bv_term -> bv_term
val mk_bv_udiv : bv_term -> bv_term -> bv_term
val mk_bv_sdiv : bv_term -> bv_term -> bv_term
val mk_bv_urem : bv_term -> bv_term -> bv_term
val mk_bv_srem : bv_term -> bv_term -> bv_term
val mk_bv_smod : bv_term -> bv_term -> bv_term
val mk_bv_shl : bv_term -> bv_term -> bv_term
val mk_bv_ashr : bv_term -> bv_term -> bv_term
val mk_bv_lshr : bv_term -> bv_term -> bv_term
val mk_bl_equal : bl_term -> bl_term -> bl_term
val mk_bl_distinct : bl_term -> bl_term -> bl_term
val mk_bv_equal : bv_term -> bv_term -> bl_term
val mk_bv_distinct : bv_term -> bv_term -> bl_term
val mk_ax_equal : ax_term -> ax_term -> bl_term
val mk_ax_distinct : ax_term -> ax_term -> bl_term
val mk_bv_ult : bv_term -> bv_term -> bl_term
val mk_bv_ule : bv_term -> bv_term -> bl_term
val mk_bv_ugt : bv_term -> bv_term -> bl_term
val mk_bv_uge : bv_term -> bv_term -> bl_term
val mk_bv_slt : bv_term -> bv_term -> bl_term
val mk_bv_sle : bv_term -> bv_term -> bl_term
val mk_bv_sgt : bv_term -> bv_term -> bl_term
val mk_bv_sge : bv_term -> bv_term -> bl_term
val mk_bv_zero : bv_term
val mk_bv_one : bv_term
val mk_bv_zeros : int -> bv_term
val mk_bv_ones : int -> bv_term
val mk_bv_fill : int -> bv_term
val mk_bv_add_int : bv_term -> int -> bv_term
val mk_bv_sub_int : bv_term -> int -> bv_term
module VarSet : Set.S with type elt = var
module BlVarSet : Set.S with type elt = bl_var
module BvVarSet : Set.S with type elt = bv_var
module AxVarSet : Set.S with type elt = ax_var
module BlVarHashtbl : Hashtbl.S with type key = bl_var
module BvVarHashtbl : Hashtbl.S with type key = bv_var
module AxVarHashtbl : Hashtbl.S with type key = ax_var
module BlTermHashtbl : Hashtbl.S with type key = bl_term
module BvTermHashtbl : Hashtbl.S with type key = bv_term
module AxTermHashtbl : Hashtbl.S with type key = ax_term
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