Module Binsec_smtlib.FormulaSource

include module type of struct include Formula end
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 Binsec_base.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 Binsec_base.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
  6. | Custom of custom_desc
and custom_desc = ..

An user defined entry.

Custom entry support is experimental and very limited. For now, it will work only for formula creation (no transformation) and printing (and by extension, call to external SMT solver).

type custom_handler = {
  1. hash : custom_desc -> int option;
  2. pp : Format.formatter -> custom_desc -> bool;
}
val register_custom : custom_handler -> unit

register_custom { hash; pp } registers a hash and a pretty printer functions for custom entries.

The hash function should return Some h for the custom entries the handler supports, None otherwise. The pretty printer should print the entry without the surrounding parenthesis and return true for the custom entries the handler supports, false otherwise.

Handlers will be scanned in the reverse order of the call to the register_custom function. Using a custom entry without any registered handler will raise Invalid_custom.

exception Invalid_custom

An exception raised by a function that can not handle a custom entry, either because no hander has been registered for this entry or because the function does not support entry extension.

type entry = private {
  1. entry_hash : int;
  2. entry_desc : entry_desc;
}
type formula = private {
  1. entries : entry Binsec_base.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 : Binsec_base.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 Binsec_base.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 : sig ... end
module BlVarSet : sig ... end
module BvVarSet : sig ... end
module AxVarSet : sig ... end
module BlVarHashtbl : sig ... end
module BvVarHashtbl : sig ... end
module AxVarHashtbl : sig ... end
module BlTermHashtbl : sig ... end
module BvTermHashtbl : sig ... end
module AxTermHashtbl : sig ... end

This module aim at generating well formatted smtlib2 formulas, taking in account some solvers differences (e.g: boolector not supporting function have arrays in parameters). All the strings generated by this module are smtlib 2 compliant.

val pp_status : Format.formatter -> Formula.status -> unit

pretty print the smt_result with a given color

val print_status : Formula.status -> string
  • returns

    the string associated with a smt_result

val print_bv_unop : Formula.bv_unop -> string
  • returns

    the string of an unary bitvector expression

val print_bv_bnop : Formula.bv_bnop -> string
  • returns

    the string of a binary bitvector expression

val print_bv_comp : Formula.bv_comp -> string
  • returns

    the string of a binary bitvector expression

val print_bv_term : Formula.bv_term -> string
  • returns

    the string of a bitvector expression.

val print_ax_term : Formula.ax_term -> string

see print_bv_term

val print_bl_term : Formula.bl_term -> string

see print_bv_term

val print_varset : Formula.VarSet.t -> string
  • returns

    the string formatting every input variable on a new line

val pp_varset : Format.formatter -> Formula.VarSet.t -> unit
val print_header : theory:string -> unit -> string
  • returns

    the preformatted header

val pp_header : theory:string -> Format.formatter -> unit -> unit
val pp_as_comment : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
val pp_bl_term : Format.formatter -> Formula.bl_term -> unit
val pp_bv_term : Format.formatter -> Formula.bv_term -> unit
val pp_ax_term : Format.formatter -> Formula.ax_term -> unit
val pp_term : Format.formatter -> Formula.term -> unit
val pp_entry : Format.formatter -> Formula.entry -> unit
val pp_formula : Format.formatter -> Formula.formula -> unit
module To_smtlib : sig ... end

Translation functions from BINSEC inner representation to SMT-LIB terms

module Transformation : sig ... end
module Model : sig ... end

Internal model representation

module Solver : sig ... end

Interface with SMT solvers

module Utils : sig ... end

Utility functions for formula creation

module Logger : sig ... end