Module Binsec.Formula

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