Module Formula

module Formula: sig .. end
SMT Formula manipulation module

val get_varindex : Formula_type.formula -> string -> int
Returns the current index for the given variable
val add_comment : Formula_type.formula -> string -> Formula_type.formula
Add a comment in in the formula (considered as a command)
val contains_variable : Formula_type.formula -> string -> bool
Returns true if the formula contains a variable named with the given string
val add_initial_state : Formula_type.formula -> int Basic_types.Addr64.Map.t -> Formula_type.formula
Initialize the memory with all the values given in the map
val add_symbolic_input : Formula_type.formula -> string -> int -> Formula_type.formula
add_symbolic_input name size add a new bitvector in the formula.
val add_constraint : Formula_type.formula -> Smtlib2.smt_expr -> Formula_type.formula
add the given smt_expr as constraint in the formula

_comment is unused in the body of this function

val build_formula_incremental : Formula_type.formula ->
Smtlib2.smt_expr ->
?ksteps:int ->
?forward:bool ->
?pruning:bool ->
?push:bool ->
?file:string ->
Solver.solver_session ->
Common_piqi.solver_t -> Formula_type.formula * Smtlib2.smt_result option
build_formula_incremental pred ~ksteps ~forward ~pruning ~push ~file session solver
val build_formula_file : Formula_type.formula ->
Smtlib2.smt_expr ->
?ksteps:int ->
?forward:bool ->
?pruning:bool ->
string ->
Common_piqi.solver_t -> Formula_type.formula * Smtlib2.smt_result option
same as build_formula_file but provide a file name in which to output the generated formula
val new_tmpvar : Formula_type.formula -> int -> Formula_type.formula * Smtlib2.smt_bv_expr
create unique temporary variable in the formula
val optim_str : Formula_type.formula -> string
getting a string code representing the optimizations activated in the formula
val store_memory : Formula_type.formula ->
?constraints:Smtlib2.smt_expr list ->
Smtlib2.smt_abv_expr -> Formula_type.formula
store_memory ~constraints abv_expr add a new store in memory add optionally attach some additional ~constraints constraints to it
val change_variable : Formula_type.formula ->
string ->
int ->
int ->
int ->
?constraints:Smtlib2.smt_expr list ->
Smtlib2.smt_bv_expr -> Formula_type.formula
main function to change a variable value in the formula. change_variable name size low high ~csts expr:
val get_var_or_create : Formula_type.formula ->
string -> int -> int -> int -> Formula_type.formula * Smtlib2.smt_bv_expr
get a variable logical expression or create it if not existing. get_var_or_create name fullsize low high(see change_variable).
Returns the formula modified and the logical value of the variable
val new_variable_name : Formula_type.formula -> string -> string * Formula_type.formula
get a new variable name for a given variable (eg. if internal eax value is eax10 returns eax11)
val pp_stat_formula : Formula_type.formula -> unit
print the logical store of a formula (all the variables)