Module Smtml.Rewrite

Module that performs two 'important' rewritings:

1. Replace symbols' Ty_none with the correct type specified in declare-const.

2. Propagate the correct theory encoding for Unop, Binop, Relop, and Triop.

3. Inlines Let_in binders into a single big expr

module Symb_map : sig ... end
val debug : ('a, Format.formatter, unit) format -> ('a -> unit) -> unit
val unify_types : Ty.t list -> Ty.t
val rewrite_ty : Ty.t -> Ty.t list -> Ty.t
val rewrite_expr : (Ty.t Symb_map.t * Expr.t Symb_map.t) -> Expr.t -> Expr.t

Propagates types in type_map and inlines Let_in binders

val rewrite_cmd : Ty.t Symb_map.t -> Ast.t -> Ty.t Symb_map.t * Ast.t

Acccumulates types of symbols in type_map and calls rewrite_expr

val rewrite : Ast.t list -> Ast.t list