module Formula_optim:`sig`

..`end`

Formula optimizations

Functions trying to propagate constants on the
given expression.

`val propagate_cst : ``Formula_type.formula ->`

?recursive:int -> Smtlib2.smt_expr -> Smtlib2.smt_expr

`val propagate_cst_bv : ``Formula_type.formula ->`

?recursive:int -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr

`val propagate_cst_abv : ``Formula_type.formula ->`

?recursive:int -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr

In the formula all the variables are in a SSA
form. The rebase optimization will intent to
redefine variables used in the expression by
older variables declaration eg:
esp1 := esp0 + 4
esp2 := esp1 + 4
esp3 := esp2 + 4 => esp2+4 will be replaced by esp1+8
thus obsolating the esp2 declaration. This reduce
the number of variables defined and is crucial for some
other optimizations

`val rebase_expr : ``Formula_type.formula -> Smtlib2.smt_expr -> Smtlib2.smt_expr`

`val rebase_bvexpr : ``Formula_type.formula -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr`

`val rebase_abvexpr : ``Formula_type.formula -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr`

The Read-Over-Write as an array theory optimization
based on the fact that read(store(M, addr, X),addr) = X.
Thus the optimization will try for every read to replace
it by its store value (if any). To do so the classic linear
method look in the store chain if the read address has
previously been written. The hybrid method does the same
but in a more efficient manner.

`val get_row_stats : ``unit -> int * int * int * int * int * int`

- min number of iteration for the lookup
- max number of iteration for the lookup
- moy number of iteration for the lookup
- found number of read replaced
- rebase number of read rebased on an older memory
- disjoint others

`val read_over_write : ``Formula_type.formula -> Smtlib2.smt_expr -> Smtlib2.smt_expr`

`val read_over_write_bv : ``Formula_type.formula -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr`

`val read_over_write_abv : ``Formula_type.formula -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr`

`val update_hybrid_memory : ``Formula_type.formula ->`

string ->

Smtlib2.smt_abv_expr -> Formula_type.hybrid_mem_t * Smtlib2.smt_abv_expr

`val read_over_write_hybrid : ``Formula_type.formula -> Smtlib2.smt_expr -> Smtlib2.smt_expr`

`val read_over_write_hybrid_bv : ``Formula_type.formula -> Smtlib2.smt_bv_expr -> Smtlib2.smt_bv_expr`

`val read_over_write_hybrid_abv : ``Formula_type.formula -> Smtlib2.smt_abv_expr -> Smtlib2.smt_abv_expr`

We call memory flattening the act of removing
every array operations in the specific cases
where all select/store are being made on constant
addresses. This allows to generate formulas "solvable"
by solvers not supporting the SMT array theory

class memory_flattener_visitor :`object`

..`end`

Class that remove all read in memory by constant
bitvector values