Normalize and simplify

[felixL-K]

Trying to normalize some expr

[filipeom]

Some comments below. Regarding the issue with testing using these examples:

(set-logic QF_BVFP)
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ FloatingPoint 8 24))
(assert (= x ((_ fp.to_ubv 32) roundNearestTiesToEven y)))
(check-sat)

These are not working because the parser fails? I'm going to be working on fixing some issues in the parser. So I can take a look at these examples.

In any case, I don't think using the smtlib to test simplifications is the most easy thing to do. I'd actually recommend writing unit tests here: https://github.com/formalsec/smtml/blob/main/test/unit/test_expr.ml

For example you could use the formulas here for inspiration to try out some of the rules you wrote. For example, for these:

(f32.add
 (f32.add
   (f32.reinterpret_int (i32.reinterpret_float symbol_0)) 
   0.) 
 (f32.reinterpret_int (i32.reinterpret_float symbol_1))))

You could write:

let test_simplify_reinterpret_int _ =
  let open Infix in
  let sym_0 = symbol "symbol_0" (Ty_fp 32) in
  let lhs =
    Expr.binop (Ty_fp 32) Add 
      (Expr.cvtop (Ty_fp 32) Reinterpret_int 
        (Expr.cvtop (Ty_bitv 32) Reinterpret_float sym_0))
      (float32 0.)
   in
   let sym_1 = symbol "symbol_1" (Ty_fp 32) in
   let rhs =
      Expr.cvtop (Ty_fp 32) Reinterpret_int
        (Expr.cvtop (Ty_bitv 32) Reinterpret_float sym_0)
   in
   let result = Expr.binop (Ty_fp 32) Add lhs rhs in 
   let expected = Expr.binop (Ty_fp 32) Add sym_0 sym_1 in
   check result expected