Module Formula_type

module Formula_type: sig .. end
alias to string Map

module SymbVar: Basic_types.String.Map
type formula_entry = 
| Comment of string
| VarDefinition of Smtlib2.smt_expr * Smtlib2.smt_expr * Smtlib2.smt_expr list (*
Variable reified in smt_expr, expression, attached constraints
*)
| Constraint of Smtlib2.smt_expr
the three different kind of entries in the path predicate:
type path_t = formula_entry list 
Path predicate type
type input_t = Smtlib2.SmtVarSet.t 
type hybrid_mem_chunk = {
   base : Smtlib2.smt_bv_expr;
   name : string;
   mapping : Smtlib2.smt_bv_expr Basic_types.Addr64.Map.t;
}
structure used for the RoW hybrid. It represent each chunk of memory having the same base
type hybrid_mem_t = hybrid_mem_chunk list 
any hybrid memory (just a list of chunks)
type formula = {
   vars : (int * int * Smtlib2.smt_bv_expr) SymbVar.t;
   varsindex : int SymbVar.t;
   path : path_t;
   memory : Smtlib2.smt_abv_expr;
   inputs : input_t;
   addr_size : int;
   nb_input : int;
   nb_load : int;
   nb_store : int;
   nb_let : int;
   nb_op : int;
   nb_constraint : int;
   global_counter : int;
   optim_cst_prop : bool;
   optim_rebase : bool;
   aux_optim_rebase : bool;
   optim_row : bool;
   optim_row_k : int;
   optim_rowplus : bool;
   hybrid_memory : hybrid_mem_t;
   optim_eq_prop : bool;
   optim_map : (int * (Smtlib2.smt_expr * Smtlib2.smt_expr * Smtlib2.smt_expr list))
SymbVar.t
;
   pushed_variable : Basic_types.String.Set.t;
   last_constraint : Smtlib2.smt_expr;
}
SMT formula as represented internally
val empty_formula : ?cst_pro:bool ->
?rebase:bool ->
?row:bool ->
?aux_rebase:bool ->
?row_plus:bool -> ?eq_prop:bool -> int -> formula
create an empty formula
val to_stringmap : Smtlib2.SmtVarSet.t -> Basic_types.String.Set.t